YES (VAR x y z l l1 l2) (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) -> # *(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)) ) Proving termination of rewriting for list_sum_prod_bin_assoc_distr_app: -> 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),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) -> Proof of termination for list_sum_prod_bin_assoc_distr_app_1_1: -> -> 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 list_sum_prod_bin_assoc_distr_app_1_2: -> -> 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 list_sum_prod_bin_assoc_distr_app_1_3: -> -> Dependency pairs in cycle: nF_app(cons(x,l1),l2) -> nF_app(l1,l2) Termination proved: Cycles verify subterm criterion. -> Proof of termination for list_sum_prod_bin_assoc_distr_app_1_4: -> -> 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 list_sum_prod_bin_assoc_distr_app_1_5: -> -> 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 [app](X1,X2) = 0 [nil] = 0 [cons](X1,X2) = 0 [sum](X) = 0 [prod](X) = 0 [nF_+](X1,X2) = X1 + X2 TIME: 0.138197 -> -> 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 [app](X1,X2) = 0 [nil] = 0 [cons](X1,X2) = 0 [sum](X) = 0 [prod](X) = 0 [nF_+](X1,X2) = X1 + X2 TIME: 5.0568e-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 [app](X1,X2) = 0 [nil] = 0 [cons](X1,X2) = 0 [sum](X) = 0 [prod](X) = 0 [nF_+](X1,X2) = X1 + X2 TIME: 4.9233e-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 [app](X1,X2) = 0 [nil] = 0 [cons](X1,X2) = 0 [sum](X) = 0 [prod](X) = 0 [nF_+](X1,X2) = X1 + X2 TIME: 7.1575e-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.