(GOAL COMPLEXITY) (STARTTERM CONSTRUCTOR-BASED) (STRATEGY INNERMOST) (STRATEGY INNERMOST) (VAR m n) (DATATYPES A = µX.< 0, ack_out(X), s(X) >) (SIGNATURES ack_in :: [A x A] -> A u11 :: [A] -> A u21 :: [A x A] -> A u22 :: [A] -> A) (RULES ack_in(0(),n) -> ack_out(s(n)) ack_in(s(m),0()) -> u11(ack_in(m ,s(0()))) u11(ack_out(n)) -> ack_out(n) ack_in(s(m),s(n)) -> u21(ack_in(s(m),n),m) u21(ack_out(n),m) -> u22(ack_in(m,n)) u22(ack_out(n)) -> ack_out(n))