:: deftheorem Def10 defines -BitFTA1CarryOutput FTACELL2:def 10 :
for n being Nat
for ap, bm, cp, dm being FinSequence
for b₆ being Element of InnerVertices (n -BitFTA1Str (ap,bm,cp,dm)) holds
( b₆ = n -BitFTA1CarryOutput (ap,bm,cp,dm) iff ex h being ManySortedSet of NAT st
( b₆ = h . n & h . 0 = [<*>,((0 -tuples_on BOOLEAN) --> FALSE)] & ( for n being Nat holds h . (n + 1) = BitFTA1CarryOutput ((ap . (n + 1)),(bm . (n + 1)),(cp . (n + 1)),(dm . (n + 1)),(h . n)) ) ) );