Thread: Correctness of the addition algorithm

Hello, the addition algorithm that is commonly used in the base 10 positional notation seems to make sense:
-we add the 1s with the 1s
-we add the 10s with the 10s
...
-when we reach at least 10 units in a position, we increment the following position and leave the remainder in the current position

yet can someone provide me with a proof that the addition algorithm guarantees that adding, for instance, 12 with 10 will yield the same result as 12 +1+1+1+1+1+1+1+1+1... (10 times)?
I know that 10 is the same as 1+1+1+1+1+1 (10 times) plus 12 = 1+1+1+1+1.... since the resulting number of 1s is the same. But what guarantees that this happens in the addition algorithm? What does it make to support this?

Thanks in advance

This is how I see a way to formalize your question. Long addition operates on strings of decimal digits. On the other hand, we can define our basic addition, which is our starting point, to operate on strings of 1's (unary notation), or, equivalently, on terms of the form S(S(...S(0)...)) (here S stands for "successor"). We can define unary addition and multiplication by recursion as follows.

0 + y = y
S(x) + y = S(x + y)

x * 0 = 0
x * S(y) = x * y + x

These definition are supposed to express our intuitive concept of addition and multiplication and act as a starting point.

We can also define a translation from decimal to unary strings, also by recursion:

f(0) = 0
f(1) = S(0)
f(2) = S(S(0))
...
f(9) = S(S(S(S(S(S(S(S(S(0)))))))))
f(ds) = S(S(S(S(S(S(S(S(S(S(0)))))))))) * f(d) + f(s) where d is a decimal digit and s is a string of decimal digits.

Finally, we define long addition on decimal string. Let's denote it by add(s1, s2). Then correctness of long addition (with respect to unary addition) means that

f(s1) + f(s2) = f(add(s1, s2)) for all decimal strings s1, s2.

Similar theorems for binary addition were formally proved using proof assistants like PVS, Coq and Isabelle.