Proof: Add Three Uints

Let's prove the following theorem:

sum of unsigned integers (list 1 and (list 1 and (empty list))) and (list 1 and (list 1 and (empty list))) = list 0 and (list 1 and (list 1 and (empty list)))

Proof:

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

Proof Table
# Claim Reason
1 sum of unsigned integers (list 1 and (list 1 and (empty list))) and (list 1 and (list 1 and (empty list))) = sum of (list 1 and (list 1 and (empty list))) (list 1 and (list 1 and (empty list))) and carry bit 0 sum of unsigned integers (list 1 and (list 1 and (empty list))) and (list 1 and (list 1 and (empty list))) = sum of (list 1 and (list 1 and (empty list))) (list 1 and (list 1 and (empty list))) and carry bit 0
2 sum of (list 1 and (list 1 and (empty list))) (list 1 and (list 1 and (empty list))) and carry bit 0 = list (sum of bit 1 bit 1 and bit 0) and (sum of (list 1 and (empty list)) (list 1 and (empty list)) and carry bit (carry on sum of bit 1 bit 1 and 0)) sum of (list 1 and (list 1 and (empty list))) (list 1 and (list 1 and (empty list))) and carry bit 0 = list (sum of bit 1 bit 1 and bit 0) and (sum of (list 1 and (empty list)) (list 1 and (empty list)) and carry bit (carry on sum of bit 1 bit 1 and 0))
3 carry on sum of bit 1 bit 1 and 0 = 1 carry on sum of bit 1 bit 1 and 0 = 1
4 sum of (list 1 and (empty list)) (list 1 and (empty list)) and carry bit (carry on sum of bit 1 bit 1 and 0) = sum of (list 1 and (empty list)) (list 1 and (empty list)) and carry bit 1 if carry on sum of bit 1 bit 1 and 0 = 1, then sum of (list 1 and (empty list)) (list 1 and (empty list)) and carry bit (carry on sum of bit 1 bit 1 and 0) = sum of (list 1 and (empty list)) (list 1 and (empty list)) and carry bit 1
5 sum of (list 1 and (empty list)) (list 1 and (empty list)) and carry bit 1 = list (sum of bit 1 bit 1 and bit 1) and (sum of (empty list) (empty list) and carry bit (carry on sum of bit 1 bit 1 and 1)) sum of (list 1 and (empty list)) (list 1 and (empty list)) and carry bit 1 = list (sum of bit 1 bit 1 and bit 1) and (sum of (empty list) (empty list) and carry bit (carry on sum of bit 1 bit 1 and 1))
6 carry on sum of bit 1 bit 1 and 1 = 1 carry on sum of bit 1 bit 1 and 1 = 1
7 sum of (empty list) (empty list) and carry bit (carry on sum of bit 1 bit 1 and 1) = sum of (empty list) (empty list) and carry bit 1 if carry on sum of bit 1 bit 1 and 1 = 1, then sum of (empty list) (empty list) and carry bit (carry on sum of bit 1 bit 1 and 1) = sum of (empty list) (empty list) and carry bit 1
8 sum of (empty list) (empty list) and carry bit 1 = list 1 and (empty list) sum of (empty list) (empty list) and carry bit 1 = list 1 and (empty list)
9 sum of (empty list) (empty list) and carry bit (carry on sum of bit 1 bit 1 and 1) = list 1 and (empty list) if sum of (empty list) (empty list) and carry bit (carry on sum of bit 1 bit 1 and 1) = sum of (empty list) (empty list) and carry bit 1 and sum of (empty list) (empty list) and carry bit 1 = list 1 and (empty list), then sum of (empty list) (empty list) and carry bit (carry on sum of bit 1 bit 1 and 1) = list 1 and (empty list)
10 list (sum of bit 1 bit 1 and bit 1) and (sum of (empty list) (empty list) and carry bit (carry on sum of bit 1 bit 1 and 1)) = list (sum of bit 1 bit 1 and bit 1) and (list 1 and (empty list)) if sum of (empty list) (empty list) and carry bit (carry on sum of bit 1 bit 1 and 1) = list 1 and (empty list), then list (sum of bit 1 bit 1 and bit 1) and (sum of (empty list) (empty list) and carry bit (carry on sum of bit 1 bit 1 and 1)) = list (sum of bit 1 bit 1 and bit 1) and (list 1 and (empty list))
11 sum of bit 1 bit 1 and bit 1 = 1 sum of bit 1 bit 1 and bit 1 = 1
12 list (sum of bit 1 bit 1 and bit 1) and (list 1 and (empty list)) = list 1 and (list 1 and (empty list)) if sum of bit 1 bit 1 and bit 1 = 1, then list (sum of bit 1 bit 1 and bit 1) and (list 1 and (empty list)) = list 1 and (list 1 and (empty list))
13 list (sum of bit 1 bit 1 and bit 1) and (sum of (empty list) (empty list) and carry bit (carry on sum of bit 1 bit 1 and 1)) = list 1 and (list 1 and (empty list)) if list (sum of bit 1 bit 1 and bit 1) and (sum of (empty list) (empty list) and carry bit (carry on sum of bit 1 bit 1 and 1)) = list (sum of bit 1 bit 1 and bit 1) and (list 1 and (empty list)) and list (sum of bit 1 bit 1 and bit 1) and (list 1 and (empty list)) = list 1 and (list 1 and (empty list)), then list (sum of bit 1 bit 1 and bit 1) and (sum of (empty list) (empty list) and carry bit (carry on sum of bit 1 bit 1 and 1)) = list 1 and (list 1 and (empty list))
14 sum of (list 1 and (empty list)) (list 1 and (empty list)) and carry bit 1 = list 1 and (list 1 and (empty list)) if sum of (list 1 and (empty list)) (list 1 and (empty list)) and carry bit 1 = list (sum of bit 1 bit 1 and bit 1) and (sum of (empty list) (empty list) and carry bit (carry on sum of bit 1 bit 1 and 1)) and list (sum of bit 1 bit 1 and bit 1) and (sum of (empty list) (empty list) and carry bit (carry on sum of bit 1 bit 1 and 1)) = list 1 and (list 1 and (empty list)), then sum of (list 1 and (empty list)) (list 1 and (empty list)) and carry bit 1 = list 1 and (list 1 and (empty list))
15 sum of (list 1 and (empty list)) (list 1 and (empty list)) and carry bit (carry on sum of bit 1 bit 1 and 0) = list 1 and (list 1 and (empty list)) if sum of (list 1 and (empty list)) (list 1 and (empty list)) and carry bit (carry on sum of bit 1 bit 1 and 0) = sum of (list 1 and (empty list)) (list 1 and (empty list)) and carry bit 1 and sum of (list 1 and (empty list)) (list 1 and (empty list)) and carry bit 1 = list 1 and (list 1 and (empty list)), then sum of (list 1 and (empty list)) (list 1 and (empty list)) and carry bit (carry on sum of bit 1 bit 1 and 0) = list 1 and (list 1 and (empty list))
16 list (sum of bit 1 bit 1 and bit 0) and (sum of (list 1 and (empty list)) (list 1 and (empty list)) and carry bit (carry on sum of bit 1 bit 1 and 0)) = list (sum of bit 1 bit 1 and bit 0) and (list 1 and (list 1 and (empty list))) if sum of (list 1 and (empty list)) (list 1 and (empty list)) and carry bit (carry on sum of bit 1 bit 1 and 0) = list 1 and (list 1 and (empty list)), then list (sum of bit 1 bit 1 and bit 0) and (sum of (list 1 and (empty list)) (list 1 and (empty list)) and carry bit (carry on sum of bit 1 bit 1 and 0)) = list (sum of bit 1 bit 1 and bit 0) and (list 1 and (list 1 and (empty list)))
17 sum of bit 1 bit 1 and bit 0 = 0 sum of bit 1 bit 1 and bit 0 = 0
18 list (sum of bit 1 bit 1 and bit 0) and (list 1 and (list 1 and (empty list))) = list 0 and (list 1 and (list 1 and (empty list))) if sum of bit 1 bit 1 and bit 0 = 0, then list (sum of bit 1 bit 1 and bit 0) and (list 1 and (list 1 and (empty list))) = list 0 and (list 1 and (list 1 and (empty list)))
19 list (sum of bit 1 bit 1 and bit 0) and (sum of (list 1 and (empty list)) (list 1 and (empty list)) and carry bit (carry on sum of bit 1 bit 1 and 0)) = list 0 and (list 1 and (list 1 and (empty list))) if list (sum of bit 1 bit 1 and bit 0) and (sum of (list 1 and (empty list)) (list 1 and (empty list)) and carry bit (carry on sum of bit 1 bit 1 and 0)) = list (sum of bit 1 bit 1 and bit 0) and (list 1 and (list 1 and (empty list))) and list (sum of bit 1 bit 1 and bit 0) and (list 1 and (list 1 and (empty list))) = list 0 and (list 1 and (list 1 and (empty list))), then list (sum of bit 1 bit 1 and bit 0) and (sum of (list 1 and (empty list)) (list 1 and (empty list)) and carry bit (carry on sum of bit 1 bit 1 and 0)) = list 0 and (list 1 and (list 1 and (empty list)))
20 sum of (list 1 and (list 1 and (empty list))) (list 1 and (list 1 and (empty list))) and carry bit 0 = list 0 and (list 1 and (list 1 and (empty list))) if sum of (list 1 and (list 1 and (empty list))) (list 1 and (list 1 and (empty list))) and carry bit 0 = list (sum of bit 1 bit 1 and bit 0) and (sum of (list 1 and (empty list)) (list 1 and (empty list)) and carry bit (carry on sum of bit 1 bit 1 and 0)) and list (sum of bit 1 bit 1 and bit 0) and (sum of (list 1 and (empty list)) (list 1 and (empty list)) and carry bit (carry on sum of bit 1 bit 1 and 0)) = list 0 and (list 1 and (list 1 and (empty list))), then sum of (list 1 and (list 1 and (empty list))) (list 1 and (list 1 and (empty list))) and carry bit 0 = list 0 and (list 1 and (list 1 and (empty list)))
21 sum of unsigned integers (list 1 and (list 1 and (empty list))) and (list 1 and (list 1 and (empty list))) = list 0 and (list 1 and (list 1 and (empty list))) if sum of unsigned integers (list 1 and (list 1 and (empty list))) and (list 1 and (list 1 and (empty list))) = sum of (list 1 and (list 1 and (empty list))) (list 1 and (list 1 and (empty list))) and carry bit 0 and sum of (list 1 and (list 1 and (empty list))) (list 1 and (list 1 and (empty list))) and carry bit 0 = list 0 and (list 1 and (list 1 and (empty list))), then sum of unsigned integers (list 1 and (list 1 and (empty list))) and (list 1 and (list 1 and (empty list))) = list 0 and (list 1 and (list 1 and (empty list)))

Comments

Please log in to add comments