:: deftheorem Def3 defines -BitFTA0CarryOutput FTACELL2:def 3 :
for n being Nat
for ap, bp, cp, dp being FinSequence
for b₆ being Element of InnerVertices (n -BitFTA0Str (ap,bp,cp,dp)) holds
( b₆ = n -BitFTA0CarryOutput (ap,bp,cp,dp) 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) = BitFTA0CarryOutput ((ap . (n + 1)),(bp . (n + 1)),(cp . (n + 1)),(dp . (n + 1)),(h . n)) ) ) );