Properties

Properties are true expressions. They are used to prove theorems

Add 0, 1, 1
sum of bit 0 bit 1 and bit 1 = 0

Add 1, 1, 1
sum of bit 1 bit 1 and bit 1 = 1

Add Carry 0 0 0
carry on sum of bit 0 bit 0 and 0 = 0

Add Carry 1 0 0
carry on sum of bit 1 bit 0 and 0 = 0

Add Carry 0 1 0
carry on sum of bit 0 bit 1 and 0 = 0

Add Carry 1 1 0
carry on sum of bit 1 bit 1 and 0 = 1

Add Carry 0 0 1
carry on sum of bit 0 bit 0 and 1 = 0

Add Carry 1 0 1
carry on sum of bit 1 bit 0 and 1 = 1

Add Carry 0 1 1
carry on sum of bit 0 bit 1 and 1 = 1

Add Carry 1 1 1
carry on sum of bit 1 bit 1 and 1 = 1

Add List Carry
sum of (empty list) (empty list) and carry bit 0 = empty list

Add List Carry (2)
sum of (empty list) (empty list) and carry bit 1 = list 1 and (empty list)

Add List Carry (3)
sum of (list x and xs) (empty list) and carry bit 0 = list x and xs

Add List Carry (4)
sum of (list 0 and xs) (empty list) and carry bit 1 = list 1 and xs

Add List Carry (5)
sum of (list 1 and xs) (empty list) and carry bit 1 = list 0 and (sum of xs (empty list) and carry bit 1)

Add List Carry (6)
sum of (empty list) (list y and ys) and carry bit 0 = list y and ys

Add List Carry (7)
sum of (empty list) (list 0 and ys) and carry bit 1 = list 1 and ys

Add List Carry (8)
sum of (empty list) (list 1 and ys) and carry bit 1 = list 0 and (sum of (empty list) ys and carry bit 1)

Add List Carry (9)
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))

Add Unsigned Integer
sum of unsigned integers a and b = sum of a b and carry bit 0

Decrement Unsigned Integer
decrement (list 0 and (list 1 and (empty list))) by 1 = list 1 and (empty list)

Decrement Unsigned Integer (2)
decrement (list 0 and (list 1 and (list x and xs))) by 1 = list 1 and (list 0 and (list x and xs))

Decrement Unsigned Integer (3)
decrement (list 1 and xs) by 1 = list 0 and xs

Multiply x By 0
(list x and xs) multiplied by (list 0 and (empty list)) = list 0 and (empty list)

Multiply 0 By x
(list 0 and (empty list)) multiplied by (list y and ys) = list 0 and (empty list)

Multiply by 1
(list x and xs) multiplied by (list 1 and (empty list)) = list x and xs

Multiply Unsigned Integers
(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))

Add Bit Output Property
sum of bit x bit 0 and bit 0 = x

Add Bit Carry Property
carry on sum of bit x bit 0 and 0 = 0

Add List Carry Property
sum of x (empty list) and carry bit 0 = x

Pages: 2 3