(COMMENT from Gluck and Kawabe's paper)
(COMMENT
The function inc increments a given binary natural number. Numbers
are represented by (improper) lists of bits, from LSB to MSB, where
nil corresponds to 1. Since we only consider integer numbers greater
than 0, the last CDR of a list is always 1. For example, decimal 11
is 1011 in binary, and represented as (1 1 0 . 1). The result of
applying inc is (0 0 1 . 1).
)
(COMMENT
fun inc [] = [0]
| inc (0::xs) = 1 :: xs
| inc (1::xs) = 0 :: inc xs;
)
(VAR xs)
(RULES
inc(nil) -> cons(0,nil)
inc(cons(0,xs)) -> cons(1,xs)
inc(cons(1,xs)) -> cons(0,inc(xs))
)