Proof: Add Three by Zero

Let's prove the following theorem:

sum of unsigned integers (list 1 and (list 1 and (empty list))) and (list 0 and (empty list)) = 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 0 and (empty list)) = sum of (list 1 and (list 1 and (empty list))) (list 0 and (empty list)) and carry bit 0 sum of unsigned integers (list 1 and (list 1 and (empty list))) and (list 0 and (empty list)) = sum of (list 1 and (list 1 and (empty list))) (list 0 and (empty list)) and carry bit 0
2 sum of (list 1 and (list 1 and (empty list))) (list 0 and (empty list)) and carry bit 0 = list (sum of bit 1 bit 0 and bit 0) and (sum of (list 1 and (empty list)) (empty list) and carry bit (carry on sum of bit 1 bit 0 and 0)) sum of (list 1 and (list 1 and (empty list))) (list 0 and (empty list)) and carry bit 0 = list (sum of bit 1 bit 0 and bit 0) and (sum of (list 1 and (empty list)) (empty list) and carry bit (carry on sum of bit 1 bit 0 and 0))
3 carry on sum of bit 1 bit 0 and 0 = 0 carry on sum of bit 1 bit 0 and 0 = 0
4 sum of (list 1 and (empty list)) (empty list) and carry bit (carry on sum of bit 1 bit 0 and 0) = sum of (list 1 and (empty list)) (empty list) and carry bit 0 if carry on sum of bit 1 bit 0 and 0 = 0, then sum of (list 1 and (empty list)) (empty list) and carry bit (carry on sum of bit 1 bit 0 and 0) = sum of (list 1 and (empty list)) (empty list) and carry bit 0
5 sum of (list 1 and (empty list)) (empty list) and carry bit 0 = list 1 and (empty list) sum of (list 1 and (empty list)) (empty list) and carry bit 0 = list 1 and (empty list)
6 sum of (list 1 and (empty list)) (empty list) and carry bit (carry on sum of bit 1 bit 0 and 0) = list 1 and (empty list) if sum of (list 1 and (empty list)) (empty list) and carry bit (carry on sum of bit 1 bit 0 and 0) = sum of (list 1 and (empty list)) (empty list) and carry bit 0 and sum of (list 1 and (empty list)) (empty list) and carry bit 0 = list 1 and (empty list), then sum of (list 1 and (empty list)) (empty list) and carry bit (carry on sum of bit 1 bit 0 and 0) = list 1 and (empty list)
7 list (sum of bit 1 bit 0 and bit 0) and (sum of (list 1 and (empty list)) (empty list) and carry bit (carry on sum of bit 1 bit 0 and 0)) = list (sum of bit 1 bit 0 and bit 0) and (list 1 and (empty list)) if sum of (list 1 and (empty list)) (empty list) and carry bit (carry on sum of bit 1 bit 0 and 0) = list 1 and (empty list), then list (sum of bit 1 bit 0 and bit 0) and (sum of (list 1 and (empty list)) (empty list) and carry bit (carry on sum of bit 1 bit 0 and 0)) = list (sum of bit 1 bit 0 and bit 0) and (list 1 and (empty list))
8 sum of bit 1 bit 0 and bit 0 = 1 sum of bit 1 bit 0 and bit 0 = 1
9 list (sum of bit 1 bit 0 and bit 0) and (list 1 and (empty list)) = list 1 and (list 1 and (empty list)) if sum of bit 1 bit 0 and bit 0 = 1, then list (sum of bit 1 bit 0 and bit 0) and (list 1 and (empty list)) = list 1 and (list 1 and (empty list))
10 list (sum of bit 1 bit 0 and bit 0) and (sum of (list 1 and (empty list)) (empty list) and carry bit (carry on sum of bit 1 bit 0 and 0)) = list 1 and (list 1 and (empty list)) if list (sum of bit 1 bit 0 and bit 0) and (sum of (list 1 and (empty list)) (empty list) and carry bit (carry on sum of bit 1 bit 0 and 0)) = list (sum of bit 1 bit 0 and bit 0) and (list 1 and (empty list)) and list (sum of bit 1 bit 0 and bit 0) and (list 1 and (empty list)) = list 1 and (list 1 and (empty list)), then list (sum of bit 1 bit 0 and bit 0) and (sum of (list 1 and (empty list)) (empty list) and carry bit (carry on sum of bit 1 bit 0 and 0)) = list 1 and (list 1 and (empty list))
11 sum of (list 1 and (list 1 and (empty list))) (list 0 and (empty list)) and carry bit 0 = list 1 and (list 1 and (empty list)) if sum of (list 1 and (list 1 and (empty list))) (list 0 and (empty list)) and carry bit 0 = list (sum of bit 1 bit 0 and bit 0) and (sum of (list 1 and (empty list)) (empty list) and carry bit (carry on sum of bit 1 bit 0 and 0)) and list (sum of bit 1 bit 0 and bit 0) and (sum of (list 1 and (empty list)) (empty list) and carry bit (carry on sum of bit 1 bit 0 and 0)) = list 1 and (list 1 and (empty list)), then sum of (list 1 and (list 1 and (empty list))) (list 0 and (empty list)) and carry bit 0 = list 1 and (list 1 and (empty list))
12 sum of unsigned integers (list 1 and (list 1 and (empty list))) and (list 0 and (empty list)) = list 1 and (list 1 and (empty list)) if sum of unsigned integers (list 1 and (list 1 and (empty list))) and (list 0 and (empty list)) = sum of (list 1 and (list 1 and (empty list))) (list 0 and (empty list)) and carry bit 0 and sum of (list 1 and (list 1 and (empty list))) (list 0 and (empty list)) and carry bit 0 = list 1 and (list 1 and (empty list)), then sum of unsigned integers (list 1 and (list 1 and (empty list))) and (list 0 and (empty list)) = list 1 and (list 1 and (empty list))

Comments

Please log in to add comments