:: deftheorem Def3 defines -BitGFA0CarryOutput GFACIRC2:def 3 :
for n being Nat
for x, y being FinSequence
for b₄ being Element of InnerVertices (n -BitGFA0Str (x,y)) holds
( b₄ = n -BitGFA0CarryOutput (x,y) 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) = GFA0CarryOutput ((x . (n + 1)),(y . (n + 1)),(h . n)) ) ) );