set f1 = and2 ;
set f2 = and2 ;
set f3 = and2 ;
set f0 = xor2 ;
let x, y, z be set ; :: thesis: ( z <> [<*x,y*>,xor2] & x <> [<*y,z*>,and2] & y <> [<*z,x*>,and2] & z <> [<*x,y*>,and2] implies for s being State of (BitGFA0Circ (x,y,z)) holds Following (s,2) is stable )
assume that
A1: z <> [<*x,y*>,xor2] and
A2: ( x <> [<*y,z*>,and2] & y <> [<*z,x*>,and2] & z <> [<*x,y*>,and2] ) ; :: thesis: for s being State of (BitGFA0Circ (x,y,z)) holds Following (s,2) is stable
set A = BitGFA0Circ (x,y,z);
let s be State of (BitGFA0Circ (x,y,z)); :: thesis: Following (s,2) is stable
set S2 = GFA0CarryStr (x,y,z);
set S1 = GFA0AdderStr (x,y,z);
InputVertices (GFA0AdderStr (x,y,z)) = {x,y,z} by A1, FACIRC_1:57;
then A3: InputVertices (GFA0AdderStr (x,y,z)) = InputVertices (GFA0CarryStr (x,y,z)) by A2, Th14;
set A1 = GFA0AdderCirc (x,y,z);
reconsider s1 = s | the carrier of (GFA0AdderStr (x,y,z)) as State of (GFA0AdderCirc (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 = GFA0CarryCirc (x,y,z);
reconsider s2 = s | the carrier of (GFA0CarryStr (x,y,z)) as State of (GFA0CarryCirc (x,y,z)) by FACIRC_1:26;
Following (s2,2) is stable by A2, Th23;
then A5: Following (s2,2) = Following (Following (s2,2))
.= Following (s2,(2 + 1)) by FACIRC_1:12 ;
reconsider t = s as State of ((GFA0AdderCirc (x,y,z)) +* (GFA0CarryCirc (x,y,z))) ;
set S = BitGFA0Str (x,y,z);
A6: dom (Following (s,3)) = the carrier of (BitGFA0Str (x,y,z)) by CIRCUIT1:3;
InnerVertices (GFA0CarryStr (x,y,z)) misses InputVertices (GFA0CarryStr (x,y,z)) by XBOOLE_1:79;
then A7: ( Following (s1,2) = (Following (t,2)) | the carrier of (GFA0AdderStr (x,y,z)) & Following (s1,3) = (Following (t,3)) | the carrier of (GFA0AdderStr (x,y,z)) ) by A3, FACIRC_1:30;
InnerVertices (GFA0AdderStr (x,y,z)) misses InputVertices (GFA0AdderStr (x,y,z)) by XBOOLE_1:79;
then A8: ( Following (s2,2) = (Following (t,2)) | the carrier of (GFA0CarryStr (x,y,z)) & Following (s2,3) = (Following (t,3)) | the carrier of (GFA0CarryStr (x,y,z)) ) by A3, FACIRC_1:31;
A9: the carrier of (BitGFA0Str (x,y,z)) = the carrier of (GFA0AdderStr (x,y,z)) \/ the carrier of (GFA0CarryStr (x,y,z)) by CIRCCOMB:def 2;
A10: ( dom (Following (s1,2)) = the carrier of (GFA0AdderStr (x,y,z)) & dom (Following (s2,2)) = the carrier of (GFA0CarryStr (x,y,z)) ) by CIRCUIT1:3;

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

let a be object ; :: thesis: ( a in the carrier of (BitGFA0Str (x,y,z)) implies (Following (s,2)) . a = (Following (Following (s,2))) . a )
assume a in the carrier of (BitGFA0Str (x,y,z)) ; :: thesis: (Following (s,2)) . a = (Following (Following (s,2))) . a
then ( a in the carrier of (GFA0AdderStr (x,y,z)) or a in the carrier of (GFA0CarryStr (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 (BitGFA0Str (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