YES proof of Transformed_CSR_04_Ex1_2_AEL03_iGM.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, 30 ms] (2) QDP (3) DependencyGraphProof [EQUIVALENT, 0 ms] (4) AND (5) QDP (6) UsableRulesProof [EQUIVALENT, 0 ms] (7) QDP (8) QDPSizeChangeProof [EQUIVALENT, 0 ms] (9) YES (10) QDP (11) UsableRulesProof [EQUIVALENT, 0 ms] (12) QDP (13) QDPSizeChangeProof [EQUIVALENT, 0 ms] (14) YES (15) QDP (16) UsableRulesProof [EQUIVALENT, 0 ms] (17) QDP (18) QDPSizeChangeProof [EQUIVALENT, 0 ms] (19) YES (20) QDP (21) UsableRulesProof [EQUIVALENT, 0 ms] (22) QDP (23) QDPSizeChangeProof [EQUIVALENT, 0 ms] (24) YES (25) QDP (26) UsableRulesProof [EQUIVALENT, 0 ms] (27) QDP (28) QDPSizeChangeProof [EQUIVALENT, 0 ms] (29) YES (30) QDP (31) UsableRulesProof [EQUIVALENT, 0 ms] (32) QDP (33) QDPSizeChangeProof [EQUIVALENT, 0 ms] (34) YES (35) QDP (36) UsableRulesProof [EQUIVALENT, 0 ms] (37) QDP (38) QDPSizeChangeProof [EQUIVALENT, 0 ms] (39) YES (40) QDP (41) UsableRulesProof [EQUIVALENT, 0 ms] (42) QDP (43) QDPSizeChangeProof [EQUIVALENT, 0 ms] (44) YES (45) QDP (46) UsableRulesProof [EQUIVALENT, 0 ms] (47) QDP (48) QDPSizeChangeProof [EQUIVALENT, 0 ms] (49) YES (50) QDP (51) UsableRulesProof [EQUIVALENT, 0 ms] (52) QDP (53) QDPSizeChangeProof [EQUIVALENT, 0 ms] (54) YES (55) QDP (56) UsableRulesProof [EQUIVALENT, 0 ms] (57) QDP (58) QDPSizeChangeProof [EQUIVALENT, 0 ms] (59) YES (60) QDP (61) UsableRulesProof [EQUIVALENT, 0 ms] (62) QDP (63) QDPSizeChangeProof [EQUIVALENT, 0 ms] (64) YES (65) QDP (66) QDPOrderProof [EQUIVALENT, 242 ms] (67) QDP (68) QDPOrderProof [EQUIVALENT, 231 ms] (69) QDP (70) QDPOrderProof [EQUIVALENT, 140 ms] (71) QDP (72) QDPOrderProof [EQUIVALENT, 229 ms] (73) QDP (74) QDPOrderProof [EQUIVALENT, 99 ms] (75) QDP (76) QDPOrderProof [EQUIVALENT, 429 ms] (77) QDP (78) QDPOrderProof [EQUIVALENT, 254 ms] (79) QDP (80) QDPOrderProof [EQUIVALENT, 153 ms] (81) QDP (82) QDPOrderProof [EQUIVALENT, 239 ms] (83) QDP (84) QDPOrderProof [EQUIVALENT, 259 ms] (85) QDP (86) QDPOrderProof [EQUIVALENT, 360 ms] (87) QDP (88) QDPOrderProof [EQUIVALENT, 218 ms] (89) QDP (90) QDPOrderProof [EQUIVALENT, 144 ms] (91) QDP (92) QDPOrderProof [EQUIVALENT, 174 ms] (93) QDP (94) QDPOrderProof [EQUIVALENT, 362 ms] (95) QDP (96) QDPOrderProof [EQUIVALENT, 421 ms] (97) QDP (98) QDPOrderProof [EQUIVALENT, 174 ms] (99) QDP (100) QDPOrderProof [EQUIVALENT, 196 ms] (101) QDP (102) QDPOrderProof [EQUIVALENT, 205 ms] (103) QDP (104) QDPOrderProof [EQUIVALENT, 124 ms] (105) QDP (106) QDPOrderProof [EQUIVALENT, 113 ms] (107) QDP (108) QDPOrderProof [EQUIVALENT, 383 ms] (109) QDP (110) PisEmptyProof [EQUIVALENT, 0 ms] (111) YES ---------------------------------------- (0) Obligation: Q restricted rewrite system: The TRS R consists of the following rules: active(from(X)) -> mark(cons(X, from(s(X)))) active(2ndspos(0, Z)) -> mark(rnil) active(2ndspos(s(N), cons(X, cons(Y, Z)))) -> mark(rcons(posrecip(Y), 2ndsneg(N, Z))) active(2ndsneg(0, Z)) -> mark(rnil) active(2ndsneg(s(N), cons(X, cons(Y, Z)))) -> mark(rcons(negrecip(Y), 2ndspos(N, Z))) active(pi(X)) -> mark(2ndspos(X, from(0))) active(plus(0, Y)) -> mark(Y) active(plus(s(X), Y)) -> mark(s(plus(X, Y))) active(times(0, Y)) -> mark(0) active(times(s(X), Y)) -> mark(plus(Y, times(X, Y))) active(square(X)) -> mark(times(X, X)) mark(from(X)) -> active(from(mark(X))) mark(cons(X1, X2)) -> active(cons(mark(X1), X2)) mark(s(X)) -> active(s(mark(X))) mark(2ndspos(X1, X2)) -> active(2ndspos(mark(X1), mark(X2))) mark(0) -> active(0) mark(rnil) -> active(rnil) mark(rcons(X1, X2)) -> active(rcons(mark(X1), mark(X2))) mark(posrecip(X)) -> active(posrecip(mark(X))) mark(2ndsneg(X1, X2)) -> active(2ndsneg(mark(X1), mark(X2))) mark(negrecip(X)) -> active(negrecip(mark(X))) mark(pi(X)) -> active(pi(mark(X))) mark(plus(X1, X2)) -> active(plus(mark(X1), mark(X2))) mark(times(X1, X2)) -> active(times(mark(X1), mark(X2))) mark(square(X)) -> active(square(mark(X))) from(mark(X)) -> from(X) from(active(X)) -> from(X) cons(mark(X1), X2) -> cons(X1, X2) cons(X1, mark(X2)) -> cons(X1, X2) cons(active(X1), X2) -> cons(X1, X2) cons(X1, active(X2)) -> cons(X1, X2) s(mark(X)) -> s(X) s(active(X)) -> s(X) 2ndspos(mark(X1), X2) -> 2ndspos(X1, X2) 2ndspos(X1, mark(X2)) -> 2ndspos(X1, X2) 2ndspos(active(X1), X2) -> 2ndspos(X1, X2) 2ndspos(X1, active(X2)) -> 2ndspos(X1, X2) rcons(mark(X1), X2) -> rcons(X1, X2) rcons(X1, mark(X2)) -> rcons(X1, X2) rcons(active(X1), X2) -> rcons(X1, X2) rcons(X1, active(X2)) -> rcons(X1, X2) posrecip(mark(X)) -> posrecip(X) posrecip(active(X)) -> posrecip(X) 2ndsneg(mark(X1), X2) -> 2ndsneg(X1, X2) 2ndsneg(X1, mark(X2)) -> 2ndsneg(X1, X2) 2ndsneg(active(X1), X2) -> 2ndsneg(X1, X2) 2ndsneg(X1, active(X2)) -> 2ndsneg(X1, X2) negrecip(mark(X)) -> negrecip(X) negrecip(active(X)) -> negrecip(X) pi(mark(X)) -> pi(X) pi(active(X)) -> pi(X) plus(mark(X1), X2) -> plus(X1, X2) plus(X1, mark(X2)) -> plus(X1, X2) plus(active(X1), X2) -> plus(X1, X2) plus(X1, active(X2)) -> plus(X1, X2) times(mark(X1), X2) -> times(X1, X2) times(X1, mark(X2)) -> times(X1, X2) times(active(X1), X2) -> times(X1, X2) times(X1, active(X2)) -> times(X1, X2) square(mark(X)) -> square(X) square(active(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: ACTIVE(from(X)) -> MARK(cons(X, from(s(X)))) ACTIVE(from(X)) -> CONS(X, from(s(X))) ACTIVE(from(X)) -> FROM(s(X)) ACTIVE(from(X)) -> S(X) ACTIVE(2ndspos(0, Z)) -> MARK(rnil) ACTIVE(2ndspos(s(N), cons(X, cons(Y, Z)))) -> MARK(rcons(posrecip(Y), 2ndsneg(N, Z))) ACTIVE(2ndspos(s(N), cons(X, cons(Y, Z)))) -> RCONS(posrecip(Y), 2ndsneg(N, Z)) ACTIVE(2ndspos(s(N), cons(X, cons(Y, Z)))) -> POSRECIP(Y) ACTIVE(2ndspos(s(N), cons(X, cons(Y, Z)))) -> 2NDSNEG(N, Z) ACTIVE(2ndsneg(0, Z)) -> MARK(rnil) ACTIVE(2ndsneg(s(N), cons(X, cons(Y, Z)))) -> MARK(rcons(negrecip(Y), 2ndspos(N, Z))) ACTIVE(2ndsneg(s(N), cons(X, cons(Y, Z)))) -> RCONS(negrecip(Y), 2ndspos(N, Z)) ACTIVE(2ndsneg(s(N), cons(X, cons(Y, Z)))) -> NEGRECIP(Y) ACTIVE(2ndsneg(s(N), cons(X, cons(Y, Z)))) -> 2NDSPOS(N, Z) ACTIVE(pi(X)) -> MARK(2ndspos(X, from(0))) ACTIVE(pi(X)) -> 2NDSPOS(X, from(0)) ACTIVE(pi(X)) -> FROM(0) ACTIVE(plus(0, Y)) -> MARK(Y) ACTIVE(plus(s(X), Y)) -> MARK(s(plus(X, Y))) ACTIVE(plus(s(X), Y)) -> S(plus(X, Y)) ACTIVE(plus(s(X), Y)) -> PLUS(X, Y) ACTIVE(times(0, Y)) -> MARK(0) ACTIVE(times(s(X), Y)) -> MARK(plus(Y, times(X, Y))) ACTIVE(times(s(X), Y)) -> PLUS(Y, times(X, Y)) ACTIVE(times(s(X), Y)) -> TIMES(X, Y) ACTIVE(square(X)) -> MARK(times(X, X)) ACTIVE(square(X)) -> TIMES(X, X) MARK(from(X)) -> ACTIVE(from(mark(X))) MARK(from(X)) -> FROM(mark(X)) MARK(from(X)) -> MARK(X) MARK(cons(X1, X2)) -> ACTIVE(cons(mark(X1), X2)) MARK(cons(X1, X2)) -> CONS(mark(X1), X2) MARK(cons(X1, X2)) -> MARK(X1) MARK(s(X)) -> ACTIVE(s(mark(X))) MARK(s(X)) -> S(mark(X)) MARK(s(X)) -> MARK(X) MARK(2ndspos(X1, X2)) -> ACTIVE(2ndspos(mark(X1), mark(X2))) MARK(2ndspos(X1, X2)) -> 2NDSPOS(mark(X1), mark(X2)) MARK(2ndspos(X1, X2)) -> MARK(X1) MARK(2ndspos(X1, X2)) -> MARK(X2) MARK(0) -> ACTIVE(0) MARK(rnil) -> ACTIVE(rnil) MARK(rcons(X1, X2)) -> ACTIVE(rcons(mark(X1), mark(X2))) MARK(rcons(X1, X2)) -> RCONS(mark(X1), mark(X2)) MARK(rcons(X1, X2)) -> MARK(X1) MARK(rcons(X1, X2)) -> MARK(X2) MARK(posrecip(X)) -> ACTIVE(posrecip(mark(X))) MARK(posrecip(X)) -> POSRECIP(mark(X)) MARK(posrecip(X)) -> MARK(X) MARK(2ndsneg(X1, X2)) -> ACTIVE(2ndsneg(mark(X1), mark(X2))) MARK(2ndsneg(X1, X2)) -> 2NDSNEG(mark(X1), mark(X2)) MARK(2ndsneg(X1, X2)) -> MARK(X1) MARK(2ndsneg(X1, X2)) -> MARK(X2) MARK(negrecip(X)) -> ACTIVE(negrecip(mark(X))) MARK(negrecip(X)) -> NEGRECIP(mark(X)) MARK(negrecip(X)) -> MARK(X) MARK(pi(X)) -> ACTIVE(pi(mark(X))) MARK(pi(X)) -> PI(mark(X)) MARK(pi(X)) -> MARK(X) MARK(plus(X1, X2)) -> ACTIVE(plus(mark(X1), mark(X2))) MARK(plus(X1, X2)) -> PLUS(mark(X1), mark(X2)) MARK(plus(X1, X2)) -> MARK(X1) MARK(plus(X1, X2)) -> MARK(X2) MARK(times(X1, X2)) -> ACTIVE(times(mark(X1), mark(X2))) MARK(times(X1, X2)) -> TIMES(mark(X1), mark(X2)) MARK(times(X1, X2)) -> MARK(X1) MARK(times(X1, X2)) -> MARK(X2) MARK(square(X)) -> ACTIVE(square(mark(X))) MARK(square(X)) -> SQUARE(mark(X)) MARK(square(X)) -> MARK(X) FROM(mark(X)) -> FROM(X) FROM(active(X)) -> FROM(X) CONS(mark(X1), X2) -> CONS(X1, X2) CONS(X1, mark(X2)) -> CONS(X1, X2) CONS(active(X1), X2) -> CONS(X1, X2) CONS(X1, active(X2)) -> CONS(X1, X2) S(mark(X)) -> S(X) S(active(X)) -> S(X) 2NDSPOS(mark(X1), X2) -> 2NDSPOS(X1, X2) 2NDSPOS(X1, mark(X2)) -> 2NDSPOS(X1, X2) 2NDSPOS(active(X1), X2) -> 2NDSPOS(X1, X2) 2NDSPOS(X1, active(X2)) -> 2NDSPOS(X1, X2) RCONS(mark(X1), X2) -> RCONS(X1, X2) RCONS(X1, mark(X2)) -> RCONS(X1, X2) RCONS(active(X1), X2) -> RCONS(X1, X2) RCONS(X1, active(X2)) -> RCONS(X1, X2) POSRECIP(mark(X)) -> POSRECIP(X) POSRECIP(active(X)) -> POSRECIP(X) 2NDSNEG(mark(X1), X2) -> 2NDSNEG(X1, X2) 2NDSNEG(X1, mark(X2)) -> 2NDSNEG(X1, X2) 2NDSNEG(active(X1), X2) -> 2NDSNEG(X1, X2) 2NDSNEG(X1, active(X2)) -> 2NDSNEG(X1, X2) NEGRECIP(mark(X)) -> NEGRECIP(X) NEGRECIP(active(X)) -> NEGRECIP(X) PI(mark(X)) -> PI(X) PI(active(X)) -> PI(X) PLUS(mark(X1), X2) -> PLUS(X1, X2) PLUS(X1, mark(X2)) -> PLUS(X1, X2) PLUS(active(X1), X2) -> PLUS(X1, X2) PLUS(X1, active(X2)) -> PLUS(X1, X2) TIMES(mark(X1), X2) -> TIMES(X1, X2) TIMES(X1, mark(X2)) -> TIMES(X1, X2) TIMES(active(X1), X2) -> TIMES(X1, X2) TIMES(X1, active(X2)) -> TIMES(X1, X2) SQUARE(mark(X)) -> SQUARE(X) SQUARE(active(X)) -> SQUARE(X) The TRS R consists of the following rules: active(from(X)) -> mark(cons(X, from(s(X)))) active(2ndspos(0, Z)) -> mark(rnil) active(2ndspos(s(N), cons(X, cons(Y, Z)))) -> mark(rcons(posrecip(Y), 2ndsneg(N, Z))) active(2ndsneg(0, Z)) -> mark(rnil) active(2ndsneg(s(N), cons(X, cons(Y, Z)))) -> mark(rcons(negrecip(Y), 2ndspos(N, Z))) active(pi(X)) -> mark(2ndspos(X, from(0))) active(plus(0, Y)) -> mark(Y) active(plus(s(X), Y)) -> mark(s(plus(X, Y))) active(times(0, Y)) -> mark(0) active(times(s(X), Y)) -> mark(plus(Y, times(X, Y))) active(square(X)) -> mark(times(X, X)) mark(from(X)) -> active(from(mark(X))) mark(cons(X1, X2)) -> active(cons(mark(X1), X2)) mark(s(X)) -> active(s(mark(X))) mark(2ndspos(X1, X2)) -> active(2ndspos(mark(X1), mark(X2))) mark(0) -> active(0) mark(rnil) -> active(rnil) mark(rcons(X1, X2)) -> active(rcons(mark(X1), mark(X2))) mark(posrecip(X)) -> active(posrecip(mark(X))) mark(2ndsneg(X1, X2)) -> active(2ndsneg(mark(X1), mark(X2))) mark(negrecip(X)) -> active(negrecip(mark(X))) mark(pi(X)) -> active(pi(mark(X))) mark(plus(X1, X2)) -> active(plus(mark(X1), mark(X2))) mark(times(X1, X2)) -> active(times(mark(X1), mark(X2))) mark(square(X)) -> active(square(mark(X))) from(mark(X)) -> from(X) from(active(X)) -> from(X) cons(mark(X1), X2) -> cons(X1, X2) cons(X1, mark(X2)) -> cons(X1, X2) cons(active(X1), X2) -> cons(X1, X2) cons(X1, active(X2)) -> cons(X1, X2) s(mark(X)) -> s(X) s(active(X)) -> s(X) 2ndspos(mark(X1), X2) -> 2ndspos(X1, X2) 2ndspos(X1, mark(X2)) -> 2ndspos(X1, X2) 2ndspos(active(X1), X2) -> 2ndspos(X1, X2) 2ndspos(X1, active(X2)) -> 2ndspos(X1, X2) rcons(mark(X1), X2) -> rcons(X1, X2) rcons(X1, mark(X2)) -> rcons(X1, X2) rcons(active(X1), X2) -> rcons(X1, X2) rcons(X1, active(X2)) -> rcons(X1, X2) posrecip(mark(X)) -> posrecip(X) posrecip(active(X)) -> posrecip(X) 2ndsneg(mark(X1), X2) -> 2ndsneg(X1, X2) 2ndsneg(X1, mark(X2)) -> 2ndsneg(X1, X2) 2ndsneg(active(X1), X2) -> 2ndsneg(X1, X2) 2ndsneg(X1, active(X2)) -> 2ndsneg(X1, X2) negrecip(mark(X)) -> negrecip(X) negrecip(active(X)) -> negrecip(X) pi(mark(X)) -> pi(X) pi(active(X)) -> pi(X) plus(mark(X1), X2) -> plus(X1, X2) plus(X1, mark(X2)) -> plus(X1, X2) plus(active(X1), X2) -> plus(X1, X2) plus(X1, active(X2)) -> plus(X1, X2) times(mark(X1), X2) -> times(X1, X2) times(X1, mark(X2)) -> times(X1, X2) times(active(X1), X2) -> times(X1, X2) times(X1, active(X2)) -> times(X1, X2) square(mark(X)) -> square(X) square(active(X)) -> square(X) Q is empty. We have to consider all minimal (P,Q,R)-chains. ---------------------------------------- (3) DependencyGraphProof (EQUIVALENT) The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 13 SCCs with 33 less nodes. ---------------------------------------- (4) Complex Obligation (AND) ---------------------------------------- (5) Obligation: Q DP problem: The TRS P consists of the following rules: SQUARE(active(X)) -> SQUARE(X) SQUARE(mark(X)) -> SQUARE(X) The TRS R consists of the following rules: active(from(X)) -> mark(cons(X, from(s(X)))) active(2ndspos(0, Z)) -> mark(rnil) active(2ndspos(s(N), cons(X, cons(Y, Z)))) -> mark(rcons(posrecip(Y), 2ndsneg(N, Z))) active(2ndsneg(0, Z)) -> mark(rnil) active(2ndsneg(s(N), cons(X, cons(Y, Z)))) -> mark(rcons(negrecip(Y), 2ndspos(N, Z))) active(pi(X)) -> mark(2ndspos(X, from(0))) active(plus(0, Y)) -> mark(Y) active(plus(s(X), Y)) -> mark(s(plus(X, Y))) active(times(0, Y)) -> mark(0) active(times(s(X), Y)) -> mark(plus(Y, times(X, Y))) active(square(X)) -> mark(times(X, X)) mark(from(X)) -> active(from(mark(X))) mark(cons(X1, X2)) -> active(cons(mark(X1), X2)) mark(s(X)) -> active(s(mark(X))) mark(2ndspos(X1, X2)) -> active(2ndspos(mark(X1), mark(X2))) mark(0) -> active(0) mark(rnil) -> active(rnil) mark(rcons(X1, X2)) -> active(rcons(mark(X1), mark(X2))) mark(posrecip(X)) -> active(posrecip(mark(X))) mark(2ndsneg(X1, X2)) -> active(2ndsneg(mark(X1), mark(X2))) mark(negrecip(X)) -> active(negrecip(mark(X))) mark(pi(X)) -> active(pi(mark(X))) mark(plus(X1, X2)) -> active(plus(mark(X1), mark(X2))) mark(times(X1, X2)) -> active(times(mark(X1), mark(X2))) mark(square(X)) -> active(square(mark(X))) from(mark(X)) -> from(X) from(active(X)) -> from(X) cons(mark(X1), X2) -> cons(X1, X2) cons(X1, mark(X2)) -> cons(X1, X2) cons(active(X1), X2) -> cons(X1, X2) cons(X1, active(X2)) -> cons(X1, X2) s(mark(X)) -> s(X) s(active(X)) -> s(X) 2ndspos(mark(X1), X2) -> 2ndspos(X1, X2) 2ndspos(X1, mark(X2)) -> 2ndspos(X1, X2) 2ndspos(active(X1), X2) -> 2ndspos(X1, X2) 2ndspos(X1, active(X2)) -> 2ndspos(X1, X2) rcons(mark(X1), X2) -> rcons(X1, X2) rcons(X1, mark(X2)) -> rcons(X1, X2) rcons(active(X1), X2) -> rcons(X1, X2) rcons(X1, active(X2)) -> rcons(X1, X2) posrecip(mark(X)) -> posrecip(X) posrecip(active(X)) -> posrecip(X) 2ndsneg(mark(X1), X2) -> 2ndsneg(X1, X2) 2ndsneg(X1, mark(X2)) -> 2ndsneg(X1, X2) 2ndsneg(active(X1), X2) -> 2ndsneg(X1, X2) 2ndsneg(X1, active(X2)) -> 2ndsneg(X1, X2) negrecip(mark(X)) -> negrecip(X) negrecip(active(X)) -> negrecip(X) pi(mark(X)) -> pi(X) pi(active(X)) -> pi(X) plus(mark(X1), X2) -> plus(X1, X2) plus(X1, mark(X2)) -> plus(X1, X2) plus(active(X1), X2) -> plus(X1, X2) plus(X1, active(X2)) -> plus(X1, X2) times(mark(X1), X2) -> times(X1, X2) times(X1, mark(X2)) -> times(X1, X2) times(active(X1), X2) -> times(X1, X2) times(X1, active(X2)) -> times(X1, X2) square(mark(X)) -> square(X) square(active(X)) -> square(X) Q is empty. We have to consider all minimal (P,Q,R)-chains. ---------------------------------------- (6) 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. ---------------------------------------- (7) Obligation: Q DP problem: The TRS P consists of the following rules: SQUARE(active(X)) -> SQUARE(X) SQUARE(mark(X)) -> SQUARE(X) R is empty. Q is empty. We have to consider all minimal (P,Q,R)-chains. ---------------------------------------- (8) 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: *SQUARE(active(X)) -> SQUARE(X) The graph contains the following edges 1 > 1 *SQUARE(mark(X)) -> SQUARE(X) The graph contains the following edges 1 > 1 ---------------------------------------- (9) YES ---------------------------------------- (10) Obligation: Q DP problem: The TRS P consists of the following rules: TIMES(X1, mark(X2)) -> TIMES(X1, X2) TIMES(mark(X1), X2) -> TIMES(X1, X2) TIMES(active(X1), X2) -> TIMES(X1, X2) TIMES(X1, active(X2)) -> TIMES(X1, X2) The TRS R consists of the following rules: active(from(X)) -> mark(cons(X, from(s(X)))) active(2ndspos(0, Z)) -> mark(rnil) active(2ndspos(s(N), cons(X, cons(Y, Z)))) -> mark(rcons(posrecip(Y), 2ndsneg(N, Z))) active(2ndsneg(0, Z)) -> mark(rnil) active(2ndsneg(s(N), cons(X, cons(Y, Z)))) -> mark(rcons(negrecip(Y), 2ndspos(N, Z))) active(pi(X)) -> mark(2ndspos(X, from(0))) active(plus(0, Y)) -> mark(Y) active(plus(s(X), Y)) -> mark(s(plus(X, Y))) active(times(0, Y)) -> mark(0) active(times(s(X), Y)) -> mark(plus(Y, times(X, Y))) active(square(X)) -> mark(times(X, X)) mark(from(X)) -> active(from(mark(X))) mark(cons(X1, X2)) -> active(cons(mark(X1), X2)) mark(s(X)) -> active(s(mark(X))) mark(2ndspos(X1, X2)) -> active(2ndspos(mark(X1), mark(X2))) mark(0) -> active(0) mark(rnil) -> active(rnil) mark(rcons(X1, X2)) -> active(rcons(mark(X1), mark(X2))) mark(posrecip(X)) -> active(posrecip(mark(X))) mark(2ndsneg(X1, X2)) -> active(2ndsneg(mark(X1), mark(X2))) mark(negrecip(X)) -> active(negrecip(mark(X))) mark(pi(X)) -> active(pi(mark(X))) mark(plus(X1, X2)) -> active(plus(mark(X1), mark(X2))) mark(times(X1, X2)) -> active(times(mark(X1), mark(X2))) mark(square(X)) -> active(square(mark(X))) from(mark(X)) -> from(X) from(active(X)) -> from(X) cons(mark(X1), X2) -> cons(X1, X2) cons(X1, mark(X2)) -> cons(X1, X2) cons(active(X1), X2) -> cons(X1, X2) cons(X1, active(X2)) -> cons(X1, X2) s(mark(X)) -> s(X) s(active(X)) -> s(X) 2ndspos(mark(X1), X2) -> 2ndspos(X1, X2) 2ndspos(X1, mark(X2)) -> 2ndspos(X1, X2) 2ndspos(active(X1), X2) -> 2ndspos(X1, X2) 2ndspos(X1, active(X2)) -> 2ndspos(X1, X2) rcons(mark(X1), X2) -> rcons(X1, X2) rcons(X1, mark(X2)) -> rcons(X1, X2) rcons(active(X1), X2) -> rcons(X1, X2) rcons(X1, active(X2)) -> rcons(X1, X2) posrecip(mark(X)) -> posrecip(X) posrecip(active(X)) -> posrecip(X) 2ndsneg(mark(X1), X2) -> 2ndsneg(X1, X2) 2ndsneg(X1, mark(X2)) -> 2ndsneg(X1, X2) 2ndsneg(active(X1), X2) -> 2ndsneg(X1, X2) 2ndsneg(X1, active(X2)) -> 2ndsneg(X1, X2) negrecip(mark(X)) -> negrecip(X) negrecip(active(X)) -> negrecip(X) pi(mark(X)) -> pi(X) pi(active(X)) -> pi(X) plus(mark(X1), X2) -> plus(X1, X2) plus(X1, mark(X2)) -> plus(X1, X2) plus(active(X1), X2) -> plus(X1, X2) plus(X1, active(X2)) -> plus(X1, X2) times(mark(X1), X2) -> times(X1, X2) times(X1, mark(X2)) -> times(X1, X2) times(active(X1), X2) -> times(X1, X2) times(X1, active(X2)) -> times(X1, X2) square(mark(X)) -> square(X) square(active(X)) -> square(X) Q is empty. We have to consider all minimal (P,Q,R)-chains. ---------------------------------------- (11) 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. ---------------------------------------- (12) Obligation: Q DP problem: The TRS P consists of the following rules: TIMES(X1, mark(X2)) -> TIMES(X1, X2) TIMES(mark(X1), X2) -> TIMES(X1, X2) TIMES(active(X1), X2) -> TIMES(X1, X2) TIMES(X1, active(X2)) -> TIMES(X1, X2) R is empty. Q is empty. We have to consider all minimal (P,Q,R)-chains. ---------------------------------------- (13) 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: *TIMES(X1, mark(X2)) -> TIMES(X1, X2) The graph contains the following edges 1 >= 1, 2 > 2 *TIMES(mark(X1), X2) -> TIMES(X1, X2) The graph contains the following edges 1 > 1, 2 >= 2 *TIMES(active(X1), X2) -> TIMES(X1, X2) The graph contains the following edges 1 > 1, 2 >= 2 *TIMES(X1, active(X2)) -> TIMES(X1, X2) The graph contains the following edges 1 >= 1, 2 > 2 ---------------------------------------- (14) YES ---------------------------------------- (15) Obligation: Q DP problem: The TRS P consists of the following rules: PLUS(X1, mark(X2)) -> PLUS(X1, X2) PLUS(mark(X1), X2) -> PLUS(X1, X2) PLUS(active(X1), X2) -> PLUS(X1, X2) PLUS(X1, active(X2)) -> PLUS(X1, X2) The TRS R consists of the following rules: active(from(X)) -> mark(cons(X, from(s(X)))) active(2ndspos(0, Z)) -> mark(rnil) active(2ndspos(s(N), cons(X, cons(Y, Z)))) -> mark(rcons(posrecip(Y), 2ndsneg(N, Z))) active(2ndsneg(0, Z)) -> mark(rnil) active(2ndsneg(s(N), cons(X, cons(Y, Z)))) -> mark(rcons(negrecip(Y), 2ndspos(N, Z))) active(pi(X)) -> mark(2ndspos(X, from(0))) active(plus(0, Y)) -> mark(Y) active(plus(s(X), Y)) -> mark(s(plus(X, Y))) active(times(0, Y)) -> mark(0) active(times(s(X), Y)) -> mark(plus(Y, times(X, Y))) active(square(X)) -> mark(times(X, X)) mark(from(X)) -> active(from(mark(X))) mark(cons(X1, X2)) -> active(cons(mark(X1), X2)) mark(s(X)) -> active(s(mark(X))) mark(2ndspos(X1, X2)) -> active(2ndspos(mark(X1), mark(X2))) mark(0) -> active(0) mark(rnil) -> active(rnil) mark(rcons(X1, X2)) -> active(rcons(mark(X1), mark(X2))) mark(posrecip(X)) -> active(posrecip(mark(X))) mark(2ndsneg(X1, X2)) -> active(2ndsneg(mark(X1), mark(X2))) mark(negrecip(X)) -> active(negrecip(mark(X))) mark(pi(X)) -> active(pi(mark(X))) mark(plus(X1, X2)) -> active(plus(mark(X1), mark(X2))) mark(times(X1, X2)) -> active(times(mark(X1), mark(X2))) mark(square(X)) -> active(square(mark(X))) from(mark(X)) -> from(X) from(active(X)) -> from(X) cons(mark(X1), X2) -> cons(X1, X2) cons(X1, mark(X2)) -> cons(X1, X2) cons(active(X1), X2) -> cons(X1, X2) cons(X1, active(X2)) -> cons(X1, X2) s(mark(X)) -> s(X) s(active(X)) -> s(X) 2ndspos(mark(X1), X2) -> 2ndspos(X1, X2) 2ndspos(X1, mark(X2)) -> 2ndspos(X1, X2) 2ndspos(active(X1), X2) -> 2ndspos(X1, X2) 2ndspos(X1, active(X2)) -> 2ndspos(X1, X2) rcons(mark(X1), X2) -> rcons(X1, X2) rcons(X1, mark(X2)) -> rcons(X1, X2) rcons(active(X1), X2) -> rcons(X1, X2) rcons(X1, active(X2)) -> rcons(X1, X2) posrecip(mark(X)) -> posrecip(X) posrecip(active(X)) -> posrecip(X) 2ndsneg(mark(X1), X2) -> 2ndsneg(X1, X2) 2ndsneg(X1, mark(X2)) -> 2ndsneg(X1, X2) 2ndsneg(active(X1), X2) -> 2ndsneg(X1, X2) 2ndsneg(X1, active(X2)) -> 2ndsneg(X1, X2) negrecip(mark(X)) -> negrecip(X) negrecip(active(X)) -> negrecip(X) pi(mark(X)) -> pi(X) pi(active(X)) -> pi(X) plus(mark(X1), X2) -> plus(X1, X2) plus(X1, mark(X2)) -> plus(X1, X2) plus(active(X1), X2) -> plus(X1, X2) plus(X1, active(X2)) -> plus(X1, X2) times(mark(X1), X2) -> times(X1, X2) times(X1, mark(X2)) -> times(X1, X2) times(active(X1), X2) -> times(X1, X2) times(X1, active(X2)) -> times(X1, X2) square(mark(X)) -> square(X) square(active(X)) -> square(X) Q is empty. We have to consider all minimal (P,Q,R)-chains. ---------------------------------------- (16) 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. ---------------------------------------- (17) Obligation: Q DP problem: The TRS P consists of the following rules: PLUS(X1, mark(X2)) -> PLUS(X1, X2) PLUS(mark(X1), X2) -> PLUS(X1, X2) PLUS(active(X1), X2) -> PLUS(X1, X2) PLUS(X1, active(X2)) -> PLUS(X1, X2) R is empty. Q is empty. We have to consider all minimal (P,Q,R)-chains. ---------------------------------------- (18) 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: *PLUS(X1, mark(X2)) -> PLUS(X1, X2) The graph contains the following edges 1 >= 1, 2 > 2 *PLUS(mark(X1), X2) -> PLUS(X1, X2) The graph contains the following edges 1 > 1, 2 >= 2 *PLUS(active(X1), X2) -> PLUS(X1, X2) The graph contains the following edges 1 > 1, 2 >= 2 *PLUS(X1, active(X2)) -> PLUS(X1, X2) The graph contains the following edges 1 >= 1, 2 > 2 ---------------------------------------- (19) YES ---------------------------------------- (20) Obligation: Q DP problem: The TRS P consists of the following rules: PI(active(X)) -> PI(X) PI(mark(X)) -> PI(X) The TRS R consists of the following rules: active(from(X)) -> mark(cons(X, from(s(X)))) active(2ndspos(0, Z)) -> mark(rnil) active(2ndspos(s(N), cons(X, cons(Y, Z)))) -> mark(rcons(posrecip(Y), 2ndsneg(N, Z))) active(2ndsneg(0, Z)) -> mark(rnil) active(2ndsneg(s(N), cons(X, cons(Y, Z)))) -> mark(rcons(negrecip(Y), 2ndspos(N, Z))) active(pi(X)) -> mark(2ndspos(X, from(0))) active(plus(0, Y)) -> mark(Y) active(plus(s(X), Y)) -> mark(s(plus(X, Y))) active(times(0, Y)) -> mark(0) active(times(s(X), Y)) -> mark(plus(Y, times(X, Y))) active(square(X)) -> mark(times(X, X)) mark(from(X)) -> active(from(mark(X))) mark(cons(X1, X2)) -> active(cons(mark(X1), X2)) mark(s(X)) -> active(s(mark(X))) mark(2ndspos(X1, X2)) -> active(2ndspos(mark(X1), mark(X2))) mark(0) -> active(0) mark(rnil) -> active(rnil) mark(rcons(X1, X2)) -> active(rcons(mark(X1), mark(X2))) mark(posrecip(X)) -> active(posrecip(mark(X))) mark(2ndsneg(X1, X2)) -> active(2ndsneg(mark(X1), mark(X2))) mark(negrecip(X)) -> active(negrecip(mark(X))) mark(pi(X)) -> active(pi(mark(X))) mark(plus(X1, X2)) -> active(plus(mark(X1), mark(X2))) mark(times(X1, X2)) -> active(times(mark(X1), mark(X2))) mark(square(X)) -> active(square(mark(X))) from(mark(X)) -> from(X) from(active(X)) -> from(X) cons(mark(X1), X2) -> cons(X1, X2) cons(X1, mark(X2)) -> cons(X1, X2) cons(active(X1), X2) -> cons(X1, X2) cons(X1, active(X2)) -> cons(X1, X2) s(mark(X)) -> s(X) s(active(X)) -> s(X) 2ndspos(mark(X1), X2) -> 2ndspos(X1, X2) 2ndspos(X1, mark(X2)) -> 2ndspos(X1, X2) 2ndspos(active(X1), X2) -> 2ndspos(X1, X2) 2ndspos(X1, active(X2)) -> 2ndspos(X1, X2) rcons(mark(X1), X2) -> rcons(X1, X2) rcons(X1, mark(X2)) -> rcons(X1, X2) rcons(active(X1), X2) -> rcons(X1, X2) rcons(X1, active(X2)) -> rcons(X1, X2) posrecip(mark(X)) -> posrecip(X) posrecip(active(X)) -> posrecip(X) 2ndsneg(mark(X1), X2) -> 2ndsneg(X1, X2) 2ndsneg(X1, mark(X2)) -> 2ndsneg(X1, X2) 2ndsneg(active(X1), X2) -> 2ndsneg(X1, X2) 2ndsneg(X1, active(X2)) -> 2ndsneg(X1, X2) negrecip(mark(X)) -> negrecip(X) negrecip(active(X)) -> negrecip(X) pi(mark(X)) -> pi(X) pi(active(X)) -> pi(X) plus(mark(X1), X2) -> plus(X1, X2) plus(X1, mark(X2)) -> plus(X1, X2) plus(active(X1), X2) -> plus(X1, X2) plus(X1, active(X2)) -> plus(X1, X2) times(mark(X1), X2) -> times(X1, X2) times(X1, mark(X2)) -> times(X1, X2) times(active(X1), X2) -> times(X1, X2) times(X1, active(X2)) -> times(X1, X2) square(mark(X)) -> square(X) square(active(X)) -> square(X) Q is empty. We have to consider all minimal (P,Q,R)-chains. ---------------------------------------- (21) 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. ---------------------------------------- (22) Obligation: Q DP problem: The TRS P consists of the following rules: PI(active(X)) -> PI(X) PI(mark(X)) -> PI(X) R is empty. Q is empty. We have to consider all minimal (P,Q,R)-chains. ---------------------------------------- (23) 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: *PI(active(X)) -> PI(X) The graph contains the following edges 1 > 1 *PI(mark(X)) -> PI(X) The graph contains the following edges 1 > 1 ---------------------------------------- (24) YES ---------------------------------------- (25) Obligation: Q DP problem: The TRS P consists of the following rules: NEGRECIP(active(X)) -> NEGRECIP(X) NEGRECIP(mark(X)) -> NEGRECIP(X) The TRS R consists of the following rules: active(from(X)) -> mark(cons(X, from(s(X)))) active(2ndspos(0, Z)) -> mark(rnil) active(2ndspos(s(N), cons(X, cons(Y, Z)))) -> mark(rcons(posrecip(Y), 2ndsneg(N, Z))) active(2ndsneg(0, Z)) -> mark(rnil) active(2ndsneg(s(N), cons(X, cons(Y, Z)))) -> mark(rcons(negrecip(Y), 2ndspos(N, Z))) active(pi(X)) -> mark(2ndspos(X, from(0))) active(plus(0, Y)) -> mark(Y) active(plus(s(X), Y)) -> mark(s(plus(X, Y))) active(times(0, Y)) -> mark(0) active(times(s(X), Y)) -> mark(plus(Y, times(X, Y))) active(square(X)) -> mark(times(X, X)) mark(from(X)) -> active(from(mark(X))) mark(cons(X1, X2)) -> active(cons(mark(X1), X2)) mark(s(X)) -> active(s(mark(X))) mark(2ndspos(X1, X2)) -> active(2ndspos(mark(X1), mark(X2))) mark(0) -> active(0) mark(rnil) -> active(rnil) mark(rcons(X1, X2)) -> active(rcons(mark(X1), mark(X2))) mark(posrecip(X)) -> active(posrecip(mark(X))) mark(2ndsneg(X1, X2)) -> active(2ndsneg(mark(X1), mark(X2))) mark(negrecip(X)) -> active(negrecip(mark(X))) mark(pi(X)) -> active(pi(mark(X))) mark(plus(X1, X2)) -> active(plus(mark(X1), mark(X2))) mark(times(X1, X2)) -> active(times(mark(X1), mark(X2))) mark(square(X)) -> active(square(mark(X))) from(mark(X)) -> from(X) from(active(X)) -> from(X) cons(mark(X1), X2) -> cons(X1, X2) cons(X1, mark(X2)) -> cons(X1, X2) cons(active(X1), X2) -> cons(X1, X2) cons(X1, active(X2)) -> cons(X1, X2) s(mark(X)) -> s(X) s(active(X)) -> s(X) 2ndspos(mark(X1), X2) -> 2ndspos(X1, X2) 2ndspos(X1, mark(X2)) -> 2ndspos(X1, X2) 2ndspos(active(X1), X2) -> 2ndspos(X1, X2) 2ndspos(X1, active(X2)) -> 2ndspos(X1, X2) rcons(mark(X1), X2) -> rcons(X1, X2) rcons(X1, mark(X2)) -> rcons(X1, X2) rcons(active(X1), X2) -> rcons(X1, X2) rcons(X1, active(X2)) -> rcons(X1, X2) posrecip(mark(X)) -> posrecip(X) posrecip(active(X)) -> posrecip(X) 2ndsneg(mark(X1), X2) -> 2ndsneg(X1, X2) 2ndsneg(X1, mark(X2)) -> 2ndsneg(X1, X2) 2ndsneg(active(X1), X2) -> 2ndsneg(X1, X2) 2ndsneg(X1, active(X2)) -> 2ndsneg(X1, X2) negrecip(mark(X)) -> negrecip(X) negrecip(active(X)) -> negrecip(X) pi(mark(X)) -> pi(X) pi(active(X)) -> pi(X) plus(mark(X1), X2) -> plus(X1, X2) plus(X1, mark(X2)) -> plus(X1, X2) plus(active(X1), X2) -> plus(X1, X2) plus(X1, active(X2)) -> plus(X1, X2) times(mark(X1), X2) -> times(X1, X2) times(X1, mark(X2)) -> times(X1, X2) times(active(X1), X2) -> times(X1, X2) times(X1, active(X2)) -> times(X1, X2) square(mark(X)) -> square(X) square(active(X)) -> square(X) Q is empty. We have to consider all minimal (P,Q,R)-chains. ---------------------------------------- (26) 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. ---------------------------------------- (27) Obligation: Q DP problem: The TRS P consists of the following rules: NEGRECIP(active(X)) -> NEGRECIP(X) NEGRECIP(mark(X)) -> NEGRECIP(X) R is empty. Q is empty. We have to consider all minimal (P,Q,R)-chains. ---------------------------------------- (28) 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: *NEGRECIP(active(X)) -> NEGRECIP(X) The graph contains the following edges 1 > 1 *NEGRECIP(mark(X)) -> NEGRECIP(X) The graph contains the following edges 1 > 1 ---------------------------------------- (29) YES ---------------------------------------- (30) Obligation: Q DP problem: The TRS P consists of the following rules: 2NDSNEG(X1, mark(X2)) -> 2NDSNEG(X1, X2) 2NDSNEG(mark(X1), X2) -> 2NDSNEG(X1, X2) 2NDSNEG(active(X1), X2) -> 2NDSNEG(X1, X2) 2NDSNEG(X1, active(X2)) -> 2NDSNEG(X1, X2) The TRS R consists of the following rules: active(from(X)) -> mark(cons(X, from(s(X)))) active(2ndspos(0, Z)) -> mark(rnil) active(2ndspos(s(N), cons(X, cons(Y, Z)))) -> mark(rcons(posrecip(Y), 2ndsneg(N, Z))) active(2ndsneg(0, Z)) -> mark(rnil) active(2ndsneg(s(N), cons(X, cons(Y, Z)))) -> mark(rcons(negrecip(Y), 2ndspos(N, Z))) active(pi(X)) -> mark(2ndspos(X, from(0))) active(plus(0, Y)) -> mark(Y) active(plus(s(X), Y)) -> mark(s(plus(X, Y))) active(times(0, Y)) -> mark(0) active(times(s(X), Y)) -> mark(plus(Y, times(X, Y))) active(square(X)) -> mark(times(X, X)) mark(from(X)) -> active(from(mark(X))) mark(cons(X1, X2)) -> active(cons(mark(X1), X2)) mark(s(X)) -> active(s(mark(X))) mark(2ndspos(X1, X2)) -> active(2ndspos(mark(X1), mark(X2))) mark(0) -> active(0) mark(rnil) -> active(rnil) mark(rcons(X1, X2)) -> active(rcons(mark(X1), mark(X2))) mark(posrecip(X)) -> active(posrecip(mark(X))) mark(2ndsneg(X1, X2)) -> active(2ndsneg(mark(X1), mark(X2))) mark(negrecip(X)) -> active(negrecip(mark(X))) mark(pi(X)) -> active(pi(mark(X))) mark(plus(X1, X2)) -> active(plus(mark(X1), mark(X2))) mark(times(X1, X2)) -> active(times(mark(X1), mark(X2))) mark(square(X)) -> active(square(mark(X))) from(mark(X)) -> from(X) from(active(X)) -> from(X) cons(mark(X1), X2) -> cons(X1, X2) cons(X1, mark(X2)) -> cons(X1, X2) cons(active(X1), X2) -> cons(X1, X2) cons(X1, active(X2)) -> cons(X1, X2) s(mark(X)) -> s(X) s(active(X)) -> s(X) 2ndspos(mark(X1), X2) -> 2ndspos(X1, X2) 2ndspos(X1, mark(X2)) -> 2ndspos(X1, X2) 2ndspos(active(X1), X2) -> 2ndspos(X1, X2) 2ndspos(X1, active(X2)) -> 2ndspos(X1, X2) rcons(mark(X1), X2) -> rcons(X1, X2) rcons(X1, mark(X2)) -> rcons(X1, X2) rcons(active(X1), X2) -> rcons(X1, X2) rcons(X1, active(X2)) -> rcons(X1, X2) posrecip(mark(X)) -> posrecip(X) posrecip(active(X)) -> posrecip(X) 2ndsneg(mark(X1), X2) -> 2ndsneg(X1, X2) 2ndsneg(X1, mark(X2)) -> 2ndsneg(X1, X2) 2ndsneg(active(X1), X2) -> 2ndsneg(X1, X2) 2ndsneg(X1, active(X2)) -> 2ndsneg(X1, X2) negrecip(mark(X)) -> negrecip(X) negrecip(active(X)) -> negrecip(X) pi(mark(X)) -> pi(X) pi(active(X)) -> pi(X) plus(mark(X1), X2) -> plus(X1, X2) plus(X1, mark(X2)) -> plus(X1, X2) plus(active(X1), X2) -> plus(X1, X2) plus(X1, active(X2)) -> plus(X1, X2) times(mark(X1), X2) -> times(X1, X2) times(X1, mark(X2)) -> times(X1, X2) times(active(X1), X2) -> times(X1, X2) times(X1, active(X2)) -> times(X1, X2) square(mark(X)) -> square(X) square(active(X)) -> square(X) Q is empty. We have to consider all minimal (P,Q,R)-chains. ---------------------------------------- (31) 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. ---------------------------------------- (32) Obligation: Q DP problem: The TRS P consists of the following rules: 2NDSNEG(X1, mark(X2)) -> 2NDSNEG(X1, X2) 2NDSNEG(mark(X1), X2) -> 2NDSNEG(X1, X2) 2NDSNEG(active(X1), X2) -> 2NDSNEG(X1, X2) 2NDSNEG(X1, active(X2)) -> 2NDSNEG(X1, X2) R is empty. Q is empty. We have to consider all minimal (P,Q,R)-chains. ---------------------------------------- (33) 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: *2NDSNEG(X1, mark(X2)) -> 2NDSNEG(X1, X2) The graph contains the following edges 1 >= 1, 2 > 2 *2NDSNEG(mark(X1), X2) -> 2NDSNEG(X1, X2) The graph contains the following edges 1 > 1, 2 >= 2 *2NDSNEG(active(X1), X2) -> 2NDSNEG(X1, X2) The graph contains the following edges 1 > 1, 2 >= 2 *2NDSNEG(X1, active(X2)) -> 2NDSNEG(X1, X2) The graph contains the following edges 1 >= 1, 2 > 2 ---------------------------------------- (34) YES ---------------------------------------- (35) Obligation: Q DP problem: The TRS P consists of the following rules: POSRECIP(active(X)) -> POSRECIP(X) POSRECIP(mark(X)) -> POSRECIP(X) The TRS R consists of the following rules: active(from(X)) -> mark(cons(X, from(s(X)))) active(2ndspos(0, Z)) -> mark(rnil) active(2ndspos(s(N), cons(X, cons(Y, Z)))) -> mark(rcons(posrecip(Y), 2ndsneg(N, Z))) active(2ndsneg(0, Z)) -> mark(rnil) active(2ndsneg(s(N), cons(X, cons(Y, Z)))) -> mark(rcons(negrecip(Y), 2ndspos(N, Z))) active(pi(X)) -> mark(2ndspos(X, from(0))) active(plus(0, Y)) -> mark(Y) active(plus(s(X), Y)) -> mark(s(plus(X, Y))) active(times(0, Y)) -> mark(0) active(times(s(X), Y)) -> mark(plus(Y, times(X, Y))) active(square(X)) -> mark(times(X, X)) mark(from(X)) -> active(from(mark(X))) mark(cons(X1, X2)) -> active(cons(mark(X1), X2)) mark(s(X)) -> active(s(mark(X))) mark(2ndspos(X1, X2)) -> active(2ndspos(mark(X1), mark(X2))) mark(0) -> active(0) mark(rnil) -> active(rnil) mark(rcons(X1, X2)) -> active(rcons(mark(X1), mark(X2))) mark(posrecip(X)) -> active(posrecip(mark(X))) mark(2ndsneg(X1, X2)) -> active(2ndsneg(mark(X1), mark(X2))) mark(negrecip(X)) -> active(negrecip(mark(X))) mark(pi(X)) -> active(pi(mark(X))) mark(plus(X1, X2)) -> active(plus(mark(X1), mark(X2))) mark(times(X1, X2)) -> active(times(mark(X1), mark(X2))) mark(square(X)) -> active(square(mark(X))) from(mark(X)) -> from(X) from(active(X)) -> from(X) cons(mark(X1), X2) -> cons(X1, X2) cons(X1, mark(X2)) -> cons(X1, X2) cons(active(X1), X2) -> cons(X1, X2) cons(X1, active(X2)) -> cons(X1, X2) s(mark(X)) -> s(X) s(active(X)) -> s(X) 2ndspos(mark(X1), X2) -> 2ndspos(X1, X2) 2ndspos(X1, mark(X2)) -> 2ndspos(X1, X2) 2ndspos(active(X1), X2) -> 2ndspos(X1, X2) 2ndspos(X1, active(X2)) -> 2ndspos(X1, X2) rcons(mark(X1), X2) -> rcons(X1, X2) rcons(X1, mark(X2)) -> rcons(X1, X2) rcons(active(X1), X2) -> rcons(X1, X2) rcons(X1, active(X2)) -> rcons(X1, X2) posrecip(mark(X)) -> posrecip(X) posrecip(active(X)) -> posrecip(X) 2ndsneg(mark(X1), X2) -> 2ndsneg(X1, X2) 2ndsneg(X1, mark(X2)) -> 2ndsneg(X1, X2) 2ndsneg(active(X1), X2) -> 2ndsneg(X1, X2) 2ndsneg(X1, active(X2)) -> 2ndsneg(X1, X2) negrecip(mark(X)) -> negrecip(X) negrecip(active(X)) -> negrecip(X) pi(mark(X)) -> pi(X) pi(active(X)) -> pi(X) plus(mark(X1), X2) -> plus(X1, X2) plus(X1, mark(X2)) -> plus(X1, X2) plus(active(X1), X2) -> plus(X1, X2) plus(X1, active(X2)) -> plus(X1, X2) times(mark(X1), X2) -> times(X1, X2) times(X1, mark(X2)) -> times(X1, X2) times(active(X1), X2) -> times(X1, X2) times(X1, active(X2)) -> times(X1, X2) square(mark(X)) -> square(X) square(active(X)) -> square(X) Q is empty. We have to consider all minimal (P,Q,R)-chains. ---------------------------------------- (36) 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. ---------------------------------------- (37) Obligation: Q DP problem: The TRS P consists of the following rules: POSRECIP(active(X)) -> POSRECIP(X) POSRECIP(mark(X)) -> POSRECIP(X) R is empty. Q is empty. We have to consider all minimal (P,Q,R)-chains. ---------------------------------------- (38) 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: *POSRECIP(active(X)) -> POSRECIP(X) The graph contains the following edges 1 > 1 *POSRECIP(mark(X)) -> POSRECIP(X) The graph contains the following edges 1 > 1 ---------------------------------------- (39) YES ---------------------------------------- (40) Obligation: Q DP problem: The TRS P consists of the following rules: RCONS(X1, mark(X2)) -> RCONS(X1, X2) RCONS(mark(X1), X2) -> RCONS(X1, X2) RCONS(active(X1), X2) -> RCONS(X1, X2) RCONS(X1, active(X2)) -> RCONS(X1, X2) The TRS R consists of the following rules: active(from(X)) -> mark(cons(X, from(s(X)))) active(2ndspos(0, Z)) -> mark(rnil) active(2ndspos(s(N), cons(X, cons(Y, Z)))) -> mark(rcons(posrecip(Y), 2ndsneg(N, Z))) active(2ndsneg(0, Z)) -> mark(rnil) active(2ndsneg(s(N), cons(X, cons(Y, Z)))) -> mark(rcons(negrecip(Y), 2ndspos(N, Z))) active(pi(X)) -> mark(2ndspos(X, from(0))) active(plus(0, Y)) -> mark(Y) active(plus(s(X), Y)) -> mark(s(plus(X, Y))) active(times(0, Y)) -> mark(0) active(times(s(X), Y)) -> mark(plus(Y, times(X, Y))) active(square(X)) -> mark(times(X, X)) mark(from(X)) -> active(from(mark(X))) mark(cons(X1, X2)) -> active(cons(mark(X1), X2)) mark(s(X)) -> active(s(mark(X))) mark(2ndspos(X1, X2)) -> active(2ndspos(mark(X1), mark(X2))) mark(0) -> active(0) mark(rnil) -> active(rnil) mark(rcons(X1, X2)) -> active(rcons(mark(X1), mark(X2))) mark(posrecip(X)) -> active(posrecip(mark(X))) mark(2ndsneg(X1, X2)) -> active(2ndsneg(mark(X1), mark(X2))) mark(negrecip(X)) -> active(negrecip(mark(X))) mark(pi(X)) -> active(pi(mark(X))) mark(plus(X1, X2)) -> active(plus(mark(X1), mark(X2))) mark(times(X1, X2)) -> active(times(mark(X1), mark(X2))) mark(square(X)) -> active(square(mark(X))) from(mark(X)) -> from(X) from(active(X)) -> from(X) cons(mark(X1), X2) -> cons(X1, X2) cons(X1, mark(X2)) -> cons(X1, X2) cons(active(X1), X2) -> cons(X1, X2) cons(X1, active(X2)) -> cons(X1, X2) s(mark(X)) -> s(X) s(active(X)) -> s(X) 2ndspos(mark(X1), X2) -> 2ndspos(X1, X2) 2ndspos(X1, mark(X2)) -> 2ndspos(X1, X2) 2ndspos(active(X1), X2) -> 2ndspos(X1, X2) 2ndspos(X1, active(X2)) -> 2ndspos(X1, X2) rcons(mark(X1), X2) -> rcons(X1, X2) rcons(X1, mark(X2)) -> rcons(X1, X2) rcons(active(X1), X2) -> rcons(X1, X2) rcons(X1, active(X2)) -> rcons(X1, X2) posrecip(mark(X)) -> posrecip(X) posrecip(active(X)) -> posrecip(X) 2ndsneg(mark(X1), X2) -> 2ndsneg(X1, X2) 2ndsneg(X1, mark(X2)) -> 2ndsneg(X1, X2) 2ndsneg(active(X1), X2) -> 2ndsneg(X1, X2) 2ndsneg(X1, active(X2)) -> 2ndsneg(X1, X2) negrecip(mark(X)) -> negrecip(X) negrecip(active(X)) -> negrecip(X) pi(mark(X)) -> pi(X) pi(active(X)) -> pi(X) plus(mark(X1), X2) -> plus(X1, X2) plus(X1, mark(X2)) -> plus(X1, X2) plus(active(X1), X2) -> plus(X1, X2) plus(X1, active(X2)) -> plus(X1, X2) times(mark(X1), X2) -> times(X1, X2) times(X1, mark(X2)) -> times(X1, X2) times(active(X1), X2) -> times(X1, X2) times(X1, active(X2)) -> times(X1, X2) square(mark(X)) -> square(X) square(active(X)) -> square(X) Q is empty. We have to consider all minimal (P,Q,R)-chains. ---------------------------------------- (41) 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. ---------------------------------------- (42) Obligation: Q DP problem: The TRS P consists of the following rules: RCONS(X1, mark(X2)) -> RCONS(X1, X2) RCONS(mark(X1), X2) -> RCONS(X1, X2) RCONS(active(X1), X2) -> RCONS(X1, X2) RCONS(X1, active(X2)) -> RCONS(X1, X2) R is empty. Q is empty. We have to consider all minimal (P,Q,R)-chains. ---------------------------------------- (43) 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: *RCONS(X1, mark(X2)) -> RCONS(X1, X2) The graph contains the following edges 1 >= 1, 2 > 2 *RCONS(mark(X1), X2) -> RCONS(X1, X2) The graph contains the following edges 1 > 1, 2 >= 2 *RCONS(active(X1), X2) -> RCONS(X1, X2) The graph contains the following edges 1 > 1, 2 >= 2 *RCONS(X1, active(X2)) -> RCONS(X1, X2) The graph contains the following edges 1 >= 1, 2 > 2 ---------------------------------------- (44) YES ---------------------------------------- (45) Obligation: Q DP problem: The TRS P consists of the following rules: 2NDSPOS(X1, mark(X2)) -> 2NDSPOS(X1, X2) 2NDSPOS(mark(X1), X2) -> 2NDSPOS(X1, X2) 2NDSPOS(active(X1), X2) -> 2NDSPOS(X1, X2) 2NDSPOS(X1, active(X2)) -> 2NDSPOS(X1, X2) The TRS R consists of the following rules: active(from(X)) -> mark(cons(X, from(s(X)))) active(2ndspos(0, Z)) -> mark(rnil) active(2ndspos(s(N), cons(X, cons(Y, Z)))) -> mark(rcons(posrecip(Y), 2ndsneg(N, Z))) active(2ndsneg(0, Z)) -> mark(rnil) active(2ndsneg(s(N), cons(X, cons(Y, Z)))) -> mark(rcons(negrecip(Y), 2ndspos(N, Z))) active(pi(X)) -> mark(2ndspos(X, from(0))) active(plus(0, Y)) -> mark(Y) active(plus(s(X), Y)) -> mark(s(plus(X, Y))) active(times(0, Y)) -> mark(0) active(times(s(X), Y)) -> mark(plus(Y, times(X, Y))) active(square(X)) -> mark(times(X, X)) mark(from(X)) -> active(from(mark(X))) mark(cons(X1, X2)) -> active(cons(mark(X1), X2)) mark(s(X)) -> active(s(mark(X))) mark(2ndspos(X1, X2)) -> active(2ndspos(mark(X1), mark(X2))) mark(0) -> active(0) mark(rnil) -> active(rnil) mark(rcons(X1, X2)) -> active(rcons(mark(X1), mark(X2))) mark(posrecip(X)) -> active(posrecip(mark(X))) mark(2ndsneg(X1, X2)) -> active(2ndsneg(mark(X1), mark(X2))) mark(negrecip(X)) -> active(negrecip(mark(X))) mark(pi(X)) -> active(pi(mark(X))) mark(plus(X1, X2)) -> active(plus(mark(X1), mark(X2))) mark(times(X1, X2)) -> active(times(mark(X1), mark(X2))) mark(square(X)) -> active(square(mark(X))) from(mark(X)) -> from(X) from(active(X)) -> from(X) cons(mark(X1), X2) -> cons(X1, X2) cons(X1, mark(X2)) -> cons(X1, X2) cons(active(X1), X2) -> cons(X1, X2) cons(X1, active(X2)) -> cons(X1, X2) s(mark(X)) -> s(X) s(active(X)) -> s(X) 2ndspos(mark(X1), X2) -> 2ndspos(X1, X2) 2ndspos(X1, mark(X2)) -> 2ndspos(X1, X2) 2ndspos(active(X1), X2) -> 2ndspos(X1, X2) 2ndspos(X1, active(X2)) -> 2ndspos(X1, X2) rcons(mark(X1), X2) -> rcons(X1, X2) rcons(X1, mark(X2)) -> rcons(X1, X2) rcons(active(X1), X2) -> rcons(X1, X2) rcons(X1, active(X2)) -> rcons(X1, X2) posrecip(mark(X)) -> posrecip(X) posrecip(active(X)) -> posrecip(X) 2ndsneg(mark(X1), X2) -> 2ndsneg(X1, X2) 2ndsneg(X1, mark(X2)) -> 2ndsneg(X1, X2) 2ndsneg(active(X1), X2) -> 2ndsneg(X1, X2) 2ndsneg(X1, active(X2)) -> 2ndsneg(X1, X2) negrecip(mark(X)) -> negrecip(X) negrecip(active(X)) -> negrecip(X) pi(mark(X)) -> pi(X) pi(active(X)) -> pi(X) plus(mark(X1), X2) -> plus(X1, X2) plus(X1, mark(X2)) -> plus(X1, X2) plus(active(X1), X2) -> plus(X1, X2) plus(X1, active(X2)) -> plus(X1, X2) times(mark(X1), X2) -> times(X1, X2) times(X1, mark(X2)) -> times(X1, X2) times(active(X1), X2) -> times(X1, X2) times(X1, active(X2)) -> times(X1, X2) square(mark(X)) -> square(X) square(active(X)) -> square(X) Q is empty. We have to consider all minimal (P,Q,R)-chains. ---------------------------------------- (46) 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. ---------------------------------------- (47) Obligation: Q DP problem: The TRS P consists of the following rules: 2NDSPOS(X1, mark(X2)) -> 2NDSPOS(X1, X2) 2NDSPOS(mark(X1), X2) -> 2NDSPOS(X1, X2) 2NDSPOS(active(X1), X2) -> 2NDSPOS(X1, X2) 2NDSPOS(X1, active(X2)) -> 2NDSPOS(X1, X2) R is empty. Q is empty. We have to consider all minimal (P,Q,R)-chains. ---------------------------------------- (48) 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: *2NDSPOS(X1, mark(X2)) -> 2NDSPOS(X1, X2) The graph contains the following edges 1 >= 1, 2 > 2 *2NDSPOS(mark(X1), X2) -> 2NDSPOS(X1, X2) The graph contains the following edges 1 > 1, 2 >= 2 *2NDSPOS(active(X1), X2) -> 2NDSPOS(X1, X2) The graph contains the following edges 1 > 1, 2 >= 2 *2NDSPOS(X1, active(X2)) -> 2NDSPOS(X1, X2) The graph contains the following edges 1 >= 1, 2 > 2 ---------------------------------------- (49) YES ---------------------------------------- (50) Obligation: Q DP problem: The TRS P consists of the following rules: S(active(X)) -> S(X) S(mark(X)) -> S(X) The TRS R consists of the following rules: active(from(X)) -> mark(cons(X, from(s(X)))) active(2ndspos(0, Z)) -> mark(rnil) active(2ndspos(s(N), cons(X, cons(Y, Z)))) -> mark(rcons(posrecip(Y), 2ndsneg(N, Z))) active(2ndsneg(0, Z)) -> mark(rnil) active(2ndsneg(s(N), cons(X, cons(Y, Z)))) -> mark(rcons(negrecip(Y), 2ndspos(N, Z))) active(pi(X)) -> mark(2ndspos(X, from(0))) active(plus(0, Y)) -> mark(Y) active(plus(s(X), Y)) -> mark(s(plus(X, Y))) active(times(0, Y)) -> mark(0) active(times(s(X), Y)) -> mark(plus(Y, times(X, Y))) active(square(X)) -> mark(times(X, X)) mark(from(X)) -> active(from(mark(X))) mark(cons(X1, X2)) -> active(cons(mark(X1), X2)) mark(s(X)) -> active(s(mark(X))) mark(2ndspos(X1, X2)) -> active(2ndspos(mark(X1), mark(X2))) mark(0) -> active(0) mark(rnil) -> active(rnil) mark(rcons(X1, X2)) -> active(rcons(mark(X1), mark(X2))) mark(posrecip(X)) -> active(posrecip(mark(X))) mark(2ndsneg(X1, X2)) -> active(2ndsneg(mark(X1), mark(X2))) mark(negrecip(X)) -> active(negrecip(mark(X))) mark(pi(X)) -> active(pi(mark(X))) mark(plus(X1, X2)) -> active(plus(mark(X1), mark(X2))) mark(times(X1, X2)) -> active(times(mark(X1), mark(X2))) mark(square(X)) -> active(square(mark(X))) from(mark(X)) -> from(X) from(active(X)) -> from(X) cons(mark(X1), X2) -> cons(X1, X2) cons(X1, mark(X2)) -> cons(X1, X2) cons(active(X1), X2) -> cons(X1, X2) cons(X1, active(X2)) -> cons(X1, X2) s(mark(X)) -> s(X) s(active(X)) -> s(X) 2ndspos(mark(X1), X2) -> 2ndspos(X1, X2) 2ndspos(X1, mark(X2)) -> 2ndspos(X1, X2) 2ndspos(active(X1), X2) -> 2ndspos(X1, X2) 2ndspos(X1, active(X2)) -> 2ndspos(X1, X2) rcons(mark(X1), X2) -> rcons(X1, X2) rcons(X1, mark(X2)) -> rcons(X1, X2) rcons(active(X1), X2) -> rcons(X1, X2) rcons(X1, active(X2)) -> rcons(X1, X2) posrecip(mark(X)) -> posrecip(X) posrecip(active(X)) -> posrecip(X) 2ndsneg(mark(X1), X2) -> 2ndsneg(X1, X2) 2ndsneg(X1, mark(X2)) -> 2ndsneg(X1, X2) 2ndsneg(active(X1), X2) -> 2ndsneg(X1, X2) 2ndsneg(X1, active(X2)) -> 2ndsneg(X1, X2) negrecip(mark(X)) -> negrecip(X) negrecip(active(X)) -> negrecip(X) pi(mark(X)) -> pi(X) pi(active(X)) -> pi(X) plus(mark(X1), X2) -> plus(X1, X2) plus(X1, mark(X2)) -> plus(X1, X2) plus(active(X1), X2) -> plus(X1, X2) plus(X1, active(X2)) -> plus(X1, X2) times(mark(X1), X2) -> times(X1, X2) times(X1, mark(X2)) -> times(X1, X2) times(active(X1), X2) -> times(X1, X2) times(X1, active(X2)) -> times(X1, X2) square(mark(X)) -> square(X) square(active(X)) -> square(X) Q is empty. We have to consider all minimal (P,Q,R)-chains. ---------------------------------------- (51) 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. ---------------------------------------- (52) Obligation: Q DP problem: The TRS P consists of the following rules: S(active(X)) -> S(X) S(mark(X)) -> S(X) R is empty. Q is empty. We have to consider all minimal (P,Q,R)-chains. ---------------------------------------- (53) 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: *S(active(X)) -> S(X) The graph contains the following edges 1 > 1 *S(mark(X)) -> S(X) The graph contains the following edges 1 > 1 ---------------------------------------- (54) YES ---------------------------------------- (55) Obligation: Q DP problem: The TRS P consists of the following rules: CONS(X1, mark(X2)) -> CONS(X1, X2) CONS(mark(X1), X2) -> CONS(X1, X2) CONS(active(X1), X2) -> CONS(X1, X2) CONS(X1, active(X2)) -> CONS(X1, X2) The TRS R consists of the following rules: active(from(X)) -> mark(cons(X, from(s(X)))) active(2ndspos(0, Z)) -> mark(rnil) active(2ndspos(s(N), cons(X, cons(Y, Z)))) -> mark(rcons(posrecip(Y), 2ndsneg(N, Z))) active(2ndsneg(0, Z)) -> mark(rnil) active(2ndsneg(s(N), cons(X, cons(Y, Z)))) -> mark(rcons(negrecip(Y), 2ndspos(N, Z))) active(pi(X)) -> mark(2ndspos(X, from(0))) active(plus(0, Y)) -> mark(Y) active(plus(s(X), Y)) -> mark(s(plus(X, Y))) active(times(0, Y)) -> mark(0) active(times(s(X), Y)) -> mark(plus(Y, times(X, Y))) active(square(X)) -> mark(times(X, X)) mark(from(X)) -> active(from(mark(X))) mark(cons(X1, X2)) -> active(cons(mark(X1), X2)) mark(s(X)) -> active(s(mark(X))) mark(2ndspos(X1, X2)) -> active(2ndspos(mark(X1), mark(X2))) mark(0) -> active(0) mark(rnil) -> active(rnil) mark(rcons(X1, X2)) -> active(rcons(mark(X1), mark(X2))) mark(posrecip(X)) -> active(posrecip(mark(X))) mark(2ndsneg(X1, X2)) -> active(2ndsneg(mark(X1), mark(X2))) mark(negrecip(X)) -> active(negrecip(mark(X))) mark(pi(X)) -> active(pi(mark(X))) mark(plus(X1, X2)) -> active(plus(mark(X1), mark(X2))) mark(times(X1, X2)) -> active(times(mark(X1), mark(X2))) mark(square(X)) -> active(square(mark(X))) from(mark(X)) -> from(X) from(active(X)) -> from(X) cons(mark(X1), X2) -> cons(X1, X2) cons(X1, mark(X2)) -> cons(X1, X2) cons(active(X1), X2) -> cons(X1, X2) cons(X1, active(X2)) -> cons(X1, X2) s(mark(X)) -> s(X) s(active(X)) -> s(X) 2ndspos(mark(X1), X2) -> 2ndspos(X1, X2) 2ndspos(X1, mark(X2)) -> 2ndspos(X1, X2) 2ndspos(active(X1), X2) -> 2ndspos(X1, X2) 2ndspos(X1, active(X2)) -> 2ndspos(X1, X2) rcons(mark(X1), X2) -> rcons(X1, X2) rcons(X1, mark(X2)) -> rcons(X1, X2) rcons(active(X1), X2) -> rcons(X1, X2) rcons(X1, active(X2)) -> rcons(X1, X2) posrecip(mark(X)) -> posrecip(X) posrecip(active(X)) -> posrecip(X) 2ndsneg(mark(X1), X2) -> 2ndsneg(X1, X2) 2ndsneg(X1, mark(X2)) -> 2ndsneg(X1, X2) 2ndsneg(active(X1), X2) -> 2ndsneg(X1, X2) 2ndsneg(X1, active(X2)) -> 2ndsneg(X1, X2) negrecip(mark(X)) -> negrecip(X) negrecip(active(X)) -> negrecip(X) pi(mark(X)) -> pi(X) pi(active(X)) -> pi(X) plus(mark(X1), X2) -> plus(X1, X2) plus(X1, mark(X2)) -> plus(X1, X2) plus(active(X1), X2) -> plus(X1, X2) plus(X1, active(X2)) -> plus(X1, X2) times(mark(X1), X2) -> times(X1, X2) times(X1, mark(X2)) -> times(X1, X2) times(active(X1), X2) -> times(X1, X2) times(X1, active(X2)) -> times(X1, X2) square(mark(X)) -> square(X) square(active(X)) -> square(X) Q is empty. We have to consider all minimal (P,Q,R)-chains. ---------------------------------------- (56) 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. ---------------------------------------- (57) Obligation: Q DP problem: The TRS P consists of the following rules: CONS(X1, mark(X2)) -> CONS(X1, X2) CONS(mark(X1), X2) -> CONS(X1, X2) CONS(active(X1), X2) -> CONS(X1, X2) CONS(X1, active(X2)) -> CONS(X1, X2) R is empty. Q is empty. We have to consider all minimal (P,Q,R)-chains. ---------------------------------------- (58) 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: *CONS(X1, mark(X2)) -> CONS(X1, X2) The graph contains the following edges 1 >= 1, 2 > 2 *CONS(mark(X1), X2) -> CONS(X1, X2) The graph contains the following edges 1 > 1, 2 >= 2 *CONS(active(X1), X2) -> CONS(X1, X2) The graph contains the following edges 1 > 1, 2 >= 2 *CONS(X1, active(X2)) -> CONS(X1, X2) The graph contains the following edges 1 >= 1, 2 > 2 ---------------------------------------- (59) YES ---------------------------------------- (60) Obligation: Q DP problem: The TRS P consists of the following rules: FROM(active(X)) -> FROM(X) FROM(mark(X)) -> FROM(X) The TRS R consists of the following rules: active(from(X)) -> mark(cons(X, from(s(X)))) active(2ndspos(0, Z)) -> mark(rnil) active(2ndspos(s(N), cons(X, cons(Y, Z)))) -> mark(rcons(posrecip(Y), 2ndsneg(N, Z))) active(2ndsneg(0, Z)) -> mark(rnil) active(2ndsneg(s(N), cons(X, cons(Y, Z)))) -> mark(rcons(negrecip(Y), 2ndspos(N, Z))) active(pi(X)) -> mark(2ndspos(X, from(0))) active(plus(0, Y)) -> mark(Y) active(plus(s(X), Y)) -> mark(s(plus(X, Y))) active(times(0, Y)) -> mark(0) active(times(s(X), Y)) -> mark(plus(Y, times(X, Y))) active(square(X)) -> mark(times(X, X)) mark(from(X)) -> active(from(mark(X))) mark(cons(X1, X2)) -> active(cons(mark(X1), X2)) mark(s(X)) -> active(s(mark(X))) mark(2ndspos(X1, X2)) -> active(2ndspos(mark(X1), mark(X2))) mark(0) -> active(0) mark(rnil) -> active(rnil) mark(rcons(X1, X2)) -> active(rcons(mark(X1), mark(X2))) mark(posrecip(X)) -> active(posrecip(mark(X))) mark(2ndsneg(X1, X2)) -> active(2ndsneg(mark(X1), mark(X2))) mark(negrecip(X)) -> active(negrecip(mark(X))) mark(pi(X)) -> active(pi(mark(X))) mark(plus(X1, X2)) -> active(plus(mark(X1), mark(X2))) mark(times(X1, X2)) -> active(times(mark(X1), mark(X2))) mark(square(X)) -> active(square(mark(X))) from(mark(X)) -> from(X) from(active(X)) -> from(X) cons(mark(X1), X2) -> cons(X1, X2) cons(X1, mark(X2)) -> cons(X1, X2) cons(active(X1), X2) -> cons(X1, X2) cons(X1, active(X2)) -> cons(X1, X2) s(mark(X)) -> s(X) s(active(X)) -> s(X) 2ndspos(mark(X1), X2) -> 2ndspos(X1, X2) 2ndspos(X1, mark(X2)) -> 2ndspos(X1, X2) 2ndspos(active(X1), X2) -> 2ndspos(X1, X2) 2ndspos(X1, active(X2)) -> 2ndspos(X1, X2) rcons(mark(X1), X2) -> rcons(X1, X2) rcons(X1, mark(X2)) -> rcons(X1, X2) rcons(active(X1), X2) -> rcons(X1, X2) rcons(X1, active(X2)) -> rcons(X1, X2) posrecip(mark(X)) -> posrecip(X) posrecip(active(X)) -> posrecip(X) 2ndsneg(mark(X1), X2) -> 2ndsneg(X1, X2) 2ndsneg(X1, mark(X2)) -> 2ndsneg(X1, X2) 2ndsneg(active(X1), X2) -> 2ndsneg(X1, X2) 2ndsneg(X1, active(X2)) -> 2ndsneg(X1, X2) negrecip(mark(X)) -> negrecip(X) negrecip(active(X)) -> negrecip(X) pi(mark(X)) -> pi(X) pi(active(X)) -> pi(X) plus(mark(X1), X2) -> plus(X1, X2) plus(X1, mark(X2)) -> plus(X1, X2) plus(active(X1), X2) -> plus(X1, X2) plus(X1, active(X2)) -> plus(X1, X2) times(mark(X1), X2) -> times(X1, X2) times(X1, mark(X2)) -> times(X1, X2) times(active(X1), X2) -> times(X1, X2) times(X1, active(X2)) -> times(X1, X2) square(mark(X)) -> square(X) square(active(X)) -> square(X) Q is empty. We have to consider all minimal (P,Q,R)-chains. ---------------------------------------- (61) 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. ---------------------------------------- (62) Obligation: Q DP problem: The TRS P consists of the following rules: FROM(active(X)) -> FROM(X) FROM(mark(X)) -> FROM(X) R is empty. Q is empty. We have to consider all minimal (P,Q,R)-chains. ---------------------------------------- (63) 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: *FROM(active(X)) -> FROM(X) The graph contains the following edges 1 > 1 *FROM(mark(X)) -> FROM(X) The graph contains the following edges 1 > 1 ---------------------------------------- (64) YES ---------------------------------------- (65) Obligation: Q DP problem: The TRS P consists of the following rules: MARK(from(X)) -> ACTIVE(from(mark(X))) ACTIVE(from(X)) -> MARK(cons(X, from(s(X)))) MARK(from(X)) -> MARK(X) MARK(cons(X1, X2)) -> ACTIVE(cons(mark(X1), X2)) ACTIVE(2ndspos(s(N), cons(X, cons(Y, Z)))) -> MARK(rcons(posrecip(Y), 2ndsneg(N, Z))) MARK(cons(X1, X2)) -> MARK(X1) MARK(s(X)) -> ACTIVE(s(mark(X))) ACTIVE(2ndsneg(s(N), cons(X, cons(Y, Z)))) -> MARK(rcons(negrecip(Y), 2ndspos(N, Z))) MARK(s(X)) -> MARK(X) MARK(2ndspos(X1, X2)) -> ACTIVE(2ndspos(mark(X1), mark(X2))) ACTIVE(pi(X)) -> MARK(2ndspos(X, from(0))) MARK(2ndspos(X1, X2)) -> MARK(X1) MARK(2ndspos(X1, X2)) -> MARK(X2) MARK(rcons(X1, X2)) -> ACTIVE(rcons(mark(X1), mark(X2))) ACTIVE(plus(0, Y)) -> MARK(Y) MARK(rcons(X1, X2)) -> MARK(X1) MARK(rcons(X1, X2)) -> MARK(X2) MARK(posrecip(X)) -> ACTIVE(posrecip(mark(X))) ACTIVE(plus(s(X), Y)) -> MARK(s(plus(X, Y))) MARK(posrecip(X)) -> MARK(X) MARK(2ndsneg(X1, X2)) -> ACTIVE(2ndsneg(mark(X1), mark(X2))) ACTIVE(times(s(X), Y)) -> MARK(plus(Y, times(X, Y))) MARK(2ndsneg(X1, X2)) -> MARK(X1) MARK(2ndsneg(X1, X2)) -> MARK(X2) MARK(negrecip(X)) -> ACTIVE(negrecip(mark(X))) ACTIVE(square(X)) -> MARK(times(X, X)) MARK(negrecip(X)) -> MARK(X) MARK(pi(X)) -> ACTIVE(pi(mark(X))) MARK(pi(X)) -> MARK(X) MARK(plus(X1, X2)) -> ACTIVE(plus(mark(X1), mark(X2))) MARK(plus(X1, X2)) -> MARK(X1) MARK(plus(X1, X2)) -> MARK(X2) MARK(times(X1, X2)) -> ACTIVE(times(mark(X1), mark(X2))) MARK(times(X1, X2)) -> MARK(X1) MARK(times(X1, X2)) -> MARK(X2) MARK(square(X)) -> ACTIVE(square(mark(X))) MARK(square(X)) -> MARK(X) The TRS R consists of the following rules: active(from(X)) -> mark(cons(X, from(s(X)))) active(2ndspos(0, Z)) -> mark(rnil) active(2ndspos(s(N), cons(X, cons(Y, Z)))) -> mark(rcons(posrecip(Y), 2ndsneg(N, Z))) active(2ndsneg(0, Z)) -> mark(rnil) active(2ndsneg(s(N), cons(X, cons(Y, Z)))) -> mark(rcons(negrecip(Y), 2ndspos(N, Z))) active(pi(X)) -> mark(2ndspos(X, from(0))) active(plus(0, Y)) -> mark(Y) active(plus(s(X), Y)) -> mark(s(plus(X, Y))) active(times(0, Y)) -> mark(0) active(times(s(X), Y)) -> mark(plus(Y, times(X, Y))) active(square(X)) -> mark(times(X, X)) mark(from(X)) -> active(from(mark(X))) mark(cons(X1, X2)) -> active(cons(mark(X1), X2)) mark(s(X)) -> active(s(mark(X))) mark(2ndspos(X1, X2)) -> active(2ndspos(mark(X1), mark(X2))) mark(0) -> active(0) mark(rnil) -> active(rnil) mark(rcons(X1, X2)) -> active(rcons(mark(X1), mark(X2))) mark(posrecip(X)) -> active(posrecip(mark(X))) mark(2ndsneg(X1, X2)) -> active(2ndsneg(mark(X1), mark(X2))) mark(negrecip(X)) -> active(negrecip(mark(X))) mark(pi(X)) -> active(pi(mark(X))) mark(plus(X1, X2)) -> active(plus(mark(X1), mark(X2))) mark(times(X1, X2)) -> active(times(mark(X1), mark(X2))) mark(square(X)) -> active(square(mark(X))) from(mark(X)) -> from(X) from(active(X)) -> from(X) cons(mark(X1), X2) -> cons(X1, X2) cons(X1, mark(X2)) -> cons(X1, X2) cons(active(X1), X2) -> cons(X1, X2) cons(X1, active(X2)) -> cons(X1, X2) s(mark(X)) -> s(X) s(active(X)) -> s(X) 2ndspos(mark(X1), X2) -> 2ndspos(X1, X2) 2ndspos(X1, mark(X2)) -> 2ndspos(X1, X2) 2ndspos(active(X1), X2) -> 2ndspos(X1, X2) 2ndspos(X1, active(X2)) -> 2ndspos(X1, X2) rcons(mark(X1), X2) -> rcons(X1, X2) rcons(X1, mark(X2)) -> rcons(X1, X2) rcons(active(X1), X2) -> rcons(X1, X2) rcons(X1, active(X2)) -> rcons(X1, X2) posrecip(mark(X)) -> posrecip(X) posrecip(active(X)) -> posrecip(X) 2ndsneg(mark(X1), X2) -> 2ndsneg(X1, X2) 2ndsneg(X1, mark(X2)) -> 2ndsneg(X1, X2) 2ndsneg(active(X1), X2) -> 2ndsneg(X1, X2) 2ndsneg(X1, active(X2)) -> 2ndsneg(X1, X2) negrecip(mark(X)) -> negrecip(X) negrecip(active(X)) -> negrecip(X) pi(mark(X)) -> pi(X) pi(active(X)) -> pi(X) plus(mark(X1), X2) -> plus(X1, X2) plus(X1, mark(X2)) -> plus(X1, X2) plus(active(X1), X2) -> plus(X1, X2) plus(X1, active(X2)) -> plus(X1, X2) times(mark(X1), X2) -> times(X1, X2) times(X1, mark(X2)) -> times(X1, X2) times(active(X1), X2) -> times(X1, X2) times(X1, active(X2)) -> times(X1, X2) square(mark(X)) -> square(X) square(active(X)) -> square(X) Q is empty. We have to consider all minimal (P,Q,R)-chains. ---------------------------------------- (66) QDPOrderProof (EQUIVALENT) We use the reduction pair processor [LPAR04,JAR06]. The following pairs can be oriented strictly and are deleted. MARK(posrecip(X)) -> ACTIVE(posrecip(mark(X))) The remaining pairs can at least be oriented weakly. Used ordering: Polynomial Order [NEGPOLO,POLO] with Interpretation: POL( 2ndsneg_2(x_1, x_2) ) = 2 POL( ACTIVE_1(x_1) ) = max{0, x_1 - 1} POL( 2ndspos_2(x_1, x_2) ) = 2 POL( cons_2(x_1, x_2) ) = 2 POL( from_1(x_1) ) = 2 POL( negrecip_1(x_1) ) = 2 POL( pi_1(x_1) ) = 2 POL( plus_2(x_1, x_2) ) = 2 POL( posrecip_1(x_1) ) = max{0, -2} POL( rcons_2(x_1, x_2) ) = 2 POL( s_1(x_1) ) = 2 POL( square_1(x_1) ) = 2 POL( times_2(x_1, x_2) ) = 2 POL( mark_1(x_1) ) = max{0, -2} POL( active_1(x_1) ) = 1 POL( 0 ) = 0 POL( rnil ) = 0 POL( MARK_1(x_1) ) = 1 The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented: from(active(X)) -> from(X) from(mark(X)) -> from(X) s(active(X)) -> s(X) s(mark(X)) -> s(X) cons(X1, mark(X2)) -> cons(X1, X2) cons(mark(X1), X2) -> cons(X1, X2) cons(active(X1), X2) -> cons(X1, X2) cons(X1, active(X2)) -> cons(X1, X2) posrecip(active(X)) -> posrecip(X) posrecip(mark(X)) -> posrecip(X) 2ndsneg(X1, mark(X2)) -> 2ndsneg(X1, X2) 2ndsneg(mark(X1), X2) -> 2ndsneg(X1, X2) 2ndsneg(active(X1), X2) -> 2ndsneg(X1, X2) 2ndsneg(X1, active(X2)) -> 2ndsneg(X1, X2) rcons(X1, mark(X2)) -> rcons(X1, X2) rcons(mark(X1), X2) -> rcons(X1, X2) rcons(active(X1), X2) -> rcons(X1, X2) rcons(X1, active(X2)) -> rcons(X1, X2) negrecip(active(X)) -> negrecip(X) negrecip(mark(X)) -> negrecip(X) 2ndspos(X1, mark(X2)) -> 2ndspos(X1, X2) 2ndspos(mark(X1), X2) -> 2ndspos(X1, X2) 2ndspos(active(X1), X2) -> 2ndspos(X1, X2) 2ndspos(X1, active(X2)) -> 2ndspos(X1, X2) plus(X1, mark(X2)) -> plus(X1, X2) plus(mark(X1), X2) -> plus(X1, X2) plus(active(X1), X2) -> plus(X1, X2) plus(X1, active(X2)) -> plus(X1, X2) times(X1, mark(X2)) -> times(X1, X2) times(mark(X1), X2) -> times(X1, X2) times(active(X1), X2) -> times(X1, X2) times(X1, active(X2)) -> times(X1, X2) pi(active(X)) -> pi(X) pi(mark(X)) -> pi(X) square(active(X)) -> square(X) square(mark(X)) -> square(X) ---------------------------------------- (67) Obligation: Q DP problem: The TRS P consists of the following rules: MARK(from(X)) -> ACTIVE(from(mark(X))) ACTIVE(from(X)) -> MARK(cons(X, from(s(X)))) MARK(from(X)) -> MARK(X) MARK(cons(X1, X2)) -> ACTIVE(cons(mark(X1), X2)) ACTIVE(2ndspos(s(N), cons(X, cons(Y, Z)))) -> MARK(rcons(posrecip(Y), 2ndsneg(N, Z))) MARK(cons(X1, X2)) -> MARK(X1) MARK(s(X)) -> ACTIVE(s(mark(X))) ACTIVE(2ndsneg(s(N), cons(X, cons(Y, Z)))) -> MARK(rcons(negrecip(Y), 2ndspos(N, Z))) MARK(s(X)) -> MARK(X) MARK(2ndspos(X1, X2)) -> ACTIVE(2ndspos(mark(X1), mark(X2))) ACTIVE(pi(X)) -> MARK(2ndspos(X, from(0))) MARK(2ndspos(X1, X2)) -> MARK(X1) MARK(2ndspos(X1, X2)) -> MARK(X2) MARK(rcons(X1, X2)) -> ACTIVE(rcons(mark(X1), mark(X2))) ACTIVE(plus(0, Y)) -> MARK(Y) MARK(rcons(X1, X2)) -> MARK(X1) MARK(rcons(X1, X2)) -> MARK(X2) ACTIVE(plus(s(X), Y)) -> MARK(s(plus(X, Y))) MARK(posrecip(X)) -> MARK(X) MARK(2ndsneg(X1, X2)) -> ACTIVE(2ndsneg(mark(X1), mark(X2))) ACTIVE(times(s(X), Y)) -> MARK(plus(Y, times(X, Y))) MARK(2ndsneg(X1, X2)) -> MARK(X1) MARK(2ndsneg(X1, X2)) -> MARK(X2) MARK(negrecip(X)) -> ACTIVE(negrecip(mark(X))) ACTIVE(square(X)) -> MARK(times(X, X)) MARK(negrecip(X)) -> MARK(X) MARK(pi(X)) -> ACTIVE(pi(mark(X))) MARK(pi(X)) -> MARK(X) MARK(plus(X1, X2)) -> ACTIVE(plus(mark(X1), mark(X2))) MARK(plus(X1, X2)) -> MARK(X1) MARK(plus(X1, X2)) -> MARK(X2) MARK(times(X1, X2)) -> ACTIVE(times(mark(X1), mark(X2))) MARK(times(X1, X2)) -> MARK(X1) MARK(times(X1, X2)) -> MARK(X2) MARK(square(X)) -> ACTIVE(square(mark(X))) MARK(square(X)) -> MARK(X) The TRS R consists of the following rules: active(from(X)) -> mark(cons(X, from(s(X)))) active(2ndspos(0, Z)) -> mark(rnil) active(2ndspos(s(N), cons(X, cons(Y, Z)))) -> mark(rcons(posrecip(Y), 2ndsneg(N, Z))) active(2ndsneg(0, Z)) -> mark(rnil) active(2ndsneg(s(N), cons(X, cons(Y, Z)))) -> mark(rcons(negrecip(Y), 2ndspos(N, Z))) active(pi(X)) -> mark(2ndspos(X, from(0))) active(plus(0, Y)) -> mark(Y) active(plus(s(X), Y)) -> mark(s(plus(X, Y))) active(times(0, Y)) -> mark(0) active(times(s(X), Y)) -> mark(plus(Y, times(X, Y))) active(square(X)) -> mark(times(X, X)) mark(from(X)) -> active(from(mark(X))) mark(cons(X1, X2)) -> active(cons(mark(X1), X2)) mark(s(X)) -> active(s(mark(X))) mark(2ndspos(X1, X2)) -> active(2ndspos(mark(X1), mark(X2))) mark(0) -> active(0) mark(rnil) -> active(rnil) mark(rcons(X1, X2)) -> active(rcons(mark(X1), mark(X2))) mark(posrecip(X)) -> active(posrecip(mark(X))) mark(2ndsneg(X1, X2)) -> active(2ndsneg(mark(X1), mark(X2))) mark(negrecip(X)) -> active(negrecip(mark(X))) mark(pi(X)) -> active(pi(mark(X))) mark(plus(X1, X2)) -> active(plus(mark(X1), mark(X2))) mark(times(X1, X2)) -> active(times(mark(X1), mark(X2))) mark(square(X)) -> active(square(mark(X))) from(mark(X)) -> from(X) from(active(X)) -> from(X) cons(mark(X1), X2) -> cons(X1, X2) cons(X1, mark(X2)) -> cons(X1, X2) cons(active(X1), X2) -> cons(X1, X2) cons(X1, active(X2)) -> cons(X1, X2) s(mark(X)) -> s(X) s(active(X)) -> s(X) 2ndspos(mark(X1), X2) -> 2ndspos(X1, X2) 2ndspos(X1, mark(X2)) -> 2ndspos(X1, X2) 2ndspos(active(X1), X2) -> 2ndspos(X1, X2) 2ndspos(X1, active(X2)) -> 2ndspos(X1, X2) rcons(mark(X1), X2) -> rcons(X1, X2) rcons(X1, mark(X2)) -> rcons(X1, X2) rcons(active(X1), X2) -> rcons(X1, X2) rcons(X1, active(X2)) -> rcons(X1, X2) posrecip(mark(X)) -> posrecip(X) posrecip(active(X)) -> posrecip(X) 2ndsneg(mark(X1), X2) -> 2ndsneg(X1, X2) 2ndsneg(X1, mark(X2)) -> 2ndsneg(X1, X2) 2ndsneg(active(X1), X2) -> 2ndsneg(X1, X2) 2ndsneg(X1, active(X2)) -> 2ndsneg(X1, X2) negrecip(mark(X)) -> negrecip(X) negrecip(active(X)) -> negrecip(X) pi(mark(X)) -> pi(X) pi(active(X)) -> pi(X) plus(mark(X1), X2) -> plus(X1, X2) plus(X1, mark(X2)) -> plus(X1, X2) plus(active(X1), X2) -> plus(X1, X2) plus(X1, active(X2)) -> plus(X1, X2) times(mark(X1), X2) -> times(X1, X2) times(X1, mark(X2)) -> times(X1, X2) times(active(X1), X2) -> times(X1, X2) times(X1, active(X2)) -> times(X1, X2) square(mark(X)) -> square(X) square(active(X)) -> square(X) Q is empty. We have to consider all minimal (P,Q,R)-chains. ---------------------------------------- (68) QDPOrderProof (EQUIVALENT) We use the reduction pair processor [LPAR04,JAR06]. The following pairs can be oriented strictly and are deleted. MARK(cons(X1, X2)) -> ACTIVE(cons(mark(X1), X2)) The remaining pairs can at least be oriented weakly. Used ordering: Polynomial Order [NEGPOLO,POLO] with Interpretation: POL( 2ndsneg_2(x_1, x_2) ) = 1 POL( ACTIVE_1(x_1) ) = max{0, 2x_1 - 1} POL( 2ndspos_2(x_1, x_2) ) = 1 POL( cons_2(x_1, x_2) ) = max{0, -2} POL( from_1(x_1) ) = 1 POL( negrecip_1(x_1) ) = 1 POL( pi_1(x_1) ) = 1 POL( plus_2(x_1, x_2) ) = 1 POL( rcons_2(x_1, x_2) ) = 1 POL( s_1(x_1) ) = 1 POL( square_1(x_1) ) = 1 POL( times_2(x_1, x_2) ) = 1 POL( mark_1(x_1) ) = 2 POL( active_1(x_1) ) = max{0, x_1 - 2} POL( posrecip_1(x_1) ) = max{0, -2} POL( 0 ) = 0 POL( rnil ) = 0 POL( MARK_1(x_1) ) = 1 The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented: from(active(X)) -> from(X) from(mark(X)) -> from(X) s(active(X)) -> s(X) s(mark(X)) -> s(X) cons(X1, mark(X2)) -> cons(X1, X2) cons(mark(X1), X2) -> cons(X1, X2) cons(active(X1), X2) -> cons(X1, X2) cons(X1, active(X2)) -> cons(X1, X2) 2ndsneg(X1, mark(X2)) -> 2ndsneg(X1, X2) 2ndsneg(mark(X1), X2) -> 2ndsneg(X1, X2) 2ndsneg(active(X1), X2) -> 2ndsneg(X1, X2) 2ndsneg(X1, active(X2)) -> 2ndsneg(X1, X2) rcons(X1, mark(X2)) -> rcons(X1, X2) rcons(mark(X1), X2) -> rcons(X1, X2) rcons(active(X1), X2) -> rcons(X1, X2) rcons(X1, active(X2)) -> rcons(X1, X2) negrecip(active(X)) -> negrecip(X) negrecip(mark(X)) -> negrecip(X) 2ndspos(X1, mark(X2)) -> 2ndspos(X1, X2) 2ndspos(mark(X1), X2) -> 2ndspos(X1, X2) 2ndspos(active(X1), X2) -> 2ndspos(X1, X2) 2ndspos(X1, active(X2)) -> 2ndspos(X1, X2) plus(X1, mark(X2)) -> plus(X1, X2) plus(mark(X1), X2) -> plus(X1, X2) plus(active(X1), X2) -> plus(X1, X2) plus(X1, active(X2)) -> plus(X1, X2) times(X1, mark(X2)) -> times(X1, X2) times(mark(X1), X2) -> times(X1, X2) times(active(X1), X2) -> times(X1, X2) times(X1, active(X2)) -> times(X1, X2) pi(active(X)) -> pi(X) pi(mark(X)) -> pi(X) square(active(X)) -> square(X) square(mark(X)) -> square(X) ---------------------------------------- (69) Obligation: Q DP problem: The TRS P consists of the following rules: MARK(from(X)) -> ACTIVE(from(mark(X))) ACTIVE(from(X)) -> MARK(cons(X, from(s(X)))) MARK(from(X)) -> MARK(X) ACTIVE(2ndspos(s(N), cons(X, cons(Y, Z)))) -> MARK(rcons(posrecip(Y), 2ndsneg(N, Z))) MARK(cons(X1, X2)) -> MARK(X1) MARK(s(X)) -> ACTIVE(s(mark(X))) ACTIVE(2ndsneg(s(N), cons(X, cons(Y, Z)))) -> MARK(rcons(negrecip(Y), 2ndspos(N, Z))) MARK(s(X)) -> MARK(X) MARK(2ndspos(X1, X2)) -> ACTIVE(2ndspos(mark(X1), mark(X2))) ACTIVE(pi(X)) -> MARK(2ndspos(X, from(0))) MARK(2ndspos(X1, X2)) -> MARK(X1) MARK(2ndspos(X1, X2)) -> MARK(X2) MARK(rcons(X1, X2)) -> ACTIVE(rcons(mark(X1), mark(X2))) ACTIVE(plus(0, Y)) -> MARK(Y) MARK(rcons(X1, X2)) -> MARK(X1) MARK(rcons(X1, X2)) -> MARK(X2) ACTIVE(plus(s(X), Y)) -> MARK(s(plus(X, Y))) MARK(posrecip(X)) -> MARK(X) MARK(2ndsneg(X1, X2)) -> ACTIVE(2ndsneg(mark(X1), mark(X2))) ACTIVE(times(s(X), Y)) -> MARK(plus(Y, times(X, Y))) MARK(2ndsneg(X1, X2)) -> MARK(X1) MARK(2ndsneg(X1, X2)) -> MARK(X2) MARK(negrecip(X)) -> ACTIVE(negrecip(mark(X))) ACTIVE(square(X)) -> MARK(times(X, X)) MARK(negrecip(X)) -> MARK(X) MARK(pi(X)) -> ACTIVE(pi(mark(X))) MARK(pi(X)) -> MARK(X) MARK(plus(X1, X2)) -> ACTIVE(plus(mark(X1), mark(X2))) MARK(plus(X1, X2)) -> MARK(X1) MARK(plus(X1, X2)) -> MARK(X2) MARK(times(X1, X2)) -> ACTIVE(times(mark(X1), mark(X2))) MARK(times(X1, X2)) -> MARK(X1) MARK(times(X1, X2)) -> MARK(X2) MARK(square(X)) -> ACTIVE(square(mark(X))) MARK(square(X)) -> MARK(X) The TRS R consists of the following rules: active(from(X)) -> mark(cons(X, from(s(X)))) active(2ndspos(0, Z)) -> mark(rnil) active(2ndspos(s(N), cons(X, cons(Y, Z)))) -> mark(rcons(posrecip(Y), 2ndsneg(N, Z))) active(2ndsneg(0, Z)) -> mark(rnil) active(2ndsneg(s(N), cons(X, cons(Y, Z)))) -> mark(rcons(negrecip(Y), 2ndspos(N, Z))) active(pi(X)) -> mark(2ndspos(X, from(0))) active(plus(0, Y)) -> mark(Y) active(plus(s(X), Y)) -> mark(s(plus(X, Y))) active(times(0, Y)) -> mark(0) active(times(s(X), Y)) -> mark(plus(Y, times(X, Y))) active(square(X)) -> mark(times(X, X)) mark(from(X)) -> active(from(mark(X))) mark(cons(X1, X2)) -> active(cons(mark(X1), X2)) mark(s(X)) -> active(s(mark(X))) mark(2ndspos(X1, X2)) -> active(2ndspos(mark(X1), mark(X2))) mark(0) -> active(0) mark(rnil) -> active(rnil) mark(rcons(X1, X2)) -> active(rcons(mark(X1), mark(X2))) mark(posrecip(X)) -> active(posrecip(mark(X))) mark(2ndsneg(X1, X2)) -> active(2ndsneg(mark(X1), mark(X2))) mark(negrecip(X)) -> active(negrecip(mark(X))) mark(pi(X)) -> active(pi(mark(X))) mark(plus(X1, X2)) -> active(plus(mark(X1), mark(X2))) mark(times(X1, X2)) -> active(times(mark(X1), mark(X2))) mark(square(X)) -> active(square(mark(X))) from(mark(X)) -> from(X) from(active(X)) -> from(X) cons(mark(X1), X2) -> cons(X1, X2) cons(X1, mark(X2)) -> cons(X1, X2) cons(active(X1), X2) -> cons(X1, X2) cons(X1, active(X2)) -> cons(X1, X2) s(mark(X)) -> s(X) s(active(X)) -> s(X) 2ndspos(mark(X1), X2) -> 2ndspos(X1, X2) 2ndspos(X1, mark(X2)) -> 2ndspos(X1, X2) 2ndspos(active(X1), X2) -> 2ndspos(X1, X2) 2ndspos(X1, active(X2)) -> 2ndspos(X1, X2) rcons(mark(X1), X2) -> rcons(X1, X2) rcons(X1, mark(X2)) -> rcons(X1, X2) rcons(active(X1), X2) -> rcons(X1, X2) rcons(X1, active(X2)) -> rcons(X1, X2) posrecip(mark(X)) -> posrecip(X) posrecip(active(X)) -> posrecip(X) 2ndsneg(mark(X1), X2) -> 2ndsneg(X1, X2) 2ndsneg(X1, mark(X2)) -> 2ndsneg(X1, X2) 2ndsneg(active(X1), X2) -> 2ndsneg(X1, X2) 2ndsneg(X1, active(X2)) -> 2ndsneg(X1, X2) negrecip(mark(X)) -> negrecip(X) negrecip(active(X)) -> negrecip(X) pi(mark(X)) -> pi(X) pi(active(X)) -> pi(X) plus(mark(X1), X2) -> plus(X1, X2) plus(X1, mark(X2)) -> plus(X1, X2) plus(active(X1), X2) -> plus(X1, X2) plus(X1, active(X2)) -> plus(X1, X2) times(mark(X1), X2) -> times(X1, X2) times(X1, mark(X2)) -> times(X1, X2) times(active(X1), X2) -> times(X1, X2) times(X1, active(X2)) -> times(X1, X2) square(mark(X)) -> square(X) square(active(X)) -> square(X) Q is empty. We have to consider all minimal (P,Q,R)-chains. ---------------------------------------- (70) QDPOrderProof (EQUIVALENT) We use the reduction pair processor [LPAR04,JAR06]. The following pairs can be oriented strictly and are deleted. MARK(s(X)) -> ACTIVE(s(mark(X))) The remaining pairs can at least be oriented weakly. Used ordering: Polynomial Order [NEGPOLO,POLO] with Interpretation: POL( 2ndsneg_2(x_1, x_2) ) = 1 POL( ACTIVE_1(x_1) ) = x_1 + 1 POL( 2ndspos_2(x_1, x_2) ) = 1 POL( from_1(x_1) ) = 1 POL( negrecip_1(x_1) ) = 1 POL( pi_1(x_1) ) = 1 POL( plus_2(x_1, x_2) ) = 1 POL( rcons_2(x_1, x_2) ) = 1 POL( s_1(x_1) ) = max{0, -2} POL( square_1(x_1) ) = 1 POL( times_2(x_1, x_2) ) = 1 POL( mark_1(x_1) ) = max{0, -2} POL( active_1(x_1) ) = max{0, 2x_1 - 1} POL( cons_2(x_1, x_2) ) = 2x_1 + 2 POL( posrecip_1(x_1) ) = 2x_1 POL( 0 ) = 0 POL( rnil ) = 0 POL( MARK_1(x_1) ) = 2 The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented: from(active(X)) -> from(X) from(mark(X)) -> from(X) s(active(X)) -> s(X) s(mark(X)) -> s(X) 2ndsneg(X1, mark(X2)) -> 2ndsneg(X1, X2) 2ndsneg(mark(X1), X2) -> 2ndsneg(X1, X2) 2ndsneg(active(X1), X2) -> 2ndsneg(X1, X2) 2ndsneg(X1, active(X2)) -> 2ndsneg(X1, X2) rcons(X1, mark(X2)) -> rcons(X1, X2) rcons(mark(X1), X2) -> rcons(X1, X2) rcons(active(X1), X2) -> rcons(X1, X2) rcons(X1, active(X2)) -> rcons(X1, X2) negrecip(active(X)) -> negrecip(X) negrecip(mark(X)) -> negrecip(X) 2ndspos(X1, mark(X2)) -> 2ndspos(X1, X2) 2ndspos(mark(X1), X2) -> 2ndspos(X1, X2) 2ndspos(active(X1), X2) -> 2ndspos(X1, X2) 2ndspos(X1, active(X2)) -> 2ndspos(X1, X2) plus(X1, mark(X2)) -> plus(X1, X2) plus(mark(X1), X2) -> plus(X1, X2) plus(active(X1), X2) -> plus(X1, X2) plus(X1, active(X2)) -> plus(X1, X2) times(X1, mark(X2)) -> times(X1, X2) times(mark(X1), X2) -> times(X1, X2) times(active(X1), X2) -> times(X1, X2) times(X1, active(X2)) -> times(X1, X2) pi(active(X)) -> pi(X) pi(mark(X)) -> pi(X) square(active(X)) -> square(X) square(mark(X)) -> square(X) ---------------------------------------- (71) Obligation: Q DP problem: The TRS P consists of the following rules: MARK(from(X)) -> ACTIVE(from(mark(X))) ACTIVE(from(X)) -> MARK(cons(X, from(s(X)))) MARK(from(X)) -> MARK(X) ACTIVE(2ndspos(s(N), cons(X, cons(Y, Z)))) -> MARK(rcons(posrecip(Y), 2ndsneg(N, Z))) MARK(cons(X1, X2)) -> MARK(X1) ACTIVE(2ndsneg(s(N), cons(X, cons(Y, Z)))) -> MARK(rcons(negrecip(Y), 2ndspos(N, Z))) MARK(s(X)) -> MARK(X) MARK(2ndspos(X1, X2)) -> ACTIVE(2ndspos(mark(X1), mark(X2))) ACTIVE(pi(X)) -> MARK(2ndspos(X, from(0))) MARK(2ndspos(X1, X2)) -> MARK(X1) MARK(2ndspos(X1, X2)) -> MARK(X2) MARK(rcons(X1, X2)) -> ACTIVE(rcons(mark(X1), mark(X2))) ACTIVE(plus(0, Y)) -> MARK(Y) MARK(rcons(X1, X2)) -> MARK(X1) MARK(rcons(X1, X2)) -> MARK(X2) ACTIVE(plus(s(X), Y)) -> MARK(s(plus(X, Y))) MARK(posrecip(X)) -> MARK(X) MARK(2ndsneg(X1, X2)) -> ACTIVE(2ndsneg(mark(X1), mark(X2))) ACTIVE(times(s(X), Y)) -> MARK(plus(Y, times(X, Y))) MARK(2ndsneg(X1, X2)) -> MARK(X1) MARK(2ndsneg(X1, X2)) -> MARK(X2) MARK(negrecip(X)) -> ACTIVE(negrecip(mark(X))) ACTIVE(square(X)) -> MARK(times(X, X)) MARK(negrecip(X)) -> MARK(X) MARK(pi(X)) -> ACTIVE(pi(mark(X))) MARK(pi(X)) -> MARK(X) MARK(plus(X1, X2)) -> ACTIVE(plus(mark(X1), mark(X2))) MARK(plus(X1, X2)) -> MARK(X1) MARK(plus(X1, X2)) -> MARK(X2) MARK(times(X1, X2)) -> ACTIVE(times(mark(X1), mark(X2))) MARK(times(X1, X2)) -> MARK(X1) MARK(times(X1, X2)) -> MARK(X2) MARK(square(X)) -> ACTIVE(square(mark(X))) MARK(square(X)) -> MARK(X) The TRS R consists of the following rules: active(from(X)) -> mark(cons(X, from(s(X)))) active(2ndspos(0, Z)) -> mark(rnil) active(2ndspos(s(N), cons(X, cons(Y, Z)))) -> mark(rcons(posrecip(Y), 2ndsneg(N, Z))) active(2ndsneg(0, Z)) -> mark(rnil) active(2ndsneg(s(N), cons(X, cons(Y, Z)))) -> mark(rcons(negrecip(Y), 2ndspos(N, Z))) active(pi(X)) -> mark(2ndspos(X, from(0))) active(plus(0, Y)) -> mark(Y) active(plus(s(X), Y)) -> mark(s(plus(X, Y))) active(times(0, Y)) -> mark(0) active(times(s(X), Y)) -> mark(plus(Y, times(X, Y))) active(square(X)) -> mark(times(X, X)) mark(from(X)) -> active(from(mark(X))) mark(cons(X1, X2)) -> active(cons(mark(X1), X2)) mark(s(X)) -> active(s(mark(X))) mark(2ndspos(X1, X2)) -> active(2ndspos(mark(X1), mark(X2))) mark(0) -> active(0) mark(rnil) -> active(rnil) mark(rcons(X1, X2)) -> active(rcons(mark(X1), mark(X2))) mark(posrecip(X)) -> active(posrecip(mark(X))) mark(2ndsneg(X1, X2)) -> active(2ndsneg(mark(X1), mark(X2))) mark(negrecip(X)) -> active(negrecip(mark(X))) mark(pi(X)) -> active(pi(mark(X))) mark(plus(X1, X2)) -> active(plus(mark(X1), mark(X2))) mark(times(X1, X2)) -> active(times(mark(X1), mark(X2))) mark(square(X)) -> active(square(mark(X))) from(mark(X)) -> from(X) from(active(X)) -> from(X) cons(mark(X1), X2) -> cons(X1, X2) cons(X1, mark(X2)) -> cons(X1, X2) cons(active(X1), X2) -> cons(X1, X2) cons(X1, active(X2)) -> cons(X1, X2) s(mark(X)) -> s(X) s(active(X)) -> s(X) 2ndspos(mark(X1), X2) -> 2ndspos(X1, X2) 2ndspos(X1, mark(X2)) -> 2ndspos(X1, X2) 2ndspos(active(X1), X2) -> 2ndspos(X1, X2) 2ndspos(X1, active(X2)) -> 2ndspos(X1, X2) rcons(mark(X1), X2) -> rcons(X1, X2) rcons(X1, mark(X2)) -> rcons(X1, X2) rcons(active(X1), X2) -> rcons(X1, X2) rcons(X1, active(X2)) -> rcons(X1, X2) posrecip(mark(X)) -> posrecip(X) posrecip(active(X)) -> posrecip(X) 2ndsneg(mark(X1), X2) -> 2ndsneg(X1, X2) 2ndsneg(X1, mark(X2)) -> 2ndsneg(X1, X2) 2ndsneg(active(X1), X2) -> 2ndsneg(X1, X2) 2ndsneg(X1, active(X2)) -> 2ndsneg(X1, X2) negrecip(mark(X)) -> negrecip(X) negrecip(active(X)) -> negrecip(X) pi(mark(X)) -> pi(X) pi(active(X)) -> pi(X) plus(mark(X1), X2) -> plus(X1, X2) plus(X1, mark(X2)) -> plus(X1, X2) plus(active(X1), X2) -> plus(X1, X2) plus(X1, active(X2)) -> plus(X1, X2) times(mark(X1), X2) -> times(X1, X2) times(X1, mark(X2)) -> times(X1, X2) times(active(X1), X2) -> times(X1, X2) times(X1, active(X2)) -> times(X1, X2) square(mark(X)) -> square(X) square(active(X)) -> square(X) Q is empty. We have to consider all minimal (P,Q,R)-chains. ---------------------------------------- (72) QDPOrderProof (EQUIVALENT) We use the reduction pair processor [LPAR04,JAR06]. The following pairs can be oriented strictly and are deleted. MARK(rcons(X1, X2)) -> ACTIVE(rcons(mark(X1), mark(X2))) The remaining pairs can at least be oriented weakly. Used ordering: Polynomial Order [NEGPOLO,POLO] with Interpretation: POL( 2ndsneg_2(x_1, x_2) ) = 1 POL( ACTIVE_1(x_1) ) = 2x_1 POL( 2ndspos_2(x_1, x_2) ) = 1 POL( from_1(x_1) ) = 1 POL( negrecip_1(x_1) ) = 1 POL( pi_1(x_1) ) = 1 POL( plus_2(x_1, x_2) ) = 1 POL( rcons_2(x_1, x_2) ) = 0 POL( square_1(x_1) ) = 1 POL( times_2(x_1, x_2) ) = 1 POL( mark_1(x_1) ) = x_1 + 1 POL( active_1(x_1) ) = 2x_1 POL( cons_2(x_1, x_2) ) = 2x_2 POL( s_1(x_1) ) = max{0, 2x_1 - 2} POL( posrecip_1(x_1) ) = 2x_1 POL( 0 ) = 1 POL( rnil ) = 2 POL( MARK_1(x_1) ) = 2 The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented: from(active(X)) -> from(X) from(mark(X)) -> from(X) 2ndsneg(X1, mark(X2)) -> 2ndsneg(X1, X2) 2ndsneg(mark(X1), X2) -> 2ndsneg(X1, X2) 2ndsneg(active(X1), X2) -> 2ndsneg(X1, X2) 2ndsneg(X1, active(X2)) -> 2ndsneg(X1, X2) rcons(X1, mark(X2)) -> rcons(X1, X2) rcons(mark(X1), X2) -> rcons(X1, X2) rcons(active(X1), X2) -> rcons(X1, X2) rcons(X1, active(X2)) -> rcons(X1, X2) negrecip(active(X)) -> negrecip(X) negrecip(mark(X)) -> negrecip(X) 2ndspos(X1, mark(X2)) -> 2ndspos(X1, X2) 2ndspos(mark(X1), X2) -> 2ndspos(X1, X2) 2ndspos(active(X1), X2) -> 2ndspos(X1, X2) 2ndspos(X1, active(X2)) -> 2ndspos(X1, X2) plus(X1, mark(X2)) -> plus(X1, X2) plus(mark(X1), X2) -> plus(X1, X2) plus(active(X1), X2) -> plus(X1, X2) plus(X1, active(X2)) -> plus(X1, X2) times(X1, mark(X2)) -> times(X1, X2) times(mark(X1), X2) -> times(X1, X2) times(active(X1), X2) -> times(X1, X2) times(X1, active(X2)) -> times(X1, X2) pi(active(X)) -> pi(X) pi(mark(X)) -> pi(X) square(active(X)) -> square(X) square(mark(X)) -> square(X) ---------------------------------------- (73) Obligation: Q DP problem: The TRS P consists of the following rules: MARK(from(X)) -> ACTIVE(from(mark(X))) ACTIVE(from(X)) -> MARK(cons(X, from(s(X)))) MARK(from(X)) -> MARK(X) ACTIVE(2ndspos(s(N), cons(X, cons(Y, Z)))) -> MARK(rcons(posrecip(Y), 2ndsneg(N, Z))) MARK(cons(X1, X2)) -> MARK(X1) ACTIVE(2ndsneg(s(N), cons(X, cons(Y, Z)))) -> MARK(rcons(negrecip(Y), 2ndspos(N, Z))) MARK(s(X)) -> MARK(X) MARK(2ndspos(X1, X2)) -> ACTIVE(2ndspos(mark(X1), mark(X2))) ACTIVE(pi(X)) -> MARK(2ndspos(X, from(0))) MARK(2ndspos(X1, X2)) -> MARK(X1) MARK(2ndspos(X1, X2)) -> MARK(X2) ACTIVE(plus(0, Y)) -> MARK(Y) MARK(rcons(X1, X2)) -> MARK(X1) MARK(rcons(X1, X2)) -> MARK(X2) ACTIVE(plus(s(X), Y)) -> MARK(s(plus(X, Y))) MARK(posrecip(X)) -> MARK(X) MARK(2ndsneg(X1, X2)) -> ACTIVE(2ndsneg(mark(X1), mark(X2))) ACTIVE(times(s(X), Y)) -> MARK(plus(Y, times(X, Y))) MARK(2ndsneg(X1, X2)) -> MARK(X1) MARK(2ndsneg(X1, X2)) -> MARK(X2) MARK(negrecip(X)) -> ACTIVE(negrecip(mark(X))) ACTIVE(square(X)) -> MARK(times(X, X)) MARK(negrecip(X)) -> MARK(X) MARK(pi(X)) -> ACTIVE(pi(mark(X))) MARK(pi(X)) -> MARK(X) MARK(plus(X1, X2)) -> ACTIVE(plus(mark(X1), mark(X2))) MARK(plus(X1, X2)) -> MARK(X1) MARK(plus(X1, X2)) -> MARK(X2) MARK(times(X1, X2)) -> ACTIVE(times(mark(X1), mark(X2))) MARK(times(X1, X2)) -> MARK(X1) MARK(times(X1, X2)) -> MARK(X2) MARK(square(X)) -> ACTIVE(square(mark(X))) MARK(square(X)) -> MARK(X) The TRS R consists of the following rules: active(from(X)) -> mark(cons(X, from(s(X)))) active(2ndspos(0, Z)) -> mark(rnil) active(2ndspos(s(N), cons(X, cons(Y, Z)))) -> mark(rcons(posrecip(Y), 2ndsneg(N, Z))) active(2ndsneg(0, Z)) -> mark(rnil) active(2ndsneg(s(N), cons(X, cons(Y, Z)))) -> mark(rcons(negrecip(Y), 2ndspos(N, Z))) active(pi(X)) -> mark(2ndspos(X, from(0))) active(plus(0, Y)) -> mark(Y) active(plus(s(X), Y)) -> mark(s(plus(X, Y))) active(times(0, Y)) -> mark(0) active(times(s(X), Y)) -> mark(plus(Y, times(X, Y))) active(square(X)) -> mark(times(X, X)) mark(from(X)) -> active(from(mark(X))) mark(cons(X1, X2)) -> active(cons(mark(X1), X2)) mark(s(X)) -> active(s(mark(X))) mark(2ndspos(X1, X2)) -> active(2ndspos(mark(X1), mark(X2))) mark(0) -> active(0) mark(rnil) -> active(rnil) mark(rcons(X1, X2)) -> active(rcons(mark(X1), mark(X2))) mark(posrecip(X)) -> active(posrecip(mark(X))) mark(2ndsneg(X1, X2)) -> active(2ndsneg(mark(X1), mark(X2))) mark(negrecip(X)) -> active(negrecip(mark(X))) mark(pi(X)) -> active(pi(mark(X))) mark(plus(X1, X2)) -> active(plus(mark(X1), mark(X2))) mark(times(X1, X2)) -> active(times(mark(X1), mark(X2))) mark(square(X)) -> active(square(mark(X))) from(mark(X)) -> from(X) from(active(X)) -> from(X) cons(mark(X1), X2) -> cons(X1, X2) cons(X1, mark(X2)) -> cons(X1, X2) cons(active(X1), X2) -> cons(X1, X2) cons(X1, active(X2)) -> cons(X1, X2) s(mark(X)) -> s(X) s(active(X)) -> s(X) 2ndspos(mark(X1), X2) -> 2ndspos(X1, X2) 2ndspos(X1, mark(X2)) -> 2ndspos(X1, X2) 2ndspos(active(X1), X2) -> 2ndspos(X1, X2) 2ndspos(X1, active(X2)) -> 2ndspos(X1, X2) rcons(mark(X1), X2) -> rcons(X1, X2) rcons(X1, mark(X2)) -> rcons(X1, X2) rcons(active(X1), X2) -> rcons(X1, X2) rcons(X1, active(X2)) -> rcons(X1, X2) posrecip(mark(X)) -> posrecip(X) posrecip(active(X)) -> posrecip(X) 2ndsneg(mark(X1), X2) -> 2ndsneg(X1, X2) 2ndsneg(X1, mark(X2)) -> 2ndsneg(X1, X2) 2ndsneg(active(X1), X2) -> 2ndsneg(X1, X2) 2ndsneg(X1, active(X2)) -> 2ndsneg(X1, X2) negrecip(mark(X)) -> negrecip(X) negrecip(active(X)) -> negrecip(X) pi(mark(X)) -> pi(X) pi(active(X)) -> pi(X) plus(mark(X1), X2) -> plus(X1, X2) plus(X1, mark(X2)) -> plus(X1, X2) plus(active(X1), X2) -> plus(X1, X2) plus(X1, active(X2)) -> plus(X1, X2) times(mark(X1), X2) -> times(X1, X2) times(X1, mark(X2)) -> times(X1, X2) times(active(X1), X2) -> times(X1, X2) times(X1, active(X2)) -> times(X1, X2) square(mark(X)) -> square(X) square(active(X)) -> square(X) Q is empty. We have to consider all minimal (P,Q,R)-chains. ---------------------------------------- (74) QDPOrderProof (EQUIVALENT) We use the reduction pair processor [LPAR04,JAR06]. The following pairs can be oriented strictly and are deleted. MARK(negrecip(X)) -> ACTIVE(negrecip(mark(X))) The remaining pairs can at least be oriented weakly. Used ordering: Polynomial Order [NEGPOLO,POLO] with Interpretation: POL( 2ndsneg_2(x_1, x_2) ) = 1 POL( ACTIVE_1(x_1) ) = x_1 + 1 POL( 2ndspos_2(x_1, x_2) ) = 1 POL( from_1(x_1) ) = 1 POL( negrecip_1(x_1) ) = 0 POL( pi_1(x_1) ) = 1 POL( plus_2(x_1, x_2) ) = 1 POL( square_1(x_1) ) = 1 POL( times_2(x_1, x_2) ) = 1 POL( mark_1(x_1) ) = x_1 + 1 POL( active_1(x_1) ) = 1 POL( cons_2(x_1, x_2) ) = max{0, x_2 - 2} POL( s_1(x_1) ) = x_1 + 1 POL( rcons_2(x_1, x_2) ) = 2x_1 + x_2 + 1 POL( posrecip_1(x_1) ) = 2x_1 POL( 0 ) = 1 POL( rnil ) = 1 POL( MARK_1(x_1) ) = 2 The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented: from(active(X)) -> from(X) from(mark(X)) -> from(X) 2ndsneg(X1, mark(X2)) -> 2ndsneg(X1, X2) 2ndsneg(mark(X1), X2) -> 2ndsneg(X1, X2) 2ndsneg(active(X1), X2) -> 2ndsneg(X1, X2) 2ndsneg(X1, active(X2)) -> 2ndsneg(X1, X2) negrecip(active(X)) -> negrecip(X) negrecip(mark(X)) -> negrecip(X) 2ndspos(X1, mark(X2)) -> 2ndspos(X1, X2) 2ndspos(mark(X1), X2) -> 2ndspos(X1, X2) 2ndspos(active(X1), X2) -> 2ndspos(X1, X2) 2ndspos(X1, active(X2)) -> 2ndspos(X1, X2) plus(X1, mark(X2)) -> plus(X1, X2) plus(mark(X1), X2) -> plus(X1, X2) plus(active(X1), X2) -> plus(X1, X2) plus(X1, active(X2)) -> plus(X1, X2) times(X1, mark(X2)) -> times(X1, X2) times(mark(X1), X2) -> times(X1, X2) times(active(X1), X2) -> times(X1, X2) times(X1, active(X2)) -> times(X1, X2) pi(active(X)) -> pi(X) pi(mark(X)) -> pi(X) square(active(X)) -> square(X) square(mark(X)) -> square(X) ---------------------------------------- (75) Obligation: Q DP problem: The TRS P consists of the following rules: MARK(from(X)) -> ACTIVE(from(mark(X))) ACTIVE(from(X)) -> MARK(cons(X, from(s(X)))) MARK(from(X)) -> MARK(X) ACTIVE(2ndspos(s(N), cons(X, cons(Y, Z)))) -> MARK(rcons(posrecip(Y), 2ndsneg(N, Z))) MARK(cons(X1, X2)) -> MARK(X1) ACTIVE(2ndsneg(s(N), cons(X, cons(Y, Z)))) -> MARK(rcons(negrecip(Y), 2ndspos(N, Z))) MARK(s(X)) -> MARK(X) MARK(2ndspos(X1, X2)) -> ACTIVE(2ndspos(mark(X1), mark(X2))) ACTIVE(pi(X)) -> MARK(2ndspos(X, from(0))) MARK(2ndspos(X1, X2)) -> MARK(X1) MARK(2ndspos(X1, X2)) -> MARK(X2) ACTIVE(plus(0, Y)) -> MARK(Y) MARK(rcons(X1, X2)) -> MARK(X1) MARK(rcons(X1, X2)) -> MARK(X2) ACTIVE(plus(s(X), Y)) -> MARK(s(plus(X, Y))) MARK(posrecip(X)) -> MARK(X) MARK(2ndsneg(X1, X2)) -> ACTIVE(2ndsneg(mark(X1), mark(X2))) ACTIVE(times(s(X), Y)) -> MARK(plus(Y, times(X, Y))) MARK(2ndsneg(X1, X2)) -> MARK(X1) MARK(2ndsneg(X1, X2)) -> MARK(X2) ACTIVE(square(X)) -> MARK(times(X, X)) MARK(negrecip(X)) -> MARK(X) MARK(pi(X)) -> ACTIVE(pi(mark(X))) MARK(pi(X)) -> MARK(X) MARK(plus(X1, X2)) -> ACTIVE(plus(mark(X1), mark(X2))) MARK(plus(X1, X2)) -> MARK(X1) MARK(plus(X1, X2)) -> MARK(X2) MARK(times(X1, X2)) -> ACTIVE(times(mark(X1), mark(X2))) MARK(times(X1, X2)) -> MARK(X1) MARK(times(X1, X2)) -> MARK(X2) MARK(square(X)) -> ACTIVE(square(mark(X))) MARK(square(X)) -> MARK(X) The TRS R consists of the following rules: active(from(X)) -> mark(cons(X, from(s(X)))) active(2ndspos(0, Z)) -> mark(rnil) active(2ndspos(s(N), cons(X, cons(Y, Z)))) -> mark(rcons(posrecip(Y), 2ndsneg(N, Z))) active(2ndsneg(0, Z)) -> mark(rnil) active(2ndsneg(s(N), cons(X, cons(Y, Z)))) -> mark(rcons(negrecip(Y), 2ndspos(N, Z))) active(pi(X)) -> mark(2ndspos(X, from(0))) active(plus(0, Y)) -> mark(Y) active(plus(s(X), Y)) -> mark(s(plus(X, Y))) active(times(0, Y)) -> mark(0) active(times(s(X), Y)) -> mark(plus(Y, times(X, Y))) active(square(X)) -> mark(times(X, X)) mark(from(X)) -> active(from(mark(X))) mark(cons(X1, X2)) -> active(cons(mark(X1), X2)) mark(s(X)) -> active(s(mark(X))) mark(2ndspos(X1, X2)) -> active(2ndspos(mark(X1), mark(X2))) mark(0) -> active(0) mark(rnil) -> active(rnil) mark(rcons(X1, X2)) -> active(rcons(mark(X1), mark(X2))) mark(posrecip(X)) -> active(posrecip(mark(X))) mark(2ndsneg(X1, X2)) -> active(2ndsneg(mark(X1), mark(X2))) mark(negrecip(X)) -> active(negrecip(mark(X))) mark(pi(X)) -> active(pi(mark(X))) mark(plus(X1, X2)) -> active(plus(mark(X1), mark(X2))) mark(times(X1, X2)) -> active(times(mark(X1), mark(X2))) mark(square(X)) -> active(square(mark(X))) from(mark(X)) -> from(X) from(active(X)) -> from(X) cons(mark(X1), X2) -> cons(X1, X2) cons(X1, mark(X2)) -> cons(X1, X2) cons(active(X1), X2) -> cons(X1, X2) cons(X1, active(X2)) -> cons(X1, X2) s(mark(X)) -> s(X) s(active(X)) -> s(X) 2ndspos(mark(X1), X2) -> 2ndspos(X1, X2) 2ndspos(X1, mark(X2)) -> 2ndspos(X1, X2) 2ndspos(active(X1), X2) -> 2ndspos(X1, X2) 2ndspos(X1, active(X2)) -> 2ndspos(X1, X2) rcons(mark(X1), X2) -> rcons(X1, X2) rcons(X1, mark(X2)) -> rcons(X1, X2) rcons(active(X1), X2) -> rcons(X1, X2) rcons(X1, active(X2)) -> rcons(X1, X2) posrecip(mark(X)) -> posrecip(X) posrecip(active(X)) -> posrecip(X) 2ndsneg(mark(X1), X2) -> 2ndsneg(X1, X2) 2ndsneg(X1, mark(X2)) -> 2ndsneg(X1, X2) 2ndsneg(active(X1), X2) -> 2ndsneg(X1, X2) 2ndsneg(X1, active(X2)) -> 2ndsneg(X1, X2) negrecip(mark(X)) -> negrecip(X) negrecip(active(X)) -> negrecip(X) pi(mark(X)) -> pi(X) pi(active(X)) -> pi(X) plus(mark(X1), X2) -> plus(X1, X2) plus(X1, mark(X2)) -> plus(X1, X2) plus(active(X1), X2) -> plus(X1, X2) plus(X1, active(X2)) -> plus(X1, X2) times(mark(X1), X2) -> times(X1, X2) times(X1, mark(X2)) -> times(X1, X2) times(active(X1), X2) -> times(X1, X2) times(X1, active(X2)) -> times(X1, X2) square(mark(X)) -> square(X) square(active(X)) -> square(X) Q is empty. We have to consider all minimal (P,Q,R)-chains. ---------------------------------------- (76) QDPOrderProof (EQUIVALENT) We use the reduction pair processor [LPAR04,JAR06]. The following pairs can be oriented strictly and are deleted. MARK(2ndsneg(X1, X2)) -> MARK(X1) The remaining pairs can at least be oriented weakly. Used ordering: Matrix interpretation [MATRO] with arctic natural numbers [ARCTIC]: <<< POL(MARK(x_1)) = [[1A]] + [[1A]] * x_1 >>> <<< POL(from(x_1)) = [[0A]] + [[0A]] * x_1 >>> <<< POL(ACTIVE(x_1)) = [[1A]] + [[1A]] * x_1 >>> <<< POL(mark(x_1)) = [[-I]] + [[0A]] * x_1 >>> <<< POL(cons(x_1, x_2)) = [[-I]] + [[0A]] * x_1 + [[0A]] * x_2 >>> <<< POL(s(x_1)) = [[0A]] + [[0A]] * x_1 >>> <<< POL(2ndspos(x_1, x_2)) = [[-I]] + [[2A]] * x_1 + [[0A]] * x_2 >>> <<< POL(rcons(x_1, x_2)) = [[-I]] + [[0A]] * x_1 + [[0A]] * x_2 >>> <<< POL(posrecip(x_1)) = [[-I]] + [[0A]] * x_1 >>> <<< POL(2ndsneg(x_1, x_2)) = [[1A]] + [[2A]] * x_1 + [[0A]] * x_2 >>> <<< POL(negrecip(x_1)) = [[2A]] + [[0A]] * x_1 >>> <<< POL(pi(x_1)) = [[0A]] + [[3A]] * x_1 >>> <<< POL(0) = [[0A]] >>> <<< POL(plus(x_1, x_2)) = [[-I]] + [[1A]] * x_1 + [[0A]] * x_2 >>> <<< POL(times(x_1, x_2)) = [[-I]] + [[4A]] * x_1 + [[1A]] * x_2 >>> <<< POL(square(x_1)) = [[0A]] + [[4A]] * x_1 >>> <<< POL(active(x_1)) = [[-I]] + [[0A]] * x_1 >>> <<< POL(rnil) = [[0A]] >>> The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented: mark(from(X)) -> active(from(mark(X))) active(from(X)) -> mark(cons(X, from(s(X)))) mark(cons(X1, X2)) -> active(cons(mark(X1), X2)) active(2ndspos(s(N), cons(X, cons(Y, Z)))) -> mark(rcons(posrecip(Y), 2ndsneg(N, Z))) mark(s(X)) -> active(s(mark(X))) active(2ndsneg(s(N), cons(X, cons(Y, Z)))) -> mark(rcons(negrecip(Y), 2ndspos(N, Z))) mark(2ndspos(X1, X2)) -> active(2ndspos(mark(X1), mark(X2))) active(pi(X)) -> mark(2ndspos(X, from(0))) mark(rcons(X1, X2)) -> active(rcons(mark(X1), mark(X2))) active(plus(0, Y)) -> mark(Y) mark(posrecip(X)) -> active(posrecip(mark(X))) active(plus(s(X), Y)) -> mark(s(plus(X, Y))) mark(2ndsneg(X1, X2)) -> active(2ndsneg(mark(X1), mark(X2))) active(times(s(X), Y)) -> mark(plus(Y, times(X, Y))) mark(negrecip(X)) -> active(negrecip(mark(X))) active(square(X)) -> mark(times(X, X)) mark(pi(X)) -> active(pi(mark(X))) mark(plus(X1, X2)) -> active(plus(mark(X1), mark(X2))) mark(times(X1, X2)) -> active(times(mark(X1), mark(X2))) mark(square(X)) -> active(square(mark(X))) mark(0) -> active(0) mark(rnil) -> active(rnil) from(active(X)) -> from(X) from(mark(X)) -> from(X) s(active(X)) -> s(X) s(mark(X)) -> s(X) cons(X1, mark(X2)) -> cons(X1, X2) cons(mark(X1), X2) -> cons(X1, X2) cons(active(X1), X2) -> cons(X1, X2) cons(X1, active(X2)) -> cons(X1, X2) posrecip(active(X)) -> posrecip(X) posrecip(mark(X)) -> posrecip(X) 2ndsneg(X1, mark(X2)) -> 2ndsneg(X1, X2) 2ndsneg(mark(X1), X2) -> 2ndsneg(X1, X2) 2ndsneg(active(X1), X2) -> 2ndsneg(X1, X2) 2ndsneg(X1, active(X2)) -> 2ndsneg(X1, X2) rcons(X1, mark(X2)) -> rcons(X1, X2) rcons(mark(X1), X2) -> rcons(X1, X2) rcons(active(X1), X2) -> rcons(X1, X2) rcons(X1, active(X2)) -> rcons(X1, X2) negrecip(active(X)) -> negrecip(X) negrecip(mark(X)) -> negrecip(X) 2ndspos(X1, mark(X2)) -> 2ndspos(X1, X2) 2ndspos(mark(X1), X2) -> 2ndspos(X1, X2) 2ndspos(active(X1), X2) -> 2ndspos(X1, X2) 2ndspos(X1, active(X2)) -> 2ndspos(X1, X2) plus(X1, mark(X2)) -> plus(X1, X2) plus(mark(X1), X2) -> plus(X1, X2) plus(active(X1), X2) -> plus(X1, X2) plus(X1, active(X2)) -> plus(X1, X2) times(X1, mark(X2)) -> times(X1, X2) times(mark(X1), X2) -> times(X1, X2) times(active(X1), X2) -> times(X1, X2) times(X1, active(X2)) -> times(X1, X2) pi(active(X)) -> pi(X) pi(mark(X)) -> pi(X) square(active(X)) -> square(X) square(mark(X)) -> square(X) active(2ndspos(0, Z)) -> mark(rnil) active(2ndsneg(0, Z)) -> mark(rnil) active(times(0, Y)) -> mark(0) ---------------------------------------- (77) Obligation: Q DP problem: The TRS P consists of the following rules: MARK(from(X)) -> ACTIVE(from(mark(X))) ACTIVE(from(X)) -> MARK(cons(X, from(s(X)))) MARK(from(X)) -> MARK(X) ACTIVE(2ndspos(s(N), cons(X, cons(Y, Z)))) -> MARK(rcons(posrecip(Y), 2ndsneg(N, Z))) MARK(cons(X1, X2)) -> MARK(X1) ACTIVE(2ndsneg(s(N), cons(X, cons(Y, Z)))) -> MARK(rcons(negrecip(Y), 2ndspos(N, Z))) MARK(s(X)) -> MARK(X) MARK(2ndspos(X1, X2)) -> ACTIVE(2ndspos(mark(X1), mark(X2))) ACTIVE(pi(X)) -> MARK(2ndspos(X, from(0))) MARK(2ndspos(X1, X2)) -> MARK(X1) MARK(2ndspos(X1, X2)) -> MARK(X2) ACTIVE(plus(0, Y)) -> MARK(Y) MARK(rcons(X1, X2)) -> MARK(X1) MARK(rcons(X1, X2)) -> MARK(X2) ACTIVE(plus(s(X), Y)) -> MARK(s(plus(X, Y))) MARK(posrecip(X)) -> MARK(X) MARK(2ndsneg(X1, X2)) -> ACTIVE(2ndsneg(mark(X1), mark(X2))) ACTIVE(times(s(X), Y)) -> MARK(plus(Y, times(X, Y))) MARK(2ndsneg(X1, X2)) -> MARK(X2) ACTIVE(square(X)) -> MARK(times(X, X)) MARK(negrecip(X)) -> MARK(X) MARK(pi(X)) -> ACTIVE(pi(mark(X))) MARK(pi(X)) -> MARK(X) MARK(plus(X1, X2)) -> ACTIVE(plus(mark(X1), mark(X2))) MARK(plus(X1, X2)) -> MARK(X1) MARK(plus(X1, X2)) -> MARK(X2) MARK(times(X1, X2)) -> ACTIVE(times(mark(X1), mark(X2))) MARK(times(X1, X2)) -> MARK(X1) MARK(times(X1, X2)) -> MARK(X2) MARK(square(X)) -> ACTIVE(square(mark(X))) MARK(square(X)) -> MARK(X) The TRS R consists of the following rules: active(from(X)) -> mark(cons(X, from(s(X)))) active(2ndspos(0, Z)) -> mark(rnil) active(2ndspos(s(N), cons(X, cons(Y, Z)))) -> mark(rcons(posrecip(Y), 2ndsneg(N, Z))) active(2ndsneg(0, Z)) -> mark(rnil) active(2ndsneg(s(N), cons(X, cons(Y, Z)))) -> mark(rcons(negrecip(Y), 2ndspos(N, Z))) active(pi(X)) -> mark(2ndspos(X, from(0))) active(plus(0, Y)) -> mark(Y) active(plus(s(X), Y)) -> mark(s(plus(X, Y))) active(times(0, Y)) -> mark(0) active(times(s(X), Y)) -> mark(plus(Y, times(X, Y))) active(square(X)) -> mark(times(X, X)) mark(from(X)) -> active(from(mark(X))) mark(cons(X1, X2)) -> active(cons(mark(X1), X2)) mark(s(X)) -> active(s(mark(X))) mark(2ndspos(X1, X2)) -> active(2ndspos(mark(X1), mark(X2))) mark(0) -> active(0) mark(rnil) -> active(rnil) mark(rcons(X1, X2)) -> active(rcons(mark(X1), mark(X2))) mark(posrecip(X)) -> active(posrecip(mark(X))) mark(2ndsneg(X1, X2)) -> active(2ndsneg(mark(X1), mark(X2))) mark(negrecip(X)) -> active(negrecip(mark(X))) mark(pi(X)) -> active(pi(mark(X))) mark(plus(X1, X2)) -> active(plus(mark(X1), mark(X2))) mark(times(X1, X2)) -> active(times(mark(X1), mark(X2))) mark(square(X)) -> active(square(mark(X))) from(mark(X)) -> from(X) from(active(X)) -> from(X) cons(mark(X1), X2) -> cons(X1, X2) cons(X1, mark(X2)) -> cons(X1, X2) cons(active(X1), X2) -> cons(X1, X2) cons(X1, active(X2)) -> cons(X1, X2) s(mark(X)) -> s(X) s(active(X)) -> s(X) 2ndspos(mark(X1), X2) -> 2ndspos(X1, X2) 2ndspos(X1, mark(X2)) -> 2ndspos(X1, X2) 2ndspos(active(X1), X2) -> 2ndspos(X1, X2) 2ndspos(X1, active(X2)) -> 2ndspos(X1, X2) rcons(mark(X1), X2) -> rcons(X1, X2) rcons(X1, mark(X2)) -> rcons(X1, X2) rcons(active(X1), X2) -> rcons(X1, X2) rcons(X1, active(X2)) -> rcons(X1, X2) posrecip(mark(X)) -> posrecip(X) posrecip(active(X)) -> posrecip(X) 2ndsneg(mark(X1), X2) -> 2ndsneg(X1, X2) 2ndsneg(X1, mark(X2)) -> 2ndsneg(X1, X2) 2ndsneg(active(X1), X2) -> 2ndsneg(X1, X2) 2ndsneg(X1, active(X2)) -> 2ndsneg(X1, X2) negrecip(mark(X)) -> negrecip(X) negrecip(active(X)) -> negrecip(X) pi(mark(X)) -> pi(X) pi(active(X)) -> pi(X) plus(mark(X1), X2) -> plus(X1, X2) plus(X1, mark(X2)) -> plus(X1, X2) plus(active(X1), X2) -> plus(X1, X2) plus(X1, active(X2)) -> plus(X1, X2) times(mark(X1), X2) -> times(X1, X2) times(X1, mark(X2)) -> times(X1, X2) times(active(X1), X2) -> times(X1, X2) times(X1, active(X2)) -> times(X1, X2) square(mark(X)) -> square(X) square(active(X)) -> square(X) Q is empty. We have to consider all minimal (P,Q,R)-chains. ---------------------------------------- (78) QDPOrderProof (EQUIVALENT) We use the reduction pair processor [LPAR04,JAR06]. The following pairs can be oriented strictly and are deleted. ACTIVE(pi(X)) -> MARK(2ndspos(X, from(0))) MARK(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)) = [[3A]] + [[0A]] * x_1 >>> <<< POL(from(x_1)) = [[4A]] + [[0A]] * x_1 >>> <<< POL(ACTIVE(x_1)) = [[1A]] + [[0A]] * x_1 >>> <<< POL(mark(x_1)) = [[4A]] + [[0A]] * x_1 >>> <<< POL(cons(x_1, x_2)) = [[-I]] + [[0A]] * x_1 + [[0A]] * x_2 >>> <<< POL(s(x_1)) = [[-I]] + [[0A]] * x_1 >>> <<< POL(2ndspos(x_1, x_2)) = [[4A]] + [[0A]] * x_1 + [[0A]] * x_2 >>> <<< POL(rcons(x_1, x_2)) = [[-I]] + [[0A]] * x_1 + [[0A]] * x_2 >>> <<< POL(posrecip(x_1)) = [[-I]] + [[0A]] * x_1 >>> <<< POL(2ndsneg(x_1, x_2)) = [[4A]] + [[0A]] * x_1 + [[0A]] * x_2 >>> <<< POL(negrecip(x_1)) = [[-I]] + [[0A]] * x_1 >>> <<< POL(pi(x_1)) = [[5A]] + [[1A]] * x_1 >>> <<< POL(0) = [[0A]] >>> <<< POL(plus(x_1, x_2)) = [[4A]] + [[0A]] * x_1 + [[0A]] * x_2 >>> <<< POL(times(x_1, x_2)) = [[4A]] + [[0A]] * x_1 + [[0A]] * x_2 >>> <<< POL(square(x_1)) = [[4A]] + [[0A]] * x_1 >>> <<< POL(active(x_1)) = [[4A]] + [[0A]] * x_1 >>> <<< POL(rnil) = [[3A]] >>> The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented: mark(from(X)) -> active(from(mark(X))) active(from(X)) -> mark(cons(X, from(s(X)))) mark(cons(X1, X2)) -> active(cons(mark(X1), X2)) active(2ndspos(s(N), cons(X, cons(Y, Z)))) -> mark(rcons(posrecip(Y), 2ndsneg(N, Z))) mark(s(X)) -> active(s(mark(X))) active(2ndsneg(s(N), cons(X, cons(Y, Z)))) -> mark(rcons(negrecip(Y), 2ndspos(N, Z))) mark(2ndspos(X1, X2)) -> active(2ndspos(mark(X1), mark(X2))) active(pi(X)) -> mark(2ndspos(X, from(0))) mark(rcons(X1, X2)) -> active(rcons(mark(X1), mark(X2))) active(plus(0, Y)) -> mark(Y) mark(posrecip(X)) -> active(posrecip(mark(X))) active(plus(s(X), Y)) -> mark(s(plus(X, Y))) mark(2ndsneg(X1, X2)) -> active(2ndsneg(mark(X1), mark(X2))) active(times(s(X), Y)) -> mark(plus(Y, times(X, Y))) mark(negrecip(X)) -> active(negrecip(mark(X))) active(square(X)) -> mark(times(X, X)) mark(pi(X)) -> active(pi(mark(X))) mark(plus(X1, X2)) -> active(plus(mark(X1), mark(X2))) mark(times(X1, X2)) -> active(times(mark(X1), mark(X2))) mark(square(X)) -> active(square(mark(X))) mark(0) -> active(0) mark(rnil) -> active(rnil) from(active(X)) -> from(X) from(mark(X)) -> from(X) s(active(X)) -> s(X) s(mark(X)) -> s(X) cons(X1, mark(X2)) -> cons(X1, X2) cons(mark(X1), X2) -> cons(X1, X2) cons(active(X1), X2) -> cons(X1, X2) cons(X1, active(X2)) -> cons(X1, X2) posrecip(active(X)) -> posrecip(X) posrecip(mark(X)) -> posrecip(X) 2ndsneg(X1, mark(X2)) -> 2ndsneg(X1, X2) 2ndsneg(mark(X1), X2) -> 2ndsneg(X1, X2) 2ndsneg(active(X1), X2) -> 2ndsneg(X1, X2) 2ndsneg(X1, active(X2)) -> 2ndsneg(X1, X2) rcons(X1, mark(X2)) -> rcons(X1, X2) rcons(mark(X1), X2) -> rcons(X1, X2) rcons(active(X1), X2) -> rcons(X1, X2) rcons(X1, active(X2)) -> rcons(X1, X2) negrecip(active(X)) -> negrecip(X) negrecip(mark(X)) -> negrecip(X) 2ndspos(X1, mark(X2)) -> 2ndspos(X1, X2) 2ndspos(mark(X1), X2) -> 2ndspos(X1, X2) 2ndspos(active(X1), X2) -> 2ndspos(X1, X2) 2ndspos(X1, active(X2)) -> 2ndspos(X1, X2) plus(X1, mark(X2)) -> plus(X1, X2) plus(mark(X1), X2) -> plus(X1, X2) plus(active(X1), X2) -> plus(X1, X2) plus(X1, active(X2)) -> plus(X1, X2) times(X1, mark(X2)) -> times(X1, X2) times(mark(X1), X2) -> times(X1, X2) times(active(X1), X2) -> times(X1, X2) times(X1, active(X2)) -> times(X1, X2) pi(active(X)) -> pi(X) pi(mark(X)) -> pi(X) square(active(X)) -> square(X) square(mark(X)) -> square(X) active(2ndspos(0, Z)) -> mark(rnil) active(2ndsneg(0, Z)) -> mark(rnil) active(times(0, Y)) -> mark(0) ---------------------------------------- (79) Obligation: Q DP problem: The TRS P consists of the following rules: MARK(from(X)) -> ACTIVE(from(mark(X))) ACTIVE(from(X)) -> MARK(cons(X, from(s(X)))) MARK(from(X)) -> MARK(X) ACTIVE(2ndspos(s(N), cons(X, cons(Y, Z)))) -> MARK(rcons(posrecip(Y), 2ndsneg(N, Z))) MARK(cons(X1, X2)) -> MARK(X1) ACTIVE(2ndsneg(s(N), cons(X, cons(Y, Z)))) -> MARK(rcons(negrecip(Y), 2ndspos(N, Z))) MARK(s(X)) -> MARK(X) MARK(2ndspos(X1, X2)) -> ACTIVE(2ndspos(mark(X1), mark(X2))) MARK(2ndspos(X1, X2)) -> MARK(X1) MARK(2ndspos(X1, X2)) -> MARK(X2) ACTIVE(plus(0, Y)) -> MARK(Y) MARK(rcons(X1, X2)) -> MARK(X1) MARK(rcons(X1, X2)) -> MARK(X2) ACTIVE(plus(s(X), Y)) -> MARK(s(plus(X, Y))) MARK(posrecip(X)) -> MARK(X) MARK(2ndsneg(X1, X2)) -> ACTIVE(2ndsneg(mark(X1), mark(X2))) ACTIVE(times(s(X), Y)) -> MARK(plus(Y, times(X, Y))) MARK(2ndsneg(X1, X2)) -> MARK(X2) ACTIVE(square(X)) -> MARK(times(X, X)) MARK(negrecip(X)) -> MARK(X) MARK(pi(X)) -> ACTIVE(pi(mark(X))) MARK(plus(X1, X2)) -> ACTIVE(plus(mark(X1), mark(X2))) MARK(plus(X1, X2)) -> MARK(X1) MARK(plus(X1, X2)) -> MARK(X2) MARK(times(X1, X2)) -> ACTIVE(times(mark(X1), mark(X2))) MARK(times(X1, X2)) -> MARK(X1) MARK(times(X1, X2)) -> MARK(X2) MARK(square(X)) -> ACTIVE(square(mark(X))) MARK(square(X)) -> MARK(X) The TRS R consists of the following rules: active(from(X)) -> mark(cons(X, from(s(X)))) active(2ndspos(0, Z)) -> mark(rnil) active(2ndspos(s(N), cons(X, cons(Y, Z)))) -> mark(rcons(posrecip(Y), 2ndsneg(N, Z))) active(2ndsneg(0, Z)) -> mark(rnil) active(2ndsneg(s(N), cons(X, cons(Y, Z)))) -> mark(rcons(negrecip(Y), 2ndspos(N, Z))) active(pi(X)) -> mark(2ndspos(X, from(0))) active(plus(0, Y)) -> mark(Y) active(plus(s(X), Y)) -> mark(s(plus(X, Y))) active(times(0, Y)) -> mark(0) active(times(s(X), Y)) -> mark(plus(Y, times(X, Y))) active(square(X)) -> mark(times(X, X)) mark(from(X)) -> active(from(mark(X))) mark(cons(X1, X2)) -> active(cons(mark(X1), X2)) mark(s(X)) -> active(s(mark(X))) mark(2ndspos(X1, X2)) -> active(2ndspos(mark(X1), mark(X2))) mark(0) -> active(0) mark(rnil) -> active(rnil) mark(rcons(X1, X2)) -> active(rcons(mark(X1), mark(X2))) mark(posrecip(X)) -> active(posrecip(mark(X))) mark(2ndsneg(X1, X2)) -> active(2ndsneg(mark(X1), mark(X2))) mark(negrecip(X)) -> active(negrecip(mark(X))) mark(pi(X)) -> active(pi(mark(X))) mark(plus(X1, X2)) -> active(plus(mark(X1), mark(X2))) mark(times(X1, X2)) -> active(times(mark(X1), mark(X2))) mark(square(X)) -> active(square(mark(X))) from(mark(X)) -> from(X) from(active(X)) -> from(X) cons(mark(X1), X2) -> cons(X1, X2) cons(X1, mark(X2)) -> cons(X1, X2) cons(active(X1), X2) -> cons(X1, X2) cons(X1, active(X2)) -> cons(X1, X2) s(mark(X)) -> s(X) s(active(X)) -> s(X) 2ndspos(mark(X1), X2) -> 2ndspos(X1, X2) 2ndspos(X1, mark(X2)) -> 2ndspos(X1, X2) 2ndspos(active(X1), X2) -> 2ndspos(X1, X2) 2ndspos(X1, active(X2)) -> 2ndspos(X1, X2) rcons(mark(X1), X2) -> rcons(X1, X2) rcons(X1, mark(X2)) -> rcons(X1, X2) rcons(active(X1), X2) -> rcons(X1, X2) rcons(X1, active(X2)) -> rcons(X1, X2) posrecip(mark(X)) -> posrecip(X) posrecip(active(X)) -> posrecip(X) 2ndsneg(mark(X1), X2) -> 2ndsneg(X1, X2) 2ndsneg(X1, mark(X2)) -> 2ndsneg(X1, X2) 2ndsneg(active(X1), X2) -> 2ndsneg(X1, X2) 2ndsneg(X1, active(X2)) -> 2ndsneg(X1, X2) negrecip(mark(X)) -> negrecip(X) negrecip(active(X)) -> negrecip(X) pi(mark(X)) -> pi(X) pi(active(X)) -> pi(X) plus(mark(X1), X2) -> plus(X1, X2) plus(X1, mark(X2)) -> plus(X1, X2) plus(active(X1), X2) -> plus(X1, X2) plus(X1, active(X2)) -> plus(X1, X2) times(mark(X1), X2) -> times(X1, X2) times(X1, mark(X2)) -> times(X1, X2) times(active(X1), X2) -> times(X1, X2) times(X1, active(X2)) -> times(X1, X2) square(mark(X)) -> square(X) square(active(X)) -> square(X) Q is empty. We have to consider all minimal (P,Q,R)-chains. ---------------------------------------- (80) QDPOrderProof (EQUIVALENT) We use the reduction pair processor [LPAR04,JAR06]. The following pairs can be oriented strictly and are deleted. MARK(pi(X)) -> ACTIVE(pi(mark(X))) The remaining pairs can at least be oriented weakly. Used ordering: Polynomial Order [NEGPOLO,POLO] with Interpretation: POL( 2ndsneg_2(x_1, x_2) ) = 2 POL( ACTIVE_1(x_1) ) = max{0, 2x_1 - 2} POL( 2ndspos_2(x_1, x_2) ) = 2 POL( from_1(x_1) ) = 2 POL( pi_1(x_1) ) = 1 POL( plus_2(x_1, x_2) ) = 2 POL( square_1(x_1) ) = 2 POL( times_2(x_1, x_2) ) = 2 POL( mark_1(x_1) ) = x_1 + 2 POL( active_1(x_1) ) = max{0, x_1 - 1} POL( cons_2(x_1, x_2) ) = 2x_1 + 2x_2 + 1 POL( s_1(x_1) ) = x_1 POL( rcons_2(x_1, x_2) ) = 2x_1 + 2 POL( posrecip_1(x_1) ) = max{0, -2} POL( negrecip_1(x_1) ) = x_1 + 1 POL( 0 ) = 1 POL( rnil ) = 1 POL( MARK_1(x_1) ) = 2 The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented: from(active(X)) -> from(X) from(mark(X)) -> from(X) 2ndsneg(X1, mark(X2)) -> 2ndsneg(X1, X2) 2ndsneg(mark(X1), X2) -> 2ndsneg(X1, X2) 2ndsneg(active(X1), X2) -> 2ndsneg(X1, X2) 2ndsneg(X1, active(X2)) -> 2ndsneg(X1, X2) 2ndspos(X1, mark(X2)) -> 2ndspos(X1, X2) 2ndspos(mark(X1), X2) -> 2ndspos(X1, X2) 2ndspos(active(X1), X2) -> 2ndspos(X1, X2) 2ndspos(X1, active(X2)) -> 2ndspos(X1, X2) plus(X1, mark(X2)) -> plus(X1, X2) plus(mark(X1), X2) -> plus(X1, X2) plus(active(X1), X2) -> plus(X1, X2) plus(X1, active(X2)) -> plus(X1, X2) times(X1, mark(X2)) -> times(X1, X2) times(mark(X1), X2) -> times(X1, X2) times(active(X1), X2) -> times(X1, X2) times(X1, active(X2)) -> times(X1, X2) pi(active(X)) -> pi(X) pi(mark(X)) -> pi(X) square(active(X)) -> square(X) square(mark(X)) -> square(X) ---------------------------------------- (81) Obligation: Q DP problem: The TRS P consists of the following rules: MARK(from(X)) -> ACTIVE(from(mark(X))) ACTIVE(from(X)) -> MARK(cons(X, from(s(X)))) MARK(from(X)) -> MARK(X) ACTIVE(2ndspos(s(N), cons(X, cons(Y, Z)))) -> MARK(rcons(posrecip(Y), 2ndsneg(N, Z))) MARK(cons(X1, X2)) -> MARK(X1) ACTIVE(2ndsneg(s(N), cons(X, cons(Y, Z)))) -> MARK(rcons(negrecip(Y), 2ndspos(N, Z))) MARK(s(X)) -> MARK(X) MARK(2ndspos(X1, X2)) -> ACTIVE(2ndspos(mark(X1), mark(X2))) MARK(2ndspos(X1, X2)) -> MARK(X1) MARK(2ndspos(X1, X2)) -> MARK(X2) ACTIVE(plus(0, Y)) -> MARK(Y) MARK(rcons(X1, X2)) -> MARK(X1) MARK(rcons(X1, X2)) -> MARK(X2) ACTIVE(plus(s(X), Y)) -> MARK(s(plus(X, Y))) MARK(posrecip(X)) -> MARK(X) MARK(2ndsneg(X1, X2)) -> ACTIVE(2ndsneg(mark(X1), mark(X2))) ACTIVE(times(s(X), Y)) -> MARK(plus(Y, times(X, Y))) MARK(2ndsneg(X1, X2)) -> MARK(X2) ACTIVE(square(X)) -> MARK(times(X, X)) MARK(negrecip(X)) -> MARK(X) MARK(plus(X1, X2)) -> ACTIVE(plus(mark(X1), mark(X2))) MARK(plus(X1, X2)) -> MARK(X1) MARK(plus(X1, X2)) -> MARK(X2) MARK(times(X1, X2)) -> ACTIVE(times(mark(X1), mark(X2))) MARK(times(X1, X2)) -> MARK(X1) MARK(times(X1, X2)) -> MARK(X2) MARK(square(X)) -> ACTIVE(square(mark(X))) MARK(square(X)) -> MARK(X) The TRS R consists of the following rules: active(from(X)) -> mark(cons(X, from(s(X)))) active(2ndspos(0, Z)) -> mark(rnil) active(2ndspos(s(N), cons(X, cons(Y, Z)))) -> mark(rcons(posrecip(Y), 2ndsneg(N, Z))) active(2ndsneg(0, Z)) -> mark(rnil) active(2ndsneg(s(N), cons(X, cons(Y, Z)))) -> mark(rcons(negrecip(Y), 2ndspos(N, Z))) active(pi(X)) -> mark(2ndspos(X, from(0))) active(plus(0, Y)) -> mark(Y) active(plus(s(X), Y)) -> mark(s(plus(X, Y))) active(times(0, Y)) -> mark(0) active(times(s(X), Y)) -> mark(plus(Y, times(X, Y))) active(square(X)) -> mark(times(X, X)) mark(from(X)) -> active(from(mark(X))) mark(cons(X1, X2)) -> active(cons(mark(X1), X2)) mark(s(X)) -> active(s(mark(X))) mark(2ndspos(X1, X2)) -> active(2ndspos(mark(X1), mark(X2))) mark(0) -> active(0) mark(rnil) -> active(rnil) mark(rcons(X1, X2)) -> active(rcons(mark(X1), mark(X2))) mark(posrecip(X)) -> active(posrecip(mark(X))) mark(2ndsneg(X1, X2)) -> active(2ndsneg(mark(X1), mark(X2))) mark(negrecip(X)) -> active(negrecip(mark(X))) mark(pi(X)) -> active(pi(mark(X))) mark(plus(X1, X2)) -> active(plus(mark(X1), mark(X2))) mark(times(X1, X2)) -> active(times(mark(X1), mark(X2))) mark(square(X)) -> active(square(mark(X))) from(mark(X)) -> from(X) from(active(X)) -> from(X) cons(mark(X1), X2) -> cons(X1, X2) cons(X1, mark(X2)) -> cons(X1, X2) cons(active(X1), X2) -> cons(X1, X2) cons(X1, active(X2)) -> cons(X1, X2) s(mark(X)) -> s(X) s(active(X)) -> s(X) 2ndspos(mark(X1), X2) -> 2ndspos(X1, X2) 2ndspos(X1, mark(X2)) -> 2ndspos(X1, X2) 2ndspos(active(X1), X2) -> 2ndspos(X1, X2) 2ndspos(X1, active(X2)) -> 2ndspos(X1, X2) rcons(mark(X1), X2) -> rcons(X1, X2) rcons(X1, mark(X2)) -> rcons(X1, X2) rcons(active(X1), X2) -> rcons(X1, X2) rcons(X1, active(X2)) -> rcons(X1, X2) posrecip(mark(X)) -> posrecip(X) posrecip(active(X)) -> posrecip(X) 2ndsneg(mark(X1), X2) -> 2ndsneg(X1, X2) 2ndsneg(X1, mark(X2)) -> 2ndsneg(X1, X2) 2ndsneg(active(X1), X2) -> 2ndsneg(X1, X2) 2ndsneg(X1, active(X2)) -> 2ndsneg(X1, X2) negrecip(mark(X)) -> negrecip(X) negrecip(active(X)) -> negrecip(X) pi(mark(X)) -> pi(X) pi(active(X)) -> pi(X) plus(mark(X1), X2) -> plus(X1, X2) plus(X1, mark(X2)) -> plus(X1, X2) plus(active(X1), X2) -> plus(X1, X2) plus(X1, active(X2)) -> plus(X1, X2) times(mark(X1), X2) -> times(X1, X2) times(X1, mark(X2)) -> times(X1, X2) times(active(X1), X2) -> times(X1, X2) times(X1, active(X2)) -> times(X1, X2) square(mark(X)) -> square(X) square(active(X)) -> square(X) Q is empty. We have to consider all minimal (P,Q,R)-chains. ---------------------------------------- (82) 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) The remaining pairs can at least be oriented weakly. Used ordering: Matrix interpretation [MATRO] with arctic natural numbers [ARCTIC]: <<< POL(MARK(x_1)) = [[1A]] + [[1A]] * x_1 >>> <<< POL(from(x_1)) = [[-I]] + [[0A]] * x_1 >>> <<< POL(ACTIVE(x_1)) = [[1A]] + [[1A]] * x_1 >>> <<< POL(mark(x_1)) = [[0A]] + [[0A]] * x_1 >>> <<< POL(cons(x_1, x_2)) = [[-I]] + [[0A]] * x_1 + [[0A]] * x_2 >>> <<< POL(s(x_1)) = [[-I]] + [[0A]] * x_1 >>> <<< POL(2ndspos(x_1, x_2)) = [[1A]] + [[1A]] * x_1 + [[0A]] * x_2 >>> <<< POL(rcons(x_1, x_2)) = [[-I]] + [[0A]] * x_1 + [[0A]] * x_2 >>> <<< POL(posrecip(x_1)) = [[1A]] + [[0A]] * x_1 >>> <<< POL(2ndsneg(x_1, x_2)) = [[1A]] + [[1A]] * x_1 + [[0A]] * x_2 >>> <<< POL(negrecip(x_1)) = [[-I]] + [[0A]] * x_1 >>> <<< POL(plus(x_1, x_2)) = [[-I]] + [[0A]] * x_1 + [[0A]] * x_2 >>> <<< POL(0) = [[2A]] >>> <<< POL(times(x_1, x_2)) = [[-I]] + [[0A]] * x_1 + [[0A]] * x_2 >>> <<< POL(square(x_1)) = [[0A]] + [[0A]] * x_1 >>> <<< POL(active(x_1)) = [[0A]] + [[0A]] * x_1 >>> <<< POL(pi(x_1)) = [[3A]] + [[3A]] * x_1 >>> <<< POL(rnil) = [[0A]] >>> The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented: mark(from(X)) -> active(from(mark(X))) active(from(X)) -> mark(cons(X, from(s(X)))) mark(cons(X1, X2)) -> active(cons(mark(X1), X2)) active(2ndspos(s(N), cons(X, cons(Y, Z)))) -> mark(rcons(posrecip(Y), 2ndsneg(N, Z))) mark(s(X)) -> active(s(mark(X))) active(2ndsneg(s(N), cons(X, cons(Y, Z)))) -> mark(rcons(negrecip(Y), 2ndspos(N, Z))) mark(2ndspos(X1, X2)) -> active(2ndspos(mark(X1), mark(X2))) active(pi(X)) -> mark(2ndspos(X, from(0))) mark(rcons(X1, X2)) -> active(rcons(mark(X1), mark(X2))) active(plus(0, Y)) -> mark(Y) mark(posrecip(X)) -> active(posrecip(mark(X))) active(plus(s(X), Y)) -> mark(s(plus(X, Y))) mark(2ndsneg(X1, X2)) -> active(2ndsneg(mark(X1), mark(X2))) active(times(s(X), Y)) -> mark(plus(Y, times(X, Y))) mark(negrecip(X)) -> active(negrecip(mark(X))) active(square(X)) -> mark(times(X, X)) mark(pi(X)) -> active(pi(mark(X))) mark(plus(X1, X2)) -> active(plus(mark(X1), mark(X2))) mark(times(X1, X2)) -> active(times(mark(X1), mark(X2))) mark(square(X)) -> active(square(mark(X))) mark(0) -> active(0) mark(rnil) -> active(rnil) from(active(X)) -> from(X) from(mark(X)) -> from(X) s(active(X)) -> s(X) s(mark(X)) -> s(X) cons(X1, mark(X2)) -> cons(X1, X2) cons(mark(X1), X2) -> cons(X1, X2) cons(active(X1), X2) -> cons(X1, X2) cons(X1, active(X2)) -> cons(X1, X2) posrecip(active(X)) -> posrecip(X) posrecip(mark(X)) -> posrecip(X) 2ndsneg(X1, mark(X2)) -> 2ndsneg(X1, X2) 2ndsneg(mark(X1), X2) -> 2ndsneg(X1, X2) 2ndsneg(active(X1), X2) -> 2ndsneg(X1, X2) 2ndsneg(X1, active(X2)) -> 2ndsneg(X1, X2) rcons(X1, mark(X2)) -> rcons(X1, X2) rcons(mark(X1), X2) -> rcons(X1, X2) rcons(active(X1), X2) -> rcons(X1, X2) rcons(X1, active(X2)) -> rcons(X1, X2) negrecip(active(X)) -> negrecip(X) negrecip(mark(X)) -> negrecip(X) 2ndspos(X1, mark(X2)) -> 2ndspos(X1, X2) 2ndspos(mark(X1), X2) -> 2ndspos(X1, X2) 2ndspos(active(X1), X2) -> 2ndspos(X1, X2) 2ndspos(X1, active(X2)) -> 2ndspos(X1, X2) plus(X1, mark(X2)) -> plus(X1, X2) plus(mark(X1), X2) -> plus(X1, X2) plus(active(X1), X2) -> plus(X1, X2) plus(X1, active(X2)) -> plus(X1, X2) times(X1, mark(X2)) -> times(X1, X2) times(mark(X1), X2) -> times(X1, X2) times(active(X1), X2) -> times(X1, X2) times(X1, active(X2)) -> times(X1, X2) square(active(X)) -> square(X) square(mark(X)) -> square(X) active(2ndspos(0, Z)) -> mark(rnil) active(2ndsneg(0, Z)) -> mark(rnil) active(times(0, Y)) -> mark(0) pi(active(X)) -> pi(X) pi(mark(X)) -> pi(X) ---------------------------------------- (83) Obligation: Q DP problem: The TRS P consists of the following rules: MARK(from(X)) -> ACTIVE(from(mark(X))) ACTIVE(from(X)) -> MARK(cons(X, from(s(X)))) MARK(from(X)) -> MARK(X) ACTIVE(2ndspos(s(N), cons(X, cons(Y, Z)))) -> MARK(rcons(posrecip(Y), 2ndsneg(N, Z))) MARK(cons(X1, X2)) -> MARK(X1) ACTIVE(2ndsneg(s(N), cons(X, cons(Y, Z)))) -> MARK(rcons(negrecip(Y), 2ndspos(N, Z))) MARK(s(X)) -> MARK(X) MARK(2ndspos(X1, X2)) -> ACTIVE(2ndspos(mark(X1), mark(X2))) MARK(2ndspos(X1, X2)) -> MARK(X2) ACTIVE(plus(0, Y)) -> MARK(Y) MARK(rcons(X1, X2)) -> MARK(X1) MARK(rcons(X1, X2)) -> MARK(X2) ACTIVE(plus(s(X), Y)) -> MARK(s(plus(X, Y))) MARK(posrecip(X)) -> MARK(X) MARK(2ndsneg(X1, X2)) -> ACTIVE(2ndsneg(mark(X1), mark(X2))) ACTIVE(times(s(X), Y)) -> MARK(plus(Y, times(X, Y))) MARK(2ndsneg(X1, X2)) -> MARK(X2) ACTIVE(square(X)) -> MARK(times(X, X)) MARK(negrecip(X)) -> MARK(X) MARK(plus(X1, X2)) -> ACTIVE(plus(mark(X1), mark(X2))) MARK(plus(X1, X2)) -> MARK(X1) MARK(plus(X1, X2)) -> MARK(X2) MARK(times(X1, X2)) -> ACTIVE(times(mark(X1), mark(X2))) MARK(times(X1, X2)) -> MARK(X1) MARK(times(X1, X2)) -> MARK(X2) MARK(square(X)) -> ACTIVE(square(mark(X))) MARK(square(X)) -> MARK(X) The TRS R consists of the following rules: active(from(X)) -> mark(cons(X, from(s(X)))) active(2ndspos(0, Z)) -> mark(rnil) active(2ndspos(s(N), cons(X, cons(Y, Z)))) -> mark(rcons(posrecip(Y), 2ndsneg(N, Z))) active(2ndsneg(0, Z)) -> mark(rnil) active(2ndsneg(s(N), cons(X, cons(Y, Z)))) -> mark(rcons(negrecip(Y), 2ndspos(N, Z))) active(pi(X)) -> mark(2ndspos(X, from(0))) active(plus(0, Y)) -> mark(Y) active(plus(s(X), Y)) -> mark(s(plus(X, Y))) active(times(0, Y)) -> mark(0) active(times(s(X), Y)) -> mark(plus(Y, times(X, Y))) active(square(X)) -> mark(times(X, X)) mark(from(X)) -> active(from(mark(X))) mark(cons(X1, X2)) -> active(cons(mark(X1), X2)) mark(s(X)) -> active(s(mark(X))) mark(2ndspos(X1, X2)) -> active(2ndspos(mark(X1), mark(X2))) mark(0) -> active(0) mark(rnil) -> active(rnil) mark(rcons(X1, X2)) -> active(rcons(mark(X1), mark(X2))) mark(posrecip(X)) -> active(posrecip(mark(X))) mark(2ndsneg(X1, X2)) -> active(2ndsneg(mark(X1), mark(X2))) mark(negrecip(X)) -> active(negrecip(mark(X))) mark(pi(X)) -> active(pi(mark(X))) mark(plus(X1, X2)) -> active(plus(mark(X1), mark(X2))) mark(times(X1, X2)) -> active(times(mark(X1), mark(X2))) mark(square(X)) -> active(square(mark(X))) from(mark(X)) -> from(X) from(active(X)) -> from(X) cons(mark(X1), X2) -> cons(X1, X2) cons(X1, mark(X2)) -> cons(X1, X2) cons(active(X1), X2) -> cons(X1, X2) cons(X1, active(X2)) -> cons(X1, X2) s(mark(X)) -> s(X) s(active(X)) -> s(X) 2ndspos(mark(X1), X2) -> 2ndspos(X1, X2) 2ndspos(X1, mark(X2)) -> 2ndspos(X1, X2) 2ndspos(active(X1), X2) -> 2ndspos(X1, X2) 2ndspos(X1, active(X2)) -> 2ndspos(X1, X2) rcons(mark(X1), X2) -> rcons(X1, X2) rcons(X1, mark(X2)) -> rcons(X1, X2) rcons(active(X1), X2) -> rcons(X1, X2) rcons(X1, active(X2)) -> rcons(X1, X2) posrecip(mark(X)) -> posrecip(X) posrecip(active(X)) -> posrecip(X) 2ndsneg(mark(X1), X2) -> 2ndsneg(X1, X2) 2ndsneg(X1, mark(X2)) -> 2ndsneg(X1, X2) 2ndsneg(active(X1), X2) -> 2ndsneg(X1, X2) 2ndsneg(X1, active(X2)) -> 2ndsneg(X1, X2) negrecip(mark(X)) -> negrecip(X) negrecip(active(X)) -> negrecip(X) pi(mark(X)) -> pi(X) pi(active(X)) -> pi(X) plus(mark(X1), X2) -> plus(X1, X2) plus(X1, mark(X2)) -> plus(X1, X2) plus(active(X1), X2) -> plus(X1, X2) plus(X1, active(X2)) -> plus(X1, X2) times(mark(X1), X2) -> times(X1, X2) times(X1, mark(X2)) -> times(X1, X2) times(active(X1), X2) -> times(X1, X2) times(X1, active(X2)) -> times(X1, X2) square(mark(X)) -> square(X) square(active(X)) -> square(X) Q is empty. We have to consider all minimal (P,Q,R)-chains. ---------------------------------------- (84) QDPOrderProof (EQUIVALENT) We use the reduction pair processor [LPAR04,JAR06]. The following pairs can be oriented strictly and are deleted. MARK(rcons(X1, X2)) -> MARK(X1) 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)) = [[3A]] + [[0A]] * x_1 >>> <<< POL(ACTIVE(x_1)) = [[-I]] + [[0A]] * x_1 >>> <<< POL(mark(x_1)) = [[2A]] + [[0A]] * x_1 >>> <<< POL(cons(x_1, x_2)) = [[-I]] + [[0A]] * x_1 + [[0A]] * x_2 >>> <<< POL(s(x_1)) = [[3A]] + [[0A]] * x_1 >>> <<< POL(2ndspos(x_1, x_2)) = [[3A]] + [[1A]] * x_1 + [[1A]] * x_2 >>> <<< POL(rcons(x_1, x_2)) = [[4A]] + [[1A]] * x_1 + [[0A]] * x_2 >>> <<< POL(posrecip(x_1)) = [[3A]] + [[0A]] * x_1 >>> <<< POL(2ndsneg(x_1, x_2)) = [[3A]] + [[1A]] * x_1 + [[1A]] * x_2 >>> <<< POL(negrecip(x_1)) = [[0A]] + [[0A]] * x_1 >>> <<< POL(plus(x_1, x_2)) = [[3A]] + [[0A]] * x_1 + [[0A]] * x_2 >>> <<< POL(0) = [[4A]] >>> <<< POL(times(x_1, x_2)) = [[-I]] + [[0A]] * x_1 + [[0A]] * x_2 >>> <<< POL(square(x_1)) = [[3A]] + [[0A]] * x_1 >>> <<< POL(active(x_1)) = [[0A]] + [[0A]] * x_1 >>> <<< POL(pi(x_1)) = [[5A]] + [[3A]] * x_1 >>> <<< POL(rnil) = [[1A]] >>> The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented: mark(from(X)) -> active(from(mark(X))) active(from(X)) -> mark(cons(X, from(s(X)))) mark(cons(X1, X2)) -> active(cons(mark(X1), X2)) active(2ndspos(s(N), cons(X, cons(Y, Z)))) -> mark(rcons(posrecip(Y), 2ndsneg(N, Z))) mark(s(X)) -> active(s(mark(X))) active(2ndsneg(s(N), cons(X, cons(Y, Z)))) -> mark(rcons(negrecip(Y), 2ndspos(N, Z))) mark(2ndspos(X1, X2)) -> active(2ndspos(mark(X1), mark(X2))) active(pi(X)) -> mark(2ndspos(X, from(0))) mark(rcons(X1, X2)) -> active(rcons(mark(X1), mark(X2))) active(plus(0, Y)) -> mark(Y) mark(posrecip(X)) -> active(posrecip(mark(X))) active(plus(s(X), Y)) -> mark(s(plus(X, Y))) mark(2ndsneg(X1, X2)) -> active(2ndsneg(mark(X1), mark(X2))) active(times(s(X), Y)) -> mark(plus(Y, times(X, Y))) mark(negrecip(X)) -> active(negrecip(mark(X))) active(square(X)) -> mark(times(X, X)) mark(pi(X)) -> active(pi(mark(X))) mark(plus(X1, X2)) -> active(plus(mark(X1), mark(X2))) mark(times(X1, X2)) -> active(times(mark(X1), mark(X2))) mark(square(X)) -> active(square(mark(X))) mark(0) -> active(0) mark(rnil) -> active(rnil) from(active(X)) -> from(X) from(mark(X)) -> from(X) s(active(X)) -> s(X) s(mark(X)) -> s(X) cons(X1, mark(X2)) -> cons(X1, X2) cons(mark(X1), X2) -> cons(X1, X2) cons(active(X1), X2) -> cons(X1, X2) cons(X1, active(X2)) -> cons(X1, X2) posrecip(active(X)) -> posrecip(X) posrecip(mark(X)) -> posrecip(X) 2ndsneg(X1, mark(X2)) -> 2ndsneg(X1, X2) 2ndsneg(mark(X1), X2) -> 2ndsneg(X1, X2) 2ndsneg(active(X1), X2) -> 2ndsneg(X1, X2) 2ndsneg(X1, active(X2)) -> 2ndsneg(X1, X2) rcons(X1, mark(X2)) -> rcons(X1, X2) rcons(mark(X1), X2) -> rcons(X1, X2) rcons(active(X1), X2) -> rcons(X1, X2) rcons(X1, active(X2)) -> rcons(X1, X2) negrecip(active(X)) -> negrecip(X) negrecip(mark(X)) -> negrecip(X) 2ndspos(X1, mark(X2)) -> 2ndspos(X1, X2) 2ndspos(mark(X1), X2) -> 2ndspos(X1, X2) 2ndspos(active(X1), X2) -> 2ndspos(X1, X2) 2ndspos(X1, active(X2)) -> 2ndspos(X1, X2) plus(X1, mark(X2)) -> plus(X1, X2) plus(mark(X1), X2) -> plus(X1, X2) plus(active(X1), X2) -> plus(X1, X2) plus(X1, active(X2)) -> plus(X1, X2) times(X1, mark(X2)) -> times(X1, X2) times(mark(X1), X2) -> times(X1, X2) times(active(X1), X2) -> times(X1, X2) times(X1, active(X2)) -> times(X1, X2) square(active(X)) -> square(X) square(mark(X)) -> square(X) active(2ndspos(0, Z)) -> mark(rnil) active(2ndsneg(0, Z)) -> mark(rnil) active(times(0, Y)) -> mark(0) pi(active(X)) -> pi(X) pi(mark(X)) -> pi(X) ---------------------------------------- (85) Obligation: Q DP problem: The TRS P consists of the following rules: MARK(from(X)) -> ACTIVE(from(mark(X))) ACTIVE(from(X)) -> MARK(cons(X, from(s(X)))) MARK(from(X)) -> MARK(X) ACTIVE(2ndspos(s(N), cons(X, cons(Y, Z)))) -> MARK(rcons(posrecip(Y), 2ndsneg(N, Z))) MARK(cons(X1, X2)) -> MARK(X1) ACTIVE(2ndsneg(s(N), cons(X, cons(Y, Z)))) -> MARK(rcons(negrecip(Y), 2ndspos(N, Z))) MARK(s(X)) -> MARK(X) MARK(2ndspos(X1, X2)) -> ACTIVE(2ndspos(mark(X1), mark(X2))) MARK(2ndspos(X1, X2)) -> MARK(X2) ACTIVE(plus(0, Y)) -> MARK(Y) MARK(rcons(X1, X2)) -> MARK(X2) ACTIVE(plus(s(X), Y)) -> MARK(s(plus(X, Y))) MARK(posrecip(X)) -> MARK(X) MARK(2ndsneg(X1, X2)) -> ACTIVE(2ndsneg(mark(X1), mark(X2))) ACTIVE(times(s(X), Y)) -> MARK(plus(Y, times(X, Y))) MARK(2ndsneg(X1, X2)) -> MARK(X2) ACTIVE(square(X)) -> MARK(times(X, X)) MARK(negrecip(X)) -> MARK(X) MARK(plus(X1, X2)) -> ACTIVE(plus(mark(X1), mark(X2))) MARK(plus(X1, X2)) -> MARK(X1) MARK(plus(X1, X2)) -> MARK(X2) MARK(times(X1, X2)) -> ACTIVE(times(mark(X1), mark(X2))) MARK(times(X1, X2)) -> MARK(X1) MARK(times(X1, X2)) -> MARK(X2) MARK(square(X)) -> ACTIVE(square(mark(X))) MARK(square(X)) -> MARK(X) The TRS R consists of the following rules: active(from(X)) -> mark(cons(X, from(s(X)))) active(2ndspos(0, Z)) -> mark(rnil) active(2ndspos(s(N), cons(X, cons(Y, Z)))) -> mark(rcons(posrecip(Y), 2ndsneg(N, Z))) active(2ndsneg(0, Z)) -> mark(rnil) active(2ndsneg(s(N), cons(X, cons(Y, Z)))) -> mark(rcons(negrecip(Y), 2ndspos(N, Z))) active(pi(X)) -> mark(2ndspos(X, from(0))) active(plus(0, Y)) -> mark(Y) active(plus(s(X), Y)) -> mark(s(plus(X, Y))) active(times(0, Y)) -> mark(0) active(times(s(X), Y)) -> mark(plus(Y, times(X, Y))) active(square(X)) -> mark(times(X, X)) mark(from(X)) -> active(from(mark(X))) mark(cons(X1, X2)) -> active(cons(mark(X1), X2)) mark(s(X)) -> active(s(mark(X))) mark(2ndspos(X1, X2)) -> active(2ndspos(mark(X1), mark(X2))) mark(0) -> active(0) mark(rnil) -> active(rnil) mark(rcons(X1, X2)) -> active(rcons(mark(X1), mark(X2))) mark(posrecip(X)) -> active(posrecip(mark(X))) mark(2ndsneg(X1, X2)) -> active(2ndsneg(mark(X1), mark(X2))) mark(negrecip(X)) -> active(negrecip(mark(X))) mark(pi(X)) -> active(pi(mark(X))) mark(plus(X1, X2)) -> active(plus(mark(X1), mark(X2))) mark(times(X1, X2)) -> active(times(mark(X1), mark(X2))) mark(square(X)) -> active(square(mark(X))) from(mark(X)) -> from(X) from(active(X)) -> from(X) cons(mark(X1), X2) -> cons(X1, X2) cons(X1, mark(X2)) -> cons(X1, X2) cons(active(X1), X2) -> cons(X1, X2) cons(X1, active(X2)) -> cons(X1, X2) s(mark(X)) -> s(X) s(active(X)) -> s(X) 2ndspos(mark(X1), X2) -> 2ndspos(X1, X2) 2ndspos(X1, mark(X2)) -> 2ndspos(X1, X2) 2ndspos(active(X1), X2) -> 2ndspos(X1, X2) 2ndspos(X1, active(X2)) -> 2ndspos(X1, X2) rcons(mark(X1), X2) -> rcons(X1, X2) rcons(X1, mark(X2)) -> rcons(X1, X2) rcons(active(X1), X2) -> rcons(X1, X2) rcons(X1, active(X2)) -> rcons(X1, X2) posrecip(mark(X)) -> posrecip(X) posrecip(active(X)) -> posrecip(X) 2ndsneg(mark(X1), X2) -> 2ndsneg(X1, X2) 2ndsneg(X1, mark(X2)) -> 2ndsneg(X1, X2) 2ndsneg(active(X1), X2) -> 2ndsneg(X1, X2) 2ndsneg(X1, active(X2)) -> 2ndsneg(X1, X2) negrecip(mark(X)) -> negrecip(X) negrecip(active(X)) -> negrecip(X) pi(mark(X)) -> pi(X) pi(active(X)) -> pi(X) plus(mark(X1), X2) -> plus(X1, X2) plus(X1, mark(X2)) -> plus(X1, X2) plus(active(X1), X2) -> plus(X1, X2) plus(X1, active(X2)) -> plus(X1, X2) times(mark(X1), X2) -> times(X1, X2) times(X1, mark(X2)) -> times(X1, X2) times(active(X1), X2) -> times(X1, X2) times(X1, active(X2)) -> times(X1, X2) square(mark(X)) -> square(X) square(active(X)) -> square(X) Q is empty. We have to consider all minimal (P,Q,R)-chains. ---------------------------------------- (86) 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: Matrix interpretation [MATRO] with arctic natural numbers [ARCTIC]: <<< POL(MARK(x_1)) = [[1A]] + [[1A]] * x_1 >>> <<< POL(from(x_1)) = [[2A]] + [[0A]] * x_1 >>> <<< POL(ACTIVE(x_1)) = [[1A]] + [[1A]] * x_1 >>> <<< POL(mark(x_1)) = [[0A]] + [[0A]] * x_1 >>> <<< POL(cons(x_1, x_2)) = [[-I]] + [[0A]] * x_1 + [[0A]] * x_2 >>> <<< POL(s(x_1)) = [[-I]] + [[0A]] * x_1 >>> <<< POL(2ndspos(x_1, x_2)) = [[-I]] + [[-I]] * x_1 + [[0A]] * x_2 >>> <<< POL(rcons(x_1, x_2)) = [[-I]] + [[-I]] * x_1 + [[0A]] * x_2 >>> <<< POL(posrecip(x_1)) = [[3A]] + [[1A]] * x_1 >>> <<< POL(2ndsneg(x_1, x_2)) = [[0A]] + [[-I]] * x_1 + [[0A]] * x_2 >>> <<< POL(negrecip(x_1)) = [[-I]] + [[0A]] * x_1 >>> <<< POL(plus(x_1, x_2)) = [[1A]] + [[0A]] * x_1 + [[0A]] * x_2 >>> <<< POL(0) = [[0A]] >>> <<< POL(times(x_1, x_2)) = [[1A]] + [[0A]] * x_1 + [[0A]] * x_2 >>> <<< POL(square(x_1)) = [[1A]] + [[0A]] * x_1 >>> <<< POL(active(x_1)) = [[0A]] + [[0A]] * x_1 >>> <<< POL(pi(x_1)) = [[5A]] + [[3A]] * x_1 >>> <<< POL(rnil) = [[0A]] >>> The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented: mark(from(X)) -> active(from(mark(X))) active(from(X)) -> mark(cons(X, from(s(X)))) mark(cons(X1, X2)) -> active(cons(mark(X1), X2)) active(2ndspos(s(N), cons(X, cons(Y, Z)))) -> mark(rcons(posrecip(Y), 2ndsneg(N, Z))) mark(s(X)) -> active(s(mark(X))) active(2ndsneg(s(N), cons(X, cons(Y, Z)))) -> mark(rcons(negrecip(Y), 2ndspos(N, Z))) mark(2ndspos(X1, X2)) -> active(2ndspos(mark(X1), mark(X2))) active(pi(X)) -> mark(2ndspos(X, from(0))) mark(rcons(X1, X2)) -> active(rcons(mark(X1), mark(X2))) active(plus(0, Y)) -> mark(Y) mark(posrecip(X)) -> active(posrecip(mark(X))) active(plus(s(X), Y)) -> mark(s(plus(X, Y))) mark(2ndsneg(X1, X2)) -> active(2ndsneg(mark(X1), mark(X2))) active(times(s(X), Y)) -> mark(plus(Y, times(X, Y))) mark(negrecip(X)) -> active(negrecip(mark(X))) active(square(X)) -> mark(times(X, X)) mark(pi(X)) -> active(pi(mark(X))) mark(plus(X1, X2)) -> active(plus(mark(X1), mark(X2))) mark(times(X1, X2)) -> active(times(mark(X1), mark(X2))) mark(square(X)) -> active(square(mark(X))) mark(0) -> active(0) mark(rnil) -> active(rnil) from(active(X)) -> from(X) from(mark(X)) -> from(X) s(active(X)) -> s(X) s(mark(X)) -> s(X) cons(X1, mark(X2)) -> cons(X1, X2) cons(mark(X1), X2) -> cons(X1, X2) cons(active(X1), X2) -> cons(X1, X2) cons(X1, active(X2)) -> cons(X1, X2) posrecip(active(X)) -> posrecip(X) posrecip(mark(X)) -> posrecip(X) 2ndsneg(X1, mark(X2)) -> 2ndsneg(X1, X2) 2ndsneg(mark(X1), X2) -> 2ndsneg(X1, X2) 2ndsneg(active(X1), X2) -> 2ndsneg(X1, X2) 2ndsneg(X1, active(X2)) -> 2ndsneg(X1, X2) rcons(X1, mark(X2)) -> rcons(X1, X2) rcons(mark(X1), X2) -> rcons(X1, X2) rcons(active(X1), X2) -> rcons(X1, X2) rcons(X1, active(X2)) -> rcons(X1, X2) negrecip(active(X)) -> negrecip(X) negrecip(mark(X)) -> negrecip(X) 2ndspos(X1, mark(X2)) -> 2ndspos(X1, X2) 2ndspos(mark(X1), X2) -> 2ndspos(X1, X2) 2ndspos(active(X1), X2) -> 2ndspos(X1, X2) 2ndspos(X1, active(X2)) -> 2ndspos(X1, X2) plus(X1, mark(X2)) -> plus(X1, X2) plus(mark(X1), X2) -> plus(X1, X2) plus(active(X1), X2) -> plus(X1, X2) plus(X1, active(X2)) -> plus(X1, X2) times(X1, mark(X2)) -> times(X1, X2) times(mark(X1), X2) -> times(X1, X2) times(active(X1), X2) -> times(X1, X2) times(X1, active(X2)) -> times(X1, X2) square(active(X)) -> square(X) square(mark(X)) -> square(X) active(2ndspos(0, Z)) -> mark(rnil) active(2ndsneg(0, Z)) -> mark(rnil) active(times(0, Y)) -> mark(0) pi(active(X)) -> pi(X) pi(mark(X)) -> pi(X) ---------------------------------------- (87) Obligation: Q DP problem: The TRS P consists of the following rules: MARK(from(X)) -> ACTIVE(from(mark(X))) ACTIVE(from(X)) -> MARK(cons(X, from(s(X)))) MARK(from(X)) -> MARK(X) ACTIVE(2ndspos(s(N), cons(X, cons(Y, Z)))) -> MARK(rcons(posrecip(Y), 2ndsneg(N, Z))) MARK(cons(X1, X2)) -> MARK(X1) ACTIVE(2ndsneg(s(N), cons(X, cons(Y, Z)))) -> MARK(rcons(negrecip(Y), 2ndspos(N, Z))) MARK(s(X)) -> MARK(X) MARK(2ndspos(X1, X2)) -> ACTIVE(2ndspos(mark(X1), mark(X2))) MARK(2ndspos(X1, X2)) -> MARK(X2) ACTIVE(plus(0, Y)) -> MARK(Y) MARK(rcons(X1, X2)) -> MARK(X2) ACTIVE(plus(s(X), Y)) -> MARK(s(plus(X, Y))) MARK(2ndsneg(X1, X2)) -> ACTIVE(2ndsneg(mark(X1), mark(X2))) ACTIVE(times(s(X), Y)) -> MARK(plus(Y, times(X, Y))) MARK(2ndsneg(X1, X2)) -> MARK(X2) ACTIVE(square(X)) -> MARK(times(X, X)) MARK(negrecip(X)) -> MARK(X) MARK(plus(X1, X2)) -> ACTIVE(plus(mark(X1), mark(X2))) MARK(plus(X1, X2)) -> MARK(X1) MARK(plus(X1, X2)) -> MARK(X2) MARK(times(X1, X2)) -> ACTIVE(times(mark(X1), mark(X2))) MARK(times(X1, X2)) -> MARK(X1) MARK(times(X1, X2)) -> MARK(X2) MARK(square(X)) -> ACTIVE(square(mark(X))) MARK(square(X)) -> MARK(X) The TRS R consists of the following rules: active(from(X)) -> mark(cons(X, from(s(X)))) active(2ndspos(0, Z)) -> mark(rnil) active(2ndspos(s(N), cons(X, cons(Y, Z)))) -> mark(rcons(posrecip(Y), 2ndsneg(N, Z))) active(2ndsneg(0, Z)) -> mark(rnil) active(2ndsneg(s(N), cons(X, cons(Y, Z)))) -> mark(rcons(negrecip(Y), 2ndspos(N, Z))) active(pi(X)) -> mark(2ndspos(X, from(0))) active(plus(0, Y)) -> mark(Y) active(plus(s(X), Y)) -> mark(s(plus(X, Y))) active(times(0, Y)) -> mark(0) active(times(s(X), Y)) -> mark(plus(Y, times(X, Y))) active(square(X)) -> mark(times(X, X)) mark(from(X)) -> active(from(mark(X))) mark(cons(X1, X2)) -> active(cons(mark(X1), X2)) mark(s(X)) -> active(s(mark(X))) mark(2ndspos(X1, X2)) -> active(2ndspos(mark(X1), mark(X2))) mark(0) -> active(0) mark(rnil) -> active(rnil) mark(rcons(X1, X2)) -> active(rcons(mark(X1), mark(X2))) mark(posrecip(X)) -> active(posrecip(mark(X))) mark(2ndsneg(X1, X2)) -> active(2ndsneg(mark(X1), mark(X2))) mark(negrecip(X)) -> active(negrecip(mark(X))) mark(pi(X)) -> active(pi(mark(X))) mark(plus(X1, X2)) -> active(plus(mark(X1), mark(X2))) mark(times(X1, X2)) -> active(times(mark(X1), mark(X2))) mark(square(X)) -> active(square(mark(X))) from(mark(X)) -> from(X) from(active(X)) -> from(X) cons(mark(X1), X2) -> cons(X1, X2) cons(X1, mark(X2)) -> cons(X1, X2) cons(active(X1), X2) -> cons(X1, X2) cons(X1, active(X2)) -> cons(X1, X2) s(mark(X)) -> s(X) s(active(X)) -> s(X) 2ndspos(mark(X1), X2) -> 2ndspos(X1, X2) 2ndspos(X1, mark(X2)) -> 2ndspos(X1, X2) 2ndspos(active(X1), X2) -> 2ndspos(X1, X2) 2ndspos(X1, active(X2)) -> 2ndspos(X1, X2) rcons(mark(X1), X2) -> rcons(X1, X2) rcons(X1, mark(X2)) -> rcons(X1, X2) rcons(active(X1), X2) -> rcons(X1, X2) rcons(X1, active(X2)) -> rcons(X1, X2) posrecip(mark(X)) -> posrecip(X) posrecip(active(X)) -> posrecip(X) 2ndsneg(mark(X1), X2) -> 2ndsneg(X1, X2) 2ndsneg(X1, mark(X2)) -> 2ndsneg(X1, X2) 2ndsneg(active(X1), X2) -> 2ndsneg(X1, X2) 2ndsneg(X1, active(X2)) -> 2ndsneg(X1, X2) negrecip(mark(X)) -> negrecip(X) negrecip(active(X)) -> negrecip(X) pi(mark(X)) -> pi(X) pi(active(X)) -> pi(X) plus(mark(X1), X2) -> plus(X1, X2) plus(X1, mark(X2)) -> plus(X1, X2) plus(active(X1), X2) -> plus(X1, X2) plus(X1, active(X2)) -> plus(X1, X2) times(mark(X1), X2) -> times(X1, X2) times(X1, mark(X2)) -> times(X1, X2) times(active(X1), X2) -> times(X1, X2) times(X1, active(X2)) -> times(X1, X2) square(mark(X)) -> square(X) square(active(X)) -> square(X) Q is empty. We have to consider all minimal (P,Q,R)-chains. ---------------------------------------- (88) QDPOrderProof (EQUIVALENT) We use the reduction pair processor [LPAR04,JAR06]. The following pairs can be oriented strictly and are deleted. ACTIVE(square(X)) -> MARK(times(X, X)) MARK(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)) = [[0A]] + [[0A]] * x_1 >>> <<< POL(from(x_1)) = [[-I]] + [[0A]] * x_1 >>> <<< POL(ACTIVE(x_1)) = [[0A]] + [[0A]] * x_1 >>> <<< POL(mark(x_1)) = [[-I]] + [[0A]] * x_1 >>> <<< POL(cons(x_1, x_2)) = [[-I]] + [[0A]] * x_1 + [[0A]] * x_2 >>> <<< POL(s(x_1)) = [[-I]] + [[0A]] * x_1 >>> <<< POL(2ndspos(x_1, x_2)) = [[-I]] + [[2A]] * x_1 + [[5A]] * x_2 >>> <<< POL(rcons(x_1, x_2)) = [[-I]] + [[-I]] * x_1 + [[0A]] * x_2 >>> <<< POL(posrecip(x_1)) = [[1A]] + [[3A]] * x_1 >>> <<< POL(2ndsneg(x_1, x_2)) = [[-I]] + [[2A]] * x_1 + [[5A]] * x_2 >>> <<< POL(negrecip(x_1)) = [[-I]] + [[0A]] * x_1 >>> <<< POL(plus(x_1, x_2)) = [[0A]] + [[1A]] * x_1 + [[0A]] * x_2 >>> <<< POL(0) = [[0A]] >>> <<< POL(times(x_1, x_2)) = [[0A]] + [[0A]] * x_1 + [[4A]] * x_2 >>> <<< POL(square(x_1)) = [[4A]] + [[5A]] * x_1 >>> <<< POL(active(x_1)) = [[-I]] + [[0A]] * x_1 >>> <<< POL(pi(x_1)) = [[5A]] + [[3A]] * x_1 >>> <<< POL(rnil) = [[2A]] >>> The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented: mark(from(X)) -> active(from(mark(X))) active(from(X)) -> mark(cons(X, from(s(X)))) mark(cons(X1, X2)) -> active(cons(mark(X1), X2)) active(2ndspos(s(N), cons(X, cons(Y, Z)))) -> mark(rcons(posrecip(Y), 2ndsneg(N, Z))) mark(s(X)) -> active(s(mark(X))) active(2ndsneg(s(N), cons(X, cons(Y, Z)))) -> mark(rcons(negrecip(Y), 2ndspos(N, Z))) mark(2ndspos(X1, X2)) -> active(2ndspos(mark(X1), mark(X2))) active(pi(X)) -> mark(2ndspos(X, from(0))) mark(rcons(X1, X2)) -> active(rcons(mark(X1), mark(X2))) active(plus(0, Y)) -> mark(Y) mark(posrecip(X)) -> active(posrecip(mark(X))) active(plus(s(X), Y)) -> mark(s(plus(X, Y))) mark(2ndsneg(X1, X2)) -> active(2ndsneg(mark(X1), mark(X2))) active(times(s(X), Y)) -> mark(plus(Y, times(X, Y))) mark(negrecip(X)) -> active(negrecip(mark(X))) active(square(X)) -> mark(times(X, X)) mark(pi(X)) -> active(pi(mark(X))) mark(plus(X1, X2)) -> active(plus(mark(X1), mark(X2))) mark(times(X1, X2)) -> active(times(mark(X1), mark(X2))) mark(square(X)) -> active(square(mark(X))) mark(0) -> active(0) mark(rnil) -> active(rnil) from(active(X)) -> from(X) from(mark(X)) -> from(X) s(active(X)) -> s(X) s(mark(X)) -> s(X) cons(X1, mark(X2)) -> cons(X1, X2) cons(mark(X1), X2) -> cons(X1, X2) cons(active(X1), X2) -> cons(X1, X2) cons(X1, active(X2)) -> cons(X1, X2) posrecip(active(X)) -> posrecip(X) posrecip(mark(X)) -> posrecip(X) 2ndsneg(X1, mark(X2)) -> 2ndsneg(X1, X2) 2ndsneg(mark(X1), X2) -> 2ndsneg(X1, X2) 2ndsneg(active(X1), X2) -> 2ndsneg(X1, X2) 2ndsneg(X1, active(X2)) -> 2ndsneg(X1, X2) rcons(X1, mark(X2)) -> rcons(X1, X2) rcons(mark(X1), X2) -> rcons(X1, X2) rcons(active(X1), X2) -> rcons(X1, X2) rcons(X1, active(X2)) -> rcons(X1, X2) negrecip(active(X)) -> negrecip(X) negrecip(mark(X)) -> negrecip(X) 2ndspos(X1, mark(X2)) -> 2ndspos(X1, X2) 2ndspos(mark(X1), X2) -> 2ndspos(X1, X2) 2ndspos(active(X1), X2) -> 2ndspos(X1, X2) 2ndspos(X1, active(X2)) -> 2ndspos(X1, X2) plus(X1, mark(X2)) -> plus(X1, X2) plus(mark(X1), X2) -> plus(X1, X2) plus(active(X1), X2) -> plus(X1, X2) plus(X1, active(X2)) -> plus(X1, X2) times(X1, mark(X2)) -> times(X1, X2) times(mark(X1), X2) -> times(X1, X2) times(active(X1), X2) -> times(X1, X2) times(X1, active(X2)) -> times(X1, X2) square(active(X)) -> square(X) square(mark(X)) -> square(X) active(2ndspos(0, Z)) -> mark(rnil) active(2ndsneg(0, Z)) -> mark(rnil) active(times(0, Y)) -> mark(0) pi(active(X)) -> pi(X) pi(mark(X)) -> pi(X) ---------------------------------------- (89) Obligation: Q DP problem: The TRS P consists of the following rules: MARK(from(X)) -> ACTIVE(from(mark(X))) ACTIVE(from(X)) -> MARK(cons(X, from(s(X)))) MARK(from(X)) -> MARK(X) ACTIVE(2ndspos(s(N), cons(X, cons(Y, Z)))) -> MARK(rcons(posrecip(Y), 2ndsneg(N, Z))) MARK(cons(X1, X2)) -> MARK(X1) ACTIVE(2ndsneg(s(N), cons(X, cons(Y, Z)))) -> MARK(rcons(negrecip(Y), 2ndspos(N, Z))) MARK(s(X)) -> MARK(X) MARK(2ndspos(X1, X2)) -> ACTIVE(2ndspos(mark(X1), mark(X2))) MARK(2ndspos(X1, X2)) -> MARK(X2) ACTIVE(plus(0, Y)) -> MARK(Y) MARK(rcons(X1, X2)) -> MARK(X2) ACTIVE(plus(s(X), Y)) -> MARK(s(plus(X, Y))) MARK(2ndsneg(X1, X2)) -> ACTIVE(2ndsneg(mark(X1), mark(X2))) ACTIVE(times(s(X), Y)) -> MARK(plus(Y, times(X, Y))) MARK(2ndsneg(X1, X2)) -> MARK(X2) MARK(negrecip(X)) -> MARK(X) MARK(plus(X1, X2)) -> ACTIVE(plus(mark(X1), mark(X2))) MARK(plus(X1, X2)) -> MARK(X1) MARK(plus(X1, X2)) -> MARK(X2) MARK(times(X1, X2)) -> ACTIVE(times(mark(X1), mark(X2))) MARK(times(X1, X2)) -> MARK(X1) MARK(times(X1, X2)) -> MARK(X2) MARK(square(X)) -> ACTIVE(square(mark(X))) The TRS R consists of the following rules: active(from(X)) -> mark(cons(X, from(s(X)))) active(2ndspos(0, Z)) -> mark(rnil) active(2ndspos(s(N), cons(X, cons(Y, Z)))) -> mark(rcons(posrecip(Y), 2ndsneg(N, Z))) active(2ndsneg(0, Z)) -> mark(rnil) active(2ndsneg(s(N), cons(X, cons(Y, Z)))) -> mark(rcons(negrecip(Y), 2ndspos(N, Z))) active(pi(X)) -> mark(2ndspos(X, from(0))) active(plus(0, Y)) -> mark(Y) active(plus(s(X), Y)) -> mark(s(plus(X, Y))) active(times(0, Y)) -> mark(0) active(times(s(X), Y)) -> mark(plus(Y, times(X, Y))) active(square(X)) -> mark(times(X, X)) mark(from(X)) -> active(from(mark(X))) mark(cons(X1, X2)) -> active(cons(mark(X1), X2)) mark(s(X)) -> active(s(mark(X))) mark(2ndspos(X1, X2)) -> active(2ndspos(mark(X1), mark(X2))) mark(0) -> active(0) mark(rnil) -> active(rnil) mark(rcons(X1, X2)) -> active(rcons(mark(X1), mark(X2))) mark(posrecip(X)) -> active(posrecip(mark(X))) mark(2ndsneg(X1, X2)) -> active(2ndsneg(mark(X1), mark(X2))) mark(negrecip(X)) -> active(negrecip(mark(X))) mark(pi(X)) -> active(pi(mark(X))) mark(plus(X1, X2)) -> active(plus(mark(X1), mark(X2))) mark(times(X1, X2)) -> active(times(mark(X1), mark(X2))) mark(square(X)) -> active(square(mark(X))) from(mark(X)) -> from(X) from(active(X)) -> from(X) cons(mark(X1), X2) -> cons(X1, X2) cons(X1, mark(X2)) -> cons(X1, X2) cons(active(X1), X2) -> cons(X1, X2) cons(X1, active(X2)) -> cons(X1, X2) s(mark(X)) -> s(X) s(active(X)) -> s(X) 2ndspos(mark(X1), X2) -> 2ndspos(X1, X2) 2ndspos(X1, mark(X2)) -> 2ndspos(X1, X2) 2ndspos(active(X1), X2) -> 2ndspos(X1, X2) 2ndspos(X1, active(X2)) -> 2ndspos(X1, X2) rcons(mark(X1), X2) -> rcons(X1, X2) rcons(X1, mark(X2)) -> rcons(X1, X2) rcons(active(X1), X2) -> rcons(X1, X2) rcons(X1, active(X2)) -> rcons(X1, X2) posrecip(mark(X)) -> posrecip(X) posrecip(active(X)) -> posrecip(X) 2ndsneg(mark(X1), X2) -> 2ndsneg(X1, X2) 2ndsneg(X1, mark(X2)) -> 2ndsneg(X1, X2) 2ndsneg(active(X1), X2) -> 2ndsneg(X1, X2) 2ndsneg(X1, active(X2)) -> 2ndsneg(X1, X2) negrecip(mark(X)) -> negrecip(X) negrecip(active(X)) -> negrecip(X) pi(mark(X)) -> pi(X) pi(active(X)) -> pi(X) plus(mark(X1), X2) -> plus(X1, X2) plus(X1, mark(X2)) -> plus(X1, X2) plus(active(X1), X2) -> plus(X1, X2) plus(X1, active(X2)) -> plus(X1, X2) times(mark(X1), X2) -> times(X1, X2) times(X1, mark(X2)) -> times(X1, X2) times(active(X1), X2) -> times(X1, X2) times(X1, active(X2)) -> times(X1, X2) square(mark(X)) -> square(X) square(active(X)) -> square(X) Q is empty. We have to consider all minimal (P,Q,R)-chains. ---------------------------------------- (90) QDPOrderProof (EQUIVALENT) We use the reduction pair processor [LPAR04,JAR06]. The following pairs can be oriented strictly and are deleted. MARK(square(X)) -> ACTIVE(square(mark(X))) The remaining pairs can at least be oriented weakly. Used ordering: Polynomial Order [NEGPOLO,POLO] with Interpretation: POL( 2ndsneg_2(x_1, x_2) ) = 2 POL( ACTIVE_1(x_1) ) = max{0, x_1 - 1} POL( 2ndspos_2(x_1, x_2) ) = 2 POL( from_1(x_1) ) = 2 POL( plus_2(x_1, x_2) ) = 2 POL( square_1(x_1) ) = 1 POL( times_2(x_1, x_2) ) = 2 POL( mark_1(x_1) ) = x_1 + 2 POL( active_1(x_1) ) = x_1 + 2 POL( cons_2(x_1, x_2) ) = x_2 + 1 POL( s_1(x_1) ) = x_1 POL( rcons_2(x_1, x_2) ) = 2x_2 + 1 POL( posrecip_1(x_1) ) = x_1 + 1 POL( negrecip_1(x_1) ) = x_1 POL( pi_1(x_1) ) = max{0, x_1 - 2} POL( 0 ) = 1 POL( rnil ) = 0 POL( MARK_1(x_1) ) = 1 The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented: from(active(X)) -> from(X) from(mark(X)) -> from(X) 2ndsneg(X1, mark(X2)) -> 2ndsneg(X1, X2) 2ndsneg(mark(X1), X2) -> 2ndsneg(X1, X2) 2ndsneg(active(X1), X2) -> 2ndsneg(X1, X2) 2ndsneg(X1, active(X2)) -> 2ndsneg(X1, X2) 2ndspos(X1, mark(X2)) -> 2ndspos(X1, X2) 2ndspos(mark(X1), X2) -> 2ndspos(X1, X2) 2ndspos(active(X1), X2) -> 2ndspos(X1, X2) 2ndspos(X1, active(X2)) -> 2ndspos(X1, X2) plus(X1, mark(X2)) -> plus(X1, X2) plus(mark(X1), X2) -> plus(X1, X2) plus(active(X1), X2) -> plus(X1, X2) plus(X1, active(X2)) -> plus(X1, X2) times(X1, mark(X2)) -> times(X1, X2) times(mark(X1), X2) -> times(X1, X2) times(active(X1), X2) -> times(X1, X2) times(X1, active(X2)) -> times(X1, X2) square(active(X)) -> square(X) square(mark(X)) -> square(X) ---------------------------------------- (91) Obligation: Q DP problem: The TRS P consists of the following rules: MARK(from(X)) -> ACTIVE(from(mark(X))) ACTIVE(from(X)) -> MARK(cons(X, from(s(X)))) MARK(from(X)) -> MARK(X) ACTIVE(2ndspos(s(N), cons(X, cons(Y, Z)))) -> MARK(rcons(posrecip(Y), 2ndsneg(N, Z))) MARK(cons(X1, X2)) -> MARK(X1) ACTIVE(2ndsneg(s(N), cons(X, cons(Y, Z)))) -> MARK(rcons(negrecip(Y), 2ndspos(N, Z))) MARK(s(X)) -> MARK(X) MARK(2ndspos(X1, X2)) -> ACTIVE(2ndspos(mark(X1), mark(X2))) MARK(2ndspos(X1, X2)) -> MARK(X2) ACTIVE(plus(0, Y)) -> MARK(Y) MARK(rcons(X1, X2)) -> MARK(X2) ACTIVE(plus(s(X), Y)) -> MARK(s(plus(X, Y))) MARK(2ndsneg(X1, X2)) -> ACTIVE(2ndsneg(mark(X1), mark(X2))) ACTIVE(times(s(X), Y)) -> MARK(plus(Y, times(X, Y))) MARK(2ndsneg(X1, X2)) -> MARK(X2) MARK(negrecip(X)) -> MARK(X) MARK(plus(X1, X2)) -> ACTIVE(plus(mark(X1), mark(X2))) MARK(plus(X1, X2)) -> MARK(X1) MARK(plus(X1, X2)) -> MARK(X2) MARK(times(X1, X2)) -> ACTIVE(times(mark(X1), mark(X2))) MARK(times(X1, X2)) -> MARK(X1) MARK(times(X1, X2)) -> MARK(X2) The TRS R consists of the following rules: active(from(X)) -> mark(cons(X, from(s(X)))) active(2ndspos(0, Z)) -> mark(rnil) active(2ndspos(s(N), cons(X, cons(Y, Z)))) -> mark(rcons(posrecip(Y), 2ndsneg(N, Z))) active(2ndsneg(0, Z)) -> mark(rnil) active(2ndsneg(s(N), cons(X, cons(Y, Z)))) -> mark(rcons(negrecip(Y), 2ndspos(N, Z))) active(pi(X)) -> mark(2ndspos(X, from(0))) active(plus(0, Y)) -> mark(Y) active(plus(s(X), Y)) -> mark(s(plus(X, Y))) active(times(0, Y)) -> mark(0) active(times(s(X), Y)) -> mark(plus(Y, times(X, Y))) active(square(X)) -> mark(times(X, X)) mark(from(X)) -> active(from(mark(X))) mark(cons(X1, X2)) -> active(cons(mark(X1), X2)) mark(s(X)) -> active(s(mark(X))) mark(2ndspos(X1, X2)) -> active(2ndspos(mark(X1), mark(X2))) mark(0) -> active(0) mark(rnil) -> active(rnil) mark(rcons(X1, X2)) -> active(rcons(mark(X1), mark(X2))) mark(posrecip(X)) -> active(posrecip(mark(X))) mark(2ndsneg(X1, X2)) -> active(2ndsneg(mark(X1), mark(X2))) mark(negrecip(X)) -> active(negrecip(mark(X))) mark(pi(X)) -> active(pi(mark(X))) mark(plus(X1, X2)) -> active(plus(mark(X1), mark(X2))) mark(times(X1, X2)) -> active(times(mark(X1), mark(X2))) mark(square(X)) -> active(square(mark(X))) from(mark(X)) -> from(X) from(active(X)) -> from(X) cons(mark(X1), X2) -> cons(X1, X2) cons(X1, mark(X2)) -> cons(X1, X2) cons(active(X1), X2) -> cons(X1, X2) cons(X1, active(X2)) -> cons(X1, X2) s(mark(X)) -> s(X) s(active(X)) -> s(X) 2ndspos(mark(X1), X2) -> 2ndspos(X1, X2) 2ndspos(X1, mark(X2)) -> 2ndspos(X1, X2) 2ndspos(active(X1), X2) -> 2ndspos(X1, X2) 2ndspos(X1, active(X2)) -> 2ndspos(X1, X2) rcons(mark(X1), X2) -> rcons(X1, X2) rcons(X1, mark(X2)) -> rcons(X1, X2) rcons(active(X1), X2) -> rcons(X1, X2) rcons(X1, active(X2)) -> rcons(X1, X2) posrecip(mark(X)) -> posrecip(X) posrecip(active(X)) -> posrecip(X) 2ndsneg(mark(X1), X2) -> 2ndsneg(X1, X2) 2ndsneg(X1, mark(X2)) -> 2ndsneg(X1, X2) 2ndsneg(active(X1), X2) -> 2ndsneg(X1, X2) 2ndsneg(X1, active(X2)) -> 2ndsneg(X1, X2) negrecip(mark(X)) -> negrecip(X) negrecip(active(X)) -> negrecip(X) pi(mark(X)) -> pi(X) pi(active(X)) -> pi(X) plus(mark(X1), X2) -> plus(X1, X2) plus(X1, mark(X2)) -> plus(X1, X2) plus(active(X1), X2) -> plus(X1, X2) plus(X1, active(X2)) -> plus(X1, X2) times(mark(X1), X2) -> times(X1, X2) times(X1, mark(X2)) -> times(X1, X2) times(active(X1), X2) -> times(X1, X2) times(X1, active(X2)) -> times(X1, X2) square(mark(X)) -> square(X) square(active(X)) -> square(X) Q is empty. We have to consider all minimal (P,Q,R)-chains. ---------------------------------------- (92) 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) The remaining pairs can at least be oriented weakly. Used ordering: Matrix interpretation [MATRO] with arctic natural numbers [ARCTIC]: <<< POL(MARK(x_1)) = [[2A]] + [[2A]] * x_1 >>> <<< POL(from(x_1)) = [[4A]] + [[1A]] * x_1 >>> <<< POL(ACTIVE(x_1)) = [[2A]] + [[2A]] * x_1 >>> <<< POL(mark(x_1)) = [[0A]] + [[0A]] * x_1 >>> <<< POL(cons(x_1, x_2)) = [[0A]] + [[0A]] * x_1 + [[0A]] * x_2 >>> <<< POL(s(x_1)) = [[-I]] + [[0A]] * x_1 >>> <<< POL(2ndspos(x_1, x_2)) = [[-I]] + [[0A]] * x_1 + [[0A]] * x_2 >>> <<< POL(rcons(x_1, x_2)) = [[-I]] + [[-I]] * x_1 + [[0A]] * x_2 >>> <<< POL(posrecip(x_1)) = [[-I]] + [[0A]] * x_1 >>> <<< POL(2ndsneg(x_1, x_2)) = [[-I]] + [[0A]] * x_1 + [[0A]] * x_2 >>> <<< POL(negrecip(x_1)) = [[-I]] + [[0A]] * x_1 >>> <<< POL(plus(x_1, x_2)) = [[-I]] + [[0A]] * x_1 + [[0A]] * x_2 >>> <<< POL(0) = [[0A]] >>> <<< POL(times(x_1, x_2)) = [[3A]] + [[0A]] * x_1 + [[0A]] * x_2 >>> <<< POL(active(x_1)) = [[0A]] + [[0A]] * x_1 >>> <<< POL(pi(x_1)) = [[4A]] + [[1A]] * x_1 >>> <<< POL(square(x_1)) = [[3A]] + [[3A]] * x_1 >>> <<< POL(rnil) = [[0A]] >>> The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented: mark(from(X)) -> active(from(mark(X))) active(from(X)) -> mark(cons(X, from(s(X)))) mark(cons(X1, X2)) -> active(cons(mark(X1), X2)) active(2ndspos(s(N), cons(X, cons(Y, Z)))) -> mark(rcons(posrecip(Y), 2ndsneg(N, Z))) mark(s(X)) -> active(s(mark(X))) active(2ndsneg(s(N), cons(X, cons(Y, Z)))) -> mark(rcons(negrecip(Y), 2ndspos(N, Z))) mark(2ndspos(X1, X2)) -> active(2ndspos(mark(X1), mark(X2))) active(pi(X)) -> mark(2ndspos(X, from(0))) mark(rcons(X1, X2)) -> active(rcons(mark(X1), mark(X2))) active(plus(0, Y)) -> mark(Y) mark(posrecip(X)) -> active(posrecip(mark(X))) active(plus(s(X), Y)) -> mark(s(plus(X, Y))) mark(2ndsneg(X1, X2)) -> active(2ndsneg(mark(X1), mark(X2))) active(times(s(X), Y)) -> mark(plus(Y, times(X, Y))) mark(negrecip(X)) -> active(negrecip(mark(X))) active(square(X)) -> mark(times(X, X)) mark(pi(X)) -> active(pi(mark(X))) mark(plus(X1, X2)) -> active(plus(mark(X1), mark(X2))) mark(times(X1, X2)) -> active(times(mark(X1), mark(X2))) mark(square(X)) -> active(square(mark(X))) mark(0) -> active(0) mark(rnil) -> active(rnil) from(active(X)) -> from(X) from(mark(X)) -> from(X) s(active(X)) -> s(X) s(mark(X)) -> s(X) cons(X1, mark(X2)) -> cons(X1, X2) cons(mark(X1), X2) -> cons(X1, X2) cons(active(X1), X2) -> cons(X1, X2) cons(X1, active(X2)) -> cons(X1, X2) posrecip(active(X)) -> posrecip(X) posrecip(mark(X)) -> posrecip(X) 2ndsneg(X1, mark(X2)) -> 2ndsneg(X1, X2) 2ndsneg(mark(X1), X2) -> 2ndsneg(X1, X2) 2ndsneg(active(X1), X2) -> 2ndsneg(X1, X2) 2ndsneg(X1, active(X2)) -> 2ndsneg(X1, X2) rcons(X1, mark(X2)) -> rcons(X1, X2) rcons(mark(X1), X2) -> rcons(X1, X2) rcons(active(X1), X2) -> rcons(X1, X2) rcons(X1, active(X2)) -> rcons(X1, X2) negrecip(active(X)) -> negrecip(X) negrecip(mark(X)) -> negrecip(X) 2ndspos(X1, mark(X2)) -> 2ndspos(X1, X2) 2ndspos(mark(X1), X2) -> 2ndspos(X1, X2) 2ndspos(active(X1), X2) -> 2ndspos(X1, X2) 2ndspos(X1, active(X2)) -> 2ndspos(X1, X2) plus(X1, mark(X2)) -> plus(X1, X2) plus(mark(X1), X2) -> plus(X1, X2) plus(active(X1), X2) -> plus(X1, X2) plus(X1, active(X2)) -> plus(X1, X2) times(X1, mark(X2)) -> times(X1, X2) times(mark(X1), X2) -> times(X1, X2) times(active(X1), X2) -> times(X1, X2) times(X1, active(X2)) -> times(X1, X2) active(2ndspos(0, Z)) -> mark(rnil) active(2ndsneg(0, Z)) -> mark(rnil) active(times(0, Y)) -> mark(0) pi(active(X)) -> pi(X) pi(mark(X)) -> pi(X) square(active(X)) -> square(X) square(mark(X)) -> square(X) ---------------------------------------- (93) Obligation: Q DP problem: The TRS P consists of the following rules: MARK(from(X)) -> ACTIVE(from(mark(X))) ACTIVE(from(X)) -> MARK(cons(X, from(s(X)))) ACTIVE(2ndspos(s(N), cons(X, cons(Y, Z)))) -> MARK(rcons(posrecip(Y), 2ndsneg(N, Z))) MARK(cons(X1, X2)) -> MARK(X1) ACTIVE(2ndsneg(s(N), cons(X, cons(Y, Z)))) -> MARK(rcons(negrecip(Y), 2ndspos(N, Z))) MARK(s(X)) -> MARK(X) MARK(2ndspos(X1, X2)) -> ACTIVE(2ndspos(mark(X1), mark(X2))) MARK(2ndspos(X1, X2)) -> MARK(X2) ACTIVE(plus(0, Y)) -> MARK(Y) MARK(rcons(X1, X2)) -> MARK(X2) ACTIVE(plus(s(X), Y)) -> MARK(s(plus(X, Y))) MARK(2ndsneg(X1, X2)) -> ACTIVE(2ndsneg(mark(X1), mark(X2))) ACTIVE(times(s(X), Y)) -> MARK(plus(Y, times(X, Y))) MARK(2ndsneg(X1, X2)) -> MARK(X2) MARK(negrecip(X)) -> MARK(X) MARK(plus(X1, X2)) -> ACTIVE(plus(mark(X1), mark(X2))) MARK(plus(X1, X2)) -> MARK(X1) MARK(plus(X1, X2)) -> MARK(X2) MARK(times(X1, X2)) -> ACTIVE(times(mark(X1), mark(X2))) MARK(times(X1, X2)) -> MARK(X1) MARK(times(X1, X2)) -> MARK(X2) The TRS R consists of the following rules: active(from(X)) -> mark(cons(X, from(s(X)))) active(2ndspos(0, Z)) -> mark(rnil) active(2ndspos(s(N), cons(X, cons(Y, Z)))) -> mark(rcons(posrecip(Y), 2ndsneg(N, Z))) active(2ndsneg(0, Z)) -> mark(rnil) active(2ndsneg(s(N), cons(X, cons(Y, Z)))) -> mark(rcons(negrecip(Y), 2ndspos(N, Z))) active(pi(X)) -> mark(2ndspos(X, from(0))) active(plus(0, Y)) -> mark(Y) active(plus(s(X), Y)) -> mark(s(plus(X, Y))) active(times(0, Y)) -> mark(0) active(times(s(X), Y)) -> mark(plus(Y, times(X, Y))) active(square(X)) -> mark(times(X, X)) mark(from(X)) -> active(from(mark(X))) mark(cons(X1, X2)) -> active(cons(mark(X1), X2)) mark(s(X)) -> active(s(mark(X))) mark(2ndspos(X1, X2)) -> active(2ndspos(mark(X1), mark(X2))) mark(0) -> active(0) mark(rnil) -> active(rnil) mark(rcons(X1, X2)) -> active(rcons(mark(X1), mark(X2))) mark(posrecip(X)) -> active(posrecip(mark(X))) mark(2ndsneg(X1, X2)) -> active(2ndsneg(mark(X1), mark(X2))) mark(negrecip(X)) -> active(negrecip(mark(X))) mark(pi(X)) -> active(pi(mark(X))) mark(plus(X1, X2)) -> active(plus(mark(X1), mark(X2))) mark(times(X1, X2)) -> active(times(mark(X1), mark(X2))) mark(square(X)) -> active(square(mark(X))) from(mark(X)) -> from(X) from(active(X)) -> from(X) cons(mark(X1), X2) -> cons(X1, X2) cons(X1, mark(X2)) -> cons(X1, X2) cons(active(X1), X2) -> cons(X1, X2) cons(X1, active(X2)) -> cons(X1, X2) s(mark(X)) -> s(X) s(active(X)) -> s(X) 2ndspos(mark(X1), X2) -> 2ndspos(X1, X2) 2ndspos(X1, mark(X2)) -> 2ndspos(X1, X2) 2ndspos(active(X1), X2) -> 2ndspos(X1, X2) 2ndspos(X1, active(X2)) -> 2ndspos(X1, X2) rcons(mark(X1), X2) -> rcons(X1, X2) rcons(X1, mark(X2)) -> rcons(X1, X2) rcons(active(X1), X2) -> rcons(X1, X2) rcons(X1, active(X2)) -> rcons(X1, X2) posrecip(mark(X)) -> posrecip(X) posrecip(active(X)) -> posrecip(X) 2ndsneg(mark(X1), X2) -> 2ndsneg(X1, X2) 2ndsneg(X1, mark(X2)) -> 2ndsneg(X1, X2) 2ndsneg(active(X1), X2) -> 2ndsneg(X1, X2) 2ndsneg(X1, active(X2)) -> 2ndsneg(X1, X2) negrecip(mark(X)) -> negrecip(X) negrecip(active(X)) -> negrecip(X) pi(mark(X)) -> pi(X) pi(active(X)) -> pi(X) plus(mark(X1), X2) -> plus(X1, X2) plus(X1, mark(X2)) -> plus(X1, X2) plus(active(X1), X2) -> plus(X1, X2) plus(X1, active(X2)) -> plus(X1, X2) times(mark(X1), X2) -> times(X1, X2) times(X1, mark(X2)) -> times(X1, X2) times(active(X1), X2) -> times(X1, X2) times(X1, active(X2)) -> times(X1, X2) square(mark(X)) -> square(X) square(active(X)) -> square(X) Q is empty. We have to consider all minimal (P,Q,R)-chains. ---------------------------------------- (94) QDPOrderProof (EQUIVALENT) We use the reduction pair processor [LPAR04,JAR06]. The following pairs can be oriented strictly and are deleted. 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(MARK(x_1)) = [[-I]] + [[2A]] * x_1 >>> <<< POL(from(x_1)) = [[2A]] + [[3A]] * x_1 >>> <<< POL(ACTIVE(x_1)) = [[3A]] + [[2A]] * x_1 >>> <<< POL(mark(x_1)) = [[-I]] + [[0A]] * x_1 >>> <<< POL(cons(x_1, x_2)) = [[-I]] + [[1A]] * x_1 + [[0A]] * x_2 >>> <<< POL(s(x_1)) = [[-I]] + [[0A]] * x_1 >>> <<< POL(2ndspos(x_1, x_2)) = [[1A]] + [[-I]] * x_1 + [[0A]] * x_2 >>> <<< POL(rcons(x_1, x_2)) = [[-I]] + [[-I]] * x_1 + [[0A]] * x_2 >>> <<< POL(posrecip(x_1)) = [[5A]] + [[-I]] * x_1 >>> <<< POL(2ndsneg(x_1, x_2)) = [[1A]] + [[-I]] * x_1 + [[0A]] * x_2 >>> <<< POL(negrecip(x_1)) = [[-I]] + [[0A]] * x_1 >>> <<< POL(plus(x_1, x_2)) = [[1A]] + [[0A]] * x_1 + [[0A]] * x_2 >>> <<< POL(0) = [[2A]] >>> <<< POL(times(x_1, x_2)) = [[1A]] + [[0A]] * x_1 + [[0A]] * x_2 >>> <<< POL(active(x_1)) = [[-I]] + [[0A]] * x_1 >>> <<< POL(pi(x_1)) = [[5A]] + [[-I]] * x_1 >>> <<< POL(square(x_1)) = [[5A]] + [[5A]] * x_1 >>> <<< POL(rnil) = [[1A]] >>> The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented: mark(from(X)) -> active(from(mark(X))) active(from(X)) -> mark(cons(X, from(s(X)))) mark(cons(X1, X2)) -> active(cons(mark(X1), X2)) active(2ndspos(s(N), cons(X, cons(Y, Z)))) -> mark(rcons(posrecip(Y), 2ndsneg(N, Z))) mark(s(X)) -> active(s(mark(X))) active(2ndsneg(s(N), cons(X, cons(Y, Z)))) -> mark(rcons(negrecip(Y), 2ndspos(N, Z))) mark(2ndspos(X1, X2)) -> active(2ndspos(mark(X1), mark(X2))) active(pi(X)) -> mark(2ndspos(X, from(0))) mark(rcons(X1, X2)) -> active(rcons(mark(X1), mark(X2))) active(plus(0, Y)) -> mark(Y) mark(posrecip(X)) -> active(posrecip(mark(X))) active(plus(s(X), Y)) -> mark(s(plus(X, Y))) mark(2ndsneg(X1, X2)) -> active(2ndsneg(mark(X1), mark(X2))) active(times(s(X), Y)) -> mark(plus(Y, times(X, Y))) mark(negrecip(X)) -> active(negrecip(mark(X))) active(square(X)) -> mark(times(X, X)) mark(pi(X)) -> active(pi(mark(X))) mark(plus(X1, X2)) -> active(plus(mark(X1), mark(X2))) mark(times(X1, X2)) -> active(times(mark(X1), mark(X2))) mark(square(X)) -> active(square(mark(X))) mark(0) -> active(0) mark(rnil) -> active(rnil) from(active(X)) -> from(X) from(mark(X)) -> from(X) s(active(X)) -> s(X) s(mark(X)) -> s(X) cons(X1, mark(X2)) -> cons(X1, X2) cons(mark(X1), X2) -> cons(X1, X2) cons(active(X1), X2) -> cons(X1, X2) cons(X1, active(X2)) -> cons(X1, X2) posrecip(active(X)) -> posrecip(X) posrecip(mark(X)) -> posrecip(X) 2ndsneg(X1, mark(X2)) -> 2ndsneg(X1, X2) 2ndsneg(mark(X1), X2) -> 2ndsneg(X1, X2) 2ndsneg(active(X1), X2) -> 2ndsneg(X1, X2) 2ndsneg(X1, active(X2)) -> 2ndsneg(X1, X2) rcons(X1, mark(X2)) -> rcons(X1, X2) rcons(mark(X1), X2) -> rcons(X1, X2) rcons(active(X1), X2) -> rcons(X1, X2) rcons(X1, active(X2)) -> rcons(X1, X2) negrecip(active(X)) -> negrecip(X) negrecip(mark(X)) -> negrecip(X) 2ndspos(X1, mark(X2)) -> 2ndspos(X1, X2) 2ndspos(mark(X1), X2) -> 2ndspos(X1, X2) 2ndspos(active(X1), X2) -> 2ndspos(X1, X2) 2ndspos(X1, active(X2)) -> 2ndspos(X1, X2) plus(X1, mark(X2)) -> plus(X1, X2) plus(mark(X1), X2) -> plus(X1, X2) plus(active(X1), X2) -> plus(X1, X2) plus(X1, active(X2)) -> plus(X1, X2) times(X1, mark(X2)) -> times(X1, X2) times(mark(X1), X2) -> times(X1, X2) times(active(X1), X2) -> times(X1, X2) times(X1, active(X2)) -> times(X1, X2) active(2ndspos(0, Z)) -> mark(rnil) active(2ndsneg(0, Z)) -> mark(rnil) active(times(0, Y)) -> mark(0) pi(active(X)) -> pi(X) pi(mark(X)) -> pi(X) square(active(X)) -> square(X) square(mark(X)) -> square(X) ---------------------------------------- (95) Obligation: Q DP problem: The TRS P consists of the following rules: MARK(from(X)) -> ACTIVE(from(mark(X))) ACTIVE(from(X)) -> MARK(cons(X, from(s(X)))) ACTIVE(2ndspos(s(N), cons(X, cons(Y, Z)))) -> MARK(rcons(posrecip(Y), 2ndsneg(N, Z))) ACTIVE(2ndsneg(s(N), cons(X, cons(Y, Z)))) -> MARK(rcons(negrecip(Y), 2ndspos(N, Z))) MARK(s(X)) -> MARK(X) MARK(2ndspos(X1, X2)) -> ACTIVE(2ndspos(mark(X1), mark(X2))) MARK(2ndspos(X1, X2)) -> MARK(X2) ACTIVE(plus(0, Y)) -> MARK(Y) MARK(rcons(X1, X2)) -> MARK(X2) ACTIVE(plus(s(X), Y)) -> MARK(s(plus(X, Y))) MARK(2ndsneg(X1, X2)) -> ACTIVE(2ndsneg(mark(X1), mark(X2))) ACTIVE(times(s(X), Y)) -> MARK(plus(Y, times(X, Y))) MARK(2ndsneg(X1, X2)) -> MARK(X2) MARK(negrecip(X)) -> MARK(X) MARK(plus(X1, X2)) -> ACTIVE(plus(mark(X1), mark(X2))) MARK(plus(X1, X2)) -> MARK(X1) MARK(plus(X1, X2)) -> MARK(X2) MARK(times(X1, X2)) -> ACTIVE(times(mark(X1), mark(X2))) MARK(times(X1, X2)) -> MARK(X1) MARK(times(X1, X2)) -> MARK(X2) The TRS R consists of the following rules: active(from(X)) -> mark(cons(X, from(s(X)))) active(2ndspos(0, Z)) -> mark(rnil) active(2ndspos(s(N), cons(X, cons(Y, Z)))) -> mark(rcons(posrecip(Y), 2ndsneg(N, Z))) active(2ndsneg(0, Z)) -> mark(rnil) active(2ndsneg(s(N), cons(X, cons(Y, Z)))) -> mark(rcons(negrecip(Y), 2ndspos(N, Z))) active(pi(X)) -> mark(2ndspos(X, from(0))) active(plus(0, Y)) -> mark(Y) active(plus(s(X), Y)) -> mark(s(plus(X, Y))) active(times(0, Y)) -> mark(0) active(times(s(X), Y)) -> mark(plus(Y, times(X, Y))) active(square(X)) -> mark(times(X, X)) mark(from(X)) -> active(from(mark(X))) mark(cons(X1, X2)) -> active(cons(mark(X1), X2)) mark(s(X)) -> active(s(mark(X))) mark(2ndspos(X1, X2)) -> active(2ndspos(mark(X1), mark(X2))) mark(0) -> active(0) mark(rnil) -> active(rnil) mark(rcons(X1, X2)) -> active(rcons(mark(X1), mark(X2))) mark(posrecip(X)) -> active(posrecip(mark(X))) mark(2ndsneg(X1, X2)) -> active(2ndsneg(mark(X1), mark(X2))) mark(negrecip(X)) -> active(negrecip(mark(X))) mark(pi(X)) -> active(pi(mark(X))) mark(plus(X1, X2)) -> active(plus(mark(X1), mark(X2))) mark(times(X1, X2)) -> active(times(mark(X1), mark(X2))) mark(square(X)) -> active(square(mark(X))) from(mark(X)) -> from(X) from(active(X)) -> from(X) cons(mark(X1), X2) -> cons(X1, X2) cons(X1, mark(X2)) -> cons(X1, X2) cons(active(X1), X2) -> cons(X1, X2) cons(X1, active(X2)) -> cons(X1, X2) s(mark(X)) -> s(X) s(active(X)) -> s(X) 2ndspos(mark(X1), X2) -> 2ndspos(X1, X2) 2ndspos(X1, mark(X2)) -> 2ndspos(X1, X2) 2ndspos(active(X1), X2) -> 2ndspos(X1, X2) 2ndspos(X1, active(X2)) -> 2ndspos(X1, X2) rcons(mark(X1), X2) -> rcons(X1, X2) rcons(X1, mark(X2)) -> rcons(X1, X2) rcons(active(X1), X2) -> rcons(X1, X2) rcons(X1, active(X2)) -> rcons(X1, X2) posrecip(mark(X)) -> posrecip(X) posrecip(active(X)) -> posrecip(X) 2ndsneg(mark(X1), X2) -> 2ndsneg(X1, X2) 2ndsneg(X1, mark(X2)) -> 2ndsneg(X1, X2) 2ndsneg(active(X1), X2) -> 2ndsneg(X1, X2) 2ndsneg(X1, active(X2)) -> 2ndsneg(X1, X2) negrecip(mark(X)) -> negrecip(X) negrecip(active(X)) -> negrecip(X) pi(mark(X)) -> pi(X) pi(active(X)) -> pi(X) plus(mark(X1), X2) -> plus(X1, X2) plus(X1, mark(X2)) -> plus(X1, X2) plus(active(X1), X2) -> plus(X1, X2) plus(X1, active(X2)) -> plus(X1, X2) times(mark(X1), X2) -> times(X1, X2) times(X1, mark(X2)) -> times(X1, X2) times(active(X1), X2) -> times(X1, X2) times(X1, active(X2)) -> times(X1, X2) square(mark(X)) -> square(X) square(active(X)) -> square(X) Q is empty. We have to consider all minimal (P,Q,R)-chains. ---------------------------------------- (96) QDPOrderProof (EQUIVALENT) We use the reduction pair processor [LPAR04,JAR06]. The following pairs can be oriented strictly and are deleted. MARK(s(X)) -> MARK(X) ACTIVE(plus(0, Y)) -> MARK(Y) ACTIVE(plus(s(X), Y)) -> MARK(s(plus(X, Y))) ACTIVE(times(s(X), Y)) -> MARK(plus(Y, times(X, Y))) MARK(plus(X1, X2)) -> MARK(X1) MARK(plus(X1, X2)) -> MARK(X2) MARK(times(X1, X2)) -> MARK(X1) MARK(times(X1, X2)) -> MARK(X2) The remaining pairs can at least be oriented weakly. Used ordering: Combined order from the following AFS and order. MARK(x1) = MARK(x1) from(x1) = from ACTIVE(x1) = ACTIVE(x1) mark(x1) = x1 cons(x1, x2) = x2 s(x1) = s(x1) 2ndspos(x1, x2) = x2 rcons(x1, x2) = x2 posrecip(x1) = posrecip(x1) 2ndsneg(x1, x2) = x2 negrecip(x1) = x1 plus(x1, x2) = plus(x1, x2) 0 = 0 times(x1, x2) = times(x1, x2) active(x1) = x1 pi(x1) = pi(x1) square(x1) = square(x1) rnil = rnil Recursive path order with status [RPO]. Quasi-Precedence: [from, pi_1] > [MARK_1, ACTIVE_1, s_1, rnil] posrecip_1 > [MARK_1, ACTIVE_1, s_1, rnil] 0 > [MARK_1, ACTIVE_1, s_1, rnil] square_1 > times_2 > plus_2 > [MARK_1, ACTIVE_1, s_1, rnil] Status: MARK_1: multiset status from: [] ACTIVE_1: multiset status s_1: [1] posrecip_1: multiset status plus_2: multiset status 0: multiset status times_2: [2,1] pi_1: [1] square_1: 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)) -> active(from(mark(X))) active(from(X)) -> mark(cons(X, from(s(X)))) mark(cons(X1, X2)) -> active(cons(mark(X1), X2)) active(2ndspos(s(N), cons(X, cons(Y, Z)))) -> mark(rcons(posrecip(Y), 2ndsneg(N, Z))) mark(s(X)) -> active(s(mark(X))) active(2ndsneg(s(N), cons(X, cons(Y, Z)))) -> mark(rcons(negrecip(Y), 2ndspos(N, Z))) mark(2ndspos(X1, X2)) -> active(2ndspos(mark(X1), mark(X2))) active(pi(X)) -> mark(2ndspos(X, from(0))) mark(rcons(X1, X2)) -> active(rcons(mark(X1), mark(X2))) active(plus(0, Y)) -> mark(Y) mark(posrecip(X)) -> active(posrecip(mark(X))) active(plus(s(X), Y)) -> mark(s(plus(X, Y))) mark(2ndsneg(X1, X2)) -> active(2ndsneg(mark(X1), mark(X2))) active(times(s(X), Y)) -> mark(plus(Y, times(X, Y))) mark(negrecip(X)) -> active(negrecip(mark(X))) active(square(X)) -> mark(times(X, X)) mark(pi(X)) -> active(pi(mark(X))) mark(plus(X1, X2)) -> active(plus(mark(X1), mark(X2))) mark(times(X1, X2)) -> active(times(mark(X1), mark(X2))) mark(square(X)) -> active(square(mark(X))) mark(0) -> active(0) mark(rnil) -> active(rnil) from(active(X)) -> from(X) from(mark(X)) -> from(X) s(active(X)) -> s(X) s(mark(X)) -> s(X) cons(X1, mark(X2)) -> cons(X1, X2) cons(mark(X1), X2) -> cons(X1, X2) cons(active(X1), X2) -> cons(X1, X2) cons(X1, active(X2)) -> cons(X1, X2) posrecip(active(X)) -> posrecip(X) posrecip(mark(X)) -> posrecip(X) 2ndsneg(X1, mark(X2)) -> 2ndsneg(X1, X2) 2ndsneg(mark(X1), X2) -> 2ndsneg(X1, X2) 2ndsneg(active(X1), X2) -> 2ndsneg(X1, X2) 2ndsneg(X1, active(X2)) -> 2ndsneg(X1, X2) rcons(X1, mark(X2)) -> rcons(X1, X2) rcons(mark(X1), X2) -> rcons(X1, X2) rcons(active(X1), X2) -> rcons(X1, X2) rcons(X1, active(X2)) -> rcons(X1, X2) negrecip(active(X)) -> negrecip(X) negrecip(mark(X)) -> negrecip(X) 2ndspos(X1, mark(X2)) -> 2ndspos(X1, X2) 2ndspos(mark(X1), X2) -> 2ndspos(X1, X2) 2ndspos(active(X1), X2) -> 2ndspos(X1, X2) 2ndspos(X1, active(X2)) -> 2ndspos(X1, X2) plus(X1, mark(X2)) -> plus(X1, X2) plus(mark(X1), X2) -> plus(X1, X2) plus(active(X1), X2) -> plus(X1, X2) plus(X1, active(X2)) -> plus(X1, X2) times(X1, mark(X2)) -> times(X1, X2) times(mark(X1), X2) -> times(X1, X2) times(active(X1), X2) -> times(X1, X2) times(X1, active(X2)) -> times(X1, X2) active(2ndspos(0, Z)) -> mark(rnil) active(2ndsneg(0, Z)) -> mark(rnil) active(times(0, Y)) -> mark(0) pi(active(X)) -> pi(X) pi(mark(X)) -> pi(X) square(active(X)) -> square(X) square(mark(X)) -> square(X) ---------------------------------------- (97) Obligation: Q DP problem: The TRS P consists of the following rules: MARK(from(X)) -> ACTIVE(from(mark(X))) ACTIVE(from(X)) -> MARK(cons(X, from(s(X)))) ACTIVE(2ndspos(s(N), cons(X, cons(Y, Z)))) -> MARK(rcons(posrecip(Y), 2ndsneg(N, Z))) ACTIVE(2ndsneg(s(N), cons(X, cons(Y, Z)))) -> MARK(rcons(negrecip(Y), 2ndspos(N, Z))) MARK(2ndspos(X1, X2)) -> ACTIVE(2ndspos(mark(X1), mark(X2))) MARK(2ndspos(X1, X2)) -> MARK(X2) MARK(rcons(X1, X2)) -> MARK(X2) MARK(2ndsneg(X1, X2)) -> ACTIVE(2ndsneg(mark(X1), mark(X2))) MARK(2ndsneg(X1, X2)) -> MARK(X2) MARK(negrecip(X)) -> MARK(X) MARK(plus(X1, X2)) -> ACTIVE(plus(mark(X1), mark(X2))) MARK(times(X1, X2)) -> ACTIVE(times(mark(X1), mark(X2))) The TRS R consists of the following rules: active(from(X)) -> mark(cons(X, from(s(X)))) active(2ndspos(0, Z)) -> mark(rnil) active(2ndspos(s(N), cons(X, cons(Y, Z)))) -> mark(rcons(posrecip(Y), 2ndsneg(N, Z))) active(2ndsneg(0, Z)) -> mark(rnil) active(2ndsneg(s(N), cons(X, cons(Y, Z)))) -> mark(rcons(negrecip(Y), 2ndspos(N, Z))) active(pi(X)) -> mark(2ndspos(X, from(0))) active(plus(0, Y)) -> mark(Y) active(plus(s(X), Y)) -> mark(s(plus(X, Y))) active(times(0, Y)) -> mark(0) active(times(s(X), Y)) -> mark(plus(Y, times(X, Y))) active(square(X)) -> mark(times(X, X)) mark(from(X)) -> active(from(mark(X))) mark(cons(X1, X2)) -> active(cons(mark(X1), X2)) mark(s(X)) -> active(s(mark(X))) mark(2ndspos(X1, X2)) -> active(2ndspos(mark(X1), mark(X2))) mark(0) -> active(0) mark(rnil) -> active(rnil) mark(rcons(X1, X2)) -> active(rcons(mark(X1), mark(X2))) mark(posrecip(X)) -> active(posrecip(mark(X))) mark(2ndsneg(X1, X2)) -> active(2ndsneg(mark(X1), mark(X2))) mark(negrecip(X)) -> active(negrecip(mark(X))) mark(pi(X)) -> active(pi(mark(X))) mark(plus(X1, X2)) -> active(plus(mark(X1), mark(X2))) mark(times(X1, X2)) -> active(times(mark(X1), mark(X2))) mark(square(X)) -> active(square(mark(X))) from(mark(X)) -> from(X) from(active(X)) -> from(X) cons(mark(X1), X2) -> cons(X1, X2) cons(X1, mark(X2)) -> cons(X1, X2) cons(active(X1), X2) -> cons(X1, X2) cons(X1, active(X2)) -> cons(X1, X2) s(mark(X)) -> s(X) s(active(X)) -> s(X) 2ndspos(mark(X1), X2) -> 2ndspos(X1, X2) 2ndspos(X1, mark(X2)) -> 2ndspos(X1, X2) 2ndspos(active(X1), X2) -> 2ndspos(X1, X2) 2ndspos(X1, active(X2)) -> 2ndspos(X1, X2) rcons(mark(X1), X2) -> rcons(X1, X2) rcons(X1, mark(X2)) -> rcons(X1, X2) rcons(active(X1), X2) -> rcons(X1, X2) rcons(X1, active(X2)) -> rcons(X1, X2) posrecip(mark(X)) -> posrecip(X) posrecip(active(X)) -> posrecip(X) 2ndsneg(mark(X1), X2) -> 2ndsneg(X1, X2) 2ndsneg(X1, mark(X2)) -> 2ndsneg(X1, X2) 2ndsneg(active(X1), X2) -> 2ndsneg(X1, X2) 2ndsneg(X1, active(X2)) -> 2ndsneg(X1, X2) negrecip(mark(X)) -> negrecip(X) negrecip(active(X)) -> negrecip(X) pi(mark(X)) -> pi(X) pi(active(X)) -> pi(X) plus(mark(X1), X2) -> plus(X1, X2) plus(X1, mark(X2)) -> plus(X1, X2) plus(active(X1), X2) -> plus(X1, X2) plus(X1, active(X2)) -> plus(X1, X2) times(mark(X1), X2) -> times(X1, X2) times(X1, mark(X2)) -> times(X1, X2) times(active(X1), X2) -> times(X1, X2) times(X1, active(X2)) -> times(X1, X2) square(mark(X)) -> square(X) square(active(X)) -> square(X) Q is empty. We have to consider all minimal (P,Q,R)-chains. ---------------------------------------- (98) QDPOrderProof (EQUIVALENT) We use the reduction pair processor [LPAR04,JAR06]. The following pairs can be oriented strictly and are deleted. MARK(times(X1, X2)) -> ACTIVE(times(mark(X1), mark(X2))) The remaining pairs can at least be oriented weakly. Used ordering: Polynomial Order [NEGPOLO,POLO] with Interpretation: POL( 2ndsneg_2(x_1, x_2) ) = 2 POL( ACTIVE_1(x_1) ) = x_1 POL( 2ndspos_2(x_1, x_2) ) = 2 POL( from_1(x_1) ) = 2 POL( plus_2(x_1, x_2) ) = 2 POL( times_2(x_1, x_2) ) = max{0, -2} POL( mark_1(x_1) ) = 2 POL( active_1(x_1) ) = 2 POL( cons_2(x_1, x_2) ) = max{0, -2} POL( s_1(x_1) ) = x_1 POL( rcons_2(x_1, x_2) ) = max{0, 2x_1 - 2} POL( posrecip_1(x_1) ) = 2 POL( negrecip_1(x_1) ) = 2x_1 + 2 POL( pi_1(x_1) ) = x_1 POL( 0 ) = 0 POL( square_1(x_1) ) = 2x_1 + 2 POL( rnil ) = 0 POL( MARK_1(x_1) ) = 2 The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented: from(active(X)) -> from(X) from(mark(X)) -> from(X) 2ndsneg(X1, mark(X2)) -> 2ndsneg(X1, X2) 2ndsneg(mark(X1), X2) -> 2ndsneg(X1, X2) 2ndsneg(active(X1), X2) -> 2ndsneg(X1, X2) 2ndsneg(X1, active(X2)) -> 2ndsneg(X1, X2) 2ndspos(X1, mark(X2)) -> 2ndspos(X1, X2) 2ndspos(mark(X1), X2) -> 2ndspos(X1, X2) 2ndspos(active(X1), X2) -> 2ndspos(X1, X2) 2ndspos(X1, active(X2)) -> 2ndspos(X1, X2) plus(X1, mark(X2)) -> plus(X1, X2) plus(mark(X1), X2) -> plus(X1, X2) plus(active(X1), X2) -> plus(X1, X2) plus(X1, active(X2)) -> plus(X1, X2) times(X1, mark(X2)) -> times(X1, X2) times(mark(X1), X2) -> times(X1, X2) times(active(X1), X2) -> times(X1, X2) times(X1, active(X2)) -> times(X1, X2) ---------------------------------------- (99) Obligation: Q DP problem: The TRS P consists of the following rules: MARK(from(X)) -> ACTIVE(from(mark(X))) ACTIVE(from(X)) -> MARK(cons(X, from(s(X)))) ACTIVE(2ndspos(s(N), cons(X, cons(Y, Z)))) -> MARK(rcons(posrecip(Y), 2ndsneg(N, Z))) ACTIVE(2ndsneg(s(N), cons(X, cons(Y, Z)))) -> MARK(rcons(negrecip(Y), 2ndspos(N, Z))) MARK(2ndspos(X1, X2)) -> ACTIVE(2ndspos(mark(X1), mark(X2))) MARK(2ndspos(X1, X2)) -> MARK(X2) MARK(rcons(X1, X2)) -> MARK(X2) MARK(2ndsneg(X1, X2)) -> ACTIVE(2ndsneg(mark(X1), mark(X2))) MARK(2ndsneg(X1, X2)) -> MARK(X2) MARK(negrecip(X)) -> MARK(X) MARK(plus(X1, X2)) -> ACTIVE(plus(mark(X1), mark(X2))) The TRS R consists of the following rules: active(from(X)) -> mark(cons(X, from(s(X)))) active(2ndspos(0, Z)) -> mark(rnil) active(2ndspos(s(N), cons(X, cons(Y, Z)))) -> mark(rcons(posrecip(Y), 2ndsneg(N, Z))) active(2ndsneg(0, Z)) -> mark(rnil) active(2ndsneg(s(N), cons(X, cons(Y, Z)))) -> mark(rcons(negrecip(Y), 2ndspos(N, Z))) active(pi(X)) -> mark(2ndspos(X, from(0))) active(plus(0, Y)) -> mark(Y) active(plus(s(X), Y)) -> mark(s(plus(X, Y))) active(times(0, Y)) -> mark(0) active(times(s(X), Y)) -> mark(plus(Y, times(X, Y))) active(square(X)) -> mark(times(X, X)) mark(from(X)) -> active(from(mark(X))) mark(cons(X1, X2)) -> active(cons(mark(X1), X2)) mark(s(X)) -> active(s(mark(X))) mark(2ndspos(X1, X2)) -> active(2ndspos(mark(X1), mark(X2))) mark(0) -> active(0) mark(rnil) -> active(rnil) mark(rcons(X1, X2)) -> active(rcons(mark(X1), mark(X2))) mark(posrecip(X)) -> active(posrecip(mark(X))) mark(2ndsneg(X1, X2)) -> active(2ndsneg(mark(X1), mark(X2))) mark(negrecip(X)) -> active(negrecip(mark(X))) mark(pi(X)) -> active(pi(mark(X))) mark(plus(X1, X2)) -> active(plus(mark(X1), mark(X2))) mark(times(X1, X2)) -> active(times(mark(X1), mark(X2))) mark(square(X)) -> active(square(mark(X))) from(mark(X)) -> from(X) from(active(X)) -> from(X) cons(mark(X1), X2) -> cons(X1, X2) cons(X1, mark(X2)) -> cons(X1, X2) cons(active(X1), X2) -> cons(X1, X2) cons(X1, active(X2)) -> cons(X1, X2) s(mark(X)) -> s(X) s(active(X)) -> s(X) 2ndspos(mark(X1), X2) -> 2ndspos(X1, X2) 2ndspos(X1, mark(X2)) -> 2ndspos(X1, X2) 2ndspos(active(X1), X2) -> 2ndspos(X1, X2) 2ndspos(X1, active(X2)) -> 2ndspos(X1, X2) rcons(mark(X1), X2) -> rcons(X1, X2) rcons(X1, mark(X2)) -> rcons(X1, X2) rcons(active(X1), X2) -> rcons(X1, X2) rcons(X1, active(X2)) -> rcons(X1, X2) posrecip(mark(X)) -> posrecip(X) posrecip(active(X)) -> posrecip(X) 2ndsneg(mark(X1), X2) -> 2ndsneg(X1, X2) 2ndsneg(X1, mark(X2)) -> 2ndsneg(X1, X2) 2ndsneg(active(X1), X2) -> 2ndsneg(X1, X2) 2ndsneg(X1, active(X2)) -> 2ndsneg(X1, X2) negrecip(mark(X)) -> negrecip(X) negrecip(active(X)) -> negrecip(X) pi(mark(X)) -> pi(X) pi(active(X)) -> pi(X) plus(mark(X1), X2) -> plus(X1, X2) plus(X1, mark(X2)) -> plus(X1, X2) plus(active(X1), X2) -> plus(X1, X2) plus(X1, active(X2)) -> plus(X1, X2) times(mark(X1), X2) -> times(X1, X2) times(X1, mark(X2)) -> times(X1, X2) times(active(X1), X2) -> times(X1, X2) times(X1, active(X2)) -> times(X1, X2) square(mark(X)) -> square(X) square(active(X)) -> square(X) Q is empty. We have to consider all minimal (P,Q,R)-chains. ---------------------------------------- (100) QDPOrderProof (EQUIVALENT) We use the reduction pair processor [LPAR04,JAR06]. The following pairs can be oriented strictly and are deleted. MARK(plus(X1, X2)) -> ACTIVE(plus(mark(X1), mark(X2))) The remaining pairs can at least be oriented weakly. Used ordering: Polynomial Order [NEGPOLO,POLO] with Interpretation: POL( 2ndsneg_2(x_1, x_2) ) = 1 POL( ACTIVE_1(x_1) ) = max{0, 2x_1 - 1} POL( 2ndspos_2(x_1, x_2) ) = 1 POL( from_1(x_1) ) = 1 POL( plus_2(x_1, x_2) ) = max{0, -1} POL( mark_1(x_1) ) = x_1 + 2 POL( active_1(x_1) ) = x_1 POL( cons_2(x_1, x_2) ) = max{0, 2x_2 - 1} POL( s_1(x_1) ) = 2 POL( rcons_2(x_1, x_2) ) = max{0, x_1 - 2} POL( posrecip_1(x_1) ) = 2 POL( negrecip_1(x_1) ) = 2x_1 + 2 POL( pi_1(x_1) ) = 2 POL( 0 ) = 1 POL( times_2(x_1, x_2) ) = 0 POL( square_1(x_1) ) = max{0, x_1 - 2} POL( rnil ) = 2 POL( MARK_1(x_1) ) = 1 The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented: from(active(X)) -> from(X) from(mark(X)) -> from(X) 2ndsneg(X1, mark(X2)) -> 2ndsneg(X1, X2) 2ndsneg(mark(X1), X2) -> 2ndsneg(X1, X2) 2ndsneg(active(X1), X2) -> 2ndsneg(X1, X2) 2ndsneg(X1, active(X2)) -> 2ndsneg(X1, X2) 2ndspos(X1, mark(X2)) -> 2ndspos(X1, X2) 2ndspos(mark(X1), X2) -> 2ndspos(X1, X2) 2ndspos(active(X1), X2) -> 2ndspos(X1, X2) 2ndspos(X1, active(X2)) -> 2ndspos(X1, X2) plus(X1, mark(X2)) -> plus(X1, X2) plus(mark(X1), X2) -> plus(X1, X2) plus(active(X1), X2) -> plus(X1, X2) plus(X1, active(X2)) -> plus(X1, X2) ---------------------------------------- (101) Obligation: Q DP problem: The TRS P consists of the following rules: MARK(from(X)) -> ACTIVE(from(mark(X))) ACTIVE(from(X)) -> MARK(cons(X, from(s(X)))) ACTIVE(2ndspos(s(N), cons(X, cons(Y, Z)))) -> MARK(rcons(posrecip(Y), 2ndsneg(N, Z))) ACTIVE(2ndsneg(s(N), cons(X, cons(Y, Z)))) -> MARK(rcons(negrecip(Y), 2ndspos(N, Z))) MARK(2ndspos(X1, X2)) -> ACTIVE(2ndspos(mark(X1), mark(X2))) MARK(2ndspos(X1, X2)) -> MARK(X2) MARK(rcons(X1, X2)) -> MARK(X2) MARK(2ndsneg(X1, X2)) -> ACTIVE(2ndsneg(mark(X1), mark(X2))) MARK(2ndsneg(X1, X2)) -> MARK(X2) MARK(negrecip(X)) -> MARK(X) The TRS R consists of the following rules: active(from(X)) -> mark(cons(X, from(s(X)))) active(2ndspos(0, Z)) -> mark(rnil) active(2ndspos(s(N), cons(X, cons(Y, Z)))) -> mark(rcons(posrecip(Y), 2ndsneg(N, Z))) active(2ndsneg(0, Z)) -> mark(rnil) active(2ndsneg(s(N), cons(X, cons(Y, Z)))) -> mark(rcons(negrecip(Y), 2ndspos(N, Z))) active(pi(X)) -> mark(2ndspos(X, from(0))) active(plus(0, Y)) -> mark(Y) active(plus(s(X), Y)) -> mark(s(plus(X, Y))) active(times(0, Y)) -> mark(0) active(times(s(X), Y)) -> mark(plus(Y, times(X, Y))) active(square(X)) -> mark(times(X, X)) mark(from(X)) -> active(from(mark(X))) mark(cons(X1, X2)) -> active(cons(mark(X1), X2)) mark(s(X)) -> active(s(mark(X))) mark(2ndspos(X1, X2)) -> active(2ndspos(mark(X1), mark(X2))) mark(0) -> active(0) mark(rnil) -> active(rnil) mark(rcons(X1, X2)) -> active(rcons(mark(X1), mark(X2))) mark(posrecip(X)) -> active(posrecip(mark(X))) mark(2ndsneg(X1, X2)) -> active(2ndsneg(mark(X1), mark(X2))) mark(negrecip(X)) -> active(negrecip(mark(X))) mark(pi(X)) -> active(pi(mark(X))) mark(plus(X1, X2)) -> active(plus(mark(X1), mark(X2))) mark(times(X1, X2)) -> active(times(mark(X1), mark(X2))) mark(square(X)) -> active(square(mark(X))) from(mark(X)) -> from(X) from(active(X)) -> from(X) cons(mark(X1), X2) -> cons(X1, X2) cons(X1, mark(X2)) -> cons(X1, X2) cons(active(X1), X2) -> cons(X1, X2) cons(X1, active(X2)) -> cons(X1, X2) s(mark(X)) -> s(X) s(active(X)) -> s(X) 2ndspos(mark(X1), X2) -> 2ndspos(X1, X2) 2ndspos(X1, mark(X2)) -> 2ndspos(X1, X2) 2ndspos(active(X1), X2) -> 2ndspos(X1, X2) 2ndspos(X1, active(X2)) -> 2ndspos(X1, X2) rcons(mark(X1), X2) -> rcons(X1, X2) rcons(X1, mark(X2)) -> rcons(X1, X2) rcons(active(X1), X2) -> rcons(X1, X2) rcons(X1, active(X2)) -> rcons(X1, X2) posrecip(mark(X)) -> posrecip(X) posrecip(active(X)) -> posrecip(X) 2ndsneg(mark(X1), X2) -> 2ndsneg(X1, X2) 2ndsneg(X1, mark(X2)) -> 2ndsneg(X1, X2) 2ndsneg(active(X1), X2) -> 2ndsneg(X1, X2) 2ndsneg(X1, active(X2)) -> 2ndsneg(X1, X2) negrecip(mark(X)) -> negrecip(X) negrecip(active(X)) -> negrecip(X) pi(mark(X)) -> pi(X) pi(active(X)) -> pi(X) plus(mark(X1), X2) -> plus(X1, X2) plus(X1, mark(X2)) -> plus(X1, X2) plus(active(X1), X2) -> plus(X1, X2) plus(X1, active(X2)) -> plus(X1, X2) times(mark(X1), X2) -> times(X1, X2) times(X1, mark(X2)) -> times(X1, X2) times(active(X1), X2) -> times(X1, X2) times(X1, active(X2)) -> times(X1, X2) square(mark(X)) -> square(X) square(active(X)) -> square(X) Q is empty. We have to consider all minimal (P,Q,R)-chains. ---------------------------------------- (102) 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(X2) MARK(2ndsneg(X1, X2)) -> MARK(X2) MARK(negrecip(X)) -> MARK(X) The remaining pairs can at least be oriented weakly. Used ordering: Polynomial Order [NEGPOLO,POLO] with Interpretation: POL( 2ndsneg_2(x_1, x_2) ) = 2x_1 + x_2 + 1 POL( ACTIVE_1(x_1) ) = 2x_1 + 2 POL( 2ndspos_2(x_1, x_2) ) = 2x_1 + x_2 + 1 POL( from_1(x_1) ) = 1 POL( mark_1(x_1) ) = x_1 POL( active_1(x_1) ) = x_1 POL( cons_2(x_1, x_2) ) = x_2 POL( s_1(x_1) ) = x_1 POL( rcons_2(x_1, x_2) ) = x_2 POL( posrecip_1(x_1) ) = max{0, -2} POL( negrecip_1(x_1) ) = x_1 + 1 POL( pi_1(x_1) ) = 2x_1 + 2 POL( 0 ) = 0 POL( plus_2(x_1, x_2) ) = x_2 POL( times_2(x_1, x_2) ) = 2x_2 POL( square_1(x_1) ) = 2x_1 + 2 POL( rnil ) = 1 POL( MARK_1(x_1) ) = 2x_1 + 2 The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented: mark(from(X)) -> active(from(mark(X))) active(from(X)) -> mark(cons(X, from(s(X)))) mark(cons(X1, X2)) -> active(cons(mark(X1), X2)) active(2ndspos(s(N), cons(X, cons(Y, Z)))) -> mark(rcons(posrecip(Y), 2ndsneg(N, Z))) mark(s(X)) -> active(s(mark(X))) active(2ndsneg(s(N), cons(X, cons(Y, Z)))) -> mark(rcons(negrecip(Y), 2ndspos(N, Z))) mark(2ndspos(X1, X2)) -> active(2ndspos(mark(X1), mark(X2))) active(pi(X)) -> mark(2ndspos(X, from(0))) mark(rcons(X1, X2)) -> active(rcons(mark(X1), mark(X2))) active(plus(0, Y)) -> mark(Y) mark(posrecip(X)) -> active(posrecip(mark(X))) active(plus(s(X), Y)) -> mark(s(plus(X, Y))) mark(2ndsneg(X1, X2)) -> active(2ndsneg(mark(X1), mark(X2))) active(times(s(X), Y)) -> mark(plus(Y, times(X, Y))) mark(negrecip(X)) -> active(negrecip(mark(X))) active(square(X)) -> mark(times(X, X)) mark(pi(X)) -> active(pi(mark(X))) mark(plus(X1, X2)) -> active(plus(mark(X1), mark(X2))) mark(times(X1, X2)) -> active(times(mark(X1), mark(X2))) mark(square(X)) -> active(square(mark(X))) mark(0) -> active(0) mark(rnil) -> active(rnil) from(active(X)) -> from(X) from(mark(X)) -> from(X) s(active(X)) -> s(X) s(mark(X)) -> s(X) cons(X1, mark(X2)) -> cons(X1, X2) cons(mark(X1), X2) -> cons(X1, X2) cons(active(X1), X2) -> cons(X1, X2) cons(X1, active(X2)) -> cons(X1, X2) posrecip(active(X)) -> posrecip(X) posrecip(mark(X)) -> posrecip(X) 2ndsneg(X1, mark(X2)) -> 2ndsneg(X1, X2) 2ndsneg(mark(X1), X2) -> 2ndsneg(X1, X2) 2ndsneg(active(X1), X2) -> 2ndsneg(X1, X2) 2ndsneg(X1, active(X2)) -> 2ndsneg(X1, X2) rcons(X1, mark(X2)) -> rcons(X1, X2) rcons(mark(X1), X2) -> rcons(X1, X2) rcons(active(X1), X2) -> rcons(X1, X2) rcons(X1, active(X2)) -> rcons(X1, X2) negrecip(active(X)) -> negrecip(X) negrecip(mark(X)) -> negrecip(X) 2ndspos(X1, mark(X2)) -> 2ndspos(X1, X2) 2ndspos(mark(X1), X2) -> 2ndspos(X1, X2) 2ndspos(active(X1), X2) -> 2ndspos(X1, X2) 2ndspos(X1, active(X2)) -> 2ndspos(X1, X2) active(2ndspos(0, Z)) -> mark(rnil) active(2ndsneg(0, Z)) -> mark(rnil) active(times(0, Y)) -> mark(0) plus(X1, mark(X2)) -> plus(X1, X2) plus(mark(X1), X2) -> plus(X1, X2) plus(active(X1), X2) -> plus(X1, X2) plus(X1, active(X2)) -> plus(X1, X2) times(X1, mark(X2)) -> times(X1, X2) times(mark(X1), X2) -> times(X1, X2) times(active(X1), X2) -> times(X1, X2) times(X1, active(X2)) -> times(X1, X2) pi(active(X)) -> pi(X) pi(mark(X)) -> pi(X) square(active(X)) -> square(X) square(mark(X)) -> square(X) ---------------------------------------- (103) Obligation: Q DP problem: The TRS P consists of the following rules: MARK(from(X)) -> ACTIVE(from(mark(X))) ACTIVE(from(X)) -> MARK(cons(X, from(s(X)))) ACTIVE(2ndspos(s(N), cons(X, cons(Y, Z)))) -> MARK(rcons(posrecip(Y), 2ndsneg(N, Z))) ACTIVE(2ndsneg(s(N), cons(X, cons(Y, Z)))) -> MARK(rcons(negrecip(Y), 2ndspos(N, Z))) MARK(2ndspos(X1, X2)) -> ACTIVE(2ndspos(mark(X1), mark(X2))) MARK(rcons(X1, X2)) -> MARK(X2) MARK(2ndsneg(X1, X2)) -> ACTIVE(2ndsneg(mark(X1), mark(X2))) The TRS R consists of the following rules: active(from(X)) -> mark(cons(X, from(s(X)))) active(2ndspos(0, Z)) -> mark(rnil) active(2ndspos(s(N), cons(X, cons(Y, Z)))) -> mark(rcons(posrecip(Y), 2ndsneg(N, Z))) active(2ndsneg(0, Z)) -> mark(rnil) active(2ndsneg(s(N), cons(X, cons(Y, Z)))) -> mark(rcons(negrecip(Y), 2ndspos(N, Z))) active(pi(X)) -> mark(2ndspos(X, from(0))) active(plus(0, Y)) -> mark(Y) active(plus(s(X), Y)) -> mark(s(plus(X, Y))) active(times(0, Y)) -> mark(0) active(times(s(X), Y)) -> mark(plus(Y, times(X, Y))) active(square(X)) -> mark(times(X, X)) mark(from(X)) -> active(from(mark(X))) mark(cons(X1, X2)) -> active(cons(mark(X1), X2)) mark(s(X)) -> active(s(mark(X))) mark(2ndspos(X1, X2)) -> active(2ndspos(mark(X1), mark(X2))) mark(0) -> active(0) mark(rnil) -> active(rnil) mark(rcons(X1, X2)) -> active(rcons(mark(X1), mark(X2))) mark(posrecip(X)) -> active(posrecip(mark(X))) mark(2ndsneg(X1, X2)) -> active(2ndsneg(mark(X1), mark(X2))) mark(negrecip(X)) -> active(negrecip(mark(X))) mark(pi(X)) -> active(pi(mark(X))) mark(plus(X1, X2)) -> active(plus(mark(X1), mark(X2))) mark(times(X1, X2)) -> active(times(mark(X1), mark(X2))) mark(square(X)) -> active(square(mark(X))) from(mark(X)) -> from(X) from(active(X)) -> from(X) cons(mark(X1), X2) -> cons(X1, X2) cons(X1, mark(X2)) -> cons(X1, X2) cons(active(X1), X2) -> cons(X1, X2) cons(X1, active(X2)) -> cons(X1, X2) s(mark(X)) -> s(X) s(active(X)) -> s(X) 2ndspos(mark(X1), X2) -> 2ndspos(X1, X2) 2ndspos(X1, mark(X2)) -> 2ndspos(X1, X2) 2ndspos(active(X1), X2) -> 2ndspos(X1, X2) 2ndspos(X1, active(X2)) -> 2ndspos(X1, X2) rcons(mark(X1), X2) -> rcons(X1, X2) rcons(X1, mark(X2)) -> rcons(X1, X2) rcons(active(X1), X2) -> rcons(X1, X2) rcons(X1, active(X2)) -> rcons(X1, X2) posrecip(mark(X)) -> posrecip(X) posrecip(active(X)) -> posrecip(X) 2ndsneg(mark(X1), X2) -> 2ndsneg(X1, X2) 2ndsneg(X1, mark(X2)) -> 2ndsneg(X1, X2) 2ndsneg(active(X1), X2) -> 2ndsneg(X1, X2) 2ndsneg(X1, active(X2)) -> 2ndsneg(X1, X2) negrecip(mark(X)) -> negrecip(X) negrecip(active(X)) -> negrecip(X) pi(mark(X)) -> pi(X) pi(active(X)) -> pi(X) plus(mark(X1), X2) -> plus(X1, X2) plus(X1, mark(X2)) -> plus(X1, X2) plus(active(X1), X2) -> plus(X1, X2) plus(X1, active(X2)) -> plus(X1, X2) times(mark(X1), X2) -> times(X1, X2) times(X1, mark(X2)) -> times(X1, X2) times(active(X1), X2) -> times(X1, X2) times(X1, active(X2)) -> times(X1, X2) square(mark(X)) -> square(X) square(active(X)) -> square(X) Q is empty. We have to consider all minimal (P,Q,R)-chains. ---------------------------------------- (104) QDPOrderProof (EQUIVALENT) We use the reduction pair processor [LPAR04,JAR06]. The following pairs can be oriented strictly and are deleted. ACTIVE(from(X)) -> MARK(cons(X, from(s(X)))) The remaining pairs can at least be oriented weakly. Used ordering: Combined order from the following AFS and order. MARK(x1) = x1 from(x1) = from ACTIVE(x1) = x1 cons(x1, x2) = cons 2ndspos(x1, x2) = x1 s(x1) = x1 rcons(x1, x2) = x2 2ndsneg(x1, x2) = x1 mark(x1) = x1 active(x1) = x1 pi(x1) = x1 plus(x1, x2) = x2 posrecip(x1) = posrecip times(x1, x2) = times negrecip(x1) = negrecip square(x1) = square 0 = 0 rnil = rnil Knuth-Bendix order [KBO] with precedence:trivial and weight map: negrecip=1 rnil=2 0=3 cons=2 square=5 from=3 posrecip=2 times=4 The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented: mark(from(X)) -> active(from(mark(X))) active(from(X)) -> mark(cons(X, from(s(X)))) mark(cons(X1, X2)) -> active(cons(mark(X1), X2)) active(2ndspos(s(N), cons(X, cons(Y, Z)))) -> mark(rcons(posrecip(Y), 2ndsneg(N, Z))) mark(s(X)) -> active(s(mark(X))) active(2ndsneg(s(N), cons(X, cons(Y, Z)))) -> mark(rcons(negrecip(Y), 2ndspos(N, Z))) mark(2ndspos(X1, X2)) -> active(2ndspos(mark(X1), mark(X2))) active(pi(X)) -> mark(2ndspos(X, from(0))) mark(rcons(X1, X2)) -> active(rcons(mark(X1), mark(X2))) active(plus(0, Y)) -> mark(Y) mark(posrecip(X)) -> active(posrecip(mark(X))) active(plus(s(X), Y)) -> mark(s(plus(X, Y))) mark(2ndsneg(X1, X2)) -> active(2ndsneg(mark(X1), mark(X2))) active(times(s(X), Y)) -> mark(plus(Y, times(X, Y))) mark(negrecip(X)) -> active(negrecip(mark(X))) active(square(X)) -> mark(times(X, X)) mark(pi(X)) -> active(pi(mark(X))) mark(plus(X1, X2)) -> active(plus(mark(X1), mark(X2))) mark(times(X1, X2)) -> active(times(mark(X1), mark(X2))) mark(square(X)) -> active(square(mark(X))) mark(0) -> active(0) mark(rnil) -> active(rnil) from(active(X)) -> from(X) from(mark(X)) -> from(X) s(active(X)) -> s(X) s(mark(X)) -> s(X) cons(X1, mark(X2)) -> cons(X1, X2) cons(mark(X1), X2) -> cons(X1, X2) cons(active(X1), X2) -> cons(X1, X2) cons(X1, active(X2)) -> cons(X1, X2) posrecip(active(X)) -> posrecip(X) posrecip(mark(X)) -> posrecip(X) 2ndsneg(X1, mark(X2)) -> 2ndsneg(X1, X2) 2ndsneg(mark(X1), X2) -> 2ndsneg(X1, X2) 2ndsneg(active(X1), X2) -> 2ndsneg(X1, X2) 2ndsneg(X1, active(X2)) -> 2ndsneg(X1, X2) rcons(X1, mark(X2)) -> rcons(X1, X2) rcons(mark(X1), X2) -> rcons(X1, X2) rcons(active(X1), X2) -> rcons(X1, X2) rcons(X1, active(X2)) -> rcons(X1, X2) negrecip(active(X)) -> negrecip(X) negrecip(mark(X)) -> negrecip(X) 2ndspos(X1, mark(X2)) -> 2ndspos(X1, X2) 2ndspos(mark(X1), X2) -> 2ndspos(X1, X2) 2ndspos(active(X1), X2) -> 2ndspos(X1, X2) 2ndspos(X1, active(X2)) -> 2ndspos(X1, X2) active(2ndspos(0, Z)) -> mark(rnil) active(2ndsneg(0, Z)) -> mark(rnil) active(times(0, Y)) -> mark(0) plus(X1, mark(X2)) -> plus(X1, X2) plus(mark(X1), X2) -> plus(X1, X2) plus(active(X1), X2) -> plus(X1, X2) plus(X1, active(X2)) -> plus(X1, X2) times(X1, mark(X2)) -> times(X1, X2) times(mark(X1), X2) -> times(X1, X2) times(active(X1), X2) -> times(X1, X2) times(X1, active(X2)) -> times(X1, X2) pi(active(X)) -> pi(X) pi(mark(X)) -> pi(X) square(active(X)) -> square(X) square(mark(X)) -> square(X) ---------------------------------------- (105) Obligation: Q DP problem: The TRS P consists of the following rules: MARK(from(X)) -> ACTIVE(from(mark(X))) ACTIVE(2ndspos(s(N), cons(X, cons(Y, Z)))) -> MARK(rcons(posrecip(Y), 2ndsneg(N, Z))) ACTIVE(2ndsneg(s(N), cons(X, cons(Y, Z)))) -> MARK(rcons(negrecip(Y), 2ndspos(N, Z))) MARK(2ndspos(X1, X2)) -> ACTIVE(2ndspos(mark(X1), mark(X2))) MARK(rcons(X1, X2)) -> MARK(X2) MARK(2ndsneg(X1, X2)) -> ACTIVE(2ndsneg(mark(X1), mark(X2))) The TRS R consists of the following rules: active(from(X)) -> mark(cons(X, from(s(X)))) active(2ndspos(0, Z)) -> mark(rnil) active(2ndspos(s(N), cons(X, cons(Y, Z)))) -> mark(rcons(posrecip(Y), 2ndsneg(N, Z))) active(2ndsneg(0, Z)) -> mark(rnil) active(2ndsneg(s(N), cons(X, cons(Y, Z)))) -> mark(rcons(negrecip(Y), 2ndspos(N, Z))) active(pi(X)) -> mark(2ndspos(X, from(0))) active(plus(0, Y)) -> mark(Y) active(plus(s(X), Y)) -> mark(s(plus(X, Y))) active(times(0, Y)) -> mark(0) active(times(s(X), Y)) -> mark(plus(Y, times(X, Y))) active(square(X)) -> mark(times(X, X)) mark(from(X)) -> active(from(mark(X))) mark(cons(X1, X2)) -> active(cons(mark(X1), X2)) mark(s(X)) -> active(s(mark(X))) mark(2ndspos(X1, X2)) -> active(2ndspos(mark(X1), mark(X2))) mark(0) -> active(0) mark(rnil) -> active(rnil) mark(rcons(X1, X2)) -> active(rcons(mark(X1), mark(X2))) mark(posrecip(X)) -> active(posrecip(mark(X))) mark(2ndsneg(X1, X2)) -> active(2ndsneg(mark(X1), mark(X2))) mark(negrecip(X)) -> active(negrecip(mark(X))) mark(pi(X)) -> active(pi(mark(X))) mark(plus(X1, X2)) -> active(plus(mark(X1), mark(X2))) mark(times(X1, X2)) -> active(times(mark(X1), mark(X2))) mark(square(X)) -> active(square(mark(X))) from(mark(X)) -> from(X) from(active(X)) -> from(X) cons(mark(X1), X2) -> cons(X1, X2) cons(X1, mark(X2)) -> cons(X1, X2) cons(active(X1), X2) -> cons(X1, X2) cons(X1, active(X2)) -> cons(X1, X2) s(mark(X)) -> s(X) s(active(X)) -> s(X) 2ndspos(mark(X1), X2) -> 2ndspos(X1, X2) 2ndspos(X1, mark(X2)) -> 2ndspos(X1, X2) 2ndspos(active(X1), X2) -> 2ndspos(X1, X2) 2ndspos(X1, active(X2)) -> 2ndspos(X1, X2) rcons(mark(X1), X2) -> rcons(X1, X2) rcons(X1, mark(X2)) -> rcons(X1, X2) rcons(active(X1), X2) -> rcons(X1, X2) rcons(X1, active(X2)) -> rcons(X1, X2) posrecip(mark(X)) -> posrecip(X) posrecip(active(X)) -> posrecip(X) 2ndsneg(mark(X1), X2) -> 2ndsneg(X1, X2) 2ndsneg(X1, mark(X2)) -> 2ndsneg(X1, X2) 2ndsneg(active(X1), X2) -> 2ndsneg(X1, X2) 2ndsneg(X1, active(X2)) -> 2ndsneg(X1, X2) negrecip(mark(X)) -> negrecip(X) negrecip(active(X)) -> negrecip(X) pi(mark(X)) -> pi(X) pi(active(X)) -> pi(X) plus(mark(X1), X2) -> plus(X1, X2) plus(X1, mark(X2)) -> plus(X1, X2) plus(active(X1), X2) -> plus(X1, X2) plus(X1, active(X2)) -> plus(X1, X2) times(mark(X1), X2) -> times(X1, X2) times(X1, mark(X2)) -> times(X1, X2) times(active(X1), X2) -> times(X1, X2) times(X1, active(X2)) -> times(X1, X2) square(mark(X)) -> square(X) square(active(X)) -> square(X) Q is empty. We have to consider all minimal (P,Q,R)-chains. ---------------------------------------- (106) QDPOrderProof (EQUIVALENT) We use the reduction pair processor [LPAR04,JAR06]. The following pairs can be oriented strictly and are deleted. MARK(from(X)) -> ACTIVE(from(mark(X))) The remaining pairs can at least be oriented weakly. Used ordering: Polynomial Order [NEGPOLO,POLO] with Interpretation: POL( 2ndsneg_2(x_1, x_2) ) = max{0, -1} POL( ACTIVE_1(x_1) ) = x_1 POL( 2ndspos_2(x_1, x_2) ) = 0 POL( from_1(x_1) ) = x_1 + 2 POL( mark_1(x_1) ) = 2x_1 POL( active_1(x_1) ) = x_1 POL( cons_2(x_1, x_2) ) = max{0, -1} POL( s_1(x_1) ) = max{0, -1} POL( rcons_2(x_1, x_2) ) = 2x_1 + 2x_2 POL( posrecip_1(x_1) ) = 0 POL( negrecip_1(x_1) ) = 0 POL( pi_1(x_1) ) = max{0, -2} POL( 0 ) = 0 POL( plus_2(x_1, x_2) ) = 2x_2 POL( times_2(x_1, x_2) ) = 0 POL( square_1(x_1) ) = 1 POL( rnil ) = 0 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)) -> active(from(mark(X))) active(from(X)) -> mark(cons(X, from(s(X)))) mark(cons(X1, X2)) -> active(cons(mark(X1), X2)) active(2ndspos(s(N), cons(X, cons(Y, Z)))) -> mark(rcons(posrecip(Y), 2ndsneg(N, Z))) mark(s(X)) -> active(s(mark(X))) active(2ndsneg(s(N), cons(X, cons(Y, Z)))) -> mark(rcons(negrecip(Y), 2ndspos(N, Z))) mark(2ndspos(X1, X2)) -> active(2ndspos(mark(X1), mark(X2))) active(pi(X)) -> mark(2ndspos(X, from(0))) mark(rcons(X1, X2)) -> active(rcons(mark(X1), mark(X2))) active(plus(0, Y)) -> mark(Y) mark(posrecip(X)) -> active(posrecip(mark(X))) active(plus(s(X), Y)) -> mark(s(plus(X, Y))) mark(2ndsneg(X1, X2)) -> active(2ndsneg(mark(X1), mark(X2))) active(times(s(X), Y)) -> mark(plus(Y, times(X, Y))) mark(negrecip(X)) -> active(negrecip(mark(X))) active(square(X)) -> mark(times(X, X)) mark(pi(X)) -> active(pi(mark(X))) mark(plus(X1, X2)) -> active(plus(mark(X1), mark(X2))) mark(times(X1, X2)) -> active(times(mark(X1), mark(X2))) mark(square(X)) -> active(square(mark(X))) mark(0) -> active(0) mark(rnil) -> active(rnil) from(active(X)) -> from(X) from(mark(X)) -> from(X) posrecip(active(X)) -> posrecip(X) posrecip(mark(X)) -> posrecip(X) 2ndsneg(X1, mark(X2)) -> 2ndsneg(X1, X2) 2ndsneg(mark(X1), X2) -> 2ndsneg(X1, X2) 2ndsneg(active(X1), X2) -> 2ndsneg(X1, X2) 2ndsneg(X1, active(X2)) -> 2ndsneg(X1, X2) rcons(X1, mark(X2)) -> rcons(X1, X2) rcons(mark(X1), X2) -> rcons(X1, X2) rcons(active(X1), X2) -> rcons(X1, X2) rcons(X1, active(X2)) -> rcons(X1, X2) negrecip(active(X)) -> negrecip(X) negrecip(mark(X)) -> negrecip(X) 2ndspos(X1, mark(X2)) -> 2ndspos(X1, X2) 2ndspos(mark(X1), X2) -> 2ndspos(X1, X2) 2ndspos(active(X1), X2) -> 2ndspos(X1, X2) 2ndspos(X1, active(X2)) -> 2ndspos(X1, X2) active(2ndspos(0, Z)) -> mark(rnil) active(2ndsneg(0, Z)) -> mark(rnil) active(times(0, Y)) -> mark(0) s(active(X)) -> s(X) s(mark(X)) -> s(X) cons(X1, mark(X2)) -> cons(X1, X2) cons(mark(X1), X2) -> cons(X1, X2) cons(active(X1), X2) -> cons(X1, X2) cons(X1, active(X2)) -> cons(X1, X2) plus(X1, mark(X2)) -> plus(X1, X2) plus(mark(X1), X2) -> plus(X1, X2) plus(active(X1), X2) -> plus(X1, X2) plus(X1, active(X2)) -> plus(X1, X2) times(X1, mark(X2)) -> times(X1, X2) times(mark(X1), X2) -> times(X1, X2) times(active(X1), X2) -> times(X1, X2) times(X1, active(X2)) -> times(X1, X2) pi(active(X)) -> pi(X) pi(mark(X)) -> pi(X) square(active(X)) -> square(X) square(mark(X)) -> square(X) ---------------------------------------- (107) Obligation: Q DP problem: The TRS P consists of the following rules: ACTIVE(2ndspos(s(N), cons(X, cons(Y, Z)))) -> MARK(rcons(posrecip(Y), 2ndsneg(N, Z))) ACTIVE(2ndsneg(s(N), cons(X, cons(Y, Z)))) -> MARK(rcons(negrecip(Y), 2ndspos(N, Z))) MARK(2ndspos(X1, X2)) -> ACTIVE(2ndspos(mark(X1), mark(X2))) MARK(rcons(X1, X2)) -> MARK(X2) MARK(2ndsneg(X1, X2)) -> ACTIVE(2ndsneg(mark(X1), mark(X2))) The TRS R consists of the following rules: active(from(X)) -> mark(cons(X, from(s(X)))) active(2ndspos(0, Z)) -> mark(rnil) active(2ndspos(s(N), cons(X, cons(Y, Z)))) -> mark(rcons(posrecip(Y), 2ndsneg(N, Z))) active(2ndsneg(0, Z)) -> mark(rnil) active(2ndsneg(s(N), cons(X, cons(Y, Z)))) -> mark(rcons(negrecip(Y), 2ndspos(N, Z))) active(pi(X)) -> mark(2ndspos(X, from(0))) active(plus(0, Y)) -> mark(Y) active(plus(s(X), Y)) -> mark(s(plus(X, Y))) active(times(0, Y)) -> mark(0) active(times(s(X), Y)) -> mark(plus(Y, times(X, Y))) active(square(X)) -> mark(times(X, X)) mark(from(X)) -> active(from(mark(X))) mark(cons(X1, X2)) -> active(cons(mark(X1), X2)) mark(s(X)) -> active(s(mark(X))) mark(2ndspos(X1, X2)) -> active(2ndspos(mark(X1), mark(X2))) mark(0) -> active(0) mark(rnil) -> active(rnil) mark(rcons(X1, X2)) -> active(rcons(mark(X1), mark(X2))) mark(posrecip(X)) -> active(posrecip(mark(X))) mark(2ndsneg(X1, X2)) -> active(2ndsneg(mark(X1), mark(X2))) mark(negrecip(X)) -> active(negrecip(mark(X))) mark(pi(X)) -> active(pi(mark(X))) mark(plus(X1, X2)) -> active(plus(mark(X1), mark(X2))) mark(times(X1, X2)) -> active(times(mark(X1), mark(X2))) mark(square(X)) -> active(square(mark(X))) from(mark(X)) -> from(X) from(active(X)) -> from(X) cons(mark(X1), X2) -> cons(X1, X2) cons(X1, mark(X2)) -> cons(X1, X2) cons(active(X1), X2) -> cons(X1, X2) cons(X1, active(X2)) -> cons(X1, X2) s(mark(X)) -> s(X) s(active(X)) -> s(X) 2ndspos(mark(X1), X2) -> 2ndspos(X1, X2) 2ndspos(X1, mark(X2)) -> 2ndspos(X1, X2) 2ndspos(active(X1), X2) -> 2ndspos(X1, X2) 2ndspos(X1, active(X2)) -> 2ndspos(X1, X2) rcons(mark(X1), X2) -> rcons(X1, X2) rcons(X1, mark(X2)) -> rcons(X1, X2) rcons(active(X1), X2) -> rcons(X1, X2) rcons(X1, active(X2)) -> rcons(X1, X2) posrecip(mark(X)) -> posrecip(X) posrecip(active(X)) -> posrecip(X) 2ndsneg(mark(X1), X2) -> 2ndsneg(X1, X2) 2ndsneg(X1, mark(X2)) -> 2ndsneg(X1, X2) 2ndsneg(active(X1), X2) -> 2ndsneg(X1, X2) 2ndsneg(X1, active(X2)) -> 2ndsneg(X1, X2) negrecip(mark(X)) -> negrecip(X) negrecip(active(X)) -> negrecip(X) pi(mark(X)) -> pi(X) pi(active(X)) -> pi(X) plus(mark(X1), X2) -> plus(X1, X2) plus(X1, mark(X2)) -> plus(X1, X2) plus(active(X1), X2) -> plus(X1, X2) plus(X1, active(X2)) -> plus(X1, X2) times(mark(X1), X2) -> times(X1, X2) times(X1, mark(X2)) -> times(X1, X2) times(active(X1), X2) -> times(X1, X2) times(X1, active(X2)) -> times(X1, X2) square(mark(X)) -> square(X) square(active(X)) -> square(X) Q is empty. We have to consider all minimal (P,Q,R)-chains. ---------------------------------------- (108) QDPOrderProof (EQUIVALENT) We use the reduction pair processor [LPAR04,JAR06]. The following pairs can be oriented strictly and are deleted. ACTIVE(2ndspos(s(N), cons(X, cons(Y, Z)))) -> MARK(rcons(posrecip(Y), 2ndsneg(N, Z))) ACTIVE(2ndsneg(s(N), cons(X, cons(Y, Z)))) -> MARK(rcons(negrecip(Y), 2ndspos(N, Z))) MARK(2ndspos(X1, X2)) -> ACTIVE(2ndspos(mark(X1), mark(X2))) MARK(rcons(X1, X2)) -> MARK(X2) MARK(2ndsneg(X1, X2)) -> ACTIVE(2ndsneg(mark(X1), mark(X2))) The remaining pairs can at least be oriented weakly. Used ordering: Combined order from the following AFS and order. ACTIVE(x1) = ACTIVE(x1) 2ndspos(x1, x2) = x1 s(x1) = s(x1) cons(x1, x2) = x2 MARK(x1) = MARK(x1) rcons(x1, x2) = rcons(x1, x2) posrecip(x1) = posrecip 2ndsneg(x1, x2) = x1 negrecip(x1) = negrecip mark(x1) = x1 active(x1) = x1 from(x1) = from pi(x1) = pi(x1) 0 = 0 plus(x1, x2) = plus(x1, x2) times(x1, x2) = times(x1, x2) square(x1) = square(x1) rnil = rnil Recursive path order with status [RPO]. Quasi-Precedence: from > [s_1, negrecip] > MARK_1 > [ACTIVE_1, rcons_2, rnil] from > [s_1, negrecip] > posrecip > [ACTIVE_1, rcons_2, rnil] pi_1 > [ACTIVE_1, rcons_2, rnil] 0 > [ACTIVE_1, rcons_2, rnil] square_1 > times_2 > plus_2 > [s_1, negrecip] > MARK_1 > [ACTIVE_1, rcons_2, rnil] square_1 > times_2 > plus_2 > [s_1, negrecip] > posrecip > [ACTIVE_1, rcons_2, rnil] Status: ACTIVE_1: [1] s_1: [1] MARK_1: multiset status rcons_2: [1,2] posrecip: multiset status negrecip: [] from: [] pi_1: multiset status 0: multiset status plus_2: [2,1] times_2: [2,1] square_1: multiset status rnil: multiset status The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented: posrecip(active(X)) -> posrecip(X) posrecip(mark(X)) -> posrecip(X) 2ndsneg(X1, mark(X2)) -> 2ndsneg(X1, X2) 2ndsneg(mark(X1), X2) -> 2ndsneg(X1, X2) 2ndsneg(active(X1), X2) -> 2ndsneg(X1, X2) 2ndsneg(X1, active(X2)) -> 2ndsneg(X1, X2) rcons(X1, mark(X2)) -> rcons(X1, X2) rcons(mark(X1), X2) -> rcons(X1, X2) rcons(active(X1), X2) -> rcons(X1, X2) rcons(X1, active(X2)) -> rcons(X1, X2) negrecip(active(X)) -> negrecip(X) negrecip(mark(X)) -> negrecip(X) 2ndspos(X1, mark(X2)) -> 2ndspos(X1, X2) 2ndspos(mark(X1), X2) -> 2ndspos(X1, X2) 2ndspos(active(X1), X2) -> 2ndspos(X1, X2) 2ndspos(X1, active(X2)) -> 2ndspos(X1, X2) mark(from(X)) -> active(from(mark(X))) active(from(X)) -> mark(cons(X, from(s(X)))) mark(cons(X1, X2)) -> active(cons(mark(X1), X2)) active(2ndspos(s(N), cons(X, cons(Y, Z)))) -> mark(rcons(posrecip(Y), 2ndsneg(N, Z))) mark(s(X)) -> active(s(mark(X))) active(2ndsneg(s(N), cons(X, cons(Y, Z)))) -> mark(rcons(negrecip(Y), 2ndspos(N, Z))) mark(2ndspos(X1, X2)) -> active(2ndspos(mark(X1), mark(X2))) active(pi(X)) -> mark(2ndspos(X, from(0))) mark(rcons(X1, X2)) -> active(rcons(mark(X1), mark(X2))) active(plus(0, Y)) -> mark(Y) mark(posrecip(X)) -> active(posrecip(mark(X))) active(plus(s(X), Y)) -> mark(s(plus(X, Y))) mark(2ndsneg(X1, X2)) -> active(2ndsneg(mark(X1), mark(X2))) active(times(s(X), Y)) -> mark(plus(Y, times(X, Y))) mark(negrecip(X)) -> active(negrecip(mark(X))) active(square(X)) -> mark(times(X, X)) mark(pi(X)) -> active(pi(mark(X))) mark(plus(X1, X2)) -> active(plus(mark(X1), mark(X2))) mark(times(X1, X2)) -> active(times(mark(X1), mark(X2))) mark(square(X)) -> active(square(mark(X))) mark(0) -> active(0) mark(rnil) -> active(rnil) from(active(X)) -> from(X) from(mark(X)) -> from(X) active(2ndspos(0, Z)) -> mark(rnil) active(2ndsneg(0, Z)) -> mark(rnil) active(times(0, Y)) -> mark(0) s(active(X)) -> s(X) s(mark(X)) -> s(X) cons(X1, mark(X2)) -> cons(X1, X2) cons(mark(X1), X2) -> cons(X1, X2) cons(active(X1), X2) -> cons(X1, X2) cons(X1, active(X2)) -> cons(X1, X2) plus(X1, mark(X2)) -> plus(X1, X2) plus(mark(X1), X2) -> plus(X1, X2) plus(active(X1), X2) -> plus(X1, X2) plus(X1, active(X2)) -> plus(X1, X2) times(X1, mark(X2)) -> times(X1, X2) times(mark(X1), X2) -> times(X1, X2) times(active(X1), X2) -> times(X1, X2) times(X1, active(X2)) -> times(X1, X2) pi(active(X)) -> pi(X) pi(mark(X)) -> pi(X) square(active(X)) -> square(X) square(mark(X)) -> square(X) ---------------------------------------- (109) Obligation: Q DP problem: P is empty. The TRS R consists of the following rules: active(from(X)) -> mark(cons(X, from(s(X)))) active(2ndspos(0, Z)) -> mark(rnil) active(2ndspos(s(N), cons(X, cons(Y, Z)))) -> mark(rcons(posrecip(Y), 2ndsneg(N, Z))) active(2ndsneg(0, Z)) -> mark(rnil) active(2ndsneg(s(N), cons(X, cons(Y, Z)))) -> mark(rcons(negrecip(Y), 2ndspos(N, Z))) active(pi(X)) -> mark(2ndspos(X, from(0))) active(plus(0, Y)) -> mark(Y) active(plus(s(X), Y)) -> mark(s(plus(X, Y))) active(times(0, Y)) -> mark(0) active(times(s(X), Y)) -> mark(plus(Y, times(X, Y))) active(square(X)) -> mark(times(X, X)) mark(from(X)) -> active(from(mark(X))) mark(cons(X1, X2)) -> active(cons(mark(X1), X2)) mark(s(X)) -> active(s(mark(X))) mark(2ndspos(X1, X2)) -> active(2ndspos(mark(X1), mark(X2))) mark(0) -> active(0) mark(rnil) -> active(rnil) mark(rcons(X1, X2)) -> active(rcons(mark(X1), mark(X2))) mark(posrecip(X)) -> active(posrecip(mark(X))) mark(2ndsneg(X1, X2)) -> active(2ndsneg(mark(X1), mark(X2))) mark(negrecip(X)) -> active(negrecip(mark(X))) mark(pi(X)) -> active(pi(mark(X))) mark(plus(X1, X2)) -> active(plus(mark(X1), mark(X2))) mark(times(X1, X2)) -> active(times(mark(X1), mark(X2))) mark(square(X)) -> active(square(mark(X))) from(mark(X)) -> from(X) from(active(X)) -> from(X) cons(mark(X1), X2) -> cons(X1, X2) cons(X1, mark(X2)) -> cons(X1, X2) cons(active(X1), X2) -> cons(X1, X2) cons(X1, active(X2)) -> cons(X1, X2) s(mark(X)) -> s(X) s(active(X)) -> s(X) 2ndspos(mark(X1), X2) -> 2ndspos(X1, X2) 2ndspos(X1, mark(X2)) -> 2ndspos(X1, X2) 2ndspos(active(X1), X2) -> 2ndspos(X1, X2) 2ndspos(X1, active(X2)) -> 2ndspos(X1, X2) rcons(mark(X1), X2) -> rcons(X1, X2) rcons(X1, mark(X2)) -> rcons(X1, X2) rcons(active(X1), X2) -> rcons(X1, X2) rcons(X1, active(X2)) -> rcons(X1, X2) posrecip(mark(X)) -> posrecip(X) posrecip(active(X)) -> posrecip(X) 2ndsneg(mark(X1), X2) -> 2ndsneg(X1, X2) 2ndsneg(X1, mark(X2)) -> 2ndsneg(X1, X2) 2ndsneg(active(X1), X2) -> 2ndsneg(X1, X2) 2ndsneg(X1, active(X2)) -> 2ndsneg(X1, X2) negrecip(mark(X)) -> negrecip(X) negrecip(active(X)) -> negrecip(X) pi(mark(X)) -> pi(X) pi(active(X)) -> pi(X) plus(mark(X1), X2) -> plus(X1, X2) plus(X1, mark(X2)) -> plus(X1, X2) plus(active(X1), X2) -> plus(X1, X2) plus(X1, active(X2)) -> plus(X1, X2) times(mark(X1), X2) -> times(X1, X2) times(X1, mark(X2)) -> times(X1, X2) times(active(X1), X2) -> times(X1, X2) times(X1, active(X2)) -> times(X1, X2) square(mark(X)) -> square(X) square(active(X)) -> square(X) Q is empty. We have to consider all minimal (P,Q,R)-chains. ---------------------------------------- (110) PisEmptyProof (EQUIVALENT) The TRS P is empty. Hence, there is no (P,Q,R) chain. ---------------------------------------- (111) YES