Multiply by Two

Proof: Multiply by Two

Let's prove the following theorem:

(list x and xs) multiplied by (list 0 and (list 1 and (empty list))) = sum of unsigned integers (list x and xs) and (list x and xs)

Proof:

View as a tree | View dependent proofs | Try proving it

Proof Table
# Claim Reason
1 (list x and xs) multiplied by (list 0 and (list 1 and (empty list))) = sum of unsigned integers (list x and xs) and ((list x and xs) multiplied by (decrement (list 0 and (list 1 and (empty list))) by 1)) (list x and xs) multiplied by (list 0 and (list 1 and (empty list))) = sum of unsigned integers (list x and xs) and ((list x and xs) 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 x and xs) multiplied by (decrement (list 0 and (list 1 and (empty list))) by 1) = (list x and xs) 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 x and xs) multiplied by (decrement (list 0 and (list 1 and (empty list))) by 1) = (list x and xs) multiplied by (list 1 and (empty list))
4 sum of unsigned integers (list x and xs) and ((list x and xs) multiplied by (decrement (list 0 and (list 1 and (empty list))) by 1)) = sum of unsigned integers (list x and xs) and ((list x and xs) multiplied by (list 1 and (empty list))) if (list x and xs) multiplied by (decrement (list 0 and (list 1 and (empty list))) by 1) = (list x and xs) multiplied by (list 1 and (empty list)), then sum of unsigned integers (list x and xs) and ((list x and xs) multiplied by (decrement (list 0 and (list 1 and (empty list))) by 1)) = sum of unsigned integers (list x and xs) and ((list x and xs) multiplied by (list 1 and (empty list)))
5 (list x and xs) multiplied by (list 1 and (empty list)) = list x and xs (list x and xs) multiplied by (list 1 and (empty list)) = list x and xs
6 sum of unsigned integers (list x and xs) and ((list x and xs) multiplied by (list 1 and (empty list))) = sum of unsigned integers (list x and xs) and (list x and xs) if (list x and xs) multiplied by (list 1 and (empty list)) = list x and xs, then sum of unsigned integers (list x and xs) and ((list x and xs) multiplied by (list 1 and (empty list))) = sum of unsigned integers (list x and xs) and (list x and xs)
7 sum of unsigned integers (list x and xs) and ((list x and xs) multiplied by (decrement (list 0 and (list 1 and (empty list))) by 1)) = sum of unsigned integers (list x and xs) and (list x and xs) if sum of unsigned integers (list x and xs) and ((list x and xs) multiplied by (decrement (list 0 and (list 1 and (empty list))) by 1)) = sum of unsigned integers (list x and xs) and ((list x and xs) multiplied by (list 1 and (empty list))) and sum of unsigned integers (list x and xs) and ((list x and xs) multiplied by (list 1 and (empty list))) = sum of unsigned integers (list x and xs) and (list x and xs), then sum of unsigned integers (list x and xs) and ((list x and xs) multiplied by (decrement (list 0 and (list 1 and (empty list))) by 1)) = sum of unsigned integers (list x and xs) and (list x and xs)
8 (list x and xs) multiplied by (list 0 and (list 1 and (empty list))) = sum of unsigned integers (list x and xs) and (list x and xs) if (list x and xs) multiplied by (list 0 and (list 1 and (empty list))) = sum of unsigned integers (list x and xs) and ((list x and xs) multiplied by (decrement (list 0 and (list 1 and (empty list))) by 1)) and sum of unsigned integers (list x and xs) and ((list x and xs) multiplied by (decrement (list 0 and (list 1 and (empty list))) by 1)) = sum of unsigned integers (list x and xs) and (list x and xs), then (list x and xs) multiplied by (list 0 and (list 1 and (empty list))) = sum of unsigned integers (list x and xs) and (list x and xs)

Comments

Please log in to add comments