(STRATEGY
    INNERMOST)

(VAR
    x y)
(DATATYPES
    A = µX.< s(X), 0, false, nil, true, cons(X, X), entry(X, X, X) >)
(SIGNATURES
    table :: [] -> A
    gen :: [A] -> A
    if1 :: [A x A] -> A
    if2 :: [A x A] -> A
    if3 :: [A x A x A] -> A
    le :: [A x A] -> A
    plus :: [A x A] -> A
    times :: [A x A] -> A
    10 :: [] -> A)
(RULES
    table() -> gen(s(0()))
    gen(x) -> if1(le(x,10()),x)
    if1(false(),x) -> nil()
    if1(true(),x) -> if2(x,x)
    if2(x,y) -> if3(le(y,10()),x,y)
    if3(true(),x,y) -> cons(entry(x
                                 ,y
                                 ,times(x,y))
                           ,if2(x,s(y)))
    if3(false(),x,y) -> gen(s(x))
    le(0(),y) -> true()
    le(s(x),0()) -> false()
    le(s(x),s(y)) -> le(x,y)
    plus(0(),y) -> y
    plus(s(x),y) -> s(plus(x,y))
    times(0(),y) -> 0()
    times(s(x),y) -> plus(y
                         ,times(x,y))
    10() ->
      s(s(s(s(s(s(s(s(s(s(0())))))))))))