let am, bm, cm, dm be non pair set ; :: thesis: for cin being set st cin <> [<*dm,(GFA3AdderOutput am,bm,cm)*>,and2b ] holds
for s being State of (BitFTA3Circ am,bm,cm,dm,cin) holds Following s,4 is stable
let cin be set ; :: thesis: ( cin <> [<*dm,(GFA3AdderOutput am,bm,cm)*>,and2b ] implies for s being State of (BitFTA3Circ am,bm,cm,dm,cin) holds Following s,4 is stable )
set S = BitFTA3Str am,bm,cm,dm,cin;
set C = BitFTA3Circ am,bm,cm,dm,cin;
set S1 = BitGFA3Str am,bm,cm;
set C1 = BitGFA3Circ am,bm,cm;
set A1 = GFA3AdderOutput am,bm,cm;
set S2 = BitGFA3Str (GFA3AdderOutput am,bm,cm),cin,dm;
set C2 = BitGFA3Circ (GFA3AdderOutput am,bm,cm),cin,dm;
set ambm0 = [<*am,bm*>,xor2 ];
set ambm = [<*am,bm*>,and2b ];
set bmcm = [<*bm,cm*>,and2b ];
set cmam = [<*cm,am*>,and2b ];
set A1cin0 = [<*(GFA3AdderOutput am,bm,cm),cin*>,xor2 ];
set A1cin = [<*(GFA3AdderOutput am,bm,cm),cin*>,and2b ];
set cindm = [<*cin,dm*>,and2b ];
set dmA1 = [<*dm,(GFA3AdderOutput am,bm,cm)*>,and2b ];
set n1 = 2;
set n2 = 2;
set n12 = 4;
assume A1: cin <> [<*dm,(GFA3AdderOutput am,bm,cm)*>,and2b ] ; :: thesis: for s being State of (BitFTA3Circ am,bm,cm,dm,cin) holds Following s,4 is stable
let s be State of (BitFTA3Circ am,bm,cm,dm,cin); :: thesis: Following s,4 is stable
A2: BitGFA3Circ am,bm,cm tolerates BitGFA3Circ (GFA3AdderOutput am,bm,cm),cin,dm by CIRCCOMB:68;
A3: InputVertices (BitGFA3Str am,bm,cm) misses InnerVertices (BitGFA3Str (GFA3AdderOutput am,bm,cm),cin,dm) by LemmaX42;
A4: the Sorts of (BitGFA3Circ am,bm,cm) tolerates the Sorts of (BitGFA3Circ (GFA3AdderOutput am,bm,cm),cin,dm) by A2, CIRCCOMB:def 3;
then reconsider s1 = s | the carrier of (BitGFA3Str am,bm,cm) as State of (BitGFA3Circ am,bm,cm) by CIRCCOMB:33;
reconsider s2 = (Following s,2) | the carrier of (BitGFA3Str (GFA3AdderOutput am,bm,cm),cin,dm) as State of (BitGFA3Circ (GFA3AdderOutput am,bm,cm),cin,dm) by A4, CIRCCOMB:33;
A5: Following s1,2 is stable by GFACIRC1:159;
( dm <> [<*(GFA3AdderOutput am,bm,cm),cin*>,xor2 ] & GFA3AdderOutput am,bm,cm <> [<*cin,dm*>,and2b ] & cin <> [<*dm,(GFA3AdderOutput am,bm,cm)*>,and2b ] & dm <> [<*(GFA3AdderOutput am,bm,cm),cin*>,and2b ] ) by A1, LemmaX41;
then Following s2,2 is stable by GFACIRC1:159;
then Following s,(2 + 2) is stable by A3, A5, CIRCCMB2:20, CIRCCOMB:68;
hence Following s,4 is stable ; :: thesis: verum