:: deftheorem Def12 defines -BitFTA1Layer1Circ FTACELL2:def 12 :
for n being Nat
for ap, bm, cp being FinSequence
for b₅ being strict gate`2=den Boolean Circuit of n -BitFTA1Layer1Str (ap,bm,cp) holds
( b₅ = n -BitFTA1Layer1Circ (ap,bm,cp) iff ex f, g being ManySortedSet of NAT st
( n -BitFTA1Layer1Str (ap,bm,cp) = f . n & b₅ = 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)))) ) ) ) );