:: deftheorem Def8 defines -BitGFA1AdderOutput GFACIRC2:def 8 :
for k, n being Nat st k >= 1 & k <= n holds
for x, y being FinSequence
for b₅ being Element of InnerVertices (n -BitGFA1Str (x,y)) holds
( b₅ = (k,n) -BitGFA1AdderOutput (x,y) iff ex i being Nat st
( k = i + 1 & b₅ = GFA1AdderOutput ((x . k),(y . k),(i -BitGFA1CarryOutput (x,y))) ) );