Proof: Multiply Two

Let's prove the following theorem:

(list 1 and (list 1 and (empty list))) multiplied by (list 0 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	(list 1 and (list 1 and (empty list))) multiplied by (list 0 and (list 1 and (empty list))) = sum of unsigned integers (list 1 and (list 1 and (empty list))) and ((list 1 and (list 1 and (empty list))) multiplied by (decrement (list 0 and (list 1 and (empty list))) by 1))	(list 1 and (list 1 and (empty list))) multiplied by (list 0 and (list 1 and (empty list))) = sum of unsigned integers (list 1 and (list 1 and (empty list))) and ((list 1 and (list 1 and (empty list))) multiplied by (decrement (list 0 and (list 1 and (empty list))) by 1)) (Multiply Unsigned Integers)
2	decrement (list 0 and (list 1 and (empty list))) by 1 = list 1 and (empty list)	decrement (list 0 and (list 1 and (empty list))) by 1 = list 1 and (empty list) (Decrement Unsigned Integer)
3	(list 1 and (list 1 and (empty list))) multiplied by (decrement (list 0 and (list 1 and (empty list))) by 1) = (list 1 and (list 1 and (empty list))) multiplied by (list 1 and (empty list))	if decrement (list 0 and (list 1 and (empty list))) by 1 = list 1 and (empty list), then (list 1 and (list 1 and (empty list))) multiplied by (decrement (list 0 and (list 1 and (empty list))) by 1) = (list 1 and (list 1 and (empty list))) multiplied by (list 1 and (empty list)) (Substitution)
4	(list 1 and (list 1 and (empty list))) multiplied by (list 1 and (empty list)) = list 1 and (list 1 and (empty list))	(list 1 and (list 1 and (empty list))) multiplied by (list 1 and (empty list)) = list 1 and (list 1 and (empty list)) (Multiply by 1)
5	(list 1 and (list 1 and (empty list))) multiplied by (decrement (list 0 and (list 1 and (empty list))) by 1) = list 1 and (list 1 and (empty list))	if (list 1 and (list 1 and (empty list))) multiplied by (decrement (list 0 and (list 1 and (empty list))) by 1) = (list 1 and (list 1 and (empty list))) multiplied by (list 1 and (empty list)) and (list 1 and (list 1 and (empty list))) multiplied by (list 1 and (empty list)) = list 1 and (list 1 and (empty list)), then (list 1 and (list 1 and (empty list))) multiplied by (decrement (list 0 and (list 1 and (empty list))) by 1) = list 1 and (list 1 and (empty list)) (Transitive Property of Equality)
6	sum of unsigned integers (list 1 and (list 1 and (empty list))) and ((list 1 and (list 1 and (empty list))) multiplied by (decrement (list 0 and (list 1 and (empty list))) by 1)) = sum of unsigned integers (list 1 and (list 1 and (empty list))) and (list 1 and (list 1 and (empty list)))	if (list 1 and (list 1 and (empty list))) multiplied by (decrement (list 0 and (list 1 and (empty list))) by 1) = 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))) multiplied by (decrement (list 0 and (list 1 and (empty list))) by 1)) = sum of unsigned integers (list 1 and (list 1 and (empty list))) and (list 1 and (list 1 and (empty list))) (Substitution)
7	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)))	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))) (add_three_uints)
8	sum of unsigned integers (list 1 and (list 1 and (empty list))) and ((list 1 and (list 1 and (empty list))) multiplied by (decrement (list 0 and (list 1 and (empty list))) by 1)) = 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))) multiplied by (decrement (list 0 and (list 1 and (empty list))) by 1)) = sum of unsigned integers (list 1 and (list 1 and (empty list))) and (list 1 and (list 1 and (empty list))) and 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))), then sum of unsigned integers (list 1 and (list 1 and (empty list))) and ((list 1 and (list 1 and (empty list))) multiplied by (decrement (list 0 and (list 1 and (empty list))) by 1)) = list 0 and (list 1 and (list 1 and (empty list))) (Transitive Property of Equality)
9	(list 1 and (list 1 and (empty list))) multiplied by (list 0 and (list 1 and (empty list))) = list 0 and (list 1 and (list 1 and (empty list)))	if (list 1 and (list 1 and (empty list))) multiplied by (list 0 and (list 1 and (empty list))) = sum of unsigned integers (list 1 and (list 1 and (empty list))) and ((list 1 and (list 1 and (empty list))) multiplied by (decrement (list 0 and (list 1 and (empty list))) by 1)) and sum of unsigned integers (list 1 and (list 1 and (empty list))) and ((list 1 and (list 1 and (empty list))) multiplied by (decrement (list 0 and (list 1 and (empty list))) by 1)) = list 0 and (list 1 and (list 1 and (empty list))), then (list 1 and (list 1 and (empty list))) multiplied by (list 0 and (list 1 and (empty list))) = list 0 and (list 1 and (list 1 and (empty list))) (Transitive Property of Equality)

Comments

Please log in to add comments