Proof: Add One

Let's prove the following theorem:

Proof:

Proof Table

#	Claim	Reason
1	sum of (list 0 and (empty list)) (list 0 and (empty list)) and carry bit 0 = list (sum of bit 0 bit 0 and bit 0) and (sum of (empty list) (empty list) and carry bit (carry on sum of bit 0 bit 0 and 0))	sum of (list 0 and (empty list)) (list 0 and (empty list)) and carry bit 0 = list (sum of bit 0 bit 0 and bit 0) and (sum of (empty list) (empty list) and carry bit (carry on sum of bit 0 bit 0 and 0)) (Add List Carry (9))
2	sum of bit 0 bit 0 and bit 0 = 0	sum of bit 0 bit 0 and bit 0 = 0 (Add 0, 0, 0)
3	list (sum of bit 0 bit 0 and bit 0) and (sum of (empty list) (empty list) and carry bit (carry on sum of bit 0 bit 0 and 0)) = list 0 and (sum of (empty list) (empty list) and carry bit (carry on sum of bit 0 bit 0 and 0))	if sum of bit 0 bit 0 and bit 0 = 0, then list (sum of bit 0 bit 0 and bit 0) and (sum of (empty list) (empty list) and carry bit (carry on sum of bit 0 bit 0 and 0)) = list 0 and (sum of (empty list) (empty list) and carry bit (carry on sum of bit 0 bit 0 and 0)) (Substitution)
4	sum of (list 0 and (empty list)) (list 0 and (empty list)) and carry bit 0 = list 0 and (sum of (empty list) (empty list) and carry bit (carry on sum of bit 0 bit 0 and 0))	if sum of (list 0 and (empty list)) (list 0 and (empty list)) and carry bit 0 = list (sum of bit 0 bit 0 and bit 0) and (sum of (empty list) (empty list) and carry bit (carry on sum of bit 0 bit 0 and 0)) and list (sum of bit 0 bit 0 and bit 0) and (sum of (empty list) (empty list) and carry bit (carry on sum of bit 0 bit 0 and 0)) = list 0 and (sum of (empty list) (empty list) and carry bit (carry on sum of bit 0 bit 0 and 0)), then sum of (list 0 and (empty list)) (list 0 and (empty list)) and carry bit 0 = list 0 and (sum of (empty list) (empty list) and carry bit (carry on sum of bit 0 bit 0 and 0)) (Transitive Property of Equality)
5	carry on sum of bit 0 bit 0 and 0 = 0	carry on sum of bit 0 bit 0 and 0 = 0 (Add Carry 0 0 0)
6	sum of (empty list) (empty list) and carry bit (carry on sum of bit 0 bit 0 and 0) = sum of (empty list) (empty list) and carry bit 0	if carry on sum of bit 0 bit 0 and 0 = 0, then sum of (empty list) (empty list) and carry bit (carry on sum of bit 0 bit 0 and 0) = sum of (empty list) (empty list) and carry bit 0 (Substitution)
7	list 0 and (sum of (empty list) (empty list) and carry bit (carry on sum of bit 0 bit 0 and 0)) = list 0 and (sum of (empty list) (empty list) and carry bit 0)	if sum of (empty list) (empty list) and carry bit (carry on sum of bit 0 bit 0 and 0) = sum of (empty list) (empty list) and carry bit 0, then list 0 and (sum of (empty list) (empty list) and carry bit (carry on sum of bit 0 bit 0 and 0)) = list 0 and (sum of (empty list) (empty list) and carry bit 0) (Substitution)
8	sum of (list 0 and (empty list)) (list 0 and (empty list)) and carry bit 0 = list 0 and (sum of (empty list) (empty list) and carry bit 0)	if sum of (list 0 and (empty list)) (list 0 and (empty list)) and carry bit 0 = list 0 and (sum of (empty list) (empty list) and carry bit (carry on sum of bit 0 bit 0 and 0)) and list 0 and (sum of (empty list) (empty list) and carry bit (carry on sum of bit 0 bit 0 and 0)) = list 0 and (sum of (empty list) (empty list) and carry bit 0), then sum of (list 0 and (empty list)) (list 0 and (empty list)) and carry bit 0 = list 0 and (sum of (empty list) (empty list) and carry bit 0) (Transitive Property of Equality)
9	sum of (empty list) (empty list) and carry bit 0 = empty list	sum of (empty list) (empty list) and carry bit 0 = empty list (Add List Carry)
10	list 0 and (sum of (empty list) (empty list) and carry bit 0) = list 0 and (empty list)	if sum of (empty list) (empty list) and carry bit 0 = empty list, then list 0 and (sum of (empty list) (empty list) and carry bit 0) = list 0 and (empty list) (Substitution)
11	sum of (list 0 and (empty list)) (list 0 and (empty list)) and carry bit 0 = list 0 and (empty list)	if sum of (list 0 and (empty list)) (list 0 and (empty list)) and carry bit 0 = list 0 and (sum of (empty list) (empty list) and carry bit 0) and list 0 and (sum of (empty list) (empty list) and carry bit 0) = list 0 and (empty list), then sum of (list 0 and (empty list)) (list 0 and (empty list)) and carry bit 0 = list 0 and (empty list) (Transitive Property of Equality)

Comments

Please log in to add comments