Properties
Properties are true expressions. They are used to prove theorems
sum of bit 0 bit 1 and bit 1 = 0
sum of bit 1 bit 1 and bit 1 = 1
carry on sum of bit 0 bit 0 and 0 = 0
carry on sum of bit 1 bit 0 and 0 = 0
carry on sum of bit 0 bit 1 and 0 = 0
carry on sum of bit 1 bit 1 and 0 = 1
carry on sum of bit 0 bit 0 and 1 = 0
carry on sum of bit 1 bit 0 and 1 = 1
carry on sum of bit 0 bit 1 and 1 = 1
carry on sum of bit 1 bit 1 and 1 = 1
sum of (empty list) (empty list) and carry bit 0 = empty list
sum of (empty list) (empty list) and carry bit 1 = list 1 and (empty list)
sum of (list x and xs) (empty list) and carry bit 0 = list x and xs
sum of (list 0 and xs) (empty list) and carry bit 1 = list 1 and xs
sum of (list 1 and xs) (empty list) and carry bit 1 = list 0 and (sum of xs (empty list) and carry bit 1)
sum of (empty list) (list y and ys) and carry bit 0 = list y and ys
sum of (empty list) (list 0 and ys) and carry bit 1 = list 1 and ys
sum of (empty list) (list 1 and ys) and carry bit 1 = list 0 and (sum of (empty list) ys and carry bit 1)
sum of (list x and xs) (list y and ys) and carry bit carry = list (sum of bit x bit y and bit carry) and (sum of xs ys and carry bit (carry on sum of bit x bit y and carry))
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
Pages:
2
3