Function list x and xs
a recursive list whose first element is x and the rest of the list is in xs
Format:
list x and xs
Input:
bit x -
list xs -
Output:
list - None
Properties that reference this function:
sum of (empty list) (empty list) and carry bit 1 = list 1 and (empty list) (Add List Carry (2))
sum of (list x and xs) (empty list) and carry bit 0 = list x and xs (Add List Carry (3))
sum of (list 0 and xs) (empty list) and carry bit 1 = list 1 and xs (Add List Carry (4))
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 (5))
sum of (empty list) (list y and ys) and carry bit 0 = list y and ys (Add List Carry (6))
sum of (empty list) (list 0 and ys) and carry bit 1 = list 1 and ys (Add List Carry (7))
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 (8))
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 List Carry (9))
decrement (list 0 and (list 1 and (empty list))) by 1 = list 1 and (empty list) (Decrement Unsigned Integer)
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 (2))
decrement (list 1 and xs) by 1 = list 0 and xs (Decrement Unsigned Integer (3))
(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)) (Multiply Unsigned Integers)
Comments
Please log in to add comments