YES (VAR x1 x0 x y z) (RULES i2(f(x1,x0)) -> f(i2(x0),i2(x1)) i1(x0) -> f(i2(x0),a1()) i2(i2(i2(x0))) -> i2(x0) f(i2(i2(x0)),x1) -> f(x0,x1) f(i2(x0),f(x0,x1)) -> x1 f(x0,i2(a1())) -> i2(i2(x0)) f(x,i2(x)) -> i2(a1()) f(x1,f(i2(x1),x0)) -> x0 f(i2(a1()),y) -> y i2(i2(a1())) -> i2(a1()) a2() -> i2(a1()) f(a1(),y) -> y f(f(x,y),z) -> f(x,f(y,z)) ) (COMMENT Termination is shown by KBO with weight w0 = 1 w(f) = 0 w(a1) = 1 w(a2) = 3 w(i1) = 4 w(i2) = 0 and precedence: i2 > i1 > f > a1 > a2 )