YES (VAR x y z u v) (RULES and(null(nil()),null(nil())) -> null(nil()) null(end(x,y)) -> false() true() -> null(nil()) .(end(x,y),z) -> .(x,f(y,z)) .(nil(),y) -> y f(x,end(y,z)) -> end(f(x,y),z) f(x,nil()) -> end(nil(),x) eq(end(x,y),end(u,v)) -> and(eq(y,v),eq(x,u)) eq(end(x,y),nil()) -> false() eq(nil(),end(y,z)) -> false() eq(x,x) -> null(nil()) ) (COMMENT Termination is shown by EKBO with interpretations on natural numbers eq_A(x1,x2) = 1 true_A = 0 nil_A = 2 end_A(x1,x2) = 1 false_A = 0 and_A(x1,x2) = x1 f_A(x1,x2) = x2 ._A(x1,x2) = x2 null_A(x1) = 0 eq#_A(x1,x2) = 0 true#_A = 0 nil#_A = 0 false#_A = 0 and#_A(x1,x2) = x1 + x2 f#_A(x1,x2) = 0 .#_A(x1,x2) = x2 weights w0 = 1 w(eq) = 3 w(true) = 3 w(nil) = 1 w(end) = 2 w(false) = 4 w(and) = 0 w(f) = 2 w(.) = 0 w(null) = 1 and precedence: eq > true > null > and > f > . > end > nil > false )