Properties
Properties are true expressions. They are used to prove theorems
sum of unsigned integers a and b = sum of a b and carry bit 0
decrement (list 0 and (list 1 and (empty list))) by 1 = list 1 and (empty list)
decrement (list 0 and (list 1 and (list x and xs))) by 1 = list 1 and (list 0 and (list x and xs))
decrement (list 1 and xs) by 1 = list 0 and xs
(list x and xs) multiplied by (list 0 and (empty list)) = list 0 and (empty list)
(list 0 and (empty list)) multiplied by (list y and ys) = list 0 and (empty list)
(list x and xs) multiplied by (list 1 and (empty list)) = list x and xs
(list x and xs) multiplied by (list y and (list y2 and ys)) = sum of unsigned integers (list x and xs) and ((list x and xs) multiplied by (decrement (list y and (list y2 and ys)) by 1))
sum of bit x bit 0 and bit 0 = x
carry on sum of bit x bit 0 and 0 = 0
sum of x (empty list) and carry bit 0 = x
2
3