Proof: Add Two
Let's prove the following theorem:
sum of unsigned integers (list 1 and (empty list)) and (list 1 and (empty list)) = list 0 and (list 1 and (empty list))
Proof:
# | Claim | Reason |
---|---|---|
1 | sum of unsigned integers (list 1 and (empty list)) and (list 1 and (empty list)) = sum of (list 1 and (empty list)) (list 1 and (empty list)) and carry bit 0 | sum of unsigned integers (list 1 and (empty list)) and (list 1 and (empty list)) = sum of (list 1 and (empty list)) (list 1 and (empty list)) and carry bit 0 |
2 | sum of (list 1 and (empty list)) (list 1 and (empty list)) and carry bit 0 = list (sum of bit 1 bit 1 and bit 0) and (sum of (empty list) (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 0 = list (sum of bit 1 bit 1 and bit 0) and (sum of (empty list) (empty list) and carry bit (carry on sum of bit 1 bit 1 and 0)) |
3 | sum of unsigned integers (list 1 and (empty list)) and (list 1 and (empty list)) = list (sum of bit 1 bit 1 and bit 0) and (sum of (empty list) (empty list) and carry bit (carry on sum of bit 1 bit 1 and 0)) | if sum of unsigned integers (list 1 and (empty list)) and (list 1 and (empty list)) = sum of (list 1 and (empty list)) (list 1 and (empty list)) and carry bit 0 and sum of (list 1 and (empty list)) (list 1 and (empty list)) and carry bit 0 = list (sum of bit 1 bit 1 and bit 0) and (sum of (empty list) (empty list) and carry bit (carry on sum of bit 1 bit 1 and 0)), then sum of unsigned integers (list 1 and (empty list)) and (list 1 and (empty list)) = list (sum of bit 1 bit 1 and bit 0) and (sum of (empty list) (empty list) and carry bit (carry on sum of bit 1 bit 1 and 0)) |
4 | sum of bit 1 bit 1 and bit 0 = 0 | sum of bit 1 bit 1 and bit 0 = 0 |
5 | list (sum of bit 1 bit 1 and bit 0) and (sum of (empty list) (empty list) and carry bit (carry on sum of bit 1 bit 1 and 0)) = list 0 and (sum of (empty list) (empty list) and carry bit (carry on sum of bit 1 bit 1 and 0)) | if sum of bit 1 bit 1 and bit 0 = 0, then list (sum of bit 1 bit 1 and bit 0) and (sum of (empty list) (empty list) and carry bit (carry on sum of bit 1 bit 1 and 0)) = list 0 and (sum of (empty list) (empty list) and carry bit (carry on sum of bit 1 bit 1 and 0)) |
6 | sum of unsigned integers (list 1 and (empty list)) and (list 1 and (empty list)) = list 0 and (sum of (empty list) (empty list) and carry bit (carry on sum of bit 1 bit 1 and 0)) | if sum of unsigned integers (list 1 and (empty list)) and (list 1 and (empty list)) = list (sum of bit 1 bit 1 and bit 0) and (sum of (empty list) (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 (empty list) (empty list) and carry bit (carry on sum of bit 1 bit 1 and 0)) = list 0 and (sum of (empty list) (empty list) and carry bit (carry on sum of bit 1 bit 1 and 0)), then sum of unsigned integers (list 1 and (empty list)) and (list 1 and (empty list)) = list 0 and (sum of (empty list) (empty list) and carry bit (carry on sum of bit 1 bit 1 and 0)) |
7 | carry on sum of bit 1 bit 1 and 0 = 1 | carry on sum of bit 1 bit 1 and 0 = 1 |
8 | sum of (empty list) (empty list) and carry bit (carry on sum of bit 1 bit 1 and 0) = sum of (empty list) (empty list) and carry bit 1 | if carry on sum of bit 1 bit 1 and 0 = 1, then sum of (empty list) (empty list) and carry bit (carry on sum of bit 1 bit 1 and 0) = sum of (empty list) (empty list) and carry bit 1 |
9 | 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) |
10 | sum of (empty list) (empty list) and carry bit (carry on sum of bit 1 bit 1 and 0) = list 1 and (empty list) | if sum of (empty list) (empty list) and carry bit (carry on sum of bit 1 bit 1 and 0) = 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 0) = list 1 and (empty list) |
11 | list 0 and (sum of (empty list) (empty list) and carry bit (carry on sum of bit 1 bit 1 and 0)) = list 0 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 0) = list 1 and (empty list), then list 0 and (sum of (empty list) (empty list) and carry bit (carry on sum of bit 1 bit 1 and 0)) = list 0 and (list 1 and (empty list)) |
12 | sum of unsigned integers (list 1 and (empty list)) and (list 1 and (empty list)) = list 0 and (list 1 and (empty list)) | if sum of unsigned integers (list 1 and (empty list)) and (list 1 and (empty list)) = list 0 and (sum of (empty list) (empty list) and carry bit (carry on sum of bit 1 bit 1 and 0)) and list 0 and (sum of (empty list) (empty list) and carry bit (carry on sum of bit 1 bit 1 and 0)) = list 0 and (list 1 and (empty list)), then sum of unsigned integers (list 1 and (empty list)) and (list 1 and (empty list)) = list 0 and (list 1 and (empty list)) |
Comments
Please log in to add comments