Proof: Add by Zero

Let's prove the following theorem:

sum of unsigned integers (list x and xs) and (list 0 and (empty list)) = list x and xs

Proof:

View as a tree | View dependent proofs | Try proving it

Proof Table
# Claim Reason
1 sum of unsigned integers (list x and xs) and (list 0 and (empty list)) = sum of (list x and xs) (list 0 and (empty list)) and carry bit 0 sum of unsigned integers (list x and xs) and (list 0 and (empty list)) = sum of (list x and xs) (list 0 and (empty list)) and carry bit 0
2 sum of (list x and xs) (list 0 and (empty list)) and carry bit 0 = list (sum of bit x bit 0 and bit 0) and (sum of xs (empty list) and carry bit (carry on sum of bit x bit 0 and 0)) sum of (list x and xs) (list 0 and (empty list)) and carry bit 0 = list (sum of bit x bit 0 and bit 0) and (sum of xs (empty list) and carry bit (carry on sum of bit x bit 0 and 0))
3 carry on sum of bit x bit 0 and 0 = 0 carry on sum of bit x bit 0 and 0 = 0
4 sum of xs (empty list) and carry bit (carry on sum of bit x bit 0 and 0) = sum of xs (empty list) and carry bit 0 if carry on sum of bit x bit 0 and 0 = 0, then sum of xs (empty list) and carry bit (carry on sum of bit x bit 0 and 0) = sum of xs (empty list) and carry bit 0
5 sum of xs (empty list) and carry bit 0 = xs sum of xs (empty list) and carry bit 0 = xs
6 sum of xs (empty list) and carry bit (carry on sum of bit x bit 0 and 0) = xs if sum of xs (empty list) and carry bit (carry on sum of bit x bit 0 and 0) = sum of xs (empty list) and carry bit 0 and sum of xs (empty list) and carry bit 0 = xs, then sum of xs (empty list) and carry bit (carry on sum of bit x bit 0 and 0) = xs
7 list (sum of bit x bit 0 and bit 0) and (sum of xs (empty list) and carry bit (carry on sum of bit x bit 0 and 0)) = list (sum of bit x bit 0 and bit 0) and xs if sum of xs (empty list) and carry bit (carry on sum of bit x bit 0 and 0) = xs, then list (sum of bit x bit 0 and bit 0) and (sum of xs (empty list) and carry bit (carry on sum of bit x bit 0 and 0)) = list (sum of bit x bit 0 and bit 0) and xs
8 sum of bit x bit 0 and bit 0 = x sum of bit x bit 0 and bit 0 = x
9 list (sum of bit x bit 0 and bit 0) and xs = list x and xs if sum of bit x bit 0 and bit 0 = x, then list (sum of bit x bit 0 and bit 0) and xs = list x and xs
10 list (sum of bit x bit 0 and bit 0) and (sum of xs (empty list) and carry bit (carry on sum of bit x bit 0 and 0)) = list x and xs if list (sum of bit x bit 0 and bit 0) and (sum of xs (empty list) and carry bit (carry on sum of bit x bit 0 and 0)) = list (sum of bit x bit 0 and bit 0) and xs and list (sum of bit x bit 0 and bit 0) and xs = list x and xs, then list (sum of bit x bit 0 and bit 0) and (sum of xs (empty list) and carry bit (carry on sum of bit x bit 0 and 0)) = list x and xs
11 sum of (list x and xs) (list 0 and (empty list)) and carry bit 0 = list x and xs if sum of (list x and xs) (list 0 and (empty list)) and carry bit 0 = list (sum of bit x bit 0 and bit 0) and (sum of xs (empty list) and carry bit (carry on sum of bit x bit 0 and 0)) and list (sum of bit x bit 0 and bit 0) and (sum of xs (empty list) and carry bit (carry on sum of bit x bit 0 and 0)) = list x and xs, then sum of (list x and xs) (list 0 and (empty list)) and carry bit 0 = list x and xs
12 sum of unsigned integers (list x and xs) and (list 0 and (empty list)) = list x and xs if sum of unsigned integers (list x and xs) and (list 0 and (empty list)) = sum of (list x and xs) (list 0 and (empty list)) and carry bit 0 and sum of (list x and xs) (list 0 and (empty list)) and carry bit 0 = list x and xs, then sum of unsigned integers (list x and xs) and (list 0 and (empty list)) = list x and xs

Comments

Please log in to add comments