for x, y, c being object
for f being Function of (2 -tuples_on BOOLEAN),BOOLEAN
for s being State of (2GatesCircuit (x,y,c,f)) st c <> [<*x,y*>,f] holds
( (Following (s,2)) . (2GatesCircOutput (x,y,c,f)) = f . <*(f . <*(s . x),(s . y)*>),(s . c)*> & (Following (s,2)) . [<*x,y*>,f] = f . <*(s . x),(s . y)*> & (Following (s,2)) . x = s . x & (Following (s,2)) . y = s . y & (Following (s,2)) . c = s . c )