Add Three Uints
Multiply Two

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))
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)
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))
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))
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))
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)))
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)))
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)))
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)))
Previous Lesson

Comments

Please log in to add comments