:: deftheorem Def2 defines carry BINARITH:def 2 :
for n being non zero Nat
for x, y, b₄ being Tuple of n, BOOLEAN holds
( b₄ = carry (x,y) iff ( b₄ /. 1 = FALSE & ( for i being Nat st 1 <= i & i < n holds
b₄ /. (i + 1) = (((x /. i) '&' (y /. i)) 'or' ((x /. i) '&' (b₄ /. i))) 'or' ((y /. i) '&' (b₄ /. i)) ) ) );