defpred S₁[ Nat] means for ap, bp, cp, dp being FinSequence holds $1 -BitFTA0Str (ap,bp,cp,dp) = ($1 -BitFTA0Layer1Str (ap,bp,cp)) +* ($1 -BitFTA0Layer2Str (ap,bp,cp,dp));
A1: S₁[ 0 ]

proof

let ap, bp, cp, dp be FinSequence; :: thesis: 0 -BitFTA0Str (ap,bp,cp,dp) = (0 -BitFTA0Layer1Str (ap,bp,cp)) +* (0 -BitFTA0Layer2Str (ap,bp,cp,dp))
set s0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE));
consider f being ManySortedSet of NAT such that
B1: 0 -BitFTA0Layer1Str (ap,bp,cp) = f . 0 and
B2: f . 0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) and
for k being Nat
for S being non empty ManySortedSign st S = f . k holds
f . (k + 1) = S +* (BitGFA0Str ((ap . (k + 1)),(bp . (k + 1)),(cp . (k + 1)))) by Def4;
consider g, h being ManySortedSet of NAT such that
B3: 0 -BitFTA0Layer2Str (ap,bp,cp,dp) = g . 0 and
B4: g . 0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) and
h . 0 = [<*>,((0 -tuples_on BOOLEAN) --> FALSE)] and
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 +* (BitGFA0Str ((GFA0AdderOutput ((ap . (k + 1)),(bp . (k + 1)),(cp . (k + 1)))),z,(dp . (k + 1)))) & h . (k + 1) = GFA0CarryOutput ((ap . (k + 1)),(bp . (k + 1)),(cp . (k + 1))) ) by Def6;
(1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE))) +* (1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE))) = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) by CIRCCOMB:4;
hence 0 -BitFTA0Str (ap,bp,cp,dp) = (0 -BitFTA0Layer1Str (ap,bp,cp)) +* (0 -BitFTA0Layer2Str (ap,bp,cp,dp)) by B1, B2, B3, B4, Th2; :: thesis: verum

end;

A2: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume B1: S₁[k] ; :: thesis: S₁[k + 1]
let ap, bp, cp, dp be FinSequence; :: thesis: (k + 1) -BitFTA0Str (ap,bp,cp,dp) = ((k + 1) -BitFTA0Layer1Str (ap,bp,cp)) +* ((k + 1) -BitFTA0Layer2Str (ap,bp,cp,dp))
set a = k -BitFTA0Layer1Str (ap,bp,cp);
set b = k -BitFTA0Layer2Str (ap,bp,cp,dp);
set s1 = BitGFA0Str ((ap . (k + 1)),(bp . (k + 1)),(cp . (k + 1)));
set s2 = BitGFA0Str ((GFA0AdderOutput ((ap . (k + 1)),(bp . (k + 1)),(cp . (k + 1)))),(k -BitFTA0CarryOutput (ap,bp,cp,dp)),(dp . (k + 1)));
B2: k -BitFTA0Str (ap,bp,cp,dp) = (k -BitFTA0Layer1Str (ap,bp,cp)) +* (k -BitFTA0Layer2Str (ap,bp,cp,dp)) by B1;
B3: BitFTA0Str ((ap . (k + 1)),(bp . (k + 1)),(cp . (k + 1)),(dp . (k + 1)),(k -BitFTA0CarryOutput (ap,bp,cp,dp))) = (BitGFA0Str ((ap . (k + 1)),(bp . (k + 1)),(cp . (k + 1)))) +* (BitGFA0Str ((GFA0AdderOutput ((ap . (k + 1)),(bp . (k + 1)),(cp . (k + 1)))),(k -BitFTA0CarryOutput (ap,bp,cp,dp)),(dp . (k + 1)))) ;
B4: (k + 1) -BitFTA0Str (ap,bp,cp,dp) = ((k -BitFTA0Layer1Str (ap,bp,cp)) +* (k -BitFTA0Layer2Str (ap,bp,cp,dp))) +* ((BitGFA0Str ((ap . (k + 1)),(bp . (k + 1)),(cp . (k + 1)))) +* (BitGFA0Str ((GFA0AdderOutput ((ap . (k + 1)),(bp . (k + 1)),(cp . (k + 1)))),(k -BitFTA0CarryOutput (ap,bp,cp,dp)),(dp . (k + 1))))) by Th3, B2, B3;
B5: (k + 1) -BitFTA0Layer2Str (ap,bp,cp,dp) = (k -BitFTA0Layer2Str (ap,bp,cp,dp)) +* (BitGFA0Str ((GFA0AdderOutput ((ap . (k + 1)),(bp . (k + 1)),(cp . (k + 1)))),(k -BitFTA0CarryOutput (ap,bp,cp,dp)),(dp . (k + 1)))) by LmT05B;
((k -BitFTA0Layer1Str (ap,bp,cp)) +* (k -BitFTA0Layer2Str (ap,bp,cp,dp))) +* ((BitGFA0Str ((ap . (k + 1)),(bp . (k + 1)),(cp . (k + 1)))) +* (BitGFA0Str ((GFA0AdderOutput ((ap . (k + 1)),(bp . (k + 1)),(cp . (k + 1)))),(k -BitFTA0CarryOutput (ap,bp,cp,dp)),(dp . (k + 1))))) = (k -BitFTA0Layer1Str (ap,bp,cp)) +* ((k -BitFTA0Layer2Str (ap,bp,cp,dp)) +* ((BitGFA0Str ((ap . (k + 1)),(bp . (k + 1)),(cp . (k + 1)))) +* (BitGFA0Str ((GFA0AdderOutput ((ap . (k + 1)),(bp . (k + 1)),(cp . (k + 1)))),(k -BitFTA0CarryOutput (ap,bp,cp,dp)),(dp . (k + 1)))))) by CIRCCOMB:6
.= (k -BitFTA0Layer1Str (ap,bp,cp)) +* (((k -BitFTA0Layer2Str (ap,bp,cp,dp)) +* (BitGFA0Str ((ap . (k + 1)),(bp . (k + 1)),(cp . (k + 1))))) +* (BitGFA0Str ((GFA0AdderOutput ((ap . (k + 1)),(bp . (k + 1)),(cp . (k + 1)))),(k -BitFTA0CarryOutput (ap,bp,cp,dp)),(dp . (k + 1))))) by CIRCCOMB:6
.= (k -BitFTA0Layer1Str (ap,bp,cp)) +* (((BitGFA0Str ((ap . (k + 1)),(bp . (k + 1)),(cp . (k + 1)))) +* (k -BitFTA0Layer2Str (ap,bp,cp,dp))) +* (BitGFA0Str ((GFA0AdderOutput ((ap . (k + 1)),(bp . (k + 1)),(cp . (k + 1)))),(k -BitFTA0CarryOutput (ap,bp,cp,dp)),(dp . (k + 1))))) by FACIRC_1:23
.= (k -BitFTA0Layer1Str (ap,bp,cp)) +* ((BitGFA0Str ((ap . (k + 1)),(bp . (k + 1)),(cp . (k + 1)))) +* ((k -BitFTA0Layer2Str (ap,bp,cp,dp)) +* (BitGFA0Str ((GFA0AdderOutput ((ap . (k + 1)),(bp . (k + 1)),(cp . (k + 1)))),(k -BitFTA0CarryOutput (ap,bp,cp,dp)),(dp . (k + 1)))))) by CIRCCOMB:6
.= ((k -BitFTA0Layer1Str (ap,bp,cp)) +* (BitGFA0Str ((ap . (k + 1)),(bp . (k + 1)),(cp . (k + 1))))) +* ((k -BitFTA0Layer2Str (ap,bp,cp,dp)) +* (BitGFA0Str ((GFA0AdderOutput ((ap . (k + 1)),(bp . (k + 1)),(cp . (k + 1)))),(k -BitFTA0CarryOutput (ap,bp,cp,dp)),(dp . (k + 1))))) by CIRCCOMB:6 ;
hence (k + 1) -BitFTA0Str (ap,bp,cp,dp) = ((k + 1) -BitFTA0Layer1Str (ap,bp,cp)) +* ((k + 1) -BitFTA0Layer2Str (ap,bp,cp,dp)) by B4, LmT05A, B5; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A1, A2);
hence for n being Nat
for ap, bp, cp, dp being FinSequence holds n -BitFTA0Str (ap,bp,cp,dp) = (n -BitFTA0Layer1Str (ap,bp,cp)) +* (n -BitFTA0Layer2Str (ap,bp,cp,dp)) ; :: thesis: verum