YES (VAR X N M X1 X2) (RULES a__and(tt,X) -> mark(X) a__plus(N,0) -> mark(N) a__plus(N,s(M)) -> s(a__plus(mark(N),mark(M))) mark(and(X1,X2)) -> a__and(mark(X1),X2) mark(plus(X1,X2)) -> a__plus(mark(X1),mark(X2)) mark(tt) -> tt mark(0) -> 0 mark(s(X)) -> s(mark(X)) a__and(X1,X2) -> and(X1,X2) a__plus(X1,X2) -> plus(X1,X2) ) Proving termination of rewriting for PEANO_nosorts_GM: -> Dependency pairs: nF_a__and(tt,X) -> nF_mark(X) nF_a__plus(N,0) -> nF_mark(N) nF_a__plus(N,s(M)) -> nF_a__plus(mark(N),mark(M)) nF_a__plus(N,s(M)) -> nF_mark(N) nF_a__plus(N,s(M)) -> nF_mark(M) nF_mark(and(X1,X2)) -> nF_a__and(mark(X1),X2) nF_mark(and(X1,X2)) -> nF_mark(X1) nF_mark(plus(X1,X2)) -> nF_a__plus(mark(X1),mark(X2)) nF_mark(plus(X1,X2)) -> nF_mark(X1) nF_mark(plus(X1,X2)) -> nF_mark(X2) nF_mark(s(X)) -> nF_mark(X) -> Proof of termination for PEANO_nosorts_GM_1: -> -> Dependency pairs in cycle: nF_a__and(tt,X) -> nF_mark(X) nF_mark(and(X1,X2)) -> nF_a__and(mark(X1),X2) nF_mark(s(X)) -> nF_mark(X) nF_mark(plus(X1,X2)) -> nF_mark(X2) nF_mark(plus(X1,X2)) -> nF_mark(X1) nF_mark(and(X1,X2)) -> nF_mark(X1) nF_a__plus(N,s(M)) -> nF_mark(M) nF_mark(plus(X1,X2)) -> nF_a__plus(mark(X1),mark(X2)) nF_a__plus(N,s(M)) -> nF_mark(N) nF_a__plus(N,s(M)) -> nF_a__plus(mark(N),mark(M)) nF_a__plus(N,0) -> nF_mark(N) UsableRules: a__and(tt,X) -> mark(X) a__plus(N,0) -> mark(N) a__plus(N,s(M)) -> s(a__plus(mark(N),mark(M))) mark(and(X1,X2)) -> a__and(mark(X1),X2) mark(plus(X1,X2)) -> a__plus(mark(X1),mark(X2)) mark(tt) -> tt mark(0) -> 0 mark(s(X)) -> s(mark(X)) a__and(X1,X2) -> and(X1,X2) a__plus(X1,X2) -> plus(X1,X2) Polynomial Interpretation: [a__and](X1,X2) = X1 + X2 [tt] = 0 [mark](X) = X [a__plus](X1,X2) = X1 + X2 + 1 [0] = 0 [s](X) = X + 1 [and](X1,X2) = X1 + X2 [plus](X1,X2) = X1 + X2 + 1 [nF_a__and](X1,X2) = X2 [nF_mark](X) = X [nF_a__plus](X1,X2) = X1 + X2 + 1 TIME: 8.7403e-2 -> -> Dependency pairs in cycle: nF_a__and(tt,X) -> nF_mark(X) nF_mark(and(X1,X2)) -> nF_a__and(mark(X1),X2) nF_a__plus(N,s(M)) -> nF_mark(N) nF_a__plus(N,s(M)) -> nF_a__plus(mark(N),mark(M)) nF_mark(plus(X1,X2)) -> nF_a__plus(mark(X1),mark(X2)) nF_a__plus(N,s(M)) -> nF_mark(M) nF_mark(and(X1,X2)) -> nF_mark(X1) nF_mark(plus(X1,X2)) -> nF_mark(X1) nF_mark(plus(X1,X2)) -> nF_mark(X2) nF_mark(s(X)) -> nF_mark(X) UsableRules: a__and(tt,X) -> mark(X) a__plus(N,0) -> mark(N) a__plus(N,s(M)) -> s(a__plus(mark(N),mark(M))) mark(and(X1,X2)) -> a__and(mark(X1),X2) mark(plus(X1,X2)) -> a__plus(mark(X1),mark(X2)) mark(tt) -> tt mark(0) -> 0 mark(s(X)) -> s(mark(X)) a__and(X1,X2) -> and(X1,X2) a__plus(X1,X2) -> plus(X1,X2) Polynomial Interpretation: [a__and](X1,X2) = X1 + X2 [tt] = 1 [mark](X) = X [a__plus](X1,X2) = X1 + X2 [0] = 1 [s](X) = X + 1 [and](X1,X2) = X1 + X2 [plus](X1,X2) = X1 + X2 [nF_a__and](X1,X2) = X2 [nF_mark](X) = X [nF_a__plus](X1,X2) = X1 + X2 TIME: 8.3597e-2 -> -> Dependency pairs in cycle: nF_a__and(tt,X) -> nF_mark(X) nF_mark(and(X1,X2)) -> nF_a__and(mark(X1),X2) nF_mark(plus(X1,X2)) -> nF_mark(X2) nF_mark(plus(X1,X2)) -> nF_mark(X1) nF_mark(and(X1,X2)) -> nF_mark(X1) nF_a__plus(N,s(M)) -> nF_mark(M) nF_mark(plus(X1,X2)) -> nF_a__plus(mark(X1),mark(X2)) nF_a__plus(N,s(M)) -> nF_mark(N) nF_a__plus(N,s(M)) -> nF_a__plus(mark(N),mark(M)) UsableRules: a__and(tt,X) -> mark(X) a__plus(N,0) -> mark(N) a__plus(N,s(M)) -> s(a__plus(mark(N),mark(M))) mark(and(X1,X2)) -> a__and(mark(X1),X2) mark(plus(X1,X2)) -> a__plus(mark(X1),mark(X2)) mark(tt) -> tt mark(0) -> 0 mark(s(X)) -> s(mark(X)) a__and(X1,X2) -> and(X1,X2) a__plus(X1,X2) -> plus(X1,X2) Polynomial Interpretation: [a__and](X1,X2) = X1 + X2 [tt] = 1 [mark](X) = X [a__plus](X1,X2) = X1 + X2 [0] = 1 [s](X) = X + 1 [and](X1,X2) = X1 + X2 [plus](X1,X2) = X1 + X2 [nF_a__and](X1,X2) = X2 [nF_mark](X) = X [nF_a__plus](X1,X2) = X1 + X2 TIME: 9.1812e-2 -> -> Dependency pairs in cycle: nF_a__and(tt,X) -> nF_mark(X) nF_mark(and(X1,X2)) -> nF_a__and(mark(X1),X2) nF_a__plus(N,s(M)) -> nF_mark(N) nF_mark(plus(X1,X2)) -> nF_a__plus(mark(X1),mark(X2)) nF_a__plus(N,s(M)) -> nF_mark(M) nF_mark(and(X1,X2)) -> nF_mark(X1) nF_mark(plus(X1,X2)) -> nF_mark(X1) nF_mark(plus(X1,X2)) -> nF_mark(X2) UsableRules: a__and(tt,X) -> mark(X) a__plus(N,0) -> mark(N) a__plus(N,s(M)) -> s(a__plus(mark(N),mark(M))) mark(and(X1,X2)) -> a__and(mark(X1),X2) mark(plus(X1,X2)) -> a__plus(mark(X1),mark(X2)) mark(tt) -> tt mark(0) -> 0 mark(s(X)) -> s(mark(X)) a__and(X1,X2) -> and(X1,X2) a__plus(X1,X2) -> plus(X1,X2) Polynomial Interpretation: [a__and](X1,X2) = X1 + X2 [tt] = 1 [mark](X) = X [a__plus](X1,X2) = X1 + X2 + 1 [0] = 1 [s](X) = X [and](X1,X2) = X1 + X2 [plus](X1,X2) = X1 + X2 + 1 [nF_a__and](X1,X2) = X2 [nF_mark](X) = X [nF_a__plus](X1,X2) = X1 + X2 TIME: 4.5852e-2 -> -> Dependency pairs in cycle: nF_a__and(tt,X) -> nF_mark(X) nF_mark(and(X1,X2)) -> nF_a__and(mark(X1),X2) nF_mark(plus(X1,X2)) -> nF_mark(X1) nF_mark(and(X1,X2)) -> nF_mark(X1) nF_a__plus(N,s(M)) -> nF_mark(M) nF_mark(plus(X1,X2)) -> nF_a__plus(mark(X1),mark(X2)) nF_a__plus(N,s(M)) -> nF_mark(N) UsableRules: a__and(tt,X) -> mark(X) a__plus(N,0) -> mark(N) a__plus(N,s(M)) -> s(a__plus(mark(N),mark(M))) mark(and(X1,X2)) -> a__and(mark(X1),X2) mark(plus(X1,X2)) -> a__plus(mark(X1),mark(X2)) mark(tt) -> tt mark(0) -> 0 mark(s(X)) -> s(mark(X)) a__and(X1,X2) -> and(X1,X2) a__plus(X1,X2) -> plus(X1,X2) Polynomial Interpretation: [a__and](X1,X2) = X1 + X2 [tt] = 1 [mark](X) = X [a__plus](X1,X2) = X1 + X2 + 1 [0] = 1 [s](X) = X [and](X1,X2) = X1 + X2 [plus](X1,X2) = X1 + X2 + 1 [nF_a__and](X1,X2) = X2 [nF_mark](X) = X [nF_a__plus](X1,X2) = X1 + X2 + 1 TIME: 4.5042e-2 -> -> Dependency pairs in cycle: nF_a__and(tt,X) -> nF_mark(X) nF_mark(and(X1,X2)) -> nF_a__and(mark(X1),X2) nF_a__plus(N,s(M)) -> nF_mark(M) nF_mark(plus(X1,X2)) -> nF_a__plus(mark(X1),mark(X2)) nF_mark(and(X1,X2)) -> nF_mark(X1) nF_mark(plus(X1,X2)) -> nF_mark(X1) UsableRules: a__and(tt,X) -> mark(X) a__plus(N,0) -> mark(N) a__plus(N,s(M)) -> s(a__plus(mark(N),mark(M))) mark(and(X1,X2)) -> a__and(mark(X1),X2) mark(plus(X1,X2)) -> a__plus(mark(X1),mark(X2)) mark(tt) -> tt mark(0) -> 0 mark(s(X)) -> s(mark(X)) a__and(X1,X2) -> and(X1,X2) a__plus(X1,X2) -> plus(X1,X2) Polynomial Interpretation: [a__and](X1,X2) = X1 + X2 [tt] = 1 [mark](X) = X [a__plus](X1,X2) = X1 + X2 + 1 [0] = 1 [s](X) = X [and](X1,X2) = X1 + X2 [plus](X1,X2) = X1 + X2 + 1 [nF_a__and](X1,X2) = X2 [nF_mark](X) = X [nF_a__plus](X1,X2) = X2 TIME: 4.5849e-2 -> -> Dependency pairs in cycle: nF_a__and(tt,X) -> nF_mark(X) nF_mark(and(X1,X2)) -> nF_a__and(mark(X1),X2) nF_mark(and(X1,X2)) -> nF_mark(X1) nF_a__plus(N,s(M)) -> nF_mark(M) nF_mark(plus(X1,X2)) -> nF_a__plus(mark(X1),mark(X2)) UsableRules: a__and(tt,X) -> mark(X) a__plus(N,0) -> mark(N) a__plus(N,s(M)) -> s(a__plus(mark(N),mark(M))) mark(and(X1,X2)) -> a__and(mark(X1),X2) mark(plus(X1,X2)) -> a__plus(mark(X1),mark(X2)) mark(tt) -> tt mark(0) -> 0 mark(s(X)) -> s(mark(X)) a__and(X1,X2) -> and(X1,X2) a__plus(X1,X2) -> plus(X1,X2) Polynomial Interpretation: [a__and](X1,X2) = X1 + X2 [tt] = 1 [mark](X) = X [a__plus](X1,X2) = X1 + X2 + 1 [0] = 1 [s](X) = X [and](X1,X2) = X1 + X2 [plus](X1,X2) = X1 + X2 + 1 [nF_a__and](X1,X2) = X2 [nF_mark](X) = X [nF_a__plus](X1,X2) = X2 TIME: 4.3859e-2 -> -> Dependency pairs in cycle: nF_a__and(tt,X) -> nF_mark(X) nF_mark(and(X1,X2)) -> nF_a__and(mark(X1),X2) nF_mark(and(X1,X2)) -> nF_mark(X1) 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.