I don't see how you got from 3) S cannot prove that A won't play chicken to 4) S cannot prove that A()=B(). That inference seems way too general; it should apply to any agent of this type. In particular, S certainly can prove that A()=A(). Perhaps 3 is supposed to break some symmetry between A and B? Perhaps I wasn't clear that I wanted B to play chicken, too. That restores the symmetry, if that's what the point of 4 was.

I also think that there is a subtle gap in 5 => 6. If S could prove that all of A's actions imply B's defection, then S could prove that B defects, hence contradiction. But A's decision doesn't need to examine all of A's actions: crying can be omitted. I doubt that this actually helps, though.