set n1 = 2;
set n2 = 2;
let ap, bp, cp, dp be non pair set ; :: thesis: for cin being set st cin <> [<*dp,(GFA0AdderOutput (ap,bp,cp))*>,and2] holds
for s being State of (BitFTA0Circ (ap,bp,cp,dp,cin)) holds Following (s,4) is stable
let cin be set ; :: thesis: ( cin <> [<*dp,(GFA0AdderOutput (ap,bp,cp))*>,and2] implies for s being State of (BitFTA0Circ (ap,bp,cp,dp,cin)) holds Following (s,4) is stable )
set C = BitFTA0Circ (ap,bp,cp,dp,cin);
set S1 = BitGFA0Str (ap,bp,cp);
set C1 = BitGFA0Circ (ap,bp,cp);
set A1 = GFA0AdderOutput (ap,bp,cp);
set S2 = BitGFA0Str ((GFA0AdderOutput (ap,bp,cp)),cin,dp);
set C2 = BitGFA0Circ ((GFA0AdderOutput (ap,bp,cp)),cin,dp);
set cindp = [<*cin,dp*>,and2];
set dpA1 = [<*dp,(GFA0AdderOutput (ap,bp,cp))*>,and2];
assume A1: cin <> [<*dp,(GFA0AdderOutput (ap,bp,cp))*>,and2] ; :: thesis: for s being State of (BitFTA0Circ (ap,bp,cp,dp,cin)) holds Following (s,4) is stable
let s be State of (BitFTA0Circ (ap,bp,cp,dp,cin)); :: thesis: Following (s,4) is stable
BitGFA0Circ (ap,bp,cp) tolerates BitGFA0Circ ((GFA0AdderOutput (ap,bp,cp)),cin,dp) by CIRCCOMB:60;
then A2: the Sorts of (BitGFA0Circ (ap,bp,cp)) tolerates the Sorts of (BitGFA0Circ ((GFA0AdderOutput (ap,bp,cp)),cin,dp)) by CIRCCOMB:def 3;
then reconsider s1 = s | the carrier of (BitGFA0Str (ap,bp,cp)) as State of (BitGFA0Circ (ap,bp,cp)) by CIRCCOMB:26;
reconsider s2 = (Following (s,2)) | the carrier of (BitGFA0Str ((GFA0AdderOutput (ap,bp,cp)),cin,dp)) as State of (BitGFA0Circ ((GFA0AdderOutput (ap,bp,cp)),cin,dp)) by A2, CIRCCOMB:26;
A3: ( InputVertices (BitGFA0Str (ap,bp,cp)) misses InnerVertices (BitGFA0Str ((GFA0AdderOutput (ap,bp,cp)),cin,dp)) & Following (s1,2) is stable ) by Lm2, GFACIRC1:40;
GFA0AdderOutput (ap,bp,cp) <> [<*cin,dp*>,and2] by Lm1;
then Following (s2,2) is stable by A1, GFACIRC1:40;
then Following (s,(2 + 2)) is stable by A3, CIRCCMB2:19, CIRCCOMB:60;
hence Following (s,4) is stable ; :: thesis: verum