YES proof of Transformed_CSR_04_Ex1_2_AEL03_GM.trs # AProVE Commit ID: c69e44bd14796315568835c1ffa2502984884775 jera 20211004 unpublished Termination w.r.t. Q of the given QTRS could be proven: (0) QTRS (1) DependencyPairsProof [EQUIVALENT, 33 ms] (2) QDP (3) TransformationProof [EQUIVALENT, 0 ms] (4) QDP (5) DependencyGraphProof [EQUIVALENT, 0 ms] (6) QDP (7) QDPOrderProof [EQUIVALENT, 258 ms] (8) QDP (9) QDPOrderProof [EQUIVALENT, 255 ms] (10) QDP (11) QDPOrderProof [EQUIVALENT, 265 ms] (12) QDP (13) DependencyGraphProof [EQUIVALENT, 0 ms] (14) QDP (15) QDPOrderProof [EQUIVALENT, 281 ms] (16) QDP (17) QDPOrderProof [EQUIVALENT, 230 ms] (18) QDP (19) DependencyGraphProof [EQUIVALENT, 0 ms] (20) QDP (21) QDPOrderProof [EQUIVALENT, 171 ms] (22) QDP (23) DependencyGraphProof [EQUIVALENT, 0 ms] (24) QDP (25) QDPOrderProof [EQUIVALENT, 141 ms] (26) QDP (27) DependencyGraphProof [EQUIVALENT, 0 ms] (28) AND (29) QDP (30) QDPOrderProof [EQUIVALENT, 56 ms] (31) QDP (32) QDPOrderProof [EQUIVALENT, 47 ms] (33) QDP (34) QDPOrderProof [EQUIVALENT, 267 ms] (35) QDP (36) DependencyGraphProof [EQUIVALENT, 0 ms] (37) AND (38) QDP (39) UsableRulesProof [EQUIVALENT, 0 ms] (40) QDP (41) QDPSizeChangeProof [EQUIVALENT, 0 ms] (42) YES (43) QDP (44) QDPOrderProof [EQUIVALENT, 192 ms] (45) QDP (46) PisEmptyProof [EQUIVALENT, 0 ms] (47) YES (48) QDP (49) QDPOrderProof [EQUIVALENT, 263 ms] (50) QDP (51) PisEmptyProof [EQUIVALENT, 0 ms] (52) YES ---------------------------------------- (0) Obligation: Q restricted rewrite system: The TRS R consists of the following rules: a__from(X) -> cons(mark(X), from(s(X))) a__2ndspos(0, Z) -> rnil a__2ndspos(s(N), cons(X, cons(Y, Z))) -> rcons(posrecip(mark(Y)), a__2ndsneg(mark(N), mark(Z))) a__2ndsneg(0, Z) -> rnil a__2ndsneg(s(N), cons(X, cons(Y, Z))) -> rcons(negrecip(mark(Y)), a__2ndspos(mark(N), mark(Z))) a__pi(X) -> a__2ndspos(mark(X), a__from(0)) a__plus(0, Y) -> mark(Y) a__plus(s(X), Y) -> s(a__plus(mark(X), mark(Y))) a__times(0, Y) -> 0 a__times(s(X), Y) -> a__plus(mark(Y), a__times(mark(X), mark(Y))) a__square(X) -> a__times(mark(X), mark(X)) mark(from(X)) -> a__from(mark(X)) mark(2ndspos(X1, X2)) -> a__2ndspos(mark(X1), mark(X2)) mark(2ndsneg(X1, X2)) -> a__2ndsneg(mark(X1), mark(X2)) mark(pi(X)) -> a__pi(mark(X)) mark(plus(X1, X2)) -> a__plus(mark(X1), mark(X2)) mark(times(X1, X2)) -> a__times(mark(X1), mark(X2)) mark(square(X)) -> a__square(mark(X)) mark(0) -> 0 mark(s(X)) -> s(mark(X)) mark(posrecip(X)) -> posrecip(mark(X)) mark(negrecip(X)) -> negrecip(mark(X)) mark(nil) -> nil mark(cons(X1, X2)) -> cons(mark(X1), X2) mark(rnil) -> rnil mark(rcons(X1, X2)) -> rcons(mark(X1), mark(X2)) a__from(X) -> from(X) a__2ndspos(X1, X2) -> 2ndspos(X1, X2) a__2ndsneg(X1, X2) -> 2ndsneg(X1, X2) a__pi(X) -> pi(X) a__plus(X1, X2) -> plus(X1, X2) a__times(X1, X2) -> times(X1, X2) a__square(X) -> square(X) Q is empty. ---------------------------------------- (1) DependencyPairsProof (EQUIVALENT) Using Dependency Pairs [AG00,LPAR04] we result in the following initial DP problem. ---------------------------------------- (2) Obligation: Q DP problem: The TRS P consists of the following rules: A__FROM(X) -> MARK(X) A__2NDSPOS(s(N), cons(X, cons(Y, Z))) -> MARK(Y) A__2NDSPOS(s(N), cons(X, cons(Y, Z))) -> A__2NDSNEG(mark(N), mark(Z)) A__2NDSPOS(s(N), cons(X, cons(Y, Z))) -> MARK(N) A__2NDSPOS(s(N), cons(X, cons(Y, Z))) -> MARK(Z) A__2NDSNEG(s(N), cons(X, cons(Y, Z))) -> MARK(Y) A__2NDSNEG(s(N), cons(X, cons(Y, Z))) -> A__2NDSPOS(mark(N), mark(Z)) A__2NDSNEG(s(N), cons(X, cons(Y, Z))) -> MARK(N) A__2NDSNEG(s(N), cons(X, cons(Y, Z))) -> MARK(Z) A__PI(X) -> A__2NDSPOS(mark(X), a__from(0)) A__PI(X) -> MARK(X) A__PI(X) -> A__FROM(0) A__PLUS(0, Y) -> MARK(Y) A__PLUS(s(X), Y) -> A__PLUS(mark(X), mark(Y)) A__PLUS(s(X), Y) -> MARK(X) A__PLUS(s(X), Y) -> MARK(Y) A__TIMES(s(X), Y) -> A__PLUS(mark(Y), a__times(mark(X), mark(Y))) A__TIMES(s(X), Y) -> MARK(Y) A__TIMES(s(X), Y) -> A__TIMES(mark(X), mark(Y)) A__TIMES(s(X), Y) -> MARK(X) A__SQUARE(X) -> A__TIMES(mark(X), mark(X)) A__SQUARE(X) -> MARK(X) MARK(from(X)) -> A__FROM(mark(X)) MARK(from(X)) -> MARK(X) MARK(2ndspos(X1, X2)) -> A__2NDSPOS(mark(X1), mark(X2)) MARK(2ndspos(X1, X2)) -> MARK(X1) MARK(2ndspos(X1, X2)) -> MARK(X2) MARK(2ndsneg(X1, X2)) -> A__2NDSNEG(mark(X1), mark(X2)) MARK(2ndsneg(X1, X2)) -> MARK(X1) MARK(2ndsneg(X1, X2)) -> MARK(X2) MARK(pi(X)) -> A__PI(mark(X)) MARK(pi(X)) -> MARK(X) MARK(plus(X1, X2)) -> A__PLUS(mark(X1), mark(X2)) MARK(plus(X1, X2)) -> MARK(X1) MARK(plus(X1, X2)) -> MARK(X2) MARK(times(X1, X2)) -> A__TIMES(mark(X1), mark(X2)) MARK(times(X1, X2)) -> MARK(X1) MARK(times(X1, X2)) -> MARK(X2) MARK(square(X)) -> A__SQUARE(mark(X)) MARK(square(X)) -> MARK(X) MARK(s(X)) -> MARK(X) MARK(posrecip(X)) -> MARK(X) MARK(negrecip(X)) -> MARK(X) MARK(cons(X1, X2)) -> MARK(X1) MARK(rcons(X1, X2)) -> MARK(X1) MARK(rcons(X1, X2)) -> MARK(X2) The TRS R consists of the following rules: a__from(X) -> cons(mark(X), from(s(X))) a__2ndspos(0, Z) -> rnil a__2ndspos(s(N), cons(X, cons(Y, Z))) -> rcons(posrecip(mark(Y)), a__2ndsneg(mark(N), mark(Z))) a__2ndsneg(0, Z) -> rnil a__2ndsneg(s(N), cons(X, cons(Y, Z))) -> rcons(negrecip(mark(Y)), a__2ndspos(mark(N), mark(Z))) a__pi(X) -> a__2ndspos(mark(X), a__from(0)) a__plus(0, Y) -> mark(Y) a__plus(s(X), Y) -> s(a__plus(mark(X), mark(Y))) a__times(0, Y) -> 0 a__times(s(X), Y) -> a__plus(mark(Y), a__times(mark(X), mark(Y))) a__square(X) -> a__times(mark(X), mark(X)) mark(from(X)) -> a__from(mark(X)) mark(2ndspos(X1, X2)) -> a__2ndspos(mark(X1), mark(X2)) mark(2ndsneg(X1, X2)) -> a__2ndsneg(mark(X1), mark(X2)) mark(pi(X)) -> a__pi(mark(X)) mark(plus(X1, X2)) -> a__plus(mark(X1), mark(X2)) mark(times(X1, X2)) -> a__times(mark(X1), mark(X2)) mark(square(X)) -> a__square(mark(X)) mark(0) -> 0 mark(s(X)) -> s(mark(X)) mark(posrecip(X)) -> posrecip(mark(X)) mark(negrecip(X)) -> negrecip(mark(X)) mark(nil) -> nil mark(cons(X1, X2)) -> cons(mark(X1), X2) mark(rnil) -> rnil mark(rcons(X1, X2)) -> rcons(mark(X1), mark(X2)) a__from(X) -> from(X) a__2ndspos(X1, X2) -> 2ndspos(X1, X2) a__2ndsneg(X1, X2) -> 2ndsneg(X1, X2) a__pi(X) -> pi(X) a__plus(X1, X2) -> plus(X1, X2) a__times(X1, X2) -> times(X1, X2) a__square(X) -> square(X) Q is empty. We have to consider all minimal (P,Q,R)-chains. ---------------------------------------- (3) TransformationProof (EQUIVALENT) By narrowing [LPAR04] the rule A__PI(X) -> A__2NDSPOS(mark(X), a__from(0)) at position [1] we obtained the following new rules [LPAR04]: (A__PI(y0) -> A__2NDSPOS(mark(y0), cons(mark(0), from(s(0)))),A__PI(y0) -> A__2NDSPOS(mark(y0), cons(mark(0), from(s(0))))) (A__PI(y0) -> A__2NDSPOS(mark(y0), from(0)),A__PI(y0) -> A__2NDSPOS(mark(y0), from(0))) ---------------------------------------- (4) Obligation: Q DP problem: The TRS P consists of the following rules: A__FROM(X) -> MARK(X) A__2NDSPOS(s(N), cons(X, cons(Y, Z))) -> MARK(Y) A__2NDSPOS(s(N), cons(X, cons(Y, Z))) -> A__2NDSNEG(mark(N), mark(Z)) A__2NDSPOS(s(N), cons(X, cons(Y, Z))) -> MARK(N) A__2NDSPOS(s(N), cons(X, cons(Y, Z))) -> MARK(Z) A__2NDSNEG(s(N), cons(X, cons(Y, Z))) -> MARK(Y) A__2NDSNEG(s(N), cons(X, cons(Y, Z))) -> A__2NDSPOS(mark(N), mark(Z)) A__2NDSNEG(s(N), cons(X, cons(Y, Z))) -> MARK(N) A__2NDSNEG(s(N), cons(X, cons(Y, Z))) -> MARK(Z) A__PI(X) -> MARK(X) A__PI(X) -> A__FROM(0) A__PLUS(0, Y) -> MARK(Y) A__PLUS(s(X), Y) -> A__PLUS(mark(X), mark(Y)) A__PLUS(s(X), Y) -> MARK(X) A__PLUS(s(X), Y) -> MARK(Y) A__TIMES(s(X), Y) -> A__PLUS(mark(Y), a__times(mark(X), mark(Y))) A__TIMES(s(X), Y) -> MARK(Y) A__TIMES(s(X), Y) -> A__TIMES(mark(X), mark(Y)) A__TIMES(s(X), Y) -> MARK(X) A__SQUARE(X) -> A__TIMES(mark(X), mark(X)) A__SQUARE(X) -> MARK(X) MARK(from(X)) -> A__FROM(mark(X)) MARK(from(X)) -> MARK(X) MARK(2ndspos(X1, X2)) -> A__2NDSPOS(mark(X1), mark(X2)) MARK(2ndspos(X1, X2)) -> MARK(X1) MARK(2ndspos(X1, X2)) -> MARK(X2) MARK(2ndsneg(X1, X2)) -> A__2NDSNEG(mark(X1), mark(X2)) MARK(2ndsneg(X1, X2)) -> MARK(X1) MARK(2ndsneg(X1, X2)) -> MARK(X2) MARK(pi(X)) -> A__PI(mark(X)) MARK(pi(X)) -> MARK(X) MARK(plus(X1, X2)) -> A__PLUS(mark(X1), mark(X2)) MARK(plus(X1, X2)) -> MARK(X1) MARK(plus(X1, X2)) -> MARK(X2) MARK(times(X1, X2)) -> A__TIMES(mark(X1), mark(X2)) MARK(times(X1, X2)) -> MARK(X1) MARK(times(X1, X2)) -> MARK(X2) MARK(square(X)) -> A__SQUARE(mark(X)) MARK(square(X)) -> MARK(X) MARK(s(X)) -> MARK(X) MARK(posrecip(X)) -> MARK(X) MARK(negrecip(X)) -> MARK(X) MARK(cons(X1, X2)) -> MARK(X1) MARK(rcons(X1, X2)) -> MARK(X1) MARK(rcons(X1, X2)) -> MARK(X2) A__PI(y0) -> A__2NDSPOS(mark(y0), cons(mark(0), from(s(0)))) A__PI(y0) -> A__2NDSPOS(mark(y0), from(0)) The TRS R consists of the following rules: a__from(X) -> cons(mark(X), from(s(X))) a__2ndspos(0, Z) -> rnil a__2ndspos(s(N), cons(X, cons(Y, Z))) -> rcons(posrecip(mark(Y)), a__2ndsneg(mark(N), mark(Z))) a__2ndsneg(0, Z) -> rnil a__2ndsneg(s(N), cons(X, cons(Y, Z))) -> rcons(negrecip(mark(Y)), a__2ndspos(mark(N), mark(Z))) a__pi(X) -> a__2ndspos(mark(X), a__from(0)) a__plus(0, Y) -> mark(Y) a__plus(s(X), Y) -> s(a__plus(mark(X), mark(Y))) a__times(0, Y) -> 0 a__times(s(X), Y) -> a__plus(mark(Y), a__times(mark(X), mark(Y))) a__square(X) -> a__times(mark(X), mark(X)) mark(from(X)) -> a__from(mark(X)) mark(2ndspos(X1, X2)) -> a__2ndspos(mark(X1), mark(X2)) mark(2ndsneg(X1, X2)) -> a__2ndsneg(mark(X1), mark(X2)) mark(pi(X)) -> a__pi(mark(X)) mark(plus(X1, X2)) -> a__plus(mark(X1), mark(X2)) mark(times(X1, X2)) -> a__times(mark(X1), mark(X2)) mark(square(X)) -> a__square(mark(X)) mark(0) -> 0 mark(s(X)) -> s(mark(X)) mark(posrecip(X)) -> posrecip(mark(X)) mark(negrecip(X)) -> negrecip(mark(X)) mark(nil) -> nil mark(cons(X1, X2)) -> cons(mark(X1), X2) mark(rnil) -> rnil mark(rcons(X1, X2)) -> rcons(mark(X1), mark(X2)) a__from(X) -> from(X) a__2ndspos(X1, X2) -> 2ndspos(X1, X2) a__2ndsneg(X1, X2) -> 2ndsneg(X1, X2) a__pi(X) -> pi(X) a__plus(X1, X2) -> plus(X1, X2) a__times(X1, X2) -> times(X1, X2) a__square(X) -> square(X) Q is empty. We have to consider all minimal (P,Q,R)-chains. ---------------------------------------- (5) DependencyGraphProof (EQUIVALENT) The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 2 less nodes. ---------------------------------------- (6) Obligation: Q DP problem: The TRS P consists of the following rules: MARK(from(X)) -> A__FROM(mark(X)) A__FROM(X) -> MARK(X) MARK(from(X)) -> MARK(X) MARK(2ndspos(X1, X2)) -> A__2NDSPOS(mark(X1), mark(X2)) A__2NDSPOS(s(N), cons(X, cons(Y, Z))) -> MARK(Y) MARK(2ndspos(X1, X2)) -> MARK(X1) MARK(2ndspos(X1, X2)) -> MARK(X2) MARK(2ndsneg(X1, X2)) -> A__2NDSNEG(mark(X1), mark(X2)) A__2NDSNEG(s(N), cons(X, cons(Y, Z))) -> MARK(Y) MARK(2ndsneg(X1, X2)) -> MARK(X1) MARK(2ndsneg(X1, X2)) -> MARK(X2) MARK(pi(X)) -> A__PI(mark(X)) A__PI(X) -> MARK(X) MARK(pi(X)) -> MARK(X) MARK(plus(X1, X2)) -> A__PLUS(mark(X1), mark(X2)) A__PLUS(0, Y) -> MARK(Y) MARK(plus(X1, X2)) -> MARK(X1) MARK(plus(X1, X2)) -> MARK(X2) MARK(times(X1, X2)) -> A__TIMES(mark(X1), mark(X2)) A__TIMES(s(X), Y) -> A__PLUS(mark(Y), a__times(mark(X), mark(Y))) A__PLUS(s(X), Y) -> A__PLUS(mark(X), mark(Y)) A__PLUS(s(X), Y) -> MARK(X) MARK(times(X1, X2)) -> MARK(X1) MARK(times(X1, X2)) -> MARK(X2) MARK(square(X)) -> A__SQUARE(mark(X)) A__SQUARE(X) -> A__TIMES(mark(X), mark(X)) A__TIMES(s(X), Y) -> MARK(Y) MARK(square(X)) -> MARK(X) MARK(s(X)) -> MARK(X) MARK(posrecip(X)) -> MARK(X) MARK(negrecip(X)) -> MARK(X) MARK(cons(X1, X2)) -> MARK(X1) MARK(rcons(X1, X2)) -> MARK(X1) MARK(rcons(X1, X2)) -> MARK(X2) A__TIMES(s(X), Y) -> A__TIMES(mark(X), mark(Y)) A__TIMES(s(X), Y) -> MARK(X) A__SQUARE(X) -> MARK(X) A__PLUS(s(X), Y) -> MARK(Y) A__PI(X) -> A__FROM(0) A__2NDSNEG(s(N), cons(X, cons(Y, Z))) -> A__2NDSPOS(mark(N), mark(Z)) A__2NDSPOS(s(N), cons(X, cons(Y, Z))) -> A__2NDSNEG(mark(N), mark(Z)) A__2NDSNEG(s(N), cons(X, cons(Y, Z))) -> MARK(N) A__2NDSNEG(s(N), cons(X, cons(Y, Z))) -> MARK(Z) A__2NDSPOS(s(N), cons(X, cons(Y, Z))) -> MARK(N) A__2NDSPOS(s(N), cons(X, cons(Y, Z))) -> MARK(Z) The TRS R consists of the following rules: a__from(X) -> cons(mark(X), from(s(X))) a__2ndspos(0, Z) -> rnil a__2ndspos(s(N), cons(X, cons(Y, Z))) -> rcons(posrecip(mark(Y)), a__2ndsneg(mark(N), mark(Z))) a__2ndsneg(0, Z) -> rnil a__2ndsneg(s(N), cons(X, cons(Y, Z))) -> rcons(negrecip(mark(Y)), a__2ndspos(mark(N), mark(Z))) a__pi(X) -> a__2ndspos(mark(X), a__from(0)) a__plus(0, Y) -> mark(Y) a__plus(s(X), Y) -> s(a__plus(mark(X), mark(Y))) a__times(0, Y) -> 0 a__times(s(X), Y) -> a__plus(mark(Y), a__times(mark(X), mark(Y))) a__square(X) -> a__times(mark(X), mark(X)) mark(from(X)) -> a__from(mark(X)) mark(2ndspos(X1, X2)) -> a__2ndspos(mark(X1), mark(X2)) mark(2ndsneg(X1, X2)) -> a__2ndsneg(mark(X1), mark(X2)) mark(pi(X)) -> a__pi(mark(X)) mark(plus(X1, X2)) -> a__plus(mark(X1), mark(X2)) mark(times(X1, X2)) -> a__times(mark(X1), mark(X2)) mark(square(X)) -> a__square(mark(X)) mark(0) -> 0 mark(s(X)) -> s(mark(X)) mark(posrecip(X)) -> posrecip(mark(X)) mark(negrecip(X)) -> negrecip(mark(X)) mark(nil) -> nil mark(cons(X1, X2)) -> cons(mark(X1), X2) mark(rnil) -> rnil mark(rcons(X1, X2)) -> rcons(mark(X1), mark(X2)) a__from(X) -> from(X) a__2ndspos(X1, X2) -> 2ndspos(X1, X2) a__2ndsneg(X1, X2) -> 2ndsneg(X1, X2) a__pi(X) -> pi(X) a__plus(X1, X2) -> plus(X1, X2) a__times(X1, X2) -> times(X1, X2) a__square(X) -> square(X) Q is empty. We have to consider all minimal (P,Q,R)-chains. ---------------------------------------- (7) QDPOrderProof (EQUIVALENT) We use the reduction pair processor [LPAR04,JAR06]. The following pairs can be oriented strictly and are deleted. MARK(pi(X)) -> MARK(X) A__PLUS(s(X), Y) -> MARK(X) MARK(square(X)) -> MARK(X) A__SQUARE(X) -> MARK(X) The remaining pairs can at least be oriented weakly. Used ordering: Matrix interpretation [MATRO] with arctic natural numbers [ARCTIC]: <<< POL(MARK(x_1)) = [[4A]] + [[0A]] * x_1 >>> <<< POL(from(x_1)) = [[2A]] + [[2A]] * x_1 >>> <<< POL(A__FROM(x_1)) = [[4A]] + [[2A]] * x_1 >>> <<< POL(mark(x_1)) = [[-I]] + [[0A]] * x_1 >>> <<< POL(2ndspos(x_1, x_2)) = [[4A]] + [[0A]] * x_1 + [[3A]] * x_2 >>> <<< POL(A__2NDSPOS(x_1, x_2)) = [[4A]] + [[0A]] * x_1 + [[1A]] * x_2 >>> <<< POL(s(x_1)) = [[0A]] + [[0A]] * x_1 >>> <<< POL(cons(x_1, x_2)) = [[0A]] + [[1A]] * x_1 + [[0A]] * x_2 >>> <<< POL(2ndsneg(x_1, x_2)) = [[4A]] + [[0A]] * x_1 + [[3A]] * x_2 >>> <<< POL(A__2NDSNEG(x_1, x_2)) = [[4A]] + [[0A]] * x_1 + [[1A]] * x_2 >>> <<< POL(pi(x_1)) = [[5A]] + [[1A]] * x_1 >>> <<< POL(A__PI(x_1)) = [[4A]] + [[1A]] * x_1 >>> <<< POL(plus(x_1, x_2)) = [[3A]] + [[5A]] * x_1 + [[0A]] * x_2 >>> <<< POL(A__PLUS(x_1, x_2)) = [[3A]] + [[5A]] * x_1 + [[0A]] * x_2 >>> <<< POL(0) = [[0A]] >>> <<< POL(times(x_1, x_2)) = [[3A]] + [[0A]] * x_1 + [[5A]] * x_2 >>> <<< POL(A__TIMES(x_1, x_2)) = [[4A]] + [[0A]] * x_1 + [[5A]] * x_2 >>> <<< POL(a__times(x_1, x_2)) = [[3A]] + [[0A]] * x_1 + [[5A]] * x_2 >>> <<< POL(square(x_1)) = [[5A]] + [[5A]] * x_1 >>> <<< POL(A__SQUARE(x_1)) = [[5A]] + [[5A]] * x_1 >>> <<< POL(posrecip(x_1)) = [[-I]] + [[0A]] * x_1 >>> <<< POL(negrecip(x_1)) = [[-I]] + [[0A]] * x_1 >>> <<< POL(rcons(x_1, x_2)) = [[-I]] + [[0A]] * x_1 + [[0A]] * x_2 >>> <<< POL(a__from(x_1)) = [[2A]] + [[2A]] * x_1 >>> <<< POL(a__2ndspos(x_1, x_2)) = [[4A]] + [[0A]] * x_1 + [[3A]] * x_2 >>> <<< POL(a__2ndsneg(x_1, x_2)) = [[4A]] + [[0A]] * x_1 + [[3A]] * x_2 >>> <<< POL(a__pi(x_1)) = [[5A]] + [[1A]] * x_1 >>> <<< POL(a__plus(x_1, x_2)) = [[3A]] + [[5A]] * x_1 + [[0A]] * x_2 >>> <<< POL(a__square(x_1)) = [[5A]] + [[5A]] * x_1 >>> <<< POL(nil) = [[2A]] >>> <<< POL(rnil) = [[3A]] >>> The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented: mark(from(X)) -> a__from(mark(X)) mark(2ndspos(X1, X2)) -> a__2ndspos(mark(X1), mark(X2)) mark(2ndsneg(X1, X2)) -> a__2ndsneg(mark(X1), mark(X2)) mark(pi(X)) -> a__pi(mark(X)) mark(plus(X1, X2)) -> a__plus(mark(X1), mark(X2)) a__plus(0, Y) -> mark(Y) mark(times(X1, X2)) -> a__times(mark(X1), mark(X2)) a__times(s(X), Y) -> a__plus(mark(Y), a__times(mark(X), mark(Y))) mark(square(X)) -> a__square(mark(X)) a__square(X) -> a__times(mark(X), mark(X)) mark(0) -> 0 mark(s(X)) -> s(mark(X)) mark(posrecip(X)) -> posrecip(mark(X)) mark(negrecip(X)) -> negrecip(mark(X)) mark(nil) -> nil mark(cons(X1, X2)) -> cons(mark(X1), X2) mark(rnil) -> rnil mark(rcons(X1, X2)) -> rcons(mark(X1), mark(X2)) a__times(0, Y) -> 0 a__times(X1, X2) -> times(X1, X2) a__from(X) -> from(X) a__2ndspos(0, Z) -> rnil a__2ndspos(X1, X2) -> 2ndspos(X1, X2) a__2ndsneg(0, Z) -> rnil a__2ndsneg(X1, X2) -> 2ndsneg(X1, X2) a__pi(X) -> pi(X) a__plus(X1, X2) -> plus(X1, X2) a__square(X) -> square(X) a__plus(s(X), Y) -> s(a__plus(mark(X), mark(Y))) a__pi(X) -> a__2ndspos(mark(X), a__from(0)) a__from(X) -> cons(mark(X), from(s(X))) a__2ndspos(s(N), cons(X, cons(Y, Z))) -> rcons(posrecip(mark(Y)), a__2ndsneg(mark(N), mark(Z))) a__2ndsneg(s(N), cons(X, cons(Y, Z))) -> rcons(negrecip(mark(Y)), a__2ndspos(mark(N), mark(Z))) ---------------------------------------- (8) Obligation: Q DP problem: The TRS P consists of the following rules: MARK(from(X)) -> A__FROM(mark(X)) A__FROM(X) -> MARK(X) MARK(from(X)) -> MARK(X) MARK(2ndspos(X1, X2)) -> A__2NDSPOS(mark(X1), mark(X2)) A__2NDSPOS(s(N), cons(X, cons(Y, Z))) -> MARK(Y) MARK(2ndspos(X1, X2)) -> MARK(X1) MARK(2ndspos(X1, X2)) -> MARK(X2) MARK(2ndsneg(X1, X2)) -> A__2NDSNEG(mark(X1), mark(X2)) A__2NDSNEG(s(N), cons(X, cons(Y, Z))) -> MARK(Y) MARK(2ndsneg(X1, X2)) -> MARK(X1) MARK(2ndsneg(X1, X2)) -> MARK(X2) MARK(pi(X)) -> A__PI(mark(X)) A__PI(X) -> MARK(X) MARK(plus(X1, X2)) -> A__PLUS(mark(X1), mark(X2)) A__PLUS(0, Y) -> MARK(Y) MARK(plus(X1, X2)) -> MARK(X1) MARK(plus(X1, X2)) -> MARK(X2) MARK(times(X1, X2)) -> A__TIMES(mark(X1), mark(X2)) A__TIMES(s(X), Y) -> A__PLUS(mark(Y), a__times(mark(X), mark(Y))) A__PLUS(s(X), Y) -> A__PLUS(mark(X), mark(Y)) MARK(times(X1, X2)) -> MARK(X1) MARK(times(X1, X2)) -> MARK(X2) MARK(square(X)) -> A__SQUARE(mark(X)) A__SQUARE(X) -> A__TIMES(mark(X), mark(X)) A__TIMES(s(X), Y) -> MARK(Y) MARK(s(X)) -> MARK(X) MARK(posrecip(X)) -> MARK(X) MARK(negrecip(X)) -> MARK(X) MARK(cons(X1, X2)) -> MARK(X1) MARK(rcons(X1, X2)) -> MARK(X1) MARK(rcons(X1, X2)) -> MARK(X2) A__TIMES(s(X), Y) -> A__TIMES(mark(X), mark(Y)) A__TIMES(s(X), Y) -> MARK(X) A__PLUS(s(X), Y) -> MARK(Y) A__PI(X) -> A__FROM(0) A__2NDSNEG(s(N), cons(X, cons(Y, Z))) -> A__2NDSPOS(mark(N), mark(Z)) A__2NDSPOS(s(N), cons(X, cons(Y, Z))) -> A__2NDSNEG(mark(N), mark(Z)) A__2NDSNEG(s(N), cons(X, cons(Y, Z))) -> MARK(N) A__2NDSNEG(s(N), cons(X, cons(Y, Z))) -> MARK(Z) A__2NDSPOS(s(N), cons(X, cons(Y, Z))) -> MARK(N) A__2NDSPOS(s(N), cons(X, cons(Y, Z))) -> MARK(Z) The TRS R consists of the following rules: a__from(X) -> cons(mark(X), from(s(X))) a__2ndspos(0, Z) -> rnil a__2ndspos(s(N), cons(X, cons(Y, Z))) -> rcons(posrecip(mark(Y)), a__2ndsneg(mark(N), mark(Z))) a__2ndsneg(0, Z) -> rnil a__2ndsneg(s(N), cons(X, cons(Y, Z))) -> rcons(negrecip(mark(Y)), a__2ndspos(mark(N), mark(Z))) a__pi(X) -> a__2ndspos(mark(X), a__from(0)) a__plus(0, Y) -> mark(Y) a__plus(s(X), Y) -> s(a__plus(mark(X), mark(Y))) a__times(0, Y) -> 0 a__times(s(X), Y) -> a__plus(mark(Y), a__times(mark(X), mark(Y))) a__square(X) -> a__times(mark(X), mark(X)) mark(from(X)) -> a__from(mark(X)) mark(2ndspos(X1, X2)) -> a__2ndspos(mark(X1), mark(X2)) mark(2ndsneg(X1, X2)) -> a__2ndsneg(mark(X1), mark(X2)) mark(pi(X)) -> a__pi(mark(X)) mark(plus(X1, X2)) -> a__plus(mark(X1), mark(X2)) mark(times(X1, X2)) -> a__times(mark(X1), mark(X2)) mark(square(X)) -> a__square(mark(X)) mark(0) -> 0 mark(s(X)) -> s(mark(X)) mark(posrecip(X)) -> posrecip(mark(X)) mark(negrecip(X)) -> negrecip(mark(X)) mark(nil) -> nil mark(cons(X1, X2)) -> cons(mark(X1), X2) mark(rnil) -> rnil mark(rcons(X1, X2)) -> rcons(mark(X1), mark(X2)) a__from(X) -> from(X) a__2ndspos(X1, X2) -> 2ndspos(X1, X2) a__2ndsneg(X1, X2) -> 2ndsneg(X1, X2) a__pi(X) -> pi(X) a__plus(X1, X2) -> plus(X1, X2) a__times(X1, X2) -> times(X1, X2) a__square(X) -> square(X) Q is empty. We have to consider all minimal (P,Q,R)-chains. ---------------------------------------- (9) QDPOrderProof (EQUIVALENT) We use the reduction pair processor [LPAR04,JAR06]. The following pairs can be oriented strictly and are deleted. A__PI(X) -> A__FROM(0) The remaining pairs can at least be oriented weakly. Used ordering: Matrix interpretation [MATRO] with arctic natural numbers [ARCTIC]: <<< POL(MARK(x_1)) = [[3A]] + [[0A]] * x_1 >>> <<< POL(from(x_1)) = [[5A]] + [[0A]] * x_1 >>> <<< POL(A__FROM(x_1)) = [[4A]] + [[0A]] * x_1 >>> <<< POL(mark(x_1)) = [[5A]] + [[0A]] * x_1 >>> <<< POL(2ndspos(x_1, x_2)) = [[5A]] + [[0A]] * x_1 + [[0A]] * x_2 >>> <<< POL(A__2NDSPOS(x_1, x_2)) = [[5A]] + [[0A]] * x_1 + [[0A]] * x_2 >>> <<< POL(s(x_1)) = [[4A]] + [[0A]] * x_1 >>> <<< POL(cons(x_1, x_2)) = [[3A]] + [[0A]] * x_1 + [[0A]] * x_2 >>> <<< POL(2ndsneg(x_1, x_2)) = [[5A]] + [[0A]] * x_1 + [[0A]] * x_2 >>> <<< POL(A__2NDSNEG(x_1, x_2)) = [[5A]] + [[0A]] * x_1 + [[0A]] * x_2 >>> <<< POL(pi(x_1)) = [[5A]] + [[0A]] * x_1 >>> <<< POL(A__PI(x_1)) = [[5A]] + [[0A]] * x_1 >>> <<< POL(plus(x_1, x_2)) = [[5A]] + [[0A]] * x_1 + [[0A]] * x_2 >>> <<< POL(A__PLUS(x_1, x_2)) = [[5A]] + [[-I]] * x_1 + [[0A]] * x_2 >>> <<< POL(0) = [[4A]] >>> <<< POL(times(x_1, x_2)) = [[5A]] + [[0A]] * x_1 + [[0A]] * x_2 >>> <<< POL(A__TIMES(x_1, x_2)) = [[5A]] + [[0A]] * x_1 + [[0A]] * x_2 >>> <<< POL(a__times(x_1, x_2)) = [[5A]] + [[0A]] * x_1 + [[0A]] * x_2 >>> <<< POL(square(x_1)) = [[5A]] + [[0A]] * x_1 >>> <<< POL(A__SQUARE(x_1)) = [[5A]] + [[0A]] * x_1 >>> <<< POL(posrecip(x_1)) = [[-I]] + [[0A]] * x_1 >>> <<< POL(negrecip(x_1)) = [[-I]] + [[0A]] * x_1 >>> <<< POL(rcons(x_1, x_2)) = [[-I]] + [[0A]] * x_1 + [[0A]] * x_2 >>> <<< POL(a__from(x_1)) = [[5A]] + [[0A]] * x_1 >>> <<< POL(a__2ndspos(x_1, x_2)) = [[5A]] + [[0A]] * x_1 + [[0A]] * x_2 >>> <<< POL(a__2ndsneg(x_1, x_2)) = [[5A]] + [[0A]] * x_1 + [[0A]] * x_2 >>> <<< POL(a__pi(x_1)) = [[5A]] + [[0A]] * x_1 >>> <<< POL(a__plus(x_1, x_2)) = [[5A]] + [[0A]] * x_1 + [[0A]] * x_2 >>> <<< POL(a__square(x_1)) = [[5A]] + [[0A]] * x_1 >>> <<< POL(nil) = [[4A]] >>> <<< POL(rnil) = [[3A]] >>> The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented: mark(from(X)) -> a__from(mark(X)) mark(2ndspos(X1, X2)) -> a__2ndspos(mark(X1), mark(X2)) mark(2ndsneg(X1, X2)) -> a__2ndsneg(mark(X1), mark(X2)) mark(pi(X)) -> a__pi(mark(X)) mark(plus(X1, X2)) -> a__plus(mark(X1), mark(X2)) a__plus(0, Y) -> mark(Y) mark(times(X1, X2)) -> a__times(mark(X1), mark(X2)) a__times(s(X), Y) -> a__plus(mark(Y), a__times(mark(X), mark(Y))) mark(square(X)) -> a__square(mark(X)) a__square(X) -> a__times(mark(X), mark(X)) mark(0) -> 0 mark(s(X)) -> s(mark(X)) mark(posrecip(X)) -> posrecip(mark(X)) mark(negrecip(X)) -> negrecip(mark(X)) mark(nil) -> nil mark(cons(X1, X2)) -> cons(mark(X1), X2) mark(rnil) -> rnil mark(rcons(X1, X2)) -> rcons(mark(X1), mark(X2)) a__times(0, Y) -> 0 a__times(X1, X2) -> times(X1, X2) a__from(X) -> from(X) a__2ndspos(0, Z) -> rnil a__2ndspos(X1, X2) -> 2ndspos(X1, X2) a__2ndsneg(0, Z) -> rnil a__2ndsneg(X1, X2) -> 2ndsneg(X1, X2) a__pi(X) -> pi(X) a__plus(X1, X2) -> plus(X1, X2) a__square(X) -> square(X) a__plus(s(X), Y) -> s(a__plus(mark(X), mark(Y))) a__pi(X) -> a__2ndspos(mark(X), a__from(0)) a__from(X) -> cons(mark(X), from(s(X))) a__2ndspos(s(N), cons(X, cons(Y, Z))) -> rcons(posrecip(mark(Y)), a__2ndsneg(mark(N), mark(Z))) a__2ndsneg(s(N), cons(X, cons(Y, Z))) -> rcons(negrecip(mark(Y)), a__2ndspos(mark(N), mark(Z))) ---------------------------------------- (10) Obligation: Q DP problem: The TRS P consists of the following rules: MARK(from(X)) -> A__FROM(mark(X)) A__FROM(X) -> MARK(X) MARK(from(X)) -> MARK(X) MARK(2ndspos(X1, X2)) -> A__2NDSPOS(mark(X1), mark(X2)) A__2NDSPOS(s(N), cons(X, cons(Y, Z))) -> MARK(Y) MARK(2ndspos(X1, X2)) -> MARK(X1) MARK(2ndspos(X1, X2)) -> MARK(X2) MARK(2ndsneg(X1, X2)) -> A__2NDSNEG(mark(X1), mark(X2)) A__2NDSNEG(s(N), cons(X, cons(Y, Z))) -> MARK(Y) MARK(2ndsneg(X1, X2)) -> MARK(X1) MARK(2ndsneg(X1, X2)) -> MARK(X2) MARK(pi(X)) -> A__PI(mark(X)) A__PI(X) -> MARK(X) MARK(plus(X1, X2)) -> A__PLUS(mark(X1), mark(X2)) A__PLUS(0, Y) -> MARK(Y) MARK(plus(X1, X2)) -> MARK(X1) MARK(plus(X1, X2)) -> MARK(X2) MARK(times(X1, X2)) -> A__TIMES(mark(X1), mark(X2)) A__TIMES(s(X), Y) -> A__PLUS(mark(Y), a__times(mark(X), mark(Y))) A__PLUS(s(X), Y) -> A__PLUS(mark(X), mark(Y)) MARK(times(X1, X2)) -> MARK(X1) MARK(times(X1, X2)) -> MARK(X2) MARK(square(X)) -> A__SQUARE(mark(X)) A__SQUARE(X) -> A__TIMES(mark(X), mark(X)) A__TIMES(s(X), Y) -> MARK(Y) MARK(s(X)) -> MARK(X) MARK(posrecip(X)) -> MARK(X) MARK(negrecip(X)) -> MARK(X) MARK(cons(X1, X2)) -> MARK(X1) MARK(rcons(X1, X2)) -> MARK(X1) MARK(rcons(X1, X2)) -> MARK(X2) A__TIMES(s(X), Y) -> A__TIMES(mark(X), mark(Y)) A__TIMES(s(X), Y) -> MARK(X) A__PLUS(s(X), Y) -> MARK(Y) A__2NDSNEG(s(N), cons(X, cons(Y, Z))) -> A__2NDSPOS(mark(N), mark(Z)) A__2NDSPOS(s(N), cons(X, cons(Y, Z))) -> A__2NDSNEG(mark(N), mark(Z)) A__2NDSNEG(s(N), cons(X, cons(Y, Z))) -> MARK(N) A__2NDSNEG(s(N), cons(X, cons(Y, Z))) -> MARK(Z) A__2NDSPOS(s(N), cons(X, cons(Y, Z))) -> MARK(N) A__2NDSPOS(s(N), cons(X, cons(Y, Z))) -> MARK(Z) The TRS R consists of the following rules: a__from(X) -> cons(mark(X), from(s(X))) a__2ndspos(0, Z) -> rnil a__2ndspos(s(N), cons(X, cons(Y, Z))) -> rcons(posrecip(mark(Y)), a__2ndsneg(mark(N), mark(Z))) a__2ndsneg(0, Z) -> rnil a__2ndsneg(s(N), cons(X, cons(Y, Z))) -> rcons(negrecip(mark(Y)), a__2ndspos(mark(N), mark(Z))) a__pi(X) -> a__2ndspos(mark(X), a__from(0)) a__plus(0, Y) -> mark(Y) a__plus(s(X), Y) -> s(a__plus(mark(X), mark(Y))) a__times(0, Y) -> 0 a__times(s(X), Y) -> a__plus(mark(Y), a__times(mark(X), mark(Y))) a__square(X) -> a__times(mark(X), mark(X)) mark(from(X)) -> a__from(mark(X)) mark(2ndspos(X1, X2)) -> a__2ndspos(mark(X1), mark(X2)) mark(2ndsneg(X1, X2)) -> a__2ndsneg(mark(X1), mark(X2)) mark(pi(X)) -> a__pi(mark(X)) mark(plus(X1, X2)) -> a__plus(mark(X1), mark(X2)) mark(times(X1, X2)) -> a__times(mark(X1), mark(X2)) mark(square(X)) -> a__square(mark(X)) mark(0) -> 0 mark(s(X)) -> s(mark(X)) mark(posrecip(X)) -> posrecip(mark(X)) mark(negrecip(X)) -> negrecip(mark(X)) mark(nil) -> nil mark(cons(X1, X2)) -> cons(mark(X1), X2) mark(rnil) -> rnil mark(rcons(X1, X2)) -> rcons(mark(X1), mark(X2)) a__from(X) -> from(X) a__2ndspos(X1, X2) -> 2ndspos(X1, X2) a__2ndsneg(X1, X2) -> 2ndsneg(X1, X2) a__pi(X) -> pi(X) a__plus(X1, X2) -> plus(X1, X2) a__times(X1, X2) -> times(X1, X2) a__square(X) -> square(X) Q is empty. We have to consider all minimal (P,Q,R)-chains. ---------------------------------------- (11) QDPOrderProof (EQUIVALENT) We use the reduction pair processor [LPAR04,JAR06]. The following pairs can be oriented strictly and are deleted. A__PI(X) -> MARK(X) The remaining pairs can at least be oriented weakly. Used ordering: Matrix interpretation [MATRO] with arctic natural numbers [ARCTIC]: <<< POL(MARK(x_1)) = [[2A]] + [[1A]] * x_1 >>> <<< POL(from(x_1)) = [[1A]] + [[1A]] * x_1 >>> <<< POL(A__FROM(x_1)) = [[2A]] + [[2A]] * x_1 >>> <<< POL(mark(x_1)) = [[0A]] + [[0A]] * x_1 >>> <<< POL(2ndspos(x_1, x_2)) = [[1A]] + [[1A]] * x_1 + [[1A]] * x_2 >>> <<< POL(A__2NDSPOS(x_1, x_2)) = [[2A]] + [[2A]] * x_1 + [[2A]] * x_2 >>> <<< POL(s(x_1)) = [[0A]] + [[0A]] * x_1 >>> <<< POL(cons(x_1, x_2)) = [[0A]] + [[0A]] * x_1 + [[0A]] * x_2 >>> <<< POL(2ndsneg(x_1, x_2)) = [[1A]] + [[1A]] * x_1 + [[1A]] * x_2 >>> <<< POL(A__2NDSNEG(x_1, x_2)) = [[2A]] + [[2A]] * x_1 + [[2A]] * x_2 >>> <<< POL(pi(x_1)) = [[2A]] + [[2A]] * x_1 >>> <<< POL(A__PI(x_1)) = [[3A]] + [[3A]] * x_1 >>> <<< POL(plus(x_1, x_2)) = [[0A]] + [[0A]] * x_1 + [[0A]] * x_2 >>> <<< POL(A__PLUS(x_1, x_2)) = [[2A]] + [[-I]] * x_1 + [[1A]] * x_2 >>> <<< POL(0) = [[0A]] >>> <<< POL(times(x_1, x_2)) = [[1A]] + [[1A]] * x_1 + [[1A]] * x_2 >>> <<< POL(A__TIMES(x_1, x_2)) = [[1A]] + [[2A]] * x_1 + [[2A]] * x_2 >>> <<< POL(a__times(x_1, x_2)) = [[1A]] + [[1A]] * x_1 + [[1A]] * x_2 >>> <<< POL(square(x_1)) = [[4A]] + [[1A]] * x_1 >>> <<< POL(A__SQUARE(x_1)) = [[3A]] + [[2A]] * x_1 >>> <<< POL(posrecip(x_1)) = [[-I]] + [[0A]] * x_1 >>> <<< POL(negrecip(x_1)) = [[-I]] + [[0A]] * x_1 >>> <<< POL(rcons(x_1, x_2)) = [[-I]] + [[0A]] * x_1 + [[0A]] * x_2 >>> <<< POL(a__from(x_1)) = [[1A]] + [[1A]] * x_1 >>> <<< POL(a__2ndspos(x_1, x_2)) = [[1A]] + [[1A]] * x_1 + [[1A]] * x_2 >>> <<< POL(a__2ndsneg(x_1, x_2)) = [[1A]] + [[1A]] * x_1 + [[1A]] * x_2 >>> <<< POL(a__pi(x_1)) = [[2A]] + [[2A]] * x_1 >>> <<< POL(a__plus(x_1, x_2)) = [[0A]] + [[0A]] * x_1 + [[0A]] * x_2 >>> <<< POL(a__square(x_1)) = [[4A]] + [[1A]] * x_1 >>> <<< POL(nil) = [[0A]] >>> <<< POL(rnil) = [[1A]] >>> The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented: mark(from(X)) -> a__from(mark(X)) mark(2ndspos(X1, X2)) -> a__2ndspos(mark(X1), mark(X2)) mark(2ndsneg(X1, X2)) -> a__2ndsneg(mark(X1), mark(X2)) mark(pi(X)) -> a__pi(mark(X)) mark(plus(X1, X2)) -> a__plus(mark(X1), mark(X2)) a__plus(0, Y) -> mark(Y) mark(times(X1, X2)) -> a__times(mark(X1), mark(X2)) a__times(s(X), Y) -> a__plus(mark(Y), a__times(mark(X), mark(Y))) mark(square(X)) -> a__square(mark(X)) a__square(X) -> a__times(mark(X), mark(X)) mark(0) -> 0 mark(s(X)) -> s(mark(X)) mark(posrecip(X)) -> posrecip(mark(X)) mark(negrecip(X)) -> negrecip(mark(X)) mark(nil) -> nil mark(cons(X1, X2)) -> cons(mark(X1), X2) mark(rnil) -> rnil mark(rcons(X1, X2)) -> rcons(mark(X1), mark(X2)) a__times(0, Y) -> 0 a__times(X1, X2) -> times(X1, X2) a__from(X) -> from(X) a__2ndspos(0, Z) -> rnil a__2ndspos(X1, X2) -> 2ndspos(X1, X2) a__2ndsneg(0, Z) -> rnil a__2ndsneg(X1, X2) -> 2ndsneg(X1, X2) a__pi(X) -> pi(X) a__plus(X1, X2) -> plus(X1, X2) a__square(X) -> square(X) a__plus(s(X), Y) -> s(a__plus(mark(X), mark(Y))) a__pi(X) -> a__2ndspos(mark(X), a__from(0)) a__from(X) -> cons(mark(X), from(s(X))) a__2ndspos(s(N), cons(X, cons(Y, Z))) -> rcons(posrecip(mark(Y)), a__2ndsneg(mark(N), mark(Z))) a__2ndsneg(s(N), cons(X, cons(Y, Z))) -> rcons(negrecip(mark(Y)), a__2ndspos(mark(N), mark(Z))) ---------------------------------------- (12) Obligation: Q DP problem: The TRS P consists of the following rules: MARK(from(X)) -> A__FROM(mark(X)) A__FROM(X) -> MARK(X) MARK(from(X)) -> MARK(X) MARK(2ndspos(X1, X2)) -> A__2NDSPOS(mark(X1), mark(X2)) A__2NDSPOS(s(N), cons(X, cons(Y, Z))) -> MARK(Y) MARK(2ndspos(X1, X2)) -> MARK(X1) MARK(2ndspos(X1, X2)) -> MARK(X2) MARK(2ndsneg(X1, X2)) -> A__2NDSNEG(mark(X1), mark(X2)) A__2NDSNEG(s(N), cons(X, cons(Y, Z))) -> MARK(Y) MARK(2ndsneg(X1, X2)) -> MARK(X1) MARK(2ndsneg(X1, X2)) -> MARK(X2) MARK(pi(X)) -> A__PI(mark(X)) MARK(plus(X1, X2)) -> A__PLUS(mark(X1), mark(X2)) A__PLUS(0, Y) -> MARK(Y) MARK(plus(X1, X2)) -> MARK(X1) MARK(plus(X1, X2)) -> MARK(X2) MARK(times(X1, X2)) -> A__TIMES(mark(X1), mark(X2)) A__TIMES(s(X), Y) -> A__PLUS(mark(Y), a__times(mark(X), mark(Y))) A__PLUS(s(X), Y) -> A__PLUS(mark(X), mark(Y)) MARK(times(X1, X2)) -> MARK(X1) MARK(times(X1, X2)) -> MARK(X2) MARK(square(X)) -> A__SQUARE(mark(X)) A__SQUARE(X) -> A__TIMES(mark(X), mark(X)) A__TIMES(s(X), Y) -> MARK(Y) MARK(s(X)) -> MARK(X) MARK(posrecip(X)) -> MARK(X) MARK(negrecip(X)) -> MARK(X) MARK(cons(X1, X2)) -> MARK(X1) MARK(rcons(X1, X2)) -> MARK(X1) MARK(rcons(X1, X2)) -> MARK(X2) A__TIMES(s(X), Y) -> A__TIMES(mark(X), mark(Y)) A__TIMES(s(X), Y) -> MARK(X) A__PLUS(s(X), Y) -> MARK(Y) A__2NDSNEG(s(N), cons(X, cons(Y, Z))) -> A__2NDSPOS(mark(N), mark(Z)) A__2NDSPOS(s(N), cons(X, cons(Y, Z))) -> A__2NDSNEG(mark(N), mark(Z)) A__2NDSNEG(s(N), cons(X, cons(Y, Z))) -> MARK(N) A__2NDSNEG(s(N), cons(X, cons(Y, Z))) -> MARK(Z) A__2NDSPOS(s(N), cons(X, cons(Y, Z))) -> MARK(N) A__2NDSPOS(s(N), cons(X, cons(Y, Z))) -> MARK(Z) The TRS R consists of the following rules: a__from(X) -> cons(mark(X), from(s(X))) a__2ndspos(0, Z) -> rnil a__2ndspos(s(N), cons(X, cons(Y, Z))) -> rcons(posrecip(mark(Y)), a__2ndsneg(mark(N), mark(Z))) a__2ndsneg(0, Z) -> rnil a__2ndsneg(s(N), cons(X, cons(Y, Z))) -> rcons(negrecip(mark(Y)), a__2ndspos(mark(N), mark(Z))) a__pi(X) -> a__2ndspos(mark(X), a__from(0)) a__plus(0, Y) -> mark(Y) a__plus(s(X), Y) -> s(a__plus(mark(X), mark(Y))) a__times(0, Y) -> 0 a__times(s(X), Y) -> a__plus(mark(Y), a__times(mark(X), mark(Y))) a__square(X) -> a__times(mark(X), mark(X)) mark(from(X)) -> a__from(mark(X)) mark(2ndspos(X1, X2)) -> a__2ndspos(mark(X1), mark(X2)) mark(2ndsneg(X1, X2)) -> a__2ndsneg(mark(X1), mark(X2)) mark(pi(X)) -> a__pi(mark(X)) mark(plus(X1, X2)) -> a__plus(mark(X1), mark(X2)) mark(times(X1, X2)) -> a__times(mark(X1), mark(X2)) mark(square(X)) -> a__square(mark(X)) mark(0) -> 0 mark(s(X)) -> s(mark(X)) mark(posrecip(X)) -> posrecip(mark(X)) mark(negrecip(X)) -> negrecip(mark(X)) mark(nil) -> nil mark(cons(X1, X2)) -> cons(mark(X1), X2) mark(rnil) -> rnil mark(rcons(X1, X2)) -> rcons(mark(X1), mark(X2)) a__from(X) -> from(X) a__2ndspos(X1, X2) -> 2ndspos(X1, X2) a__2ndsneg(X1, X2) -> 2ndsneg(X1, X2) a__pi(X) -> pi(X) a__plus(X1, X2) -> plus(X1, X2) a__times(X1, X2) -> times(X1, X2) a__square(X) -> square(X) Q is empty. We have to consider all minimal (P,Q,R)-chains. ---------------------------------------- (13) DependencyGraphProof (EQUIVALENT) The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node. ---------------------------------------- (14) Obligation: Q DP problem: The TRS P consists of the following rules: A__FROM(X) -> MARK(X) MARK(from(X)) -> A__FROM(mark(X)) MARK(from(X)) -> MARK(X) MARK(2ndspos(X1, X2)) -> A__2NDSPOS(mark(X1), mark(X2)) A__2NDSPOS(s(N), cons(X, cons(Y, Z))) -> MARK(Y) MARK(2ndspos(X1, X2)) -> MARK(X1) MARK(2ndspos(X1, X2)) -> MARK(X2) MARK(2ndsneg(X1, X2)) -> A__2NDSNEG(mark(X1), mark(X2)) A__2NDSNEG(s(N), cons(X, cons(Y, Z))) -> MARK(Y) MARK(2ndsneg(X1, X2)) -> MARK(X1) MARK(2ndsneg(X1, X2)) -> MARK(X2) MARK(plus(X1, X2)) -> A__PLUS(mark(X1), mark(X2)) A__PLUS(0, Y) -> MARK(Y) MARK(plus(X1, X2)) -> MARK(X1) MARK(plus(X1, X2)) -> MARK(X2) MARK(times(X1, X2)) -> A__TIMES(mark(X1), mark(X2)) A__TIMES(s(X), Y) -> A__PLUS(mark(Y), a__times(mark(X), mark(Y))) A__PLUS(s(X), Y) -> A__PLUS(mark(X), mark(Y)) A__PLUS(s(X), Y) -> MARK(Y) MARK(times(X1, X2)) -> MARK(X1) MARK(times(X1, X2)) -> MARK(X2) MARK(square(X)) -> A__SQUARE(mark(X)) A__SQUARE(X) -> A__TIMES(mark(X), mark(X)) A__TIMES(s(X), Y) -> MARK(Y) MARK(s(X)) -> MARK(X) MARK(posrecip(X)) -> MARK(X) MARK(negrecip(X)) -> MARK(X) MARK(cons(X1, X2)) -> MARK(X1) MARK(rcons(X1, X2)) -> MARK(X1) MARK(rcons(X1, X2)) -> MARK(X2) A__TIMES(s(X), Y) -> A__TIMES(mark(X), mark(Y)) A__TIMES(s(X), Y) -> MARK(X) A__2NDSNEG(s(N), cons(X, cons(Y, Z))) -> A__2NDSPOS(mark(N), mark(Z)) A__2NDSPOS(s(N), cons(X, cons(Y, Z))) -> A__2NDSNEG(mark(N), mark(Z)) A__2NDSNEG(s(N), cons(X, cons(Y, Z))) -> MARK(N) A__2NDSNEG(s(N), cons(X, cons(Y, Z))) -> MARK(Z) A__2NDSPOS(s(N), cons(X, cons(Y, Z))) -> MARK(N) A__2NDSPOS(s(N), cons(X, cons(Y, Z))) -> MARK(Z) The TRS R consists of the following rules: a__from(X) -> cons(mark(X), from(s(X))) a__2ndspos(0, Z) -> rnil a__2ndspos(s(N), cons(X, cons(Y, Z))) -> rcons(posrecip(mark(Y)), a__2ndsneg(mark(N), mark(Z))) a__2ndsneg(0, Z) -> rnil a__2ndsneg(s(N), cons(X, cons(Y, Z))) -> rcons(negrecip(mark(Y)), a__2ndspos(mark(N), mark(Z))) a__pi(X) -> a__2ndspos(mark(X), a__from(0)) a__plus(0, Y) -> mark(Y) a__plus(s(X), Y) -> s(a__plus(mark(X), mark(Y))) a__times(0, Y) -> 0 a__times(s(X), Y) -> a__plus(mark(Y), a__times(mark(X), mark(Y))) a__square(X) -> a__times(mark(X), mark(X)) mark(from(X)) -> a__from(mark(X)) mark(2ndspos(X1, X2)) -> a__2ndspos(mark(X1), mark(X2)) mark(2ndsneg(X1, X2)) -> a__2ndsneg(mark(X1), mark(X2)) mark(pi(X)) -> a__pi(mark(X)) mark(plus(X1, X2)) -> a__plus(mark(X1), mark(X2)) mark(times(X1, X2)) -> a__times(mark(X1), mark(X2)) mark(square(X)) -> a__square(mark(X)) mark(0) -> 0 mark(s(X)) -> s(mark(X)) mark(posrecip(X)) -> posrecip(mark(X)) mark(negrecip(X)) -> negrecip(mark(X)) mark(nil) -> nil mark(cons(X1, X2)) -> cons(mark(X1), X2) mark(rnil) -> rnil mark(rcons(X1, X2)) -> rcons(mark(X1), mark(X2)) a__from(X) -> from(X) a__2ndspos(X1, X2) -> 2ndspos(X1, X2) a__2ndsneg(X1, X2) -> 2ndsneg(X1, X2) a__pi(X) -> pi(X) a__plus(X1, X2) -> plus(X1, X2) a__times(X1, X2) -> times(X1, X2) a__square(X) -> square(X) Q is empty. We have to consider all minimal (P,Q,R)-chains. ---------------------------------------- (15) QDPOrderProof (EQUIVALENT) We use the reduction pair processor [LPAR04,JAR06]. The following pairs can be oriented strictly and are deleted. MARK(2ndspos(X1, X2)) -> MARK(X1) MARK(2ndsneg(X1, X2)) -> MARK(X1) A__2NDSNEG(s(N), cons(X, cons(Y, Z))) -> MARK(N) A__2NDSPOS(s(N), cons(X, cons(Y, Z))) -> MARK(N) The remaining pairs can at least be oriented weakly. Used ordering: Matrix interpretation [MATRO] with arctic natural numbers [ARCTIC]: <<< POL(A__FROM(x_1)) = [[1A]] + [[0A]] * x_1 >>> <<< POL(MARK(x_1)) = [[1A]] + [[0A]] * x_1 >>> <<< POL(from(x_1)) = [[2A]] + [[0A]] * x_1 >>> <<< POL(mark(x_1)) = [[1A]] + [[0A]] * x_1 >>> <<< POL(2ndspos(x_1, x_2)) = [[5A]] + [[4A]] * x_1 + [[0A]] * x_2 >>> <<< POL(A__2NDSPOS(x_1, x_2)) = [[3A]] + [[4A]] * x_1 + [[0A]] * x_2 >>> <<< POL(s(x_1)) = [[2A]] + [[0A]] * x_1 >>> <<< POL(cons(x_1, x_2)) = [[2A]] + [[0A]] * x_1 + [[0A]] * x_2 >>> <<< POL(2ndsneg(x_1, x_2)) = [[5A]] + [[4A]] * x_1 + [[0A]] * x_2 >>> <<< POL(A__2NDSNEG(x_1, x_2)) = [[3A]] + [[4A]] * x_1 + [[0A]] * x_2 >>> <<< POL(plus(x_1, x_2)) = [[0A]] + [[0A]] * x_1 + [[0A]] * x_2 >>> <<< POL(A__PLUS(x_1, x_2)) = [[1A]] + [[-I]] * x_1 + [[0A]] * x_2 >>> <<< POL(0) = [[5A]] >>> <<< POL(times(x_1, x_2)) = [[2A]] + [[0A]] * x_1 + [[0A]] * x_2 >>> <<< POL(A__TIMES(x_1, x_2)) = [[1A]] + [[0A]] * x_1 + [[0A]] * x_2 >>> <<< POL(a__times(x_1, x_2)) = [[2A]] + [[0A]] * x_1 + [[0A]] * x_2 >>> <<< POL(square(x_1)) = [[2A]] + [[0A]] * x_1 >>> <<< POL(A__SQUARE(x_1)) = [[2A]] + [[0A]] * x_1 >>> <<< POL(posrecip(x_1)) = [[-I]] + [[0A]] * x_1 >>> <<< POL(negrecip(x_1)) = [[-I]] + [[0A]] * x_1 >>> <<< POL(rcons(x_1, x_2)) = [[-I]] + [[0A]] * x_1 + [[0A]] * x_2 >>> <<< POL(a__from(x_1)) = [[2A]] + [[0A]] * x_1 >>> <<< POL(a__2ndspos(x_1, x_2)) = [[5A]] + [[4A]] * x_1 + [[0A]] * x_2 >>> <<< POL(a__2ndsneg(x_1, x_2)) = [[5A]] + [[4A]] * x_1 + [[0A]] * x_2 >>> <<< POL(pi(x_1)) = [[5A]] + [[4A]] * x_1 >>> <<< POL(a__pi(x_1)) = [[5A]] + [[4A]] * x_1 >>> <<< POL(a__plus(x_1, x_2)) = [[1A]] + [[0A]] * x_1 + [[0A]] * x_2 >>> <<< POL(a__square(x_1)) = [[2A]] + [[0A]] * x_1 >>> <<< POL(nil) = [[4A]] >>> <<< POL(rnil) = [[5A]] >>> The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented: mark(from(X)) -> a__from(mark(X)) mark(2ndspos(X1, X2)) -> a__2ndspos(mark(X1), mark(X2)) mark(2ndsneg(X1, X2)) -> a__2ndsneg(mark(X1), mark(X2)) mark(pi(X)) -> a__pi(mark(X)) mark(plus(X1, X2)) -> a__plus(mark(X1), mark(X2)) a__plus(0, Y) -> mark(Y) mark(times(X1, X2)) -> a__times(mark(X1), mark(X2)) a__times(s(X), Y) -> a__plus(mark(Y), a__times(mark(X), mark(Y))) mark(square(X)) -> a__square(mark(X)) a__square(X) -> a__times(mark(X), mark(X)) mark(0) -> 0 mark(s(X)) -> s(mark(X)) mark(posrecip(X)) -> posrecip(mark(X)) mark(negrecip(X)) -> negrecip(mark(X)) mark(nil) -> nil mark(cons(X1, X2)) -> cons(mark(X1), X2) mark(rnil) -> rnil mark(rcons(X1, X2)) -> rcons(mark(X1), mark(X2)) a__times(0, Y) -> 0 a__times(X1, X2) -> times(X1, X2) a__from(X) -> from(X) a__2ndspos(0, Z) -> rnil a__2ndspos(X1, X2) -> 2ndspos(X1, X2) a__2ndsneg(0, Z) -> rnil a__2ndsneg(X1, X2) -> 2ndsneg(X1, X2) a__pi(X) -> pi(X) a__plus(X1, X2) -> plus(X1, X2) a__square(X) -> square(X) a__plus(s(X), Y) -> s(a__plus(mark(X), mark(Y))) a__pi(X) -> a__2ndspos(mark(X), a__from(0)) a__from(X) -> cons(mark(X), from(s(X))) a__2ndspos(s(N), cons(X, cons(Y, Z))) -> rcons(posrecip(mark(Y)), a__2ndsneg(mark(N), mark(Z))) a__2ndsneg(s(N), cons(X, cons(Y, Z))) -> rcons(negrecip(mark(Y)), a__2ndspos(mark(N), mark(Z))) ---------------------------------------- (16) Obligation: Q DP problem: The TRS P consists of the following rules: A__FROM(X) -> MARK(X) MARK(from(X)) -> A__FROM(mark(X)) MARK(from(X)) -> MARK(X) MARK(2ndspos(X1, X2)) -> A__2NDSPOS(mark(X1), mark(X2)) A__2NDSPOS(s(N), cons(X, cons(Y, Z))) -> MARK(Y) MARK(2ndspos(X1, X2)) -> MARK(X2) MARK(2ndsneg(X1, X2)) -> A__2NDSNEG(mark(X1), mark(X2)) A__2NDSNEG(s(N), cons(X, cons(Y, Z))) -> MARK(Y) MARK(2ndsneg(X1, X2)) -> MARK(X2) MARK(plus(X1, X2)) -> A__PLUS(mark(X1), mark(X2)) A__PLUS(0, Y) -> MARK(Y) MARK(plus(X1, X2)) -> MARK(X1) MARK(plus(X1, X2)) -> MARK(X2) MARK(times(X1, X2)) -> A__TIMES(mark(X1), mark(X2)) A__TIMES(s(X), Y) -> A__PLUS(mark(Y), a__times(mark(X), mark(Y))) A__PLUS(s(X), Y) -> A__PLUS(mark(X), mark(Y)) A__PLUS(s(X), Y) -> MARK(Y) MARK(times(X1, X2)) -> MARK(X1) MARK(times(X1, X2)) -> MARK(X2) MARK(square(X)) -> A__SQUARE(mark(X)) A__SQUARE(X) -> A__TIMES(mark(X), mark(X)) A__TIMES(s(X), Y) -> MARK(Y) MARK(s(X)) -> MARK(X) MARK(posrecip(X)) -> MARK(X) MARK(negrecip(X)) -> MARK(X) MARK(cons(X1, X2)) -> MARK(X1) MARK(rcons(X1, X2)) -> MARK(X1) MARK(rcons(X1, X2)) -> MARK(X2) A__TIMES(s(X), Y) -> A__TIMES(mark(X), mark(Y)) A__TIMES(s(X), Y) -> MARK(X) A__2NDSNEG(s(N), cons(X, cons(Y, Z))) -> A__2NDSPOS(mark(N), mark(Z)) A__2NDSPOS(s(N), cons(X, cons(Y, Z))) -> A__2NDSNEG(mark(N), mark(Z)) A__2NDSNEG(s(N), cons(X, cons(Y, Z))) -> MARK(Z) A__2NDSPOS(s(N), cons(X, cons(Y, Z))) -> MARK(Z) The TRS R consists of the following rules: a__from(X) -> cons(mark(X), from(s(X))) a__2ndspos(0, Z) -> rnil a__2ndspos(s(N), cons(X, cons(Y, Z))) -> rcons(posrecip(mark(Y)), a__2ndsneg(mark(N), mark(Z))) a__2ndsneg(0, Z) -> rnil a__2ndsneg(s(N), cons(X, cons(Y, Z))) -> rcons(negrecip(mark(Y)), a__2ndspos(mark(N), mark(Z))) a__pi(X) -> a__2ndspos(mark(X), a__from(0)) a__plus(0, Y) -> mark(Y) a__plus(s(X), Y) -> s(a__plus(mark(X), mark(Y))) a__times(0, Y) -> 0 a__times(s(X), Y) -> a__plus(mark(Y), a__times(mark(X), mark(Y))) a__square(X) -> a__times(mark(X), mark(X)) mark(from(X)) -> a__from(mark(X)) mark(2ndspos(X1, X2)) -> a__2ndspos(mark(X1), mark(X2)) mark(2ndsneg(X1, X2)) -> a__2ndsneg(mark(X1), mark(X2)) mark(pi(X)) -> a__pi(mark(X)) mark(plus(X1, X2)) -> a__plus(mark(X1), mark(X2)) mark(times(X1, X2)) -> a__times(mark(X1), mark(X2)) mark(square(X)) -> a__square(mark(X)) mark(0) -> 0 mark(s(X)) -> s(mark(X)) mark(posrecip(X)) -> posrecip(mark(X)) mark(negrecip(X)) -> negrecip(mark(X)) mark(nil) -> nil mark(cons(X1, X2)) -> cons(mark(X1), X2) mark(rnil) -> rnil mark(rcons(X1, X2)) -> rcons(mark(X1), mark(X2)) a__from(X) -> from(X) a__2ndspos(X1, X2) -> 2ndspos(X1, X2) a__2ndsneg(X1, X2) -> 2ndsneg(X1, X2) a__pi(X) -> pi(X) a__plus(X1, X2) -> plus(X1, X2) a__times(X1, X2) -> times(X1, X2) a__square(X) -> square(X) Q is empty. We have to consider all minimal (P,Q,R)-chains. ---------------------------------------- (17) QDPOrderProof (EQUIVALENT) We use the reduction pair processor [LPAR04,JAR06]. The following pairs can be oriented strictly and are deleted. MARK(from(X)) -> MARK(X) A__2NDSPOS(s(N), cons(X, cons(Y, Z))) -> MARK(Y) A__2NDSNEG(s(N), cons(X, cons(Y, Z))) -> MARK(Y) MARK(square(X)) -> A__SQUARE(mark(X)) MARK(cons(X1, X2)) -> MARK(X1) The remaining pairs can at least be oriented weakly. Used ordering: Matrix interpretation [MATRO] with arctic natural numbers [ARCTIC]: <<< POL(A__FROM(x_1)) = [[4A]] + [[3A]] * x_1 >>> <<< POL(MARK(x_1)) = [[4A]] + [[2A]] * x_1 >>> <<< POL(from(x_1)) = [[5A]] + [[1A]] * x_1 >>> <<< POL(mark(x_1)) = [[-I]] + [[0A]] * x_1 >>> <<< POL(2ndspos(x_1, x_2)) = [[4A]] + [[4A]] * x_1 + [[0A]] * x_2 >>> <<< POL(A__2NDSPOS(x_1, x_2)) = [[5A]] + [[2A]] * x_1 + [[2A]] * x_2 >>> <<< POL(s(x_1)) = [[0A]] + [[0A]] * x_1 >>> <<< POL(cons(x_1, x_2)) = [[3A]] + [[1A]] * x_1 + [[0A]] * x_2 >>> <<< POL(2ndsneg(x_1, x_2)) = [[0A]] + [[4A]] * x_1 + [[0A]] * x_2 >>> <<< POL(A__2NDSNEG(x_1, x_2)) = [[4A]] + [[2A]] * x_1 + [[2A]] * x_2 >>> <<< POL(plus(x_1, x_2)) = [[0A]] + [[0A]] * x_1 + [[0A]] * x_2 >>> <<< POL(A__PLUS(x_1, x_2)) = [[4A]] + [[-I]] * x_1 + [[2A]] * x_2 >>> <<< POL(0) = [[2A]] >>> <<< POL(times(x_1, x_2)) = [[1A]] + [[0A]] * x_1 + [[0A]] * x_2 >>> <<< POL(A__TIMES(x_1, x_2)) = [[4A]] + [[2A]] * x_1 + [[2A]] * x_2 >>> <<< POL(a__times(x_1, x_2)) = [[1A]] + [[0A]] * x_1 + [[0A]] * x_2 >>> <<< POL(square(x_1)) = [[3A]] + [[2A]] * x_1 >>> <<< POL(A__SQUARE(x_1)) = [[4A]] + [[3A]] * x_1 >>> <<< POL(posrecip(x_1)) = [[3A]] + [[0A]] * x_1 >>> <<< POL(negrecip(x_1)) = [[-I]] + [[1A]] * x_1 >>> <<< POL(rcons(x_1, x_2)) = [[-I]] + [[0A]] * x_1 + [[0A]] * x_2 >>> <<< POL(a__from(x_1)) = [[5A]] + [[1A]] * x_1 >>> <<< POL(a__2ndspos(x_1, x_2)) = [[4A]] + [[4A]] * x_1 + [[0A]] * x_2 >>> <<< POL(a__2ndsneg(x_1, x_2)) = [[0A]] + [[4A]] * x_1 + [[0A]] * x_2 >>> <<< POL(pi(x_1)) = [[5A]] + [[5A]] * x_1 >>> <<< POL(a__pi(x_1)) = [[5A]] + [[5A]] * x_1 >>> <<< POL(a__plus(x_1, x_2)) = [[0A]] + [[0A]] * x_1 + [[0A]] * x_2 >>> <<< POL(a__square(x_1)) = [[3A]] + [[2A]] * x_1 >>> <<< POL(nil) = [[3A]] >>> <<< POL(rnil) = [[5A]] >>> The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented: mark(from(X)) -> a__from(mark(X)) mark(2ndspos(X1, X2)) -> a__2ndspos(mark(X1), mark(X2)) mark(2ndsneg(X1, X2)) -> a__2ndsneg(mark(X1), mark(X2)) mark(pi(X)) -> a__pi(mark(X)) mark(plus(X1, X2)) -> a__plus(mark(X1), mark(X2)) a__plus(0, Y) -> mark(Y) mark(times(X1, X2)) -> a__times(mark(X1), mark(X2)) a__times(s(X), Y) -> a__plus(mark(Y), a__times(mark(X), mark(Y))) mark(square(X)) -> a__square(mark(X)) a__square(X) -> a__times(mark(X), mark(X)) mark(0) -> 0 mark(s(X)) -> s(mark(X)) mark(posrecip(X)) -> posrecip(mark(X)) mark(negrecip(X)) -> negrecip(mark(X)) mark(nil) -> nil mark(cons(X1, X2)) -> cons(mark(X1), X2) mark(rnil) -> rnil mark(rcons(X1, X2)) -> rcons(mark(X1), mark(X2)) a__times(0, Y) -> 0 a__times(X1, X2) -> times(X1, X2) a__from(X) -> from(X) a__2ndspos(0, Z) -> rnil a__2ndspos(X1, X2) -> 2ndspos(X1, X2) a__2ndsneg(0, Z) -> rnil a__2ndsneg(X1, X2) -> 2ndsneg(X1, X2) a__pi(X) -> pi(X) a__plus(X1, X2) -> plus(X1, X2) a__square(X) -> square(X) a__plus(s(X), Y) -> s(a__plus(mark(X), mark(Y))) a__pi(X) -> a__2ndspos(mark(X), a__from(0)) a__from(X) -> cons(mark(X), from(s(X))) a__2ndspos(s(N), cons(X, cons(Y, Z))) -> rcons(posrecip(mark(Y)), a__2ndsneg(mark(N), mark(Z))) a__2ndsneg(s(N), cons(X, cons(Y, Z))) -> rcons(negrecip(mark(Y)), a__2ndspos(mark(N), mark(Z))) ---------------------------------------- (18) Obligation: Q DP problem: The TRS P consists of the following rules: A__FROM(X) -> MARK(X) MARK(from(X)) -> A__FROM(mark(X)) MARK(2ndspos(X1, X2)) -> A__2NDSPOS(mark(X1), mark(X2)) MARK(2ndspos(X1, X2)) -> MARK(X2) MARK(2ndsneg(X1, X2)) -> A__2NDSNEG(mark(X1), mark(X2)) MARK(2ndsneg(X1, X2)) -> MARK(X2) MARK(plus(X1, X2)) -> A__PLUS(mark(X1), mark(X2)) A__PLUS(0, Y) -> MARK(Y) MARK(plus(X1, X2)) -> MARK(X1) MARK(plus(X1, X2)) -> MARK(X2) MARK(times(X1, X2)) -> A__TIMES(mark(X1), mark(X2)) A__TIMES(s(X), Y) -> A__PLUS(mark(Y), a__times(mark(X), mark(Y))) A__PLUS(s(X), Y) -> A__PLUS(mark(X), mark(Y)) A__PLUS(s(X), Y) -> MARK(Y) MARK(times(X1, X2)) -> MARK(X1) MARK(times(X1, X2)) -> MARK(X2) A__SQUARE(X) -> A__TIMES(mark(X), mark(X)) A__TIMES(s(X), Y) -> MARK(Y) MARK(s(X)) -> MARK(X) MARK(posrecip(X)) -> MARK(X) MARK(negrecip(X)) -> MARK(X) MARK(rcons(X1, X2)) -> MARK(X1) MARK(rcons(X1, X2)) -> MARK(X2) A__TIMES(s(X), Y) -> A__TIMES(mark(X), mark(Y)) A__TIMES(s(X), Y) -> MARK(X) A__2NDSNEG(s(N), cons(X, cons(Y, Z))) -> A__2NDSPOS(mark(N), mark(Z)) A__2NDSPOS(s(N), cons(X, cons(Y, Z))) -> A__2NDSNEG(mark(N), mark(Z)) A__2NDSNEG(s(N), cons(X, cons(Y, Z))) -> MARK(Z) A__2NDSPOS(s(N), cons(X, cons(Y, Z))) -> MARK(Z) The TRS R consists of the following rules: a__from(X) -> cons(mark(X), from(s(X))) a__2ndspos(0, Z) -> rnil a__2ndspos(s(N), cons(X, cons(Y, Z))) -> rcons(posrecip(mark(Y)), a__2ndsneg(mark(N), mark(Z))) a__2ndsneg(0, Z) -> rnil a__2ndsneg(s(N), cons(X, cons(Y, Z))) -> rcons(negrecip(mark(Y)), a__2ndspos(mark(N), mark(Z))) a__pi(X) -> a__2ndspos(mark(X), a__from(0)) a__plus(0, Y) -> mark(Y) a__plus(s(X), Y) -> s(a__plus(mark(X), mark(Y))) a__times(0, Y) -> 0 a__times(s(X), Y) -> a__plus(mark(Y), a__times(mark(X), mark(Y))) a__square(X) -> a__times(mark(X), mark(X)) mark(from(X)) -> a__from(mark(X)) mark(2ndspos(X1, X2)) -> a__2ndspos(mark(X1), mark(X2)) mark(2ndsneg(X1, X2)) -> a__2ndsneg(mark(X1), mark(X2)) mark(pi(X)) -> a__pi(mark(X)) mark(plus(X1, X2)) -> a__plus(mark(X1), mark(X2)) mark(times(X1, X2)) -> a__times(mark(X1), mark(X2)) mark(square(X)) -> a__square(mark(X)) mark(0) -> 0 mark(s(X)) -> s(mark(X)) mark(posrecip(X)) -> posrecip(mark(X)) mark(negrecip(X)) -> negrecip(mark(X)) mark(nil) -> nil mark(cons(X1, X2)) -> cons(mark(X1), X2) mark(rnil) -> rnil mark(rcons(X1, X2)) -> rcons(mark(X1), mark(X2)) a__from(X) -> from(X) a__2ndspos(X1, X2) -> 2ndspos(X1, X2) a__2ndsneg(X1, X2) -> 2ndsneg(X1, X2) a__pi(X) -> pi(X) a__plus(X1, X2) -> plus(X1, X2) a__times(X1, X2) -> times(X1, X2) a__square(X) -> square(X) Q is empty. We have to consider all minimal (P,Q,R)-chains. ---------------------------------------- (19) DependencyGraphProof (EQUIVALENT) The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node. ---------------------------------------- (20) Obligation: Q DP problem: The TRS P consists of the following rules: MARK(from(X)) -> A__FROM(mark(X)) A__FROM(X) -> MARK(X) MARK(2ndspos(X1, X2)) -> A__2NDSPOS(mark(X1), mark(X2)) A__2NDSPOS(s(N), cons(X, cons(Y, Z))) -> A__2NDSNEG(mark(N), mark(Z)) A__2NDSNEG(s(N), cons(X, cons(Y, Z))) -> A__2NDSPOS(mark(N), mark(Z)) A__2NDSPOS(s(N), cons(X, cons(Y, Z))) -> MARK(Z) MARK(2ndspos(X1, X2)) -> MARK(X2) MARK(2ndsneg(X1, X2)) -> A__2NDSNEG(mark(X1), mark(X2)) A__2NDSNEG(s(N), cons(X, cons(Y, Z))) -> MARK(Z) MARK(2ndsneg(X1, X2)) -> MARK(X2) MARK(plus(X1, X2)) -> A__PLUS(mark(X1), mark(X2)) A__PLUS(0, Y) -> MARK(Y) MARK(plus(X1, X2)) -> MARK(X1) MARK(plus(X1, X2)) -> MARK(X2) MARK(times(X1, X2)) -> A__TIMES(mark(X1), mark(X2)) A__TIMES(s(X), Y) -> A__PLUS(mark(Y), a__times(mark(X), mark(Y))) A__PLUS(s(X), Y) -> A__PLUS(mark(X), mark(Y)) A__PLUS(s(X), Y) -> MARK(Y) MARK(times(X1, X2)) -> MARK(X1) MARK(times(X1, X2)) -> MARK(X2) MARK(s(X)) -> MARK(X) MARK(posrecip(X)) -> MARK(X) MARK(negrecip(X)) -> MARK(X) MARK(rcons(X1, X2)) -> MARK(X1) MARK(rcons(X1, X2)) -> MARK(X2) A__TIMES(s(X), Y) -> MARK(Y) A__TIMES(s(X), Y) -> A__TIMES(mark(X), mark(Y)) A__TIMES(s(X), Y) -> MARK(X) The TRS R consists of the following rules: a__from(X) -> cons(mark(X), from(s(X))) a__2ndspos(0, Z) -> rnil a__2ndspos(s(N), cons(X, cons(Y, Z))) -> rcons(posrecip(mark(Y)), a__2ndsneg(mark(N), mark(Z))) a__2ndsneg(0, Z) -> rnil a__2ndsneg(s(N), cons(X, cons(Y, Z))) -> rcons(negrecip(mark(Y)), a__2ndspos(mark(N), mark(Z))) a__pi(X) -> a__2ndspos(mark(X), a__from(0)) a__plus(0, Y) -> mark(Y) a__plus(s(X), Y) -> s(a__plus(mark(X), mark(Y))) a__times(0, Y) -> 0 a__times(s(X), Y) -> a__plus(mark(Y), a__times(mark(X), mark(Y))) a__square(X) -> a__times(mark(X), mark(X)) mark(from(X)) -> a__from(mark(X)) mark(2ndspos(X1, X2)) -> a__2ndspos(mark(X1), mark(X2)) mark(2ndsneg(X1, X2)) -> a__2ndsneg(mark(X1), mark(X2)) mark(pi(X)) -> a__pi(mark(X)) mark(plus(X1, X2)) -> a__plus(mark(X1), mark(X2)) mark(times(X1, X2)) -> a__times(mark(X1), mark(X2)) mark(square(X)) -> a__square(mark(X)) mark(0) -> 0 mark(s(X)) -> s(mark(X)) mark(posrecip(X)) -> posrecip(mark(X)) mark(negrecip(X)) -> negrecip(mark(X)) mark(nil) -> nil mark(cons(X1, X2)) -> cons(mark(X1), X2) mark(rnil) -> rnil mark(rcons(X1, X2)) -> rcons(mark(X1), mark(X2)) a__from(X) -> from(X) a__2ndspos(X1, X2) -> 2ndspos(X1, X2) a__2ndsneg(X1, X2) -> 2ndsneg(X1, X2) a__pi(X) -> pi(X) a__plus(X1, X2) -> plus(X1, X2) a__times(X1, X2) -> times(X1, X2) a__square(X) -> square(X) Q is empty. We have to consider all minimal (P,Q,R)-chains. ---------------------------------------- (21) QDPOrderProof (EQUIVALENT) We use the reduction pair processor [LPAR04,JAR06]. The following pairs can be oriented strictly and are deleted. MARK(from(X)) -> A__FROM(mark(X)) The remaining pairs can at least be oriented weakly. Used ordering: Matrix interpretation [MATRO] with arctic natural numbers [ARCTIC]: <<< POL(MARK(x_1)) = [[5A]] + [[1A]] * x_1 >>> <<< POL(from(x_1)) = [[5A]] + [[1A]] * x_1 >>> <<< POL(A__FROM(x_1)) = [[5A]] + [[1A]] * x_1 >>> <<< POL(mark(x_1)) = [[-I]] + [[0A]] * x_1 >>> <<< POL(2ndspos(x_1, x_2)) = [[-I]] + [[0A]] * x_1 + [[0A]] * x_2 >>> <<< POL(A__2NDSPOS(x_1, x_2)) = [[5A]] + [[-I]] * x_1 + [[1A]] * x_2 >>> <<< POL(s(x_1)) = [[-I]] + [[0A]] * x_1 >>> <<< POL(cons(x_1, x_2)) = [[-I]] + [[1A]] * x_1 + [[0A]] * x_2 >>> <<< POL(A__2NDSNEG(x_1, x_2)) = [[5A]] + [[-I]] * x_1 + [[1A]] * x_2 >>> <<< POL(2ndsneg(x_1, x_2)) = [[-I]] + [[0A]] * x_1 + [[0A]] * x_2 >>> <<< POL(plus(x_1, x_2)) = [[4A]] + [[1A]] * x_1 + [[0A]] * x_2 >>> <<< POL(A__PLUS(x_1, x_2)) = [[5A]] + [[2A]] * x_1 + [[1A]] * x_2 >>> <<< POL(0) = [[1A]] >>> <<< POL(times(x_1, x_2)) = [[4A]] + [[0A]] * x_1 + [[1A]] * x_2 >>> <<< POL(A__TIMES(x_1, x_2)) = [[5A]] + [[1A]] * x_1 + [[2A]] * x_2 >>> <<< POL(a__times(x_1, x_2)) = [[4A]] + [[0A]] * x_1 + [[1A]] * x_2 >>> <<< POL(posrecip(x_1)) = [[-I]] + [[0A]] * x_1 >>> <<< POL(negrecip(x_1)) = [[-I]] + [[0A]] * x_1 >>> <<< POL(rcons(x_1, x_2)) = [[-I]] + [[1A]] * x_1 + [[0A]] * x_2 >>> <<< POL(a__from(x_1)) = [[5A]] + [[1A]] * x_1 >>> <<< POL(a__2ndspos(x_1, x_2)) = [[-I]] + [[0A]] * x_1 + [[0A]] * x_2 >>> <<< POL(a__2ndsneg(x_1, x_2)) = [[-I]] + [[0A]] * x_1 + [[0A]] * x_2 >>> <<< POL(pi(x_1)) = [[5A]] + [[4A]] * x_1 >>> <<< POL(a__pi(x_1)) = [[5A]] + [[4A]] * x_1 >>> <<< POL(a__plus(x_1, x_2)) = [[4A]] + [[1A]] * x_1 + [[0A]] * x_2 >>> <<< POL(square(x_1)) = [[4A]] + [[5A]] * x_1 >>> <<< POL(a__square(x_1)) = [[4A]] + [[5A]] * x_1 >>> <<< POL(nil) = [[1A]] >>> <<< POL(rnil) = [[0A]] >>> The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented: mark(from(X)) -> a__from(mark(X)) mark(2ndspos(X1, X2)) -> a__2ndspos(mark(X1), mark(X2)) mark(2ndsneg(X1, X2)) -> a__2ndsneg(mark(X1), mark(X2)) mark(pi(X)) -> a__pi(mark(X)) mark(plus(X1, X2)) -> a__plus(mark(X1), mark(X2)) a__plus(0, Y) -> mark(Y) mark(times(X1, X2)) -> a__times(mark(X1), mark(X2)) a__times(s(X), Y) -> a__plus(mark(Y), a__times(mark(X), mark(Y))) mark(square(X)) -> a__square(mark(X)) a__square(X) -> a__times(mark(X), mark(X)) mark(0) -> 0 mark(s(X)) -> s(mark(X)) mark(posrecip(X)) -> posrecip(mark(X)) mark(negrecip(X)) -> negrecip(mark(X)) mark(nil) -> nil mark(cons(X1, X2)) -> cons(mark(X1), X2) mark(rnil) -> rnil mark(rcons(X1, X2)) -> rcons(mark(X1), mark(X2)) a__times(0, Y) -> 0 a__times(X1, X2) -> times(X1, X2) a__from(X) -> from(X) a__2ndspos(0, Z) -> rnil a__2ndspos(X1, X2) -> 2ndspos(X1, X2) a__2ndsneg(0, Z) -> rnil a__2ndsneg(X1, X2) -> 2ndsneg(X1, X2) a__pi(X) -> pi(X) a__plus(X1, X2) -> plus(X1, X2) a__square(X) -> square(X) a__plus(s(X), Y) -> s(a__plus(mark(X), mark(Y))) a__pi(X) -> a__2ndspos(mark(X), a__from(0)) a__from(X) -> cons(mark(X), from(s(X))) a__2ndspos(s(N), cons(X, cons(Y, Z))) -> rcons(posrecip(mark(Y)), a__2ndsneg(mark(N), mark(Z))) a__2ndsneg(s(N), cons(X, cons(Y, Z))) -> rcons(negrecip(mark(Y)), a__2ndspos(mark(N), mark(Z))) ---------------------------------------- (22) Obligation: Q DP problem: The TRS P consists of the following rules: A__FROM(X) -> MARK(X) MARK(2ndspos(X1, X2)) -> A__2NDSPOS(mark(X1), mark(X2)) A__2NDSPOS(s(N), cons(X, cons(Y, Z))) -> A__2NDSNEG(mark(N), mark(Z)) A__2NDSNEG(s(N), cons(X, cons(Y, Z))) -> A__2NDSPOS(mark(N), mark(Z)) A__2NDSPOS(s(N), cons(X, cons(Y, Z))) -> MARK(Z) MARK(2ndspos(X1, X2)) -> MARK(X2) MARK(2ndsneg(X1, X2)) -> A__2NDSNEG(mark(X1), mark(X2)) A__2NDSNEG(s(N), cons(X, cons(Y, Z))) -> MARK(Z) MARK(2ndsneg(X1, X2)) -> MARK(X2) MARK(plus(X1, X2)) -> A__PLUS(mark(X1), mark(X2)) A__PLUS(0, Y) -> MARK(Y) MARK(plus(X1, X2)) -> MARK(X1) MARK(plus(X1, X2)) -> MARK(X2) MARK(times(X1, X2)) -> A__TIMES(mark(X1), mark(X2)) A__TIMES(s(X), Y) -> A__PLUS(mark(Y), a__times(mark(X), mark(Y))) A__PLUS(s(X), Y) -> A__PLUS(mark(X), mark(Y)) A__PLUS(s(X), Y) -> MARK(Y) MARK(times(X1, X2)) -> MARK(X1) MARK(times(X1, X2)) -> MARK(X2) MARK(s(X)) -> MARK(X) MARK(posrecip(X)) -> MARK(X) MARK(negrecip(X)) -> MARK(X) MARK(rcons(X1, X2)) -> MARK(X1) MARK(rcons(X1, X2)) -> MARK(X2) A__TIMES(s(X), Y) -> MARK(Y) A__TIMES(s(X), Y) -> A__TIMES(mark(X), mark(Y)) A__TIMES(s(X), Y) -> MARK(X) The TRS R consists of the following rules: a__from(X) -> cons(mark(X), from(s(X))) a__2ndspos(0, Z) -> rnil a__2ndspos(s(N), cons(X, cons(Y, Z))) -> rcons(posrecip(mark(Y)), a__2ndsneg(mark(N), mark(Z))) a__2ndsneg(0, Z) -> rnil a__2ndsneg(s(N), cons(X, cons(Y, Z))) -> rcons(negrecip(mark(Y)), a__2ndspos(mark(N), mark(Z))) a__pi(X) -> a__2ndspos(mark(X), a__from(0)) a__plus(0, Y) -> mark(Y) a__plus(s(X), Y) -> s(a__plus(mark(X), mark(Y))) a__times(0, Y) -> 0 a__times(s(X), Y) -> a__plus(mark(Y), a__times(mark(X), mark(Y))) a__square(X) -> a__times(mark(X), mark(X)) mark(from(X)) -> a__from(mark(X)) mark(2ndspos(X1, X2)) -> a__2ndspos(mark(X1), mark(X2)) mark(2ndsneg(X1, X2)) -> a__2ndsneg(mark(X1), mark(X2)) mark(pi(X)) -> a__pi(mark(X)) mark(plus(X1, X2)) -> a__plus(mark(X1), mark(X2)) mark(times(X1, X2)) -> a__times(mark(X1), mark(X2)) mark(square(X)) -> a__square(mark(X)) mark(0) -> 0 mark(s(X)) -> s(mark(X)) mark(posrecip(X)) -> posrecip(mark(X)) mark(negrecip(X)) -> negrecip(mark(X)) mark(nil) -> nil mark(cons(X1, X2)) -> cons(mark(X1), X2) mark(rnil) -> rnil mark(rcons(X1, X2)) -> rcons(mark(X1), mark(X2)) a__from(X) -> from(X) a__2ndspos(X1, X2) -> 2ndspos(X1, X2) a__2ndsneg(X1, X2) -> 2ndsneg(X1, X2) a__pi(X) -> pi(X) a__plus(X1, X2) -> plus(X1, X2) a__times(X1, X2) -> times(X1, X2) a__square(X) -> square(X) Q is empty. We have to consider all minimal (P,Q,R)-chains. ---------------------------------------- (23) DependencyGraphProof (EQUIVALENT) The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node. ---------------------------------------- (24) Obligation: Q DP problem: The TRS P consists of the following rules: A__2NDSPOS(s(N), cons(X, cons(Y, Z))) -> A__2NDSNEG(mark(N), mark(Z)) A__2NDSNEG(s(N), cons(X, cons(Y, Z))) -> A__2NDSPOS(mark(N), mark(Z)) A__2NDSPOS(s(N), cons(X, cons(Y, Z))) -> MARK(Z) MARK(2ndspos(X1, X2)) -> A__2NDSPOS(mark(X1), mark(X2)) MARK(2ndspos(X1, X2)) -> MARK(X2) MARK(2ndsneg(X1, X2)) -> A__2NDSNEG(mark(X1), mark(X2)) A__2NDSNEG(s(N), cons(X, cons(Y, Z))) -> MARK(Z) MARK(2ndsneg(X1, X2)) -> MARK(X2) MARK(plus(X1, X2)) -> A__PLUS(mark(X1), mark(X2)) A__PLUS(0, Y) -> MARK(Y) MARK(plus(X1, X2)) -> MARK(X1) MARK(plus(X1, X2)) -> MARK(X2) MARK(times(X1, X2)) -> A__TIMES(mark(X1), mark(X2)) A__TIMES(s(X), Y) -> A__PLUS(mark(Y), a__times(mark(X), mark(Y))) A__PLUS(s(X), Y) -> A__PLUS(mark(X), mark(Y)) A__PLUS(s(X), Y) -> MARK(Y) MARK(times(X1, X2)) -> MARK(X1) MARK(times(X1, X2)) -> MARK(X2) MARK(s(X)) -> MARK(X) MARK(posrecip(X)) -> MARK(X) MARK(negrecip(X)) -> MARK(X) MARK(rcons(X1, X2)) -> MARK(X1) MARK(rcons(X1, X2)) -> MARK(X2) A__TIMES(s(X), Y) -> MARK(Y) A__TIMES(s(X), Y) -> A__TIMES(mark(X), mark(Y)) A__TIMES(s(X), Y) -> MARK(X) The TRS R consists of the following rules: a__from(X) -> cons(mark(X), from(s(X))) a__2ndspos(0, Z) -> rnil a__2ndspos(s(N), cons(X, cons(Y, Z))) -> rcons(posrecip(mark(Y)), a__2ndsneg(mark(N), mark(Z))) a__2ndsneg(0, Z) -> rnil a__2ndsneg(s(N), cons(X, cons(Y, Z))) -> rcons(negrecip(mark(Y)), a__2ndspos(mark(N), mark(Z))) a__pi(X) -> a__2ndspos(mark(X), a__from(0)) a__plus(0, Y) -> mark(Y) a__plus(s(X), Y) -> s(a__plus(mark(X), mark(Y))) a__times(0, Y) -> 0 a__times(s(X), Y) -> a__plus(mark(Y), a__times(mark(X), mark(Y))) a__square(X) -> a__times(mark(X), mark(X)) mark(from(X)) -> a__from(mark(X)) mark(2ndspos(X1, X2)) -> a__2ndspos(mark(X1), mark(X2)) mark(2ndsneg(X1, X2)) -> a__2ndsneg(mark(X1), mark(X2)) mark(pi(X)) -> a__pi(mark(X)) mark(plus(X1, X2)) -> a__plus(mark(X1), mark(X2)) mark(times(X1, X2)) -> a__times(mark(X1), mark(X2)) mark(square(X)) -> a__square(mark(X)) mark(0) -> 0 mark(s(X)) -> s(mark(X)) mark(posrecip(X)) -> posrecip(mark(X)) mark(negrecip(X)) -> negrecip(mark(X)) mark(nil) -> nil mark(cons(X1, X2)) -> cons(mark(X1), X2) mark(rnil) -> rnil mark(rcons(X1, X2)) -> rcons(mark(X1), mark(X2)) a__from(X) -> from(X) a__2ndspos(X1, X2) -> 2ndspos(X1, X2) a__2ndsneg(X1, X2) -> 2ndsneg(X1, X2) a__pi(X) -> pi(X) a__plus(X1, X2) -> plus(X1, X2) a__times(X1, X2) -> times(X1, X2) a__square(X) -> square(X) Q is empty. We have to consider all minimal (P,Q,R)-chains. ---------------------------------------- (25) QDPOrderProof (EQUIVALENT) We use the reduction pair processor [LPAR04,JAR06]. The following pairs can be oriented strictly and are deleted. MARK(2ndspos(X1, X2)) -> A__2NDSPOS(mark(X1), mark(X2)) MARK(2ndspos(X1, X2)) -> MARK(X2) MARK(2ndsneg(X1, X2)) -> A__2NDSNEG(mark(X1), mark(X2)) MARK(2ndsneg(X1, X2)) -> MARK(X2) MARK(plus(X1, X2)) -> MARK(X1) MARK(times(X1, X2)) -> MARK(X1) MARK(times(X1, X2)) -> MARK(X2) MARK(rcons(X1, X2)) -> MARK(X1) A__TIMES(s(X), Y) -> MARK(Y) A__TIMES(s(X), Y) -> MARK(X) The remaining pairs can at least be oriented weakly. Used ordering: Matrix interpretation [MATRO] with arctic natural numbers [ARCTIC]: <<< POL(A__2NDSPOS(x_1, x_2)) = [[3A]] + [[0A]] * x_1 + [[4A]] * x_2 >>> <<< POL(s(x_1)) = [[-I]] + [[0A]] * x_1 >>> <<< POL(cons(x_1, x_2)) = [[-I]] + [[0A]] * x_1 + [[0A]] * x_2 >>> <<< POL(A__2NDSNEG(x_1, x_2)) = [[3A]] + [[0A]] * x_1 + [[4A]] * x_2 >>> <<< POL(mark(x_1)) = [[-I]] + [[0A]] * x_1 >>> <<< POL(MARK(x_1)) = [[3A]] + [[4A]] * x_1 >>> <<< POL(2ndspos(x_1, x_2)) = [[2A]] + [[0A]] * x_1 + [[5A]] * x_2 >>> <<< POL(2ndsneg(x_1, x_2)) = [[2A]] + [[0A]] * x_1 + [[5A]] * x_2 >>> <<< POL(plus(x_1, x_2)) = [[0A]] + [[1A]] * x_1 + [[0A]] * x_2 >>> <<< POL(A__PLUS(x_1, x_2)) = [[3A]] + [[-I]] * x_1 + [[4A]] * x_2 >>> <<< POL(0) = [[0A]] >>> <<< POL(times(x_1, x_2)) = [[1A]] + [[1A]] * x_1 + [[1A]] * x_2 >>> <<< POL(A__TIMES(x_1, x_2)) = [[5A]] + [[5A]] * x_1 + [[5A]] * x_2 >>> <<< POL(a__times(x_1, x_2)) = [[1A]] + [[1A]] * x_1 + [[1A]] * x_2 >>> <<< POL(posrecip(x_1)) = [[-I]] + [[4A]] * x_1 >>> <<< POL(negrecip(x_1)) = [[-I]] + [[4A]] * x_1 >>> <<< POL(rcons(x_1, x_2)) = [[1A]] + [[1A]] * x_1 + [[0A]] * x_2 >>> <<< POL(from(x_1)) = [[-I]] + [[0A]] * x_1 >>> <<< POL(a__from(x_1)) = [[-I]] + [[0A]] * x_1 >>> <<< POL(a__2ndspos(x_1, x_2)) = [[2A]] + [[0A]] * x_1 + [[5A]] * x_2 >>> <<< POL(a__2ndsneg(x_1, x_2)) = [[2A]] + [[0A]] * x_1 + [[5A]] * x_2 >>> <<< POL(pi(x_1)) = [[5A]] + [[5A]] * x_1 >>> <<< POL(a__pi(x_1)) = [[5A]] + [[5A]] * x_1 >>> <<< POL(a__plus(x_1, x_2)) = [[0A]] + [[1A]] * x_1 + [[0A]] * x_2 >>> <<< POL(square(x_1)) = [[3A]] + [[3A]] * x_1 >>> <<< POL(a__square(x_1)) = [[3A]] + [[3A]] * x_1 >>> <<< POL(nil) = [[2A]] >>> <<< POL(rnil) = [[0A]] >>> The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented: mark(from(X)) -> a__from(mark(X)) mark(2ndspos(X1, X2)) -> a__2ndspos(mark(X1), mark(X2)) mark(2ndsneg(X1, X2)) -> a__2ndsneg(mark(X1), mark(X2)) mark(pi(X)) -> a__pi(mark(X)) mark(plus(X1, X2)) -> a__plus(mark(X1), mark(X2)) a__plus(0, Y) -> mark(Y) mark(times(X1, X2)) -> a__times(mark(X1), mark(X2)) a__times(s(X), Y) -> a__plus(mark(Y), a__times(mark(X), mark(Y))) mark(square(X)) -> a__square(mark(X)) a__square(X) -> a__times(mark(X), mark(X)) mark(0) -> 0 mark(s(X)) -> s(mark(X)) mark(posrecip(X)) -> posrecip(mark(X)) mark(negrecip(X)) -> negrecip(mark(X)) mark(nil) -> nil mark(cons(X1, X2)) -> cons(mark(X1), X2) mark(rnil) -> rnil mark(rcons(X1, X2)) -> rcons(mark(X1), mark(X2)) a__times(0, Y) -> 0 a__times(X1, X2) -> times(X1, X2) a__from(X) -> from(X) a__2ndspos(0, Z) -> rnil a__2ndspos(X1, X2) -> 2ndspos(X1, X2) a__2ndsneg(0, Z) -> rnil a__2ndsneg(X1, X2) -> 2ndsneg(X1, X2) a__pi(X) -> pi(X) a__plus(X1, X2) -> plus(X1, X2) a__square(X) -> square(X) a__plus(s(X), Y) -> s(a__plus(mark(X), mark(Y))) a__pi(X) -> a__2ndspos(mark(X), a__from(0)) a__from(X) -> cons(mark(X), from(s(X))) a__2ndspos(s(N), cons(X, cons(Y, Z))) -> rcons(posrecip(mark(Y)), a__2ndsneg(mark(N), mark(Z))) a__2ndsneg(s(N), cons(X, cons(Y, Z))) -> rcons(negrecip(mark(Y)), a__2ndspos(mark(N), mark(Z))) ---------------------------------------- (26) Obligation: Q DP problem: The TRS P consists of the following rules: A__2NDSPOS(s(N), cons(X, cons(Y, Z))) -> A__2NDSNEG(mark(N), mark(Z)) A__2NDSNEG(s(N), cons(X, cons(Y, Z))) -> A__2NDSPOS(mark(N), mark(Z)) A__2NDSPOS(s(N), cons(X, cons(Y, Z))) -> MARK(Z) A__2NDSNEG(s(N), cons(X, cons(Y, Z))) -> MARK(Z) MARK(plus(X1, X2)) -> A__PLUS(mark(X1), mark(X2)) A__PLUS(0, Y) -> MARK(Y) MARK(plus(X1, X2)) -> MARK(X2) MARK(times(X1, X2)) -> A__TIMES(mark(X1), mark(X2)) A__TIMES(s(X), Y) -> A__PLUS(mark(Y), a__times(mark(X), mark(Y))) A__PLUS(s(X), Y) -> A__PLUS(mark(X), mark(Y)) A__PLUS(s(X), Y) -> MARK(Y) MARK(s(X)) -> MARK(X) MARK(posrecip(X)) -> MARK(X) MARK(negrecip(X)) -> MARK(X) MARK(rcons(X1, X2)) -> MARK(X2) A__TIMES(s(X), Y) -> A__TIMES(mark(X), mark(Y)) The TRS R consists of the following rules: a__from(X) -> cons(mark(X), from(s(X))) a__2ndspos(0, Z) -> rnil a__2ndspos(s(N), cons(X, cons(Y, Z))) -> rcons(posrecip(mark(Y)), a__2ndsneg(mark(N), mark(Z))) a__2ndsneg(0, Z) -> rnil a__2ndsneg(s(N), cons(X, cons(Y, Z))) -> rcons(negrecip(mark(Y)), a__2ndspos(mark(N), mark(Z))) a__pi(X) -> a__2ndspos(mark(X), a__from(0)) a__plus(0, Y) -> mark(Y) a__plus(s(X), Y) -> s(a__plus(mark(X), mark(Y))) a__times(0, Y) -> 0 a__times(s(X), Y) -> a__plus(mark(Y), a__times(mark(X), mark(Y))) a__square(X) -> a__times(mark(X), mark(X)) mark(from(X)) -> a__from(mark(X)) mark(2ndspos(X1, X2)) -> a__2ndspos(mark(X1), mark(X2)) mark(2ndsneg(X1, X2)) -> a__2ndsneg(mark(X1), mark(X2)) mark(pi(X)) -> a__pi(mark(X)) mark(plus(X1, X2)) -> a__plus(mark(X1), mark(X2)) mark(times(X1, X2)) -> a__times(mark(X1), mark(X2)) mark(square(X)) -> a__square(mark(X)) mark(0) -> 0 mark(s(X)) -> s(mark(X)) mark(posrecip(X)) -> posrecip(mark(X)) mark(negrecip(X)) -> negrecip(mark(X)) mark(nil) -> nil mark(cons(X1, X2)) -> cons(mark(X1), X2) mark(rnil) -> rnil mark(rcons(X1, X2)) -> rcons(mark(X1), mark(X2)) a__from(X) -> from(X) a__2ndspos(X1, X2) -> 2ndspos(X1, X2) a__2ndsneg(X1, X2) -> 2ndsneg(X1, X2) a__pi(X) -> pi(X) a__plus(X1, X2) -> plus(X1, X2) a__times(X1, X2) -> times(X1, X2) a__square(X) -> square(X) Q is empty. We have to consider all minimal (P,Q,R)-chains. ---------------------------------------- (27) DependencyGraphProof (EQUIVALENT) The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 2 SCCs with 2 less nodes. ---------------------------------------- (28) Complex Obligation (AND) ---------------------------------------- (29) Obligation: Q DP problem: The TRS P consists of the following rules: A__PLUS(0, Y) -> MARK(Y) MARK(plus(X1, X2)) -> A__PLUS(mark(X1), mark(X2)) A__PLUS(s(X), Y) -> A__PLUS(mark(X), mark(Y)) A__PLUS(s(X), Y) -> MARK(Y) MARK(plus(X1, X2)) -> MARK(X2) MARK(times(X1, X2)) -> A__TIMES(mark(X1), mark(X2)) A__TIMES(s(X), Y) -> A__PLUS(mark(Y), a__times(mark(X), mark(Y))) A__TIMES(s(X), Y) -> A__TIMES(mark(X), mark(Y)) MARK(s(X)) -> MARK(X) MARK(posrecip(X)) -> MARK(X) MARK(negrecip(X)) -> MARK(X) MARK(rcons(X1, X2)) -> MARK(X2) The TRS R consists of the following rules: a__from(X) -> cons(mark(X), from(s(X))) a__2ndspos(0, Z) -> rnil a__2ndspos(s(N), cons(X, cons(Y, Z))) -> rcons(posrecip(mark(Y)), a__2ndsneg(mark(N), mark(Z))) a__2ndsneg(0, Z) -> rnil a__2ndsneg(s(N), cons(X, cons(Y, Z))) -> rcons(negrecip(mark(Y)), a__2ndspos(mark(N), mark(Z))) a__pi(X) -> a__2ndspos(mark(X), a__from(0)) a__plus(0, Y) -> mark(Y) a__plus(s(X), Y) -> s(a__plus(mark(X), mark(Y))) a__times(0, Y) -> 0 a__times(s(X), Y) -> a__plus(mark(Y), a__times(mark(X), mark(Y))) a__square(X) -> a__times(mark(X), mark(X)) mark(from(X)) -> a__from(mark(X)) mark(2ndspos(X1, X2)) -> a__2ndspos(mark(X1), mark(X2)) mark(2ndsneg(X1, X2)) -> a__2ndsneg(mark(X1), mark(X2)) mark(pi(X)) -> a__pi(mark(X)) mark(plus(X1, X2)) -> a__plus(mark(X1), mark(X2)) mark(times(X1, X2)) -> a__times(mark(X1), mark(X2)) mark(square(X)) -> a__square(mark(X)) mark(0) -> 0 mark(s(X)) -> s(mark(X)) mark(posrecip(X)) -> posrecip(mark(X)) mark(negrecip(X)) -> negrecip(mark(X)) mark(nil) -> nil mark(cons(X1, X2)) -> cons(mark(X1), X2) mark(rnil) -> rnil mark(rcons(X1, X2)) -> rcons(mark(X1), mark(X2)) a__from(X) -> from(X) a__2ndspos(X1, X2) -> 2ndspos(X1, X2) a__2ndsneg(X1, X2) -> 2ndsneg(X1, X2) a__pi(X) -> pi(X) a__plus(X1, X2) -> plus(X1, X2) a__times(X1, X2) -> times(X1, X2) a__square(X) -> square(X) Q is empty. We have to consider all minimal (P,Q,R)-chains. ---------------------------------------- (30) QDPOrderProof (EQUIVALENT) We use the reduction pair processor [LPAR04,JAR06]. The following pairs can be oriented strictly and are deleted. MARK(negrecip(X)) -> MARK(X) The remaining pairs can at least be oriented weakly. Used ordering: Polynomial Order [NEGPOLO,POLO] with Interpretation: POL( A__PLUS_2(x_1, x_2) ) = 2x_2 POL( A__TIMES_2(x_1, x_2) ) = 2 POL( mark_1(x_1) ) = x_1 POL( from_1(x_1) ) = max{0, -1} POL( a__from_1(x_1) ) = 0 POL( 2ndspos_2(x_1, x_2) ) = x_2 + 1 POL( a__2ndspos_2(x_1, x_2) ) = x_2 + 1 POL( 2ndsneg_2(x_1, x_2) ) = 2x_2 + 1 POL( a__2ndsneg_2(x_1, x_2) ) = 2x_2 + 1 POL( pi_1(x_1) ) = x_1 + 2 POL( a__pi_1(x_1) ) = x_1 + 2 POL( plus_2(x_1, x_2) ) = x_2 POL( a__plus_2(x_1, x_2) ) = x_2 POL( 0 ) = 0 POL( times_2(x_1, x_2) ) = 1 POL( a__times_2(x_1, x_2) ) = 1 POL( s_1(x_1) ) = x_1 POL( square_1(x_1) ) = 1 POL( a__square_1(x_1) ) = 1 POL( posrecip_1(x_1) ) = x_1 POL( negrecip_1(x_1) ) = 2x_1 + 2 POL( nil ) = 0 POL( cons_2(x_1, x_2) ) = 2x_2 POL( rnil ) = 1 POL( rcons_2(x_1, x_2) ) = x_2 POL( MARK_1(x_1) ) = 2x_1 The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented: mark(from(X)) -> a__from(mark(X)) mark(2ndspos(X1, X2)) -> a__2ndspos(mark(X1), mark(X2)) mark(2ndsneg(X1, X2)) -> a__2ndsneg(mark(X1), mark(X2)) mark(pi(X)) -> a__pi(mark(X)) mark(plus(X1, X2)) -> a__plus(mark(X1), mark(X2)) a__plus(0, Y) -> mark(Y) mark(times(X1, X2)) -> a__times(mark(X1), mark(X2)) a__times(s(X), Y) -> a__plus(mark(Y), a__times(mark(X), mark(Y))) mark(square(X)) -> a__square(mark(X)) a__square(X) -> a__times(mark(X), mark(X)) mark(0) -> 0 mark(s(X)) -> s(mark(X)) mark(posrecip(X)) -> posrecip(mark(X)) mark(negrecip(X)) -> negrecip(mark(X)) mark(nil) -> nil mark(cons(X1, X2)) -> cons(mark(X1), X2) mark(rnil) -> rnil mark(rcons(X1, X2)) -> rcons(mark(X1), mark(X2)) a__times(0, Y) -> 0 a__times(X1, X2) -> times(X1, X2) a__from(X) -> from(X) a__2ndspos(0, Z) -> rnil a__2ndspos(X1, X2) -> 2ndspos(X1, X2) a__2ndsneg(0, Z) -> rnil a__2ndsneg(X1, X2) -> 2ndsneg(X1, X2) a__pi(X) -> pi(X) a__plus(X1, X2) -> plus(X1, X2) a__square(X) -> square(X) a__plus(s(X), Y) -> s(a__plus(mark(X), mark(Y))) a__pi(X) -> a__2ndspos(mark(X), a__from(0)) a__from(X) -> cons(mark(X), from(s(X))) a__2ndspos(s(N), cons(X, cons(Y, Z))) -> rcons(posrecip(mark(Y)), a__2ndsneg(mark(N), mark(Z))) a__2ndsneg(s(N), cons(X, cons(Y, Z))) -> rcons(negrecip(mark(Y)), a__2ndspos(mark(N), mark(Z))) ---------------------------------------- (31) Obligation: Q DP problem: The TRS P consists of the following rules: A__PLUS(0, Y) -> MARK(Y) MARK(plus(X1, X2)) -> A__PLUS(mark(X1), mark(X2)) A__PLUS(s(X), Y) -> A__PLUS(mark(X), mark(Y)) A__PLUS(s(X), Y) -> MARK(Y) MARK(plus(X1, X2)) -> MARK(X2) MARK(times(X1, X2)) -> A__TIMES(mark(X1), mark(X2)) A__TIMES(s(X), Y) -> A__PLUS(mark(Y), a__times(mark(X), mark(Y))) A__TIMES(s(X), Y) -> A__TIMES(mark(X), mark(Y)) MARK(s(X)) -> MARK(X) MARK(posrecip(X)) -> MARK(X) MARK(rcons(X1, X2)) -> MARK(X2) The TRS R consists of the following rules: a__from(X) -> cons(mark(X), from(s(X))) a__2ndspos(0, Z) -> rnil a__2ndspos(s(N), cons(X, cons(Y, Z))) -> rcons(posrecip(mark(Y)), a__2ndsneg(mark(N), mark(Z))) a__2ndsneg(0, Z) -> rnil a__2ndsneg(s(N), cons(X, cons(Y, Z))) -> rcons(negrecip(mark(Y)), a__2ndspos(mark(N), mark(Z))) a__pi(X) -> a__2ndspos(mark(X), a__from(0)) a__plus(0, Y) -> mark(Y) a__plus(s(X), Y) -> s(a__plus(mark(X), mark(Y))) a__times(0, Y) -> 0 a__times(s(X), Y) -> a__plus(mark(Y), a__times(mark(X), mark(Y))) a__square(X) -> a__times(mark(X), mark(X)) mark(from(X)) -> a__from(mark(X)) mark(2ndspos(X1, X2)) -> a__2ndspos(mark(X1), mark(X2)) mark(2ndsneg(X1, X2)) -> a__2ndsneg(mark(X1), mark(X2)) mark(pi(X)) -> a__pi(mark(X)) mark(plus(X1, X2)) -> a__plus(mark(X1), mark(X2)) mark(times(X1, X2)) -> a__times(mark(X1), mark(X2)) mark(square(X)) -> a__square(mark(X)) mark(0) -> 0 mark(s(X)) -> s(mark(X)) mark(posrecip(X)) -> posrecip(mark(X)) mark(negrecip(X)) -> negrecip(mark(X)) mark(nil) -> nil mark(cons(X1, X2)) -> cons(mark(X1), X2) mark(rnil) -> rnil mark(rcons(X1, X2)) -> rcons(mark(X1), mark(X2)) a__from(X) -> from(X) a__2ndspos(X1, X2) -> 2ndspos(X1, X2) a__2ndsneg(X1, X2) -> 2ndsneg(X1, X2) a__pi(X) -> pi(X) a__plus(X1, X2) -> plus(X1, X2) a__times(X1, X2) -> times(X1, X2) a__square(X) -> square(X) Q is empty. We have to consider all minimal (P,Q,R)-chains. ---------------------------------------- (32) QDPOrderProof (EQUIVALENT) We use the reduction pair processor [LPAR04,JAR06]. The following pairs can be oriented strictly and are deleted. MARK(posrecip(X)) -> MARK(X) The remaining pairs can at least be oriented weakly. Used ordering: Polynomial Order [NEGPOLO,POLO] with Interpretation: POL( A__PLUS_2(x_1, x_2) ) = x_2 POL( A__TIMES_2(x_1, x_2) ) = 0 POL( mark_1(x_1) ) = x_1 POL( from_1(x_1) ) = 1 POL( a__from_1(x_1) ) = 1 POL( 2ndspos_2(x_1, x_2) ) = 0 POL( a__2ndspos_2(x_1, x_2) ) = 0 POL( 2ndsneg_2(x_1, x_2) ) = 0 POL( a__2ndsneg_2(x_1, x_2) ) = max{0, -1} POL( pi_1(x_1) ) = 0 POL( a__pi_1(x_1) ) = 0 POL( plus_2(x_1, x_2) ) = x_2 POL( a__plus_2(x_1, x_2) ) = x_2 POL( 0 ) = 0 POL( times_2(x_1, x_2) ) = 0 POL( a__times_2(x_1, x_2) ) = 0 POL( s_1(x_1) ) = x_1 POL( square_1(x_1) ) = 2x_1 + 1 POL( a__square_1(x_1) ) = 2x_1 + 1 POL( posrecip_1(x_1) ) = x_1 + 1 POL( negrecip_1(x_1) ) = max{0, -2} POL( nil ) = 0 POL( cons_2(x_1, x_2) ) = 1 POL( rnil ) = 0 POL( rcons_2(x_1, x_2) ) = 2x_2 POL( MARK_1(x_1) ) = x_1 The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented: mark(from(X)) -> a__from(mark(X)) mark(2ndspos(X1, X2)) -> a__2ndspos(mark(X1), mark(X2)) mark(2ndsneg(X1, X2)) -> a__2ndsneg(mark(X1), mark(X2)) mark(pi(X)) -> a__pi(mark(X)) mark(plus(X1, X2)) -> a__plus(mark(X1), mark(X2)) a__plus(0, Y) -> mark(Y) mark(times(X1, X2)) -> a__times(mark(X1), mark(X2)) a__times(s(X), Y) -> a__plus(mark(Y), a__times(mark(X), mark(Y))) mark(square(X)) -> a__square(mark(X)) a__square(X) -> a__times(mark(X), mark(X)) mark(0) -> 0 mark(s(X)) -> s(mark(X)) mark(posrecip(X)) -> posrecip(mark(X)) mark(negrecip(X)) -> negrecip(mark(X)) mark(nil) -> nil mark(cons(X1, X2)) -> cons(mark(X1), X2) mark(rnil) -> rnil mark(rcons(X1, X2)) -> rcons(mark(X1), mark(X2)) a__times(0, Y) -> 0 a__times(X1, X2) -> times(X1, X2) a__from(X) -> from(X) a__2ndspos(0, Z) -> rnil a__2ndspos(X1, X2) -> 2ndspos(X1, X2) a__2ndsneg(0, Z) -> rnil a__2ndsneg(X1, X2) -> 2ndsneg(X1, X2) a__pi(X) -> pi(X) a__plus(X1, X2) -> plus(X1, X2) a__square(X) -> square(X) a__plus(s(X), Y) -> s(a__plus(mark(X), mark(Y))) a__pi(X) -> a__2ndspos(mark(X), a__from(0)) a__from(X) -> cons(mark(X), from(s(X))) a__2ndspos(s(N), cons(X, cons(Y, Z))) -> rcons(posrecip(mark(Y)), a__2ndsneg(mark(N), mark(Z))) a__2ndsneg(s(N), cons(X, cons(Y, Z))) -> rcons(negrecip(mark(Y)), a__2ndspos(mark(N), mark(Z))) ---------------------------------------- (33) Obligation: Q DP problem: The TRS P consists of the following rules: A__PLUS(0, Y) -> MARK(Y) MARK(plus(X1, X2)) -> A__PLUS(mark(X1), mark(X2)) A__PLUS(s(X), Y) -> A__PLUS(mark(X), mark(Y)) A__PLUS(s(X), Y) -> MARK(Y) MARK(plus(X1, X2)) -> MARK(X2) MARK(times(X1, X2)) -> A__TIMES(mark(X1), mark(X2)) A__TIMES(s(X), Y) -> A__PLUS(mark(Y), a__times(mark(X), mark(Y))) A__TIMES(s(X), Y) -> A__TIMES(mark(X), mark(Y)) MARK(s(X)) -> MARK(X) MARK(rcons(X1, X2)) -> MARK(X2) The TRS R consists of the following rules: a__from(X) -> cons(mark(X), from(s(X))) a__2ndspos(0, Z) -> rnil a__2ndspos(s(N), cons(X, cons(Y, Z))) -> rcons(posrecip(mark(Y)), a__2ndsneg(mark(N), mark(Z))) a__2ndsneg(0, Z) -> rnil a__2ndsneg(s(N), cons(X, cons(Y, Z))) -> rcons(negrecip(mark(Y)), a__2ndspos(mark(N), mark(Z))) a__pi(X) -> a__2ndspos(mark(X), a__from(0)) a__plus(0, Y) -> mark(Y) a__plus(s(X), Y) -> s(a__plus(mark(X), mark(Y))) a__times(0, Y) -> 0 a__times(s(X), Y) -> a__plus(mark(Y), a__times(mark(X), mark(Y))) a__square(X) -> a__times(mark(X), mark(X)) mark(from(X)) -> a__from(mark(X)) mark(2ndspos(X1, X2)) -> a__2ndspos(mark(X1), mark(X2)) mark(2ndsneg(X1, X2)) -> a__2ndsneg(mark(X1), mark(X2)) mark(pi(X)) -> a__pi(mark(X)) mark(plus(X1, X2)) -> a__plus(mark(X1), mark(X2)) mark(times(X1, X2)) -> a__times(mark(X1), mark(X2)) mark(square(X)) -> a__square(mark(X)) mark(0) -> 0 mark(s(X)) -> s(mark(X)) mark(posrecip(X)) -> posrecip(mark(X)) mark(negrecip(X)) -> negrecip(mark(X)) mark(nil) -> nil mark(cons(X1, X2)) -> cons(mark(X1), X2) mark(rnil) -> rnil mark(rcons(X1, X2)) -> rcons(mark(X1), mark(X2)) a__from(X) -> from(X) a__2ndspos(X1, X2) -> 2ndspos(X1, X2) a__2ndsneg(X1, X2) -> 2ndsneg(X1, X2) a__pi(X) -> pi(X) a__plus(X1, X2) -> plus(X1, X2) a__times(X1, X2) -> times(X1, X2) a__square(X) -> square(X) Q is empty. We have to consider all minimal (P,Q,R)-chains. ---------------------------------------- (34) QDPOrderProof (EQUIVALENT) We use the reduction pair processor [LPAR04,JAR06]. The following pairs can be oriented strictly and are deleted. MARK(plus(X1, X2)) -> A__PLUS(mark(X1), mark(X2)) MARK(plus(X1, X2)) -> MARK(X2) MARK(times(X1, X2)) -> A__TIMES(mark(X1), mark(X2)) A__TIMES(s(X), Y) -> A__PLUS(mark(Y), a__times(mark(X), mark(Y))) A__TIMES(s(X), Y) -> A__TIMES(mark(X), mark(Y)) MARK(s(X)) -> MARK(X) The remaining pairs can at least be oriented weakly. Used ordering: Combined order from the following AFS and order. A__PLUS(x1, x2) = A__PLUS(x2) 0 = 0 MARK(x1) = MARK(x1) plus(x1, x2) = plus(x1, x2) mark(x1) = x1 s(x1) = s(x1) times(x1, x2) = times(x1, x2) A__TIMES(x1, x2) = A__TIMES(x1, x2) a__times(x1, x2) = a__times(x1, x2) rcons(x1, x2) = x2 from(x1) = x1 a__from(x1) = x1 2ndspos(x1, x2) = 2ndspos(x1) a__2ndspos(x1, x2) = a__2ndspos(x1) 2ndsneg(x1, x2) = 2ndsneg(x1) a__2ndsneg(x1, x2) = a__2ndsneg(x1) pi(x1) = pi(x1) a__pi(x1) = a__pi(x1) a__plus(x1, x2) = a__plus(x1, x2) square(x1) = square(x1) a__square(x1) = a__square(x1) posrecip(x1) = posrecip negrecip(x1) = negrecip nil = nil cons(x1, x2) = x1 rnil = rnil Recursive path order with status [RPO]. Quasi-Precedence: [2ndspos_1, a__2ndspos_1, 2ndsneg_1, a__2ndsneg_1, pi_1, a__pi_1] > [0, s_1, rnil] [square_1, a__square_1] > [times_2, A__TIMES_2, a__times_2] > [A__PLUS_1, MARK_1] > [0, s_1, rnil] [square_1, a__square_1] > [times_2, A__TIMES_2, a__times_2] > [plus_2, a__plus_2] > [0, s_1, rnil] posrecip > [0, s_1, rnil] negrecip > [0, s_1, rnil] nil > [0, s_1, rnil] Status: A__PLUS_1: [1] 0: multiset status MARK_1: [1] plus_2: [1,2] s_1: [1] times_2: [1,2] A__TIMES_2: [1,2] a__times_2: [1,2] 2ndspos_1: multiset status a__2ndspos_1: multiset status 2ndsneg_1: multiset status a__2ndsneg_1: multiset status pi_1: multiset status a__pi_1: multiset status a__plus_2: [1,2] square_1: [1] a__square_1: [1] posrecip: multiset status negrecip: [] nil: multiset status rnil: multiset status The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented: mark(from(X)) -> a__from(mark(X)) mark(2ndspos(X1, X2)) -> a__2ndspos(mark(X1), mark(X2)) mark(2ndsneg(X1, X2)) -> a__2ndsneg(mark(X1), mark(X2)) mark(pi(X)) -> a__pi(mark(X)) mark(plus(X1, X2)) -> a__plus(mark(X1), mark(X2)) a__plus(0, Y) -> mark(Y) mark(times(X1, X2)) -> a__times(mark(X1), mark(X2)) a__times(s(X), Y) -> a__plus(mark(Y), a__times(mark(X), mark(Y))) mark(square(X)) -> a__square(mark(X)) a__square(X) -> a__times(mark(X), mark(X)) mark(0) -> 0 mark(s(X)) -> s(mark(X)) mark(posrecip(X)) -> posrecip(mark(X)) mark(negrecip(X)) -> negrecip(mark(X)) mark(nil) -> nil mark(cons(X1, X2)) -> cons(mark(X1), X2) mark(rnil) -> rnil mark(rcons(X1, X2)) -> rcons(mark(X1), mark(X2)) a__times(0, Y) -> 0 a__times(X1, X2) -> times(X1, X2) a__from(X) -> from(X) a__2ndspos(0, Z) -> rnil a__2ndspos(X1, X2) -> 2ndspos(X1, X2) a__2ndsneg(0, Z) -> rnil a__2ndsneg(X1, X2) -> 2ndsneg(X1, X2) a__pi(X) -> pi(X) a__plus(X1, X2) -> plus(X1, X2) a__square(X) -> square(X) a__plus(s(X), Y) -> s(a__plus(mark(X), mark(Y))) a__pi(X) -> a__2ndspos(mark(X), a__from(0)) a__from(X) -> cons(mark(X), from(s(X))) a__2ndspos(s(N), cons(X, cons(Y, Z))) -> rcons(posrecip(mark(Y)), a__2ndsneg(mark(N), mark(Z))) a__2ndsneg(s(N), cons(X, cons(Y, Z))) -> rcons(negrecip(mark(Y)), a__2ndspos(mark(N), mark(Z))) ---------------------------------------- (35) Obligation: Q DP problem: The TRS P consists of the following rules: A__PLUS(0, Y) -> MARK(Y) A__PLUS(s(X), Y) -> A__PLUS(mark(X), mark(Y)) A__PLUS(s(X), Y) -> MARK(Y) MARK(rcons(X1, X2)) -> MARK(X2) The TRS R consists of the following rules: a__from(X) -> cons(mark(X), from(s(X))) a__2ndspos(0, Z) -> rnil a__2ndspos(s(N), cons(X, cons(Y, Z))) -> rcons(posrecip(mark(Y)), a__2ndsneg(mark(N), mark(Z))) a__2ndsneg(0, Z) -> rnil a__2ndsneg(s(N), cons(X, cons(Y, Z))) -> rcons(negrecip(mark(Y)), a__2ndspos(mark(N), mark(Z))) a__pi(X) -> a__2ndspos(mark(X), a__from(0)) a__plus(0, Y) -> mark(Y) a__plus(s(X), Y) -> s(a__plus(mark(X), mark(Y))) a__times(0, Y) -> 0 a__times(s(X), Y) -> a__plus(mark(Y), a__times(mark(X), mark(Y))) a__square(X) -> a__times(mark(X), mark(X)) mark(from(X)) -> a__from(mark(X)) mark(2ndspos(X1, X2)) -> a__2ndspos(mark(X1), mark(X2)) mark(2ndsneg(X1, X2)) -> a__2ndsneg(mark(X1), mark(X2)) mark(pi(X)) -> a__pi(mark(X)) mark(plus(X1, X2)) -> a__plus(mark(X1), mark(X2)) mark(times(X1, X2)) -> a__times(mark(X1), mark(X2)) mark(square(X)) -> a__square(mark(X)) mark(0) -> 0 mark(s(X)) -> s(mark(X)) mark(posrecip(X)) -> posrecip(mark(X)) mark(negrecip(X)) -> negrecip(mark(X)) mark(nil) -> nil mark(cons(X1, X2)) -> cons(mark(X1), X2) mark(rnil) -> rnil mark(rcons(X1, X2)) -> rcons(mark(X1), mark(X2)) a__from(X) -> from(X) a__2ndspos(X1, X2) -> 2ndspos(X1, X2) a__2ndsneg(X1, X2) -> 2ndsneg(X1, X2) a__pi(X) -> pi(X) a__plus(X1, X2) -> plus(X1, X2) a__times(X1, X2) -> times(X1, X2) a__square(X) -> square(X) Q is empty. We have to consider all minimal (P,Q,R)-chains. ---------------------------------------- (36) DependencyGraphProof (EQUIVALENT) The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 2 SCCs with 2 less nodes. ---------------------------------------- (37) Complex Obligation (AND) ---------------------------------------- (38) Obligation: Q DP problem: The TRS P consists of the following rules: MARK(rcons(X1, X2)) -> MARK(X2) The TRS R consists of the following rules: a__from(X) -> cons(mark(X), from(s(X))) a__2ndspos(0, Z) -> rnil a__2ndspos(s(N), cons(X, cons(Y, Z))) -> rcons(posrecip(mark(Y)), a__2ndsneg(mark(N), mark(Z))) a__2ndsneg(0, Z) -> rnil a__2ndsneg(s(N), cons(X, cons(Y, Z))) -> rcons(negrecip(mark(Y)), a__2ndspos(mark(N), mark(Z))) a__pi(X) -> a__2ndspos(mark(X), a__from(0)) a__plus(0, Y) -> mark(Y) a__plus(s(X), Y) -> s(a__plus(mark(X), mark(Y))) a__times(0, Y) -> 0 a__times(s(X), Y) -> a__plus(mark(Y), a__times(mark(X), mark(Y))) a__square(X) -> a__times(mark(X), mark(X)) mark(from(X)) -> a__from(mark(X)) mark(2ndspos(X1, X2)) -> a__2ndspos(mark(X1), mark(X2)) mark(2ndsneg(X1, X2)) -> a__2ndsneg(mark(X1), mark(X2)) mark(pi(X)) -> a__pi(mark(X)) mark(plus(X1, X2)) -> a__plus(mark(X1), mark(X2)) mark(times(X1, X2)) -> a__times(mark(X1), mark(X2)) mark(square(X)) -> a__square(mark(X)) mark(0) -> 0 mark(s(X)) -> s(mark(X)) mark(posrecip(X)) -> posrecip(mark(X)) mark(negrecip(X)) -> negrecip(mark(X)) mark(nil) -> nil mark(cons(X1, X2)) -> cons(mark(X1), X2) mark(rnil) -> rnil mark(rcons(X1, X2)) -> rcons(mark(X1), mark(X2)) a__from(X) -> from(X) a__2ndspos(X1, X2) -> 2ndspos(X1, X2) a__2ndsneg(X1, X2) -> 2ndsneg(X1, X2) a__pi(X) -> pi(X) a__plus(X1, X2) -> plus(X1, X2) a__times(X1, X2) -> times(X1, X2) a__square(X) -> square(X) Q is empty. We have to consider all minimal (P,Q,R)-chains. ---------------------------------------- (39) UsableRulesProof (EQUIVALENT) We can use the usable rules and reduction pair processor [LPAR04] with the Ce-compatible extension of the polynomial order that maps every function symbol to the sum of its arguments. Then, we can delete all non-usable rules [FROCOS05] from R. ---------------------------------------- (40) Obligation: Q DP problem: The TRS P consists of the following rules: MARK(rcons(X1, X2)) -> MARK(X2) R is empty. Q is empty. We have to consider all minimal (P,Q,R)-chains. ---------------------------------------- (41) QDPSizeChangeProof (EQUIVALENT) By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs: *MARK(rcons(X1, X2)) -> MARK(X2) The graph contains the following edges 1 > 1 ---------------------------------------- (42) YES ---------------------------------------- (43) Obligation: Q DP problem: The TRS P consists of the following rules: A__PLUS(s(X), Y) -> A__PLUS(mark(X), mark(Y)) The TRS R consists of the following rules: a__from(X) -> cons(mark(X), from(s(X))) a__2ndspos(0, Z) -> rnil a__2ndspos(s(N), cons(X, cons(Y, Z))) -> rcons(posrecip(mark(Y)), a__2ndsneg(mark(N), mark(Z))) a__2ndsneg(0, Z) -> rnil a__2ndsneg(s(N), cons(X, cons(Y, Z))) -> rcons(negrecip(mark(Y)), a__2ndspos(mark(N), mark(Z))) a__pi(X) -> a__2ndspos(mark(X), a__from(0)) a__plus(0, Y) -> mark(Y) a__plus(s(X), Y) -> s(a__plus(mark(X), mark(Y))) a__times(0, Y) -> 0 a__times(s(X), Y) -> a__plus(mark(Y), a__times(mark(X), mark(Y))) a__square(X) -> a__times(mark(X), mark(X)) mark(from(X)) -> a__from(mark(X)) mark(2ndspos(X1, X2)) -> a__2ndspos(mark(X1), mark(X2)) mark(2ndsneg(X1, X2)) -> a__2ndsneg(mark(X1), mark(X2)) mark(pi(X)) -> a__pi(mark(X)) mark(plus(X1, X2)) -> a__plus(mark(X1), mark(X2)) mark(times(X1, X2)) -> a__times(mark(X1), mark(X2)) mark(square(X)) -> a__square(mark(X)) mark(0) -> 0 mark(s(X)) -> s(mark(X)) mark(posrecip(X)) -> posrecip(mark(X)) mark(negrecip(X)) -> negrecip(mark(X)) mark(nil) -> nil mark(cons(X1, X2)) -> cons(mark(X1), X2) mark(rnil) -> rnil mark(rcons(X1, X2)) -> rcons(mark(X1), mark(X2)) a__from(X) -> from(X) a__2ndspos(X1, X2) -> 2ndspos(X1, X2) a__2ndsneg(X1, X2) -> 2ndsneg(X1, X2) a__pi(X) -> pi(X) a__plus(X1, X2) -> plus(X1, X2) a__times(X1, X2) -> times(X1, X2) a__square(X) -> square(X) Q is empty. We have to consider all minimal (P,Q,R)-chains. ---------------------------------------- (44) QDPOrderProof (EQUIVALENT) We use the reduction pair processor [LPAR04,JAR06]. The following pairs can be oriented strictly and are deleted. A__PLUS(s(X), Y) -> A__PLUS(mark(X), mark(Y)) The remaining pairs can at least be oriented weakly. Used ordering: Combined order from the following AFS and order. A__PLUS(x1, x2) = A__PLUS(x1, x2) s(x1) = s(x1) mark(x1) = x1 from(x1) = from a__from(x1) = a__from 2ndspos(x1, x2) = 2ndspos(x2) a__2ndspos(x1, x2) = a__2ndspos(x2) 2ndsneg(x1, x2) = 2ndsneg(x2) a__2ndsneg(x1, x2) = a__2ndsneg(x2) pi(x1) = pi(x1) a__pi(x1) = a__pi(x1) plus(x1, x2) = plus(x1, x2) a__plus(x1, x2) = a__plus(x1, x2) 0 = 0 times(x1, x2) = times(x1, x2) a__times(x1, x2) = a__times(x1, x2) square(x1) = square(x1) a__square(x1) = a__square(x1) posrecip(x1) = posrecip negrecip(x1) = negrecip nil = nil cons(x1, x2) = cons rnil = rnil rcons(x1, x2) = rcons Recursive path order with status [RPO]. Quasi-Precedence: A__PLUS_2 > [from, a__from, cons] [2ndsneg_1, a__2ndsneg_1] > [s_1, 2ndspos_1, a__2ndspos_1, pi_1, a__pi_1, negrecip] > rnil > [from, a__from, cons] [2ndsneg_1, a__2ndsneg_1] > [s_1, 2ndspos_1, a__2ndspos_1, pi_1, a__pi_1, negrecip] > rcons > [from, a__from, cons] 0 > rnil > [from, a__from, cons] [square_1, a__square_1] > [times_2, a__times_2] > [plus_2, a__plus_2] > [s_1, 2ndspos_1, a__2ndspos_1, pi_1, a__pi_1, negrecip] > rnil > [from, a__from, cons] [square_1, a__square_1] > [times_2, a__times_2] > [plus_2, a__plus_2] > [s_1, 2ndspos_1, a__2ndspos_1, pi_1, a__pi_1, negrecip] > rcons > [from, a__from, cons] posrecip > [from, a__from, cons] nil > [from, a__from, cons] Status: A__PLUS_2: [1,2] s_1: [1] from: [] a__from: [] 2ndspos_1: [1] a__2ndspos_1: [1] 2ndsneg_1: multiset status a__2ndsneg_1: multiset status pi_1: [1] a__pi_1: [1] plus_2: [1,2] a__plus_2: [1,2] 0: multiset status times_2: multiset status a__times_2: multiset status square_1: [1] a__square_1: [1] posrecip: multiset status negrecip: multiset status nil: multiset status cons: [] rnil: multiset status rcons: multiset status The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented: mark(from(X)) -> a__from(mark(X)) mark(2ndspos(X1, X2)) -> a__2ndspos(mark(X1), mark(X2)) mark(2ndsneg(X1, X2)) -> a__2ndsneg(mark(X1), mark(X2)) mark(pi(X)) -> a__pi(mark(X)) mark(plus(X1, X2)) -> a__plus(mark(X1), mark(X2)) a__plus(0, Y) -> mark(Y) mark(times(X1, X2)) -> a__times(mark(X1), mark(X2)) a__times(s(X), Y) -> a__plus(mark(Y), a__times(mark(X), mark(Y))) mark(square(X)) -> a__square(mark(X)) a__square(X) -> a__times(mark(X), mark(X)) mark(0) -> 0 mark(s(X)) -> s(mark(X)) mark(posrecip(X)) -> posrecip(mark(X)) mark(negrecip(X)) -> negrecip(mark(X)) mark(nil) -> nil mark(cons(X1, X2)) -> cons(mark(X1), X2) mark(rnil) -> rnil mark(rcons(X1, X2)) -> rcons(mark(X1), mark(X2)) a__from(X) -> from(X) a__2ndspos(0, Z) -> rnil a__2ndspos(X1, X2) -> 2ndspos(X1, X2) a__2ndsneg(0, Z) -> rnil a__2ndsneg(X1, X2) -> 2ndsneg(X1, X2) a__pi(X) -> pi(X) a__plus(X1, X2) -> plus(X1, X2) a__times(0, Y) -> 0 a__times(X1, X2) -> times(X1, X2) a__square(X) -> square(X) a__plus(s(X), Y) -> s(a__plus(mark(X), mark(Y))) a__pi(X) -> a__2ndspos(mark(X), a__from(0)) a__from(X) -> cons(mark(X), from(s(X))) a__2ndspos(s(N), cons(X, cons(Y, Z))) -> rcons(posrecip(mark(Y)), a__2ndsneg(mark(N), mark(Z))) a__2ndsneg(s(N), cons(X, cons(Y, Z))) -> rcons(negrecip(mark(Y)), a__2ndspos(mark(N), mark(Z))) ---------------------------------------- (45) Obligation: Q DP problem: P is empty. The TRS R consists of the following rules: a__from(X) -> cons(mark(X), from(s(X))) a__2ndspos(0, Z) -> rnil a__2ndspos(s(N), cons(X, cons(Y, Z))) -> rcons(posrecip(mark(Y)), a__2ndsneg(mark(N), mark(Z))) a__2ndsneg(0, Z) -> rnil a__2ndsneg(s(N), cons(X, cons(Y, Z))) -> rcons(negrecip(mark(Y)), a__2ndspos(mark(N), mark(Z))) a__pi(X) -> a__2ndspos(mark(X), a__from(0)) a__plus(0, Y) -> mark(Y) a__plus(s(X), Y) -> s(a__plus(mark(X), mark(Y))) a__times(0, Y) -> 0 a__times(s(X), Y) -> a__plus(mark(Y), a__times(mark(X), mark(Y))) a__square(X) -> a__times(mark(X), mark(X)) mark(from(X)) -> a__from(mark(X)) mark(2ndspos(X1, X2)) -> a__2ndspos(mark(X1), mark(X2)) mark(2ndsneg(X1, X2)) -> a__2ndsneg(mark(X1), mark(X2)) mark(pi(X)) -> a__pi(mark(X)) mark(plus(X1, X2)) -> a__plus(mark(X1), mark(X2)) mark(times(X1, X2)) -> a__times(mark(X1), mark(X2)) mark(square(X)) -> a__square(mark(X)) mark(0) -> 0 mark(s(X)) -> s(mark(X)) mark(posrecip(X)) -> posrecip(mark(X)) mark(negrecip(X)) -> negrecip(mark(X)) mark(nil) -> nil mark(cons(X1, X2)) -> cons(mark(X1), X2) mark(rnil) -> rnil mark(rcons(X1, X2)) -> rcons(mark(X1), mark(X2)) a__from(X) -> from(X) a__2ndspos(X1, X2) -> 2ndspos(X1, X2) a__2ndsneg(X1, X2) -> 2ndsneg(X1, X2) a__pi(X) -> pi(X) a__plus(X1, X2) -> plus(X1, X2) a__times(X1, X2) -> times(X1, X2) a__square(X) -> square(X) Q is empty. We have to consider all minimal (P,Q,R)-chains. ---------------------------------------- (46) PisEmptyProof (EQUIVALENT) The TRS P is empty. Hence, there is no (P,Q,R) chain. ---------------------------------------- (47) YES ---------------------------------------- (48) Obligation: Q DP problem: The TRS P consists of the following rules: A__2NDSNEG(s(N), cons(X, cons(Y, Z))) -> A__2NDSPOS(mark(N), mark(Z)) A__2NDSPOS(s(N), cons(X, cons(Y, Z))) -> A__2NDSNEG(mark(N), mark(Z)) The TRS R consists of the following rules: a__from(X) -> cons(mark(X), from(s(X))) a__2ndspos(0, Z) -> rnil a__2ndspos(s(N), cons(X, cons(Y, Z))) -> rcons(posrecip(mark(Y)), a__2ndsneg(mark(N), mark(Z))) a__2ndsneg(0, Z) -> rnil a__2ndsneg(s(N), cons(X, cons(Y, Z))) -> rcons(negrecip(mark(Y)), a__2ndspos(mark(N), mark(Z))) a__pi(X) -> a__2ndspos(mark(X), a__from(0)) a__plus(0, Y) -> mark(Y) a__plus(s(X), Y) -> s(a__plus(mark(X), mark(Y))) a__times(0, Y) -> 0 a__times(s(X), Y) -> a__plus(mark(Y), a__times(mark(X), mark(Y))) a__square(X) -> a__times(mark(X), mark(X)) mark(from(X)) -> a__from(mark(X)) mark(2ndspos(X1, X2)) -> a__2ndspos(mark(X1), mark(X2)) mark(2ndsneg(X1, X2)) -> a__2ndsneg(mark(X1), mark(X2)) mark(pi(X)) -> a__pi(mark(X)) mark(plus(X1, X2)) -> a__plus(mark(X1), mark(X2)) mark(times(X1, X2)) -> a__times(mark(X1), mark(X2)) mark(square(X)) -> a__square(mark(X)) mark(0) -> 0 mark(s(X)) -> s(mark(X)) mark(posrecip(X)) -> posrecip(mark(X)) mark(negrecip(X)) -> negrecip(mark(X)) mark(nil) -> nil mark(cons(X1, X2)) -> cons(mark(X1), X2) mark(rnil) -> rnil mark(rcons(X1, X2)) -> rcons(mark(X1), mark(X2)) a__from(X) -> from(X) a__2ndspos(X1, X2) -> 2ndspos(X1, X2) a__2ndsneg(X1, X2) -> 2ndsneg(X1, X2) a__pi(X) -> pi(X) a__plus(X1, X2) -> plus(X1, X2) a__times(X1, X2) -> times(X1, X2) a__square(X) -> square(X) Q is empty. We have to consider all minimal (P,Q,R)-chains. ---------------------------------------- (49) QDPOrderProof (EQUIVALENT) We use the reduction pair processor [LPAR04,JAR06]. The following pairs can be oriented strictly and are deleted. A__2NDSNEG(s(N), cons(X, cons(Y, Z))) -> A__2NDSPOS(mark(N), mark(Z)) A__2NDSPOS(s(N), cons(X, cons(Y, Z))) -> A__2NDSNEG(mark(N), mark(Z)) The remaining pairs can at least be oriented weakly. Used ordering: Combined order from the following AFS and order. A__2NDSNEG(x1, x2) = A__2NDSNEG(x1) s(x1) = s(x1) cons(x1, x2) = x1 A__2NDSPOS(x1, x2) = A__2NDSPOS(x1) mark(x1) = x1 from(x1) = x1 a__from(x1) = x1 2ndspos(x1, x2) = x1 a__2ndspos(x1, x2) = x1 2ndsneg(x1, x2) = x1 a__2ndsneg(x1, x2) = x1 pi(x1) = pi(x1) a__pi(x1) = a__pi(x1) plus(x1, x2) = plus(x1, x2) a__plus(x1, x2) = a__plus(x1, x2) 0 = 0 times(x1, x2) = times(x1, x2) a__times(x1, x2) = a__times(x1, x2) square(x1) = square(x1) a__square(x1) = a__square(x1) posrecip(x1) = posrecip negrecip(x1) = negrecip(x1) nil = nil rnil = rnil rcons(x1, x2) = rcons Recursive path order with status [RPO]. Quasi-Precedence: [pi_1, a__pi_1] > [A__2NDSNEG_1, A__2NDSPOS_1, 0, rnil] [square_1, a__square_1] > [times_2, a__times_2] > [plus_2, a__plus_2] > s_1 > negrecip_1 > [A__2NDSNEG_1, A__2NDSPOS_1, 0, rnil] [square_1, a__square_1] > [times_2, a__times_2] > [plus_2, a__plus_2] > s_1 > rcons > [A__2NDSNEG_1, A__2NDSPOS_1, 0, rnil] posrecip > [A__2NDSNEG_1, A__2NDSPOS_1, 0, rnil] nil > [A__2NDSNEG_1, A__2NDSPOS_1, 0, rnil] Status: A__2NDSNEG_1: multiset status s_1: multiset status A__2NDSPOS_1: multiset status pi_1: multiset status a__pi_1: multiset status plus_2: [1,2] a__plus_2: [1,2] 0: multiset status times_2: multiset status a__times_2: multiset status square_1: multiset status a__square_1: multiset status posrecip: multiset status negrecip_1: multiset status nil: multiset status rnil: multiset status rcons: multiset status The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented: mark(from(X)) -> a__from(mark(X)) mark(2ndspos(X1, X2)) -> a__2ndspos(mark(X1), mark(X2)) mark(2ndsneg(X1, X2)) -> a__2ndsneg(mark(X1), mark(X2)) mark(pi(X)) -> a__pi(mark(X)) mark(plus(X1, X2)) -> a__plus(mark(X1), mark(X2)) a__plus(0, Y) -> mark(Y) mark(times(X1, X2)) -> a__times(mark(X1), mark(X2)) a__times(s(X), Y) -> a__plus(mark(Y), a__times(mark(X), mark(Y))) mark(square(X)) -> a__square(mark(X)) a__square(X) -> a__times(mark(X), mark(X)) mark(0) -> 0 mark(s(X)) -> s(mark(X)) mark(posrecip(X)) -> posrecip(mark(X)) mark(negrecip(X)) -> negrecip(mark(X)) mark(nil) -> nil mark(cons(X1, X2)) -> cons(mark(X1), X2) mark(rnil) -> rnil mark(rcons(X1, X2)) -> rcons(mark(X1), mark(X2)) a__from(X) -> from(X) a__2ndspos(0, Z) -> rnil a__2ndspos(X1, X2) -> 2ndspos(X1, X2) a__2ndsneg(0, Z) -> rnil a__2ndsneg(X1, X2) -> 2ndsneg(X1, X2) a__pi(X) -> pi(X) a__plus(X1, X2) -> plus(X1, X2) a__times(0, Y) -> 0 a__times(X1, X2) -> times(X1, X2) a__square(X) -> square(X) a__plus(s(X), Y) -> s(a__plus(mark(X), mark(Y))) a__pi(X) -> a__2ndspos(mark(X), a__from(0)) a__from(X) -> cons(mark(X), from(s(X))) a__2ndspos(s(N), cons(X, cons(Y, Z))) -> rcons(posrecip(mark(Y)), a__2ndsneg(mark(N), mark(Z))) a__2ndsneg(s(N), cons(X, cons(Y, Z))) -> rcons(negrecip(mark(Y)), a__2ndspos(mark(N), mark(Z))) ---------------------------------------- (50) Obligation: Q DP problem: P is empty. The TRS R consists of the following rules: a__from(X) -> cons(mark(X), from(s(X))) a__2ndspos(0, Z) -> rnil a__2ndspos(s(N), cons(X, cons(Y, Z))) -> rcons(posrecip(mark(Y)), a__2ndsneg(mark(N), mark(Z))) a__2ndsneg(0, Z) -> rnil a__2ndsneg(s(N), cons(X, cons(Y, Z))) -> rcons(negrecip(mark(Y)), a__2ndspos(mark(N), mark(Z))) a__pi(X) -> a__2ndspos(mark(X), a__from(0)) a__plus(0, Y) -> mark(Y) a__plus(s(X), Y) -> s(a__plus(mark(X), mark(Y))) a__times(0, Y) -> 0 a__times(s(X), Y) -> a__plus(mark(Y), a__times(mark(X), mark(Y))) a__square(X) -> a__times(mark(X), mark(X)) mark(from(X)) -> a__from(mark(X)) mark(2ndspos(X1, X2)) -> a__2ndspos(mark(X1), mark(X2)) mark(2ndsneg(X1, X2)) -> a__2ndsneg(mark(X1), mark(X2)) mark(pi(X)) -> a__pi(mark(X)) mark(plus(X1, X2)) -> a__plus(mark(X1), mark(X2)) mark(times(X1, X2)) -> a__times(mark(X1), mark(X2)) mark(square(X)) -> a__square(mark(X)) mark(0) -> 0 mark(s(X)) -> s(mark(X)) mark(posrecip(X)) -> posrecip(mark(X)) mark(negrecip(X)) -> negrecip(mark(X)) mark(nil) -> nil mark(cons(X1, X2)) -> cons(mark(X1), X2) mark(rnil) -> rnil mark(rcons(X1, X2)) -> rcons(mark(X1), mark(X2)) a__from(X) -> from(X) a__2ndspos(X1, X2) -> 2ndspos(X1, X2) a__2ndsneg(X1, X2) -> 2ndsneg(X1, X2) a__pi(X) -> pi(X) a__plus(X1, X2) -> plus(X1, X2) a__times(X1, X2) -> times(X1, X2) a__square(X) -> square(X) Q is empty. We have to consider all minimal (P,Q,R)-chains. ---------------------------------------- (51) PisEmptyProof (EQUIVALENT) The TRS P is empty. Hence, there is no (P,Q,R) chain. ---------------------------------------- (52) YES