let am, bp, cm, dp be non pair set ; :: thesis: for cin being set st cin <> [<*dp,(GFA2AdderOutput am,bp,cm)*>,and2 ] holds
for s being State of (BitFTA2Circ am,bp,cm,dp,cin) holds Following s,4 is stable
let cin be set ; :: thesis: ( cin <> [<*dp,(GFA2AdderOutput am,bp,cm)*>,and2 ] implies for s being State of (BitFTA2Circ am,bp,cm,dp,cin) holds Following s,4 is stable )
set S = BitFTA2Str am,bp,cm,dp,cin;
set C = BitFTA2Circ am,bp,cm,dp,cin;
set S1 = BitGFA2Str am,bp,cm;
set C1 = BitGFA2Circ am,bp,cm;
set A1 = GFA2AdderOutput am,bp,cm;
set S2 = BitGFA1Str (GFA2AdderOutput am,bp,cm),cin,dp;
set C2 = BitGFA1Circ (GFA2AdderOutput am,bp,cm),cin,dp;
set ambp0 = [<*am,bp*>,xor2c ];
set ambp = [<*am,bp*>,and2a ];
set bpcm = [<*bp,cm*>,and2c ];
set cmam = [<*cm,am*>,and2b ];
set A1cin0 = [<*(GFA2AdderOutput am,bp,cm),cin*>,xor2c ];
set A1cin = [<*(GFA2AdderOutput am,bp,cm),cin*>,and2c ];
set cindp = [<*cin,dp*>,and2a ];
set dpA1 = [<*dp,(GFA2AdderOutput am,bp,cm)*>,and2 ];
set n1 = 2;
set n2 = 2;
set n12 = 4;
assume A1: cin <> [<*dp,(GFA2AdderOutput am,bp,cm)*>,and2 ] ; :: thesis: for s being State of (BitFTA2Circ am,bp,cm,dp,cin) holds Following s,4 is stable
let s be State of (BitFTA2Circ am,bp,cm,dp,cin); :: thesis: Following s,4 is stable
A2: BitGFA2Circ am,bp,cm tolerates BitGFA1Circ (GFA2AdderOutput am,bp,cm),cin,dp by CIRCCOMB:68;
A3: InputVertices (BitGFA2Str am,bp,cm) misses InnerVertices (BitGFA1Str (GFA2AdderOutput am,bp,cm),cin,dp) by LemmaX32;
A4: the Sorts of (BitGFA2Circ am,bp,cm) tolerates the Sorts of (BitGFA1Circ (GFA2AdderOutput am,bp,cm),cin,dp) by A2, CIRCCOMB:def 3;
then reconsider s1 = s | the carrier of (BitGFA2Str am,bp,cm) as State of (BitGFA2Circ am,bp,cm) by CIRCCOMB:33;
reconsider s2 = (Following s,2) | the carrier of (BitGFA1Str (GFA2AdderOutput am,bp,cm),cin,dp) as State of (BitGFA1Circ (GFA2AdderOutput am,bp,cm),cin,dp) by A4, CIRCCOMB:33;
A5: Following s1,2 is stable by GFACIRC1:122;
Following s2,2 is stable by A1, LemmaX31, GFACIRC1:85;
then Following s,(2 + 2) is stable by A3, A5, CIRCCMB2:20, CIRCCOMB:68;
hence Following s,4 is stable ; :: thesis: verum