WORST_CASE(Omega(n^1),O(n^1)) proof of /export/starexec/sandbox2/benchmark/theBenchmark.trs # AProVE Commit ID: c69e44bd14796315568835c1ffa2502984884775 mhark 20210624 unpublished The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, n^1). (0) CpxRelTRS (1) SInnermostTerminationProof [BOTH CONCRETE BOUNDS(ID, ID), 212 ms] (2) CpxRelTRS (3) CpxTrsToCdtProof [UPPER BOUND(ID), 6 ms] (4) CdtProblem (5) CdtLeafRemovalProof [BOTH BOUNDS(ID, ID), 0 ms] (6) CdtProblem (7) CdtGraphSplitRhsProof [BOTH BOUNDS(ID, ID), 0 ms] (8) CdtProblem (9) CdtLeafRemovalProof [ComplexityIfPolyImplication, 0 ms] (10) CdtProblem (11) CdtKnowledgeProof [BOTH BOUNDS(ID, ID), 0 ms] (12) CdtProblem (13) CdtUsableRulesProof [BOTH BOUNDS(ID, ID), 0 ms] (14) CdtProblem (15) CdtRuleRemovalProof [UPPER BOUND(ADD(n^1)), 125 ms] (16) CdtProblem (17) CdtRuleRemovalProof [UPPER BOUND(ADD(n^1)), 28 ms] (18) CdtProblem (19) SIsEmptyProof [BOTH BOUNDS(ID, ID), 0 ms] (20) BOUNDS(1, 1) (21) RelTrsToDecreasingLoopProblemProof [LOWER BOUND(ID), 0 ms] (22) TRS for Loop Detection (23) DecreasingLoopProof [LOWER BOUND(ID), 0 ms] (24) BEST (25) proven lower bound (26) LowerBoundPropagationProof [FINISHED, 0 ms] (27) BOUNDS(n^1, INF) (28) TRS for Loop Detection ---------------------------------------- (0) Obligation: The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, n^1). The TRS R consists of the following rules: WALK#1(Leaf(z0)) -> c WALK#1(Node(z0, z1)) -> c1(WALK#1(z0)) WALK#1(Node(z0, z1)) -> c2(WALK#1(z1)) COMP_F_G#1(comp_f_g(z0, z1), comp_f_g(z2, z3), z4) -> c3(COMP_F_G#1(z0, z1, comp_f_g#1(z2, z3, z4)), COMP_F_G#1(z2, z3, z4)) COMP_F_G#1(comp_f_g(z0, z1), cons_x(z2), z3) -> c4(COMP_F_G#1(z0, z1, Cons(z2, z3))) COMP_F_G#1(cons_x(z0), comp_f_g(z1, z2), z3) -> c5(COMP_F_G#1(z1, z2, z3)) COMP_F_G#1(cons_x(z0), cons_x(z1), z2) -> c6 MAIN(Leaf(z0)) -> c7 MAIN(Node(z0, z1)) -> c8(COMP_F_G#1(walk#1(z0), walk#1(z1), Nil), WALK#1(z0)) MAIN(Node(z0, z1)) -> c9(COMP_F_G#1(walk#1(z0), walk#1(z1), Nil), WALK#1(z1)) The (relative) TRS S consists of the following rules: walk#1(Leaf(z0)) -> cons_x(z0) walk#1(Node(z0, z1)) -> comp_f_g(walk#1(z0), walk#1(z1)) comp_f_g#1(comp_f_g(z0, z1), comp_f_g(z2, z3), z4) -> comp_f_g#1(z0, z1, comp_f_g#1(z2, z3, z4)) comp_f_g#1(comp_f_g(z0, z1), cons_x(z2), z3) -> comp_f_g#1(z0, z1, Cons(z2, z3)) comp_f_g#1(cons_x(z0), comp_f_g(z1, z2), z3) -> Cons(z0, comp_f_g#1(z1, z2, z3)) comp_f_g#1(cons_x(z0), cons_x(z1), z2) -> Cons(z0, Cons(z1, z2)) main(Leaf(z0)) -> Cons(z0, Nil) main(Node(z0, z1)) -> comp_f_g#1(walk#1(z0), walk#1(z1), Nil) Rewrite Strategy: INNERMOST ---------------------------------------- (1) SInnermostTerminationProof (BOTH CONCRETE BOUNDS(ID, ID)) proved innermost termination of relative rules ---------------------------------------- (2) Obligation: The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, n^1). The TRS R consists of the following rules: WALK#1(Leaf(z0)) -> c WALK#1(Node(z0, z1)) -> c1(WALK#1(z0)) WALK#1(Node(z0, z1)) -> c2(WALK#1(z1)) COMP_F_G#1(comp_f_g(z0, z1), comp_f_g(z2, z3), z4) -> c3(COMP_F_G#1(z0, z1, comp_f_g#1(z2, z3, z4)), COMP_F_G#1(z2, z3, z4)) COMP_F_G#1(comp_f_g(z0, z1), cons_x(z2), z3) -> c4(COMP_F_G#1(z0, z1, Cons(z2, z3))) COMP_F_G#1(cons_x(z0), comp_f_g(z1, z2), z3) -> c5(COMP_F_G#1(z1, z2, z3)) COMP_F_G#1(cons_x(z0), cons_x(z1), z2) -> c6 MAIN(Leaf(z0)) -> c7 MAIN(Node(z0, z1)) -> c8(COMP_F_G#1(walk#1(z0), walk#1(z1), Nil), WALK#1(z0)) MAIN(Node(z0, z1)) -> c9(COMP_F_G#1(walk#1(z0), walk#1(z1), Nil), WALK#1(z1)) The (relative) TRS S consists of the following rules: walk#1(Leaf(z0)) -> cons_x(z0) walk#1(Node(z0, z1)) -> comp_f_g(walk#1(z0), walk#1(z1)) comp_f_g#1(comp_f_g(z0, z1), comp_f_g(z2, z3), z4) -> comp_f_g#1(z0, z1, comp_f_g#1(z2, z3, z4)) comp_f_g#1(comp_f_g(z0, z1), cons_x(z2), z3) -> comp_f_g#1(z0, z1, Cons(z2, z3)) comp_f_g#1(cons_x(z0), comp_f_g(z1, z2), z3) -> Cons(z0, comp_f_g#1(z1, z2, z3)) comp_f_g#1(cons_x(z0), cons_x(z1), z2) -> Cons(z0, Cons(z1, z2)) main(Leaf(z0)) -> Cons(z0, Nil) main(Node(z0, z1)) -> comp_f_g#1(walk#1(z0), walk#1(z1), Nil) Rewrite Strategy: INNERMOST ---------------------------------------- (3) CpxTrsToCdtProof (UPPER BOUND(ID)) Converted Cpx (relative) TRS to CDT ---------------------------------------- (4) Obligation: Complexity Dependency Tuples Problem Rules: walk#1(Leaf(z0)) -> cons_x(z0) walk#1(Node(z0, z1)) -> comp_f_g(walk#1(z0), walk#1(z1)) comp_f_g#1(comp_f_g(z0, z1), comp_f_g(z2, z3), z4) -> comp_f_g#1(z0, z1, comp_f_g#1(z2, z3, z4)) comp_f_g#1(comp_f_g(z0, z1), cons_x(z2), z3) -> comp_f_g#1(z0, z1, Cons(z2, z3)) comp_f_g#1(cons_x(z0), comp_f_g(z1, z2), z3) -> Cons(z0, comp_f_g#1(z1, z2, z3)) comp_f_g#1(cons_x(z0), cons_x(z1), z2) -> Cons(z0, Cons(z1, z2)) main(Leaf(z0)) -> Cons(z0, Nil) main(Node(z0, z1)) -> comp_f_g#1(walk#1(z0), walk#1(z1), Nil) WALK#1(Leaf(z0)) -> c WALK#1(Node(z0, z1)) -> c1(WALK#1(z0)) WALK#1(Node(z0, z1)) -> c2(WALK#1(z1)) COMP_F_G#1(comp_f_g(z0, z1), comp_f_g(z2, z3), z4) -> c3(COMP_F_G#1(z0, z1, comp_f_g#1(z2, z3, z4)), COMP_F_G#1(z2, z3, z4)) COMP_F_G#1(comp_f_g(z0, z1), cons_x(z2), z3) -> c4(COMP_F_G#1(z0, z1, Cons(z2, z3))) COMP_F_G#1(cons_x(z0), comp_f_g(z1, z2), z3) -> c5(COMP_F_G#1(z1, z2, z3)) COMP_F_G#1(cons_x(z0), cons_x(z1), z2) -> c6 MAIN(Leaf(z0)) -> c7 MAIN(Node(z0, z1)) -> c8(COMP_F_G#1(walk#1(z0), walk#1(z1), Nil), WALK#1(z0)) MAIN(Node(z0, z1)) -> c9(COMP_F_G#1(walk#1(z0), walk#1(z1), Nil), WALK#1(z1)) Tuples: WALK#1'(Leaf(z0)) -> c10 WALK#1'(Node(z0, z1)) -> c11(WALK#1'(z0), WALK#1'(z1)) COMP_F_G#1'(comp_f_g(z0, z1), comp_f_g(z2, z3), z4) -> c12(COMP_F_G#1'(z0, z1, comp_f_g#1(z2, z3, z4)), COMP_F_G#1'(z2, z3, z4)) COMP_F_G#1'(comp_f_g(z0, z1), cons_x(z2), z3) -> c13(COMP_F_G#1'(z0, z1, Cons(z2, z3))) COMP_F_G#1'(cons_x(z0), comp_f_g(z1, z2), z3) -> c14(COMP_F_G#1'(z1, z2, z3)) COMP_F_G#1'(cons_x(z0), cons_x(z1), z2) -> c15 MAIN'(Leaf(z0)) -> c16 MAIN'(Node(z0, z1)) -> c17(COMP_F_G#1'(walk#1(z0), walk#1(z1), Nil), WALK#1'(z0), WALK#1'(z1)) WALK#1''(Leaf(z0)) -> c18 WALK#1''(Node(z0, z1)) -> c19(WALK#1''(z0)) WALK#1''(Node(z0, z1)) -> c20(WALK#1''(z1)) COMP_F_G#1''(comp_f_g(z0, z1), comp_f_g(z2, z3), z4) -> c21(COMP_F_G#1''(z0, z1, comp_f_g#1(z2, z3, z4)), COMP_F_G#1'(z2, z3, z4), COMP_F_G#1''(z2, z3, z4)) COMP_F_G#1''(comp_f_g(z0, z1), cons_x(z2), z3) -> c22(COMP_F_G#1''(z0, z1, Cons(z2, z3))) COMP_F_G#1''(cons_x(z0), comp_f_g(z1, z2), z3) -> c23(COMP_F_G#1''(z1, z2, z3)) COMP_F_G#1''(cons_x(z0), cons_x(z1), z2) -> c24 MAIN''(Leaf(z0)) -> c25 MAIN''(Node(z0, z1)) -> c26(COMP_F_G#1''(walk#1(z0), walk#1(z1), Nil), WALK#1'(z0), WALK#1'(z1), WALK#1''(z0)) MAIN''(Node(z0, z1)) -> c27(COMP_F_G#1''(walk#1(z0), walk#1(z1), Nil), WALK#1'(z0), WALK#1'(z1), WALK#1''(z1)) S tuples: WALK#1''(Leaf(z0)) -> c18 WALK#1''(Node(z0, z1)) -> c19(WALK#1''(z0)) WALK#1''(Node(z0, z1)) -> c20(WALK#1''(z1)) COMP_F_G#1''(comp_f_g(z0, z1), comp_f_g(z2, z3), z4) -> c21(COMP_F_G#1''(z0, z1, comp_f_g#1(z2, z3, z4)), COMP_F_G#1'(z2, z3, z4), COMP_F_G#1''(z2, z3, z4)) COMP_F_G#1''(comp_f_g(z0, z1), cons_x(z2), z3) -> c22(COMP_F_G#1''(z0, z1, Cons(z2, z3))) COMP_F_G#1''(cons_x(z0), comp_f_g(z1, z2), z3) -> c23(COMP_F_G#1''(z1, z2, z3)) COMP_F_G#1''(cons_x(z0), cons_x(z1), z2) -> c24 MAIN''(Leaf(z0)) -> c25 MAIN''(Node(z0, z1)) -> c26(COMP_F_G#1''(walk#1(z0), walk#1(z1), Nil), WALK#1'(z0), WALK#1'(z1), WALK#1''(z0)) MAIN''(Node(z0, z1)) -> c27(COMP_F_G#1''(walk#1(z0), walk#1(z1), Nil), WALK#1'(z0), WALK#1'(z1), WALK#1''(z1)) K tuples:none Defined Rule Symbols: WALK#1_1, COMP_F_G#1_3, MAIN_1, walk#1_1, comp_f_g#1_3, main_1 Defined Pair Symbols: WALK#1'_1, COMP_F_G#1'_3, MAIN'_1, WALK#1''_1, COMP_F_G#1''_3, MAIN''_1 Compound Symbols: c10, c11_2, c12_2, c13_1, c14_1, c15, c16, c17_3, c18, c19_1, c20_1, c21_3, c22_1, c23_1, c24, c25, c26_4, c27_4 ---------------------------------------- (5) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID)) Removed 6 trailing nodes: COMP_F_G#1'(cons_x(z0), cons_x(z1), z2) -> c15 COMP_F_G#1''(cons_x(z0), cons_x(z1), z2) -> c24 WALK#1'(Leaf(z0)) -> c10 MAIN''(Leaf(z0)) -> c25 WALK#1''(Leaf(z0)) -> c18 MAIN'(Leaf(z0)) -> c16 ---------------------------------------- (6) Obligation: Complexity Dependency Tuples Problem Rules: walk#1(Leaf(z0)) -> cons_x(z0) walk#1(Node(z0, z1)) -> comp_f_g(walk#1(z0), walk#1(z1)) comp_f_g#1(comp_f_g(z0, z1), comp_f_g(z2, z3), z4) -> comp_f_g#1(z0, z1, comp_f_g#1(z2, z3, z4)) comp_f_g#1(comp_f_g(z0, z1), cons_x(z2), z3) -> comp_f_g#1(z0, z1, Cons(z2, z3)) comp_f_g#1(cons_x(z0), comp_f_g(z1, z2), z3) -> Cons(z0, comp_f_g#1(z1, z2, z3)) comp_f_g#1(cons_x(z0), cons_x(z1), z2) -> Cons(z0, Cons(z1, z2)) main(Leaf(z0)) -> Cons(z0, Nil) main(Node(z0, z1)) -> comp_f_g#1(walk#1(z0), walk#1(z1), Nil) WALK#1(Leaf(z0)) -> c WALK#1(Node(z0, z1)) -> c1(WALK#1(z0)) WALK#1(Node(z0, z1)) -> c2(WALK#1(z1)) COMP_F_G#1(comp_f_g(z0, z1), comp_f_g(z2, z3), z4) -> c3(COMP_F_G#1(z0, z1, comp_f_g#1(z2, z3, z4)), COMP_F_G#1(z2, z3, z4)) COMP_F_G#1(comp_f_g(z0, z1), cons_x(z2), z3) -> c4(COMP_F_G#1(z0, z1, Cons(z2, z3))) COMP_F_G#1(cons_x(z0), comp_f_g(z1, z2), z3) -> c5(COMP_F_G#1(z1, z2, z3)) COMP_F_G#1(cons_x(z0), cons_x(z1), z2) -> c6 MAIN(Leaf(z0)) -> c7 MAIN(Node(z0, z1)) -> c8(COMP_F_G#1(walk#1(z0), walk#1(z1), Nil), WALK#1(z0)) MAIN(Node(z0, z1)) -> c9(COMP_F_G#1(walk#1(z0), walk#1(z1), Nil), WALK#1(z1)) Tuples: WALK#1'(Node(z0, z1)) -> c11(WALK#1'(z0), WALK#1'(z1)) COMP_F_G#1'(comp_f_g(z0, z1), comp_f_g(z2, z3), z4) -> c12(COMP_F_G#1'(z0, z1, comp_f_g#1(z2, z3, z4)), COMP_F_G#1'(z2, z3, z4)) COMP_F_G#1'(comp_f_g(z0, z1), cons_x(z2), z3) -> c13(COMP_F_G#1'(z0, z1, Cons(z2, z3))) COMP_F_G#1'(cons_x(z0), comp_f_g(z1, z2), z3) -> c14(COMP_F_G#1'(z1, z2, z3)) MAIN'(Node(z0, z1)) -> c17(COMP_F_G#1'(walk#1(z0), walk#1(z1), Nil), WALK#1'(z0), WALK#1'(z1)) WALK#1''(Node(z0, z1)) -> c19(WALK#1''(z0)) WALK#1''(Node(z0, z1)) -> c20(WALK#1''(z1)) COMP_F_G#1''(comp_f_g(z0, z1), comp_f_g(z2, z3), z4) -> c21(COMP_F_G#1''(z0, z1, comp_f_g#1(z2, z3, z4)), COMP_F_G#1'(z2, z3, z4), COMP_F_G#1''(z2, z3, z4)) COMP_F_G#1''(comp_f_g(z0, z1), cons_x(z2), z3) -> c22(COMP_F_G#1''(z0, z1, Cons(z2, z3))) COMP_F_G#1''(cons_x(z0), comp_f_g(z1, z2), z3) -> c23(COMP_F_G#1''(z1, z2, z3)) MAIN''(Node(z0, z1)) -> c26(COMP_F_G#1''(walk#1(z0), walk#1(z1), Nil), WALK#1'(z0), WALK#1'(z1), WALK#1''(z0)) MAIN''(Node(z0, z1)) -> c27(COMP_F_G#1''(walk#1(z0), walk#1(z1), Nil), WALK#1'(z0), WALK#1'(z1), WALK#1''(z1)) S tuples: WALK#1''(Node(z0, z1)) -> c19(WALK#1''(z0)) WALK#1''(Node(z0, z1)) -> c20(WALK#1''(z1)) COMP_F_G#1''(comp_f_g(z0, z1), comp_f_g(z2, z3), z4) -> c21(COMP_F_G#1''(z0, z1, comp_f_g#1(z2, z3, z4)), COMP_F_G#1'(z2, z3, z4), COMP_F_G#1''(z2, z3, z4)) COMP_F_G#1''(comp_f_g(z0, z1), cons_x(z2), z3) -> c22(COMP_F_G#1''(z0, z1, Cons(z2, z3))) COMP_F_G#1''(cons_x(z0), comp_f_g(z1, z2), z3) -> c23(COMP_F_G#1''(z1, z2, z3)) MAIN''(Node(z0, z1)) -> c26(COMP_F_G#1''(walk#1(z0), walk#1(z1), Nil), WALK#1'(z0), WALK#1'(z1), WALK#1''(z0)) MAIN''(Node(z0, z1)) -> c27(COMP_F_G#1''(walk#1(z0), walk#1(z1), Nil), WALK#1'(z0), WALK#1'(z1), WALK#1''(z1)) K tuples:none Defined Rule Symbols: WALK#1_1, COMP_F_G#1_3, MAIN_1, walk#1_1, comp_f_g#1_3, main_1 Defined Pair Symbols: WALK#1'_1, COMP_F_G#1'_3, MAIN'_1, WALK#1''_1, COMP_F_G#1''_3, MAIN''_1 Compound Symbols: c11_2, c12_2, c13_1, c14_1, c17_3, c19_1, c20_1, c21_3, c22_1, c23_1, c26_4, c27_4 ---------------------------------------- (7) CdtGraphSplitRhsProof (BOTH BOUNDS(ID, ID)) Split RHS of tuples not part of any SCC ---------------------------------------- (8) Obligation: Complexity Dependency Tuples Problem Rules: walk#1(Leaf(z0)) -> cons_x(z0) walk#1(Node(z0, z1)) -> comp_f_g(walk#1(z0), walk#1(z1)) comp_f_g#1(comp_f_g(z0, z1), comp_f_g(z2, z3), z4) -> comp_f_g#1(z0, z1, comp_f_g#1(z2, z3, z4)) comp_f_g#1(comp_f_g(z0, z1), cons_x(z2), z3) -> comp_f_g#1(z0, z1, Cons(z2, z3)) comp_f_g#1(cons_x(z0), comp_f_g(z1, z2), z3) -> Cons(z0, comp_f_g#1(z1, z2, z3)) comp_f_g#1(cons_x(z0), cons_x(z1), z2) -> Cons(z0, Cons(z1, z2)) main(Leaf(z0)) -> Cons(z0, Nil) main(Node(z0, z1)) -> comp_f_g#1(walk#1(z0), walk#1(z1), Nil) WALK#1(Leaf(z0)) -> c WALK#1(Node(z0, z1)) -> c1(WALK#1(z0)) WALK#1(Node(z0, z1)) -> c2(WALK#1(z1)) COMP_F_G#1(comp_f_g(z0, z1), comp_f_g(z2, z3), z4) -> c3(COMP_F_G#1(z0, z1, comp_f_g#1(z2, z3, z4)), COMP_F_G#1(z2, z3, z4)) COMP_F_G#1(comp_f_g(z0, z1), cons_x(z2), z3) -> c4(COMP_F_G#1(z0, z1, Cons(z2, z3))) COMP_F_G#1(cons_x(z0), comp_f_g(z1, z2), z3) -> c5(COMP_F_G#1(z1, z2, z3)) COMP_F_G#1(cons_x(z0), cons_x(z1), z2) -> c6 MAIN(Leaf(z0)) -> c7 MAIN(Node(z0, z1)) -> c8(COMP_F_G#1(walk#1(z0), walk#1(z1), Nil), WALK#1(z0)) MAIN(Node(z0, z1)) -> c9(COMP_F_G#1(walk#1(z0), walk#1(z1), Nil), WALK#1(z1)) Tuples: WALK#1'(Node(z0, z1)) -> c11(WALK#1'(z0), WALK#1'(z1)) COMP_F_G#1'(comp_f_g(z0, z1), comp_f_g(z2, z3), z4) -> c12(COMP_F_G#1'(z0, z1, comp_f_g#1(z2, z3, z4)), COMP_F_G#1'(z2, z3, z4)) COMP_F_G#1'(comp_f_g(z0, z1), cons_x(z2), z3) -> c13(COMP_F_G#1'(z0, z1, Cons(z2, z3))) COMP_F_G#1'(cons_x(z0), comp_f_g(z1, z2), z3) -> c14(COMP_F_G#1'(z1, z2, z3)) WALK#1''(Node(z0, z1)) -> c19(WALK#1''(z0)) WALK#1''(Node(z0, z1)) -> c20(WALK#1''(z1)) COMP_F_G#1''(comp_f_g(z0, z1), comp_f_g(z2, z3), z4) -> c21(COMP_F_G#1''(z0, z1, comp_f_g#1(z2, z3, z4)), COMP_F_G#1'(z2, z3, z4), COMP_F_G#1''(z2, z3, z4)) COMP_F_G#1''(comp_f_g(z0, z1), cons_x(z2), z3) -> c22(COMP_F_G#1''(z0, z1, Cons(z2, z3))) COMP_F_G#1''(cons_x(z0), comp_f_g(z1, z2), z3) -> c23(COMP_F_G#1''(z1, z2, z3)) MAIN'(Node(z0, z1)) -> c10(COMP_F_G#1'(walk#1(z0), walk#1(z1), Nil)) MAIN'(Node(z0, z1)) -> c10(WALK#1'(z0)) MAIN'(Node(z0, z1)) -> c10(WALK#1'(z1)) MAIN''(Node(z0, z1)) -> c10(COMP_F_G#1''(walk#1(z0), walk#1(z1), Nil)) MAIN''(Node(z0, z1)) -> c10(WALK#1'(z0)) MAIN''(Node(z0, z1)) -> c10(WALK#1'(z1)) MAIN''(Node(z0, z1)) -> c10(WALK#1''(z0)) MAIN''(Node(z0, z1)) -> c10(WALK#1''(z1)) S tuples: WALK#1''(Node(z0, z1)) -> c19(WALK#1''(z0)) WALK#1''(Node(z0, z1)) -> c20(WALK#1''(z1)) COMP_F_G#1''(comp_f_g(z0, z1), comp_f_g(z2, z3), z4) -> c21(COMP_F_G#1''(z0, z1, comp_f_g#1(z2, z3, z4)), COMP_F_G#1'(z2, z3, z4), COMP_F_G#1''(z2, z3, z4)) COMP_F_G#1''(comp_f_g(z0, z1), cons_x(z2), z3) -> c22(COMP_F_G#1''(z0, z1, Cons(z2, z3))) COMP_F_G#1''(cons_x(z0), comp_f_g(z1, z2), z3) -> c23(COMP_F_G#1''(z1, z2, z3)) MAIN''(Node(z0, z1)) -> c10(COMP_F_G#1''(walk#1(z0), walk#1(z1), Nil)) MAIN''(Node(z0, z1)) -> c10(WALK#1'(z0)) MAIN''(Node(z0, z1)) -> c10(WALK#1'(z1)) MAIN''(Node(z0, z1)) -> c10(WALK#1''(z0)) MAIN''(Node(z0, z1)) -> c10(WALK#1''(z1)) K tuples:none Defined Rule Symbols: WALK#1_1, COMP_F_G#1_3, MAIN_1, walk#1_1, comp_f_g#1_3, main_1 Defined Pair Symbols: WALK#1'_1, COMP_F_G#1'_3, WALK#1''_1, COMP_F_G#1''_3, MAIN'_1, MAIN''_1 Compound Symbols: c11_2, c12_2, c13_1, c14_1, c19_1, c20_1, c21_3, c22_1, c23_1, c10_1 ---------------------------------------- (9) CdtLeafRemovalProof (ComplexityIfPolyImplication) Removed 6 leading nodes: MAIN'(Node(z0, z1)) -> c10(WALK#1'(z0)) MAIN'(Node(z0, z1)) -> c10(WALK#1'(z1)) MAIN''(Node(z0, z1)) -> c10(WALK#1'(z0)) MAIN''(Node(z0, z1)) -> c10(WALK#1'(z1)) MAIN''(Node(z0, z1)) -> c10(WALK#1''(z0)) MAIN''(Node(z0, z1)) -> c10(WALK#1''(z1)) ---------------------------------------- (10) Obligation: Complexity Dependency Tuples Problem Rules: walk#1(Leaf(z0)) -> cons_x(z0) walk#1(Node(z0, z1)) -> comp_f_g(walk#1(z0), walk#1(z1)) comp_f_g#1(comp_f_g(z0, z1), comp_f_g(z2, z3), z4) -> comp_f_g#1(z0, z1, comp_f_g#1(z2, z3, z4)) comp_f_g#1(comp_f_g(z0, z1), cons_x(z2), z3) -> comp_f_g#1(z0, z1, Cons(z2, z3)) comp_f_g#1(cons_x(z0), comp_f_g(z1, z2), z3) -> Cons(z0, comp_f_g#1(z1, z2, z3)) comp_f_g#1(cons_x(z0), cons_x(z1), z2) -> Cons(z0, Cons(z1, z2)) main(Leaf(z0)) -> Cons(z0, Nil) main(Node(z0, z1)) -> comp_f_g#1(walk#1(z0), walk#1(z1), Nil) WALK#1(Leaf(z0)) -> c WALK#1(Node(z0, z1)) -> c1(WALK#1(z0)) WALK#1(Node(z0, z1)) -> c2(WALK#1(z1)) COMP_F_G#1(comp_f_g(z0, z1), comp_f_g(z2, z3), z4) -> c3(COMP_F_G#1(z0, z1, comp_f_g#1(z2, z3, z4)), COMP_F_G#1(z2, z3, z4)) COMP_F_G#1(comp_f_g(z0, z1), cons_x(z2), z3) -> c4(COMP_F_G#1(z0, z1, Cons(z2, z3))) COMP_F_G#1(cons_x(z0), comp_f_g(z1, z2), z3) -> c5(COMP_F_G#1(z1, z2, z3)) COMP_F_G#1(cons_x(z0), cons_x(z1), z2) -> c6 MAIN(Leaf(z0)) -> c7 MAIN(Node(z0, z1)) -> c8(COMP_F_G#1(walk#1(z0), walk#1(z1), Nil), WALK#1(z0)) MAIN(Node(z0, z1)) -> c9(COMP_F_G#1(walk#1(z0), walk#1(z1), Nil), WALK#1(z1)) Tuples: WALK#1'(Node(z0, z1)) -> c11(WALK#1'(z0), WALK#1'(z1)) COMP_F_G#1'(comp_f_g(z0, z1), comp_f_g(z2, z3), z4) -> c12(COMP_F_G#1'(z0, z1, comp_f_g#1(z2, z3, z4)), COMP_F_G#1'(z2, z3, z4)) COMP_F_G#1'(comp_f_g(z0, z1), cons_x(z2), z3) -> c13(COMP_F_G#1'(z0, z1, Cons(z2, z3))) COMP_F_G#1'(cons_x(z0), comp_f_g(z1, z2), z3) -> c14(COMP_F_G#1'(z1, z2, z3)) WALK#1''(Node(z0, z1)) -> c19(WALK#1''(z0)) WALK#1''(Node(z0, z1)) -> c20(WALK#1''(z1)) COMP_F_G#1''(comp_f_g(z0, z1), comp_f_g(z2, z3), z4) -> c21(COMP_F_G#1''(z0, z1, comp_f_g#1(z2, z3, z4)), COMP_F_G#1'(z2, z3, z4), COMP_F_G#1''(z2, z3, z4)) COMP_F_G#1''(comp_f_g(z0, z1), cons_x(z2), z3) -> c22(COMP_F_G#1''(z0, z1, Cons(z2, z3))) COMP_F_G#1''(cons_x(z0), comp_f_g(z1, z2), z3) -> c23(COMP_F_G#1''(z1, z2, z3)) MAIN'(Node(z0, z1)) -> c10(COMP_F_G#1'(walk#1(z0), walk#1(z1), Nil)) MAIN''(Node(z0, z1)) -> c10(COMP_F_G#1''(walk#1(z0), walk#1(z1), Nil)) S tuples: WALK#1''(Node(z0, z1)) -> c19(WALK#1''(z0)) WALK#1''(Node(z0, z1)) -> c20(WALK#1''(z1)) COMP_F_G#1''(comp_f_g(z0, z1), comp_f_g(z2, z3), z4) -> c21(COMP_F_G#1''(z0, z1, comp_f_g#1(z2, z3, z4)), COMP_F_G#1'(z2, z3, z4), COMP_F_G#1''(z2, z3, z4)) COMP_F_G#1''(comp_f_g(z0, z1), cons_x(z2), z3) -> c22(COMP_F_G#1''(z0, z1, Cons(z2, z3))) COMP_F_G#1''(cons_x(z0), comp_f_g(z1, z2), z3) -> c23(COMP_F_G#1''(z1, z2, z3)) MAIN''(Node(z0, z1)) -> c10(COMP_F_G#1''(walk#1(z0), walk#1(z1), Nil)) K tuples:none Defined Rule Symbols: WALK#1_1, COMP_F_G#1_3, MAIN_1, walk#1_1, comp_f_g#1_3, main_1 Defined Pair Symbols: WALK#1'_1, COMP_F_G#1'_3, WALK#1''_1, COMP_F_G#1''_3, MAIN'_1, MAIN''_1 Compound Symbols: c11_2, c12_2, c13_1, c14_1, c19_1, c20_1, c21_3, c22_1, c23_1, c10_1 ---------------------------------------- (11) CdtKnowledgeProof (BOTH BOUNDS(ID, ID)) The following tuples could be moved from S to K by knowledge propagation: MAIN''(Node(z0, z1)) -> c10(COMP_F_G#1''(walk#1(z0), walk#1(z1), Nil)) MAIN''(Node(z0, z1)) -> c10(COMP_F_G#1''(walk#1(z0), walk#1(z1), Nil)) ---------------------------------------- (12) Obligation: Complexity Dependency Tuples Problem Rules: walk#1(Leaf(z0)) -> cons_x(z0) walk#1(Node(z0, z1)) -> comp_f_g(walk#1(z0), walk#1(z1)) comp_f_g#1(comp_f_g(z0, z1), comp_f_g(z2, z3), z4) -> comp_f_g#1(z0, z1, comp_f_g#1(z2, z3, z4)) comp_f_g#1(comp_f_g(z0, z1), cons_x(z2), z3) -> comp_f_g#1(z0, z1, Cons(z2, z3)) comp_f_g#1(cons_x(z0), comp_f_g(z1, z2), z3) -> Cons(z0, comp_f_g#1(z1, z2, z3)) comp_f_g#1(cons_x(z0), cons_x(z1), z2) -> Cons(z0, Cons(z1, z2)) main(Leaf(z0)) -> Cons(z0, Nil) main(Node(z0, z1)) -> comp_f_g#1(walk#1(z0), walk#1(z1), Nil) WALK#1(Leaf(z0)) -> c WALK#1(Node(z0, z1)) -> c1(WALK#1(z0)) WALK#1(Node(z0, z1)) -> c2(WALK#1(z1)) COMP_F_G#1(comp_f_g(z0, z1), comp_f_g(z2, z3), z4) -> c3(COMP_F_G#1(z0, z1, comp_f_g#1(z2, z3, z4)), COMP_F_G#1(z2, z3, z4)) COMP_F_G#1(comp_f_g(z0, z1), cons_x(z2), z3) -> c4(COMP_F_G#1(z0, z1, Cons(z2, z3))) COMP_F_G#1(cons_x(z0), comp_f_g(z1, z2), z3) -> c5(COMP_F_G#1(z1, z2, z3)) COMP_F_G#1(cons_x(z0), cons_x(z1), z2) -> c6 MAIN(Leaf(z0)) -> c7 MAIN(Node(z0, z1)) -> c8(COMP_F_G#1(walk#1(z0), walk#1(z1), Nil), WALK#1(z0)) MAIN(Node(z0, z1)) -> c9(COMP_F_G#1(walk#1(z0), walk#1(z1), Nil), WALK#1(z1)) Tuples: WALK#1'(Node(z0, z1)) -> c11(WALK#1'(z0), WALK#1'(z1)) COMP_F_G#1'(comp_f_g(z0, z1), comp_f_g(z2, z3), z4) -> c12(COMP_F_G#1'(z0, z1, comp_f_g#1(z2, z3, z4)), COMP_F_G#1'(z2, z3, z4)) COMP_F_G#1'(comp_f_g(z0, z1), cons_x(z2), z3) -> c13(COMP_F_G#1'(z0, z1, Cons(z2, z3))) COMP_F_G#1'(cons_x(z0), comp_f_g(z1, z2), z3) -> c14(COMP_F_G#1'(z1, z2, z3)) WALK#1''(Node(z0, z1)) -> c19(WALK#1''(z0)) WALK#1''(Node(z0, z1)) -> c20(WALK#1''(z1)) COMP_F_G#1''(comp_f_g(z0, z1), comp_f_g(z2, z3), z4) -> c21(COMP_F_G#1''(z0, z1, comp_f_g#1(z2, z3, z4)), COMP_F_G#1'(z2, z3, z4), COMP_F_G#1''(z2, z3, z4)) COMP_F_G#1''(comp_f_g(z0, z1), cons_x(z2), z3) -> c22(COMP_F_G#1''(z0, z1, Cons(z2, z3))) COMP_F_G#1''(cons_x(z0), comp_f_g(z1, z2), z3) -> c23(COMP_F_G#1''(z1, z2, z3)) MAIN'(Node(z0, z1)) -> c10(COMP_F_G#1'(walk#1(z0), walk#1(z1), Nil)) MAIN''(Node(z0, z1)) -> c10(COMP_F_G#1''(walk#1(z0), walk#1(z1), Nil)) S tuples: WALK#1''(Node(z0, z1)) -> c19(WALK#1''(z0)) WALK#1''(Node(z0, z1)) -> c20(WALK#1''(z1)) COMP_F_G#1''(comp_f_g(z0, z1), comp_f_g(z2, z3), z4) -> c21(COMP_F_G#1''(z0, z1, comp_f_g#1(z2, z3, z4)), COMP_F_G#1'(z2, z3, z4), COMP_F_G#1''(z2, z3, z4)) COMP_F_G#1''(comp_f_g(z0, z1), cons_x(z2), z3) -> c22(COMP_F_G#1''(z0, z1, Cons(z2, z3))) COMP_F_G#1''(cons_x(z0), comp_f_g(z1, z2), z3) -> c23(COMP_F_G#1''(z1, z2, z3)) K tuples: MAIN''(Node(z0, z1)) -> c10(COMP_F_G#1''(walk#1(z0), walk#1(z1), Nil)) Defined Rule Symbols: WALK#1_1, COMP_F_G#1_3, MAIN_1, walk#1_1, comp_f_g#1_3, main_1 Defined Pair Symbols: WALK#1'_1, COMP_F_G#1'_3, WALK#1''_1, COMP_F_G#1''_3, MAIN'_1, MAIN''_1 Compound Symbols: c11_2, c12_2, c13_1, c14_1, c19_1, c20_1, c21_3, c22_1, c23_1, c10_1 ---------------------------------------- (13) CdtUsableRulesProof (BOTH BOUNDS(ID, ID)) The following rules are not usable and were removed: main(Leaf(z0)) -> Cons(z0, Nil) main(Node(z0, z1)) -> comp_f_g#1(walk#1(z0), walk#1(z1), Nil) WALK#1(Leaf(z0)) -> c WALK#1(Node(z0, z1)) -> c1(WALK#1(z0)) WALK#1(Node(z0, z1)) -> c2(WALK#1(z1)) COMP_F_G#1(comp_f_g(z0, z1), comp_f_g(z2, z3), z4) -> c3(COMP_F_G#1(z0, z1, comp_f_g#1(z2, z3, z4)), COMP_F_G#1(z2, z3, z4)) COMP_F_G#1(comp_f_g(z0, z1), cons_x(z2), z3) -> c4(COMP_F_G#1(z0, z1, Cons(z2, z3))) COMP_F_G#1(cons_x(z0), comp_f_g(z1, z2), z3) -> c5(COMP_F_G#1(z1, z2, z3)) COMP_F_G#1(cons_x(z0), cons_x(z1), z2) -> c6 MAIN(Leaf(z0)) -> c7 MAIN(Node(z0, z1)) -> c8(COMP_F_G#1(walk#1(z0), walk#1(z1), Nil), WALK#1(z0)) MAIN(Node(z0, z1)) -> c9(COMP_F_G#1(walk#1(z0), walk#1(z1), Nil), WALK#1(z1)) ---------------------------------------- (14) Obligation: Complexity Dependency Tuples Problem Rules: comp_f_g#1(comp_f_g(z0, z1), comp_f_g(z2, z3), z4) -> comp_f_g#1(z0, z1, comp_f_g#1(z2, z3, z4)) comp_f_g#1(comp_f_g(z0, z1), cons_x(z2), z3) -> comp_f_g#1(z0, z1, Cons(z2, z3)) comp_f_g#1(cons_x(z0), comp_f_g(z1, z2), z3) -> Cons(z0, comp_f_g#1(z1, z2, z3)) comp_f_g#1(cons_x(z0), cons_x(z1), z2) -> Cons(z0, Cons(z1, z2)) walk#1(Leaf(z0)) -> cons_x(z0) walk#1(Node(z0, z1)) -> comp_f_g(walk#1(z0), walk#1(z1)) Tuples: WALK#1'(Node(z0, z1)) -> c11(WALK#1'(z0), WALK#1'(z1)) COMP_F_G#1'(comp_f_g(z0, z1), comp_f_g(z2, z3), z4) -> c12(COMP_F_G#1'(z0, z1, comp_f_g#1(z2, z3, z4)), COMP_F_G#1'(z2, z3, z4)) COMP_F_G#1'(comp_f_g(z0, z1), cons_x(z2), z3) -> c13(COMP_F_G#1'(z0, z1, Cons(z2, z3))) COMP_F_G#1'(cons_x(z0), comp_f_g(z1, z2), z3) -> c14(COMP_F_G#1'(z1, z2, z3)) WALK#1''(Node(z0, z1)) -> c19(WALK#1''(z0)) WALK#1''(Node(z0, z1)) -> c20(WALK#1''(z1)) COMP_F_G#1''(comp_f_g(z0, z1), comp_f_g(z2, z3), z4) -> c21(COMP_F_G#1''(z0, z1, comp_f_g#1(z2, z3, z4)), COMP_F_G#1'(z2, z3, z4), COMP_F_G#1''(z2, z3, z4)) COMP_F_G#1''(comp_f_g(z0, z1), cons_x(z2), z3) -> c22(COMP_F_G#1''(z0, z1, Cons(z2, z3))) COMP_F_G#1''(cons_x(z0), comp_f_g(z1, z2), z3) -> c23(COMP_F_G#1''(z1, z2, z3)) MAIN'(Node(z0, z1)) -> c10(COMP_F_G#1'(walk#1(z0), walk#1(z1), Nil)) MAIN''(Node(z0, z1)) -> c10(COMP_F_G#1''(walk#1(z0), walk#1(z1), Nil)) S tuples: WALK#1''(Node(z0, z1)) -> c19(WALK#1''(z0)) WALK#1''(Node(z0, z1)) -> c20(WALK#1''(z1)) COMP_F_G#1''(comp_f_g(z0, z1), comp_f_g(z2, z3), z4) -> c21(COMP_F_G#1''(z0, z1, comp_f_g#1(z2, z3, z4)), COMP_F_G#1'(z2, z3, z4), COMP_F_G#1''(z2, z3, z4)) COMP_F_G#1''(comp_f_g(z0, z1), cons_x(z2), z3) -> c22(COMP_F_G#1''(z0, z1, Cons(z2, z3))) COMP_F_G#1''(cons_x(z0), comp_f_g(z1, z2), z3) -> c23(COMP_F_G#1''(z1, z2, z3)) K tuples: MAIN''(Node(z0, z1)) -> c10(COMP_F_G#1''(walk#1(z0), walk#1(z1), Nil)) Defined Rule Symbols: comp_f_g#1_3, walk#1_1 Defined Pair Symbols: WALK#1'_1, COMP_F_G#1'_3, WALK#1''_1, COMP_F_G#1''_3, MAIN'_1, MAIN''_1 Compound Symbols: c11_2, c12_2, c13_1, c14_1, c19_1, c20_1, c21_3, c22_1, c23_1, c10_1 ---------------------------------------- (15) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1))) Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S. WALK#1''(Node(z0, z1)) -> c19(WALK#1''(z0)) WALK#1''(Node(z0, z1)) -> c20(WALK#1''(z1)) COMP_F_G#1''(comp_f_g(z0, z1), cons_x(z2), z3) -> c22(COMP_F_G#1''(z0, z1, Cons(z2, z3))) COMP_F_G#1''(cons_x(z0), comp_f_g(z1, z2), z3) -> c23(COMP_F_G#1''(z1, z2, z3)) We considered the (Usable) Rules: comp_f_g#1(cons_x(z0), cons_x(z1), z2) -> Cons(z0, Cons(z1, z2)) walk#1(Node(z0, z1)) -> comp_f_g(walk#1(z0), walk#1(z1)) comp_f_g#1(comp_f_g(z0, z1), comp_f_g(z2, z3), z4) -> comp_f_g#1(z0, z1, comp_f_g#1(z2, z3, z4)) walk#1(Leaf(z0)) -> cons_x(z0) comp_f_g#1(cons_x(z0), comp_f_g(z1, z2), z3) -> Cons(z0, comp_f_g#1(z1, z2, z3)) comp_f_g#1(comp_f_g(z0, z1), cons_x(z2), z3) -> comp_f_g#1(z0, z1, Cons(z2, z3)) And the Tuples: WALK#1'(Node(z0, z1)) -> c11(WALK#1'(z0), WALK#1'(z1)) COMP_F_G#1'(comp_f_g(z0, z1), comp_f_g(z2, z3), z4) -> c12(COMP_F_G#1'(z0, z1, comp_f_g#1(z2, z3, z4)), COMP_F_G#1'(z2, z3, z4)) COMP_F_G#1'(comp_f_g(z0, z1), cons_x(z2), z3) -> c13(COMP_F_G#1'(z0, z1, Cons(z2, z3))) COMP_F_G#1'(cons_x(z0), comp_f_g(z1, z2), z3) -> c14(COMP_F_G#1'(z1, z2, z3)) WALK#1''(Node(z0, z1)) -> c19(WALK#1''(z0)) WALK#1''(Node(z0, z1)) -> c20(WALK#1''(z1)) COMP_F_G#1''(comp_f_g(z0, z1), comp_f_g(z2, z3), z4) -> c21(COMP_F_G#1''(z0, z1, comp_f_g#1(z2, z3, z4)), COMP_F_G#1'(z2, z3, z4), COMP_F_G#1''(z2, z3, z4)) COMP_F_G#1''(comp_f_g(z0, z1), cons_x(z2), z3) -> c22(COMP_F_G#1''(z0, z1, Cons(z2, z3))) COMP_F_G#1''(cons_x(z0), comp_f_g(z1, z2), z3) -> c23(COMP_F_G#1''(z1, z2, z3)) MAIN'(Node(z0, z1)) -> c10(COMP_F_G#1'(walk#1(z0), walk#1(z1), Nil)) MAIN''(Node(z0, z1)) -> c10(COMP_F_G#1''(walk#1(z0), walk#1(z1), Nil)) The order we found is given by the following interpretation: Polynomial interpretation : POL(COMP_F_G#1'(x_1, x_2, x_3)) = 0 POL(COMP_F_G#1''(x_1, x_2, x_3)) = x_1 + x_2 + x_3 POL(Cons(x_1, x_2)) = 0 POL(Leaf(x_1)) = [1] + x_1 POL(MAIN'(x_1)) = x_1 POL(MAIN''(x_1)) = [1] + x_1 POL(Nil) = 0 POL(Node(x_1, x_2)) = [1] + x_1 + x_2 POL(WALK#1'(x_1)) = [1] + x_1 POL(WALK#1''(x_1)) = x_1 POL(c10(x_1)) = x_1 POL(c11(x_1, x_2)) = x_1 + x_2 POL(c12(x_1, x_2)) = x_1 + x_2 POL(c13(x_1)) = x_1 POL(c14(x_1)) = x_1 POL(c19(x_1)) = x_1 POL(c20(x_1)) = x_1 POL(c21(x_1, x_2, x_3)) = x_1 + x_2 + x_3 POL(c22(x_1)) = x_1 POL(c23(x_1)) = x_1 POL(comp_f_g(x_1, x_2)) = x_1 + x_2 POL(comp_f_g#1(x_1, x_2, x_3)) = 0 POL(cons_x(x_1)) = [1] + x_1 POL(walk#1(x_1)) = [1] + x_1 ---------------------------------------- (16) Obligation: Complexity Dependency Tuples Problem Rules: comp_f_g#1(comp_f_g(z0, z1), comp_f_g(z2, z3), z4) -> comp_f_g#1(z0, z1, comp_f_g#1(z2, z3, z4)) comp_f_g#1(comp_f_g(z0, z1), cons_x(z2), z3) -> comp_f_g#1(z0, z1, Cons(z2, z3)) comp_f_g#1(cons_x(z0), comp_f_g(z1, z2), z3) -> Cons(z0, comp_f_g#1(z1, z2, z3)) comp_f_g#1(cons_x(z0), cons_x(z1), z2) -> Cons(z0, Cons(z1, z2)) walk#1(Leaf(z0)) -> cons_x(z0) walk#1(Node(z0, z1)) -> comp_f_g(walk#1(z0), walk#1(z1)) Tuples: WALK#1'(Node(z0, z1)) -> c11(WALK#1'(z0), WALK#1'(z1)) COMP_F_G#1'(comp_f_g(z0, z1), comp_f_g(z2, z3), z4) -> c12(COMP_F_G#1'(z0, z1, comp_f_g#1(z2, z3, z4)), COMP_F_G#1'(z2, z3, z4)) COMP_F_G#1'(comp_f_g(z0, z1), cons_x(z2), z3) -> c13(COMP_F_G#1'(z0, z1, Cons(z2, z3))) COMP_F_G#1'(cons_x(z0), comp_f_g(z1, z2), z3) -> c14(COMP_F_G#1'(z1, z2, z3)) WALK#1''(Node(z0, z1)) -> c19(WALK#1''(z0)) WALK#1''(Node(z0, z1)) -> c20(WALK#1''(z1)) COMP_F_G#1''(comp_f_g(z0, z1), comp_f_g(z2, z3), z4) -> c21(COMP_F_G#1''(z0, z1, comp_f_g#1(z2, z3, z4)), COMP_F_G#1'(z2, z3, z4), COMP_F_G#1''(z2, z3, z4)) COMP_F_G#1''(comp_f_g(z0, z1), cons_x(z2), z3) -> c22(COMP_F_G#1''(z0, z1, Cons(z2, z3))) COMP_F_G#1''(cons_x(z0), comp_f_g(z1, z2), z3) -> c23(COMP_F_G#1''(z1, z2, z3)) MAIN'(Node(z0, z1)) -> c10(COMP_F_G#1'(walk#1(z0), walk#1(z1), Nil)) MAIN''(Node(z0, z1)) -> c10(COMP_F_G#1''(walk#1(z0), walk#1(z1), Nil)) S tuples: COMP_F_G#1''(comp_f_g(z0, z1), comp_f_g(z2, z3), z4) -> c21(COMP_F_G#1''(z0, z1, comp_f_g#1(z2, z3, z4)), COMP_F_G#1'(z2, z3, z4), COMP_F_G#1''(z2, z3, z4)) K tuples: MAIN''(Node(z0, z1)) -> c10(COMP_F_G#1''(walk#1(z0), walk#1(z1), Nil)) WALK#1''(Node(z0, z1)) -> c19(WALK#1''(z0)) WALK#1''(Node(z0, z1)) -> c20(WALK#1''(z1)) COMP_F_G#1''(comp_f_g(z0, z1), cons_x(z2), z3) -> c22(COMP_F_G#1''(z0, z1, Cons(z2, z3))) COMP_F_G#1''(cons_x(z0), comp_f_g(z1, z2), z3) -> c23(COMP_F_G#1''(z1, z2, z3)) Defined Rule Symbols: comp_f_g#1_3, walk#1_1 Defined Pair Symbols: WALK#1'_1, COMP_F_G#1'_3, WALK#1''_1, COMP_F_G#1''_3, MAIN'_1, MAIN''_1 Compound Symbols: c11_2, c12_2, c13_1, c14_1, c19_1, c20_1, c21_3, c22_1, c23_1, c10_1 ---------------------------------------- (17) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1))) Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S. COMP_F_G#1''(comp_f_g(z0, z1), comp_f_g(z2, z3), z4) -> c21(COMP_F_G#1''(z0, z1, comp_f_g#1(z2, z3, z4)), COMP_F_G#1'(z2, z3, z4), COMP_F_G#1''(z2, z3, z4)) We considered the (Usable) Rules: walk#1(Node(z0, z1)) -> comp_f_g(walk#1(z0), walk#1(z1)) walk#1(Leaf(z0)) -> cons_x(z0) And the Tuples: WALK#1'(Node(z0, z1)) -> c11(WALK#1'(z0), WALK#1'(z1)) COMP_F_G#1'(comp_f_g(z0, z1), comp_f_g(z2, z3), z4) -> c12(COMP_F_G#1'(z0, z1, comp_f_g#1(z2, z3, z4)), COMP_F_G#1'(z2, z3, z4)) COMP_F_G#1'(comp_f_g(z0, z1), cons_x(z2), z3) -> c13(COMP_F_G#1'(z0, z1, Cons(z2, z3))) COMP_F_G#1'(cons_x(z0), comp_f_g(z1, z2), z3) -> c14(COMP_F_G#1'(z1, z2, z3)) WALK#1''(Node(z0, z1)) -> c19(WALK#1''(z0)) WALK#1''(Node(z0, z1)) -> c20(WALK#1''(z1)) COMP_F_G#1''(comp_f_g(z0, z1), comp_f_g(z2, z3), z4) -> c21(COMP_F_G#1''(z0, z1, comp_f_g#1(z2, z3, z4)), COMP_F_G#1'(z2, z3, z4), COMP_F_G#1''(z2, z3, z4)) COMP_F_G#1''(comp_f_g(z0, z1), cons_x(z2), z3) -> c22(COMP_F_G#1''(z0, z1, Cons(z2, z3))) COMP_F_G#1''(cons_x(z0), comp_f_g(z1, z2), z3) -> c23(COMP_F_G#1''(z1, z2, z3)) MAIN'(Node(z0, z1)) -> c10(COMP_F_G#1'(walk#1(z0), walk#1(z1), Nil)) MAIN''(Node(z0, z1)) -> c10(COMP_F_G#1''(walk#1(z0), walk#1(z1), Nil)) The order we found is given by the following interpretation: Polynomial interpretation : POL(COMP_F_G#1'(x_1, x_2, x_3)) = 0 POL(COMP_F_G#1''(x_1, x_2, x_3)) = [1] + x_1 + x_2 POL(Cons(x_1, x_2)) = [1] + x_1 + x_2 POL(Leaf(x_1)) = [1] + x_1 POL(MAIN'(x_1)) = [1] + x_1 POL(MAIN''(x_1)) = x_1 POL(Nil) = [1] POL(Node(x_1, x_2)) = [1] + x_1 + x_2 POL(WALK#1'(x_1)) = [1] + x_1 POL(WALK#1''(x_1)) = x_1 POL(c10(x_1)) = x_1 POL(c11(x_1, x_2)) = x_1 + x_2 POL(c12(x_1, x_2)) = x_1 + x_2 POL(c13(x_1)) = x_1 POL(c14(x_1)) = x_1 POL(c19(x_1)) = x_1 POL(c20(x_1)) = x_1 POL(c21(x_1, x_2, x_3)) = x_1 + x_2 + x_3 POL(c22(x_1)) = x_1 POL(c23(x_1)) = x_1 POL(comp_f_g(x_1, x_2)) = [1] + x_1 + x_2 POL(comp_f_g#1(x_1, x_2, x_3)) = [1] + x_1 + x_2 + x_3 POL(cons_x(x_1)) = [1] + x_1 POL(walk#1(x_1)) = x_1 ---------------------------------------- (18) Obligation: Complexity Dependency Tuples Problem Rules: comp_f_g#1(comp_f_g(z0, z1), comp_f_g(z2, z3), z4) -> comp_f_g#1(z0, z1, comp_f_g#1(z2, z3, z4)) comp_f_g#1(comp_f_g(z0, z1), cons_x(z2), z3) -> comp_f_g#1(z0, z1, Cons(z2, z3)) comp_f_g#1(cons_x(z0), comp_f_g(z1, z2), z3) -> Cons(z0, comp_f_g#1(z1, z2, z3)) comp_f_g#1(cons_x(z0), cons_x(z1), z2) -> Cons(z0, Cons(z1, z2)) walk#1(Leaf(z0)) -> cons_x(z0) walk#1(Node(z0, z1)) -> comp_f_g(walk#1(z0), walk#1(z1)) Tuples: WALK#1'(Node(z0, z1)) -> c11(WALK#1'(z0), WALK#1'(z1)) COMP_F_G#1'(comp_f_g(z0, z1), comp_f_g(z2, z3), z4) -> c12(COMP_F_G#1'(z0, z1, comp_f_g#1(z2, z3, z4)), COMP_F_G#1'(z2, z3, z4)) COMP_F_G#1'(comp_f_g(z0, z1), cons_x(z2), z3) -> c13(COMP_F_G#1'(z0, z1, Cons(z2, z3))) COMP_F_G#1'(cons_x(z0), comp_f_g(z1, z2), z3) -> c14(COMP_F_G#1'(z1, z2, z3)) WALK#1''(Node(z0, z1)) -> c19(WALK#1''(z0)) WALK#1''(Node(z0, z1)) -> c20(WALK#1''(z1)) COMP_F_G#1''(comp_f_g(z0, z1), comp_f_g(z2, z3), z4) -> c21(COMP_F_G#1''(z0, z1, comp_f_g#1(z2, z3, z4)), COMP_F_G#1'(z2, z3, z4), COMP_F_G#1''(z2, z3, z4)) COMP_F_G#1''(comp_f_g(z0, z1), cons_x(z2), z3) -> c22(COMP_F_G#1''(z0, z1, Cons(z2, z3))) COMP_F_G#1''(cons_x(z0), comp_f_g(z1, z2), z3) -> c23(COMP_F_G#1''(z1, z2, z3)) MAIN'(Node(z0, z1)) -> c10(COMP_F_G#1'(walk#1(z0), walk#1(z1), Nil)) MAIN''(Node(z0, z1)) -> c10(COMP_F_G#1''(walk#1(z0), walk#1(z1), Nil)) S tuples:none K tuples: MAIN''(Node(z0, z1)) -> c10(COMP_F_G#1''(walk#1(z0), walk#1(z1), Nil)) WALK#1''(Node(z0, z1)) -> c19(WALK#1''(z0)) WALK#1''(Node(z0, z1)) -> c20(WALK#1''(z1)) COMP_F_G#1''(comp_f_g(z0, z1), cons_x(z2), z3) -> c22(COMP_F_G#1''(z0, z1, Cons(z2, z3))) COMP_F_G#1''(cons_x(z0), comp_f_g(z1, z2), z3) -> c23(COMP_F_G#1''(z1, z2, z3)) COMP_F_G#1''(comp_f_g(z0, z1), comp_f_g(z2, z3), z4) -> c21(COMP_F_G#1''(z0, z1, comp_f_g#1(z2, z3, z4)), COMP_F_G#1'(z2, z3, z4), COMP_F_G#1''(z2, z3, z4)) Defined Rule Symbols: comp_f_g#1_3, walk#1_1 Defined Pair Symbols: WALK#1'_1, COMP_F_G#1'_3, WALK#1''_1, COMP_F_G#1''_3, MAIN'_1, MAIN''_1 Compound Symbols: c11_2, c12_2, c13_1, c14_1, c19_1, c20_1, c21_3, c22_1, c23_1, c10_1 ---------------------------------------- (19) SIsEmptyProof (BOTH BOUNDS(ID, ID)) The set S is empty ---------------------------------------- (20) BOUNDS(1, 1) ---------------------------------------- (21) RelTrsToDecreasingLoopProblemProof (LOWER BOUND(ID)) Transformed a relative TRS into a decreasing-loop problem. ---------------------------------------- (22) Obligation: Analyzing the following TRS for decreasing loops: The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, n^1). The TRS R consists of the following rules: WALK#1(Leaf(z0)) -> c WALK#1(Node(z0, z1)) -> c1(WALK#1(z0)) WALK#1(Node(z0, z1)) -> c2(WALK#1(z1)) COMP_F_G#1(comp_f_g(z0, z1), comp_f_g(z2, z3), z4) -> c3(COMP_F_G#1(z0, z1, comp_f_g#1(z2, z3, z4)), COMP_F_G#1(z2, z3, z4)) COMP_F_G#1(comp_f_g(z0, z1), cons_x(z2), z3) -> c4(COMP_F_G#1(z0, z1, Cons(z2, z3))) COMP_F_G#1(cons_x(z0), comp_f_g(z1, z2), z3) -> c5(COMP_F_G#1(z1, z2, z3)) COMP_F_G#1(cons_x(z0), cons_x(z1), z2) -> c6 MAIN(Leaf(z0)) -> c7 MAIN(Node(z0, z1)) -> c8(COMP_F_G#1(walk#1(z0), walk#1(z1), Nil), WALK#1(z0)) MAIN(Node(z0, z1)) -> c9(COMP_F_G#1(walk#1(z0), walk#1(z1), Nil), WALK#1(z1)) The (relative) TRS S consists of the following rules: walk#1(Leaf(z0)) -> cons_x(z0) walk#1(Node(z0, z1)) -> comp_f_g(walk#1(z0), walk#1(z1)) comp_f_g#1(comp_f_g(z0, z1), comp_f_g(z2, z3), z4) -> comp_f_g#1(z0, z1, comp_f_g#1(z2, z3, z4)) comp_f_g#1(comp_f_g(z0, z1), cons_x(z2), z3) -> comp_f_g#1(z0, z1, Cons(z2, z3)) comp_f_g#1(cons_x(z0), comp_f_g(z1, z2), z3) -> Cons(z0, comp_f_g#1(z1, z2, z3)) comp_f_g#1(cons_x(z0), cons_x(z1), z2) -> Cons(z0, Cons(z1, z2)) main(Leaf(z0)) -> Cons(z0, Nil) main(Node(z0, z1)) -> comp_f_g#1(walk#1(z0), walk#1(z1), Nil) Rewrite Strategy: INNERMOST ---------------------------------------- (23) DecreasingLoopProof (LOWER BOUND(ID)) The following loop(s) give(s) rise to the lower bound Omega(n^1): The rewrite sequence WALK#1(Node(z0, z1)) ->^+ c2(WALK#1(z1)) gives rise to a decreasing loop by considering the right hand sides subterm at position [0]. The pumping substitution is [z1 / Node(z0, z1)]. The result substitution is [ ]. ---------------------------------------- (24) Complex Obligation (BEST) ---------------------------------------- (25) Obligation: Proved the lower bound n^1 for the following obligation: The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, n^1). The TRS R consists of the following rules: WALK#1(Leaf(z0)) -> c WALK#1(Node(z0, z1)) -> c1(WALK#1(z0)) WALK#1(Node(z0, z1)) -> c2(WALK#1(z1)) COMP_F_G#1(comp_f_g(z0, z1), comp_f_g(z2, z3), z4) -> c3(COMP_F_G#1(z0, z1, comp_f_g#1(z2, z3, z4)), COMP_F_G#1(z2, z3, z4)) COMP_F_G#1(comp_f_g(z0, z1), cons_x(z2), z3) -> c4(COMP_F_G#1(z0, z1, Cons(z2, z3))) COMP_F_G#1(cons_x(z0), comp_f_g(z1, z2), z3) -> c5(COMP_F_G#1(z1, z2, z3)) COMP_F_G#1(cons_x(z0), cons_x(z1), z2) -> c6 MAIN(Leaf(z0)) -> c7 MAIN(Node(z0, z1)) -> c8(COMP_F_G#1(walk#1(z0), walk#1(z1), Nil), WALK#1(z0)) MAIN(Node(z0, z1)) -> c9(COMP_F_G#1(walk#1(z0), walk#1(z1), Nil), WALK#1(z1)) The (relative) TRS S consists of the following rules: walk#1(Leaf(z0)) -> cons_x(z0) walk#1(Node(z0, z1)) -> comp_f_g(walk#1(z0), walk#1(z1)) comp_f_g#1(comp_f_g(z0, z1), comp_f_g(z2, z3), z4) -> comp_f_g#1(z0, z1, comp_f_g#1(z2, z3, z4)) comp_f_g#1(comp_f_g(z0, z1), cons_x(z2), z3) -> comp_f_g#1(z0, z1, Cons(z2, z3)) comp_f_g#1(cons_x(z0), comp_f_g(z1, z2), z3) -> Cons(z0, comp_f_g#1(z1, z2, z3)) comp_f_g#1(cons_x(z0), cons_x(z1), z2) -> Cons(z0, Cons(z1, z2)) main(Leaf(z0)) -> Cons(z0, Nil) main(Node(z0, z1)) -> comp_f_g#1(walk#1(z0), walk#1(z1), Nil) Rewrite Strategy: INNERMOST ---------------------------------------- (26) LowerBoundPropagationProof (FINISHED) Propagated lower bound. ---------------------------------------- (27) BOUNDS(n^1, INF) ---------------------------------------- (28) Obligation: Analyzing the following TRS for decreasing loops: The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, n^1). The TRS R consists of the following rules: WALK#1(Leaf(z0)) -> c WALK#1(Node(z0, z1)) -> c1(WALK#1(z0)) WALK#1(Node(z0, z1)) -> c2(WALK#1(z1)) COMP_F_G#1(comp_f_g(z0, z1), comp_f_g(z2, z3), z4) -> c3(COMP_F_G#1(z0, z1, comp_f_g#1(z2, z3, z4)), COMP_F_G#1(z2, z3, z4)) COMP_F_G#1(comp_f_g(z0, z1), cons_x(z2), z3) -> c4(COMP_F_G#1(z0, z1, Cons(z2, z3))) COMP_F_G#1(cons_x(z0), comp_f_g(z1, z2), z3) -> c5(COMP_F_G#1(z1, z2, z3)) COMP_F_G#1(cons_x(z0), cons_x(z1), z2) -> c6 MAIN(Leaf(z0)) -> c7 MAIN(Node(z0, z1)) -> c8(COMP_F_G#1(walk#1(z0), walk#1(z1), Nil), WALK#1(z0)) MAIN(Node(z0, z1)) -> c9(COMP_F_G#1(walk#1(z0), walk#1(z1), Nil), WALK#1(z1)) The (relative) TRS S consists of the following rules: walk#1(Leaf(z0)) -> cons_x(z0) walk#1(Node(z0, z1)) -> comp_f_g(walk#1(z0), walk#1(z1)) comp_f_g#1(comp_f_g(z0, z1), comp_f_g(z2, z3), z4) -> comp_f_g#1(z0, z1, comp_f_g#1(z2, z3, z4)) comp_f_g#1(comp_f_g(z0, z1), cons_x(z2), z3) -> comp_f_g#1(z0, z1, Cons(z2, z3)) comp_f_g#1(cons_x(z0), comp_f_g(z1, z2), z3) -> Cons(z0, comp_f_g#1(z1, z2, z3)) comp_f_g#1(cons_x(z0), cons_x(z1), z2) -> Cons(z0, Cons(z1, z2)) main(Leaf(z0)) -> Cons(z0, Nil) main(Node(z0, z1)) -> comp_f_g#1(walk#1(z0), walk#1(z1), Nil) Rewrite Strategy: INNERMOST