:: deftheorem Def4 defines -BitFTA0Layer1Str FTACELL2:def 4 :
for n being Nat
for ap, bp, cp being FinSequence
for b₅ being non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign holds
( b₅ = n -BitFTA0Layer1Str (ap,bp,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 +* (BitGFA0Str ((ap . (k + 1)),(bp . (k + 1)),(cp . (k + 1)))) ) ) );