for n being non zero Nat
for l, m being Nat st l + m <= (2 to_power (n -' 1)) - 1 holds
(carry ((n -BinarySequence l),(n -BinarySequence m))) /. n = FALSE