Proof: Add Two

Let's prove the following theorem:

Proof:

Proof Table

#	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 (Add Unsigned Integer)
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)) (Add List Carry (9))
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)) (Transitive Property of Equality)
4	sum of bit 1 bit 1 and bit 0 = 0	sum of bit 1 bit 1 and bit 0 = 0 (Add 1, 1, 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)) (Substitution)
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)) (Transitive Property of Equality)
7	carry on sum of bit 1 bit 1 and 0 = 1	carry on sum of bit 1 bit 1 and 0 = 1 (Add Carry 1 1 0)
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 (Substitution)
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) (Add List Carry (2))
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) (Transitive Property of Equality)
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)) (Substitution)
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)) (Transitive Property of Equality)

Comments

Please log in to add comments