YES (VAR x y z) (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)) +(0(x),j(y)) -> j(+(x,y)) +(j(x),0(y)) -> j(+(x,y)) +(1(x),1(y)) -> j(+(+(x,y),1(#))) +(j(x),j(y)) -> 1(+(+(x,y),j(#))) +(1(x),j(y)) -> 0(+(x,y)) +(j(x),1(y)) -> 0(+(x,y)) +(+(x,y),z) -> +(x,+(y,z)) opp(#) -> # opp(0(x)) -> 0(opp(x)) opp(1(x)) -> j(opp(x)) opp(j(x)) -> 1(opp(x)) -(x,y) -> +(x,opp(y)) *(#,x) -> # *(0(x),y) -> 0(*(x,y)) *(1(x),y) -> +(0(*(x,y)),y) *(j(x),y) -> -(0(*(x,y)),y) *(*(x,y),z) -> *(x,*(y,z)) *(+(x,y),z) -> +(*(x,z),*(y,z)) *(x,+(y,z)) -> +(*(x,y),*(x,z)) ) Proving termination of rewriting for ternary_hard: -> 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_+(0(x),j(y)) -> nF_+(x,y) nF_+(j(x),0(y)) -> nF_+(x,y) nF_+(1(x),1(y)) -> nF_+(+(x,y),1(#)) nF_+(1(x),1(y)) -> nF_+(x,y) nF_+(j(x),j(y)) -> nF_+(+(x,y),j(#)) nF_+(j(x),j(y)) -> nF_+(x,y) nF_+(1(x),j(y)) -> nF_0(+(x,y)) nF_+(1(x),j(y)) -> nF_+(x,y) nF_+(j(x),1(y)) -> nF_0(+(x,y)) nF_+(j(x),1(y)) -> nF_+(x,y) nF_+(+(x,y),z) -> nF_+(x,+(y,z)) nF_+(+(x,y),z) -> nF_+(y,z) nF_opp(0(x)) -> nF_0(opp(x)) nF_opp(0(x)) -> nF_opp(x) nF_opp(1(x)) -> nF_opp(x) nF_opp(j(x)) -> nF_opp(x) nF_-(x,y) -> nF_+(x,opp(y)) nF_-(x,y) -> nF_opp(y) 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_*(j(x),y) -> nF_-(0(*(x,y)),y) nF_*(j(x),y) -> nF_0(*(x,y)) nF_*(j(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,z),*(y,z)) nF_*(+(x,y),z) -> nF_*(x,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) -> Proof of termination for ternary_hard_1_1: -> -> 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,z) nF_*(*(x,y),z) -> nF_*(y,z) nF_*(*(x,y),z) -> nF_*(x,*(y,z)) nF_*(j(x),y) -> nF_*(x,y) 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 ternary_hard_1_2: -> -> Dependency pairs in cycle: nF_opp(0(x)) -> nF_opp(x) nF_opp(j(x)) -> nF_opp(x) nF_opp(1(x)) -> nF_opp(x) Termination proved: Cycles verify subterm criterion. -> Proof of termination for ternary_hard_1_3: -> -> 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_+(j(x),1(y)) -> nF_+(x,y) nF_+(1(x),j(y)) -> nF_+(x,y) nF_+(j(x),j(y)) -> nF_+(x,y) nF_+(j(x),j(y)) -> nF_+(+(x,y),j(#)) nF_+(1(x),1(y)) -> nF_+(x,y) nF_+(1(x),1(y)) -> nF_+(+(x,y),1(#)) nF_+(j(x),0(y)) -> nF_+(x,y) nF_+(0(x),j(y)) -> nF_+(x,y) 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)) +(0(x),j(y)) -> j(+(x,y)) +(j(x),0(y)) -> j(+(x,y)) +(1(x),1(y)) -> j(+(+(x,y),1(#))) +(j(x),j(y)) -> 1(+(+(x,y),j(#))) +(1(x),j(y)) -> 0(+(x,y)) +(j(x),1(y)) -> 0(+(x,y)) +(+(x,y),z) -> +(x,+(y,z)) Polynomial Interpretation: [0](X) = X [#] = 0 [+](X1,X2) = X1 + X2 [1](X) = X + 1 [j](X) = X + 1 [opp](X) = 0 [-](X1,X2) = 0 [*](X1,X2) = 0 [nF_+](X1,X2) = X1 + X2 TIME: 6.5532e-2 -> -> Dependency pairs in cycle: nF_+(0(x),0(y)) -> nF_+(x,y) nF_+(1(x),0(y)) -> nF_+(x,y) nF_+(0(x),j(y)) -> nF_+(x,y) nF_+(j(x),0(y)) -> nF_+(x,y) nF_+(1(x),1(y)) -> nF_+(x,y) nF_+(1(x),1(y)) -> nF_+(+(x,y),1(#)) nF_+(j(x),j(y)) -> nF_+(x,y) nF_+(j(x),j(y)) -> nF_+(+(x,y),j(#)) nF_+(1(x),j(y)) -> nF_+(x,y) nF_+(j(x),1(y)) -> nF_+(x,y) 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)) +(0(x),j(y)) -> j(+(x,y)) +(j(x),0(y)) -> j(+(x,y)) +(1(x),1(y)) -> j(+(+(x,y),1(#))) +(j(x),j(y)) -> 1(+(+(x,y),j(#))) +(1(x),j(y)) -> 0(+(x,y)) +(j(x),1(y)) -> 0(+(x,y)) +(+(x,y),z) -> +(x,+(y,z)) Polynomial Interpretation: [0](X) = X [#] = 0 [+](X1,X2) = X1 + X2 [1](X) = X + 1 [j](X) = X + 1 [opp](X) = 0 [-](X1,X2) = 0 [*](X1,X2) = 0 [nF_+](X1,X2) = X1 + X2 TIME: 6.543e-2 -> -> 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),j(y)) -> nF_+(x,y) nF_+(j(x),j(y)) -> nF_+(+(x,y),j(#)) nF_+(j(x),j(y)) -> nF_+(x,y) nF_+(1(x),1(y)) -> nF_+(x,y) nF_+(1(x),1(y)) -> nF_+(+(x,y),1(#)) nF_+(j(x),0(y)) -> nF_+(x,y) nF_+(0(x),j(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)) +(0(x),j(y)) -> j(+(x,y)) +(j(x),0(y)) -> j(+(x,y)) +(1(x),1(y)) -> j(+(+(x,y),1(#))) +(j(x),j(y)) -> 1(+(+(x,y),j(#))) +(1(x),j(y)) -> 0(+(x,y)) +(j(x),1(y)) -> 0(+(x,y)) +(+(x,y),z) -> +(x,+(y,z)) Polynomial Interpretation: [0](X) = X + 1 [#] = 0 [+](X1,X2) = X1 + X2 [1](X) = X + 1 [j](X) = X + 1 [opp](X) = 0 [-](X1,X2) = 0 [*](X1,X2) = 0 [nF_+](X1,X2) = X1 + X2 TIME: 6.0816e-2 -> -> Dependency pairs in cycle: nF_+(0(x),0(y)) -> nF_+(x,y) nF_+(0(x),j(y)) -> nF_+(x,y) nF_+(j(x),0(y)) -> nF_+(x,y) nF_+(1(x),1(y)) -> nF_+(x,y) nF_+(1(x),1(y)) -> nF_+(+(x,y),1(#)) nF_+(j(x),j(y)) -> nF_+(x,y) nF_+(j(x),j(y)) -> nF_+(+(x,y),j(#)) nF_+(1(x),j(y)) -> nF_+(x,y) 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)) +(0(x),j(y)) -> j(+(x,y)) +(j(x),0(y)) -> j(+(x,y)) +(1(x),1(y)) -> j(+(+(x,y),1(#))) +(j(x),j(y)) -> 1(+(+(x,y),j(#))) +(1(x),j(y)) -> 0(+(x,y)) +(j(x),1(y)) -> 0(+(x,y)) +(+(x,y),z) -> +(x,+(y,z)) Polynomial Interpretation: [0](X) = X [#] = 0 [+](X1,X2) = X1 + X2 [1](X) = X + 1 [j](X) = X + 1 [opp](X) = 0 [-](X1,X2) = 0 [*](X1,X2) = 0 [nF_+](X1,X2) = X1 + X2 TIME: 6.2862e-2 -> -> 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_+(j(x),j(y)) -> nF_+(+(x,y),j(#)) nF_+(j(x),j(y)) -> nF_+(x,y) nF_+(1(x),1(y)) -> nF_+(x,y) nF_+(1(x),1(y)) -> nF_+(+(x,y),1(#)) nF_+(j(x),0(y)) -> nF_+(x,y) nF_+(0(x),j(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)) +(0(x),j(y)) -> j(+(x,y)) +(j(x),0(y)) -> j(+(x,y)) +(1(x),1(y)) -> j(+(+(x,y),1(#))) +(j(x),j(y)) -> 1(+(+(x,y),j(#))) +(1(x),j(y)) -> 0(+(x,y)) +(j(x),1(y)) -> 0(+(x,y)) +(+(x,y),z) -> +(x,+(y,z)) Polynomial Interpretation: [0](X) = X [#] = 0 [+](X1,X2) = X1 + X2 [1](X) = X + 1 [j](X) = X + 1 [opp](X) = 0 [-](X1,X2) = 0 [*](X1,X2) = 0 [nF_+](X1,X2) = X1 + X2 TIME: 6.1664e-2 -> -> Dependency pairs in cycle: nF_+(0(x),0(y)) -> nF_+(x,y) nF_+(j(x),0(y)) -> nF_+(x,y) nF_+(1(x),1(y)) -> nF_+(x,y) nF_+(1(x),1(y)) -> nF_+(+(x,y),1(#)) nF_+(j(x),j(y)) -> nF_+(x,y) nF_+(j(x),j(y)) -> nF_+(+(x,y),j(#)) 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)) +(0(x),j(y)) -> j(+(x,y)) +(j(x),0(y)) -> j(+(x,y)) +(1(x),1(y)) -> j(+(+(x,y),1(#))) +(j(x),j(y)) -> 1(+(+(x,y),j(#))) +(1(x),j(y)) -> 0(+(x,y)) +(j(x),1(y)) -> 0(+(x,y)) +(+(x,y),z) -> +(x,+(y,z)) Polynomial Interpretation: [0](X) = X [#] = 0 [+](X1,X2) = X1 + X2 [1](X) = X + 1 [j](X) = X + 1 [opp](X) = 0 [-](X1,X2) = 0 [*](X1,X2) = 0 [nF_+](X1,X2) = X1 + X2 TIME: 6.001e-2 -> -> 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_+(j(x),j(y)) -> nF_+(x,y) nF_+(1(x),1(y)) -> nF_+(x,y) nF_+(1(x),1(y)) -> nF_+(+(x,y),1(#)) nF_+(j(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)) +(0(x),j(y)) -> j(+(x,y)) +(j(x),0(y)) -> j(+(x,y)) +(1(x),1(y)) -> j(+(+(x,y),1(#))) +(j(x),j(y)) -> 1(+(+(x,y),j(#))) +(1(x),j(y)) -> 0(+(x,y)) +(j(x),1(y)) -> 0(+(x,y)) +(+(x,y),z) -> +(x,+(y,z)) Polynomial Interpretation: [0](X) = X + 1 [#] = 0 [+](X1,X2) = X1 + X2 [1](X) = X + 1 [j](X) = X + 1 [opp](X) = 0 [-](X1,X2) = 0 [*](X1,X2) = 0 [nF_+](X1,X2) = X1 + X2 TIME: 6.3517e-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_+(j(x),j(y)) -> nF_+(x,y) 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)) +(0(x),j(y)) -> j(+(x,y)) +(j(x),0(y)) -> j(+(x,y)) +(1(x),1(y)) -> j(+(+(x,y),1(#))) +(j(x),j(y)) -> 1(+(+(x,y),j(#))) +(1(x),j(y)) -> 0(+(x,y)) +(j(x),1(y)) -> 0(+(x,y)) +(+(x,y),z) -> +(x,+(y,z)) Polynomial Interpretation: [0](X) = X [#] = 0 [+](X1,X2) = X1 + X2 [1](X) = X + 1 [j](X) = X + 1 [opp](X) = 0 [-](X1,X2) = 0 [*](X1,X2) = 0 [nF_+](X1,X2) = X1 + X2 TIME: 6.9025e-2 -> -> 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),1(#)) nF_+(1(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)) +(0(x),j(y)) -> j(+(x,y)) +(j(x),0(y)) -> j(+(x,y)) +(1(x),1(y)) -> j(+(+(x,y),1(#))) +(j(x),j(y)) -> 1(+(+(x,y),j(#))) +(1(x),j(y)) -> 0(+(x,y)) +(j(x),1(y)) -> 0(+(x,y)) +(+(x,y),z) -> +(x,+(y,z)) Polynomial Interpretation: [0](X) = X [#] = 0 [+](X1,X2) = X1 + X2 [1](X) = X + 1 [j](X) = X + 1 [opp](X) = 0 [-](X1,X2) = 0 [*](X1,X2) = 0 [nF_+](X1,X2) = X1 + X2 TIME: 6.5622e-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_+(+(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)) +(0(x),j(y)) -> j(+(x,y)) +(j(x),0(y)) -> j(+(x,y)) +(1(x),1(y)) -> j(+(+(x,y),1(#))) +(j(x),j(y)) -> 1(+(+(x,y),j(#))) +(1(x),j(y)) -> 0(+(x,y)) +(j(x),1(y)) -> 0(+(x,y)) +(+(x,y),z) -> +(x,+(y,z)) Polynomial Interpretation: [0](X) = X [#] = 0 [+](X1,X2) = X1 + X2 [1](X) = X + 1 [j](X) = X + 1 [opp](X) = 0 [-](X1,X2) = 0 [*](X1,X2) = 0 [nF_+](X1,X2) = X1 + X2 TIME: 6.8554e-2 -> -> 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)) 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.