YES (VAR x y z l l1 l2 l3) (RULES 0(#) -> # +(x,#) -> x +(#,x) -> x +(0(x),0(y)) -> 0(+(x,y)) +(0(x),1(y)) -> 1(+(x,y)) +(1(x),0(y)) -> 1(+(x,y)) +(1(x),1(y)) -> 0(+(+(x,y),1(#))) +(+(x,y),z) -> +(x,+(y,z)) -(#,x) -> # -(x,#) -> x -(0(x),0(y)) -> 0(-(x,y)) -(0(x),1(y)) -> 1(-(-(x,y),1(#))) -(1(x),0(y)) -> 1(-(x,y)) -(1(x),1(y)) -> 0(-(x,y)) not(true) -> false not(false) -> true if(true,x,y) -> x if(false,x,y) -> y eq(#,#) -> true eq(#,1(y)) -> false eq(1(x),#) -> false eq(#,0(y)) -> eq(#,y) eq(0(x),#) -> eq(x,#) eq(1(x),1(y)) -> eq(x,y) eq(0(x),1(y)) -> false eq(1(x),0(y)) -> false eq(0(x),0(y)) -> eq(x,y) ge(0(x),0(y)) -> ge(x,y) ge(0(x),1(y)) -> not(ge(y,x)) ge(1(x),0(y)) -> ge(x,y) ge(1(x),1(y)) -> ge(x,y) ge(x,#) -> true ge(#,0(x)) -> ge(#,x) ge(#,1(x)) -> false log(x) -> -(log'(x),1(#)) log'(#) -> # log'(1(x)) -> +(log'(x),1(#)) log'(0(x)) -> if(ge(x,1(#)),+(log'(x),1(#)),#) *(#,x) -> # *(0(x),y) -> 0(*(x,y)) *(1(x),y) -> +(0(*(x,y)),y) *(*(x,y),z) -> *(x,*(y,z)) *(x,+(y,z)) -> +(*(x,y),*(x,z)) app(nil,l) -> l app(cons(x,l1),l2) -> cons(x,app(l1,l2)) sum(nil) -> 0(#) sum(cons(x,l)) -> +(x,sum(l)) sum(app(l1,l2)) -> +(sum(l1),sum(l2)) prod(nil) -> 1(#) prod(cons(x,l)) -> *(x,prod(l)) prod(app(l1,l2)) -> *(prod(l1),prod(l2)) mem(x,nil) -> false mem(x,cons(y,l)) -> if(eq(x,y),true,mem(x,l)) inter(x,nil) -> nil inter(nil,x) -> nil inter(app(l1,l2),l3) -> app(inter(l1,l3),inter(l2,l3)) inter(l1,app(l2,l3)) -> app(inter(l1,l2),inter(l1,l3)) inter(cons(x,l1),l2) -> ifinter(mem(x,l2),x,l1,l2) inter(l1,cons(x,l2)) -> ifinter(mem(x,l1),x,l2,l1) ifinter(true,x,l1,l2) -> cons(x,inter(l1,l2)) ifinter(false,x,l1,l2) -> inter(l1,l2) ) Proving termination of rewriting for big: -> Dependency pairs: nF_+(0(x),0(y)) -> nF_0(+(x,y)) nF_+(0(x),0(y)) -> nF_+(x,y) nF_+(0(x),1(y)) -> nF_+(x,y) nF_+(1(x),0(y)) -> nF_+(x,y) nF_+(1(x),1(y)) -> nF_0(+(+(x,y),1(#))) nF_+(1(x),1(y)) -> nF_+(+(x,y),1(#)) nF_+(1(x),1(y)) -> nF_+(x,y) nF_+(+(x,y),z) -> nF_+(x,+(y,z)) nF_+(+(x,y),z) -> nF_+(y,z) nF_-(0(x),0(y)) -> nF_0(-(x,y)) nF_-(0(x),0(y)) -> nF_-(x,y) nF_-(0(x),1(y)) -> nF_-(-(x,y),1(#)) nF_-(0(x),1(y)) -> nF_-(x,y) nF_-(1(x),0(y)) -> nF_-(x,y) nF_-(1(x),1(y)) -> nF_0(-(x,y)) nF_-(1(x),1(y)) -> nF_-(x,y) nF_eq(#,0(y)) -> nF_eq(#,y) nF_eq(0(x),#) -> nF_eq(x,#) nF_eq(1(x),1(y)) -> nF_eq(x,y) nF_eq(0(x),0(y)) -> nF_eq(x,y) nF_ge(0(x),0(y)) -> nF_ge(x,y) nF_ge(0(x),1(y)) -> nF_not(ge(y,x)) nF_ge(0(x),1(y)) -> nF_ge(y,x) nF_ge(1(x),0(y)) -> nF_ge(x,y) nF_ge(1(x),1(y)) -> nF_ge(x,y) nF_ge(#,0(x)) -> nF_ge(#,x) nF_log(x) -> nF_-(log'(x),1(#)) nF_log(x) -> nF_log'(x) nF_log'(1(x)) -> nF_+(log'(x),1(#)) nF_log'(1(x)) -> nF_log'(x) nF_log'(0(x)) -> nF_if(ge(x,1(#)),+(log'(x),1(#)),#) nF_log'(0(x)) -> nF_ge(x,1(#)) nF_log'(0(x)) -> nF_+(log'(x),1(#)) nF_log'(0(x)) -> nF_log'(x) nF_*(0(x),y) -> nF_0(*(x,y)) nF_*(0(x),y) -> nF_*(x,y) nF_*(1(x),y) -> nF_+(0(*(x,y)),y) nF_*(1(x),y) -> nF_0(*(x,y)) nF_*(1(x),y) -> nF_*(x,y) nF_*(*(x,y),z) -> nF_*(x,*(y,z)) nF_*(*(x,y),z) -> nF_*(y,z) nF_*(x,+(y,z)) -> nF_+(*(x,y),*(x,z)) nF_*(x,+(y,z)) -> nF_*(x,y) nF_*(x,+(y,z)) -> nF_*(x,z) nF_app(cons(x,l1),l2) -> nF_app(l1,l2) nF_sum(nil) -> nF_0(#) nF_sum(cons(x,l)) -> nF_+(x,sum(l)) nF_sum(cons(x,l)) -> nF_sum(l) nF_sum(app(l1,l2)) -> nF_+(sum(l1),sum(l2)) nF_sum(app(l1,l2)) -> nF_sum(l1) nF_sum(app(l1,l2)) -> nF_sum(l2) nF_prod(cons(x,l)) -> nF_*(x,prod(l)) nF_prod(cons(x,l)) -> nF_prod(l) nF_prod(app(l1,l2)) -> nF_*(prod(l1),prod(l2)) nF_prod(app(l1,l2)) -> nF_prod(l1) nF_prod(app(l1,l2)) -> nF_prod(l2) nF_mem(x,cons(y,l)) -> nF_if(eq(x,y),true,mem(x,l)) nF_mem(x,cons(y,l)) -> nF_eq(x,y) nF_mem(x,cons(y,l)) -> nF_mem(x,l) nF_inter(app(l1,l2),l3) -> nF_app(inter(l1,l3),inter(l2,l3)) nF_inter(app(l1,l2),l3) -> nF_inter(l1,l3) nF_inter(app(l1,l2),l3) -> nF_inter(l2,l3) nF_inter(l1,app(l2,l3)) -> nF_app(inter(l1,l2),inter(l1,l3)) nF_inter(l1,app(l2,l3)) -> nF_inter(l1,l2) nF_inter(l1,app(l2,l3)) -> nF_inter(l1,l3) nF_inter(cons(x,l1),l2) -> nF_ifinter(mem(x,l2),x,l1,l2) nF_inter(cons(x,l1),l2) -> nF_mem(x,l2) nF_inter(l1,cons(x,l2)) -> nF_ifinter(mem(x,l1),x,l2,l1) nF_inter(l1,cons(x,l2)) -> nF_mem(x,l1) nF_ifinter(true,x,l1,l2) -> nF_inter(l1,l2) nF_ifinter(false,x,l1,l2) -> nF_inter(l1,l2) -> Proof of termination for big_1_1: -> -> Dependency pairs in cycle: nF_inter(app(l1,l2),l3) -> nF_inter(l1,l3) nF_ifinter(false,x,l1,l2) -> nF_inter(l1,l2) nF_inter(l1,cons(x,l2)) -> nF_ifinter(mem(x,l1),x,l2,l1) nF_ifinter(true,x,l1,l2) -> nF_inter(l1,l2) nF_inter(cons(x,l1),l2) -> nF_ifinter(mem(x,l2),x,l1,l2) nF_inter(l1,app(l2,l3)) -> nF_inter(l1,l3) nF_inter(l1,app(l2,l3)) -> nF_inter(l1,l2) nF_inter(app(l1,l2),l3) -> nF_inter(l2,l3) UsableRules: if(true,x,y) -> x if(false,x,y) -> y eq(#,#) -> true eq(#,1(y)) -> false eq(1(x),#) -> false eq(#,0(y)) -> eq(#,y) eq(0(x),#) -> eq(x,#) eq(1(x),1(y)) -> eq(x,y) eq(0(x),1(y)) -> false eq(1(x),0(y)) -> false eq(0(x),0(y)) -> eq(x,y) mem(x,nil) -> false mem(x,cons(y,l)) -> if(eq(x,y),true,mem(x,l)) Polynomial Interpretation: [0](X) = X + 1 [#] = 1 [+](X1,X2) = 0 [1](X) = X [-](X1,X2) = 0 [not](X) = 0 [true] = 0 [false] = 0 [if](X1,X2,X3) = X2 + X3 [eq](X1,X2) = X1 + X2 [ge](X1,X2) = 0 [log](X) = 0 [log'](X) = 0 [*](X1,X2) = 0 [app](X1,X2) = X1 + X2 + 1 [nil] = 1 [cons](X1,X2) = X2 [sum](X) = 0 [prod](X) = 0 [mem](X1,X2) = X1 + X2 [inter](X1,X2) = 0 [ifinter](X1,X2,X3,X4) = 0 [nF_inter](X1,X2) = X1 + X2 [nF_ifinter](X1,X2,X3,X4) = X3 + X4 TIME: 5.4785e-2 -> -> Dependency pairs in cycle: nF_inter(app(l1,l2),l3) -> nF_inter(l1,l3) nF_inter(l1,app(l2,l3)) -> nF_inter(l1,l2) nF_inter(l1,app(l2,l3)) -> nF_inter(l1,l3) nF_ifinter(true,x,l1,l2) -> nF_inter(l1,l2) nF_inter(cons(x,l1),l2) -> nF_ifinter(mem(x,l2),x,l1,l2) nF_ifinter(false,x,l1,l2) -> nF_inter(l1,l2) nF_inter(l1,cons(x,l2)) -> nF_ifinter(mem(x,l1),x,l2,l1) UsableRules: if(true,x,y) -> x if(false,x,y) -> y eq(#,#) -> true eq(#,1(y)) -> false eq(1(x),#) -> false eq(#,0(y)) -> eq(#,y) eq(0(x),#) -> eq(x,#) eq(1(x),1(y)) -> eq(x,y) eq(0(x),1(y)) -> false eq(1(x),0(y)) -> false eq(0(x),0(y)) -> eq(x,y) mem(x,nil) -> false mem(x,cons(y,l)) -> if(eq(x,y),true,mem(x,l)) Polynomial Interpretation: [0](X) = 0 [#] = 0 [+](X1,X2) = 0 [1](X) = 0 [-](X1,X2) = 0 [not](X) = 0 [true] = 0 [false] = 0 [if](X1,X2,X3) = X2 + X3 [eq](X1,X2) = 0 [ge](X1,X2) = 0 [log](X) = 0 [log'](X) = 0 [*](X1,X2) = 0 [app](X1,X2) = X1 + X2 [nil] = 1 [cons](X1,X2) = X2 + 1 [sum](X) = 0 [prod](X) = 0 [mem](X1,X2) = X1 + X2 [inter](X1,X2) = 0 [ifinter](X1,X2,X3,X4) = 0 [nF_inter](X1,X2) = X1 + X2 [nF_ifinter](X1,X2,X3,X4) = X3 + X4 TIME: 4.936e-2 -> -> Dependency pairs in cycle: nF_inter(app(l1,l2),l3) -> nF_inter(l1,l3) nF_ifinter(false,x,l1,l2) -> nF_inter(l1,l2) nF_inter(cons(x,l1),l2) -> nF_ifinter(mem(x,l2),x,l1,l2) nF_ifinter(true,x,l1,l2) -> nF_inter(l1,l2) nF_inter(l1,app(l2,l3)) -> nF_inter(l1,l3) nF_inter(l1,app(l2,l3)) -> nF_inter(l1,l2) Dependency pairs oriented using subterm criterion. -> -> Dependency pairs in cycle: nF_inter(l1,app(l2,l3)) -> nF_inter(l1,l2) nF_inter(l1,app(l2,l3)) -> nF_inter(l1,l3) Termination proved: Cycles verify subterm criterion. -> Proof of termination for big_1_2: -> -> Dependency pairs in cycle: nF_mem(x,cons(y,l)) -> nF_mem(x,l) Termination proved: Cycles verify subterm criterion. -> Proof of termination for big_1_3: -> -> Dependency pairs in cycle: nF_prod(cons(x,l)) -> nF_prod(l) nF_prod(app(l1,l2)) -> nF_prod(l2) nF_prod(app(l1,l2)) -> nF_prod(l1) Termination proved: Cycles verify subterm criterion. -> Proof of termination for big_1_4: -> -> Dependency pairs in cycle: nF_sum(cons(x,l)) -> nF_sum(l) nF_sum(app(l1,l2)) -> nF_sum(l2) nF_sum(app(l1,l2)) -> nF_sum(l1) Termination proved: Cycles verify subterm criterion. -> Proof of termination for big_1_5: -> -> Dependency pairs in cycle: nF_app(cons(x,l1),l2) -> nF_app(l1,l2) Termination proved: Cycles verify subterm criterion. -> Proof of termination for big_1_6: -> -> Dependency pairs in cycle: nF_*(0(x),y) -> nF_*(x,y) nF_*(x,+(y,z)) -> nF_*(x,z) nF_*(x,+(y,z)) -> nF_*(x,y) nF_*(*(x,y),z) -> nF_*(y,z) nF_*(*(x,y),z) -> nF_*(x,*(y,z)) nF_*(1(x),y) -> nF_*(x,y) Dependency pairs oriented using subterm criterion. -> -> Dependency pairs in cycle: nF_*(x,+(y,z)) -> nF_*(x,z) nF_*(x,+(y,z)) -> nF_*(x,y) Termination proved: Cycles verify subterm criterion. -> Proof of termination for big_1_7: -> -> Dependency pairs in cycle: nF_log'(0(x)) -> nF_log'(x) nF_log'(1(x)) -> nF_log'(x) Termination proved: Cycles verify subterm criterion. -> Proof of termination for big_1_8: -> -> Dependency pairs in cycle: nF_ge(0(x),0(y)) -> nF_ge(x,y) nF_ge(1(x),1(y)) -> nF_ge(x,y) nF_ge(1(x),0(y)) -> nF_ge(x,y) nF_ge(0(x),1(y)) -> nF_ge(y,x) There are no usable rules. Polynomial Interpretation: [0](X) = X [#] = 0 [+](X1,X2) = 0 [1](X) = X + 1 [-](X1,X2) = 0 [not](X) = 0 [true] = 0 [false] = 0 [if](X1,X2,X3) = 0 [eq](X1,X2) = 0 [ge](X1,X2) = 0 [log](X) = 0 [log'](X) = 0 [*](X1,X2) = 0 [app](X1,X2) = 0 [nil] = 0 [cons](X1,X2) = 0 [sum](X) = 0 [prod](X) = 0 [mem](X1,X2) = 0 [inter](X1,X2) = 0 [ifinter](X1,X2,X3,X4) = 0 [nF_ge](X1,X2) = X1 + X2 TIME: 4.1898e-2 -> -> Dependency pairs in cycle: nF_ge(0(x),0(y)) -> nF_ge(x,y) nF_ge(1(x),0(y)) -> nF_ge(x,y) nF_ge(1(x),1(y)) -> nF_ge(x,y) Termination proved: Cycles verify subterm criterion. -> Proof of termination for big_1_9: -> -> Dependency pairs in cycle: nF_ge(#,0(x)) -> nF_ge(#,x) Termination proved: Cycles verify subterm criterion. -> Proof of termination for big_1_10: -> -> Dependency pairs in cycle: nF_eq(1(x),1(y)) -> nF_eq(x,y) nF_eq(0(x),0(y)) -> nF_eq(x,y) Termination proved: Cycles verify subterm criterion. -> Proof of termination for big_1_11: -> -> Dependency pairs in cycle: nF_eq(0(x),#) -> nF_eq(x,#) Termination proved: Cycles verify subterm criterion. -> Proof of termination for big_1_12: -> -> Dependency pairs in cycle: nF_eq(#,0(y)) -> nF_eq(#,y) Termination proved: Cycles verify subterm criterion. -> Proof of termination for big_1_13: -> -> Dependency pairs in cycle: nF_-(0(x),0(y)) -> nF_-(x,y) nF_-(1(x),1(y)) -> nF_-(x,y) nF_-(1(x),0(y)) -> nF_-(x,y) nF_-(0(x),1(y)) -> nF_-(x,y) nF_-(0(x),1(y)) -> nF_-(-(x,y),1(#)) UsableRules: 0(#) -> # -(#,x) -> # -(x,#) -> x -(0(x),0(y)) -> 0(-(x,y)) -(0(x),1(y)) -> 1(-(-(x,y),1(#))) -(1(x),0(y)) -> 1(-(x,y)) -(1(x),1(y)) -> 0(-(x,y)) Polynomial Interpretation: [0](X) = X + 1 [#] = 1 [+](X1,X2) = 0 [1](X) = X + 1 [-](X1,X2) = X1 [not](X) = 0 [true] = 0 [false] = 0 [if](X1,X2,X3) = 0 [eq](X1,X2) = 0 [ge](X1,X2) = 0 [log](X) = 0 [log'](X) = 0 [*](X1,X2) = 0 [app](X1,X2) = 0 [nil] = 0 [cons](X1,X2) = 0 [sum](X) = 0 [prod](X) = 0 [mem](X1,X2) = 0 [inter](X1,X2) = 0 [ifinter](X1,X2,X3,X4) = 0 [nF_-](X1,X2) = X1 TIME: 4.8424e-2 -> -> Dependency pairs in cycle: nF_-(0(x),0(y)) -> nF_-(x,y) nF_-(0(x),1(y)) -> nF_-(x,y) nF_-(1(x),0(y)) -> nF_-(x,y) nF_-(1(x),1(y)) -> nF_-(x,y) Termination proved: Cycles verify subterm criterion. -> Proof of termination for big_1_14: -> -> Dependency pairs in cycle: nF_+(0(x),0(y)) -> nF_+(x,y) nF_+(+(x,y),z) -> nF_+(y,z) nF_+(+(x,y),z) -> nF_+(x,+(y,z)) nF_+(1(x),1(y)) -> nF_+(x,y) nF_+(1(x),1(y)) -> nF_+(+(x,y),1(#)) nF_+(1(x),0(y)) -> nF_+(x,y) nF_+(0(x),1(y)) -> nF_+(x,y) UsableRules: 0(#) -> # +(x,#) -> x +(#,x) -> x +(0(x),0(y)) -> 0(+(x,y)) +(0(x),1(y)) -> 1(+(x,y)) +(1(x),0(y)) -> 1(+(x,y)) +(1(x),1(y)) -> 0(+(+(x,y),1(#))) +(+(x,y),z) -> +(x,+(y,z)) Polynomial Interpretation: [0](X) = X [#] = 0 [+](X1,X2) = X1 + X2 [1](X) = X + 1 [-](X1,X2) = 0 [not](X) = 0 [true] = 0 [false] = 0 [if](X1,X2,X3) = 0 [eq](X1,X2) = 0 [ge](X1,X2) = 0 [log](X) = 0 [log'](X) = 0 [*](X1,X2) = 0 [app](X1,X2) = 0 [nil] = 0 [cons](X1,X2) = 0 [sum](X) = 0 [prod](X) = 0 [mem](X1,X2) = 0 [inter](X1,X2) = 0 [ifinter](X1,X2,X3,X4) = 0 [nF_+](X1,X2) = X1 + X2 TIME: 4.6676e-2 -> -> Dependency pairs in cycle: nF_+(0(x),0(y)) -> nF_+(x,y) nF_+(1(x),0(y)) -> nF_+(x,y) nF_+(1(x),1(y)) -> nF_+(x,y) nF_+(1(x),1(y)) -> nF_+(+(x,y),1(#)) nF_+(+(x,y),z) -> nF_+(x,+(y,z)) nF_+(+(x,y),z) -> nF_+(y,z) UsableRules: 0(#) -> # +(x,#) -> x +(#,x) -> x +(0(x),0(y)) -> 0(+(x,y)) +(0(x),1(y)) -> 1(+(x,y)) +(1(x),0(y)) -> 1(+(x,y)) +(1(x),1(y)) -> 0(+(+(x,y),1(#))) +(+(x,y),z) -> +(x,+(y,z)) Polynomial Interpretation: [0](X) = X [#] = 0 [+](X1,X2) = X1 + X2 + 1 [1](X) = X + 1 [-](X1,X2) = 0 [not](X) = 0 [true] = 0 [false] = 0 [if](X1,X2,X3) = 0 [eq](X1,X2) = 0 [ge](X1,X2) = 0 [log](X) = 0 [log'](X) = 0 [*](X1,X2) = 0 [app](X1,X2) = 0 [nil] = 0 [cons](X1,X2) = 0 [sum](X) = 0 [prod](X) = 0 [mem](X1,X2) = 0 [inter](X1,X2) = 0 [ifinter](X1,X2,X3,X4) = 0 [nF_+](X1,X2) = X1 + X2 TIME: 4.9646e-2 -> -> Dependency pairs in cycle: nF_+(0(x),0(y)) -> nF_+(x,y) nF_+(+(x,y),z) -> nF_+(x,+(y,z)) nF_+(1(x),1(y)) -> nF_+(+(x,y),1(#)) nF_+(1(x),1(y)) -> nF_+(x,y) nF_+(1(x),0(y)) -> nF_+(x,y) UsableRules: 0(#) -> # +(x,#) -> x +(#,x) -> x +(0(x),0(y)) -> 0(+(x,y)) +(0(x),1(y)) -> 1(+(x,y)) +(1(x),0(y)) -> 1(+(x,y)) +(1(x),1(y)) -> 0(+(+(x,y),1(#))) +(+(x,y),z) -> +(x,+(y,z)) Polynomial Interpretation: [0](X) = X + 1 [#] = 0 [+](X1,X2) = X1 + X2 [1](X) = X + 1 [-](X1,X2) = 0 [not](X) = 0 [true] = 0 [false] = 0 [if](X1,X2,X3) = 0 [eq](X1,X2) = 0 [ge](X1,X2) = 0 [log](X) = 0 [log'](X) = 0 [*](X1,X2) = 0 [app](X1,X2) = 0 [nil] = 0 [cons](X1,X2) = 0 [sum](X) = 0 [prod](X) = 0 [mem](X1,X2) = 0 [inter](X1,X2) = 0 [ifinter](X1,X2,X3,X4) = 0 [nF_+](X1,X2) = X1 + X2 TIME: 4.82e-2 -> -> Dependency pairs in cycle: nF_+(0(x),0(y)) -> nF_+(x,y) nF_+(1(x),1(y)) -> nF_+(x,y) nF_+(1(x),1(y)) -> nF_+(+(x,y),1(#)) nF_+(+(x,y),z) -> nF_+(x,+(y,z)) UsableRules: 0(#) -> # +(x,#) -> x +(#,x) -> x +(0(x),0(y)) -> 0(+(x,y)) +(0(x),1(y)) -> 1(+(x,y)) +(1(x),0(y)) -> 1(+(x,y)) +(1(x),1(y)) -> 0(+(+(x,y),1(#))) +(+(x,y),z) -> +(x,+(y,z)) Polynomial Interpretation: [0](X) = X [#] = 0 [+](X1,X2) = X1 + X2 [1](X) = X + 1 [-](X1,X2) = 0 [not](X) = 0 [true] = 0 [false] = 0 [if](X1,X2,X3) = 0 [eq](X1,X2) = 0 [ge](X1,X2) = 0 [log](X) = 0 [log'](X) = 0 [*](X1,X2) = 0 [app](X1,X2) = 0 [nil] = 0 [cons](X1,X2) = 0 [sum](X) = 0 [prod](X) = 0 [mem](X1,X2) = 0 [inter](X1,X2) = 0 [ifinter](X1,X2,X3,X4) = 0 [nF_+](X1,X2) = X1 + X2 TIME: 5.8640000000000025e-2 -> -> Dependency pairs in cycle: nF_+(0(x),0(y)) -> nF_+(x,y) nF_+(+(x,y),z) -> nF_+(x,+(y,z)) nF_+(1(x),1(y)) -> nF_+(x,y) Termination proved: Cycles verify subterm criterion. SETTINGS: Base ordering: Polynomial ordering Proof mode: SCCs in DG + base ordering Upper bound for coeffs: 1 Rationals below 1 for all non-replacing args: No Polynomial interpretation: Linear Coeffs in polynomials: No rationals Delta: automatic Termination was proved succesfully.