let n be Nat; :: thesis: for ap, bp, cp, dp being FinSequence holds (n + 1) -BitFTA0Layer2Circ (ap,bp,cp,dp) = (n -BitFTA0Layer2Circ (ap,bp,cp,dp)) +* (BitGFA0Circ ((GFA0AdderOutput ((ap . (n + 1)),(bp . (n + 1)),(cp . (n + 1)))),(n -BitFTA0CarryOutput (ap,bp,cp,dp)),(dp . (n + 1))))
let ap, bp, cp, dp be FinSequence; :: thesis: (n + 1) -BitFTA0Layer2Circ (ap,bp,cp,dp) = (n -BitFTA0Layer2Circ (ap,bp,cp,dp)) +* (BitGFA0Circ ((GFA0AdderOutput ((ap . (n + 1)),(bp . (n + 1)),(cp . (n + 1)))),(n -BitFTA0CarryOutput (ap,bp,cp,dp)),(dp . (n + 1))))
set S0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE));
set A0 = 1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> FALSE));
set h0 = [<*>,((0 -tuples_on BOOLEAN) --> FALSE)];
deffunc H₁( non empty ManySortedSign , set , Nat) -> ManySortedSign = $1 +* (BitGFA0Str ((GFA0AdderOutput ((ap . ($3 + 1)),(bp . ($3 + 1)),(cp . ($3 + 1)))),$2,(dp . ($3 + 1))));
deffunc H₂( non empty ManySortedSign , non-empty MSAlgebra over $1, set , Nat) -> MSAlgebra over $1 +* (BitGFA0Str ((GFA0AdderOutput ((ap . ($4 + 1)),(bp . ($4 + 1)),(cp . ($4 + 1)))),$3,(dp . ($4 + 1)))) = $2 +* (BitGFA0Circ ((GFA0AdderOutput ((ap . ($4 + 1)),(bp . ($4 + 1)),(cp . ($4 + 1)))),$3,(dp . ($4 + 1))));
deffunc H₃( set , Nat) -> Element of InnerVertices (GFA0CarryStr ((ap . ($2 + 1)),(bp . ($2 + 1)),(cp . ($2 + 1)))) = GFA0CarryOutput ((ap . ($2 + 1)),(bp . ($2 + 1)),(cp . ($2 + 1)));
deffunc H₄( Nat, set ) -> Element of InnerVertices (GFA0CarryStr ((ap . ($1 + 1)),(bp . ($1 + 1)),(cp . ($1 + 1)))) = GFA0CarryOutput ((ap . ($1 + 1)),(bp . ($1 + 1)),(cp . ($1 + 1)));
consider f1, g1, h1 being ManySortedSet of NAT such that
A1: n -BitFTA0Layer2Str (ap,bp,cp,dp) = f1 . n and
A2: n -BitFTA0Layer2Circ (ap,bp,cp,dp) = g1 . n and
A3: f1 . 0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) and
A4: g1 . 0 = 1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) and
A5: h1 . 0 = [<*>,((0 -tuples_on BOOLEAN) --> FALSE)] and
A6: for k being Nat
for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S
for z being set st S = f1 . k & A = g1 . k & z = h1 . k holds
( f1 . (k + 1) = S +* (BitGFA0Str ((GFA0AdderOutput ((ap . (k + 1)),(bp . (k + 1)),(cp . (k + 1)))),z,(dp . (k + 1)))) & g1 . (k + 1) = A +* (BitGFA0Circ ((GFA0AdderOutput ((ap . (k + 1)),(bp . (k + 1)),(cp . (k + 1)))),z,(dp . (k + 1)))) & h1 . (k + 1) = GFA0CarryOutput ((ap . (k + 1)),(bp . (k + 1)),(cp . (k + 1))) ) by Def7;
consider f2, g2, h2 being ManySortedSet of NAT such that
(n + 1) -BitFTA0Layer2Str (ap,bp,cp,dp) = f2 . (n + 1) and
A7: (n + 1) -BitFTA0Layer2Circ (ap,bp,cp,dp) = g2 . (n + 1) and
A8: f2 . 0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) and
A9: g2 . 0 = 1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) and
A10: h2 . 0 = [<*>,((0 -tuples_on BOOLEAN) --> FALSE)] and
A11: for k being Nat
for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S
for z being set st S = f2 . k & A = g2 . k & z = h2 . k holds
( f2 . (k + 1) = S +* (BitGFA0Str ((GFA0AdderOutput ((ap . (k + 1)),(bp . (k + 1)),(cp . (k + 1)))),z,(dp . (k + 1)))) & g2 . (k + 1) = A +* (BitGFA0Circ ((GFA0AdderOutput ((ap . (k + 1)),(bp . (k + 1)),(cp . (k + 1)))),z,(dp . (k + 1)))) & h2 . (k + 1) = GFA0CarryOutput ((ap . (k + 1)),(bp . (k + 1)),(cp . (k + 1))) ) by Def7;
A12: ex S being non empty ManySortedSign ex A being non-empty MSAlgebra over S st
( S = f1 . 0 & A = g1 . 0 ) by A3, A4;
A13: ( f1 . 0 = f2 . 0 & g1 . 0 = g2 . 0 & h1 . 0 = h2 . 0 ) by A3, A4, A5, A8, A9, A10;
A14: for k being Nat
for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S
for x being set st S = f1 . k & A = g1 . k & x = h1 . k holds
( f1 . (k + 1) = H₁(S,x,k) & g1 . (k + 1) = H₂(S,A,x,k) & h1 . (k + 1) = H₃(x,k) ) by A6;
A15: for k being Nat
for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S
for x being set st S = f2 . k & A = g2 . k & x = h2 . k holds
( f2 . (k + 1) = H₁(S,x,k) & g2 . (k + 1) = H₂(S,A,x,k) & h2 . (k + 1) = H₃(x,k) ) by A11;
A16: for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S
for x being set
for k being Nat holds H₂(S,A,x,k) is non-empty MSAlgebra over H₁(S,x,k) ;
A17: ( f1 = f2 & g1 = g2 & h1 = h2 ) from CIRCCMB2:sch 14(A12, A13, A14, A15, A16);
A18: ( f1 . 0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) & g1 . 0 = 1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) ) by A3, A4;
A19: for k being Nat
for S being non empty ManySortedSign
for z being set st S = f1 . k & z = h1 . k holds
( f1 . (k + 1) = H₁(S,z,k) & h1 . (k + 1) = H₃(z,k) ) from CIRCCMB2:sch 15(A18, A14, A16);
A20: for k being Nat
for z being set st z = h1 . k holds
h1 . (k + 1) = H₃(z,k) from CIRCCMB2:sch 3(A3, A19);
A21: for k being Nat holds h1 . (k + 1) = H₄(k,h1 . k)

proof

let k be Nat; :: thesis: h1 . (k + 1) = H₄(k,h1 . k)
h1 . k = h1 . k ;
hence h1 . (k + 1) = H₄(k,h1 . k) by A20; :: thesis: verum

end;

consider h3 being ManySortedSet of NAT such that
A22: n -BitFTA0CarryOutput (ap,bp,cp,dp) = h3 . n and
A23: h3 . 0 = [<*>,((0 -tuples_on BOOLEAN) --> FALSE)] and
A24: for k being Nat holds h3 . (k + 1) = BitFTA0CarryOutput ((ap . (k + 1)),(bp . (k + 1)),(cp . (k + 1)),(dp . (k + 1)),(h3 . k)) by Def3;
A25: for k being Nat holds h3 . (k + 1) = H₄(k,h3 . k)

proof

let k be Nat; :: thesis: h3 . (k + 1) = H₄(k,h3 . k)
h3 . (k + 1) = BitFTA0CarryOutput ((ap . (k + 1)),(bp . (k + 1)),(cp . (k + 1)),(dp . (k + 1)),(h3 . k)) by A24
.= GFA0CarryOutput ((ap . (k + 1)),(bp . (k + 1)),(cp . (k + 1))) ;
hence h3 . (k + 1) = H₄(k,h3 . k) ; :: thesis: verum

end;

A26: dom h1 = NAT by PARTFUN1:def 2;
A27: dom h3 = NAT by PARTFUN1:def 2;
A28: h1 = h3 from NAT_1:sch 15(A26, A5, A21, A27, A23, A25);
thus (n + 1) -BitFTA0Layer2Circ (ap,bp,cp,dp) = (n -BitFTA0Layer2Circ (ap,bp,cp,dp)) +* (BitGFA0Circ ((GFA0AdderOutput ((ap . (n + 1)),(bp . (n + 1)),(cp . (n + 1)))),(n -BitFTA0CarryOutput (ap,bp,cp,dp)),(dp . (n + 1)))) by A17, A7, A6, A28, A22, A1, A2; :: thesis: verum