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 = {} ;
Q1: 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) ;
let AA1, AA2 be strict gate`2=den Boolean Circuit of n -BitFTA1Layer1Str (ap,bm,cp); :: thesis: ( ex f, g being ManySortedSet of NAT st
( n -BitFTA1Layer1Str (ap,bm,cp) = f . n & AA1 = 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)))) ) ) ) & ex f, g being ManySortedSet of NAT st
( n -BitFTA1Layer1Str (ap,bm,cp) = f . n & AA2 = 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)))) ) ) ) implies AA1 = AA2 )
given f1, g1 being ManySortedSet of NAT such that E1: n -BitFTA1Layer1Str (ap,bm,cp) = f1 . n and
E1b: AA1 = g1 . n and
E2: f1 . 0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) and
E2b: g1 . 0 = 1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) and
E3: for k being Nat
for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S st S = f1 . k & A = g1 . k holds
( f1 . (k + 1) = S +* (BitGFA1Str ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1)))) & g1 . (k + 1) = A +* (BitGFA1Circ ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1)))) ) ; :: thesis: ( for f, g being ManySortedSet of NAT holds
( not n -BitFTA1Layer1Str (ap,bm,cp) = f . n or not AA2 = g . n or not f . 0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) or not g . 0 = 1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) or ex k being Nat ex S being non empty ManySortedSign ex A being non-empty MSAlgebra over S st
( S = f . k & A = g . k & not ( 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)))) ) ) ) or AA1 = AA2 )
given f2, g2 being ManySortedSet of NAT such that E4: n -BitFTA1Layer1Str (ap,bm,cp) = f2 . n and
E4b: AA2 = g2 . n and
E5: f2 . 0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) and
E5b: g2 . 0 = 1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) and
E6: for k being Nat
for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S st S = f2 . k & A = g2 . k holds
( f2 . (k + 1) = S +* (BitGFA1Str ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1)))) & g2 . (k + 1) = A +* (BitGFA1Circ ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1)))) ) ; :: thesis: AA1 = AA2
P1: ex f, g, hh being ManySortedSet of NAT st
( n -BitFTA1Layer1Str (ap,bm,cp) = f . n & AA1 = 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) ) ) )

proof

take f1 ; :: thesis: ex g, hh being ManySortedSet of NAT st
( n -BitFTA1Layer1Str (ap,bm,cp) = f1 . n & AA1 = g . n & f1 . 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 = f1 . m & A = g . m & x = hh . m holds
( f1 . (m + 1) = H₁(S,x,m) & g . (m + 1) = H₂(S,A,x,m) & hh . (m + 1) = H₃(x,m) ) ) )
take g1 ; :: thesis: ex hh being ManySortedSet of NAT st
( n -BitFTA1Layer1Str (ap,bm,cp) = f1 . n & AA1 = g1 . n & f1 . 0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) & g1 . 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 = f1 . m & A = g1 . m & x = hh . m holds
( f1 . (m + 1) = H₁(S,x,m) & g1 . (m + 1) = H₂(S,A,x,m) & hh . (m + 1) = H₃(x,m) ) ) )
take EmptyMS NAT ; :: thesis: ( n -BitFTA1Layer1Str (ap,bm,cp) = f1 . n & AA1 = g1 . n & f1 . 0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) & g1 . 0 = 1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) & (EmptyMS NAT) . 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 = f1 . m & A = g1 . m & x = (EmptyMS NAT) . m holds
( f1 . (m + 1) = H₁(S,x,m) & g1 . (m + 1) = H₂(S,A,x,m) & (EmptyMS NAT) . (m + 1) = H₃(x,m) ) ) )
thus ( n -BitFTA1Layer1Str (ap,bm,cp) = f1 . n & AA1 = g1 . n & f1 . 0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) & g1 . 0 = 1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) & (EmptyMS NAT) . 0 = {} ) by E1, E1b, E2, E2b, PBOOLE:5; :: thesis: for m being Nat
for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S
for x being set st S = f1 . m & A = g1 . m & x = (EmptyMS NAT) . m holds
( f1 . (m + 1) = H₁(S,x,m) & g1 . (m + 1) = H₂(S,A,x,m) & (EmptyMS NAT) . (m + 1) = H₃(x,m) )
let m be Nat; :: thesis: for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S
for x being set st S = f1 . m & A = g1 . m & x = (EmptyMS NAT) . m holds
( f1 . (m + 1) = H₁(S,x,m) & g1 . (m + 1) = H₂(S,A,x,m) & (EmptyMS NAT) . (m + 1) = H₃(x,m) )
let S be non empty ManySortedSign ; :: thesis: for A being non-empty MSAlgebra over S
for x being set st S = f1 . m & A = g1 . m & x = (EmptyMS NAT) . m holds
( f1 . (m + 1) = H₁(S,x,m) & g1 . (m + 1) = H₂(S,A,x,m) & (EmptyMS NAT) . (m + 1) = H₃(x,m) )
let A be non-empty MSAlgebra over S; :: thesis: for x being set st S = f1 . m & A = g1 . m & x = (EmptyMS NAT) . m holds
( f1 . (m + 1) = H₁(S,x,m) & g1 . (m + 1) = H₂(S,A,x,m) & (EmptyMS NAT) . (m + 1) = H₃(x,m) )
let x be set ; :: thesis: ( S = f1 . m & A = g1 . m & x = (EmptyMS NAT) . m implies ( f1 . (m + 1) = H₁(S,x,m) & g1 . (m + 1) = H₂(S,A,x,m) & (EmptyMS NAT) . (m + 1) = H₃(x,m) ) )
assume that
H1: ( S = f1 . m & A = g1 . m ) and
x = (EmptyMS NAT) . m ; :: thesis: ( f1 . (m + 1) = H₁(S,x,m) & g1 . (m + 1) = H₂(S,A,x,m) & (EmptyMS NAT) . (m + 1) = H₃(x,m) )
thus ( f1 . (m + 1) = H₁(S,x,m) & g1 . (m + 1) = H₂(S,A,x,m) ) by E3, H1; :: thesis: (EmptyMS NAT) . (m + 1) = H₃(x,m)
thus (EmptyMS NAT) . (m + 1) = H₃(x,m) by PBOOLE:5; :: thesis: verum

end;

P2: ex f, g, hh being ManySortedSet of NAT st
( n -BitFTA1Layer1Str (ap,bm,cp) = f . n & AA2 = 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) ) ) )

proof

take f2 ; :: thesis: ex g, hh being ManySortedSet of NAT st
( n -BitFTA1Layer1Str (ap,bm,cp) = f2 . n & AA2 = g . n & f2 . 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 = f2 . m & A = g . m & x = hh . m holds
( f2 . (m + 1) = H₁(S,x,m) & g . (m + 1) = H₂(S,A,x,m) & hh . (m + 1) = H₃(x,m) ) ) )
take g2 ; :: thesis: ex hh being ManySortedSet of NAT st
( n -BitFTA1Layer1Str (ap,bm,cp) = f2 . n & AA2 = g2 . n & f2 . 0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) & g2 . 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 = f2 . m & A = g2 . m & x = hh . m holds
( f2 . (m + 1) = H₁(S,x,m) & g2 . (m + 1) = H₂(S,A,x,m) & hh . (m + 1) = H₃(x,m) ) ) )
take EmptyMS NAT ; :: thesis: ( n -BitFTA1Layer1Str (ap,bm,cp) = f2 . n & AA2 = g2 . n & f2 . 0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) & g2 . 0 = 1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) & (EmptyMS NAT) . 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 = f2 . m & A = g2 . m & x = (EmptyMS NAT) . m holds
( f2 . (m + 1) = H₁(S,x,m) & g2 . (m + 1) = H₂(S,A,x,m) & (EmptyMS NAT) . (m + 1) = H₃(x,m) ) ) )
thus ( n -BitFTA1Layer1Str (ap,bm,cp) = f2 . n & AA2 = g2 . n & f2 . 0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) & g2 . 0 = 1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) & (EmptyMS NAT) . 0 = {} ) by E4, E4b, E5, E5b, PBOOLE:5; :: thesis: for m being Nat
for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S
for x being set st S = f2 . m & A = g2 . m & x = (EmptyMS NAT) . m holds
( f2 . (m + 1) = H₁(S,x,m) & g2 . (m + 1) = H₂(S,A,x,m) & (EmptyMS NAT) . (m + 1) = H₃(x,m) )
let m be Nat; :: thesis: for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S
for x being set st S = f2 . m & A = g2 . m & x = (EmptyMS NAT) . m holds
( f2 . (m + 1) = H₁(S,x,m) & g2 . (m + 1) = H₂(S,A,x,m) & (EmptyMS NAT) . (m + 1) = H₃(x,m) )
let S be non empty ManySortedSign ; :: thesis: for A being non-empty MSAlgebra over S
for x being set st S = f2 . m & A = g2 . m & x = (EmptyMS NAT) . m holds
( f2 . (m + 1) = H₁(S,x,m) & g2 . (m + 1) = H₂(S,A,x,m) & (EmptyMS NAT) . (m + 1) = H₃(x,m) )
let A be non-empty MSAlgebra over S; :: thesis: for x being set st S = f2 . m & A = g2 . m & x = (EmptyMS NAT) . m holds
( f2 . (m + 1) = H₁(S,x,m) & g2 . (m + 1) = H₂(S,A,x,m) & (EmptyMS NAT) . (m + 1) = H₃(x,m) )
let x be set ; :: thesis: ( S = f2 . m & A = g2 . m & x = (EmptyMS NAT) . m implies ( f2 . (m + 1) = H₁(S,x,m) & g2 . (m + 1) = H₂(S,A,x,m) & (EmptyMS NAT) . (m + 1) = H₃(x,m) ) )
assume that
H2: ( S = f2 . m & A = g2 . m ) and
x = (EmptyMS NAT) . m ; :: thesis: ( f2 . (m + 1) = H₁(S,x,m) & g2 . (m + 1) = H₂(S,A,x,m) & (EmptyMS NAT) . (m + 1) = H₃(x,m) )
thus ( f2 . (m + 1) = H₁(S,x,m) & g2 . (m + 1) = H₂(S,A,x,m) ) by E6, H2; :: thesis: (EmptyMS NAT) . (m + 1) = H₃(x,m)
thus (EmptyMS NAT) . (m + 1) = H₃(x,m) by PBOOLE:5; :: thesis: verum

end;

for B1, B2 being strict gate`2=den Boolean Circuit of n -BitFTA1Layer1Str (ap,bm,cp) st ex f, g, hh being ManySortedSet of NAT st
( n -BitFTA1Layer1Str (ap,bm,cp) = f . n & B1 = 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) ) ) ) & ex f, g, hh being ManySortedSet of NAT st
( n -BitFTA1Layer1Str (ap,bm,cp) = f . n & B2 = 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) ) ) ) holds
B1 = B2 from CIRCCMB2:sch 21(Q1);
hence AA1 = AA2 by P1, P2; :: thesis: verum