:: deftheorem Def11 defines -BitFTA1Layer1Str FTACELL2:def 11 :
for n being Nat
for ap, bm, cp being FinSequence
for b₅ being non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign holds
( b₅ = n -BitFTA1Layer1Str (ap,bm,cp) iff ex f being ManySortedSet of NAT st
( b₅ = f . n & f . 0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) & ( 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)))) ) ) );