(STRATEGY
    INNERMOST)

(VAR
    X X1 X2 Y)
(DATATYPES
    A = µX.< n__s(X), n__0, n__prod(X, X), n__fact(X), n__p(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
    0 :: [] -> A
    activate :: [A] -> A)
(RULES
    fact(X) -> if(zero(X)
                 ,n__s(n__0())
                 ,n__prod(X,n__fact(n__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)
    0() -> n__0()
    prod(X1,X2) -> n__prod(X1,X2)
    fact(X) -> n__fact(X)
    p(X) -> n__p(X)
    activate(n__s(X)) ->
      s(activate(X))
    activate(n__0()) -> 0()
    activate(n__prod(X1,X2)) ->
      prod(activate(X1),activate(X2))
    activate(n__fact(X)) ->
      fact(activate(X))
    activate(n__p(X)) ->
      p(activate(X))
    activate(X) -> X)