set f1 = and2a ;
set f2 = and2c ;
set f3 = nor2 ;
set f0 = xor2c ;
let x, y, z be set ; :: thesis: ( z <> [<*x,y*>,xor2c] & x <> [<*y,z*>,and2c] & y <> [<*z,x*>,nor2] & z <> [<*x,y*>,and2a] implies for s being State of (BitGFA2Circ (x,y,z)) holds Following (s,2) is stable )
assume that
A1: z <> [<*x,y*>,xor2c] and
A2: ( x <> [<*y,z*>,and2c] & y <> [<*z,x*>,nor2] & z <> [<*x,y*>,and2a] ) ; :: thesis: for s being State of (BitGFA2Circ (x,y,z)) holds Following (s,2) is stable
set A = BitGFA2Circ (x,y,z);
let s be State of (BitGFA2Circ (x,y,z)); :: thesis: Following (s,2) is stable
set S2 = GFA2CarryStr (x,y,z);
set S1 = GFA2AdderStr (x,y,z);
InputVertices (GFA2AdderStr (x,y,z)) = {x,y,z} by A1, FACIRC_1:57;
then A3: InputVertices (GFA2AdderStr (x,y,z)) = InputVertices (GFA2CarryStr (x,y,z)) by A2, Th77;
set A1 = GFA2AdderCirc (x,y,z);
reconsider s1 = s | the carrier of (GFA2AdderStr (x,y,z)) as State of (GFA2AdderCirc (x,y,z)) by FACIRC_1:26;
Following (s1,2) is stable by A1, FACIRC_1:63;
then A4: Following (s1,2) = Following (Following (s1,2))
.= Following (s1,(2 + 1)) by FACIRC_1:12 ;
set A2 = GFA2CarryCirc (x,y,z);
reconsider s2 = s | the carrier of (GFA2CarryStr (x,y,z)) as State of (GFA2CarryCirc (x,y,z)) by FACIRC_1:26;
Following (s2,2) is stable by A2, Th86;
then A5: Following (s2,2) = Following (Following (s2,2))
.= Following (s2,(2 + 1)) by FACIRC_1:12 ;
reconsider t = s as State of ((GFA2AdderCirc (x,y,z)) +* (GFA2CarryCirc (x,y,z))) ;
set S = BitGFA2Str (x,y,z);
A6: dom (Following (s,3)) = the carrier of (BitGFA2Str (x,y,z)) by CIRCUIT1:3;
InnerVertices (GFA2CarryStr (x,y,z)) misses InputVertices (GFA2CarryStr (x,y,z)) by XBOOLE_1:79;
then A7: ( Following (s1,2) = (Following (t,2)) | the carrier of (GFA2AdderStr (x,y,z)) & Following (s1,3) = (Following (t,3)) | the carrier of (GFA2AdderStr (x,y,z)) ) by A3, FACIRC_1:30;
InnerVertices (GFA2AdderStr (x,y,z)) misses InputVertices (GFA2AdderStr (x,y,z)) by XBOOLE_1:79;
then A8: ( Following (s2,2) = (Following (t,2)) | the carrier of (GFA2CarryStr (x,y,z)) & Following (s2,3) = (Following (t,3)) | the carrier of (GFA2CarryStr (x,y,z)) ) by A3, FACIRC_1:31;
A9: the carrier of (BitGFA2Str (x,y,z)) = the carrier of (GFA2AdderStr (x,y,z)) \/ the carrier of (GFA2CarryStr (x,y,z)) by CIRCCOMB:def 2;
A10: ( dom (Following (s1,2)) = the carrier of (GFA2AdderStr (x,y,z)) & dom (Following (s2,2)) = the carrier of (GFA2CarryStr (x,y,z)) ) by CIRCUIT1:3;

A11: now :: thesis: for a being object st a in the carrier of (BitGFA2Str (x,y,z)) holds
(Following (s,2)) . a = (Following (Following (s,2))) . a

let a be object ; :: thesis: ( a in the carrier of (BitGFA2Str (x,y,z)) implies (Following (s,2)) . a = (Following (Following (s,2))) . a )
assume a in the carrier of (BitGFA2Str (x,y,z)) ; :: thesis: (Following (s,2)) . a = (Following (Following (s,2))) . a
then ( a in the carrier of (GFA2AdderStr (x,y,z)) or a in the carrier of (GFA2CarryStr (x,y,z)) ) by A9, XBOOLE_0:def 3;
then ( ( (Following (s,2)) . a = (Following (s1,2)) . a & (Following (s,3)) . a = (Following (s1,3)) . a ) or ( (Following (s,2)) . a = (Following (s2,2)) . a & (Following (s,3)) . a = (Following (s2,3)) . a ) ) by A7, A8, A4, A5, A10, FUNCT_1:47;
hence (Following (s,2)) . a = (Following (Following (s,2))) . a by A4, A5, FACIRC_1:12; :: thesis: verum

end;

( Following (s,(2 + 1)) = Following (Following (s,2)) & dom (Following (s,2)) = the carrier of (BitGFA2Str (x,y,z)) ) by CIRCUIT1:3, FACIRC_1:12;
hence Following (s,2) = Following (Following (s,2)) by A6, A11, FUNCT_1:2; :: according to CIRCUIT2:def 6 :: thesis: verum