theorem Th84: :: GFACIRC1:84

for x, y, z being set
for s being State of (GFA2CarryCirc (x,y,z))
for a1, a2, a3 being Element of BOOLEAN st a1 = s . [<*x,y*>,and2a] & a2 = s . [<*y,z*>,and2c] & a3 = s . [<*z,x*>,nor2] holds
(Following s) . (GFA2CarryOutput (x,y,z)) = 'not' ((a1 'or' a2) 'or' a3)