set n1 = 2;
set n2 = 2;
let am, bp, cm, dp be non pair set ; 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 ; ( 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 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 dpA1 = [<*dp,(GFA2AdderOutput (am,bp,cm))*>,and2];
assume A1:
cin <> [<*dp,(GFA2AdderOutput (am,bp,cm))*>,and2]
; 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)); Following (s,4) is stable
BitGFA2Circ (am,bp,cm) tolerates BitGFA1Circ ((GFA2AdderOutput (am,bp,cm)),cin,dp)
by CIRCCOMB:60;
then A2:
the Sorts of (BitGFA2Circ (am,bp,cm)) tolerates the Sorts of (BitGFA1Circ ((GFA2AdderOutput (am,bp,cm)),cin,dp))
by CIRCCOMB:def 3;
then reconsider s1 = s | the carrier of (BitGFA2Str (am,bp,cm)) as State of (BitGFA2Circ (am,bp,cm)) by CIRCCOMB:26;
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 A2, CIRCCOMB:26;
A3:
( InputVertices (BitGFA2Str (am,bp,cm)) misses InnerVertices (BitGFA1Str ((GFA2AdderOutput (am,bp,cm)),cin,dp)) & Following (s1,2) is stable )
by Lm22, GFACIRC1:104;
Following (s2,2) is stable
by A1, Lm21, GFACIRC1:72;
then
Following (s,(2 + 2)) is stable
by A3, CIRCCMB2:19, CIRCCOMB:60;
hence
Following (s,4) is stable
; verum