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

A11: now

let a be set ; :: thesis: ( a in the carrier of (BitGFA3Str x,y,z) implies (Following s,2) . a = (Following (Following s,2)) . a )
assume a in the carrier of (BitGFA3Str x,y,z) ; :: thesis: (Following s,2) . a = (Following (Following s,2)) . a
then ( a in the carrier of (GFA3AdderStr x,y,z) or a in the carrier of (GFA3CarryStr 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:70;
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 (BitGFA3Str x,y,z) ) by CIRCUIT1:4, FACIRC_1:12;
hence Following s,2 = Following (Following s,2) by A6, A11, FUNCT_1:9; :: according to CIRCUIT2:def 6 :: thesis: verum