let n be Nat; :: thesis: for ap, bm, cp, dm being FinSequence holds (n + 1) -BitFTA1Layer2Str (ap,bm,cp,dm) = (n -BitFTA1Layer2Str (ap,bm,cp,dm)) +* (BitGFA2Str ((GFA1AdderOutput ((ap . (n + 1)),(bm . (n + 1)),(cp . (n + 1)))),(n -BitFTA1CarryOutput (ap,bm,cp,dm)),(dm . (n + 1))))
let ap, bm, cp, dm be FinSequence; :: thesis: (n + 1) -BitFTA1Layer2Str (ap,bm,cp,dm) = (n -BitFTA1Layer2Str (ap,bm,cp,dm)) +* (BitGFA2Str ((GFA1AdderOutput ((ap . (n + 1)),(bm . (n + 1)),(cp . (n + 1)))),(n -BitFTA1CarryOutput (ap,bm,cp,dm)),(dm . (n + 1))))
set s0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE));
set h0 = [<*>,((0 -tuples_on BOOLEAN) --> FALSE)];
deffunc H₁( non empty ManySortedSign , set , Nat) -> ManySortedSign = $1 +* (BitGFA2Str ((GFA1AdderOutput ((ap . ($3 + 1)),(bm . ($3 + 1)),(cp . ($3 + 1)))),$2,(dm . ($3 + 1))));
deffunc H₂( set , Nat) -> Element of InnerVertices (GFA1CarryStr ((ap . ($2 + 1)),(bm . ($2 + 1)),(cp . ($2 + 1)))) = GFA1CarryOutput ((ap . ($2 + 1)),(bm . ($2 + 1)),(cp . ($2 + 1)));
deffunc H₃( Nat, set ) -> Element of InnerVertices (GFA1CarryStr ((ap . ($1 + 1)),(bm . ($1 + 1)),(cp . ($1 + 1)))) = GFA1CarryOutput ((ap . ($1 + 1)),(bm . ($1 + 1)),(cp . ($1 + 1)));
consider g, h being ManySortedSet of NAT such that
A1: (n + 1) -BitFTA1Layer2Str (ap,bm,cp,dm) = g . (n + 1) and
A2: g . 0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) and
A3: h . 0 = [<*>,((0 -tuples_on BOOLEAN) --> FALSE)] and
A4: for k being Nat
for S being non empty ManySortedSign
for z being set st S = g . k & z = h . k holds
( g . (k + 1) = S +* (BitGFA2Str ((GFA1AdderOutput ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1)))),z,(dm . (k + 1)))) & h . (k + 1) = GFA1CarryOutput ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1))) ) by Def13;
defpred S₁[ Nat] means g . $1 is non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign ;
A5: S₁[ 0 ] by A2;
A6: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume S₁[k] ; :: thesis: S₁[k + 1]
then reconsider S = g . k as non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign ;
g . (k + 1) = S +* (BitGFA2Str ((GFA1AdderOutput ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1)))),(h . k),(dm . (k + 1)))) by A4;
hence S₁[k + 1] ; :: thesis: verum

end;

A7: for k being Nat holds S₁[k] from NAT_1:sch 2(A5, A6);
A8: for k being Nat holds h . (k + 1) = H₃(k,h . k)

proof

let k be Nat; :: thesis: h . (k + 1) = H₃(k,h . k)
reconsider S = g . k as non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign by A7;
reconsider z = h . k as set ;
( S = g . k & z = h . k ) ;
hence h . (k + 1) = H₃(k,h . k) by A4; :: thesis: verum

end;

consider h3 being ManySortedSet of NAT such that
A9: n -BitFTA1CarryOutput (ap,bm,cp,dm) = h3 . n and
A10: h3 . 0 = [<*>,((0 -tuples_on BOOLEAN) --> FALSE)] and
A11: for k being Nat holds h3 . (k + 1) = BitFTA1CarryOutput ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1)),(dm . (k + 1)),(h3 . k)) by Def10;
A12: 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) = BitFTA1CarryOutput ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1)),(dm . (k + 1)),(h3 . k)) by A11
.= GFA1CarryOutput ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1))) ;
hence h3 . (k + 1) = H₃(k,h3 . k) ; :: thesis: verum

end;

A13: dom h = NAT by PARTFUN1:def 2;
A14: dom h3 = NAT by PARTFUN1:def 2;
A15: h = h3 from NAT_1:sch 15(A13, A3, A8, A14, A10, A12);
A16: n -BitFTA1Layer2Str (ap,bm,cp,dm) = g . n

proof

reconsider gn = g . n as non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign by A7;
gn = n -BitFTA1Layer2Str (ap,bm,cp,dm) by A2, A3, A4, Def13;
hence n -BitFTA1Layer2Str (ap,bm,cp,dm) = g . n ; :: thesis: verum

end;

thus (n + 1) -BitFTA1Layer2Str (ap,bm,cp,dm) = (n -BitFTA1Layer2Str (ap,bm,cp,dm)) +* (BitGFA2Str ((GFA1AdderOutput ((ap . (n + 1)),(bm . (n + 1)),(cp . (n + 1)))),(n -BitFTA1CarryOutput (ap,bm,cp,dm)),(dm . (n + 1)))) by A1, A4, A15, A9, A16; :: thesis: verum