:: deftheorem Def5 defines -BitFTA0Layer1Circ FTACELL2:def 5 :
for n being Nat
for ap, bp, cp being FinSequence
for b₅ being strict gate`2=den Boolean Circuit of n -BitFTA0Layer1Str (ap,bp,cp) holds
( b₅ = n -BitFTA0Layer1Circ (ap,bp,cp) iff ex f, g being ManySortedSet of NAT st
( n -BitFTA0Layer1Str (ap,bp,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 +* (BitGFA0Str ((ap . (k + 1)),(bp . (k + 1)),(cp . (k + 1)))) & g . (k + 1) = A +* (BitGFA0Circ ((ap . (k + 1)),(bp . (k + 1)),(cp . (k + 1)))) ) ) ) );