KILLED proof of input_IYOLP2l1gx.trs # AProVE Commit ID: aff8ecad908e01718a4c36e68d2e55d5e0f16e15 fuhs 20220216 unpublished The Runtime Complexity (parallel-innermost) of the given CpxTRS could be proven to be BOUNDS(1, INF). (0) CpxTRS (1) RenamingProof [BOTH BOUNDS(ID, ID), 0 ms] (2) CpxTRS (3) RelTrsToTrsProof [UPPER BOUND(ID), 0 ms] (4) CpxTRS (5) RelTrsToWeightedTrsProof [UPPER BOUND(ID), 0 ms] (6) CpxWeightedTrs (7) TypeInferenceProof [BOTH BOUNDS(ID, ID), 0 ms] (8) CpxTypedWeightedTrs (9) CompletionProof [UPPER BOUND(ID), 0 ms] (10) CpxTypedWeightedCompleteTrs (11) NarrowingProof [BOTH BOUNDS(ID, ID), 0 ms] (12) CpxTypedWeightedCompleteTrs (13) CpxTypedWeightedTrsToRntsProof [UPPER BOUND(ID), 0 ms] (14) CpxRNTS (15) SimplificationProof [BOTH BOUNDS(ID, ID), 0 ms] (16) CpxRNTS (17) CpxRntsAnalysisOrderProof [BOTH BOUNDS(ID, ID), 0 ms] (18) CpxRNTS (19) ResultPropagationProof [UPPER BOUND(ID), 0 ms] (20) CpxRNTS (21) IntTrsBoundProof [UPPER BOUND(ID), 407 ms] (22) CpxRNTS (23) IntTrsBoundProof [UPPER BOUND(ID), 141 ms] (24) CpxRNTS (25) ResultPropagationProof [UPPER BOUND(ID), 0 ms] (26) CpxRNTS (27) IntTrsBoundProof [UPPER BOUND(ID), 832 ms] (28) CpxRNTS (29) IntTrsBoundProof [UPPER BOUND(ID), 164 ms] (30) CpxRNTS (31) CompletionProof [UPPER BOUND(ID), 0 ms] (32) CpxTypedWeightedCompleteTrs (33) CpxTypedWeightedTrsToRntsProof [UPPER BOUND(ID), 0 ms] (34) CpxRNTS (35) CpxTrsToCdtProof [UPPER BOUND(ID), 0 ms] (36) CdtProblem (37) CdtGraphSplitRhsProof [BOTH BOUNDS(ID, ID), 0 ms] (38) CdtProblem (39) CdtLeafRemovalProof [ComplexityIfPolyImplication, 0 ms] (40) CdtProblem (41) CdtKnowledgeProof [BOTH BOUNDS(ID, ID), 0 ms] (42) CdtProblem (43) CdtUsableRulesProof [BOTH BOUNDS(ID, ID), 0 ms] (44) CdtProblem (45) CdtNarrowingProof [BOTH BOUNDS(ID, ID), 0 ms] (46) CdtProblem (47) CdtNarrowingProof [BOTH BOUNDS(ID, ID), 0 ms] (48) CdtProblem (49) CdtNarrowingProof [BOTH BOUNDS(ID, ID), 0 ms] (50) CdtProblem (51) CdtInstantiationProof [BOTH BOUNDS(ID, ID), 0 ms] (52) CdtProblem (53) CdtRewritingProof [BOTH BOUNDS(ID, ID), 0 ms] (54) CdtProblem (55) CdtInstantiationProof [BOTH BOUNDS(ID, ID), 0 ms] (56) CdtProblem (57) CdtRewritingProof [BOTH BOUNDS(ID, ID), 0 ms] (58) CdtProblem (59) CdtForwardInstantiationProof [BOTH BOUNDS(ID, ID), 0 ms] (60) CdtProblem (61) CdtForwardInstantiationProof [BOTH BOUNDS(ID, ID), 0 ms] (62) CdtProblem (63) CdtForwardInstantiationProof [BOTH BOUNDS(ID, ID), 0 ms] (64) CdtProblem (65) CdtNarrowingProof [BOTH BOUNDS(ID, ID), 0 ms] (66) CdtProblem (67) CdtRuleRemovalProof [UPPER BOUND(ADD(n^1)), 18 ms] (68) CdtProblem (69) CdtNarrowingProof [BOTH BOUNDS(ID, ID), 0 ms] (70) CdtProblem (71) CdtRuleRemovalProof [UPPER BOUND(ADD(n^1)), 27 ms] (72) CdtProblem (73) CdtForwardInstantiationProof [BOTH BOUNDS(ID, ID), 0 ms] (74) CdtProblem (75) CdtForwardInstantiationProof [BOTH BOUNDS(ID, ID), 0 ms] (76) CdtProblem (77) CdtForwardInstantiationProof [BOTH BOUNDS(ID, ID), 0 ms] (78) CdtProblem (79) CdtForwardInstantiationProof [BOTH BOUNDS(ID, ID), 0 ms] (80) CdtProblem (81) CdtForwardInstantiationProof [BOTH BOUNDS(ID, ID), 0 ms] (82) CdtProblem (83) CdtForwardInstantiationProof [BOTH BOUNDS(ID, ID), 0 ms] (84) CdtProblem (85) CdtForwardInstantiationProof [BOTH BOUNDS(ID, ID), 0 ms] (86) CdtProblem (87) CdtForwardInstantiationProof [BOTH BOUNDS(ID, ID), 0 ms] (88) CdtProblem (89) CdtForwardInstantiationProof [BOTH BOUNDS(ID, ID), 0 ms] (90) CdtProblem (91) CdtForwardInstantiationProof [BOTH BOUNDS(ID, ID), 0 ms] (92) CdtProblem (93) CdtRuleRemovalProof [UPPER BOUND(ADD(n^2)), 44.0 s] (94) CdtProblem ---------------------------------------- (0) Obligation: The Runtime Complexity (parallel-innermost) of the given CpxTRS could be proven to be BOUNDS(1, INF). The TRS R consists of the following rules: filter(cons(X, Y), 0, M) -> cons(0, filter(Y, M, M)) filter(cons(X, Y), s(N), M) -> cons(X, filter(Y, N, M)) sieve(cons(0, Y)) -> cons(0, sieve(Y)) sieve(cons(s(N), Y)) -> cons(s(N), sieve(filter(Y, N, N))) nats(N) -> cons(N, nats(s(N))) zprimes -> sieve(nats(s(s(0)))) S is empty. Rewrite Strategy: PARALLEL_INNERMOST ---------------------------------------- (1) RenamingProof (BOTH BOUNDS(ID, ID)) Renamed function symbols to avoid clashes with predefined symbol. ---------------------------------------- (2) Obligation: The Runtime Complexity (parallel-innermost) of the given CpxTRS could be proven to be BOUNDS(1, INF). The TRS R consists of the following rules: filter(cons(X, Y), 0', M) -> cons(0', filter(Y, M, M)) filter(cons(X, Y), s(N), M) -> cons(X, filter(Y, N, M)) sieve(cons(0', Y)) -> cons(0', sieve(Y)) sieve(cons(s(N), Y)) -> cons(s(N), sieve(filter(Y, N, N))) nats(N) -> cons(N, nats(s(N))) zprimes -> sieve(nats(s(s(0')))) S is empty. Rewrite Strategy: PARALLEL_INNERMOST ---------------------------------------- (3) RelTrsToTrsProof (UPPER BOUND(ID)) transformed relative TRS to TRS ---------------------------------------- (4) Obligation: The Runtime Complexity (parallel-innermost) of the given CpxTRS could be proven to be BOUNDS(1, INF). The TRS R consists of the following rules: filter(cons(X, Y), 0, M) -> cons(0, filter(Y, M, M)) filter(cons(X, Y), s(N), M) -> cons(X, filter(Y, N, M)) sieve(cons(0, Y)) -> cons(0, sieve(Y)) sieve(cons(s(N), Y)) -> cons(s(N), sieve(filter(Y, N, N))) nats(N) -> cons(N, nats(s(N))) zprimes -> sieve(nats(s(s(0)))) S is empty. Rewrite Strategy: PARALLEL_INNERMOST ---------------------------------------- (5) RelTrsToWeightedTrsProof (UPPER BOUND(ID)) Transformed relative TRS to weighted TRS ---------------------------------------- (6) Obligation: The Runtime Complexity (innermost) of the given CpxWeightedTrs could be proven to be BOUNDS(1, INF). The TRS R consists of the following rules: filter(cons(X, Y), 0, M) -> cons(0, filter(Y, M, M)) [1] filter(cons(X, Y), s(N), M) -> cons(X, filter(Y, N, M)) [1] sieve(cons(0, Y)) -> cons(0, sieve(Y)) [1] sieve(cons(s(N), Y)) -> cons(s(N), sieve(filter(Y, N, N))) [1] nats(N) -> cons(N, nats(s(N))) [1] zprimes -> sieve(nats(s(s(0)))) [1] Rewrite Strategy: INNERMOST ---------------------------------------- (7) TypeInferenceProof (BOTH BOUNDS(ID, ID)) Infered types. ---------------------------------------- (8) Obligation: Runtime Complexity Weighted TRS with Types. The TRS R consists of the following rules: filter(cons(X, Y), 0, M) -> cons(0, filter(Y, M, M)) [1] filter(cons(X, Y), s(N), M) -> cons(X, filter(Y, N, M)) [1] sieve(cons(0, Y)) -> cons(0, sieve(Y)) [1] sieve(cons(s(N), Y)) -> cons(s(N), sieve(filter(Y, N, N))) [1] nats(N) -> cons(N, nats(s(N))) [1] zprimes -> sieve(nats(s(s(0)))) [1] The TRS has the following type information: filter :: cons -> 0:s -> 0:s -> cons cons :: 0:s -> cons -> cons 0 :: 0:s s :: 0:s -> 0:s sieve :: cons -> cons nats :: 0:s -> cons zprimes :: cons Rewrite Strategy: INNERMOST ---------------------------------------- (9) CompletionProof (UPPER BOUND(ID)) The transformation into a RNTS is sound, since: (a) The obligation is a constructor system where every type has a constant constructor, (b) The following defined symbols do not have to be completely defined, as they can never occur inside other defined symbols: sieve_1 zprimes (c) The following functions are completely defined: filter_3 nats_1 Due to the following rules being added: filter(v0, v1, v2) -> const [0] And the following fresh constants: const ---------------------------------------- (10) Obligation: Runtime Complexity Weighted TRS where critical functions are completely defined. The underlying TRS is: Runtime Complexity Weighted TRS with Types. The TRS R consists of the following rules: filter(cons(X, Y), 0, M) -> cons(0, filter(Y, M, M)) [1] filter(cons(X, Y), s(N), M) -> cons(X, filter(Y, N, M)) [1] sieve(cons(0, Y)) -> cons(0, sieve(Y)) [1] sieve(cons(s(N), Y)) -> cons(s(N), sieve(filter(Y, N, N))) [1] nats(N) -> cons(N, nats(s(N))) [1] zprimes -> sieve(nats(s(s(0)))) [1] filter(v0, v1, v2) -> const [0] The TRS has the following type information: filter :: cons:const -> 0:s -> 0:s -> cons:const cons :: 0:s -> cons:const -> cons:const 0 :: 0:s s :: 0:s -> 0:s sieve :: cons:const -> cons:const nats :: 0:s -> cons:const zprimes :: cons:const const :: cons:const Rewrite Strategy: INNERMOST ---------------------------------------- (11) NarrowingProof (BOTH BOUNDS(ID, ID)) Narrowed the inner basic terms of all right-hand sides by a single narrowing step. ---------------------------------------- (12) Obligation: Runtime Complexity Weighted TRS where critical functions are completely defined. The underlying TRS is: Runtime Complexity Weighted TRS with Types. The TRS R consists of the following rules: filter(cons(X, Y), 0, M) -> cons(0, filter(Y, M, M)) [1] filter(cons(X, Y), s(N), M) -> cons(X, filter(Y, N, M)) [1] sieve(cons(0, Y)) -> cons(0, sieve(Y)) [1] sieve(cons(s(0), cons(X', Y'))) -> cons(s(0), sieve(cons(0, filter(Y', 0, 0)))) [2] sieve(cons(s(s(N')), cons(X'', Y''))) -> cons(s(s(N')), sieve(cons(X'', filter(Y'', N', s(N'))))) [2] sieve(cons(s(N), Y)) -> cons(s(N), sieve(const)) [1] nats(N) -> cons(N, nats(s(N))) [1] zprimes -> sieve(cons(s(s(0)), nats(s(s(s(0)))))) [2] filter(v0, v1, v2) -> const [0] The TRS has the following type information: filter :: cons:const -> 0:s -> 0:s -> cons:const cons :: 0:s -> cons:const -> cons:const 0 :: 0:s s :: 0:s -> 0:s sieve :: cons:const -> cons:const nats :: 0:s -> cons:const zprimes :: cons:const const :: cons:const Rewrite Strategy: INNERMOST ---------------------------------------- (13) CpxTypedWeightedTrsToRntsProof (UPPER BOUND(ID)) Transformed the TRS into an over-approximating RNTS by (improved) Size Abstraction. The constant constructors are abstracted as follows: 0 => 0 const => 0 ---------------------------------------- (14) Obligation: Complexity RNTS consisting of the following rules: filter(z, z', z'') -{ 0 }-> 0 :|: v0 >= 0, z'' = v2, v1 >= 0, z = v0, z' = v1, v2 >= 0 filter(z, z', z'') -{ 1 }-> 1 + X + filter(Y, N, M) :|: z' = 1 + N, Y >= 0, z = 1 + X + Y, X >= 0, M >= 0, z'' = M, N >= 0 filter(z, z', z'') -{ 1 }-> 1 + 0 + filter(Y, M, M) :|: Y >= 0, z = 1 + X + Y, X >= 0, M >= 0, z' = 0, z'' = M nats(z) -{ 1 }-> 1 + N + nats(1 + N) :|: z = N, N >= 0 sieve(z) -{ 1 }-> 1 + 0 + sieve(Y) :|: Y >= 0, z = 1 + 0 + Y sieve(z) -{ 1 }-> 1 + (1 + N) + sieve(0) :|: Y >= 0, z = 1 + (1 + N) + Y, N >= 0 sieve(z) -{ 2 }-> 1 + (1 + 0) + sieve(1 + 0 + filter(Y', 0, 0)) :|: Y' >= 0, z = 1 + (1 + 0) + (1 + X' + Y'), X' >= 0 sieve(z) -{ 2 }-> 1 + (1 + (1 + N')) + sieve(1 + X'' + filter(Y'', N', 1 + N')) :|: Y'' >= 0, N' >= 0, X'' >= 0, z = 1 + (1 + (1 + N')) + (1 + X'' + Y'') zprimes -{ 2 }-> sieve(1 + (1 + (1 + 0)) + nats(1 + (1 + (1 + 0)))) :|: ---------------------------------------- (15) SimplificationProof (BOTH BOUNDS(ID, ID)) Simplified the RNTS by moving equalities from the constraints into the right-hand sides. ---------------------------------------- (16) Obligation: Complexity RNTS consisting of the following rules: filter(z, z', z'') -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0 filter(z, z', z'') -{ 1 }-> 1 + X + filter(Y, z' - 1, z'') :|: Y >= 0, z = 1 + X + Y, X >= 0, z'' >= 0, z' - 1 >= 0 filter(z, z', z'') -{ 1 }-> 1 + 0 + filter(Y, z'', z'') :|: Y >= 0, z = 1 + X + Y, X >= 0, z'' >= 0, z' = 0 nats(z) -{ 1 }-> 1 + z + nats(1 + z) :|: z >= 0 sieve(z) -{ 1 }-> 1 + 0 + sieve(z - 1) :|: z - 1 >= 0 sieve(z) -{ 1 }-> 1 + (1 + N) + sieve(0) :|: Y >= 0, z = 1 + (1 + N) + Y, N >= 0 sieve(z) -{ 2 }-> 1 + (1 + 0) + sieve(1 + 0 + filter(Y', 0, 0)) :|: Y' >= 0, z = 1 + (1 + 0) + (1 + X' + Y'), X' >= 0 sieve(z) -{ 2 }-> 1 + (1 + (1 + N')) + sieve(1 + X'' + filter(Y'', N', 1 + N')) :|: Y'' >= 0, N' >= 0, X'' >= 0, z = 1 + (1 + (1 + N')) + (1 + X'' + Y'') zprimes -{ 2 }-> sieve(1 + (1 + (1 + 0)) + nats(1 + (1 + (1 + 0)))) :|: ---------------------------------------- (17) CpxRntsAnalysisOrderProof (BOTH BOUNDS(ID, ID)) Found the following analysis order by SCC decomposition: { filter } { nats } { sieve } { zprimes } ---------------------------------------- (18) Obligation: Complexity RNTS consisting of the following rules: filter(z, z', z'') -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0 filter(z, z', z'') -{ 1 }-> 1 + X + filter(Y, z' - 1, z'') :|: Y >= 0, z = 1 + X + Y, X >= 0, z'' >= 0, z' - 1 >= 0 filter(z, z', z'') -{ 1 }-> 1 + 0 + filter(Y, z'', z'') :|: Y >= 0, z = 1 + X + Y, X >= 0, z'' >= 0, z' = 0 nats(z) -{ 1 }-> 1 + z + nats(1 + z) :|: z >= 0 sieve(z) -{ 1 }-> 1 + 0 + sieve(z - 1) :|: z - 1 >= 0 sieve(z) -{ 1 }-> 1 + (1 + N) + sieve(0) :|: Y >= 0, z = 1 + (1 + N) + Y, N >= 0 sieve(z) -{ 2 }-> 1 + (1 + 0) + sieve(1 + 0 + filter(Y', 0, 0)) :|: Y' >= 0, z = 1 + (1 + 0) + (1 + X' + Y'), X' >= 0 sieve(z) -{ 2 }-> 1 + (1 + (1 + N')) + sieve(1 + X'' + filter(Y'', N', 1 + N')) :|: Y'' >= 0, N' >= 0, X'' >= 0, z = 1 + (1 + (1 + N')) + (1 + X'' + Y'') zprimes -{ 2 }-> sieve(1 + (1 + (1 + 0)) + nats(1 + (1 + (1 + 0)))) :|: Function symbols to be analyzed: {filter}, {nats}, {sieve}, {zprimes} ---------------------------------------- (19) ResultPropagationProof (UPPER BOUND(ID)) Applied inner abstraction using the recently inferred runtime/size bounds where possible. ---------------------------------------- (20) Obligation: Complexity RNTS consisting of the following rules: filter(z, z', z'') -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0 filter(z, z', z'') -{ 1 }-> 1 + X + filter(Y, z' - 1, z'') :|: Y >= 0, z = 1 + X + Y, X >= 0, z'' >= 0, z' - 1 >= 0 filter(z, z', z'') -{ 1 }-> 1 + 0 + filter(Y, z'', z'') :|: Y >= 0, z = 1 + X + Y, X >= 0, z'' >= 0, z' = 0 nats(z) -{ 1 }-> 1 + z + nats(1 + z) :|: z >= 0 sieve(z) -{ 1 }-> 1 + 0 + sieve(z - 1) :|: z - 1 >= 0 sieve(z) -{ 1 }-> 1 + (1 + N) + sieve(0) :|: Y >= 0, z = 1 + (1 + N) + Y, N >= 0 sieve(z) -{ 2 }-> 1 + (1 + 0) + sieve(1 + 0 + filter(Y', 0, 0)) :|: Y' >= 0, z = 1 + (1 + 0) + (1 + X' + Y'), X' >= 0 sieve(z) -{ 2 }-> 1 + (1 + (1 + N')) + sieve(1 + X'' + filter(Y'', N', 1 + N')) :|: Y'' >= 0, N' >= 0, X'' >= 0, z = 1 + (1 + (1 + N')) + (1 + X'' + Y'') zprimes -{ 2 }-> sieve(1 + (1 + (1 + 0)) + nats(1 + (1 + (1 + 0)))) :|: Function symbols to be analyzed: {filter}, {nats}, {sieve}, {zprimes} ---------------------------------------- (21) IntTrsBoundProof (UPPER BOUND(ID)) Computed SIZE bound using CoFloCo for: filter after applying outer abstraction to obtain an ITS, resulting in: O(n^1) with polynomial bound: z ---------------------------------------- (22) Obligation: Complexity RNTS consisting of the following rules: filter(z, z', z'') -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0 filter(z, z', z'') -{ 1 }-> 1 + X + filter(Y, z' - 1, z'') :|: Y >= 0, z = 1 + X + Y, X >= 0, z'' >= 0, z' - 1 >= 0 filter(z, z', z'') -{ 1 }-> 1 + 0 + filter(Y, z'', z'') :|: Y >= 0, z = 1 + X + Y, X >= 0, z'' >= 0, z' = 0 nats(z) -{ 1 }-> 1 + z + nats(1 + z) :|: z >= 0 sieve(z) -{ 1 }-> 1 + 0 + sieve(z - 1) :|: z - 1 >= 0 sieve(z) -{ 1 }-> 1 + (1 + N) + sieve(0) :|: Y >= 0, z = 1 + (1 + N) + Y, N >= 0 sieve(z) -{ 2 }-> 1 + (1 + 0) + sieve(1 + 0 + filter(Y', 0, 0)) :|: Y' >= 0, z = 1 + (1 + 0) + (1 + X' + Y'), X' >= 0 sieve(z) -{ 2 }-> 1 + (1 + (1 + N')) + sieve(1 + X'' + filter(Y'', N', 1 + N')) :|: Y'' >= 0, N' >= 0, X'' >= 0, z = 1 + (1 + (1 + N')) + (1 + X'' + Y'') zprimes -{ 2 }-> sieve(1 + (1 + (1 + 0)) + nats(1 + (1 + (1 + 0)))) :|: Function symbols to be analyzed: {filter}, {nats}, {sieve}, {zprimes} Previous analysis results are: filter: runtime: ?, size: O(n^1) [z] ---------------------------------------- (23) IntTrsBoundProof (UPPER BOUND(ID)) Computed RUNTIME bound using CoFloCo for: filter after applying outer abstraction to obtain an ITS, resulting in: O(n^1) with polynomial bound: z ---------------------------------------- (24) Obligation: Complexity RNTS consisting of the following rules: filter(z, z', z'') -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0 filter(z, z', z'') -{ 1 }-> 1 + X + filter(Y, z' - 1, z'') :|: Y >= 0, z = 1 + X + Y, X >= 0, z'' >= 0, z' - 1 >= 0 filter(z, z', z'') -{ 1 }-> 1 + 0 + filter(Y, z'', z'') :|: Y >= 0, z = 1 + X + Y, X >= 0, z'' >= 0, z' = 0 nats(z) -{ 1 }-> 1 + z + nats(1 + z) :|: z >= 0 sieve(z) -{ 1 }-> 1 + 0 + sieve(z - 1) :|: z - 1 >= 0 sieve(z) -{ 1 }-> 1 + (1 + N) + sieve(0) :|: Y >= 0, z = 1 + (1 + N) + Y, N >= 0 sieve(z) -{ 2 }-> 1 + (1 + 0) + sieve(1 + 0 + filter(Y', 0, 0)) :|: Y' >= 0, z = 1 + (1 + 0) + (1 + X' + Y'), X' >= 0 sieve(z) -{ 2 }-> 1 + (1 + (1 + N')) + sieve(1 + X'' + filter(Y'', N', 1 + N')) :|: Y'' >= 0, N' >= 0, X'' >= 0, z = 1 + (1 + (1 + N')) + (1 + X'' + Y'') zprimes -{ 2 }-> sieve(1 + (1 + (1 + 0)) + nats(1 + (1 + (1 + 0)))) :|: Function symbols to be analyzed: {nats}, {sieve}, {zprimes} Previous analysis results are: filter: runtime: O(n^1) [z], size: O(n^1) [z] ---------------------------------------- (25) ResultPropagationProof (UPPER BOUND(ID)) Applied inner abstraction using the recently inferred runtime/size bounds where possible. ---------------------------------------- (26) Obligation: Complexity RNTS consisting of the following rules: filter(z, z', z'') -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0 filter(z, z', z'') -{ 1 + Y }-> 1 + X + s' :|: s' >= 0, s' <= Y, Y >= 0, z = 1 + X + Y, X >= 0, z'' >= 0, z' - 1 >= 0 filter(z, z', z'') -{ 1 + Y }-> 1 + 0 + s :|: s >= 0, s <= Y, Y >= 0, z = 1 + X + Y, X >= 0, z'' >= 0, z' = 0 nats(z) -{ 1 }-> 1 + z + nats(1 + z) :|: z >= 0 sieve(z) -{ 1 }-> 1 + 0 + sieve(z - 1) :|: z - 1 >= 0 sieve(z) -{ 1 }-> 1 + (1 + N) + sieve(0) :|: Y >= 0, z = 1 + (1 + N) + Y, N >= 0 sieve(z) -{ 2 + Y' }-> 1 + (1 + 0) + sieve(1 + 0 + s'') :|: s'' >= 0, s'' <= Y', Y' >= 0, z = 1 + (1 + 0) + (1 + X' + Y'), X' >= 0 sieve(z) -{ 2 + Y'' }-> 1 + (1 + (1 + N')) + sieve(1 + X'' + s1) :|: s1 >= 0, s1 <= Y'', Y'' >= 0, N' >= 0, X'' >= 0, z = 1 + (1 + (1 + N')) + (1 + X'' + Y'') zprimes -{ 2 }-> sieve(1 + (1 + (1 + 0)) + nats(1 + (1 + (1 + 0)))) :|: Function symbols to be analyzed: {nats}, {sieve}, {zprimes} Previous analysis results are: filter: runtime: O(n^1) [z], size: O(n^1) [z] ---------------------------------------- (27) IntTrsBoundProof (UPPER BOUND(ID)) Computed SIZE bound using CoFloCo for: nats after applying outer abstraction to obtain an ITS, resulting in: O(1) with polynomial bound: 0 ---------------------------------------- (28) Obligation: Complexity RNTS consisting of the following rules: filter(z, z', z'') -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0 filter(z, z', z'') -{ 1 + Y }-> 1 + X + s' :|: s' >= 0, s' <= Y, Y >= 0, z = 1 + X + Y, X >= 0, z'' >= 0, z' - 1 >= 0 filter(z, z', z'') -{ 1 + Y }-> 1 + 0 + s :|: s >= 0, s <= Y, Y >= 0, z = 1 + X + Y, X >= 0, z'' >= 0, z' = 0 nats(z) -{ 1 }-> 1 + z + nats(1 + z) :|: z >= 0 sieve(z) -{ 1 }-> 1 + 0 + sieve(z - 1) :|: z - 1 >= 0 sieve(z) -{ 1 }-> 1 + (1 + N) + sieve(0) :|: Y >= 0, z = 1 + (1 + N) + Y, N >= 0 sieve(z) -{ 2 + Y' }-> 1 + (1 + 0) + sieve(1 + 0 + s'') :|: s'' >= 0, s'' <= Y', Y' >= 0, z = 1 + (1 + 0) + (1 + X' + Y'), X' >= 0 sieve(z) -{ 2 + Y'' }-> 1 + (1 + (1 + N')) + sieve(1 + X'' + s1) :|: s1 >= 0, s1 <= Y'', Y'' >= 0, N' >= 0, X'' >= 0, z = 1 + (1 + (1 + N')) + (1 + X'' + Y'') zprimes -{ 2 }-> sieve(1 + (1 + (1 + 0)) + nats(1 + (1 + (1 + 0)))) :|: Function symbols to be analyzed: {nats}, {sieve}, {zprimes} Previous analysis results are: filter: runtime: O(n^1) [z], size: O(n^1) [z] nats: runtime: ?, size: O(1) [0] ---------------------------------------- (29) IntTrsBoundProof (UPPER BOUND(ID)) Computed RUNTIME bound using CoFloCo for: nats after applying outer abstraction to obtain an ITS, resulting in: INF with polynomial bound: ? ---------------------------------------- (30) Obligation: Complexity RNTS consisting of the following rules: filter(z, z', z'') -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0 filter(z, z', z'') -{ 1 + Y }-> 1 + X + s' :|: s' >= 0, s' <= Y, Y >= 0, z = 1 + X + Y, X >= 0, z'' >= 0, z' - 1 >= 0 filter(z, z', z'') -{ 1 + Y }-> 1 + 0 + s :|: s >= 0, s <= Y, Y >= 0, z = 1 + X + Y, X >= 0, z'' >= 0, z' = 0 nats(z) -{ 1 }-> 1 + z + nats(1 + z) :|: z >= 0 sieve(z) -{ 1 }-> 1 + 0 + sieve(z - 1) :|: z - 1 >= 0 sieve(z) -{ 1 }-> 1 + (1 + N) + sieve(0) :|: Y >= 0, z = 1 + (1 + N) + Y, N >= 0 sieve(z) -{ 2 + Y' }-> 1 + (1 + 0) + sieve(1 + 0 + s'') :|: s'' >= 0, s'' <= Y', Y' >= 0, z = 1 + (1 + 0) + (1 + X' + Y'), X' >= 0 sieve(z) -{ 2 + Y'' }-> 1 + (1 + (1 + N')) + sieve(1 + X'' + s1) :|: s1 >= 0, s1 <= Y'', Y'' >= 0, N' >= 0, X'' >= 0, z = 1 + (1 + (1 + N')) + (1 + X'' + Y'') zprimes -{ 2 }-> sieve(1 + (1 + (1 + 0)) + nats(1 + (1 + (1 + 0)))) :|: Function symbols to be analyzed: {nats}, {sieve}, {zprimes} Previous analysis results are: filter: runtime: O(n^1) [z], size: O(n^1) [z] nats: runtime: INF, size: O(1) [0] ---------------------------------------- (31) CompletionProof (UPPER BOUND(ID)) The TRS is a completely defined constructor system, as every type has a constant constructor and the following rules were added: filter(v0, v1, v2) -> null_filter [0] sieve(v0) -> null_sieve [0] And the following fresh constants: null_filter, null_sieve ---------------------------------------- (32) Obligation: Runtime Complexity Weighted TRS where all functions are completely defined. The underlying TRS is: Runtime Complexity Weighted TRS with Types. The TRS R consists of the following rules: filter(cons(X, Y), 0, M) -> cons(0, filter(Y, M, M)) [1] filter(cons(X, Y), s(N), M) -> cons(X, filter(Y, N, M)) [1] sieve(cons(0, Y)) -> cons(0, sieve(Y)) [1] sieve(cons(s(N), Y)) -> cons(s(N), sieve(filter(Y, N, N))) [1] nats(N) -> cons(N, nats(s(N))) [1] zprimes -> sieve(nats(s(s(0)))) [1] filter(v0, v1, v2) -> null_filter [0] sieve(v0) -> null_sieve [0] The TRS has the following type information: filter :: cons:null_filter:null_sieve -> 0:s -> 0:s -> cons:null_filter:null_sieve cons :: 0:s -> cons:null_filter:null_sieve -> cons:null_filter:null_sieve 0 :: 0:s s :: 0:s -> 0:s sieve :: cons:null_filter:null_sieve -> cons:null_filter:null_sieve nats :: 0:s -> cons:null_filter:null_sieve zprimes :: cons:null_filter:null_sieve null_filter :: cons:null_filter:null_sieve null_sieve :: cons:null_filter:null_sieve Rewrite Strategy: INNERMOST ---------------------------------------- (33) CpxTypedWeightedTrsToRntsProof (UPPER BOUND(ID)) Transformed the TRS into an over-approximating RNTS by (improved) Size Abstraction. The constant constructors are abstracted as follows: 0 => 0 null_filter => 0 null_sieve => 0 ---------------------------------------- (34) Obligation: Complexity RNTS consisting of the following rules: filter(z, z', z'') -{ 0 }-> 0 :|: v0 >= 0, z'' = v2, v1 >= 0, z = v0, z' = v1, v2 >= 0 filter(z, z', z'') -{ 1 }-> 1 + X + filter(Y, N, M) :|: z' = 1 + N, Y >= 0, z = 1 + X + Y, X >= 0, M >= 0, z'' = M, N >= 0 filter(z, z', z'') -{ 1 }-> 1 + 0 + filter(Y, M, M) :|: Y >= 0, z = 1 + X + Y, X >= 0, M >= 0, z' = 0, z'' = M nats(z) -{ 1 }-> 1 + N + nats(1 + N) :|: z = N, N >= 0 sieve(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0 sieve(z) -{ 1 }-> 1 + 0 + sieve(Y) :|: Y >= 0, z = 1 + 0 + Y sieve(z) -{ 1 }-> 1 + (1 + N) + sieve(filter(Y, N, N)) :|: Y >= 0, z = 1 + (1 + N) + Y, N >= 0 zprimes -{ 1 }-> sieve(nats(1 + (1 + 0))) :|: Only complete derivations are relevant for the runtime complexity. ---------------------------------------- (35) CpxTrsToCdtProof (UPPER BOUND(ID)) Converted Cpx (relative) TRS with rewrite strategy PARALLEL_INNERMOST to CDT ---------------------------------------- (36) Obligation: Complexity Dependency Tuples Problem Rules: filter(cons(z0, z1), 0, z2) -> cons(0, filter(z1, z2, z2)) filter(cons(z0, z1), s(z2), z3) -> cons(z0, filter(z1, z2, z3)) sieve(cons(0, z0)) -> cons(0, sieve(z0)) sieve(cons(s(z0), z1)) -> cons(s(z0), sieve(filter(z1, z0, z0))) nats(z0) -> cons(z0, nats(s(z0))) zprimes -> sieve(nats(s(s(0)))) Tuples: FILTER(cons(z0, z1), 0, z2) -> c(FILTER(z1, z2, z2)) FILTER(cons(z0, z1), s(z2), z3) -> c1(FILTER(z1, z2, z3)) SIEVE(cons(0, z0)) -> c2(SIEVE(z0)) SIEVE(cons(s(z0), z1)) -> c3(SIEVE(filter(z1, z0, z0)), FILTER(z1, z0, z0)) NATS(z0) -> c4(NATS(s(z0))) ZPRIMES -> c5(SIEVE(nats(s(s(0)))), NATS(s(s(0)))) S tuples: FILTER(cons(z0, z1), 0, z2) -> c(FILTER(z1, z2, z2)) FILTER(cons(z0, z1), s(z2), z3) -> c1(FILTER(z1, z2, z3)) SIEVE(cons(0, z0)) -> c2(SIEVE(z0)) SIEVE(cons(s(z0), z1)) -> c3(SIEVE(filter(z1, z0, z0)), FILTER(z1, z0, z0)) NATS(z0) -> c4(NATS(s(z0))) ZPRIMES -> c5(SIEVE(nats(s(s(0)))), NATS(s(s(0)))) K tuples:none Defined Rule Symbols: filter_3, sieve_1, nats_1, zprimes Defined Pair Symbols: FILTER_3, SIEVE_1, NATS_1, ZPRIMES Compound Symbols: c_1, c1_1, c2_1, c3_2, c4_1, c5_2 ---------------------------------------- (37) CdtGraphSplitRhsProof (BOTH BOUNDS(ID, ID)) Split RHS of tuples not part of any SCC ---------------------------------------- (38) Obligation: Complexity Dependency Tuples Problem Rules: filter(cons(z0, z1), 0, z2) -> cons(0, filter(z1, z2, z2)) filter(cons(z0, z1), s(z2), z3) -> cons(z0, filter(z1, z2, z3)) sieve(cons(0, z0)) -> cons(0, sieve(z0)) sieve(cons(s(z0), z1)) -> cons(s(z0), sieve(filter(z1, z0, z0))) nats(z0) -> cons(z0, nats(s(z0))) zprimes -> sieve(nats(s(s(0)))) Tuples: FILTER(cons(z0, z1), 0, z2) -> c(FILTER(z1, z2, z2)) FILTER(cons(z0, z1), s(z2), z3) -> c1(FILTER(z1, z2, z3)) SIEVE(cons(0, z0)) -> c2(SIEVE(z0)) SIEVE(cons(s(z0), z1)) -> c3(SIEVE(filter(z1, z0, z0)), FILTER(z1, z0, z0)) NATS(z0) -> c4(NATS(s(z0))) ZPRIMES -> c6(SIEVE(nats(s(s(0))))) ZPRIMES -> c6(NATS(s(s(0)))) S tuples: FILTER(cons(z0, z1), 0, z2) -> c(FILTER(z1, z2, z2)) FILTER(cons(z0, z1), s(z2), z3) -> c1(FILTER(z1, z2, z3)) SIEVE(cons(0, z0)) -> c2(SIEVE(z0)) SIEVE(cons(s(z0), z1)) -> c3(SIEVE(filter(z1, z0, z0)), FILTER(z1, z0, z0)) NATS(z0) -> c4(NATS(s(z0))) ZPRIMES -> c6(SIEVE(nats(s(s(0))))) ZPRIMES -> c6(NATS(s(s(0)))) K tuples:none Defined Rule Symbols: filter_3, sieve_1, nats_1, zprimes Defined Pair Symbols: FILTER_3, SIEVE_1, NATS_1, ZPRIMES Compound Symbols: c_1, c1_1, c2_1, c3_2, c4_1, c6_1 ---------------------------------------- (39) CdtLeafRemovalProof (ComplexityIfPolyImplication) Removed 1 leading nodes: ZPRIMES -> c6(NATS(s(s(0)))) ---------------------------------------- (40) Obligation: Complexity Dependency Tuples Problem Rules: filter(cons(z0, z1), 0, z2) -> cons(0, filter(z1, z2, z2)) filter(cons(z0, z1), s(z2), z3) -> cons(z0, filter(z1, z2, z3)) sieve(cons(0, z0)) -> cons(0, sieve(z0)) sieve(cons(s(z0), z1)) -> cons(s(z0), sieve(filter(z1, z0, z0))) nats(z0) -> cons(z0, nats(s(z0))) zprimes -> sieve(nats(s(s(0)))) Tuples: FILTER(cons(z0, z1), 0, z2) -> c(FILTER(z1, z2, z2)) FILTER(cons(z0, z1), s(z2), z3) -> c1(FILTER(z1, z2, z3)) SIEVE(cons(0, z0)) -> c2(SIEVE(z0)) SIEVE(cons(s(z0), z1)) -> c3(SIEVE(filter(z1, z0, z0)), FILTER(z1, z0, z0)) NATS(z0) -> c4(NATS(s(z0))) ZPRIMES -> c6(SIEVE(nats(s(s(0))))) S tuples: FILTER(cons(z0, z1), 0, z2) -> c(FILTER(z1, z2, z2)) FILTER(cons(z0, z1), s(z2), z3) -> c1(FILTER(z1, z2, z3)) SIEVE(cons(0, z0)) -> c2(SIEVE(z0)) SIEVE(cons(s(z0), z1)) -> c3(SIEVE(filter(z1, z0, z0)), FILTER(z1, z0, z0)) NATS(z0) -> c4(NATS(s(z0))) ZPRIMES -> c6(SIEVE(nats(s(s(0))))) K tuples:none Defined Rule Symbols: filter_3, sieve_1, nats_1, zprimes Defined Pair Symbols: FILTER_3, SIEVE_1, NATS_1, ZPRIMES Compound Symbols: c_1, c1_1, c2_1, c3_2, c4_1, c6_1 ---------------------------------------- (41) CdtKnowledgeProof (BOTH BOUNDS(ID, ID)) The following tuples could be moved from S to K by knowledge propagation: ZPRIMES -> c6(SIEVE(nats(s(s(0))))) ---------------------------------------- (42) Obligation: Complexity Dependency Tuples Problem Rules: filter(cons(z0, z1), 0, z2) -> cons(0, filter(z1, z2, z2)) filter(cons(z0, z1), s(z2), z3) -> cons(z0, filter(z1, z2, z3)) sieve(cons(0, z0)) -> cons(0, sieve(z0)) sieve(cons(s(z0), z1)) -> cons(s(z0), sieve(filter(z1, z0, z0))) nats(z0) -> cons(z0, nats(s(z0))) zprimes -> sieve(nats(s(s(0)))) Tuples: FILTER(cons(z0, z1), 0, z2) -> c(FILTER(z1, z2, z2)) FILTER(cons(z0, z1), s(z2), z3) -> c1(FILTER(z1, z2, z3)) SIEVE(cons(0, z0)) -> c2(SIEVE(z0)) SIEVE(cons(s(z0), z1)) -> c3(SIEVE(filter(z1, z0, z0)), FILTER(z1, z0, z0)) NATS(z0) -> c4(NATS(s(z0))) ZPRIMES -> c6(SIEVE(nats(s(s(0))))) S tuples: FILTER(cons(z0, z1), 0, z2) -> c(FILTER(z1, z2, z2)) FILTER(cons(z0, z1), s(z2), z3) -> c1(FILTER(z1, z2, z3)) SIEVE(cons(0, z0)) -> c2(SIEVE(z0)) SIEVE(cons(s(z0), z1)) -> c3(SIEVE(filter(z1, z0, z0)), FILTER(z1, z0, z0)) NATS(z0) -> c4(NATS(s(z0))) K tuples: ZPRIMES -> c6(SIEVE(nats(s(s(0))))) Defined Rule Symbols: filter_3, sieve_1, nats_1, zprimes Defined Pair Symbols: FILTER_3, SIEVE_1, NATS_1, ZPRIMES Compound Symbols: c_1, c1_1, c2_1, c3_2, c4_1, c6_1 ---------------------------------------- (43) CdtUsableRulesProof (BOTH BOUNDS(ID, ID)) The following rules are not usable and were removed: sieve(cons(0, z0)) -> cons(0, sieve(z0)) sieve(cons(s(z0), z1)) -> cons(s(z0), sieve(filter(z1, z0, z0))) zprimes -> sieve(nats(s(s(0)))) ---------------------------------------- (44) Obligation: Complexity Dependency Tuples Problem Rules: filter(cons(z0, z1), 0, z2) -> cons(0, filter(z1, z2, z2)) filter(cons(z0, z1), s(z2), z3) -> cons(z0, filter(z1, z2, z3)) nats(z0) -> cons(z0, nats(s(z0))) Tuples: FILTER(cons(z0, z1), 0, z2) -> c(FILTER(z1, z2, z2)) FILTER(cons(z0, z1), s(z2), z3) -> c1(FILTER(z1, z2, z3)) SIEVE(cons(0, z0)) -> c2(SIEVE(z0)) SIEVE(cons(s(z0), z1)) -> c3(SIEVE(filter(z1, z0, z0)), FILTER(z1, z0, z0)) NATS(z0) -> c4(NATS(s(z0))) ZPRIMES -> c6(SIEVE(nats(s(s(0))))) S tuples: FILTER(cons(z0, z1), 0, z2) -> c(FILTER(z1, z2, z2)) FILTER(cons(z0, z1), s(z2), z3) -> c1(FILTER(z1, z2, z3)) SIEVE(cons(0, z0)) -> c2(SIEVE(z0)) SIEVE(cons(s(z0), z1)) -> c3(SIEVE(filter(z1, z0, z0)), FILTER(z1, z0, z0)) NATS(z0) -> c4(NATS(s(z0))) K tuples: ZPRIMES -> c6(SIEVE(nats(s(s(0))))) Defined Rule Symbols: filter_3, nats_1 Defined Pair Symbols: FILTER_3, SIEVE_1, NATS_1, ZPRIMES Compound Symbols: c_1, c1_1, c2_1, c3_2, c4_1, c6_1 ---------------------------------------- (45) CdtNarrowingProof (BOTH BOUNDS(ID, ID)) Use narrowing to replace SIEVE(cons(s(z0), z1)) -> c3(SIEVE(filter(z1, z0, z0)), FILTER(z1, z0, z0)) by SIEVE(cons(s(0), cons(z0, z1))) -> c3(SIEVE(cons(0, filter(z1, 0, 0))), FILTER(cons(z0, z1), 0, 0)) SIEVE(cons(s(s(z2)), cons(z0, z1))) -> c3(SIEVE(cons(z0, filter(z1, z2, s(z2)))), FILTER(cons(z0, z1), s(z2), s(z2))) ---------------------------------------- (46) Obligation: Complexity Dependency Tuples Problem Rules: filter(cons(z0, z1), 0, z2) -> cons(0, filter(z1, z2, z2)) filter(cons(z0, z1), s(z2), z3) -> cons(z0, filter(z1, z2, z3)) nats(z0) -> cons(z0, nats(s(z0))) Tuples: FILTER(cons(z0, z1), 0, z2) -> c(FILTER(z1, z2, z2)) FILTER(cons(z0, z1), s(z2), z3) -> c1(FILTER(z1, z2, z3)) SIEVE(cons(0, z0)) -> c2(SIEVE(z0)) NATS(z0) -> c4(NATS(s(z0))) ZPRIMES -> c6(SIEVE(nats(s(s(0))))) SIEVE(cons(s(0), cons(z0, z1))) -> c3(SIEVE(cons(0, filter(z1, 0, 0))), FILTER(cons(z0, z1), 0, 0)) SIEVE(cons(s(s(z2)), cons(z0, z1))) -> c3(SIEVE(cons(z0, filter(z1, z2, s(z2)))), FILTER(cons(z0, z1), s(z2), s(z2))) S tuples: FILTER(cons(z0, z1), 0, z2) -> c(FILTER(z1, z2, z2)) FILTER(cons(z0, z1), s(z2), z3) -> c1(FILTER(z1, z2, z3)) SIEVE(cons(0, z0)) -> c2(SIEVE(z0)) NATS(z0) -> c4(NATS(s(z0))) SIEVE(cons(s(0), cons(z0, z1))) -> c3(SIEVE(cons(0, filter(z1, 0, 0))), FILTER(cons(z0, z1), 0, 0)) SIEVE(cons(s(s(z2)), cons(z0, z1))) -> c3(SIEVE(cons(z0, filter(z1, z2, s(z2)))), FILTER(cons(z0, z1), s(z2), s(z2))) K tuples: ZPRIMES -> c6(SIEVE(nats(s(s(0))))) Defined Rule Symbols: filter_3, nats_1 Defined Pair Symbols: FILTER_3, SIEVE_1, NATS_1, ZPRIMES Compound Symbols: c_1, c1_1, c2_1, c4_1, c6_1, c3_2 ---------------------------------------- (47) CdtNarrowingProof (BOTH BOUNDS(ID, ID)) Use narrowing to replace ZPRIMES -> c6(SIEVE(nats(s(s(0))))) by ZPRIMES -> c6(SIEVE(cons(s(s(0)), nats(s(s(s(0))))))) ---------------------------------------- (48) Obligation: Complexity Dependency Tuples Problem Rules: filter(cons(z0, z1), 0, z2) -> cons(0, filter(z1, z2, z2)) filter(cons(z0, z1), s(z2), z3) -> cons(z0, filter(z1, z2, z3)) nats(z0) -> cons(z0, nats(s(z0))) Tuples: FILTER(cons(z0, z1), 0, z2) -> c(FILTER(z1, z2, z2)) FILTER(cons(z0, z1), s(z2), z3) -> c1(FILTER(z1, z2, z3)) SIEVE(cons(0, z0)) -> c2(SIEVE(z0)) NATS(z0) -> c4(NATS(s(z0))) SIEVE(cons(s(0), cons(z0, z1))) -> c3(SIEVE(cons(0, filter(z1, 0, 0))), FILTER(cons(z0, z1), 0, 0)) SIEVE(cons(s(s(z2)), cons(z0, z1))) -> c3(SIEVE(cons(z0, filter(z1, z2, s(z2)))), FILTER(cons(z0, z1), s(z2), s(z2))) ZPRIMES -> c6(SIEVE(cons(s(s(0)), nats(s(s(s(0))))))) S tuples: FILTER(cons(z0, z1), 0, z2) -> c(FILTER(z1, z2, z2)) FILTER(cons(z0, z1), s(z2), z3) -> c1(FILTER(z1, z2, z3)) SIEVE(cons(0, z0)) -> c2(SIEVE(z0)) NATS(z0) -> c4(NATS(s(z0))) SIEVE(cons(s(0), cons(z0, z1))) -> c3(SIEVE(cons(0, filter(z1, 0, 0))), FILTER(cons(z0, z1), 0, 0)) SIEVE(cons(s(s(z2)), cons(z0, z1))) -> c3(SIEVE(cons(z0, filter(z1, z2, s(z2)))), FILTER(cons(z0, z1), s(z2), s(z2))) K tuples: ZPRIMES -> c6(SIEVE(nats(s(s(0))))) Defined Rule Symbols: filter_3, nats_1 Defined Pair Symbols: FILTER_3, SIEVE_1, NATS_1, ZPRIMES Compound Symbols: c_1, c1_1, c2_1, c4_1, c3_2, c6_1 ---------------------------------------- (49) CdtNarrowingProof (BOTH BOUNDS(ID, ID)) Use narrowing to replace ZPRIMES -> c6(SIEVE(cons(s(s(0)), nats(s(s(s(0))))))) by ZPRIMES -> c6(SIEVE(cons(s(s(0)), cons(s(s(s(0))), nats(s(s(s(s(0))))))))) ---------------------------------------- (50) Obligation: Complexity Dependency Tuples Problem Rules: filter(cons(z0, z1), 0, z2) -> cons(0, filter(z1, z2, z2)) filter(cons(z0, z1), s(z2), z3) -> cons(z0, filter(z1, z2, z3)) nats(z0) -> cons(z0, nats(s(z0))) Tuples: FILTER(cons(z0, z1), 0, z2) -> c(FILTER(z1, z2, z2)) FILTER(cons(z0, z1), s(z2), z3) -> c1(FILTER(z1, z2, z3)) SIEVE(cons(0, z0)) -> c2(SIEVE(z0)) NATS(z0) -> c4(NATS(s(z0))) SIEVE(cons(s(0), cons(z0, z1))) -> c3(SIEVE(cons(0, filter(z1, 0, 0))), FILTER(cons(z0, z1), 0, 0)) SIEVE(cons(s(s(z2)), cons(z0, z1))) -> c3(SIEVE(cons(z0, filter(z1, z2, s(z2)))), FILTER(cons(z0, z1), s(z2), s(z2))) ZPRIMES -> c6(SIEVE(cons(s(s(0)), cons(s(s(s(0))), nats(s(s(s(s(0))))))))) S tuples: FILTER(cons(z0, z1), 0, z2) -> c(FILTER(z1, z2, z2)) FILTER(cons(z0, z1), s(z2), z3) -> c1(FILTER(z1, z2, z3)) SIEVE(cons(0, z0)) -> c2(SIEVE(z0)) NATS(z0) -> c4(NATS(s(z0))) SIEVE(cons(s(0), cons(z0, z1))) -> c3(SIEVE(cons(0, filter(z1, 0, 0))), FILTER(cons(z0, z1), 0, 0)) SIEVE(cons(s(s(z2)), cons(z0, z1))) -> c3(SIEVE(cons(z0, filter(z1, z2, s(z2)))), FILTER(cons(z0, z1), s(z2), s(z2))) K tuples: ZPRIMES -> c6(SIEVE(nats(s(s(0))))) Defined Rule Symbols: filter_3, nats_1 Defined Pair Symbols: FILTER_3, SIEVE_1, NATS_1, ZPRIMES Compound Symbols: c_1, c1_1, c2_1, c4_1, c3_2, c6_1 ---------------------------------------- (51) CdtInstantiationProof (BOTH BOUNDS(ID, ID)) Use instantiation to replace NATS(z0) -> c4(NATS(s(z0))) by NATS(s(x0)) -> c4(NATS(s(s(x0)))) ---------------------------------------- (52) Obligation: Complexity Dependency Tuples Problem Rules: filter(cons(z0, z1), 0, z2) -> cons(0, filter(z1, z2, z2)) filter(cons(z0, z1), s(z2), z3) -> cons(z0, filter(z1, z2, z3)) nats(z0) -> cons(z0, nats(s(z0))) Tuples: FILTER(cons(z0, z1), 0, z2) -> c(FILTER(z1, z2, z2)) FILTER(cons(z0, z1), s(z2), z3) -> c1(FILTER(z1, z2, z3)) SIEVE(cons(0, z0)) -> c2(SIEVE(z0)) SIEVE(cons(s(0), cons(z0, z1))) -> c3(SIEVE(cons(0, filter(z1, 0, 0))), FILTER(cons(z0, z1), 0, 0)) SIEVE(cons(s(s(z2)), cons(z0, z1))) -> c3(SIEVE(cons(z0, filter(z1, z2, s(z2)))), FILTER(cons(z0, z1), s(z2), s(z2))) ZPRIMES -> c6(SIEVE(cons(s(s(0)), cons(s(s(s(0))), nats(s(s(s(s(0))))))))) NATS(s(x0)) -> c4(NATS(s(s(x0)))) S tuples: FILTER(cons(z0, z1), 0, z2) -> c(FILTER(z1, z2, z2)) FILTER(cons(z0, z1), s(z2), z3) -> c1(FILTER(z1, z2, z3)) SIEVE(cons(0, z0)) -> c2(SIEVE(z0)) SIEVE(cons(s(0), cons(z0, z1))) -> c3(SIEVE(cons(0, filter(z1, 0, 0))), FILTER(cons(z0, z1), 0, 0)) SIEVE(cons(s(s(z2)), cons(z0, z1))) -> c3(SIEVE(cons(z0, filter(z1, z2, s(z2)))), FILTER(cons(z0, z1), s(z2), s(z2))) NATS(s(x0)) -> c4(NATS(s(s(x0)))) K tuples: ZPRIMES -> c6(SIEVE(nats(s(s(0))))) Defined Rule Symbols: filter_3, nats_1 Defined Pair Symbols: FILTER_3, SIEVE_1, ZPRIMES, NATS_1 Compound Symbols: c_1, c1_1, c2_1, c3_2, c6_1, c4_1 ---------------------------------------- (53) CdtRewritingProof (BOTH BOUNDS(ID, ID)) Used rewriting to replace ZPRIMES -> c6(SIEVE(cons(s(s(0)), cons(s(s(s(0))), nats(s(s(s(s(0))))))))) by ZPRIMES -> c6(SIEVE(cons(s(s(0)), cons(s(s(s(0))), cons(s(s(s(s(0)))), nats(s(s(s(s(s(0))))))))))) ---------------------------------------- (54) Obligation: Complexity Dependency Tuples Problem Rules: filter(cons(z0, z1), 0, z2) -> cons(0, filter(z1, z2, z2)) filter(cons(z0, z1), s(z2), z3) -> cons(z0, filter(z1, z2, z3)) nats(z0) -> cons(z0, nats(s(z0))) Tuples: FILTER(cons(z0, z1), 0, z2) -> c(FILTER(z1, z2, z2)) FILTER(cons(z0, z1), s(z2), z3) -> c1(FILTER(z1, z2, z3)) SIEVE(cons(0, z0)) -> c2(SIEVE(z0)) SIEVE(cons(s(0), cons(z0, z1))) -> c3(SIEVE(cons(0, filter(z1, 0, 0))), FILTER(cons(z0, z1), 0, 0)) SIEVE(cons(s(s(z2)), cons(z0, z1))) -> c3(SIEVE(cons(z0, filter(z1, z2, s(z2)))), FILTER(cons(z0, z1), s(z2), s(z2))) NATS(s(x0)) -> c4(NATS(s(s(x0)))) ZPRIMES -> c6(SIEVE(cons(s(s(0)), cons(s(s(s(0))), cons(s(s(s(s(0)))), nats(s(s(s(s(s(0))))))))))) S tuples: FILTER(cons(z0, z1), 0, z2) -> c(FILTER(z1, z2, z2)) FILTER(cons(z0, z1), s(z2), z3) -> c1(FILTER(z1, z2, z3)) SIEVE(cons(0, z0)) -> c2(SIEVE(z0)) SIEVE(cons(s(0), cons(z0, z1))) -> c3(SIEVE(cons(0, filter(z1, 0, 0))), FILTER(cons(z0, z1), 0, 0)) SIEVE(cons(s(s(z2)), cons(z0, z1))) -> c3(SIEVE(cons(z0, filter(z1, z2, s(z2)))), FILTER(cons(z0, z1), s(z2), s(z2))) NATS(s(x0)) -> c4(NATS(s(s(x0)))) K tuples: ZPRIMES -> c6(SIEVE(nats(s(s(0))))) Defined Rule Symbols: filter_3, nats_1 Defined Pair Symbols: FILTER_3, SIEVE_1, NATS_1, ZPRIMES Compound Symbols: c_1, c1_1, c2_1, c3_2, c4_1, c6_1 ---------------------------------------- (55) CdtInstantiationProof (BOTH BOUNDS(ID, ID)) Use instantiation to replace NATS(s(x0)) -> c4(NATS(s(s(x0)))) by NATS(s(s(x0))) -> c4(NATS(s(s(s(x0))))) ---------------------------------------- (56) Obligation: Complexity Dependency Tuples Problem Rules: filter(cons(z0, z1), 0, z2) -> cons(0, filter(z1, z2, z2)) filter(cons(z0, z1), s(z2), z3) -> cons(z0, filter(z1, z2, z3)) nats(z0) -> cons(z0, nats(s(z0))) Tuples: FILTER(cons(z0, z1), 0, z2) -> c(FILTER(z1, z2, z2)) FILTER(cons(z0, z1), s(z2), z3) -> c1(FILTER(z1, z2, z3)) SIEVE(cons(0, z0)) -> c2(SIEVE(z0)) SIEVE(cons(s(0), cons(z0, z1))) -> c3(SIEVE(cons(0, filter(z1, 0, 0))), FILTER(cons(z0, z1), 0, 0)) SIEVE(cons(s(s(z2)), cons(z0, z1))) -> c3(SIEVE(cons(z0, filter(z1, z2, s(z2)))), FILTER(cons(z0, z1), s(z2), s(z2))) ZPRIMES -> c6(SIEVE(cons(s(s(0)), cons(s(s(s(0))), cons(s(s(s(s(0)))), nats(s(s(s(s(s(0))))))))))) NATS(s(s(x0))) -> c4(NATS(s(s(s(x0))))) S tuples: FILTER(cons(z0, z1), 0, z2) -> c(FILTER(z1, z2, z2)) FILTER(cons(z0, z1), s(z2), z3) -> c1(FILTER(z1, z2, z3)) SIEVE(cons(0, z0)) -> c2(SIEVE(z0)) SIEVE(cons(s(0), cons(z0, z1))) -> c3(SIEVE(cons(0, filter(z1, 0, 0))), FILTER(cons(z0, z1), 0, 0)) SIEVE(cons(s(s(z2)), cons(z0, z1))) -> c3(SIEVE(cons(z0, filter(z1, z2, s(z2)))), FILTER(cons(z0, z1), s(z2), s(z2))) NATS(s(s(x0))) -> c4(NATS(s(s(s(x0))))) K tuples: ZPRIMES -> c6(SIEVE(nats(s(s(0))))) Defined Rule Symbols: filter_3, nats_1 Defined Pair Symbols: FILTER_3, SIEVE_1, ZPRIMES, NATS_1 Compound Symbols: c_1, c1_1, c2_1, c3_2, c6_1, c4_1 ---------------------------------------- (57) CdtRewritingProof (BOTH BOUNDS(ID, ID)) Used rewriting to replace ZPRIMES -> c6(SIEVE(cons(s(s(0)), cons(s(s(s(0))), cons(s(s(s(s(0)))), nats(s(s(s(s(s(0))))))))))) by ZPRIMES -> c6(SIEVE(cons(s(s(0)), cons(s(s(s(0))), cons(s(s(s(s(0)))), cons(s(s(s(s(s(0))))), nats(s(s(s(s(s(s(0))))))))))))) ---------------------------------------- (58) Obligation: Complexity Dependency Tuples Problem Rules: filter(cons(z0, z1), 0, z2) -> cons(0, filter(z1, z2, z2)) filter(cons(z0, z1), s(z2), z3) -> cons(z0, filter(z1, z2, z3)) nats(z0) -> cons(z0, nats(s(z0))) Tuples: FILTER(cons(z0, z1), 0, z2) -> c(FILTER(z1, z2, z2)) FILTER(cons(z0, z1), s(z2), z3) -> c1(FILTER(z1, z2, z3)) SIEVE(cons(0, z0)) -> c2(SIEVE(z0)) SIEVE(cons(s(0), cons(z0, z1))) -> c3(SIEVE(cons(0, filter(z1, 0, 0))), FILTER(cons(z0, z1), 0, 0)) SIEVE(cons(s(s(z2)), cons(z0, z1))) -> c3(SIEVE(cons(z0, filter(z1, z2, s(z2)))), FILTER(cons(z0, z1), s(z2), s(z2))) NATS(s(s(x0))) -> c4(NATS(s(s(s(x0))))) ZPRIMES -> c6(SIEVE(cons(s(s(0)), cons(s(s(s(0))), cons(s(s(s(s(0)))), cons(s(s(s(s(s(0))))), nats(s(s(s(s(s(s(0))))))))))))) S tuples: FILTER(cons(z0, z1), 0, z2) -> c(FILTER(z1, z2, z2)) FILTER(cons(z0, z1), s(z2), z3) -> c1(FILTER(z1, z2, z3)) SIEVE(cons(0, z0)) -> c2(SIEVE(z0)) SIEVE(cons(s(0), cons(z0, z1))) -> c3(SIEVE(cons(0, filter(z1, 0, 0))), FILTER(cons(z0, z1), 0, 0)) SIEVE(cons(s(s(z2)), cons(z0, z1))) -> c3(SIEVE(cons(z0, filter(z1, z2, s(z2)))), FILTER(cons(z0, z1), s(z2), s(z2))) NATS(s(s(x0))) -> c4(NATS(s(s(s(x0))))) K tuples: ZPRIMES -> c6(SIEVE(nats(s(s(0))))) Defined Rule Symbols: filter_3, nats_1 Defined Pair Symbols: FILTER_3, SIEVE_1, NATS_1, ZPRIMES Compound Symbols: c_1, c1_1, c2_1, c3_2, c4_1, c6_1 ---------------------------------------- (59) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID)) Use forward instantiation to replace FILTER(cons(z0, z1), 0, z2) -> c(FILTER(z1, z2, z2)) by FILTER(cons(z0, cons(y0, y1)), 0, 0) -> c(FILTER(cons(y0, y1), 0, 0)) FILTER(cons(z0, cons(y0, y1)), 0, s(y2)) -> c(FILTER(cons(y0, y1), s(y2), s(y2))) ---------------------------------------- (60) Obligation: Complexity Dependency Tuples Problem Rules: filter(cons(z0, z1), 0, z2) -> cons(0, filter(z1, z2, z2)) filter(cons(z0, z1), s(z2), z3) -> cons(z0, filter(z1, z2, z3)) nats(z0) -> cons(z0, nats(s(z0))) Tuples: FILTER(cons(z0, z1), s(z2), z3) -> c1(FILTER(z1, z2, z3)) SIEVE(cons(0, z0)) -> c2(SIEVE(z0)) SIEVE(cons(s(0), cons(z0, z1))) -> c3(SIEVE(cons(0, filter(z1, 0, 0))), FILTER(cons(z0, z1), 0, 0)) SIEVE(cons(s(s(z2)), cons(z0, z1))) -> c3(SIEVE(cons(z0, filter(z1, z2, s(z2)))), FILTER(cons(z0, z1), s(z2), s(z2))) NATS(s(s(x0))) -> c4(NATS(s(s(s(x0))))) ZPRIMES -> c6(SIEVE(cons(s(s(0)), cons(s(s(s(0))), cons(s(s(s(s(0)))), cons(s(s(s(s(s(0))))), nats(s(s(s(s(s(s(0))))))))))))) FILTER(cons(z0, cons(y0, y1)), 0, 0) -> c(FILTER(cons(y0, y1), 0, 0)) FILTER(cons(z0, cons(y0, y1)), 0, s(y2)) -> c(FILTER(cons(y0, y1), s(y2), s(y2))) S tuples: FILTER(cons(z0, z1), s(z2), z3) -> c1(FILTER(z1, z2, z3)) SIEVE(cons(0, z0)) -> c2(SIEVE(z0)) SIEVE(cons(s(0), cons(z0, z1))) -> c3(SIEVE(cons(0, filter(z1, 0, 0))), FILTER(cons(z0, z1), 0, 0)) SIEVE(cons(s(s(z2)), cons(z0, z1))) -> c3(SIEVE(cons(z0, filter(z1, z2, s(z2)))), FILTER(cons(z0, z1), s(z2), s(z2))) NATS(s(s(x0))) -> c4(NATS(s(s(s(x0))))) FILTER(cons(z0, cons(y0, y1)), 0, 0) -> c(FILTER(cons(y0, y1), 0, 0)) FILTER(cons(z0, cons(y0, y1)), 0, s(y2)) -> c(FILTER(cons(y0, y1), s(y2), s(y2))) K tuples: ZPRIMES -> c6(SIEVE(nats(s(s(0))))) Defined Rule Symbols: filter_3, nats_1 Defined Pair Symbols: FILTER_3, SIEVE_1, NATS_1, ZPRIMES Compound Symbols: c1_1, c2_1, c3_2, c4_1, c6_1, c_1 ---------------------------------------- (61) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID)) Use forward instantiation to replace FILTER(cons(z0, z1), s(z2), z3) -> c1(FILTER(z1, z2, z3)) by FILTER(cons(z0, cons(y0, y1)), s(s(y2)), z3) -> c1(FILTER(cons(y0, y1), s(y2), z3)) FILTER(cons(z0, cons(y0, cons(y1, y2))), s(0), 0) -> c1(FILTER(cons(y0, cons(y1, y2)), 0, 0)) FILTER(cons(z0, cons(y0, cons(y1, y2))), s(0), s(y3)) -> c1(FILTER(cons(y0, cons(y1, y2)), 0, s(y3))) ---------------------------------------- (62) Obligation: Complexity Dependency Tuples Problem Rules: filter(cons(z0, z1), 0, z2) -> cons(0, filter(z1, z2, z2)) filter(cons(z0, z1), s(z2), z3) -> cons(z0, filter(z1, z2, z3)) nats(z0) -> cons(z0, nats(s(z0))) Tuples: SIEVE(cons(0, z0)) -> c2(SIEVE(z0)) SIEVE(cons(s(0), cons(z0, z1))) -> c3(SIEVE(cons(0, filter(z1, 0, 0))), FILTER(cons(z0, z1), 0, 0)) SIEVE(cons(s(s(z2)), cons(z0, z1))) -> c3(SIEVE(cons(z0, filter(z1, z2, s(z2)))), FILTER(cons(z0, z1), s(z2), s(z2))) NATS(s(s(x0))) -> c4(NATS(s(s(s(x0))))) ZPRIMES -> c6(SIEVE(cons(s(s(0)), cons(s(s(s(0))), cons(s(s(s(s(0)))), cons(s(s(s(s(s(0))))), nats(s(s(s(s(s(s(0))))))))))))) FILTER(cons(z0, cons(y0, y1)), 0, 0) -> c(FILTER(cons(y0, y1), 0, 0)) FILTER(cons(z0, cons(y0, y1)), 0, s(y2)) -> c(FILTER(cons(y0, y1), s(y2), s(y2))) FILTER(cons(z0, cons(y0, y1)), s(s(y2)), z3) -> c1(FILTER(cons(y0, y1), s(y2), z3)) FILTER(cons(z0, cons(y0, cons(y1, y2))), s(0), 0) -> c1(FILTER(cons(y0, cons(y1, y2)), 0, 0)) FILTER(cons(z0, cons(y0, cons(y1, y2))), s(0), s(y3)) -> c1(FILTER(cons(y0, cons(y1, y2)), 0, s(y3))) S tuples: SIEVE(cons(0, z0)) -> c2(SIEVE(z0)) SIEVE(cons(s(0), cons(z0, z1))) -> c3(SIEVE(cons(0, filter(z1, 0, 0))), FILTER(cons(z0, z1), 0, 0)) SIEVE(cons(s(s(z2)), cons(z0, z1))) -> c3(SIEVE(cons(z0, filter(z1, z2, s(z2)))), FILTER(cons(z0, z1), s(z2), s(z2))) NATS(s(s(x0))) -> c4(NATS(s(s(s(x0))))) FILTER(cons(z0, cons(y0, y1)), 0, 0) -> c(FILTER(cons(y0, y1), 0, 0)) FILTER(cons(z0, cons(y0, y1)), 0, s(y2)) -> c(FILTER(cons(y0, y1), s(y2), s(y2))) FILTER(cons(z0, cons(y0, y1)), s(s(y2)), z3) -> c1(FILTER(cons(y0, y1), s(y2), z3)) FILTER(cons(z0, cons(y0, cons(y1, y2))), s(0), 0) -> c1(FILTER(cons(y0, cons(y1, y2)), 0, 0)) FILTER(cons(z0, cons(y0, cons(y1, y2))), s(0), s(y3)) -> c1(FILTER(cons(y0, cons(y1, y2)), 0, s(y3))) K tuples: ZPRIMES -> c6(SIEVE(nats(s(s(0))))) Defined Rule Symbols: filter_3, nats_1 Defined Pair Symbols: SIEVE_1, NATS_1, ZPRIMES, FILTER_3 Compound Symbols: c2_1, c3_2, c4_1, c6_1, c_1, c1_1 ---------------------------------------- (63) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID)) Use forward instantiation to replace SIEVE(cons(0, z0)) -> c2(SIEVE(z0)) by SIEVE(cons(0, cons(0, y0))) -> c2(SIEVE(cons(0, y0))) SIEVE(cons(0, cons(s(0), cons(y0, y1)))) -> c2(SIEVE(cons(s(0), cons(y0, y1)))) SIEVE(cons(0, cons(s(s(y0)), cons(y1, y2)))) -> c2(SIEVE(cons(s(s(y0)), cons(y1, y2)))) ---------------------------------------- (64) Obligation: Complexity Dependency Tuples Problem Rules: filter(cons(z0, z1), 0, z2) -> cons(0, filter(z1, z2, z2)) filter(cons(z0, z1), s(z2), z3) -> cons(z0, filter(z1, z2, z3)) nats(z0) -> cons(z0, nats(s(z0))) Tuples: SIEVE(cons(s(0), cons(z0, z1))) -> c3(SIEVE(cons(0, filter(z1, 0, 0))), FILTER(cons(z0, z1), 0, 0)) SIEVE(cons(s(s(z2)), cons(z0, z1))) -> c3(SIEVE(cons(z0, filter(z1, z2, s(z2)))), FILTER(cons(z0, z1), s(z2), s(z2))) NATS(s(s(x0))) -> c4(NATS(s(s(s(x0))))) ZPRIMES -> c6(SIEVE(cons(s(s(0)), cons(s(s(s(0))), cons(s(s(s(s(0)))), cons(s(s(s(s(s(0))))), nats(s(s(s(s(s(s(0))))))))))))) FILTER(cons(z0, cons(y0, y1)), 0, 0) -> c(FILTER(cons(y0, y1), 0, 0)) FILTER(cons(z0, cons(y0, y1)), 0, s(y2)) -> c(FILTER(cons(y0, y1), s(y2), s(y2))) FILTER(cons(z0, cons(y0, y1)), s(s(y2)), z3) -> c1(FILTER(cons(y0, y1), s(y2), z3)) FILTER(cons(z0, cons(y0, cons(y1, y2))), s(0), 0) -> c1(FILTER(cons(y0, cons(y1, y2)), 0, 0)) FILTER(cons(z0, cons(y0, cons(y1, y2))), s(0), s(y3)) -> c1(FILTER(cons(y0, cons(y1, y2)), 0, s(y3))) SIEVE(cons(0, cons(0, y0))) -> c2(SIEVE(cons(0, y0))) SIEVE(cons(0, cons(s(0), cons(y0, y1)))) -> c2(SIEVE(cons(s(0), cons(y0, y1)))) SIEVE(cons(0, cons(s(s(y0)), cons(y1, y2)))) -> c2(SIEVE(cons(s(s(y0)), cons(y1, y2)))) S tuples: SIEVE(cons(s(0), cons(z0, z1))) -> c3(SIEVE(cons(0, filter(z1, 0, 0))), FILTER(cons(z0, z1), 0, 0)) SIEVE(cons(s(s(z2)), cons(z0, z1))) -> c3(SIEVE(cons(z0, filter(z1, z2, s(z2)))), FILTER(cons(z0, z1), s(z2), s(z2))) NATS(s(s(x0))) -> c4(NATS(s(s(s(x0))))) FILTER(cons(z0, cons(y0, y1)), 0, 0) -> c(FILTER(cons(y0, y1), 0, 0)) FILTER(cons(z0, cons(y0, y1)), 0, s(y2)) -> c(FILTER(cons(y0, y1), s(y2), s(y2))) FILTER(cons(z0, cons(y0, y1)), s(s(y2)), z3) -> c1(FILTER(cons(y0, y1), s(y2), z3)) FILTER(cons(z0, cons(y0, cons(y1, y2))), s(0), 0) -> c1(FILTER(cons(y0, cons(y1, y2)), 0, 0)) FILTER(cons(z0, cons(y0, cons(y1, y2))), s(0), s(y3)) -> c1(FILTER(cons(y0, cons(y1, y2)), 0, s(y3))) SIEVE(cons(0, cons(0, y0))) -> c2(SIEVE(cons(0, y0))) SIEVE(cons(0, cons(s(0), cons(y0, y1)))) -> c2(SIEVE(cons(s(0), cons(y0, y1)))) SIEVE(cons(0, cons(s(s(y0)), cons(y1, y2)))) -> c2(SIEVE(cons(s(s(y0)), cons(y1, y2)))) K tuples: ZPRIMES -> c6(SIEVE(nats(s(s(0))))) Defined Rule Symbols: filter_3, nats_1 Defined Pair Symbols: SIEVE_1, NATS_1, ZPRIMES, FILTER_3 Compound Symbols: c3_2, c4_1, c6_1, c_1, c1_1, c2_1 ---------------------------------------- (65) CdtNarrowingProof (BOTH BOUNDS(ID, ID)) Use narrowing to replace SIEVE(cons(s(0), cons(z0, z1))) -> c3(SIEVE(cons(0, filter(z1, 0, 0))), FILTER(cons(z0, z1), 0, 0)) by SIEVE(cons(s(0), cons(x0, cons(z0, z1)))) -> c3(SIEVE(cons(0, cons(0, filter(z1, 0, 0)))), FILTER(cons(x0, cons(z0, z1)), 0, 0)) SIEVE(cons(s(0), cons(x0, x1))) -> c3(FILTER(cons(x0, x1), 0, 0)) ---------------------------------------- (66) Obligation: Complexity Dependency Tuples Problem Rules: filter(cons(z0, z1), 0, z2) -> cons(0, filter(z1, z2, z2)) filter(cons(z0, z1), s(z2), z3) -> cons(z0, filter(z1, z2, z3)) nats(z0) -> cons(z0, nats(s(z0))) Tuples: SIEVE(cons(s(s(z2)), cons(z0, z1))) -> c3(SIEVE(cons(z0, filter(z1, z2, s(z2)))), FILTER(cons(z0, z1), s(z2), s(z2))) NATS(s(s(x0))) -> c4(NATS(s(s(s(x0))))) ZPRIMES -> c6(SIEVE(cons(s(s(0)), cons(s(s(s(0))), cons(s(s(s(s(0)))), cons(s(s(s(s(s(0))))), nats(s(s(s(s(s(s(0))))))))))))) FILTER(cons(z0, cons(y0, y1)), 0, 0) -> c(FILTER(cons(y0, y1), 0, 0)) FILTER(cons(z0, cons(y0, y1)), 0, s(y2)) -> c(FILTER(cons(y0, y1), s(y2), s(y2))) FILTER(cons(z0, cons(y0, y1)), s(s(y2)), z3) -> c1(FILTER(cons(y0, y1), s(y2), z3)) FILTER(cons(z0, cons(y0, cons(y1, y2))), s(0), 0) -> c1(FILTER(cons(y0, cons(y1, y2)), 0, 0)) FILTER(cons(z0, cons(y0, cons(y1, y2))), s(0), s(y3)) -> c1(FILTER(cons(y0, cons(y1, y2)), 0, s(y3))) SIEVE(cons(0, cons(0, y0))) -> c2(SIEVE(cons(0, y0))) SIEVE(cons(0, cons(s(0), cons(y0, y1)))) -> c2(SIEVE(cons(s(0), cons(y0, y1)))) SIEVE(cons(0, cons(s(s(y0)), cons(y1, y2)))) -> c2(SIEVE(cons(s(s(y0)), cons(y1, y2)))) SIEVE(cons(s(0), cons(x0, cons(z0, z1)))) -> c3(SIEVE(cons(0, cons(0, filter(z1, 0, 0)))), FILTER(cons(x0, cons(z0, z1)), 0, 0)) SIEVE(cons(s(0), cons(x0, x1))) -> c3(FILTER(cons(x0, x1), 0, 0)) S tuples: SIEVE(cons(s(s(z2)), cons(z0, z1))) -> c3(SIEVE(cons(z0, filter(z1, z2, s(z2)))), FILTER(cons(z0, z1), s(z2), s(z2))) NATS(s(s(x0))) -> c4(NATS(s(s(s(x0))))) FILTER(cons(z0, cons(y0, y1)), 0, 0) -> c(FILTER(cons(y0, y1), 0, 0)) FILTER(cons(z0, cons(y0, y1)), 0, s(y2)) -> c(FILTER(cons(y0, y1), s(y2), s(y2))) FILTER(cons(z0, cons(y0, y1)), s(s(y2)), z3) -> c1(FILTER(cons(y0, y1), s(y2), z3)) FILTER(cons(z0, cons(y0, cons(y1, y2))), s(0), 0) -> c1(FILTER(cons(y0, cons(y1, y2)), 0, 0)) FILTER(cons(z0, cons(y0, cons(y1, y2))), s(0), s(y3)) -> c1(FILTER(cons(y0, cons(y1, y2)), 0, s(y3))) SIEVE(cons(0, cons(0, y0))) -> c2(SIEVE(cons(0, y0))) SIEVE(cons(0, cons(s(0), cons(y0, y1)))) -> c2(SIEVE(cons(s(0), cons(y0, y1)))) SIEVE(cons(0, cons(s(s(y0)), cons(y1, y2)))) -> c2(SIEVE(cons(s(s(y0)), cons(y1, y2)))) SIEVE(cons(s(0), cons(x0, cons(z0, z1)))) -> c3(SIEVE(cons(0, cons(0, filter(z1, 0, 0)))), FILTER(cons(x0, cons(z0, z1)), 0, 0)) SIEVE(cons(s(0), cons(x0, x1))) -> c3(FILTER(cons(x0, x1), 0, 0)) K tuples: ZPRIMES -> c6(SIEVE(nats(s(s(0))))) Defined Rule Symbols: filter_3, nats_1 Defined Pair Symbols: SIEVE_1, NATS_1, ZPRIMES, FILTER_3 Compound Symbols: c3_2, c4_1, c6_1, c_1, c1_1, c2_1, c3_1 ---------------------------------------- (67) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1))) Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S. SIEVE(cons(s(0), cons(x0, x1))) -> c3(FILTER(cons(x0, x1), 0, 0)) We considered the (Usable) Rules:none And the Tuples: SIEVE(cons(s(s(z2)), cons(z0, z1))) -> c3(SIEVE(cons(z0, filter(z1, z2, s(z2)))), FILTER(cons(z0, z1), s(z2), s(z2))) NATS(s(s(x0))) -> c4(NATS(s(s(s(x0))))) ZPRIMES -> c6(SIEVE(cons(s(s(0)), cons(s(s(s(0))), cons(s(s(s(s(0)))), cons(s(s(s(s(s(0))))), nats(s(s(s(s(s(s(0))))))))))))) FILTER(cons(z0, cons(y0, y1)), 0, 0) -> c(FILTER(cons(y0, y1), 0, 0)) FILTER(cons(z0, cons(y0, y1)), 0, s(y2)) -> c(FILTER(cons(y0, y1), s(y2), s(y2))) FILTER(cons(z0, cons(y0, y1)), s(s(y2)), z3) -> c1(FILTER(cons(y0, y1), s(y2), z3)) FILTER(cons(z0, cons(y0, cons(y1, y2))), s(0), 0) -> c1(FILTER(cons(y0, cons(y1, y2)), 0, 0)) FILTER(cons(z0, cons(y0, cons(y1, y2))), s(0), s(y3)) -> c1(FILTER(cons(y0, cons(y1, y2)), 0, s(y3))) SIEVE(cons(0, cons(0, y0))) -> c2(SIEVE(cons(0, y0))) SIEVE(cons(0, cons(s(0), cons(y0, y1)))) -> c2(SIEVE(cons(s(0), cons(y0, y1)))) SIEVE(cons(0, cons(s(s(y0)), cons(y1, y2)))) -> c2(SIEVE(cons(s(s(y0)), cons(y1, y2)))) SIEVE(cons(s(0), cons(x0, cons(z0, z1)))) -> c3(SIEVE(cons(0, cons(0, filter(z1, 0, 0)))), FILTER(cons(x0, cons(z0, z1)), 0, 0)) SIEVE(cons(s(0), cons(x0, x1))) -> c3(FILTER(cons(x0, x1), 0, 0)) The order we found is given by the following interpretation: Polynomial interpretation : POL(0) = 0 POL(FILTER(x_1, x_2, x_3)) = 0 POL(NATS(x_1)) = [3]x_1 POL(SIEVE(x_1)) = [1] POL(ZPRIMES) = [1] POL(c(x_1)) = x_1 POL(c1(x_1)) = x_1 POL(c2(x_1)) = x_1 POL(c3(x_1)) = x_1 POL(c3(x_1, x_2)) = x_1 + x_2 POL(c4(x_1)) = x_1 POL(c6(x_1)) = x_1 POL(cons(x_1, x_2)) = 0 POL(filter(x_1, x_2, x_3)) = [3] POL(nats(x_1)) = [1] POL(s(x_1)) = 0 ---------------------------------------- (68) Obligation: Complexity Dependency Tuples Problem Rules: filter(cons(z0, z1), 0, z2) -> cons(0, filter(z1, z2, z2)) filter(cons(z0, z1), s(z2), z3) -> cons(z0, filter(z1, z2, z3)) nats(z0) -> cons(z0, nats(s(z0))) Tuples: SIEVE(cons(s(s(z2)), cons(z0, z1))) -> c3(SIEVE(cons(z0, filter(z1, z2, s(z2)))), FILTER(cons(z0, z1), s(z2), s(z2))) NATS(s(s(x0))) -> c4(NATS(s(s(s(x0))))) ZPRIMES -> c6(SIEVE(cons(s(s(0)), cons(s(s(s(0))), cons(s(s(s(s(0)))), cons(s(s(s(s(s(0))))), nats(s(s(s(s(s(s(0))))))))))))) FILTER(cons(z0, cons(y0, y1)), 0, 0) -> c(FILTER(cons(y0, y1), 0, 0)) FILTER(cons(z0, cons(y0, y1)), 0, s(y2)) -> c(FILTER(cons(y0, y1), s(y2), s(y2))) FILTER(cons(z0, cons(y0, y1)), s(s(y2)), z3) -> c1(FILTER(cons(y0, y1), s(y2), z3)) FILTER(cons(z0, cons(y0, cons(y1, y2))), s(0), 0) -> c1(FILTER(cons(y0, cons(y1, y2)), 0, 0)) FILTER(cons(z0, cons(y0, cons(y1, y2))), s(0), s(y3)) -> c1(FILTER(cons(y0, cons(y1, y2)), 0, s(y3))) SIEVE(cons(0, cons(0, y0))) -> c2(SIEVE(cons(0, y0))) SIEVE(cons(0, cons(s(0), cons(y0, y1)))) -> c2(SIEVE(cons(s(0), cons(y0, y1)))) SIEVE(cons(0, cons(s(s(y0)), cons(y1, y2)))) -> c2(SIEVE(cons(s(s(y0)), cons(y1, y2)))) SIEVE(cons(s(0), cons(x0, cons(z0, z1)))) -> c3(SIEVE(cons(0, cons(0, filter(z1, 0, 0)))), FILTER(cons(x0, cons(z0, z1)), 0, 0)) SIEVE(cons(s(0), cons(x0, x1))) -> c3(FILTER(cons(x0, x1), 0, 0)) S tuples: SIEVE(cons(s(s(z2)), cons(z0, z1))) -> c3(SIEVE(cons(z0, filter(z1, z2, s(z2)))), FILTER(cons(z0, z1), s(z2), s(z2))) NATS(s(s(x0))) -> c4(NATS(s(s(s(x0))))) FILTER(cons(z0, cons(y0, y1)), 0, 0) -> c(FILTER(cons(y0, y1), 0, 0)) FILTER(cons(z0, cons(y0, y1)), 0, s(y2)) -> c(FILTER(cons(y0, y1), s(y2), s(y2))) FILTER(cons(z0, cons(y0, y1)), s(s(y2)), z3) -> c1(FILTER(cons(y0, y1), s(y2), z3)) FILTER(cons(z0, cons(y0, cons(y1, y2))), s(0), 0) -> c1(FILTER(cons(y0, cons(y1, y2)), 0, 0)) FILTER(cons(z0, cons(y0, cons(y1, y2))), s(0), s(y3)) -> c1(FILTER(cons(y0, cons(y1, y2)), 0, s(y3))) SIEVE(cons(0, cons(0, y0))) -> c2(SIEVE(cons(0, y0))) SIEVE(cons(0, cons(s(0), cons(y0, y1)))) -> c2(SIEVE(cons(s(0), cons(y0, y1)))) SIEVE(cons(0, cons(s(s(y0)), cons(y1, y2)))) -> c2(SIEVE(cons(s(s(y0)), cons(y1, y2)))) SIEVE(cons(s(0), cons(x0, cons(z0, z1)))) -> c3(SIEVE(cons(0, cons(0, filter(z1, 0, 0)))), FILTER(cons(x0, cons(z0, z1)), 0, 0)) K tuples: ZPRIMES -> c6(SIEVE(nats(s(s(0))))) SIEVE(cons(s(0), cons(x0, x1))) -> c3(FILTER(cons(x0, x1), 0, 0)) Defined Rule Symbols: filter_3, nats_1 Defined Pair Symbols: SIEVE_1, NATS_1, ZPRIMES, FILTER_3 Compound Symbols: c3_2, c4_1, c6_1, c_1, c1_1, c2_1, c3_1 ---------------------------------------- (69) CdtNarrowingProof (BOTH BOUNDS(ID, ID)) Use narrowing to replace SIEVE(cons(s(s(z2)), cons(z0, z1))) -> c3(SIEVE(cons(z0, filter(z1, z2, s(z2)))), FILTER(cons(z0, z1), s(z2), s(z2))) by SIEVE(cons(s(s(0)), cons(x1, cons(z0, z1)))) -> c3(SIEVE(cons(x1, cons(0, filter(z1, s(0), s(0))))), FILTER(cons(x1, cons(z0, z1)), s(0), s(0))) SIEVE(cons(s(s(s(z2))), cons(x1, cons(z0, z1)))) -> c3(SIEVE(cons(x1, cons(z0, filter(z1, z2, s(s(z2)))))), FILTER(cons(x1, cons(z0, z1)), s(s(z2)), s(s(z2)))) SIEVE(cons(s(s(x0)), cons(x1, x2))) -> c3(FILTER(cons(x1, x2), s(x0), s(x0))) ---------------------------------------- (70) Obligation: Complexity Dependency Tuples Problem Rules: filter(cons(z0, z1), 0, z2) -> cons(0, filter(z1, z2, z2)) filter(cons(z0, z1), s(z2), z3) -> cons(z0, filter(z1, z2, z3)) nats(z0) -> cons(z0, nats(s(z0))) Tuples: NATS(s(s(x0))) -> c4(NATS(s(s(s(x0))))) ZPRIMES -> c6(SIEVE(cons(s(s(0)), cons(s(s(s(0))), cons(s(s(s(s(0)))), cons(s(s(s(s(s(0))))), nats(s(s(s(s(s(s(0))))))))))))) FILTER(cons(z0, cons(y0, y1)), 0, 0) -> c(FILTER(cons(y0, y1), 0, 0)) FILTER(cons(z0, cons(y0, y1)), 0, s(y2)) -> c(FILTER(cons(y0, y1), s(y2), s(y2))) FILTER(cons(z0, cons(y0, y1)), s(s(y2)), z3) -> c1(FILTER(cons(y0, y1), s(y2), z3)) FILTER(cons(z0, cons(y0, cons(y1, y2))), s(0), 0) -> c1(FILTER(cons(y0, cons(y1, y2)), 0, 0)) FILTER(cons(z0, cons(y0, cons(y1, y2))), s(0), s(y3)) -> c1(FILTER(cons(y0, cons(y1, y2)), 0, s(y3))) SIEVE(cons(0, cons(0, y0))) -> c2(SIEVE(cons(0, y0))) SIEVE(cons(0, cons(s(0), cons(y0, y1)))) -> c2(SIEVE(cons(s(0), cons(y0, y1)))) SIEVE(cons(0, cons(s(s(y0)), cons(y1, y2)))) -> c2(SIEVE(cons(s(s(y0)), cons(y1, y2)))) SIEVE(cons(s(0), cons(x0, cons(z0, z1)))) -> c3(SIEVE(cons(0, cons(0, filter(z1, 0, 0)))), FILTER(cons(x0, cons(z0, z1)), 0, 0)) SIEVE(cons(s(0), cons(x0, x1))) -> c3(FILTER(cons(x0, x1), 0, 0)) SIEVE(cons(s(s(0)), cons(x1, cons(z0, z1)))) -> c3(SIEVE(cons(x1, cons(0, filter(z1, s(0), s(0))))), FILTER(cons(x1, cons(z0, z1)), s(0), s(0))) SIEVE(cons(s(s(s(z2))), cons(x1, cons(z0, z1)))) -> c3(SIEVE(cons(x1, cons(z0, filter(z1, z2, s(s(z2)))))), FILTER(cons(x1, cons(z0, z1)), s(s(z2)), s(s(z2)))) SIEVE(cons(s(s(x0)), cons(x1, x2))) -> c3(FILTER(cons(x1, x2), s(x0), s(x0))) S tuples: NATS(s(s(x0))) -> c4(NATS(s(s(s(x0))))) FILTER(cons(z0, cons(y0, y1)), 0, 0) -> c(FILTER(cons(y0, y1), 0, 0)) FILTER(cons(z0, cons(y0, y1)), 0, s(y2)) -> c(FILTER(cons(y0, y1), s(y2), s(y2))) FILTER(cons(z0, cons(y0, y1)), s(s(y2)), z3) -> c1(FILTER(cons(y0, y1), s(y2), z3)) FILTER(cons(z0, cons(y0, cons(y1, y2))), s(0), 0) -> c1(FILTER(cons(y0, cons(y1, y2)), 0, 0)) FILTER(cons(z0, cons(y0, cons(y1, y2))), s(0), s(y3)) -> c1(FILTER(cons(y0, cons(y1, y2)), 0, s(y3))) SIEVE(cons(0, cons(0, y0))) -> c2(SIEVE(cons(0, y0))) SIEVE(cons(0, cons(s(0), cons(y0, y1)))) -> c2(SIEVE(cons(s(0), cons(y0, y1)))) SIEVE(cons(0, cons(s(s(y0)), cons(y1, y2)))) -> c2(SIEVE(cons(s(s(y0)), cons(y1, y2)))) SIEVE(cons(s(0), cons(x0, cons(z0, z1)))) -> c3(SIEVE(cons(0, cons(0, filter(z1, 0, 0)))), FILTER(cons(x0, cons(z0, z1)), 0, 0)) SIEVE(cons(s(s(0)), cons(x1, cons(z0, z1)))) -> c3(SIEVE(cons(x1, cons(0, filter(z1, s(0), s(0))))), FILTER(cons(x1, cons(z0, z1)), s(0), s(0))) SIEVE(cons(s(s(s(z2))), cons(x1, cons(z0, z1)))) -> c3(SIEVE(cons(x1, cons(z0, filter(z1, z2, s(s(z2)))))), FILTER(cons(x1, cons(z0, z1)), s(s(z2)), s(s(z2)))) SIEVE(cons(s(s(x0)), cons(x1, x2))) -> c3(FILTER(cons(x1, x2), s(x0), s(x0))) K tuples: ZPRIMES -> c6(SIEVE(nats(s(s(0))))) SIEVE(cons(s(0), cons(x0, x1))) -> c3(FILTER(cons(x0, x1), 0, 0)) Defined Rule Symbols: filter_3, nats_1 Defined Pair Symbols: NATS_1, ZPRIMES, FILTER_3, SIEVE_1 Compound Symbols: c4_1, c6_1, c_1, c1_1, c2_1, c3_2, c3_1 ---------------------------------------- (71) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1))) Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S. SIEVE(cons(s(s(x0)), cons(x1, x2))) -> c3(FILTER(cons(x1, x2), s(x0), s(x0))) We considered the (Usable) Rules:none And the Tuples: NATS(s(s(x0))) -> c4(NATS(s(s(s(x0))))) ZPRIMES -> c6(SIEVE(cons(s(s(0)), cons(s(s(s(0))), cons(s(s(s(s(0)))), cons(s(s(s(s(s(0))))), nats(s(s(s(s(s(s(0))))))))))))) FILTER(cons(z0, cons(y0, y1)), 0, 0) -> c(FILTER(cons(y0, y1), 0, 0)) FILTER(cons(z0, cons(y0, y1)), 0, s(y2)) -> c(FILTER(cons(y0, y1), s(y2), s(y2))) FILTER(cons(z0, cons(y0, y1)), s(s(y2)), z3) -> c1(FILTER(cons(y0, y1), s(y2), z3)) FILTER(cons(z0, cons(y0, cons(y1, y2))), s(0), 0) -> c1(FILTER(cons(y0, cons(y1, y2)), 0, 0)) FILTER(cons(z0, cons(y0, cons(y1, y2))), s(0), s(y3)) -> c1(FILTER(cons(y0, cons(y1, y2)), 0, s(y3))) SIEVE(cons(0, cons(0, y0))) -> c2(SIEVE(cons(0, y0))) SIEVE(cons(0, cons(s(0), cons(y0, y1)))) -> c2(SIEVE(cons(s(0), cons(y0, y1)))) SIEVE(cons(0, cons(s(s(y0)), cons(y1, y2)))) -> c2(SIEVE(cons(s(s(y0)), cons(y1, y2)))) SIEVE(cons(s(0), cons(x0, cons(z0, z1)))) -> c3(SIEVE(cons(0, cons(0, filter(z1, 0, 0)))), FILTER(cons(x0, cons(z0, z1)), 0, 0)) SIEVE(cons(s(0), cons(x0, x1))) -> c3(FILTER(cons(x0, x1), 0, 0)) SIEVE(cons(s(s(0)), cons(x1, cons(z0, z1)))) -> c3(SIEVE(cons(x1, cons(0, filter(z1, s(0), s(0))))), FILTER(cons(x1, cons(z0, z1)), s(0), s(0))) SIEVE(cons(s(s(s(z2))), cons(x1, cons(z0, z1)))) -> c3(SIEVE(cons(x1, cons(z0, filter(z1, z2, s(s(z2)))))), FILTER(cons(x1, cons(z0, z1)), s(s(z2)), s(s(z2)))) SIEVE(cons(s(s(x0)), cons(x1, x2))) -> c3(FILTER(cons(x1, x2), s(x0), s(x0))) The order we found is given by the following interpretation: Polynomial interpretation : POL(0) = 0 POL(FILTER(x_1, x_2, x_3)) = 0 POL(NATS(x_1)) = [3]x_1 POL(SIEVE(x_1)) = [1] POL(ZPRIMES) = [1] POL(c(x_1)) = x_1 POL(c1(x_1)) = x_1 POL(c2(x_1)) = x_1 POL(c3(x_1)) = x_1 POL(c3(x_1, x_2)) = x_1 + x_2 POL(c4(x_1)) = x_1 POL(c6(x_1)) = x_1 POL(cons(x_1, x_2)) = [1] + x_2 POL(filter(x_1, x_2, x_3)) = [2] + [2]x_1 POL(nats(x_1)) = 0 POL(s(x_1)) = 0 ---------------------------------------- (72) Obligation: Complexity Dependency Tuples Problem Rules: filter(cons(z0, z1), 0, z2) -> cons(0, filter(z1, z2, z2)) filter(cons(z0, z1), s(z2), z3) -> cons(z0, filter(z1, z2, z3)) nats(z0) -> cons(z0, nats(s(z0))) Tuples: NATS(s(s(x0))) -> c4(NATS(s(s(s(x0))))) ZPRIMES -> c6(SIEVE(cons(s(s(0)), cons(s(s(s(0))), cons(s(s(s(s(0)))), cons(s(s(s(s(s(0))))), nats(s(s(s(s(s(s(0))))))))))))) FILTER(cons(z0, cons(y0, y1)), 0, 0) -> c(FILTER(cons(y0, y1), 0, 0)) FILTER(cons(z0, cons(y0, y1)), 0, s(y2)) -> c(FILTER(cons(y0, y1), s(y2), s(y2))) FILTER(cons(z0, cons(y0, y1)), s(s(y2)), z3) -> c1(FILTER(cons(y0, y1), s(y2), z3)) FILTER(cons(z0, cons(y0, cons(y1, y2))), s(0), 0) -> c1(FILTER(cons(y0, cons(y1, y2)), 0, 0)) FILTER(cons(z0, cons(y0, cons(y1, y2))), s(0), s(y3)) -> c1(FILTER(cons(y0, cons(y1, y2)), 0, s(y3))) SIEVE(cons(0, cons(0, y0))) -> c2(SIEVE(cons(0, y0))) SIEVE(cons(0, cons(s(0), cons(y0, y1)))) -> c2(SIEVE(cons(s(0), cons(y0, y1)))) SIEVE(cons(0, cons(s(s(y0)), cons(y1, y2)))) -> c2(SIEVE(cons(s(s(y0)), cons(y1, y2)))) SIEVE(cons(s(0), cons(x0, cons(z0, z1)))) -> c3(SIEVE(cons(0, cons(0, filter(z1, 0, 0)))), FILTER(cons(x0, cons(z0, z1)), 0, 0)) SIEVE(cons(s(0), cons(x0, x1))) -> c3(FILTER(cons(x0, x1), 0, 0)) SIEVE(cons(s(s(0)), cons(x1, cons(z0, z1)))) -> c3(SIEVE(cons(x1, cons(0, filter(z1, s(0), s(0))))), FILTER(cons(x1, cons(z0, z1)), s(0), s(0))) SIEVE(cons(s(s(s(z2))), cons(x1, cons(z0, z1)))) -> c3(SIEVE(cons(x1, cons(z0, filter(z1, z2, s(s(z2)))))), FILTER(cons(x1, cons(z0, z1)), s(s(z2)), s(s(z2)))) SIEVE(cons(s(s(x0)), cons(x1, x2))) -> c3(FILTER(cons(x1, x2), s(x0), s(x0))) S tuples: NATS(s(s(x0))) -> c4(NATS(s(s(s(x0))))) FILTER(cons(z0, cons(y0, y1)), 0, 0) -> c(FILTER(cons(y0, y1), 0, 0)) FILTER(cons(z0, cons(y0, y1)), 0, s(y2)) -> c(FILTER(cons(y0, y1), s(y2), s(y2))) FILTER(cons(z0, cons(y0, y1)), s(s(y2)), z3) -> c1(FILTER(cons(y0, y1), s(y2), z3)) FILTER(cons(z0, cons(y0, cons(y1, y2))), s(0), 0) -> c1(FILTER(cons(y0, cons(y1, y2)), 0, 0)) FILTER(cons(z0, cons(y0, cons(y1, y2))), s(0), s(y3)) -> c1(FILTER(cons(y0, cons(y1, y2)), 0, s(y3))) SIEVE(cons(0, cons(0, y0))) -> c2(SIEVE(cons(0, y0))) SIEVE(cons(0, cons(s(0), cons(y0, y1)))) -> c2(SIEVE(cons(s(0), cons(y0, y1)))) SIEVE(cons(0, cons(s(s(y0)), cons(y1, y2)))) -> c2(SIEVE(cons(s(s(y0)), cons(y1, y2)))) SIEVE(cons(s(0), cons(x0, cons(z0, z1)))) -> c3(SIEVE(cons(0, cons(0, filter(z1, 0, 0)))), FILTER(cons(x0, cons(z0, z1)), 0, 0)) SIEVE(cons(s(s(0)), cons(x1, cons(z0, z1)))) -> c3(SIEVE(cons(x1, cons(0, filter(z1, s(0), s(0))))), FILTER(cons(x1, cons(z0, z1)), s(0), s(0))) SIEVE(cons(s(s(s(z2))), cons(x1, cons(z0, z1)))) -> c3(SIEVE(cons(x1, cons(z0, filter(z1, z2, s(s(z2)))))), FILTER(cons(x1, cons(z0, z1)), s(s(z2)), s(s(z2)))) K tuples: ZPRIMES -> c6(SIEVE(nats(s(s(0))))) SIEVE(cons(s(0), cons(x0, x1))) -> c3(FILTER(cons(x0, x1), 0, 0)) SIEVE(cons(s(s(x0)), cons(x1, x2))) -> c3(FILTER(cons(x1, x2), s(x0), s(x0))) Defined Rule Symbols: filter_3, nats_1 Defined Pair Symbols: NATS_1, ZPRIMES, FILTER_3, SIEVE_1 Compound Symbols: c4_1, c6_1, c_1, c1_1, c2_1, c3_2, c3_1 ---------------------------------------- (73) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID)) Use forward instantiation to replace FILTER(cons(z0, cons(y0, y1)), 0, 0) -> c(FILTER(cons(y0, y1), 0, 0)) by FILTER(cons(z0, cons(z1, cons(y1, y2))), 0, 0) -> c(FILTER(cons(z1, cons(y1, y2)), 0, 0)) ---------------------------------------- (74) Obligation: Complexity Dependency Tuples Problem Rules: filter(cons(z0, z1), 0, z2) -> cons(0, filter(z1, z2, z2)) filter(cons(z0, z1), s(z2), z3) -> cons(z0, filter(z1, z2, z3)) nats(z0) -> cons(z0, nats(s(z0))) Tuples: NATS(s(s(x0))) -> c4(NATS(s(s(s(x0))))) ZPRIMES -> c6(SIEVE(cons(s(s(0)), cons(s(s(s(0))), cons(s(s(s(s(0)))), cons(s(s(s(s(s(0))))), nats(s(s(s(s(s(s(0))))))))))))) FILTER(cons(z0, cons(y0, y1)), 0, s(y2)) -> c(FILTER(cons(y0, y1), s(y2), s(y2))) FILTER(cons(z0, cons(y0, y1)), s(s(y2)), z3) -> c1(FILTER(cons(y0, y1), s(y2), z3)) FILTER(cons(z0, cons(y0, cons(y1, y2))), s(0), 0) -> c1(FILTER(cons(y0, cons(y1, y2)), 0, 0)) FILTER(cons(z0, cons(y0, cons(y1, y2))), s(0), s(y3)) -> c1(FILTER(cons(y0, cons(y1, y2)), 0, s(y3))) SIEVE(cons(0, cons(0, y0))) -> c2(SIEVE(cons(0, y0))) SIEVE(cons(0, cons(s(0), cons(y0, y1)))) -> c2(SIEVE(cons(s(0), cons(y0, y1)))) SIEVE(cons(0, cons(s(s(y0)), cons(y1, y2)))) -> c2(SIEVE(cons(s(s(y0)), cons(y1, y2)))) SIEVE(cons(s(0), cons(x0, cons(z0, z1)))) -> c3(SIEVE(cons(0, cons(0, filter(z1, 0, 0)))), FILTER(cons(x0, cons(z0, z1)), 0, 0)) SIEVE(cons(s(0), cons(x0, x1))) -> c3(FILTER(cons(x0, x1), 0, 0)) SIEVE(cons(s(s(0)), cons(x1, cons(z0, z1)))) -> c3(SIEVE(cons(x1, cons(0, filter(z1, s(0), s(0))))), FILTER(cons(x1, cons(z0, z1)), s(0), s(0))) SIEVE(cons(s(s(s(z2))), cons(x1, cons(z0, z1)))) -> c3(SIEVE(cons(x1, cons(z0, filter(z1, z2, s(s(z2)))))), FILTER(cons(x1, cons(z0, z1)), s(s(z2)), s(s(z2)))) SIEVE(cons(s(s(x0)), cons(x1, x2))) -> c3(FILTER(cons(x1, x2), s(x0), s(x0))) FILTER(cons(z0, cons(z1, cons(y1, y2))), 0, 0) -> c(FILTER(cons(z1, cons(y1, y2)), 0, 0)) S tuples: NATS(s(s(x0))) -> c4(NATS(s(s(s(x0))))) FILTER(cons(z0, cons(y0, y1)), 0, s(y2)) -> c(FILTER(cons(y0, y1), s(y2), s(y2))) FILTER(cons(z0, cons(y0, y1)), s(s(y2)), z3) -> c1(FILTER(cons(y0, y1), s(y2), z3)) FILTER(cons(z0, cons(y0, cons(y1, y2))), s(0), 0) -> c1(FILTER(cons(y0, cons(y1, y2)), 0, 0)) FILTER(cons(z0, cons(y0, cons(y1, y2))), s(0), s(y3)) -> c1(FILTER(cons(y0, cons(y1, y2)), 0, s(y3))) SIEVE(cons(0, cons(0, y0))) -> c2(SIEVE(cons(0, y0))) SIEVE(cons(0, cons(s(0), cons(y0, y1)))) -> c2(SIEVE(cons(s(0), cons(y0, y1)))) SIEVE(cons(0, cons(s(s(y0)), cons(y1, y2)))) -> c2(SIEVE(cons(s(s(y0)), cons(y1, y2)))) SIEVE(cons(s(0), cons(x0, cons(z0, z1)))) -> c3(SIEVE(cons(0, cons(0, filter(z1, 0, 0)))), FILTER(cons(x0, cons(z0, z1)), 0, 0)) SIEVE(cons(s(s(0)), cons(x1, cons(z0, z1)))) -> c3(SIEVE(cons(x1, cons(0, filter(z1, s(0), s(0))))), FILTER(cons(x1, cons(z0, z1)), s(0), s(0))) SIEVE(cons(s(s(s(z2))), cons(x1, cons(z0, z1)))) -> c3(SIEVE(cons(x1, cons(z0, filter(z1, z2, s(s(z2)))))), FILTER(cons(x1, cons(z0, z1)), s(s(z2)), s(s(z2)))) FILTER(cons(z0, cons(z1, cons(y1, y2))), 0, 0) -> c(FILTER(cons(z1, cons(y1, y2)), 0, 0)) K tuples: ZPRIMES -> c6(SIEVE(nats(s(s(0))))) SIEVE(cons(s(0), cons(x0, x1))) -> c3(FILTER(cons(x0, x1), 0, 0)) SIEVE(cons(s(s(x0)), cons(x1, x2))) -> c3(FILTER(cons(x1, x2), s(x0), s(x0))) Defined Rule Symbols: filter_3, nats_1 Defined Pair Symbols: NATS_1, ZPRIMES, FILTER_3, SIEVE_1 Compound Symbols: c4_1, c6_1, c_1, c1_1, c2_1, c3_2, c3_1 ---------------------------------------- (75) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID)) Use forward instantiation to replace FILTER(cons(z0, cons(y0, y1)), 0, s(y2)) -> c(FILTER(cons(y0, y1), s(y2), s(y2))) by FILTER(cons(z0, cons(z1, cons(y1, y2))), 0, s(s(y3))) -> c(FILTER(cons(z1, cons(y1, y2)), s(s(y3)), s(s(y3)))) FILTER(cons(z0, cons(z1, cons(y1, cons(y2, y3)))), 0, s(0)) -> c(FILTER(cons(z1, cons(y1, cons(y2, y3))), s(0), s(0))) ---------------------------------------- (76) Obligation: Complexity Dependency Tuples Problem Rules: filter(cons(z0, z1), 0, z2) -> cons(0, filter(z1, z2, z2)) filter(cons(z0, z1), s(z2), z3) -> cons(z0, filter(z1, z2, z3)) nats(z0) -> cons(z0, nats(s(z0))) Tuples: NATS(s(s(x0))) -> c4(NATS(s(s(s(x0))))) ZPRIMES -> c6(SIEVE(cons(s(s(0)), cons(s(s(s(0))), cons(s(s(s(s(0)))), cons(s(s(s(s(s(0))))), nats(s(s(s(s(s(s(0))))))))))))) FILTER(cons(z0, cons(y0, y1)), s(s(y2)), z3) -> c1(FILTER(cons(y0, y1), s(y2), z3)) FILTER(cons(z0, cons(y0, cons(y1, y2))), s(0), 0) -> c1(FILTER(cons(y0, cons(y1, y2)), 0, 0)) FILTER(cons(z0, cons(y0, cons(y1, y2))), s(0), s(y3)) -> c1(FILTER(cons(y0, cons(y1, y2)), 0, s(y3))) SIEVE(cons(0, cons(0, y0))) -> c2(SIEVE(cons(0, y0))) SIEVE(cons(0, cons(s(0), cons(y0, y1)))) -> c2(SIEVE(cons(s(0), cons(y0, y1)))) SIEVE(cons(0, cons(s(s(y0)), cons(y1, y2)))) -> c2(SIEVE(cons(s(s(y0)), cons(y1, y2)))) SIEVE(cons(s(0), cons(x0, cons(z0, z1)))) -> c3(SIEVE(cons(0, cons(0, filter(z1, 0, 0)))), FILTER(cons(x0, cons(z0, z1)), 0, 0)) SIEVE(cons(s(0), cons(x0, x1))) -> c3(FILTER(cons(x0, x1), 0, 0)) SIEVE(cons(s(s(0)), cons(x1, cons(z0, z1)))) -> c3(SIEVE(cons(x1, cons(0, filter(z1, s(0), s(0))))), FILTER(cons(x1, cons(z0, z1)), s(0), s(0))) SIEVE(cons(s(s(s(z2))), cons(x1, cons(z0, z1)))) -> c3(SIEVE(cons(x1, cons(z0, filter(z1, z2, s(s(z2)))))), FILTER(cons(x1, cons(z0, z1)), s(s(z2)), s(s(z2)))) SIEVE(cons(s(s(x0)), cons(x1, x2))) -> c3(FILTER(cons(x1, x2), s(x0), s(x0))) FILTER(cons(z0, cons(z1, cons(y1, y2))), 0, 0) -> c(FILTER(cons(z1, cons(y1, y2)), 0, 0)) FILTER(cons(z0, cons(z1, cons(y1, y2))), 0, s(s(y3))) -> c(FILTER(cons(z1, cons(y1, y2)), s(s(y3)), s(s(y3)))) FILTER(cons(z0, cons(z1, cons(y1, cons(y2, y3)))), 0, s(0)) -> c(FILTER(cons(z1, cons(y1, cons(y2, y3))), s(0), s(0))) S tuples: NATS(s(s(x0))) -> c4(NATS(s(s(s(x0))))) FILTER(cons(z0, cons(y0, y1)), s(s(y2)), z3) -> c1(FILTER(cons(y0, y1), s(y2), z3)) FILTER(cons(z0, cons(y0, cons(y1, y2))), s(0), 0) -> c1(FILTER(cons(y0, cons(y1, y2)), 0, 0)) FILTER(cons(z0, cons(y0, cons(y1, y2))), s(0), s(y3)) -> c1(FILTER(cons(y0, cons(y1, y2)), 0, s(y3))) SIEVE(cons(0, cons(0, y0))) -> c2(SIEVE(cons(0, y0))) SIEVE(cons(0, cons(s(0), cons(y0, y1)))) -> c2(SIEVE(cons(s(0), cons(y0, y1)))) SIEVE(cons(0, cons(s(s(y0)), cons(y1, y2)))) -> c2(SIEVE(cons(s(s(y0)), cons(y1, y2)))) SIEVE(cons(s(0), cons(x0, cons(z0, z1)))) -> c3(SIEVE(cons(0, cons(0, filter(z1, 0, 0)))), FILTER(cons(x0, cons(z0, z1)), 0, 0)) SIEVE(cons(s(s(0)), cons(x1, cons(z0, z1)))) -> c3(SIEVE(cons(x1, cons(0, filter(z1, s(0), s(0))))), FILTER(cons(x1, cons(z0, z1)), s(0), s(0))) SIEVE(cons(s(s(s(z2))), cons(x1, cons(z0, z1)))) -> c3(SIEVE(cons(x1, cons(z0, filter(z1, z2, s(s(z2)))))), FILTER(cons(x1, cons(z0, z1)), s(s(z2)), s(s(z2)))) FILTER(cons(z0, cons(z1, cons(y1, y2))), 0, 0) -> c(FILTER(cons(z1, cons(y1, y2)), 0, 0)) FILTER(cons(z0, cons(z1, cons(y1, y2))), 0, s(s(y3))) -> c(FILTER(cons(z1, cons(y1, y2)), s(s(y3)), s(s(y3)))) FILTER(cons(z0, cons(z1, cons(y1, cons(y2, y3)))), 0, s(0)) -> c(FILTER(cons(z1, cons(y1, cons(y2, y3))), s(0), s(0))) K tuples: ZPRIMES -> c6(SIEVE(nats(s(s(0))))) SIEVE(cons(s(0), cons(x0, x1))) -> c3(FILTER(cons(x0, x1), 0, 0)) SIEVE(cons(s(s(x0)), cons(x1, x2))) -> c3(FILTER(cons(x1, x2), s(x0), s(x0))) Defined Rule Symbols: filter_3, nats_1 Defined Pair Symbols: NATS_1, ZPRIMES, FILTER_3, SIEVE_1 Compound Symbols: c4_1, c6_1, c1_1, c2_1, c3_2, c3_1, c_1 ---------------------------------------- (77) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID)) Use forward instantiation to replace FILTER(cons(z0, cons(y0, y1)), s(s(y2)), z3) -> c1(FILTER(cons(y0, y1), s(y2), z3)) by FILTER(cons(z0, cons(z1, cons(y1, y2))), s(s(s(y3))), z4) -> c1(FILTER(cons(z1, cons(y1, y2)), s(s(y3)), z4)) FILTER(cons(z0, cons(z1, cons(y1, cons(y2, y3)))), s(s(0)), 0) -> c1(FILTER(cons(z1, cons(y1, cons(y2, y3))), s(0), 0)) FILTER(cons(z0, cons(z1, cons(y1, cons(y2, y3)))), s(s(0)), s(y4)) -> c1(FILTER(cons(z1, cons(y1, cons(y2, y3))), s(0), s(y4))) ---------------------------------------- (78) Obligation: Complexity Dependency Tuples Problem Rules: filter(cons(z0, z1), 0, z2) -> cons(0, filter(z1, z2, z2)) filter(cons(z0, z1), s(z2), z3) -> cons(z0, filter(z1, z2, z3)) nats(z0) -> cons(z0, nats(s(z0))) Tuples: NATS(s(s(x0))) -> c4(NATS(s(s(s(x0))))) ZPRIMES -> c6(SIEVE(cons(s(s(0)), cons(s(s(s(0))), cons(s(s(s(s(0)))), cons(s(s(s(s(s(0))))), nats(s(s(s(s(s(s(0))))))))))))) FILTER(cons(z0, cons(y0, cons(y1, y2))), s(0), 0) -> c1(FILTER(cons(y0, cons(y1, y2)), 0, 0)) FILTER(cons(z0, cons(y0, cons(y1, y2))), s(0), s(y3)) -> c1(FILTER(cons(y0, cons(y1, y2)), 0, s(y3))) SIEVE(cons(0, cons(0, y0))) -> c2(SIEVE(cons(0, y0))) SIEVE(cons(0, cons(s(0), cons(y0, y1)))) -> c2(SIEVE(cons(s(0), cons(y0, y1)))) SIEVE(cons(0, cons(s(s(y0)), cons(y1, y2)))) -> c2(SIEVE(cons(s(s(y0)), cons(y1, y2)))) SIEVE(cons(s(0), cons(x0, cons(z0, z1)))) -> c3(SIEVE(cons(0, cons(0, filter(z1, 0, 0)))), FILTER(cons(x0, cons(z0, z1)), 0, 0)) SIEVE(cons(s(0), cons(x0, x1))) -> c3(FILTER(cons(x0, x1), 0, 0)) SIEVE(cons(s(s(0)), cons(x1, cons(z0, z1)))) -> c3(SIEVE(cons(x1, cons(0, filter(z1, s(0), s(0))))), FILTER(cons(x1, cons(z0, z1)), s(0), s(0))) SIEVE(cons(s(s(s(z2))), cons(x1, cons(z0, z1)))) -> c3(SIEVE(cons(x1, cons(z0, filter(z1, z2, s(s(z2)))))), FILTER(cons(x1, cons(z0, z1)), s(s(z2)), s(s(z2)))) SIEVE(cons(s(s(x0)), cons(x1, x2))) -> c3(FILTER(cons(x1, x2), s(x0), s(x0))) FILTER(cons(z0, cons(z1, cons(y1, y2))), 0, 0) -> c(FILTER(cons(z1, cons(y1, y2)), 0, 0)) FILTER(cons(z0, cons(z1, cons(y1, y2))), 0, s(s(y3))) -> c(FILTER(cons(z1, cons(y1, y2)), s(s(y3)), s(s(y3)))) FILTER(cons(z0, cons(z1, cons(y1, cons(y2, y3)))), 0, s(0)) -> c(FILTER(cons(z1, cons(y1, cons(y2, y3))), s(0), s(0))) FILTER(cons(z0, cons(z1, cons(y1, y2))), s(s(s(y3))), z4) -> c1(FILTER(cons(z1, cons(y1, y2)), s(s(y3)), z4)) FILTER(cons(z0, cons(z1, cons(y1, cons(y2, y3)))), s(s(0)), 0) -> c1(FILTER(cons(z1, cons(y1, cons(y2, y3))), s(0), 0)) FILTER(cons(z0, cons(z1, cons(y1, cons(y2, y3)))), s(s(0)), s(y4)) -> c1(FILTER(cons(z1, cons(y1, cons(y2, y3))), s(0), s(y4))) S tuples: NATS(s(s(x0))) -> c4(NATS(s(s(s(x0))))) FILTER(cons(z0, cons(y0, cons(y1, y2))), s(0), 0) -> c1(FILTER(cons(y0, cons(y1, y2)), 0, 0)) FILTER(cons(z0, cons(y0, cons(y1, y2))), s(0), s(y3)) -> c1(FILTER(cons(y0, cons(y1, y2)), 0, s(y3))) SIEVE(cons(0, cons(0, y0))) -> c2(SIEVE(cons(0, y0))) SIEVE(cons(0, cons(s(0), cons(y0, y1)))) -> c2(SIEVE(cons(s(0), cons(y0, y1)))) SIEVE(cons(0, cons(s(s(y0)), cons(y1, y2)))) -> c2(SIEVE(cons(s(s(y0)), cons(y1, y2)))) SIEVE(cons(s(0), cons(x0, cons(z0, z1)))) -> c3(SIEVE(cons(0, cons(0, filter(z1, 0, 0)))), FILTER(cons(x0, cons(z0, z1)), 0, 0)) SIEVE(cons(s(s(0)), cons(x1, cons(z0, z1)))) -> c3(SIEVE(cons(x1, cons(0, filter(z1, s(0), s(0))))), FILTER(cons(x1, cons(z0, z1)), s(0), s(0))) SIEVE(cons(s(s(s(z2))), cons(x1, cons(z0, z1)))) -> c3(SIEVE(cons(x1, cons(z0, filter(z1, z2, s(s(z2)))))), FILTER(cons(x1, cons(z0, z1)), s(s(z2)), s(s(z2)))) FILTER(cons(z0, cons(z1, cons(y1, y2))), 0, 0) -> c(FILTER(cons(z1, cons(y1, y2)), 0, 0)) FILTER(cons(z0, cons(z1, cons(y1, y2))), 0, s(s(y3))) -> c(FILTER(cons(z1, cons(y1, y2)), s(s(y3)), s(s(y3)))) FILTER(cons(z0, cons(z1, cons(y1, cons(y2, y3)))), 0, s(0)) -> c(FILTER(cons(z1, cons(y1, cons(y2, y3))), s(0), s(0))) FILTER(cons(z0, cons(z1, cons(y1, y2))), s(s(s(y3))), z4) -> c1(FILTER(cons(z1, cons(y1, y2)), s(s(y3)), z4)) FILTER(cons(z0, cons(z1, cons(y1, cons(y2, y3)))), s(s(0)), 0) -> c1(FILTER(cons(z1, cons(y1, cons(y2, y3))), s(0), 0)) FILTER(cons(z0, cons(z1, cons(y1, cons(y2, y3)))), s(s(0)), s(y4)) -> c1(FILTER(cons(z1, cons(y1, cons(y2, y3))), s(0), s(y4))) K tuples: ZPRIMES -> c6(SIEVE(nats(s(s(0))))) SIEVE(cons(s(0), cons(x0, x1))) -> c3(FILTER(cons(x0, x1), 0, 0)) SIEVE(cons(s(s(x0)), cons(x1, x2))) -> c3(FILTER(cons(x1, x2), s(x0), s(x0))) Defined Rule Symbols: filter_3, nats_1 Defined Pair Symbols: NATS_1, ZPRIMES, FILTER_3, SIEVE_1 Compound Symbols: c4_1, c6_1, c1_1, c2_1, c3_2, c3_1, c_1 ---------------------------------------- (79) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID)) Use forward instantiation to replace FILTER(cons(z0, cons(y0, cons(y1, y2))), s(0), 0) -> c1(FILTER(cons(y0, cons(y1, y2)), 0, 0)) by FILTER(cons(z0, cons(z1, cons(z2, cons(y2, y3)))), s(0), 0) -> c1(FILTER(cons(z1, cons(z2, cons(y2, y3))), 0, 0)) ---------------------------------------- (80) Obligation: Complexity Dependency Tuples Problem Rules: filter(cons(z0, z1), 0, z2) -> cons(0, filter(z1, z2, z2)) filter(cons(z0, z1), s(z2), z3) -> cons(z0, filter(z1, z2, z3)) nats(z0) -> cons(z0, nats(s(z0))) Tuples: NATS(s(s(x0))) -> c4(NATS(s(s(s(x0))))) ZPRIMES -> c6(SIEVE(cons(s(s(0)), cons(s(s(s(0))), cons(s(s(s(s(0)))), cons(s(s(s(s(s(0))))), nats(s(s(s(s(s(s(0))))))))))))) FILTER(cons(z0, cons(y0, cons(y1, y2))), s(0), s(y3)) -> c1(FILTER(cons(y0, cons(y1, y2)), 0, s(y3))) SIEVE(cons(0, cons(0, y0))) -> c2(SIEVE(cons(0, y0))) SIEVE(cons(0, cons(s(0), cons(y0, y1)))) -> c2(SIEVE(cons(s(0), cons(y0, y1)))) SIEVE(cons(0, cons(s(s(y0)), cons(y1, y2)))) -> c2(SIEVE(cons(s(s(y0)), cons(y1, y2)))) SIEVE(cons(s(0), cons(x0, cons(z0, z1)))) -> c3(SIEVE(cons(0, cons(0, filter(z1, 0, 0)))), FILTER(cons(x0, cons(z0, z1)), 0, 0)) SIEVE(cons(s(0), cons(x0, x1))) -> c3(FILTER(cons(x0, x1), 0, 0)) SIEVE(cons(s(s(0)), cons(x1, cons(z0, z1)))) -> c3(SIEVE(cons(x1, cons(0, filter(z1, s(0), s(0))))), FILTER(cons(x1, cons(z0, z1)), s(0), s(0))) SIEVE(cons(s(s(s(z2))), cons(x1, cons(z0, z1)))) -> c3(SIEVE(cons(x1, cons(z0, filter(z1, z2, s(s(z2)))))), FILTER(cons(x1, cons(z0, z1)), s(s(z2)), s(s(z2)))) SIEVE(cons(s(s(x0)), cons(x1, x2))) -> c3(FILTER(cons(x1, x2), s(x0), s(x0))) FILTER(cons(z0, cons(z1, cons(y1, y2))), 0, 0) -> c(FILTER(cons(z1, cons(y1, y2)), 0, 0)) FILTER(cons(z0, cons(z1, cons(y1, y2))), 0, s(s(y3))) -> c(FILTER(cons(z1, cons(y1, y2)), s(s(y3)), s(s(y3)))) FILTER(cons(z0, cons(z1, cons(y1, cons(y2, y3)))), 0, s(0)) -> c(FILTER(cons(z1, cons(y1, cons(y2, y3))), s(0), s(0))) FILTER(cons(z0, cons(z1, cons(y1, y2))), s(s(s(y3))), z4) -> c1(FILTER(cons(z1, cons(y1, y2)), s(s(y3)), z4)) FILTER(cons(z0, cons(z1, cons(y1, cons(y2, y3)))), s(s(0)), 0) -> c1(FILTER(cons(z1, cons(y1, cons(y2, y3))), s(0), 0)) FILTER(cons(z0, cons(z1, cons(y1, cons(y2, y3)))), s(s(0)), s(y4)) -> c1(FILTER(cons(z1, cons(y1, cons(y2, y3))), s(0), s(y4))) FILTER(cons(z0, cons(z1, cons(z2, cons(y2, y3)))), s(0), 0) -> c1(FILTER(cons(z1, cons(z2, cons(y2, y3))), 0, 0)) S tuples: NATS(s(s(x0))) -> c4(NATS(s(s(s(x0))))) FILTER(cons(z0, cons(y0, cons(y1, y2))), s(0), s(y3)) -> c1(FILTER(cons(y0, cons(y1, y2)), 0, s(y3))) SIEVE(cons(0, cons(0, y0))) -> c2(SIEVE(cons(0, y0))) SIEVE(cons(0, cons(s(0), cons(y0, y1)))) -> c2(SIEVE(cons(s(0), cons(y0, y1)))) SIEVE(cons(0, cons(s(s(y0)), cons(y1, y2)))) -> c2(SIEVE(cons(s(s(y0)), cons(y1, y2)))) SIEVE(cons(s(0), cons(x0, cons(z0, z1)))) -> c3(SIEVE(cons(0, cons(0, filter(z1, 0, 0)))), FILTER(cons(x0, cons(z0, z1)), 0, 0)) SIEVE(cons(s(s(0)), cons(x1, cons(z0, z1)))) -> c3(SIEVE(cons(x1, cons(0, filter(z1, s(0), s(0))))), FILTER(cons(x1, cons(z0, z1)), s(0), s(0))) SIEVE(cons(s(s(s(z2))), cons(x1, cons(z0, z1)))) -> c3(SIEVE(cons(x1, cons(z0, filter(z1, z2, s(s(z2)))))), FILTER(cons(x1, cons(z0, z1)), s(s(z2)), s(s(z2)))) FILTER(cons(z0, cons(z1, cons(y1, y2))), 0, 0) -> c(FILTER(cons(z1, cons(y1, y2)), 0, 0)) FILTER(cons(z0, cons(z1, cons(y1, y2))), 0, s(s(y3))) -> c(FILTER(cons(z1, cons(y1, y2)), s(s(y3)), s(s(y3)))) FILTER(cons(z0, cons(z1, cons(y1, cons(y2, y3)))), 0, s(0)) -> c(FILTER(cons(z1, cons(y1, cons(y2, y3))), s(0), s(0))) FILTER(cons(z0, cons(z1, cons(y1, y2))), s(s(s(y3))), z4) -> c1(FILTER(cons(z1, cons(y1, y2)), s(s(y3)), z4)) FILTER(cons(z0, cons(z1, cons(y1, cons(y2, y3)))), s(s(0)), 0) -> c1(FILTER(cons(z1, cons(y1, cons(y2, y3))), s(0), 0)) FILTER(cons(z0, cons(z1, cons(y1, cons(y2, y3)))), s(s(0)), s(y4)) -> c1(FILTER(cons(z1, cons(y1, cons(y2, y3))), s(0), s(y4))) FILTER(cons(z0, cons(z1, cons(z2, cons(y2, y3)))), s(0), 0) -> c1(FILTER(cons(z1, cons(z2, cons(y2, y3))), 0, 0)) K tuples: ZPRIMES -> c6(SIEVE(nats(s(s(0))))) SIEVE(cons(s(0), cons(x0, x1))) -> c3(FILTER(cons(x0, x1), 0, 0)) SIEVE(cons(s(s(x0)), cons(x1, x2))) -> c3(FILTER(cons(x1, x2), s(x0), s(x0))) Defined Rule Symbols: filter_3, nats_1 Defined Pair Symbols: NATS_1, ZPRIMES, FILTER_3, SIEVE_1 Compound Symbols: c4_1, c6_1, c1_1, c2_1, c3_2, c3_1, c_1 ---------------------------------------- (81) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID)) Use forward instantiation to replace FILTER(cons(z0, cons(y0, cons(y1, y2))), s(0), s(y3)) -> c1(FILTER(cons(y0, cons(y1, y2)), 0, s(y3))) by FILTER(cons(z0, cons(z1, cons(z2, cons(y2, y3)))), s(0), s(s(y4))) -> c1(FILTER(cons(z1, cons(z2, cons(y2, y3))), 0, s(s(y4)))) FILTER(cons(z0, cons(z1, cons(z2, cons(y2, cons(y3, y4))))), s(0), s(0)) -> c1(FILTER(cons(z1, cons(z2, cons(y2, cons(y3, y4)))), 0, s(0))) ---------------------------------------- (82) Obligation: Complexity Dependency Tuples Problem Rules: filter(cons(z0, z1), 0, z2) -> cons(0, filter(z1, z2, z2)) filter(cons(z0, z1), s(z2), z3) -> cons(z0, filter(z1, z2, z3)) nats(z0) -> cons(z0, nats(s(z0))) Tuples: NATS(s(s(x0))) -> c4(NATS(s(s(s(x0))))) ZPRIMES -> c6(SIEVE(cons(s(s(0)), cons(s(s(s(0))), cons(s(s(s(s(0)))), cons(s(s(s(s(s(0))))), nats(s(s(s(s(s(s(0))))))))))))) SIEVE(cons(0, cons(0, y0))) -> c2(SIEVE(cons(0, y0))) SIEVE(cons(0, cons(s(0), cons(y0, y1)))) -> c2(SIEVE(cons(s(0), cons(y0, y1)))) SIEVE(cons(0, cons(s(s(y0)), cons(y1, y2)))) -> c2(SIEVE(cons(s(s(y0)), cons(y1, y2)))) SIEVE(cons(s(0), cons(x0, cons(z0, z1)))) -> c3(SIEVE(cons(0, cons(0, filter(z1, 0, 0)))), FILTER(cons(x0, cons(z0, z1)), 0, 0)) SIEVE(cons(s(0), cons(x0, x1))) -> c3(FILTER(cons(x0, x1), 0, 0)) SIEVE(cons(s(s(0)), cons(x1, cons(z0, z1)))) -> c3(SIEVE(cons(x1, cons(0, filter(z1, s(0), s(0))))), FILTER(cons(x1, cons(z0, z1)), s(0), s(0))) SIEVE(cons(s(s(s(z2))), cons(x1, cons(z0, z1)))) -> c3(SIEVE(cons(x1, cons(z0, filter(z1, z2, s(s(z2)))))), FILTER(cons(x1, cons(z0, z1)), s(s(z2)), s(s(z2)))) SIEVE(cons(s(s(x0)), cons(x1, x2))) -> c3(FILTER(cons(x1, x2), s(x0), s(x0))) FILTER(cons(z0, cons(z1, cons(y1, y2))), 0, 0) -> c(FILTER(cons(z1, cons(y1, y2)), 0, 0)) FILTER(cons(z0, cons(z1, cons(y1, y2))), 0, s(s(y3))) -> c(FILTER(cons(z1, cons(y1, y2)), s(s(y3)), s(s(y3)))) FILTER(cons(z0, cons(z1, cons(y1, cons(y2, y3)))), 0, s(0)) -> c(FILTER(cons(z1, cons(y1, cons(y2, y3))), s(0), s(0))) FILTER(cons(z0, cons(z1, cons(y1, y2))), s(s(s(y3))), z4) -> c1(FILTER(cons(z1, cons(y1, y2)), s(s(y3)), z4)) FILTER(cons(z0, cons(z1, cons(y1, cons(y2, y3)))), s(s(0)), 0) -> c1(FILTER(cons(z1, cons(y1, cons(y2, y3))), s(0), 0)) FILTER(cons(z0, cons(z1, cons(y1, cons(y2, y3)))), s(s(0)), s(y4)) -> c1(FILTER(cons(z1, cons(y1, cons(y2, y3))), s(0), s(y4))) FILTER(cons(z0, cons(z1, cons(z2, cons(y2, y3)))), s(0), 0) -> c1(FILTER(cons(z1, cons(z2, cons(y2, y3))), 0, 0)) FILTER(cons(z0, cons(z1, cons(z2, cons(y2, y3)))), s(0), s(s(y4))) -> c1(FILTER(cons(z1, cons(z2, cons(y2, y3))), 0, s(s(y4)))) FILTER(cons(z0, cons(z1, cons(z2, cons(y2, cons(y3, y4))))), s(0), s(0)) -> c1(FILTER(cons(z1, cons(z2, cons(y2, cons(y3, y4)))), 0, s(0))) S tuples: NATS(s(s(x0))) -> c4(NATS(s(s(s(x0))))) SIEVE(cons(0, cons(0, y0))) -> c2(SIEVE(cons(0, y0))) SIEVE(cons(0, cons(s(0), cons(y0, y1)))) -> c2(SIEVE(cons(s(0), cons(y0, y1)))) SIEVE(cons(0, cons(s(s(y0)), cons(y1, y2)))) -> c2(SIEVE(cons(s(s(y0)), cons(y1, y2)))) SIEVE(cons(s(0), cons(x0, cons(z0, z1)))) -> c3(SIEVE(cons(0, cons(0, filter(z1, 0, 0)))), FILTER(cons(x0, cons(z0, z1)), 0, 0)) SIEVE(cons(s(s(0)), cons(x1, cons(z0, z1)))) -> c3(SIEVE(cons(x1, cons(0, filter(z1, s(0), s(0))))), FILTER(cons(x1, cons(z0, z1)), s(0), s(0))) SIEVE(cons(s(s(s(z2))), cons(x1, cons(z0, z1)))) -> c3(SIEVE(cons(x1, cons(z0, filter(z1, z2, s(s(z2)))))), FILTER(cons(x1, cons(z0, z1)), s(s(z2)), s(s(z2)))) FILTER(cons(z0, cons(z1, cons(y1, y2))), 0, 0) -> c(FILTER(cons(z1, cons(y1, y2)), 0, 0)) FILTER(cons(z0, cons(z1, cons(y1, y2))), 0, s(s(y3))) -> c(FILTER(cons(z1, cons(y1, y2)), s(s(y3)), s(s(y3)))) FILTER(cons(z0, cons(z1, cons(y1, cons(y2, y3)))), 0, s(0)) -> c(FILTER(cons(z1, cons(y1, cons(y2, y3))), s(0), s(0))) FILTER(cons(z0, cons(z1, cons(y1, y2))), s(s(s(y3))), z4) -> c1(FILTER(cons(z1, cons(y1, y2)), s(s(y3)), z4)) FILTER(cons(z0, cons(z1, cons(y1, cons(y2, y3)))), s(s(0)), 0) -> c1(FILTER(cons(z1, cons(y1, cons(y2, y3))), s(0), 0)) FILTER(cons(z0, cons(z1, cons(y1, cons(y2, y3)))), s(s(0)), s(y4)) -> c1(FILTER(cons(z1, cons(y1, cons(y2, y3))), s(0), s(y4))) FILTER(cons(z0, cons(z1, cons(z2, cons(y2, y3)))), s(0), 0) -> c1(FILTER(cons(z1, cons(z2, cons(y2, y3))), 0, 0)) FILTER(cons(z0, cons(z1, cons(z2, cons(y2, y3)))), s(0), s(s(y4))) -> c1(FILTER(cons(z1, cons(z2, cons(y2, y3))), 0, s(s(y4)))) FILTER(cons(z0, cons(z1, cons(z2, cons(y2, cons(y3, y4))))), s(0), s(0)) -> c1(FILTER(cons(z1, cons(z2, cons(y2, cons(y3, y4)))), 0, s(0))) K tuples: ZPRIMES -> c6(SIEVE(nats(s(s(0))))) SIEVE(cons(s(0), cons(x0, x1))) -> c3(FILTER(cons(x0, x1), 0, 0)) SIEVE(cons(s(s(x0)), cons(x1, x2))) -> c3(FILTER(cons(x1, x2), s(x0), s(x0))) Defined Rule Symbols: filter_3, nats_1 Defined Pair Symbols: NATS_1, ZPRIMES, SIEVE_1, FILTER_3 Compound Symbols: c4_1, c6_1, c2_1, c3_2, c3_1, c_1, c1_1 ---------------------------------------- (83) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID)) Use forward instantiation to replace SIEVE(cons(0, cons(0, y0))) -> c2(SIEVE(cons(0, y0))) by SIEVE(cons(0, cons(0, cons(0, y0)))) -> c2(SIEVE(cons(0, cons(0, y0)))) SIEVE(cons(0, cons(0, cons(s(0), cons(y0, y1))))) -> c2(SIEVE(cons(0, cons(s(0), cons(y0, y1))))) SIEVE(cons(0, cons(0, cons(s(s(y0)), cons(y1, y2))))) -> c2(SIEVE(cons(0, cons(s(s(y0)), cons(y1, y2))))) ---------------------------------------- (84) Obligation: Complexity Dependency Tuples Problem Rules: filter(cons(z0, z1), 0, z2) -> cons(0, filter(z1, z2, z2)) filter(cons(z0, z1), s(z2), z3) -> cons(z0, filter(z1, z2, z3)) nats(z0) -> cons(z0, nats(s(z0))) Tuples: NATS(s(s(x0))) -> c4(NATS(s(s(s(x0))))) ZPRIMES -> c6(SIEVE(cons(s(s(0)), cons(s(s(s(0))), cons(s(s(s(s(0)))), cons(s(s(s(s(s(0))))), nats(s(s(s(s(s(s(0))))))))))))) SIEVE(cons(0, cons(s(0), cons(y0, y1)))) -> c2(SIEVE(cons(s(0), cons(y0, y1)))) SIEVE(cons(0, cons(s(s(y0)), cons(y1, y2)))) -> c2(SIEVE(cons(s(s(y0)), cons(y1, y2)))) SIEVE(cons(s(0), cons(x0, cons(z0, z1)))) -> c3(SIEVE(cons(0, cons(0, filter(z1, 0, 0)))), FILTER(cons(x0, cons(z0, z1)), 0, 0)) SIEVE(cons(s(0), cons(x0, x1))) -> c3(FILTER(cons(x0, x1), 0, 0)) SIEVE(cons(s(s(0)), cons(x1, cons(z0, z1)))) -> c3(SIEVE(cons(x1, cons(0, filter(z1, s(0), s(0))))), FILTER(cons(x1, cons(z0, z1)), s(0), s(0))) SIEVE(cons(s(s(s(z2))), cons(x1, cons(z0, z1)))) -> c3(SIEVE(cons(x1, cons(z0, filter(z1, z2, s(s(z2)))))), FILTER(cons(x1, cons(z0, z1)), s(s(z2)), s(s(z2)))) SIEVE(cons(s(s(x0)), cons(x1, x2))) -> c3(FILTER(cons(x1, x2), s(x0), s(x0))) FILTER(cons(z0, cons(z1, cons(y1, y2))), 0, 0) -> c(FILTER(cons(z1, cons(y1, y2)), 0, 0)) FILTER(cons(z0, cons(z1, cons(y1, y2))), 0, s(s(y3))) -> c(FILTER(cons(z1, cons(y1, y2)), s(s(y3)), s(s(y3)))) FILTER(cons(z0, cons(z1, cons(y1, cons(y2, y3)))), 0, s(0)) -> c(FILTER(cons(z1, cons(y1, cons(y2, y3))), s(0), s(0))) FILTER(cons(z0, cons(z1, cons(y1, y2))), s(s(s(y3))), z4) -> c1(FILTER(cons(z1, cons(y1, y2)), s(s(y3)), z4)) FILTER(cons(z0, cons(z1, cons(y1, cons(y2, y3)))), s(s(0)), 0) -> c1(FILTER(cons(z1, cons(y1, cons(y2, y3))), s(0), 0)) FILTER(cons(z0, cons(z1, cons(y1, cons(y2, y3)))), s(s(0)), s(y4)) -> c1(FILTER(cons(z1, cons(y1, cons(y2, y3))), s(0), s(y4))) FILTER(cons(z0, cons(z1, cons(z2, cons(y2, y3)))), s(0), 0) -> c1(FILTER(cons(z1, cons(z2, cons(y2, y3))), 0, 0)) FILTER(cons(z0, cons(z1, cons(z2, cons(y2, y3)))), s(0), s(s(y4))) -> c1(FILTER(cons(z1, cons(z2, cons(y2, y3))), 0, s(s(y4)))) FILTER(cons(z0, cons(z1, cons(z2, cons(y2, cons(y3, y4))))), s(0), s(0)) -> c1(FILTER(cons(z1, cons(z2, cons(y2, cons(y3, y4)))), 0, s(0))) SIEVE(cons(0, cons(0, cons(0, y0)))) -> c2(SIEVE(cons(0, cons(0, y0)))) SIEVE(cons(0, cons(0, cons(s(0), cons(y0, y1))))) -> c2(SIEVE(cons(0, cons(s(0), cons(y0, y1))))) SIEVE(cons(0, cons(0, cons(s(s(y0)), cons(y1, y2))))) -> c2(SIEVE(cons(0, cons(s(s(y0)), cons(y1, y2))))) S tuples: NATS(s(s(x0))) -> c4(NATS(s(s(s(x0))))) SIEVE(cons(0, cons(s(0), cons(y0, y1)))) -> c2(SIEVE(cons(s(0), cons(y0, y1)))) SIEVE(cons(0, cons(s(s(y0)), cons(y1, y2)))) -> c2(SIEVE(cons(s(s(y0)), cons(y1, y2)))) SIEVE(cons(s(0), cons(x0, cons(z0, z1)))) -> c3(SIEVE(cons(0, cons(0, filter(z1, 0, 0)))), FILTER(cons(x0, cons(z0, z1)), 0, 0)) SIEVE(cons(s(s(0)), cons(x1, cons(z0, z1)))) -> c3(SIEVE(cons(x1, cons(0, filter(z1, s(0), s(0))))), FILTER(cons(x1, cons(z0, z1)), s(0), s(0))) SIEVE(cons(s(s(s(z2))), cons(x1, cons(z0, z1)))) -> c3(SIEVE(cons(x1, cons(z0, filter(z1, z2, s(s(z2)))))), FILTER(cons(x1, cons(z0, z1)), s(s(z2)), s(s(z2)))) FILTER(cons(z0, cons(z1, cons(y1, y2))), 0, 0) -> c(FILTER(cons(z1, cons(y1, y2)), 0, 0)) FILTER(cons(z0, cons(z1, cons(y1, y2))), 0, s(s(y3))) -> c(FILTER(cons(z1, cons(y1, y2)), s(s(y3)), s(s(y3)))) FILTER(cons(z0, cons(z1, cons(y1, cons(y2, y3)))), 0, s(0)) -> c(FILTER(cons(z1, cons(y1, cons(y2, y3))), s(0), s(0))) FILTER(cons(z0, cons(z1, cons(y1, y2))), s(s(s(y3))), z4) -> c1(FILTER(cons(z1, cons(y1, y2)), s(s(y3)), z4)) FILTER(cons(z0, cons(z1, cons(y1, cons(y2, y3)))), s(s(0)), 0) -> c1(FILTER(cons(z1, cons(y1, cons(y2, y3))), s(0), 0)) FILTER(cons(z0, cons(z1, cons(y1, cons(y2, y3)))), s(s(0)), s(y4)) -> c1(FILTER(cons(z1, cons(y1, cons(y2, y3))), s(0), s(y4))) FILTER(cons(z0, cons(z1, cons(z2, cons(y2, y3)))), s(0), 0) -> c1(FILTER(cons(z1, cons(z2, cons(y2, y3))), 0, 0)) FILTER(cons(z0, cons(z1, cons(z2, cons(y2, y3)))), s(0), s(s(y4))) -> c1(FILTER(cons(z1, cons(z2, cons(y2, y3))), 0, s(s(y4)))) FILTER(cons(z0, cons(z1, cons(z2, cons(y2, cons(y3, y4))))), s(0), s(0)) -> c1(FILTER(cons(z1, cons(z2, cons(y2, cons(y3, y4)))), 0, s(0))) SIEVE(cons(0, cons(0, cons(0, y0)))) -> c2(SIEVE(cons(0, cons(0, y0)))) SIEVE(cons(0, cons(0, cons(s(0), cons(y0, y1))))) -> c2(SIEVE(cons(0, cons(s(0), cons(y0, y1))))) SIEVE(cons(0, cons(0, cons(s(s(y0)), cons(y1, y2))))) -> c2(SIEVE(cons(0, cons(s(s(y0)), cons(y1, y2))))) K tuples: ZPRIMES -> c6(SIEVE(nats(s(s(0))))) SIEVE(cons(s(0), cons(x0, x1))) -> c3(FILTER(cons(x0, x1), 0, 0)) SIEVE(cons(s(s(x0)), cons(x1, x2))) -> c3(FILTER(cons(x1, x2), s(x0), s(x0))) Defined Rule Symbols: filter_3, nats_1 Defined Pair Symbols: NATS_1, ZPRIMES, SIEVE_1, FILTER_3 Compound Symbols: c4_1, c6_1, c2_1, c3_2, c3_1, c_1, c1_1 ---------------------------------------- (85) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID)) Use forward instantiation to replace SIEVE(cons(s(0), cons(x0, x1))) -> c3(FILTER(cons(x0, x1), 0, 0)) by SIEVE(cons(s(0), cons(z0, cons(y1, cons(y2, y3))))) -> c3(FILTER(cons(z0, cons(y1, cons(y2, y3))), 0, 0)) ---------------------------------------- (86) Obligation: Complexity Dependency Tuples Problem Rules: filter(cons(z0, z1), 0, z2) -> cons(0, filter(z1, z2, z2)) filter(cons(z0, z1), s(z2), z3) -> cons(z0, filter(z1, z2, z3)) nats(z0) -> cons(z0, nats(s(z0))) Tuples: NATS(s(s(x0))) -> c4(NATS(s(s(s(x0))))) ZPRIMES -> c6(SIEVE(cons(s(s(0)), cons(s(s(s(0))), cons(s(s(s(s(0)))), cons(s(s(s(s(s(0))))), nats(s(s(s(s(s(s(0))))))))))))) SIEVE(cons(0, cons(s(0), cons(y0, y1)))) -> c2(SIEVE(cons(s(0), cons(y0, y1)))) SIEVE(cons(0, cons(s(s(y0)), cons(y1, y2)))) -> c2(SIEVE(cons(s(s(y0)), cons(y1, y2)))) SIEVE(cons(s(0), cons(x0, cons(z0, z1)))) -> c3(SIEVE(cons(0, cons(0, filter(z1, 0, 0)))), FILTER(cons(x0, cons(z0, z1)), 0, 0)) SIEVE(cons(s(s(0)), cons(x1, cons(z0, z1)))) -> c3(SIEVE(cons(x1, cons(0, filter(z1, s(0), s(0))))), FILTER(cons(x1, cons(z0, z1)), s(0), s(0))) SIEVE(cons(s(s(s(z2))), cons(x1, cons(z0, z1)))) -> c3(SIEVE(cons(x1, cons(z0, filter(z1, z2, s(s(z2)))))), FILTER(cons(x1, cons(z0, z1)), s(s(z2)), s(s(z2)))) SIEVE(cons(s(s(x0)), cons(x1, x2))) -> c3(FILTER(cons(x1, x2), s(x0), s(x0))) FILTER(cons(z0, cons(z1, cons(y1, y2))), 0, 0) -> c(FILTER(cons(z1, cons(y1, y2)), 0, 0)) FILTER(cons(z0, cons(z1, cons(y1, y2))), 0, s(s(y3))) -> c(FILTER(cons(z1, cons(y1, y2)), s(s(y3)), s(s(y3)))) FILTER(cons(z0, cons(z1, cons(y1, cons(y2, y3)))), 0, s(0)) -> c(FILTER(cons(z1, cons(y1, cons(y2, y3))), s(0), s(0))) FILTER(cons(z0, cons(z1, cons(y1, y2))), s(s(s(y3))), z4) -> c1(FILTER(cons(z1, cons(y1, y2)), s(s(y3)), z4)) FILTER(cons(z0, cons(z1, cons(y1, cons(y2, y3)))), s(s(0)), 0) -> c1(FILTER(cons(z1, cons(y1, cons(y2, y3))), s(0), 0)) FILTER(cons(z0, cons(z1, cons(y1, cons(y2, y3)))), s(s(0)), s(y4)) -> c1(FILTER(cons(z1, cons(y1, cons(y2, y3))), s(0), s(y4))) FILTER(cons(z0, cons(z1, cons(z2, cons(y2, y3)))), s(0), 0) -> c1(FILTER(cons(z1, cons(z2, cons(y2, y3))), 0, 0)) FILTER(cons(z0, cons(z1, cons(z2, cons(y2, y3)))), s(0), s(s(y4))) -> c1(FILTER(cons(z1, cons(z2, cons(y2, y3))), 0, s(s(y4)))) FILTER(cons(z0, cons(z1, cons(z2, cons(y2, cons(y3, y4))))), s(0), s(0)) -> c1(FILTER(cons(z1, cons(z2, cons(y2, cons(y3, y4)))), 0, s(0))) SIEVE(cons(0, cons(0, cons(0, y0)))) -> c2(SIEVE(cons(0, cons(0, y0)))) SIEVE(cons(0, cons(0, cons(s(0), cons(y0, y1))))) -> c2(SIEVE(cons(0, cons(s(0), cons(y0, y1))))) SIEVE(cons(0, cons(0, cons(s(s(y0)), cons(y1, y2))))) -> c2(SIEVE(cons(0, cons(s(s(y0)), cons(y1, y2))))) SIEVE(cons(s(0), cons(z0, cons(y1, cons(y2, y3))))) -> c3(FILTER(cons(z0, cons(y1, cons(y2, y3))), 0, 0)) S tuples: NATS(s(s(x0))) -> c4(NATS(s(s(s(x0))))) SIEVE(cons(0, cons(s(0), cons(y0, y1)))) -> c2(SIEVE(cons(s(0), cons(y0, y1)))) SIEVE(cons(0, cons(s(s(y0)), cons(y1, y2)))) -> c2(SIEVE(cons(s(s(y0)), cons(y1, y2)))) SIEVE(cons(s(0), cons(x0, cons(z0, z1)))) -> c3(SIEVE(cons(0, cons(0, filter(z1, 0, 0)))), FILTER(cons(x0, cons(z0, z1)), 0, 0)) SIEVE(cons(s(s(0)), cons(x1, cons(z0, z1)))) -> c3(SIEVE(cons(x1, cons(0, filter(z1, s(0), s(0))))), FILTER(cons(x1, cons(z0, z1)), s(0), s(0))) SIEVE(cons(s(s(s(z2))), cons(x1, cons(z0, z1)))) -> c3(SIEVE(cons(x1, cons(z0, filter(z1, z2, s(s(z2)))))), FILTER(cons(x1, cons(z0, z1)), s(s(z2)), s(s(z2)))) FILTER(cons(z0, cons(z1, cons(y1, y2))), 0, 0) -> c(FILTER(cons(z1, cons(y1, y2)), 0, 0)) FILTER(cons(z0, cons(z1, cons(y1, y2))), 0, s(s(y3))) -> c(FILTER(cons(z1, cons(y1, y2)), s(s(y3)), s(s(y3)))) FILTER(cons(z0, cons(z1, cons(y1, cons(y2, y3)))), 0, s(0)) -> c(FILTER(cons(z1, cons(y1, cons(y2, y3))), s(0), s(0))) FILTER(cons(z0, cons(z1, cons(y1, y2))), s(s(s(y3))), z4) -> c1(FILTER(cons(z1, cons(y1, y2)), s(s(y3)), z4)) FILTER(cons(z0, cons(z1, cons(y1, cons(y2, y3)))), s(s(0)), 0) -> c1(FILTER(cons(z1, cons(y1, cons(y2, y3))), s(0), 0)) FILTER(cons(z0, cons(z1, cons(y1, cons(y2, y3)))), s(s(0)), s(y4)) -> c1(FILTER(cons(z1, cons(y1, cons(y2, y3))), s(0), s(y4))) FILTER(cons(z0, cons(z1, cons(z2, cons(y2, y3)))), s(0), 0) -> c1(FILTER(cons(z1, cons(z2, cons(y2, y3))), 0, 0)) FILTER(cons(z0, cons(z1, cons(z2, cons(y2, y3)))), s(0), s(s(y4))) -> c1(FILTER(cons(z1, cons(z2, cons(y2, y3))), 0, s(s(y4)))) FILTER(cons(z0, cons(z1, cons(z2, cons(y2, cons(y3, y4))))), s(0), s(0)) -> c1(FILTER(cons(z1, cons(z2, cons(y2, cons(y3, y4)))), 0, s(0))) SIEVE(cons(0, cons(0, cons(0, y0)))) -> c2(SIEVE(cons(0, cons(0, y0)))) SIEVE(cons(0, cons(0, cons(s(0), cons(y0, y1))))) -> c2(SIEVE(cons(0, cons(s(0), cons(y0, y1))))) SIEVE(cons(0, cons(0, cons(s(s(y0)), cons(y1, y2))))) -> c2(SIEVE(cons(0, cons(s(s(y0)), cons(y1, y2))))) K tuples: ZPRIMES -> c6(SIEVE(nats(s(s(0))))) SIEVE(cons(s(s(x0)), cons(x1, x2))) -> c3(FILTER(cons(x1, x2), s(x0), s(x0))) SIEVE(cons(s(0), cons(z0, cons(y1, cons(y2, y3))))) -> c3(FILTER(cons(z0, cons(y1, cons(y2, y3))), 0, 0)) Defined Rule Symbols: filter_3, nats_1 Defined Pair Symbols: NATS_1, ZPRIMES, SIEVE_1, FILTER_3 Compound Symbols: c4_1, c6_1, c2_1, c3_2, c3_1, c_1, c1_1 ---------------------------------------- (87) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID)) Use forward instantiation to replace SIEVE(cons(0, cons(s(0), cons(y0, y1)))) -> c2(SIEVE(cons(s(0), cons(y0, y1)))) by SIEVE(cons(0, cons(s(0), cons(z0, cons(y1, y2))))) -> c2(SIEVE(cons(s(0), cons(z0, cons(y1, y2))))) SIEVE(cons(0, cons(s(0), cons(z0, cons(y1, cons(y2, y3)))))) -> c2(SIEVE(cons(s(0), cons(z0, cons(y1, cons(y2, y3)))))) ---------------------------------------- (88) Obligation: Complexity Dependency Tuples Problem Rules: filter(cons(z0, z1), 0, z2) -> cons(0, filter(z1, z2, z2)) filter(cons(z0, z1), s(z2), z3) -> cons(z0, filter(z1, z2, z3)) nats(z0) -> cons(z0, nats(s(z0))) Tuples: NATS(s(s(x0))) -> c4(NATS(s(s(s(x0))))) ZPRIMES -> c6(SIEVE(cons(s(s(0)), cons(s(s(s(0))), cons(s(s(s(s(0)))), cons(s(s(s(s(s(0))))), nats(s(s(s(s(s(s(0))))))))))))) SIEVE(cons(0, cons(s(s(y0)), cons(y1, y2)))) -> c2(SIEVE(cons(s(s(y0)), cons(y1, y2)))) SIEVE(cons(s(0), cons(x0, cons(z0, z1)))) -> c3(SIEVE(cons(0, cons(0, filter(z1, 0, 0)))), FILTER(cons(x0, cons(z0, z1)), 0, 0)) SIEVE(cons(s(s(0)), cons(x1, cons(z0, z1)))) -> c3(SIEVE(cons(x1, cons(0, filter(z1, s(0), s(0))))), FILTER(cons(x1, cons(z0, z1)), s(0), s(0))) SIEVE(cons(s(s(s(z2))), cons(x1, cons(z0, z1)))) -> c3(SIEVE(cons(x1, cons(z0, filter(z1, z2, s(s(z2)))))), FILTER(cons(x1, cons(z0, z1)), s(s(z2)), s(s(z2)))) SIEVE(cons(s(s(x0)), cons(x1, x2))) -> c3(FILTER(cons(x1, x2), s(x0), s(x0))) FILTER(cons(z0, cons(z1, cons(y1, y2))), 0, 0) -> c(FILTER(cons(z1, cons(y1, y2)), 0, 0)) FILTER(cons(z0, cons(z1, cons(y1, y2))), 0, s(s(y3))) -> c(FILTER(cons(z1, cons(y1, y2)), s(s(y3)), s(s(y3)))) FILTER(cons(z0, cons(z1, cons(y1, cons(y2, y3)))), 0, s(0)) -> c(FILTER(cons(z1, cons(y1, cons(y2, y3))), s(0), s(0))) FILTER(cons(z0, cons(z1, cons(y1, y2))), s(s(s(y3))), z4) -> c1(FILTER(cons(z1, cons(y1, y2)), s(s(y3)), z4)) FILTER(cons(z0, cons(z1, cons(y1, cons(y2, y3)))), s(s(0)), 0) -> c1(FILTER(cons(z1, cons(y1, cons(y2, y3))), s(0), 0)) FILTER(cons(z0, cons(z1, cons(y1, cons(y2, y3)))), s(s(0)), s(y4)) -> c1(FILTER(cons(z1, cons(y1, cons(y2, y3))), s(0), s(y4))) FILTER(cons(z0, cons(z1, cons(z2, cons(y2, y3)))), s(0), 0) -> c1(FILTER(cons(z1, cons(z2, cons(y2, y3))), 0, 0)) FILTER(cons(z0, cons(z1, cons(z2, cons(y2, y3)))), s(0), s(s(y4))) -> c1(FILTER(cons(z1, cons(z2, cons(y2, y3))), 0, s(s(y4)))) FILTER(cons(z0, cons(z1, cons(z2, cons(y2, cons(y3, y4))))), s(0), s(0)) -> c1(FILTER(cons(z1, cons(z2, cons(y2, cons(y3, y4)))), 0, s(0))) SIEVE(cons(0, cons(0, cons(0, y0)))) -> c2(SIEVE(cons(0, cons(0, y0)))) SIEVE(cons(0, cons(0, cons(s(0), cons(y0, y1))))) -> c2(SIEVE(cons(0, cons(s(0), cons(y0, y1))))) SIEVE(cons(0, cons(0, cons(s(s(y0)), cons(y1, y2))))) -> c2(SIEVE(cons(0, cons(s(s(y0)), cons(y1, y2))))) SIEVE(cons(s(0), cons(z0, cons(y1, cons(y2, y3))))) -> c3(FILTER(cons(z0, cons(y1, cons(y2, y3))), 0, 0)) SIEVE(cons(0, cons(s(0), cons(z0, cons(y1, y2))))) -> c2(SIEVE(cons(s(0), cons(z0, cons(y1, y2))))) SIEVE(cons(0, cons(s(0), cons(z0, cons(y1, cons(y2, y3)))))) -> c2(SIEVE(cons(s(0), cons(z0, cons(y1, cons(y2, y3)))))) S tuples: NATS(s(s(x0))) -> c4(NATS(s(s(s(x0))))) SIEVE(cons(0, cons(s(s(y0)), cons(y1, y2)))) -> c2(SIEVE(cons(s(s(y0)), cons(y1, y2)))) SIEVE(cons(s(0), cons(x0, cons(z0, z1)))) -> c3(SIEVE(cons(0, cons(0, filter(z1, 0, 0)))), FILTER(cons(x0, cons(z0, z1)), 0, 0)) SIEVE(cons(s(s(0)), cons(x1, cons(z0, z1)))) -> c3(SIEVE(cons(x1, cons(0, filter(z1, s(0), s(0))))), FILTER(cons(x1, cons(z0, z1)), s(0), s(0))) SIEVE(cons(s(s(s(z2))), cons(x1, cons(z0, z1)))) -> c3(SIEVE(cons(x1, cons(z0, filter(z1, z2, s(s(z2)))))), FILTER(cons(x1, cons(z0, z1)), s(s(z2)), s(s(z2)))) FILTER(cons(z0, cons(z1, cons(y1, y2))), 0, 0) -> c(FILTER(cons(z1, cons(y1, y2)), 0, 0)) FILTER(cons(z0, cons(z1, cons(y1, y2))), 0, s(s(y3))) -> c(FILTER(cons(z1, cons(y1, y2)), s(s(y3)), s(s(y3)))) FILTER(cons(z0, cons(z1, cons(y1, cons(y2, y3)))), 0, s(0)) -> c(FILTER(cons(z1, cons(y1, cons(y2, y3))), s(0), s(0))) FILTER(cons(z0, cons(z1, cons(y1, y2))), s(s(s(y3))), z4) -> c1(FILTER(cons(z1, cons(y1, y2)), s(s(y3)), z4)) FILTER(cons(z0, cons(z1, cons(y1, cons(y2, y3)))), s(s(0)), 0) -> c1(FILTER(cons(z1, cons(y1, cons(y2, y3))), s(0), 0)) FILTER(cons(z0, cons(z1, cons(y1, cons(y2, y3)))), s(s(0)), s(y4)) -> c1(FILTER(cons(z1, cons(y1, cons(y2, y3))), s(0), s(y4))) FILTER(cons(z0, cons(z1, cons(z2, cons(y2, y3)))), s(0), 0) -> c1(FILTER(cons(z1, cons(z2, cons(y2, y3))), 0, 0)) FILTER(cons(z0, cons(z1, cons(z2, cons(y2, y3)))), s(0), s(s(y4))) -> c1(FILTER(cons(z1, cons(z2, cons(y2, y3))), 0, s(s(y4)))) FILTER(cons(z0, cons(z1, cons(z2, cons(y2, cons(y3, y4))))), s(0), s(0)) -> c1(FILTER(cons(z1, cons(z2, cons(y2, cons(y3, y4)))), 0, s(0))) SIEVE(cons(0, cons(0, cons(0, y0)))) -> c2(SIEVE(cons(0, cons(0, y0)))) SIEVE(cons(0, cons(0, cons(s(0), cons(y0, y1))))) -> c2(SIEVE(cons(0, cons(s(0), cons(y0, y1))))) SIEVE(cons(0, cons(0, cons(s(s(y0)), cons(y1, y2))))) -> c2(SIEVE(cons(0, cons(s(s(y0)), cons(y1, y2))))) SIEVE(cons(0, cons(s(0), cons(z0, cons(y1, y2))))) -> c2(SIEVE(cons(s(0), cons(z0, cons(y1, y2))))) SIEVE(cons(0, cons(s(0), cons(z0, cons(y1, cons(y2, y3)))))) -> c2(SIEVE(cons(s(0), cons(z0, cons(y1, cons(y2, y3)))))) K tuples: ZPRIMES -> c6(SIEVE(nats(s(s(0))))) SIEVE(cons(s(s(x0)), cons(x1, x2))) -> c3(FILTER(cons(x1, x2), s(x0), s(x0))) SIEVE(cons(s(0), cons(z0, cons(y1, cons(y2, y3))))) -> c3(FILTER(cons(z0, cons(y1, cons(y2, y3))), 0, 0)) Defined Rule Symbols: filter_3, nats_1 Defined Pair Symbols: NATS_1, ZPRIMES, SIEVE_1, FILTER_3 Compound Symbols: c4_1, c6_1, c2_1, c3_2, c3_1, c_1, c1_1 ---------------------------------------- (89) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID)) Use forward instantiation to replace SIEVE(cons(s(s(x0)), cons(x1, x2))) -> c3(FILTER(cons(x1, x2), s(x0), s(x0))) by SIEVE(cons(s(s(s(s(y4)))), cons(z1, cons(y1, cons(y2, y3))))) -> c3(FILTER(cons(z1, cons(y1, cons(y2, y3))), s(s(s(y4))), s(s(s(y4))))) SIEVE(cons(s(s(s(0))), cons(z1, cons(y1, cons(y2, cons(y3, y4)))))) -> c3(FILTER(cons(z1, cons(y1, cons(y2, cons(y3, y4)))), s(s(0)), s(s(0)))) SIEVE(cons(s(s(0)), cons(z1, cons(y1, cons(y2, cons(y3, cons(y4, y5))))))) -> c3(FILTER(cons(z1, cons(y1, cons(y2, cons(y3, cons(y4, y5))))), s(0), s(0))) ---------------------------------------- (90) Obligation: Complexity Dependency Tuples Problem Rules: filter(cons(z0, z1), 0, z2) -> cons(0, filter(z1, z2, z2)) filter(cons(z0, z1), s(z2), z3) -> cons(z0, filter(z1, z2, z3)) nats(z0) -> cons(z0, nats(s(z0))) Tuples: NATS(s(s(x0))) -> c4(NATS(s(s(s(x0))))) ZPRIMES -> c6(SIEVE(cons(s(s(0)), cons(s(s(s(0))), cons(s(s(s(s(0)))), cons(s(s(s(s(s(0))))), nats(s(s(s(s(s(s(0))))))))))))) SIEVE(cons(0, cons(s(s(y0)), cons(y1, y2)))) -> c2(SIEVE(cons(s(s(y0)), cons(y1, y2)))) SIEVE(cons(s(0), cons(x0, cons(z0, z1)))) -> c3(SIEVE(cons(0, cons(0, filter(z1, 0, 0)))), FILTER(cons(x0, cons(z0, z1)), 0, 0)) SIEVE(cons(s(s(0)), cons(x1, cons(z0, z1)))) -> c3(SIEVE(cons(x1, cons(0, filter(z1, s(0), s(0))))), FILTER(cons(x1, cons(z0, z1)), s(0), s(0))) SIEVE(cons(s(s(s(z2))), cons(x1, cons(z0, z1)))) -> c3(SIEVE(cons(x1, cons(z0, filter(z1, z2, s(s(z2)))))), FILTER(cons(x1, cons(z0, z1)), s(s(z2)), s(s(z2)))) FILTER(cons(z0, cons(z1, cons(y1, y2))), 0, 0) -> c(FILTER(cons(z1, cons(y1, y2)), 0, 0)) FILTER(cons(z0, cons(z1, cons(y1, y2))), 0, s(s(y3))) -> c(FILTER(cons(z1, cons(y1, y2)), s(s(y3)), s(s(y3)))) FILTER(cons(z0, cons(z1, cons(y1, cons(y2, y3)))), 0, s(0)) -> c(FILTER(cons(z1, cons(y1, cons(y2, y3))), s(0), s(0))) FILTER(cons(z0, cons(z1, cons(y1, y2))), s(s(s(y3))), z4) -> c1(FILTER(cons(z1, cons(y1, y2)), s(s(y3)), z4)) FILTER(cons(z0, cons(z1, cons(y1, cons(y2, y3)))), s(s(0)), 0) -> c1(FILTER(cons(z1, cons(y1, cons(y2, y3))), s(0), 0)) FILTER(cons(z0, cons(z1, cons(y1, cons(y2, y3)))), s(s(0)), s(y4)) -> c1(FILTER(cons(z1, cons(y1, cons(y2, y3))), s(0), s(y4))) FILTER(cons(z0, cons(z1, cons(z2, cons(y2, y3)))), s(0), 0) -> c1(FILTER(cons(z1, cons(z2, cons(y2, y3))), 0, 0)) FILTER(cons(z0, cons(z1, cons(z2, cons(y2, y3)))), s(0), s(s(y4))) -> c1(FILTER(cons(z1, cons(z2, cons(y2, y3))), 0, s(s(y4)))) FILTER(cons(z0, cons(z1, cons(z2, cons(y2, cons(y3, y4))))), s(0), s(0)) -> c1(FILTER(cons(z1, cons(z2, cons(y2, cons(y3, y4)))), 0, s(0))) SIEVE(cons(0, cons(0, cons(0, y0)))) -> c2(SIEVE(cons(0, cons(0, y0)))) SIEVE(cons(0, cons(0, cons(s(0), cons(y0, y1))))) -> c2(SIEVE(cons(0, cons(s(0), cons(y0, y1))))) SIEVE(cons(0, cons(0, cons(s(s(y0)), cons(y1, y2))))) -> c2(SIEVE(cons(0, cons(s(s(y0)), cons(y1, y2))))) SIEVE(cons(s(0), cons(z0, cons(y1, cons(y2, y3))))) -> c3(FILTER(cons(z0, cons(y1, cons(y2, y3))), 0, 0)) SIEVE(cons(0, cons(s(0), cons(z0, cons(y1, y2))))) -> c2(SIEVE(cons(s(0), cons(z0, cons(y1, y2))))) SIEVE(cons(0, cons(s(0), cons(z0, cons(y1, cons(y2, y3)))))) -> c2(SIEVE(cons(s(0), cons(z0, cons(y1, cons(y2, y3)))))) SIEVE(cons(s(s(s(s(y4)))), cons(z1, cons(y1, cons(y2, y3))))) -> c3(FILTER(cons(z1, cons(y1, cons(y2, y3))), s(s(s(y4))), s(s(s(y4))))) SIEVE(cons(s(s(s(0))), cons(z1, cons(y1, cons(y2, cons(y3, y4)))))) -> c3(FILTER(cons(z1, cons(y1, cons(y2, cons(y3, y4)))), s(s(0)), s(s(0)))) SIEVE(cons(s(s(0)), cons(z1, cons(y1, cons(y2, cons(y3, cons(y4, y5))))))) -> c3(FILTER(cons(z1, cons(y1, cons(y2, cons(y3, cons(y4, y5))))), s(0), s(0))) S tuples: NATS(s(s(x0))) -> c4(NATS(s(s(s(x0))))) SIEVE(cons(0, cons(s(s(y0)), cons(y1, y2)))) -> c2(SIEVE(cons(s(s(y0)), cons(y1, y2)))) SIEVE(cons(s(0), cons(x0, cons(z0, z1)))) -> c3(SIEVE(cons(0, cons(0, filter(z1, 0, 0)))), FILTER(cons(x0, cons(z0, z1)), 0, 0)) SIEVE(cons(s(s(0)), cons(x1, cons(z0, z1)))) -> c3(SIEVE(cons(x1, cons(0, filter(z1, s(0), s(0))))), FILTER(cons(x1, cons(z0, z1)), s(0), s(0))) SIEVE(cons(s(s(s(z2))), cons(x1, cons(z0, z1)))) -> c3(SIEVE(cons(x1, cons(z0, filter(z1, z2, s(s(z2)))))), FILTER(cons(x1, cons(z0, z1)), s(s(z2)), s(s(z2)))) FILTER(cons(z0, cons(z1, cons(y1, y2))), 0, 0) -> c(FILTER(cons(z1, cons(y1, y2)), 0, 0)) FILTER(cons(z0, cons(z1, cons(y1, y2))), 0, s(s(y3))) -> c(FILTER(cons(z1, cons(y1, y2)), s(s(y3)), s(s(y3)))) FILTER(cons(z0, cons(z1, cons(y1, cons(y2, y3)))), 0, s(0)) -> c(FILTER(cons(z1, cons(y1, cons(y2, y3))), s(0), s(0))) FILTER(cons(z0, cons(z1, cons(y1, y2))), s(s(s(y3))), z4) -> c1(FILTER(cons(z1, cons(y1, y2)), s(s(y3)), z4)) FILTER(cons(z0, cons(z1, cons(y1, cons(y2, y3)))), s(s(0)), 0) -> c1(FILTER(cons(z1, cons(y1, cons(y2, y3))), s(0), 0)) FILTER(cons(z0, cons(z1, cons(y1, cons(y2, y3)))), s(s(0)), s(y4)) -> c1(FILTER(cons(z1, cons(y1, cons(y2, y3))), s(0), s(y4))) FILTER(cons(z0, cons(z1, cons(z2, cons(y2, y3)))), s(0), 0) -> c1(FILTER(cons(z1, cons(z2, cons(y2, y3))), 0, 0)) FILTER(cons(z0, cons(z1, cons(z2, cons(y2, y3)))), s(0), s(s(y4))) -> c1(FILTER(cons(z1, cons(z2, cons(y2, y3))), 0, s(s(y4)))) FILTER(cons(z0, cons(z1, cons(z2, cons(y2, cons(y3, y4))))), s(0), s(0)) -> c1(FILTER(cons(z1, cons(z2, cons(y2, cons(y3, y4)))), 0, s(0))) SIEVE(cons(0, cons(0, cons(0, y0)))) -> c2(SIEVE(cons(0, cons(0, y0)))) SIEVE(cons(0, cons(0, cons(s(0), cons(y0, y1))))) -> c2(SIEVE(cons(0, cons(s(0), cons(y0, y1))))) SIEVE(cons(0, cons(0, cons(s(s(y0)), cons(y1, y2))))) -> c2(SIEVE(cons(0, cons(s(s(y0)), cons(y1, y2))))) SIEVE(cons(0, cons(s(0), cons(z0, cons(y1, y2))))) -> c2(SIEVE(cons(s(0), cons(z0, cons(y1, y2))))) SIEVE(cons(0, cons(s(0), cons(z0, cons(y1, cons(y2, y3)))))) -> c2(SIEVE(cons(s(0), cons(z0, cons(y1, cons(y2, y3)))))) K tuples: ZPRIMES -> c6(SIEVE(nats(s(s(0))))) SIEVE(cons(s(0), cons(z0, cons(y1, cons(y2, y3))))) -> c3(FILTER(cons(z0, cons(y1, cons(y2, y3))), 0, 0)) SIEVE(cons(s(s(s(s(y4)))), cons(z1, cons(y1, cons(y2, y3))))) -> c3(FILTER(cons(z1, cons(y1, cons(y2, y3))), s(s(s(y4))), s(s(s(y4))))) SIEVE(cons(s(s(s(0))), cons(z1, cons(y1, cons(y2, cons(y3, y4)))))) -> c3(FILTER(cons(z1, cons(y1, cons(y2, cons(y3, y4)))), s(s(0)), s(s(0)))) SIEVE(cons(s(s(0)), cons(z1, cons(y1, cons(y2, cons(y3, cons(y4, y5))))))) -> c3(FILTER(cons(z1, cons(y1, cons(y2, cons(y3, cons(y4, y5))))), s(0), s(0))) Defined Rule Symbols: filter_3, nats_1 Defined Pair Symbols: NATS_1, ZPRIMES, SIEVE_1, FILTER_3 Compound Symbols: c4_1, c6_1, c2_1, c3_2, c_1, c1_1, c3_1 ---------------------------------------- (91) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID)) Use forward instantiation to replace SIEVE(cons(0, cons(s(s(y0)), cons(y1, y2)))) -> c2(SIEVE(cons(s(s(y0)), cons(y1, y2)))) by SIEVE(cons(0, cons(s(s(0)), cons(z1, cons(y1, y2))))) -> c2(SIEVE(cons(s(s(0)), cons(z1, cons(y1, y2))))) SIEVE(cons(0, cons(s(s(s(y0))), cons(z1, cons(y2, y3))))) -> c2(SIEVE(cons(s(s(s(y0))), cons(z1, cons(y2, y3))))) SIEVE(cons(0, cons(s(s(s(s(y0)))), cons(z1, cons(y2, cons(y3, y4)))))) -> c2(SIEVE(cons(s(s(s(s(y0)))), cons(z1, cons(y2, cons(y3, y4)))))) SIEVE(cons(0, cons(s(s(s(0))), cons(z1, cons(y1, cons(y2, cons(y3, y4))))))) -> c2(SIEVE(cons(s(s(s(0))), cons(z1, cons(y1, cons(y2, cons(y3, y4))))))) SIEVE(cons(0, cons(s(s(0)), cons(z1, cons(y1, cons(y2, cons(y3, cons(y4, y5)))))))) -> c2(SIEVE(cons(s(s(0)), cons(z1, cons(y1, cons(y2, cons(y3, cons(y4, y5)))))))) ---------------------------------------- (92) Obligation: Complexity Dependency Tuples Problem Rules: filter(cons(z0, z1), 0, z2) -> cons(0, filter(z1, z2, z2)) filter(cons(z0, z1), s(z2), z3) -> cons(z0, filter(z1, z2, z3)) nats(z0) -> cons(z0, nats(s(z0))) Tuples: NATS(s(s(x0))) -> c4(NATS(s(s(s(x0))))) ZPRIMES -> c6(SIEVE(cons(s(s(0)), cons(s(s(s(0))), cons(s(s(s(s(0)))), cons(s(s(s(s(s(0))))), nats(s(s(s(s(s(s(0))))))))))))) SIEVE(cons(s(0), cons(x0, cons(z0, z1)))) -> c3(SIEVE(cons(0, cons(0, filter(z1, 0, 0)))), FILTER(cons(x0, cons(z0, z1)), 0, 0)) SIEVE(cons(s(s(0)), cons(x1, cons(z0, z1)))) -> c3(SIEVE(cons(x1, cons(0, filter(z1, s(0), s(0))))), FILTER(cons(x1, cons(z0, z1)), s(0), s(0))) SIEVE(cons(s(s(s(z2))), cons(x1, cons(z0, z1)))) -> c3(SIEVE(cons(x1, cons(z0, filter(z1, z2, s(s(z2)))))), FILTER(cons(x1, cons(z0, z1)), s(s(z2)), s(s(z2)))) FILTER(cons(z0, cons(z1, cons(y1, y2))), 0, 0) -> c(FILTER(cons(z1, cons(y1, y2)), 0, 0)) FILTER(cons(z0, cons(z1, cons(y1, y2))), 0, s(s(y3))) -> c(FILTER(cons(z1, cons(y1, y2)), s(s(y3)), s(s(y3)))) FILTER(cons(z0, cons(z1, cons(y1, cons(y2, y3)))), 0, s(0)) -> c(FILTER(cons(z1, cons(y1, cons(y2, y3))), s(0), s(0))) FILTER(cons(z0, cons(z1, cons(y1, y2))), s(s(s(y3))), z4) -> c1(FILTER(cons(z1, cons(y1, y2)), s(s(y3)), z4)) FILTER(cons(z0, cons(z1, cons(y1, cons(y2, y3)))), s(s(0)), 0) -> c1(FILTER(cons(z1, cons(y1, cons(y2, y3))), s(0), 0)) FILTER(cons(z0, cons(z1, cons(y1, cons(y2, y3)))), s(s(0)), s(y4)) -> c1(FILTER(cons(z1, cons(y1, cons(y2, y3))), s(0), s(y4))) FILTER(cons(z0, cons(z1, cons(z2, cons(y2, y3)))), s(0), 0) -> c1(FILTER(cons(z1, cons(z2, cons(y2, y3))), 0, 0)) FILTER(cons(z0, cons(z1, cons(z2, cons(y2, y3)))), s(0), s(s(y4))) -> c1(FILTER(cons(z1, cons(z2, cons(y2, y3))), 0, s(s(y4)))) FILTER(cons(z0, cons(z1, cons(z2, cons(y2, cons(y3, y4))))), s(0), s(0)) -> c1(FILTER(cons(z1, cons(z2, cons(y2, cons(y3, y4)))), 0, s(0))) SIEVE(cons(0, cons(0, cons(0, y0)))) -> c2(SIEVE(cons(0, cons(0, y0)))) SIEVE(cons(0, cons(0, cons(s(0), cons(y0, y1))))) -> c2(SIEVE(cons(0, cons(s(0), cons(y0, y1))))) SIEVE(cons(0, cons(0, cons(s(s(y0)), cons(y1, y2))))) -> c2(SIEVE(cons(0, cons(s(s(y0)), cons(y1, y2))))) SIEVE(cons(s(0), cons(z0, cons(y1, cons(y2, y3))))) -> c3(FILTER(cons(z0, cons(y1, cons(y2, y3))), 0, 0)) SIEVE(cons(0, cons(s(0), cons(z0, cons(y1, y2))))) -> c2(SIEVE(cons(s(0), cons(z0, cons(y1, y2))))) SIEVE(cons(0, cons(s(0), cons(z0, cons(y1, cons(y2, y3)))))) -> c2(SIEVE(cons(s(0), cons(z0, cons(y1, cons(y2, y3)))))) SIEVE(cons(s(s(s(s(y4)))), cons(z1, cons(y1, cons(y2, y3))))) -> c3(FILTER(cons(z1, cons(y1, cons(y2, y3))), s(s(s(y4))), s(s(s(y4))))) SIEVE(cons(s(s(s(0))), cons(z1, cons(y1, cons(y2, cons(y3, y4)))))) -> c3(FILTER(cons(z1, cons(y1, cons(y2, cons(y3, y4)))), s(s(0)), s(s(0)))) SIEVE(cons(s(s(0)), cons(z1, cons(y1, cons(y2, cons(y3, cons(y4, y5))))))) -> c3(FILTER(cons(z1, cons(y1, cons(y2, cons(y3, cons(y4, y5))))), s(0), s(0))) SIEVE(cons(0, cons(s(s(0)), cons(z1, cons(y1, y2))))) -> c2(SIEVE(cons(s(s(0)), cons(z1, cons(y1, y2))))) SIEVE(cons(0, cons(s(s(s(y0))), cons(z1, cons(y2, y3))))) -> c2(SIEVE(cons(s(s(s(y0))), cons(z1, cons(y2, y3))))) SIEVE(cons(0, cons(s(s(s(s(y0)))), cons(z1, cons(y2, cons(y3, y4)))))) -> c2(SIEVE(cons(s(s(s(s(y0)))), cons(z1, cons(y2, cons(y3, y4)))))) SIEVE(cons(0, cons(s(s(s(0))), cons(z1, cons(y1, cons(y2, cons(y3, y4))))))) -> c2(SIEVE(cons(s(s(s(0))), cons(z1, cons(y1, cons(y2, cons(y3, y4))))))) SIEVE(cons(0, cons(s(s(0)), cons(z1, cons(y1, cons(y2, cons(y3, cons(y4, y5)))))))) -> c2(SIEVE(cons(s(s(0)), cons(z1, cons(y1, cons(y2, cons(y3, cons(y4, y5)))))))) S tuples: NATS(s(s(x0))) -> c4(NATS(s(s(s(x0))))) SIEVE(cons(s(0), cons(x0, cons(z0, z1)))) -> c3(SIEVE(cons(0, cons(0, filter(z1, 0, 0)))), FILTER(cons(x0, cons(z0, z1)), 0, 0)) SIEVE(cons(s(s(0)), cons(x1, cons(z0, z1)))) -> c3(SIEVE(cons(x1, cons(0, filter(z1, s(0), s(0))))), FILTER(cons(x1, cons(z0, z1)), s(0), s(0))) SIEVE(cons(s(s(s(z2))), cons(x1, cons(z0, z1)))) -> c3(SIEVE(cons(x1, cons(z0, filter(z1, z2, s(s(z2)))))), FILTER(cons(x1, cons(z0, z1)), s(s(z2)), s(s(z2)))) FILTER(cons(z0, cons(z1, cons(y1, y2))), 0, 0) -> c(FILTER(cons(z1, cons(y1, y2)), 0, 0)) FILTER(cons(z0, cons(z1, cons(y1, y2))), 0, s(s(y3))) -> c(FILTER(cons(z1, cons(y1, y2)), s(s(y3)), s(s(y3)))) FILTER(cons(z0, cons(z1, cons(y1, cons(y2, y3)))), 0, s(0)) -> c(FILTER(cons(z1, cons(y1, cons(y2, y3))), s(0), s(0))) FILTER(cons(z0, cons(z1, cons(y1, y2))), s(s(s(y3))), z4) -> c1(FILTER(cons(z1, cons(y1, y2)), s(s(y3)), z4)) FILTER(cons(z0, cons(z1, cons(y1, cons(y2, y3)))), s(s(0)), 0) -> c1(FILTER(cons(z1, cons(y1, cons(y2, y3))), s(0), 0)) FILTER(cons(z0, cons(z1, cons(y1, cons(y2, y3)))), s(s(0)), s(y4)) -> c1(FILTER(cons(z1, cons(y1, cons(y2, y3))), s(0), s(y4))) FILTER(cons(z0, cons(z1, cons(z2, cons(y2, y3)))), s(0), 0) -> c1(FILTER(cons(z1, cons(z2, cons(y2, y3))), 0, 0)) FILTER(cons(z0, cons(z1, cons(z2, cons(y2, y3)))), s(0), s(s(y4))) -> c1(FILTER(cons(z1, cons(z2, cons(y2, y3))), 0, s(s(y4)))) FILTER(cons(z0, cons(z1, cons(z2, cons(y2, cons(y3, y4))))), s(0), s(0)) -> c1(FILTER(cons(z1, cons(z2, cons(y2, cons(y3, y4)))), 0, s(0))) SIEVE(cons(0, cons(0, cons(0, y0)))) -> c2(SIEVE(cons(0, cons(0, y0)))) SIEVE(cons(0, cons(0, cons(s(0), cons(y0, y1))))) -> c2(SIEVE(cons(0, cons(s(0), cons(y0, y1))))) SIEVE(cons(0, cons(0, cons(s(s(y0)), cons(y1, y2))))) -> c2(SIEVE(cons(0, cons(s(s(y0)), cons(y1, y2))))) SIEVE(cons(0, cons(s(0), cons(z0, cons(y1, y2))))) -> c2(SIEVE(cons(s(0), cons(z0, cons(y1, y2))))) SIEVE(cons(0, cons(s(0), cons(z0, cons(y1, cons(y2, y3)))))) -> c2(SIEVE(cons(s(0), cons(z0, cons(y1, cons(y2, y3)))))) SIEVE(cons(0, cons(s(s(0)), cons(z1, cons(y1, y2))))) -> c2(SIEVE(cons(s(s(0)), cons(z1, cons(y1, y2))))) SIEVE(cons(0, cons(s(s(s(y0))), cons(z1, cons(y2, y3))))) -> c2(SIEVE(cons(s(s(s(y0))), cons(z1, cons(y2, y3))))) SIEVE(cons(0, cons(s(s(s(s(y0)))), cons(z1, cons(y2, cons(y3, y4)))))) -> c2(SIEVE(cons(s(s(s(s(y0)))), cons(z1, cons(y2, cons(y3, y4)))))) SIEVE(cons(0, cons(s(s(s(0))), cons(z1, cons(y1, cons(y2, cons(y3, y4))))))) -> c2(SIEVE(cons(s(s(s(0))), cons(z1, cons(y1, cons(y2, cons(y3, y4))))))) SIEVE(cons(0, cons(s(s(0)), cons(z1, cons(y1, cons(y2, cons(y3, cons(y4, y5)))))))) -> c2(SIEVE(cons(s(s(0)), cons(z1, cons(y1, cons(y2, cons(y3, cons(y4, y5)))))))) K tuples: ZPRIMES -> c6(SIEVE(nats(s(s(0))))) SIEVE(cons(s(0), cons(z0, cons(y1, cons(y2, y3))))) -> c3(FILTER(cons(z0, cons(y1, cons(y2, y3))), 0, 0)) SIEVE(cons(s(s(s(s(y4)))), cons(z1, cons(y1, cons(y2, y3))))) -> c3(FILTER(cons(z1, cons(y1, cons(y2, y3))), s(s(s(y4))), s(s(s(y4))))) SIEVE(cons(s(s(s(0))), cons(z1, cons(y1, cons(y2, cons(y3, y4)))))) -> c3(FILTER(cons(z1, cons(y1, cons(y2, cons(y3, y4)))), s(s(0)), s(s(0)))) SIEVE(cons(s(s(0)), cons(z1, cons(y1, cons(y2, cons(y3, cons(y4, y5))))))) -> c3(FILTER(cons(z1, cons(y1, cons(y2, cons(y3, cons(y4, y5))))), s(0), s(0))) Defined Rule Symbols: filter_3, nats_1 Defined Pair Symbols: NATS_1, ZPRIMES, SIEVE_1, FILTER_3 Compound Symbols: c4_1, c6_1, c3_2, c_1, c1_1, c2_1, c3_1 ---------------------------------------- (93) CdtRuleRemovalProof (UPPER BOUND(ADD(n^2))) Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S. ZPRIMES -> c6(SIEVE(cons(s(s(0)), cons(s(s(s(0))), cons(s(s(s(s(0)))), cons(s(s(s(s(s(0))))), nats(s(s(s(s(s(s(0))))))))))))) SIEVE(cons(s(0), cons(x0, cons(z0, z1)))) -> c3(SIEVE(cons(0, cons(0, filter(z1, 0, 0)))), FILTER(cons(x0, cons(z0, z1)), 0, 0)) We considered the (Usable) Rules: filter(cons(z0, z1), 0, z2) -> cons(0, filter(z1, z2, z2)) filter(cons(z0, z1), s(z2), z3) -> cons(z0, filter(z1, z2, z3)) nats(z0) -> cons(z0, nats(s(z0))) And the Tuples: NATS(s(s(x0))) -> c4(NATS(s(s(s(x0))))) ZPRIMES -> c6(SIEVE(cons(s(s(0)), cons(s(s(s(0))), cons(s(s(s(s(0)))), cons(s(s(s(s(s(0))))), nats(s(s(s(s(s(s(0))))))))))))) SIEVE(cons(s(0), cons(x0, cons(z0, z1)))) -> c3(SIEVE(cons(0, cons(0, filter(z1, 0, 0)))), FILTER(cons(x0, cons(z0, z1)), 0, 0)) SIEVE(cons(s(s(0)), cons(x1, cons(z0, z1)))) -> c3(SIEVE(cons(x1, cons(0, filter(z1, s(0), s(0))))), FILTER(cons(x1, cons(z0, z1)), s(0), s(0))) SIEVE(cons(s(s(s(z2))), cons(x1, cons(z0, z1)))) -> c3(SIEVE(cons(x1, cons(z0, filter(z1, z2, s(s(z2)))))), FILTER(cons(x1, cons(z0, z1)), s(s(z2)), s(s(z2)))) FILTER(cons(z0, cons(z1, cons(y1, y2))), 0, 0) -> c(FILTER(cons(z1, cons(y1, y2)), 0, 0)) FILTER(cons(z0, cons(z1, cons(y1, y2))), 0, s(s(y3))) -> c(FILTER(cons(z1, cons(y1, y2)), s(s(y3)), s(s(y3)))) FILTER(cons(z0, cons(z1, cons(y1, cons(y2, y3)))), 0, s(0)) -> c(FILTER(cons(z1, cons(y1, cons(y2, y3))), s(0), s(0))) FILTER(cons(z0, cons(z1, cons(y1, y2))), s(s(s(y3))), z4) -> c1(FILTER(cons(z1, cons(y1, y2)), s(s(y3)), z4)) FILTER(cons(z0, cons(z1, cons(y1, cons(y2, y3)))), s(s(0)), 0) -> c1(FILTER(cons(z1, cons(y1, cons(y2, y3))), s(0), 0)) FILTER(cons(z0, cons(z1, cons(y1, cons(y2, y3)))), s(s(0)), s(y4)) -> c1(FILTER(cons(z1, cons(y1, cons(y2, y3))), s(0), s(y4))) FILTER(cons(z0, cons(z1, cons(z2, cons(y2, y3)))), s(0), 0) -> c1(FILTER(cons(z1, cons(z2, cons(y2, y3))), 0, 0)) FILTER(cons(z0, cons(z1, cons(z2, cons(y2, y3)))), s(0), s(s(y4))) -> c1(FILTER(cons(z1, cons(z2, cons(y2, y3))), 0, s(s(y4)))) FILTER(cons(z0, cons(z1, cons(z2, cons(y2, cons(y3, y4))))), s(0), s(0)) -> c1(FILTER(cons(z1, cons(z2, cons(y2, cons(y3, y4)))), 0, s(0))) SIEVE(cons(0, cons(0, cons(0, y0)))) -> c2(SIEVE(cons(0, cons(0, y0)))) SIEVE(cons(0, cons(0, cons(s(0), cons(y0, y1))))) -> c2(SIEVE(cons(0, cons(s(0), cons(y0, y1))))) SIEVE(cons(0, cons(0, cons(s(s(y0)), cons(y1, y2))))) -> c2(SIEVE(cons(0, cons(s(s(y0)), cons(y1, y2))))) SIEVE(cons(s(0), cons(z0, cons(y1, cons(y2, y3))))) -> c3(FILTER(cons(z0, cons(y1, cons(y2, y3))), 0, 0)) SIEVE(cons(0, cons(s(0), cons(z0, cons(y1, y2))))) -> c2(SIEVE(cons(s(0), cons(z0, cons(y1, y2))))) SIEVE(cons(0, cons(s(0), cons(z0, cons(y1, cons(y2, y3)))))) -> c2(SIEVE(cons(s(0), cons(z0, cons(y1, cons(y2, y3)))))) SIEVE(cons(s(s(s(s(y4)))), cons(z1, cons(y1, cons(y2, y3))))) -> c3(FILTER(cons(z1, cons(y1, cons(y2, y3))), s(s(s(y4))), s(s(s(y4))))) SIEVE(cons(s(s(s(0))), cons(z1, cons(y1, cons(y2, cons(y3, y4)))))) -> c3(FILTER(cons(z1, cons(y1, cons(y2, cons(y3, y4)))), s(s(0)), s(s(0)))) SIEVE(cons(s(s(0)), cons(z1, cons(y1, cons(y2, cons(y3, cons(y4, y5))))))) -> c3(FILTER(cons(z1, cons(y1, cons(y2, cons(y3, cons(y4, y5))))), s(0), s(0))) SIEVE(cons(0, cons(s(s(0)), cons(z1, cons(y1, y2))))) -> c2(SIEVE(cons(s(s(0)), cons(z1, cons(y1, y2))))) SIEVE(cons(0, cons(s(s(s(y0))), cons(z1, cons(y2, y3))))) -> c2(SIEVE(cons(s(s(s(y0))), cons(z1, cons(y2, y3))))) SIEVE(cons(0, cons(s(s(s(s(y0)))), cons(z1, cons(y2, cons(y3, y4)))))) -> c2(SIEVE(cons(s(s(s(s(y0)))), cons(z1, cons(y2, cons(y3, y4)))))) SIEVE(cons(0, cons(s(s(s(0))), cons(z1, cons(y1, cons(y2, cons(y3, y4))))))) -> c2(SIEVE(cons(s(s(s(0))), cons(z1, cons(y1, cons(y2, cons(y3, y4))))))) SIEVE(cons(0, cons(s(s(0)), cons(z1, cons(y1, cons(y2, cons(y3, cons(y4, y5)))))))) -> c2(SIEVE(cons(s(s(0)), cons(z1, cons(y1, cons(y2, cons(y3, cons(y4, y5)))))))) The order we found is given by the following interpretation: Matrix interpretation [MATRO]: Non-tuple symbols: <<< M( nats_1(x_1) ) = [[0], [0]] + [[1, 1], [0, 0]] * x_1 >>> <<< M( s_1(x_1) ) = [[0], [0]] + [[0, 1], [0, 0]] * x_1 >>> <<< M( filter_3(x_1, ..., x_3) ) = [[0], [0]] + [[1, 0], [0, 0]] * x_1 + [[0, 0], [0, 0]] * x_2 + [[0, 0], [0, 0]] * x_3 >>> <<< M( 0 ) = [[0], [2]] >>> <<< M( cons_2(x_1, x_2) ) = [[0], [0]] + [[1, 0], [0, 0]] * x_1 + [[1, 0], [0, 0]] * x_2 >>> Tuple symbols: <<< M( SIEVE_1(x_1) ) = [[0], [2]] + [[1, 0], [0, 0]] * x_1 >>> <<< M( c_1(x_1) ) = [[0], [0]] + [[1, 0], [0, 0]] * x_1 >>> <<< M( c1_1(x_1) ) = [[0], [0]] + [[1, 0], [0, 0]] * x_1 >>> <<< M( FILTER_3(x_1, ..., x_3) ) = [[0], [0]] + [[0, 0], [0, 0]] * x_1 + [[0, 0], [0, 0]] * x_2 + [[0, 0], [0, 0]] * x_3 >>> <<< M( c6_1(x_1) ) = [[0], [0]] + [[1, 0], [0, 0]] * x_1 >>> <<< M( NATS_1(x_1) ) = [[0], [1]] + [[0, 0], [0, 0]] * x_1 >>> <<< M( c3_2(x_1, x_2) ) = [[0], [2]] + [[1, 0], [0, 0]] * x_1 + [[1, 0], [0, 0]] * x_2 >>> <<< M( c3_1(x_1) ) = [[0], [0]] + [[1, 0], [0, 0]] * x_1 >>> <<< M( c4_1(x_1) ) = [[0], [0]] + [[1, 0], [0, 0]] * x_1 >>> <<< M( ZPRIMES ) = [[4], [0]] >>> <<< M( c2_1(x_1) ) = [[0], [0]] + [[1, 0], [0, 0]] * x_1 >>> Matrix type: We used a basic matrix type which is not further parametrizeable. As matrix orders are CE-compatible, we used usable rules w.r.t. argument filtering in the order. ---------------------------------------- (94) Obligation: Complexity Dependency Tuples Problem Rules: filter(cons(z0, z1), 0, z2) -> cons(0, filter(z1, z2, z2)) filter(cons(z0, z1), s(z2), z3) -> cons(z0, filter(z1, z2, z3)) nats(z0) -> cons(z0, nats(s(z0))) Tuples: NATS(s(s(x0))) -> c4(NATS(s(s(s(x0))))) ZPRIMES -> c6(SIEVE(cons(s(s(0)), cons(s(s(s(0))), cons(s(s(s(s(0)))), cons(s(s(s(s(s(0))))), nats(s(s(s(s(s(s(0))))))))))))) SIEVE(cons(s(0), cons(x0, cons(z0, z1)))) -> c3(SIEVE(cons(0, cons(0, filter(z1, 0, 0)))), FILTER(cons(x0, cons(z0, z1)), 0, 0)) SIEVE(cons(s(s(0)), cons(x1, cons(z0, z1)))) -> c3(SIEVE(cons(x1, cons(0, filter(z1, s(0), s(0))))), FILTER(cons(x1, cons(z0, z1)), s(0), s(0))) SIEVE(cons(s(s(s(z2))), cons(x1, cons(z0, z1)))) -> c3(SIEVE(cons(x1, cons(z0, filter(z1, z2, s(s(z2)))))), FILTER(cons(x1, cons(z0, z1)), s(s(z2)), s(s(z2)))) FILTER(cons(z0, cons(z1, cons(y1, y2))), 0, 0) -> c(FILTER(cons(z1, cons(y1, y2)), 0, 0)) FILTER(cons(z0, cons(z1, cons(y1, y2))), 0, s(s(y3))) -> c(FILTER(cons(z1, cons(y1, y2)), s(s(y3)), s(s(y3)))) FILTER(cons(z0, cons(z1, cons(y1, cons(y2, y3)))), 0, s(0)) -> c(FILTER(cons(z1, cons(y1, cons(y2, y3))), s(0), s(0))) FILTER(cons(z0, cons(z1, cons(y1, y2))), s(s(s(y3))), z4) -> c1(FILTER(cons(z1, cons(y1, y2)), s(s(y3)), z4)) FILTER(cons(z0, cons(z1, cons(y1, cons(y2, y3)))), s(s(0)), 0) -> c1(FILTER(cons(z1, cons(y1, cons(y2, y3))), s(0), 0)) FILTER(cons(z0, cons(z1, cons(y1, cons(y2, y3)))), s(s(0)), s(y4)) -> c1(FILTER(cons(z1, cons(y1, cons(y2, y3))), s(0), s(y4))) FILTER(cons(z0, cons(z1, cons(z2, cons(y2, y3)))), s(0), 0) -> c1(FILTER(cons(z1, cons(z2, cons(y2, y3))), 0, 0)) FILTER(cons(z0, cons(z1, cons(z2, cons(y2, y3)))), s(0), s(s(y4))) -> c1(FILTER(cons(z1, cons(z2, cons(y2, y3))), 0, s(s(y4)))) FILTER(cons(z0, cons(z1, cons(z2, cons(y2, cons(y3, y4))))), s(0), s(0)) -> c1(FILTER(cons(z1, cons(z2, cons(y2, cons(y3, y4)))), 0, s(0))) SIEVE(cons(0, cons(0, cons(0, y0)))) -> c2(SIEVE(cons(0, cons(0, y0)))) SIEVE(cons(0, cons(0, cons(s(0), cons(y0, y1))))) -> c2(SIEVE(cons(0, cons(s(0), cons(y0, y1))))) SIEVE(cons(0, cons(0, cons(s(s(y0)), cons(y1, y2))))) -> c2(SIEVE(cons(0, cons(s(s(y0)), cons(y1, y2))))) SIEVE(cons(s(0), cons(z0, cons(y1, cons(y2, y3))))) -> c3(FILTER(cons(z0, cons(y1, cons(y2, y3))), 0, 0)) SIEVE(cons(0, cons(s(0), cons(z0, cons(y1, y2))))) -> c2(SIEVE(cons(s(0), cons(z0, cons(y1, y2))))) SIEVE(cons(0, cons(s(0), cons(z0, cons(y1, cons(y2, y3)))))) -> c2(SIEVE(cons(s(0), cons(z0, cons(y1, cons(y2, y3)))))) SIEVE(cons(s(s(s(s(y4)))), cons(z1, cons(y1, cons(y2, y3))))) -> c3(FILTER(cons(z1, cons(y1, cons(y2, y3))), s(s(s(y4))), s(s(s(y4))))) SIEVE(cons(s(s(s(0))), cons(z1, cons(y1, cons(y2, cons(y3, y4)))))) -> c3(FILTER(cons(z1, cons(y1, cons(y2, cons(y3, y4)))), s(s(0)), s(s(0)))) SIEVE(cons(s(s(0)), cons(z1, cons(y1, cons(y2, cons(y3, cons(y4, y5))))))) -> c3(FILTER(cons(z1, cons(y1, cons(y2, cons(y3, cons(y4, y5))))), s(0), s(0))) SIEVE(cons(0, cons(s(s(0)), cons(z1, cons(y1, y2))))) -> c2(SIEVE(cons(s(s(0)), cons(z1, cons(y1, y2))))) SIEVE(cons(0, cons(s(s(s(y0))), cons(z1, cons(y2, y3))))) -> c2(SIEVE(cons(s(s(s(y0))), cons(z1, cons(y2, y3))))) SIEVE(cons(0, cons(s(s(s(s(y0)))), cons(z1, cons(y2, cons(y3, y4)))))) -> c2(SIEVE(cons(s(s(s(s(y0)))), cons(z1, cons(y2, cons(y3, y4)))))) SIEVE(cons(0, cons(s(s(s(0))), cons(z1, cons(y1, cons(y2, cons(y3, y4))))))) -> c2(SIEVE(cons(s(s(s(0))), cons(z1, cons(y1, cons(y2, cons(y3, y4))))))) SIEVE(cons(0, cons(s(s(0)), cons(z1, cons(y1, cons(y2, cons(y3, cons(y4, y5)))))))) -> c2(SIEVE(cons(s(s(0)), cons(z1, cons(y1, cons(y2, cons(y3, cons(y4, y5)))))))) S tuples: NATS(s(s(x0))) -> c4(NATS(s(s(s(x0))))) SIEVE(cons(s(s(0)), cons(x1, cons(z0, z1)))) -> c3(SIEVE(cons(x1, cons(0, filter(z1, s(0), s(0))))), FILTER(cons(x1, cons(z0, z1)), s(0), s(0))) SIEVE(cons(s(s(s(z2))), cons(x1, cons(z0, z1)))) -> c3(SIEVE(cons(x1, cons(z0, filter(z1, z2, s(s(z2)))))), FILTER(cons(x1, cons(z0, z1)), s(s(z2)), s(s(z2)))) FILTER(cons(z0, cons(z1, cons(y1, y2))), 0, 0) -> c(FILTER(cons(z1, cons(y1, y2)), 0, 0)) FILTER(cons(z0, cons(z1, cons(y1, y2))), 0, s(s(y3))) -> c(FILTER(cons(z1, cons(y1, y2)), s(s(y3)), s(s(y3)))) FILTER(cons(z0, cons(z1, cons(y1, cons(y2, y3)))), 0, s(0)) -> c(FILTER(cons(z1, cons(y1, cons(y2, y3))), s(0), s(0))) FILTER(cons(z0, cons(z1, cons(y1, y2))), s(s(s(y3))), z4) -> c1(FILTER(cons(z1, cons(y1, y2)), s(s(y3)), z4)) FILTER(cons(z0, cons(z1, cons(y1, cons(y2, y3)))), s(s(0)), 0) -> c1(FILTER(cons(z1, cons(y1, cons(y2, y3))), s(0), 0)) FILTER(cons(z0, cons(z1, cons(y1, cons(y2, y3)))), s(s(0)), s(y4)) -> c1(FILTER(cons(z1, cons(y1, cons(y2, y3))), s(0), s(y4))) FILTER(cons(z0, cons(z1, cons(z2, cons(y2, y3)))), s(0), 0) -> c1(FILTER(cons(z1, cons(z2, cons(y2, y3))), 0, 0)) FILTER(cons(z0, cons(z1, cons(z2, cons(y2, y3)))), s(0), s(s(y4))) -> c1(FILTER(cons(z1, cons(z2, cons(y2, y3))), 0, s(s(y4)))) FILTER(cons(z0, cons(z1, cons(z2, cons(y2, cons(y3, y4))))), s(0), s(0)) -> c1(FILTER(cons(z1, cons(z2, cons(y2, cons(y3, y4)))), 0, s(0))) SIEVE(cons(0, cons(0, cons(0, y0)))) -> c2(SIEVE(cons(0, cons(0, y0)))) SIEVE(cons(0, cons(0, cons(s(0), cons(y0, y1))))) -> c2(SIEVE(cons(0, cons(s(0), cons(y0, y1))))) SIEVE(cons(0, cons(0, cons(s(s(y0)), cons(y1, y2))))) -> c2(SIEVE(cons(0, cons(s(s(y0)), cons(y1, y2))))) SIEVE(cons(0, cons(s(0), cons(z0, cons(y1, y2))))) -> c2(SIEVE(cons(s(0), cons(z0, cons(y1, y2))))) SIEVE(cons(0, cons(s(0), cons(z0, cons(y1, cons(y2, y3)))))) -> c2(SIEVE(cons(s(0), cons(z0, cons(y1, cons(y2, y3)))))) SIEVE(cons(0, cons(s(s(0)), cons(z1, cons(y1, y2))))) -> c2(SIEVE(cons(s(s(0)), cons(z1, cons(y1, y2))))) SIEVE(cons(0, cons(s(s(s(y0))), cons(z1, cons(y2, y3))))) -> c2(SIEVE(cons(s(s(s(y0))), cons(z1, cons(y2, y3))))) SIEVE(cons(0, cons(s(s(s(s(y0)))), cons(z1, cons(y2, cons(y3, y4)))))) -> c2(SIEVE(cons(s(s(s(s(y0)))), cons(z1, cons(y2, cons(y3, y4)))))) SIEVE(cons(0, cons(s(s(s(0))), cons(z1, cons(y1, cons(y2, cons(y3, y4))))))) -> c2(SIEVE(cons(s(s(s(0))), cons(z1, cons(y1, cons(y2, cons(y3, y4))))))) SIEVE(cons(0, cons(s(s(0)), cons(z1, cons(y1, cons(y2, cons(y3, cons(y4, y5)))))))) -> c2(SIEVE(cons(s(s(0)), cons(z1, cons(y1, cons(y2, cons(y3, cons(y4, y5)))))))) K tuples: ZPRIMES -> c6(SIEVE(nats(s(s(0))))) SIEVE(cons(s(0), cons(z0, cons(y1, cons(y2, y3))))) -> c3(FILTER(cons(z0, cons(y1, cons(y2, y3))), 0, 0)) SIEVE(cons(s(s(s(s(y4)))), cons(z1, cons(y1, cons(y2, y3))))) -> c3(FILTER(cons(z1, cons(y1, cons(y2, y3))), s(s(s(y4))), s(s(s(y4))))) SIEVE(cons(s(s(s(0))), cons(z1, cons(y1, cons(y2, cons(y3, y4)))))) -> c3(FILTER(cons(z1, cons(y1, cons(y2, cons(y3, y4)))), s(s(0)), s(s(0)))) SIEVE(cons(s(s(0)), cons(z1, cons(y1, cons(y2, cons(y3, cons(y4, y5))))))) -> c3(FILTER(cons(z1, cons(y1, cons(y2, cons(y3, cons(y4, y5))))), s(0), s(0))) ZPRIMES -> c6(SIEVE(cons(s(s(0)), cons(s(s(s(0))), cons(s(s(s(s(0)))), cons(s(s(s(s(s(0))))), nats(s(s(s(s(s(s(0))))))))))))) SIEVE(cons(s(0), cons(x0, cons(z0, z1)))) -> c3(SIEVE(cons(0, cons(0, filter(z1, 0, 0)))), FILTER(cons(x0, cons(z0, z1)), 0, 0)) Defined Rule Symbols: filter_3, nats_1 Defined Pair Symbols: NATS_1, ZPRIMES, SIEVE_1, FILTER_3 Compound Symbols: c4_1, c6_1, c3_2, c_1, c1_1, c2_1, c3_1