(STRATEGY
    INNERMOST)

(VAR
    k m n psi s t u x xi y)
(DATATYPES
    A = µX.< Case(X, X, X), Sum_constant(X), Left, Right, Sum_term_var(X), Term_app(X, X), Term_pair(X, X), Term_inl(X), Term_inr(X), Term_var(X), Id, Cons_usual(X, X, X), Cons_sum(X, X, X) >)
(SIGNATURES
    Term_sub :: [A x A] -> A
    Frozen :: [A x A x A x A] -> A
    Sum_sub :: [A x A] -> A
    Concat :: [A x A] -> A)
(RULES
    Term_sub(Case(m,xi,n),s) ->
      Frozen(m,Sum_sub(xi,s),n,s)
    Frozen(m
          ,Sum_constant(Left())
          ,n
          ,s) -> Term_sub(m,s)
    Frozen(m
          ,Sum_constant(Right())
          ,n
          ,s) -> Term_sub(n,s)
    Frozen(m
          ,Sum_term_var(xi)
          ,n
          ,s) -> Case(Term_sub(m,s)
                     ,xi
                     ,Term_sub(n,s))
    Term_sub(Term_app(m,n),s) ->
      Term_app(Term_sub(m,s)
              ,Term_sub(n,s))
    Term_sub(Term_pair(m,n),s) ->
      Term_pair(Term_sub(m,s)
               ,Term_sub(n,s))
    Term_sub(Term_inl(m),s) ->
      Term_inl(Term_sub(m,s))
    Term_sub(Term_inr(m),s) ->
      Term_inr(Term_sub(m,s))
    Term_sub(Term_var(x),Id()) ->
      Term_var(x)
    Term_sub(Term_var(x)
            ,Cons_usual(y,m,s)) -> m
    Term_sub(Term_var(x)
            ,Cons_usual(y,m,s)) ->
      Term_sub(Term_var(x),s)
    Term_sub(Term_var(x)
            ,Cons_sum(xi,k,s)) ->
      Term_sub(Term_var(x),s)
    Term_sub(Term_sub(m,s),t) ->
      Term_sub(m,Concat(s,t))
    Sum_sub(xi,Id()) ->
      Sum_term_var(xi)
    Sum_sub(xi,Cons_sum(psi,k,s)) ->
      Sum_constant(k)
    Sum_sub(xi,Cons_sum(psi,k,s)) ->
      Sum_sub(xi,s)
    Sum_sub(xi,Cons_usual(y,m,s)) ->
      Sum_sub(xi,s)
    Concat(Concat(s,t),u) ->
      Concat(s,Concat(t,u))
    Concat(Cons_usual(x,m,s),t) ->
      Cons_usual(x
                ,Term_sub(m,t)
                ,Concat(s,t))
    Concat(Cons_sum(xi,k,s),t) ->
      Cons_sum(xi,k,Concat(s,t))
    Concat(Id(),s) -> s)