EQUATIONS: s(s(x)) = x f(0(),y) = y f(s(x),y) = s(f(x,y)) f(f(g(x,y),0()),0()) = g(x,y) g(0(),y) = y g(s(x),y) = f(g(x,y),0()) h(0()) = s(0()) COMPLETE TRS: RULES: f(0(),y) -> y g(0(),y) -> y f(f(x,0()),0()) -> x g(h(0()),x) -> f(x,0()) f(f(h(0()),x),y) -> f(h(0()),f(x,y)) g(f(h(0()),x),y) -> f(g(x,y),0()) s(x) -> f(h(0()),x) f(h(0()),h(0())) -> 0() f(h(0()),0()) -> h(0()) f(h(0()),f(h(0()),x)) -> x SUCCESS MaxTRS: 2 Search time: 0.16 seconds