:: deftheorem Def4 defines -BitSubtracterOutput FSCIRC_2: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 -BitSubtracterStr (x,y)) holds
( b₅ = (k,n) -BitSubtracterOutput (x,y) iff ex i being Element of NAT st
( k = i + 1 & b₅ = BitSubtracterOutput ((x . k),(y . k),(i -BitBorrowOutput (x,y))) ) );