:: deftheorem Def7 defines -BitGFA1CarryOutput GFACIRC2:def 7 :
for n being Nat
for x, y being FinSequence
for b₄ being Element of InnerVertices (n -BitGFA1Str (x,y)) holds
( b₄ = n -BitGFA1CarryOutput (x,y) iff ex h being ManySortedSet of NAT st
( b₄ = h . n & h . 0 = [<*>,((0 -tuples_on BOOLEAN) --> TRUE)] & ( for n being Nat holds h . (n + 1) = GFA1CarryOutput ((x . (n + 1)),(y . (n + 1)),(h . n)) ) ) );