theorem Th64: :: FACIRC_1:64

for x, y, c being object st c <> [<*x,y*>,'xor'] holds
for s being State of (2GatesCircuit (x,y,c,'xor'))
for a1, a2, a3 being Element of BOOLEAN st a1 = s . x & a2 = s . y & a3 = s . c holds
(Following (s,2)) . (2GatesCircOutput (x,y,c,'xor')) = (a1 'xor' a2) 'xor' a3