set S0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE));
set A0 = 1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> FALSE));
set Sn = n -BitFTA1Layer1Str (ap,bm,cp);
set h = EmptyMS NAT;
deffunc H₁( non empty ManySortedSign , set , Nat) -> ManySortedSign = $1 +* (BitGFA1Str ((ap . ($3 + 1)),(bm . ($3 + 1)),(cp . ($3 + 1))));
deffunc H₂( non empty ManySortedSign , non-empty MSAlgebra over $1, set , Nat) -> MSAlgebra over $1 +* (BitGFA1Str ((ap . ($4 + 1)),(bm . ($4 + 1)),(cp . ($4 + 1)))) = $2 +* (BitGFA1Circ ((ap . ($4 + 1)),(bm . ($4 + 1)),(cp . ($4 + 1))));
deffunc H₃( set , Nat) -> set = {} ;
A2: for S being non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign
for x being set
for m being Nat holds
( H₁(S,x,m) is unsplit & H₁(S,x,m) is gate`1=arity & H<sub>1</sub>(S,x,m) is gate`2isBoolean & not H₁(S,x,m) is void & H₁(S,x,m) is strict ) ;
A3: ex f, hh being ManySortedSet of NAT st
( n -BitFTA1Layer1Str (ap,bm,cp) = f . n & f . 0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) & hh . 0 = {} & ( for m being Nat
for S being non empty ManySortedSign
for x being set st S = f . m & x = hh . m holds
( f . (m + 1) = H₁(S,x,m) & hh . (m + 1) = H₃(x,m) ) ) )

proof

consider f being ManySortedSet of NAT such that
Q2: n -BitFTA1Layer1Str (ap,bm,cp) = f . n and
Q3: f . 0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) and
Q4: for k being Nat
for S being non empty ManySortedSign st S = f . k holds
f . (k + 1) = S +* (BitGFA1Str ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1)))) by Def11;
take f ; :: thesis: ex hh being ManySortedSet of NAT st
( n -BitFTA1Layer1Str (ap,bm,cp) = f . n & f . 0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) & hh . 0 = {} & ( for m being Nat
for S being non empty ManySortedSign
for x being set st S = f . m & x = hh . m holds
( f . (m + 1) = H₁(S,x,m) & hh . (m + 1) = H₃(x,m) ) ) )
take EmptyMS NAT ; :: thesis: ( n -BitFTA1Layer1Str (ap,bm,cp) = f . n & f . 0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) & (EmptyMS NAT) . 0 = {} & ( for m being Nat
for S being non empty ManySortedSign
for x being set st S = f . m & x = (EmptyMS NAT) . m holds
( f . (m + 1) = H₁(S,x,m) & (EmptyMS NAT) . (m + 1) = H₃(x,m) ) ) )
thus ( n -BitFTA1Layer1Str (ap,bm,cp) = f . n & f . 0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) & (EmptyMS NAT) . 0 = {} ) by Q2, Q3, PBOOLE:5; :: thesis: for m being Nat
for S being non empty ManySortedSign
for x being set st S = f . m & x = (EmptyMS NAT) . m holds
( f . (m + 1) = H₁(S,x,m) & (EmptyMS NAT) . (m + 1) = H₃(x,m) )
let m be Nat; :: thesis: for S being non empty ManySortedSign
for x being set st S = f . m & x = (EmptyMS NAT) . m holds
( f . (m + 1) = H₁(S,x,m) & (EmptyMS NAT) . (m + 1) = H₃(x,m) )
let S be non empty ManySortedSign ; :: thesis: for x being set st S = f . m & x = (EmptyMS NAT) . m holds
( f . (m + 1) = H₁(S,x,m) & (EmptyMS NAT) . (m + 1) = H₃(x,m) )
let x be set ; :: thesis: ( S = f . m & x = (EmptyMS NAT) . m implies ( f . (m + 1) = H₁(S,x,m) & (EmptyMS NAT) . (m + 1) = H₃(x,m) ) )
assume that
R1: S = f . m and
x = (EmptyMS NAT) . m ; :: thesis: ( f . (m + 1) = H₁(S,x,m) & (EmptyMS NAT) . (m + 1) = H₃(x,m) )
thus f . (m + 1) = H₁(S,x,m) by Q4, R1; :: thesis: (EmptyMS NAT) . (m + 1) = H₃(x,m)
thus (EmptyMS NAT) . (m + 1) = H₃(x,m) by PBOOLE:5; :: thesis: verum

end;

A4: for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S
for x being set
for m being Nat holds H₂(S,A,x,m) is non-empty MSAlgebra over H₁(S,x,m) ;
A5: for S, S1 being non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign
for A being strict gate`2=den Boolean Circuit of S
for x being set
for m being Nat st S1 = H<sub>1</sub>(S,x,m) holds
H<sub>2</sub>(S,A,x,m) is strict gate`2=den Boolean Circuit of S1 ;
consider AA being strict gate`2=den Boolean Circuit of n -BitFTA1Layer1Str (ap,bm,cp), f, g, hh being ManySortedSet of NAT such that
B1: ( n -BitFTA1Layer1Str (ap,bm,cp) = f . n & AA = g . n & f . 0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) & g . 0 = 1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) & hh . 0 = {} & ( for m being Nat
for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S
for x being set st S = f . m & A = g . m & x = hh . m holds
( f . (m + 1) = H₁(S,x,m) & g . (m + 1) = H₂(S,A,x,m) & hh . (m + 1) = H₃(x,m) ) ) ) from CIRCCMB2:sch 19(A2, A3, A4, A5);
take AA ; :: thesis: ex f, g being ManySortedSet of NAT st
( n -BitFTA1Layer1Str (ap,bm,cp) = f . n & AA = g . n & f . 0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) & g . 0 = 1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) & ( for k being Nat
for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S st S = f . k & A = g . k holds
( f . (k + 1) = S +* (BitGFA1Str ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1)))) & g . (k + 1) = A +* (BitGFA1Circ ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1)))) ) ) )
take f ; :: thesis: ex g being ManySortedSet of NAT st
( n -BitFTA1Layer1Str (ap,bm,cp) = f . n & AA = g . n & f . 0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) & g . 0 = 1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) & ( for k being Nat
for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S st S = f . k & A = g . k holds
( f . (k + 1) = S +* (BitGFA1Str ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1)))) & g . (k + 1) = A +* (BitGFA1Circ ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1)))) ) ) )
take g ; :: thesis: ( n -BitFTA1Layer1Str (ap,bm,cp) = f . n & AA = g . n & f . 0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) & g . 0 = 1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) & ( for k being Nat
for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S st S = f . k & A = g . k holds
( f . (k + 1) = S +* (BitGFA1Str ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1)))) & g . (k + 1) = A +* (BitGFA1Circ ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1)))) ) ) )
thus ( n -BitFTA1Layer1Str (ap,bm,cp) = f . n & AA = g . n & f . 0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) & g . 0 = 1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) ) by B1; :: thesis: for k being Nat
for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S st S = f . k & A = g . k holds
( f . (k + 1) = S +* (BitGFA1Str ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1)))) & g . (k + 1) = A +* (BitGFA1Circ ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1)))) )
let k be Nat; :: thesis: for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S st S = f . k & A = g . k holds
( f . (k + 1) = S +* (BitGFA1Str ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1)))) & g . (k + 1) = A +* (BitGFA1Circ ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1)))) )
let S be non empty ManySortedSign ; :: thesis: for A being non-empty MSAlgebra over S st S = f . k & A = g . k holds
( f . (k + 1) = S +* (BitGFA1Str ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1)))) & g . (k + 1) = A +* (BitGFA1Circ ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1)))) )
let A be non-empty MSAlgebra over S; :: thesis: ( S = f . k & A = g . k implies ( f . (k + 1) = S +* (BitGFA1Str ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1)))) & g . (k + 1) = A +* (BitGFA1Circ ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1)))) ) )
assume C1: ( S = f . k & A = g . k ) ; :: thesis: ( f . (k + 1) = S +* (BitGFA1Str ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1)))) & g . (k + 1) = A +* (BitGFA1Circ ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1)))) )
C3: hh . k = hh . k ;
thus f . (k + 1) = S +* (BitGFA1Str ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1)))) by B1, C1, C3; :: thesis: g . (k + 1) = A +* (BitGFA1Circ ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1))))
thus g . (k + 1) = A +* (BitGFA1Circ ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1)))) by B1, C1, C3; :: thesis: verum