let n be Nat; :: thesis: for ap, bp, cp being FinSequence holds (n + 1) -BitFTA0Layer1Str (ap,bp,cp) = (n -BitFTA0Layer1Str (ap,bp,cp)) +* (BitGFA0Str ((ap . (n + 1)),(bp . (n + 1)),(cp . (n + 1))))
let ap, bp, cp be FinSequence; :: thesis: (n + 1) -BitFTA0Layer1Str (ap,bp,cp) = (n -BitFTA0Layer1Str (ap,bp,cp)) +* (BitGFA0Str ((ap . (n + 1)),(bp . (n + 1)),(cp . (n + 1))))
set s0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE));
deffunc H₁( non empty ManySortedSign , set , Nat) -> ManySortedSign = $1 +* (BitGFA0Str ((ap . ($3 + 1)),(bp . ($3 + 1)),(cp . ($3 + 1))));
deffunc H₂( set , Nat) -> set = {} ;
consider f being ManySortedSet of NAT such that
A1: (n + 1) -BitFTA0Layer1Str (ap,bp,cp) = f . (n + 1) and
A2: f . 0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) and
A3: 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;
set h = EmptyMS NAT;
defpred S₁[ Nat] means f . $1 is non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign ;
A4: S₁[ 0 ] by A2;
A5: 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 = f . k as non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign ;
f . (k + 1) = S +* (BitGFA0Str ((ap . (k + 1)),(bp . (k + 1)),(cp . (k + 1)))) by A3;
hence S₁[k + 1] ; :: thesis: verum

end;

A6: for k being Nat holds S₁[k] from NAT_1:sch 2(A4, A5);
A7: n -BitFTA0Layer1Str (ap,bp,cp) = f . n

proof

reconsider fn = f . n as non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign by A6;
B1: ex ff, hh being ManySortedSet of NAT st
( fn = ff . n & ff . 0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) & hh . 0 = {} & ( for k being Nat
for S being non empty ManySortedSign
for x being set st S = ff . k & x = hh . k holds
( ff . (k + 1) = H₁(S,x,k) & hh . (k + 1) = H₂(x,k) ) ) )

proof

take f ; :: thesis: ex hh being ManySortedSet of NAT st
( fn = f . n & f . 0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) & hh . 0 = {} & ( for k being Nat
for S being non empty ManySortedSign
for x being set st S = f . k & x = hh . k holds
( f . (k + 1) = H₁(S,x,k) & hh . (k + 1) = H₂(x,k) ) ) )
take EmptyMS NAT ; :: thesis: ( fn = f . n & f . 0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) & (EmptyMS NAT) . 0 = {} & ( for k being Nat
for S being non empty ManySortedSign
for x being set st S = f . k & x = (EmptyMS NAT) . k holds
( f . (k + 1) = H₁(S,x,k) & (EmptyMS NAT) . (k + 1) = H₂(x,k) ) ) )
thus ( fn = f . n & f . 0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) & (EmptyMS NAT) . 0 = {} ) by A2, PBOOLE:5; :: thesis: for k being Nat
for S being non empty ManySortedSign
for x being set st S = f . k & x = (EmptyMS NAT) . k holds
( f . (k + 1) = H₁(S,x,k) & (EmptyMS NAT) . (k + 1) = H₂(x,k) )
let k be Nat; :: thesis: for S being non empty ManySortedSign
for x being set st S = f . k & x = (EmptyMS NAT) . k holds
( f . (k + 1) = H₁(S,x,k) & (EmptyMS NAT) . (k + 1) = H₂(x,k) )
let S be non empty ManySortedSign ; :: thesis: for x being set st S = f . k & x = (EmptyMS NAT) . k holds
( f . (k + 1) = H₁(S,x,k) & (EmptyMS NAT) . (k + 1) = H₂(x,k) )
let x be set ; :: thesis: ( S = f . k & x = (EmptyMS NAT) . k implies ( f . (k + 1) = H₁(S,x,k) & (EmptyMS NAT) . (k + 1) = H₂(x,k) ) )
assume that
C1: S = f . k and
x = (EmptyMS NAT) . k ; :: thesis: ( f . (k + 1) = H₁(S,x,k) & (EmptyMS NAT) . (k + 1) = H₂(x,k) )
thus f . (k + 1) = H₁(S,x,k) by A3, C1; :: thesis: (EmptyMS NAT) . (k + 1) = H₂(x,k)
thus (EmptyMS NAT) . (k + 1) = H₂(x,k) by PBOOLE:5; :: thesis: verum

end;

B2: ex ff, hh being ManySortedSet of NAT st
( n -BitFTA0Layer1Str (ap,bp,cp) = ff . n & ff . 0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) & hh . 0 = {} & ( for k being Nat
for S being non empty ManySortedSign
for x being set st S = ff . k & x = hh . k holds
( ff . (k + 1) = H₁(S,x,k) & hh . (k + 1) = H₂(x,k) ) ) )

proof

consider f2 being ManySortedSet of NAT such that
C1: n -BitFTA0Layer1Str (ap,bp,cp) = f2 . n and
C2: f2 . 0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) and
C3: for k being Nat
for S being non empty ManySortedSign st S = f2 . k holds
f2 . (k + 1) = S +* (BitGFA0Str ((ap . (k + 1)),(bp . (k + 1)),(cp . (k + 1)))) by Def4;
set h2 = EmptyMS NAT;
take f2 ; :: thesis: ex hh being ManySortedSet of NAT st
( n -BitFTA0Layer1Str (ap,bp,cp) = f2 . n & f2 . 0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) & hh . 0 = {} & ( for k being Nat
for S being non empty ManySortedSign
for x being set st S = f2 . k & x = hh . k holds
( f2 . (k + 1) = H₁(S,x,k) & hh . (k + 1) = H₂(x,k) ) ) )
take EmptyMS NAT ; :: thesis: ( n -BitFTA0Layer1Str (ap,bp,cp) = f2 . n & f2 . 0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) & (EmptyMS NAT) . 0 = {} & ( for k being Nat
for S being non empty ManySortedSign
for x being set st S = f2 . k & x = (EmptyMS NAT) . k holds
( f2 . (k + 1) = H₁(S,x,k) & (EmptyMS NAT) . (k + 1) = H₂(x,k) ) ) )
thus ( n -BitFTA0Layer1Str (ap,bp,cp) = f2 . n & f2 . 0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) & (EmptyMS NAT) . 0 = {} ) by C1, C2, PBOOLE:5; :: thesis: for k being Nat
for S being non empty ManySortedSign
for x being set st S = f2 . k & x = (EmptyMS NAT) . k holds
( f2 . (k + 1) = H₁(S,x,k) & (EmptyMS NAT) . (k + 1) = H₂(x,k) )
let k be Nat; :: thesis: for S being non empty ManySortedSign
for x being set st S = f2 . k & x = (EmptyMS NAT) . k holds
( f2 . (k + 1) = H₁(S,x,k) & (EmptyMS NAT) . (k + 1) = H₂(x,k) )
let S be non empty ManySortedSign ; :: thesis: for x being set st S = f2 . k & x = (EmptyMS NAT) . k holds
( f2 . (k + 1) = H₁(S,x,k) & (EmptyMS NAT) . (k + 1) = H₂(x,k) )
let x be set ; :: thesis: ( S = f2 . k & x = (EmptyMS NAT) . k implies ( f2 . (k + 1) = H₁(S,x,k) & (EmptyMS NAT) . (k + 1) = H₂(x,k) ) )
assume that
C4: S = f2 . k and
x = (EmptyMS NAT) . k ; :: thesis: ( f2 . (k + 1) = H₁(S,x,k) & (EmptyMS NAT) . (k + 1) = H₂(x,k) )
thus f2 . (k + 1) = H₁(S,x,k) by C3, C4; :: thesis: (EmptyMS NAT) . (k + 1) = H₂(x,k)
thus (EmptyMS NAT) . (k + 1) = H₂(x,k) by PBOOLE:5; :: thesis: verum

end;

for S1, S2 being non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign st ex ff, hh being ManySortedSet of NAT st
( S1 = ff . n & ff . 0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) & hh . 0 = {} & ( for k being Nat
for S being non empty ManySortedSign
for x being set st S = ff . k & x = hh . k holds
( ff . (k + 1) = H₁(S,x,k) & hh . (k + 1) = H₂(x,k) ) ) ) & ex ff, hh being ManySortedSet of NAT st
( S2 = ff . n & ff . 0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) & hh . 0 = {} & ( for k being Nat
for S being non empty ManySortedSign
for x being set st S = ff . k & x = hh . k holds
( ff . (k + 1) = H₁(S,x,k) & hh . (k + 1) = H₂(x,k) ) ) ) holds
S1 = S2 from CIRCCMB2:sch 9();
hence n -BitFTA0Layer1Str (ap,bp,cp) = f . n by B1, B2; :: thesis: verum

end;

thus (n + 1) -BitFTA0Layer1Str (ap,bp,cp) = (n -BitFTA0Layer1Str (ap,bp,cp)) +* (BitGFA0Str ((ap . (n + 1)),(bp . (n + 1)),(cp . (n + 1)))) by A1, A3, A7; :: thesis: verum