:: deftheorem Def4 defines -BitGFA0AdderOutput GFACIRC2:def 4 :
for k, n being Nat st k >= 1 & k <= n holds
for x, y being FinSequence
for b₅ being Element of InnerVertices (n -BitGFA0Str (x,y)) holds
( b₅ = (k,n) -BitGFA0AdderOutput (x,y) iff ex i being Nat st
( k = i + 1 & b₅ = GFA0AdderOutput ((x . k),(y . k),(i -BitGFA0CarryOutput (x,y))) ) );