let n be Nat; for ap, bm, cp being FinSequence holds (n + 1) -BitFTA1Layer1Circ (ap,bm,cp) = (n -BitFTA1Layer1Circ (ap,bm,cp)) +* (BitGFA1Circ ((ap . (n + 1)),(bm . (n + 1)),(cp . (n + 1))))
let ap, bm, cp be FinSequence; (n + 1) -BitFTA1Layer1Circ (ap,bm,cp) = (n -BitFTA1Layer1Circ (ap,bm,cp)) +* (BitGFA1Circ ((ap . (n + 1)),(bm . (n + 1)),(cp . (n + 1))))
set S0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE));
set A0 = 1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> FALSE));
deffunc H1( non empty ManySortedSign , set , Nat) -> ManySortedSign = $1 +* (BitGFA1Str ((ap . ($3 + 1)),(bm . ($3 + 1)),(cp . ($3 + 1))));
deffunc H2( 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 H3( set , Nat) -> set = {} ;
consider f1, g1 being ManySortedSet of NAT such that
A1:
n -BitFTA1Layer1Str (ap,bm,cp) = f1 . n
and
A2:
n -BitFTA1Layer1Circ (ap,bm,cp) = g1 . n
and
A3:
f1 . 0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE))
and
A4:
g1 . 0 = 1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> FALSE))
and
A5:
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)))) )
by Def12;
consider f2, g2 being ManySortedSet of NAT such that
(n + 1) -BitFTA1Layer1Str (ap,bm,cp) = f2 . (n + 1)
and
A6:
(n + 1) -BitFTA1Layer1Circ (ap,bm,cp) = g2 . (n + 1)
and
A7:
f2 . 0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE))
and
A8:
g2 . 0 = 1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> FALSE))
and
A9:
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)))) )
by Def12;
reconsider h1 = EmptyMS NAT, h2 = EmptyMS NAT as ManySortedSet of NAT ;
A10:
ex S being non empty ManySortedSign ex A being non-empty MSAlgebra over S st
( S = f1 . 0 & A = g1 . 0 )
by A3, A4;
A11:
( f1 . 0 = f2 . 0 & g1 . 0 = g2 . 0 & h1 . 0 = h2 . 0 )
by A3, A4, A7, A8;
A12:
for k being Nat
for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S
for x being set st S = f1 . k & A = g1 . k & x = h1 . k holds
( f1 . (k + 1) = H1(S,x,k) & g1 . (k + 1) = H2(S,A,x,k) & h1 . (k + 1) = H3(x,k) )
by A5, PBOOLE:5;
A13:
for k being Nat
for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S
for x being set st S = f2 . k & A = g2 . k & x = h2 . k holds
( f2 . (k + 1) = H1(S,x,k) & g2 . (k + 1) = H2(S,A,x,k) & h2 . (k + 1) = H3(x,k) )
by A9, PBOOLE:5;
A14:
for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S
for x being set
for k being Nat holds H2(S,A,x,k) is non-empty MSAlgebra over H1(S,x,k)
;
A15:
( f1 = f2 & g1 = g2 & h1 = h2 )
from CIRCCMB2:sch 14(A10, A11, A12, A13, A14);
thus
(n + 1) -BitFTA1Layer1Circ (ap,bm,cp) = (n -BitFTA1Layer1Circ (ap,bm,cp)) +* (BitGFA1Circ ((ap . (n + 1)),(bm . (n + 1)),(cp . (n + 1))))
by A15, A6, A5, A1, A2; verum