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 S = BitFTA0Str ap,bp,cp,dp,cin;
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 apbp0 = [<*ap,bp*>,xor2 ];
set apbp = [<*ap,bp*>,and2 ];
set bpcp = [<*bp,cp*>,and2 ];
set cpap = [<*cp,ap*>,and2 ];
set A1cin0 = [<*(GFA0AdderOutput ap,bp,cp),cin*>,xor2 ];
set A1cin = [<*(GFA0AdderOutput ap,bp,cp),cin*>,and2 ];
set cindp = [<*cin,dp*>,and2 ];
set dpA1 = [<*dp,(GFA0AdderOutput ap,bp,cp)*>,and2 ];
set n1 = 2;
set n2 = 2;
set n12 = 4;
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
A2: BitGFA0Circ ap,bp,cp tolerates BitGFA0Circ (GFA0AdderOutput ap,bp,cp),cin,dp by CIRCCOMB:68;
A3: InputVertices (BitGFA0Str ap,bp,cp) misses InnerVertices (BitGFA0Str (GFA0AdderOutput ap,bp,cp),cin,dp) by LemmaX12;
A4: the Sorts of (BitGFA0Circ ap,bp,cp) tolerates the Sorts of (BitGFA0Circ (GFA0AdderOutput ap,bp,cp),cin,dp) by A2, CIRCCOMB:def 3;
then reconsider s1 = s | the carrier of (BitGFA0Str ap,bp,cp) as State of (BitGFA0Circ ap,bp,cp) by CIRCCOMB:33;
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 A4, CIRCCOMB:33;
A5: Following s1,2 is stable by GFACIRC1:48;
( dp <> [<*(GFA0AdderOutput ap,bp,cp),cin*>,xor2 ] & GFA0AdderOutput ap,bp,cp <> [<*cin,dp*>,and2 ] & cin <> [<*dp,(GFA0AdderOutput ap,bp,cp)*>,and2 ] & dp <> [<*(GFA0AdderOutput ap,bp,cp),cin*>,and2 ] ) by A1, LemmaX11;
then Following s2,2 is stable by GFACIRC1:48;
then Following s,(2 + 2) is stable by A3, A5, CIRCCMB2:20, CIRCCOMB:68;
hence Following s,4 is stable ; :: thesis: verum