EQUATIONS: plus(plus(x,y),z) = plus(x,plus(y,z)) plus(x,0()) = x times(times(x,y),z) = times(x,times(y,z)) times(x,1()) = x exp(0()) = 1() exp(plus(x,y)) = times(exp(x),exp(y)) COMPLETE TRS: RULES: plus(plus(x,y),z) -> plus(x,plus(y,z)) plus(x,0()) -> x times(times(x,y),z) -> times(x,times(y,z)) times(x,1()) -> x exp(0()) -> 1() times(exp(x),exp(y)) -> exp(plus(x,y)) plus(x,plus(0(),y)) -> plus(x,y) times(x,times(1(),y)) -> times(x,y) exp(plus(0(),x)) -> times(1(),exp(x)) times(exp(x),times(exp(y),z)) -> times(exp(plus(x,y)),z) SUCCESS MaxTRS: 2 Search time: 0.02 seconds