YES proof of Transformed_CSR_04_Ex9_BLR02_FR.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, 0 ms] (2) QDP (3) DependencyGraphProof [EQUIVALENT, 0 ms] (4) QDP (5) QDPOrderProof [EQUIVALENT, 27 ms] (6) QDP (7) QDPOrderProof [EQUIVALENT, 26 ms] (8) QDP (9) DependencyGraphProof [EQUIVALENT, 0 ms] (10) QDP (11) QDPOrderProof [EQUIVALENT, 0 ms] (12) QDP (13) DependencyGraphProof [EQUIVALENT, 0 ms] (14) TRUE ---------------------------------------- (0) Obligation: Q restricted rewrite system: The TRS R consists of the following rules: filter(cons(X, Y), 0, M) -> cons(0, n__filter(activate(Y), M, M)) filter(cons(X, Y), s(N), M) -> cons(X, n__filter(activate(Y), N, M)) sieve(cons(0, Y)) -> cons(0, n__sieve(activate(Y))) sieve(cons(s(N), Y)) -> cons(s(N), n__sieve(n__filter(activate(Y), N, N))) nats(N) -> cons(N, n__nats(n__s(N))) zprimes -> sieve(nats(s(s(0)))) filter(X1, X2, X3) -> n__filter(X1, X2, X3) sieve(X) -> n__sieve(X) nats(X) -> n__nats(X) s(X) -> n__s(X) activate(n__filter(X1, X2, X3)) -> filter(activate(X1), activate(X2), activate(X3)) activate(n__sieve(X)) -> sieve(activate(X)) activate(n__nats(X)) -> nats(activate(X)) activate(n__s(X)) -> s(activate(X)) activate(X) -> 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: FILTER(cons(X, Y), 0, M) -> ACTIVATE(Y) FILTER(cons(X, Y), s(N), M) -> ACTIVATE(Y) SIEVE(cons(0, Y)) -> ACTIVATE(Y) SIEVE(cons(s(N), Y)) -> ACTIVATE(Y) ZPRIMES -> SIEVE(nats(s(s(0)))) ZPRIMES -> NATS(s(s(0))) ZPRIMES -> S(s(0)) ZPRIMES -> S(0) ACTIVATE(n__filter(X1, X2, X3)) -> FILTER(activate(X1), activate(X2), activate(X3)) ACTIVATE(n__filter(X1, X2, X3)) -> ACTIVATE(X1) ACTIVATE(n__filter(X1, X2, X3)) -> ACTIVATE(X2) ACTIVATE(n__filter(X1, X2, X3)) -> ACTIVATE(X3) ACTIVATE(n__sieve(X)) -> SIEVE(activate(X)) ACTIVATE(n__sieve(X)) -> ACTIVATE(X) ACTIVATE(n__nats(X)) -> NATS(activate(X)) ACTIVATE(n__nats(X)) -> ACTIVATE(X) ACTIVATE(n__s(X)) -> S(activate(X)) ACTIVATE(n__s(X)) -> ACTIVATE(X) The TRS R consists of the following rules: filter(cons(X, Y), 0, M) -> cons(0, n__filter(activate(Y), M, M)) filter(cons(X, Y), s(N), M) -> cons(X, n__filter(activate(Y), N, M)) sieve(cons(0, Y)) -> cons(0, n__sieve(activate(Y))) sieve(cons(s(N), Y)) -> cons(s(N), n__sieve(n__filter(activate(Y), N, N))) nats(N) -> cons(N, n__nats(n__s(N))) zprimes -> sieve(nats(s(s(0)))) filter(X1, X2, X3) -> n__filter(X1, X2, X3) sieve(X) -> n__sieve(X) nats(X) -> n__nats(X) s(X) -> n__s(X) activate(n__filter(X1, X2, X3)) -> filter(activate(X1), activate(X2), activate(X3)) activate(n__sieve(X)) -> sieve(activate(X)) activate(n__nats(X)) -> nats(activate(X)) activate(n__s(X)) -> s(activate(X)) activate(X) -> 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 1 SCC with 6 less nodes. ---------------------------------------- (4) Obligation: Q DP problem: The TRS P consists of the following rules: ACTIVATE(n__filter(X1, X2, X3)) -> FILTER(activate(X1), activate(X2), activate(X3)) FILTER(cons(X, Y), 0, M) -> ACTIVATE(Y) ACTIVATE(n__filter(X1, X2, X3)) -> ACTIVATE(X1) ACTIVATE(n__filter(X1, X2, X3)) -> ACTIVATE(X2) ACTIVATE(n__filter(X1, X2, X3)) -> ACTIVATE(X3) ACTIVATE(n__sieve(X)) -> SIEVE(activate(X)) SIEVE(cons(0, Y)) -> ACTIVATE(Y) ACTIVATE(n__sieve(X)) -> ACTIVATE(X) ACTIVATE(n__nats(X)) -> ACTIVATE(X) ACTIVATE(n__s(X)) -> ACTIVATE(X) SIEVE(cons(s(N), Y)) -> ACTIVATE(Y) FILTER(cons(X, Y), s(N), M) -> ACTIVATE(Y) The TRS R consists of the following rules: filter(cons(X, Y), 0, M) -> cons(0, n__filter(activate(Y), M, M)) filter(cons(X, Y), s(N), M) -> cons(X, n__filter(activate(Y), N, M)) sieve(cons(0, Y)) -> cons(0, n__sieve(activate(Y))) sieve(cons(s(N), Y)) -> cons(s(N), n__sieve(n__filter(activate(Y), N, N))) nats(N) -> cons(N, n__nats(n__s(N))) zprimes -> sieve(nats(s(s(0)))) filter(X1, X2, X3) -> n__filter(X1, X2, X3) sieve(X) -> n__sieve(X) nats(X) -> n__nats(X) s(X) -> n__s(X) activate(n__filter(X1, X2, X3)) -> filter(activate(X1), activate(X2), activate(X3)) activate(n__sieve(X)) -> sieve(activate(X)) activate(n__nats(X)) -> nats(activate(X)) activate(n__s(X)) -> s(activate(X)) activate(X) -> X Q is empty. We have to consider all minimal (P,Q,R)-chains. ---------------------------------------- (5) QDPOrderProof (EQUIVALENT) We use the reduction pair processor [LPAR04,JAR06]. The following pairs can be oriented strictly and are deleted. ACTIVATE(n__nats(X)) -> ACTIVATE(X) SIEVE(cons(s(N), Y)) -> ACTIVATE(Y) The remaining pairs can at least be oriented weakly. Used ordering: Matrix interpretation [MATRO] with arctic natural numbers [ARCTIC]: <<< POL(ACTIVATE(x_1)) = [[2A]] + [[0A]] * x_1 >>> <<< POL(n__filter(x_1, x_2, x_3)) = [[1A]] + [[0A]] * x_1 + [[1A]] * x_2 + [[1A]] * x_3 >>> <<< POL(FILTER(x_1, x_2, x_3)) = [[2A]] + [[0A]] * x_1 + [[1A]] * x_2 + [[-I]] * x_3 >>> <<< POL(activate(x_1)) = [[-I]] + [[0A]] * x_1 >>> <<< POL(cons(x_1, x_2)) = [[0A]] + [[1A]] * x_1 + [[0A]] * x_2 >>> <<< POL(0) = [[0A]] >>> <<< POL(n__sieve(x_1)) = [[2A]] + [[2A]] * x_1 >>> <<< POL(SIEVE(x_1)) = [[2A]] + [[1A]] * x_1 >>> <<< POL(n__nats(x_1)) = [[5A]] + [[1A]] * x_1 >>> <<< POL(n__s(x_1)) = [[4A]] + [[0A]] * x_1 >>> <<< POL(s(x_1)) = [[4A]] + [[0A]] * x_1 >>> <<< POL(filter(x_1, x_2, x_3)) = [[1A]] + [[0A]] * x_1 + [[1A]] * x_2 + [[1A]] * x_3 >>> <<< POL(sieve(x_1)) = [[2A]] + [[2A]] * x_1 >>> <<< POL(nats(x_1)) = [[5A]] + [[1A]] * x_1 >>> The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented: activate(n__filter(X1, X2, X3)) -> filter(activate(X1), activate(X2), activate(X3)) activate(n__sieve(X)) -> sieve(activate(X)) activate(n__nats(X)) -> nats(activate(X)) activate(n__s(X)) -> s(activate(X)) activate(X) -> X filter(X1, X2, X3) -> n__filter(X1, X2, X3) sieve(X) -> n__sieve(X) nats(N) -> cons(N, n__nats(n__s(N))) nats(X) -> n__nats(X) s(X) -> n__s(X) sieve(cons(0, Y)) -> cons(0, n__sieve(activate(Y))) sieve(cons(s(N), Y)) -> cons(s(N), n__sieve(n__filter(activate(Y), N, N))) filter(cons(X, Y), 0, M) -> cons(0, n__filter(activate(Y), M, M)) filter(cons(X, Y), s(N), M) -> cons(X, n__filter(activate(Y), N, M)) ---------------------------------------- (6) Obligation: Q DP problem: The TRS P consists of the following rules: ACTIVATE(n__filter(X1, X2, X3)) -> FILTER(activate(X1), activate(X2), activate(X3)) FILTER(cons(X, Y), 0, M) -> ACTIVATE(Y) ACTIVATE(n__filter(X1, X2, X3)) -> ACTIVATE(X1) ACTIVATE(n__filter(X1, X2, X3)) -> ACTIVATE(X2) ACTIVATE(n__filter(X1, X2, X3)) -> ACTIVATE(X3) ACTIVATE(n__sieve(X)) -> SIEVE(activate(X)) SIEVE(cons(0, Y)) -> ACTIVATE(Y) ACTIVATE(n__sieve(X)) -> ACTIVATE(X) ACTIVATE(n__s(X)) -> ACTIVATE(X) FILTER(cons(X, Y), s(N), M) -> ACTIVATE(Y) The TRS R consists of the following rules: filter(cons(X, Y), 0, M) -> cons(0, n__filter(activate(Y), M, M)) filter(cons(X, Y), s(N), M) -> cons(X, n__filter(activate(Y), N, M)) sieve(cons(0, Y)) -> cons(0, n__sieve(activate(Y))) sieve(cons(s(N), Y)) -> cons(s(N), n__sieve(n__filter(activate(Y), N, N))) nats(N) -> cons(N, n__nats(n__s(N))) zprimes -> sieve(nats(s(s(0)))) filter(X1, X2, X3) -> n__filter(X1, X2, X3) sieve(X) -> n__sieve(X) nats(X) -> n__nats(X) s(X) -> n__s(X) activate(n__filter(X1, X2, X3)) -> filter(activate(X1), activate(X2), activate(X3)) activate(n__sieve(X)) -> sieve(activate(X)) activate(n__nats(X)) -> nats(activate(X)) activate(n__s(X)) -> s(activate(X)) activate(X) -> X Q is empty. We have to consider all minimal (P,Q,R)-chains. ---------------------------------------- (7) QDPOrderProof (EQUIVALENT) We use the reduction pair processor [LPAR04,JAR06]. The following pairs can be oriented strictly and are deleted. ACTIVATE(n__sieve(X)) -> SIEVE(activate(X)) ACTIVATE(n__sieve(X)) -> ACTIVATE(X) The remaining pairs can at least be oriented weakly. Used ordering: Matrix interpretation [MATRO] with arctic natural numbers [ARCTIC]: <<< POL(ACTIVATE(x_1)) = [[5A]] + [[2A]] * x_1 >>> <<< POL(n__filter(x_1, x_2, x_3)) = [[1A]] + [[0A]] * x_1 + [[2A]] * x_2 + [[2A]] * x_3 >>> <<< POL(FILTER(x_1, x_2, x_3)) = [[5A]] + [[2A]] * x_1 + [[-I]] * x_2 + [[-I]] * x_3 >>> <<< POL(activate(x_1)) = [[-I]] + [[0A]] * x_1 >>> <<< POL(cons(x_1, x_2)) = [[-I]] + [[2A]] * x_1 + [[0A]] * x_2 >>> <<< POL(0) = [[0A]] >>> <<< POL(n__sieve(x_1)) = [[5A]] + [[4A]] * x_1 >>> <<< POL(SIEVE(x_1)) = [[5A]] + [[2A]] * x_1 >>> <<< POL(n__s(x_1)) = [[-I]] + [[0A]] * x_1 >>> <<< POL(s(x_1)) = [[-I]] + [[0A]] * x_1 >>> <<< POL(filter(x_1, x_2, x_3)) = [[1A]] + [[0A]] * x_1 + [[2A]] * x_2 + [[2A]] * x_3 >>> <<< POL(sieve(x_1)) = [[5A]] + [[4A]] * x_1 >>> <<< POL(n__nats(x_1)) = [[-I]] + [[3A]] * x_1 >>> <<< POL(nats(x_1)) = [[-I]] + [[3A]] * x_1 >>> The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented: activate(n__filter(X1, X2, X3)) -> filter(activate(X1), activate(X2), activate(X3)) activate(n__sieve(X)) -> sieve(activate(X)) activate(n__nats(X)) -> nats(activate(X)) activate(n__s(X)) -> s(activate(X)) activate(X) -> X filter(X1, X2, X3) -> n__filter(X1, X2, X3) sieve(X) -> n__sieve(X) nats(N) -> cons(N, n__nats(n__s(N))) nats(X) -> n__nats(X) s(X) -> n__s(X) sieve(cons(0, Y)) -> cons(0, n__sieve(activate(Y))) sieve(cons(s(N), Y)) -> cons(s(N), n__sieve(n__filter(activate(Y), N, N))) filter(cons(X, Y), 0, M) -> cons(0, n__filter(activate(Y), M, M)) filter(cons(X, Y), s(N), M) -> cons(X, n__filter(activate(Y), N, M)) ---------------------------------------- (8) Obligation: Q DP problem: The TRS P consists of the following rules: ACTIVATE(n__filter(X1, X2, X3)) -> FILTER(activate(X1), activate(X2), activate(X3)) FILTER(cons(X, Y), 0, M) -> ACTIVATE(Y) ACTIVATE(n__filter(X1, X2, X3)) -> ACTIVATE(X1) ACTIVATE(n__filter(X1, X2, X3)) -> ACTIVATE(X2) ACTIVATE(n__filter(X1, X2, X3)) -> ACTIVATE(X3) SIEVE(cons(0, Y)) -> ACTIVATE(Y) ACTIVATE(n__s(X)) -> ACTIVATE(X) FILTER(cons(X, Y), s(N), M) -> ACTIVATE(Y) The TRS R consists of the following rules: filter(cons(X, Y), 0, M) -> cons(0, n__filter(activate(Y), M, M)) filter(cons(X, Y), s(N), M) -> cons(X, n__filter(activate(Y), N, M)) sieve(cons(0, Y)) -> cons(0, n__sieve(activate(Y))) sieve(cons(s(N), Y)) -> cons(s(N), n__sieve(n__filter(activate(Y), N, N))) nats(N) -> cons(N, n__nats(n__s(N))) zprimes -> sieve(nats(s(s(0)))) filter(X1, X2, X3) -> n__filter(X1, X2, X3) sieve(X) -> n__sieve(X) nats(X) -> n__nats(X) s(X) -> n__s(X) activate(n__filter(X1, X2, X3)) -> filter(activate(X1), activate(X2), activate(X3)) activate(n__sieve(X)) -> sieve(activate(X)) activate(n__nats(X)) -> nats(activate(X)) activate(n__s(X)) -> s(activate(X)) activate(X) -> X Q is empty. We have to consider all minimal (P,Q,R)-chains. ---------------------------------------- (9) DependencyGraphProof (EQUIVALENT) The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node. ---------------------------------------- (10) Obligation: Q DP problem: The TRS P consists of the following rules: FILTER(cons(X, Y), 0, M) -> ACTIVATE(Y) ACTIVATE(n__filter(X1, X2, X3)) -> FILTER(activate(X1), activate(X2), activate(X3)) FILTER(cons(X, Y), s(N), M) -> ACTIVATE(Y) ACTIVATE(n__filter(X1, X2, X3)) -> ACTIVATE(X1) ACTIVATE(n__filter(X1, X2, X3)) -> ACTIVATE(X2) ACTIVATE(n__filter(X1, X2, X3)) -> ACTIVATE(X3) ACTIVATE(n__s(X)) -> ACTIVATE(X) The TRS R consists of the following rules: filter(cons(X, Y), 0, M) -> cons(0, n__filter(activate(Y), M, M)) filter(cons(X, Y), s(N), M) -> cons(X, n__filter(activate(Y), N, M)) sieve(cons(0, Y)) -> cons(0, n__sieve(activate(Y))) sieve(cons(s(N), Y)) -> cons(s(N), n__sieve(n__filter(activate(Y), N, N))) nats(N) -> cons(N, n__nats(n__s(N))) zprimes -> sieve(nats(s(s(0)))) filter(X1, X2, X3) -> n__filter(X1, X2, X3) sieve(X) -> n__sieve(X) nats(X) -> n__nats(X) s(X) -> n__s(X) activate(n__filter(X1, X2, X3)) -> filter(activate(X1), activate(X2), activate(X3)) activate(n__sieve(X)) -> sieve(activate(X)) activate(n__nats(X)) -> nats(activate(X)) activate(n__s(X)) -> s(activate(X)) activate(X) -> X Q is empty. We have to consider all minimal (P,Q,R)-chains. ---------------------------------------- (11) QDPOrderProof (EQUIVALENT) We use the reduction pair processor [LPAR04,JAR06]. The following pairs can be oriented strictly and are deleted. ACTIVATE(n__filter(X1, X2, X3)) -> FILTER(activate(X1), activate(X2), activate(X3)) FILTER(cons(X, Y), s(N), M) -> ACTIVATE(Y) ACTIVATE(n__filter(X1, X2, X3)) -> ACTIVATE(X1) ACTIVATE(n__filter(X1, X2, X3)) -> ACTIVATE(X2) ACTIVATE(n__filter(X1, X2, X3)) -> ACTIVATE(X3) ACTIVATE(n__s(X)) -> ACTIVATE(X) The remaining pairs can at least be oriented weakly. Used ordering: Polynomial interpretation [POLO,RATPOLO]: POL(0) = 0 POL(ACTIVATE(x_1)) = [1/2]x_1 POL(FILTER(x_1, x_2, x_3)) = x_1 + [1/4]x_2 + [1/4]x_3 POL(activate(x_1)) = x_1 POL(cons(x_1, x_2)) = [1/2]x_2 POL(filter(x_1, x_2, x_3)) = [1] + [2]x_1 + x_2 + x_3 POL(n__filter(x_1, x_2, x_3)) = [1] + [2]x_1 + x_2 + x_3 POL(n__nats(x_1)) = 0 POL(n__s(x_1)) = [1/4] + x_1 POL(n__sieve(x_1)) = 0 POL(nats(x_1)) = 0 POL(s(x_1)) = [1/4] + x_1 POL(sieve(x_1)) = 0 The value of delta used in the strict ordering is 1/16. The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented: activate(n__filter(X1, X2, X3)) -> filter(activate(X1), activate(X2), activate(X3)) activate(n__sieve(X)) -> sieve(activate(X)) activate(n__nats(X)) -> nats(activate(X)) activate(n__s(X)) -> s(activate(X)) activate(X) -> X filter(X1, X2, X3) -> n__filter(X1, X2, X3) sieve(X) -> n__sieve(X) nats(N) -> cons(N, n__nats(n__s(N))) nats(X) -> n__nats(X) s(X) -> n__s(X) sieve(cons(0, Y)) -> cons(0, n__sieve(activate(Y))) sieve(cons(s(N), Y)) -> cons(s(N), n__sieve(n__filter(activate(Y), N, N))) filter(cons(X, Y), 0, M) -> cons(0, n__filter(activate(Y), M, M)) filter(cons(X, Y), s(N), M) -> cons(X, n__filter(activate(Y), N, M)) ---------------------------------------- (12) Obligation: Q DP problem: The TRS P consists of the following rules: FILTER(cons(X, Y), 0, M) -> ACTIVATE(Y) The TRS R consists of the following rules: filter(cons(X, Y), 0, M) -> cons(0, n__filter(activate(Y), M, M)) filter(cons(X, Y), s(N), M) -> cons(X, n__filter(activate(Y), N, M)) sieve(cons(0, Y)) -> cons(0, n__sieve(activate(Y))) sieve(cons(s(N), Y)) -> cons(s(N), n__sieve(n__filter(activate(Y), N, N))) nats(N) -> cons(N, n__nats(n__s(N))) zprimes -> sieve(nats(s(s(0)))) filter(X1, X2, X3) -> n__filter(X1, X2, X3) sieve(X) -> n__sieve(X) nats(X) -> n__nats(X) s(X) -> n__s(X) activate(n__filter(X1, X2, X3)) -> filter(activate(X1), activate(X2), activate(X3)) activate(n__sieve(X)) -> sieve(activate(X)) activate(n__nats(X)) -> nats(activate(X)) activate(n__s(X)) -> s(activate(X)) activate(X) -> X Q is empty. We have to consider all minimal (P,Q,R)-chains. ---------------------------------------- (13) DependencyGraphProof (EQUIVALENT) The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 1 less node. ---------------------------------------- (14) TRUE