(STRATEGY
    INNERMOST)

(VAR
    X X1 X2 Y)
(DATATYPES
    A = µX.< n__s(X), 0, n__prod(X, X), true, false >)
(SIGNATURES
    fact :: [A] -> A
    add :: [A x A] -> A
    prod :: [A x A] -> A
    if :: [A x A x A] -> A
    zero :: [A] -> A
    p :: [A] -> A
    s :: [A] -> A
    activate :: [A] -> A)
(RULES
    fact(X) -> if(zero(X)
                 ,n__s(0())
                 ,n__prod(X,fact(p(X))))
    add(0(),X) -> X
    add(s(X),Y) -> s(add(X,Y))
    prod(0(),X) -> 0()
    prod(s(X),Y) -> add(Y,prod(X,Y))
    if(true(),X,Y) -> activate(X)
    if(false(),X,Y) -> activate(Y)
    zero(0()) -> true()
    zero(s(X)) -> false()
    p(s(X)) -> X
    s(X) -> n__s(X)
    prod(X1,X2) -> n__prod(X1,X2)
    activate(n__s(X)) -> s(X)
    activate(n__prod(X1,X2)) ->
      prod(X1,X2)
    activate(X) -> X)