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