KILLED proof of input_zOz2LjEEad.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) CompletionProof [UPPER BOUND(ID), 0 ms] (18) CpxTypedWeightedCompleteTrs (19) CpxTypedWeightedTrsToRntsProof [UPPER BOUND(ID), 0 ms] (20) CpxRNTS (21) CpxTrsToCdtProof [UPPER BOUND(ID), 0 ms] (22) CdtProblem (23) CdtLeafRemovalProof [ComplexityIfPolyImplication, 0 ms] (24) CdtProblem (25) CdtUsableRulesProof [BOTH BOUNDS(ID, ID), 0 ms] (26) CdtProblem (27) CdtNarrowingProof [BOTH BOUNDS(ID, ID), 0 ms] (28) CdtProblem (29) CdtRhsSimplificationProcessorProof [BOTH BOUNDS(ID, ID), 0 ms] (30) CdtProblem (31) CdtNarrowingProof [BOTH BOUNDS(ID, ID), 0 ms] (32) CdtProblem (33) CdtForwardInstantiationProof [BOTH BOUNDS(ID, ID), 0 ms] (34) CdtProblem (35) CdtRuleRemovalProof [UPPER BOUND(ADD(n^2)), 781 ms] (36) CdtProblem (37) CdtRuleRemovalProof [UPPER BOUND(ADD(n^2)), 1164 ms] (38) 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: badd(x', Cons(x, xs)) -> badd(Cons(Nil, Nil), badd(x', xs)) badd(x, Nil) -> x goal(x, y) -> badd(x, y) 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: badd(x', Cons(x, xs)) -> badd(Cons(Nil, Nil), badd(x', xs)) badd(x, Nil) -> x goal(x, y) -> badd(x, y) 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: badd(x', Cons(x, xs)) -> badd(Cons(Nil, Nil), badd(x', xs)) badd(x, Nil) -> x goal(x, y) -> badd(x, y) 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: badd(x', Cons(x, xs)) -> badd(Cons(Nil, Nil), badd(x', xs)) [1] badd(x, Nil) -> x [1] goal(x, y) -> badd(x, y) [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: badd(x', Cons(x, xs)) -> badd(Cons(Nil, Nil), badd(x', xs)) [1] badd(x, Nil) -> x [1] goal(x, y) -> badd(x, y) [1] The TRS has the following type information: badd :: Cons:Nil -> Cons:Nil -> Cons:Nil Cons :: Cons:Nil -> Cons:Nil -> Cons:Nil Nil :: Cons:Nil goal :: Cons:Nil -> Cons:Nil -> Cons:Nil 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: goal_2 (c) The following functions are completely defined: badd_2 Due to the following rules being added: none And the following fresh constants: none ---------------------------------------- (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: badd(x', Cons(x, xs)) -> badd(Cons(Nil, Nil), badd(x', xs)) [1] badd(x, Nil) -> x [1] goal(x, y) -> badd(x, y) [1] The TRS has the following type information: badd :: Cons:Nil -> Cons:Nil -> Cons:Nil Cons :: Cons:Nil -> Cons:Nil -> Cons:Nil Nil :: Cons:Nil goal :: Cons:Nil -> Cons:Nil -> Cons:Nil 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: badd(x', Cons(x, Cons(x1, xs'))) -> badd(Cons(Nil, Nil), badd(Cons(Nil, Nil), badd(x', xs'))) [2] badd(x', Cons(x, Nil)) -> badd(Cons(Nil, Nil), x') [2] badd(x, Nil) -> x [1] goal(x, y) -> badd(x, y) [1] The TRS has the following type information: badd :: Cons:Nil -> Cons:Nil -> Cons:Nil Cons :: Cons:Nil -> Cons:Nil -> Cons:Nil Nil :: Cons:Nil goal :: Cons:Nil -> Cons:Nil -> Cons:Nil 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: Nil => 0 ---------------------------------------- (14) Obligation: Complexity RNTS consisting of the following rules: badd(z, z') -{ 1 }-> x :|: x >= 0, z = x, z' = 0 badd(z, z') -{ 2 }-> badd(1 + 0 + 0, x') :|: x' >= 0, x >= 0, z' = 1 + x + 0, z = x' badd(z, z') -{ 2 }-> badd(1 + 0 + 0, badd(1 + 0 + 0, badd(x', xs'))) :|: x1 >= 0, x' >= 0, x >= 0, xs' >= 0, z = x', z' = 1 + x + (1 + x1 + xs') goal(z, z') -{ 1 }-> badd(x, y) :|: x >= 0, y >= 0, z = x, z' = y ---------------------------------------- (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: badd(z, z') -{ 1 }-> z :|: z >= 0, z' = 0 badd(z, z') -{ 2 }-> badd(1 + 0 + 0, z) :|: z >= 0, z' - 1 >= 0 badd(z, z') -{ 2 }-> badd(1 + 0 + 0, badd(1 + 0 + 0, badd(z, xs'))) :|: x1 >= 0, z >= 0, x >= 0, xs' >= 0, z' = 1 + x + (1 + x1 + xs') goal(z, z') -{ 1 }-> badd(z, z') :|: z >= 0, z' >= 0 ---------------------------------------- (17) 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: none And the following fresh constants: none ---------------------------------------- (18) 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: badd(x', Cons(x, xs)) -> badd(Cons(Nil, Nil), badd(x', xs)) [1] badd(x, Nil) -> x [1] goal(x, y) -> badd(x, y) [1] The TRS has the following type information: badd :: Cons:Nil -> Cons:Nil -> Cons:Nil Cons :: Cons:Nil -> Cons:Nil -> Cons:Nil Nil :: Cons:Nil goal :: Cons:Nil -> Cons:Nil -> Cons:Nil Rewrite Strategy: INNERMOST ---------------------------------------- (19) CpxTypedWeightedTrsToRntsProof (UPPER BOUND(ID)) Transformed the TRS into an over-approximating RNTS by (improved) Size Abstraction. The constant constructors are abstracted as follows: Nil => 0 ---------------------------------------- (20) Obligation: Complexity RNTS consisting of the following rules: badd(z, z') -{ 1 }-> x :|: x >= 0, z = x, z' = 0 badd(z, z') -{ 1 }-> badd(1 + 0 + 0, badd(x', xs)) :|: xs >= 0, z' = 1 + x + xs, x' >= 0, x >= 0, z = x' goal(z, z') -{ 1 }-> badd(x, y) :|: x >= 0, y >= 0, z = x, z' = y Only complete derivations are relevant for the runtime complexity. ---------------------------------------- (21) CpxTrsToCdtProof (UPPER BOUND(ID)) Converted Cpx (relative) TRS with rewrite strategy PARALLEL_INNERMOST to CDT ---------------------------------------- (22) Obligation: Complexity Dependency Tuples Problem Rules: badd(z0, Cons(z1, z2)) -> badd(Cons(Nil, Nil), badd(z0, z2)) badd(z0, Nil) -> z0 goal(z0, z1) -> badd(z0, z1) Tuples: BADD(z0, Cons(z1, z2)) -> c(BADD(Cons(Nil, Nil), badd(z0, z2)), BADD(z0, z2)) BADD(z0, Nil) -> c1 GOAL(z0, z1) -> c2(BADD(z0, z1)) S tuples: BADD(z0, Cons(z1, z2)) -> c(BADD(Cons(Nil, Nil), badd(z0, z2)), BADD(z0, z2)) BADD(z0, Nil) -> c1 GOAL(z0, z1) -> c2(BADD(z0, z1)) K tuples:none Defined Rule Symbols: badd_2, goal_2 Defined Pair Symbols: BADD_2, GOAL_2 Compound Symbols: c_2, c1, c2_1 ---------------------------------------- (23) CdtLeafRemovalProof (ComplexityIfPolyImplication) Removed 1 leading nodes: GOAL(z0, z1) -> c2(BADD(z0, z1)) Removed 1 trailing nodes: BADD(z0, Nil) -> c1 ---------------------------------------- (24) Obligation: Complexity Dependency Tuples Problem Rules: badd(z0, Cons(z1, z2)) -> badd(Cons(Nil, Nil), badd(z0, z2)) badd(z0, Nil) -> z0 goal(z0, z1) -> badd(z0, z1) Tuples: BADD(z0, Cons(z1, z2)) -> c(BADD(Cons(Nil, Nil), badd(z0, z2)), BADD(z0, z2)) S tuples: BADD(z0, Cons(z1, z2)) -> c(BADD(Cons(Nil, Nil), badd(z0, z2)), BADD(z0, z2)) K tuples:none Defined Rule Symbols: badd_2, goal_2 Defined Pair Symbols: BADD_2 Compound Symbols: c_2 ---------------------------------------- (25) CdtUsableRulesProof (BOTH BOUNDS(ID, ID)) The following rules are not usable and were removed: goal(z0, z1) -> badd(z0, z1) ---------------------------------------- (26) Obligation: Complexity Dependency Tuples Problem Rules: badd(z0, Cons(z1, z2)) -> badd(Cons(Nil, Nil), badd(z0, z2)) badd(z0, Nil) -> z0 Tuples: BADD(z0, Cons(z1, z2)) -> c(BADD(Cons(Nil, Nil), badd(z0, z2)), BADD(z0, z2)) S tuples: BADD(z0, Cons(z1, z2)) -> c(BADD(Cons(Nil, Nil), badd(z0, z2)), BADD(z0, z2)) K tuples:none Defined Rule Symbols: badd_2 Defined Pair Symbols: BADD_2 Compound Symbols: c_2 ---------------------------------------- (27) CdtNarrowingProof (BOTH BOUNDS(ID, ID)) Use narrowing to replace BADD(z0, Cons(z1, z2)) -> c(BADD(Cons(Nil, Nil), badd(z0, z2)), BADD(z0, z2)) by BADD(z0, Cons(x1, Cons(z1, z2))) -> c(BADD(Cons(Nil, Nil), badd(Cons(Nil, Nil), badd(z0, z2))), BADD(z0, Cons(z1, z2))) BADD(z0, Cons(x1, Nil)) -> c(BADD(Cons(Nil, Nil), z0), BADD(z0, Nil)) ---------------------------------------- (28) Obligation: Complexity Dependency Tuples Problem Rules: badd(z0, Cons(z1, z2)) -> badd(Cons(Nil, Nil), badd(z0, z2)) badd(z0, Nil) -> z0 Tuples: BADD(z0, Cons(x1, Cons(z1, z2))) -> c(BADD(Cons(Nil, Nil), badd(Cons(Nil, Nil), badd(z0, z2))), BADD(z0, Cons(z1, z2))) BADD(z0, Cons(x1, Nil)) -> c(BADD(Cons(Nil, Nil), z0), BADD(z0, Nil)) S tuples: BADD(z0, Cons(x1, Cons(z1, z2))) -> c(BADD(Cons(Nil, Nil), badd(Cons(Nil, Nil), badd(z0, z2))), BADD(z0, Cons(z1, z2))) BADD(z0, Cons(x1, Nil)) -> c(BADD(Cons(Nil, Nil), z0), BADD(z0, Nil)) K tuples:none Defined Rule Symbols: badd_2 Defined Pair Symbols: BADD_2 Compound Symbols: c_2 ---------------------------------------- (29) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID)) Removed 1 trailing tuple parts ---------------------------------------- (30) Obligation: Complexity Dependency Tuples Problem Rules: badd(z0, Cons(z1, z2)) -> badd(Cons(Nil, Nil), badd(z0, z2)) badd(z0, Nil) -> z0 Tuples: BADD(z0, Cons(x1, Cons(z1, z2))) -> c(BADD(Cons(Nil, Nil), badd(Cons(Nil, Nil), badd(z0, z2))), BADD(z0, Cons(z1, z2))) BADD(z0, Cons(x1, Nil)) -> c(BADD(Cons(Nil, Nil), z0)) S tuples: BADD(z0, Cons(x1, Cons(z1, z2))) -> c(BADD(Cons(Nil, Nil), badd(Cons(Nil, Nil), badd(z0, z2))), BADD(z0, Cons(z1, z2))) BADD(z0, Cons(x1, Nil)) -> c(BADD(Cons(Nil, Nil), z0)) K tuples:none Defined Rule Symbols: badd_2 Defined Pair Symbols: BADD_2 Compound Symbols: c_2, c_1 ---------------------------------------- (31) CdtNarrowingProof (BOTH BOUNDS(ID, ID)) Use narrowing to replace BADD(z0, Cons(x1, Cons(z1, z2))) -> c(BADD(Cons(Nil, Nil), badd(Cons(Nil, Nil), badd(z0, z2))), BADD(z0, Cons(z1, z2))) by BADD(z0, Cons(x1, Cons(x2, Cons(z1, z2)))) -> c(BADD(Cons(Nil, Nil), badd(Cons(Nil, Nil), badd(Cons(Nil, Nil), badd(z0, z2)))), BADD(z0, Cons(x2, Cons(z1, z2)))) BADD(z0, Cons(x1, Cons(x2, Nil))) -> c(BADD(Cons(Nil, Nil), badd(Cons(Nil, Nil), z0)), BADD(z0, Cons(x2, Nil))) ---------------------------------------- (32) Obligation: Complexity Dependency Tuples Problem Rules: badd(z0, Cons(z1, z2)) -> badd(Cons(Nil, Nil), badd(z0, z2)) badd(z0, Nil) -> z0 Tuples: BADD(z0, Cons(x1, Nil)) -> c(BADD(Cons(Nil, Nil), z0)) BADD(z0, Cons(x1, Cons(x2, Cons(z1, z2)))) -> c(BADD(Cons(Nil, Nil), badd(Cons(Nil, Nil), badd(Cons(Nil, Nil), badd(z0, z2)))), BADD(z0, Cons(x2, Cons(z1, z2)))) BADD(z0, Cons(x1, Cons(x2, Nil))) -> c(BADD(Cons(Nil, Nil), badd(Cons(Nil, Nil), z0)), BADD(z0, Cons(x2, Nil))) S tuples: BADD(z0, Cons(x1, Nil)) -> c(BADD(Cons(Nil, Nil), z0)) BADD(z0, Cons(x1, Cons(x2, Cons(z1, z2)))) -> c(BADD(Cons(Nil, Nil), badd(Cons(Nil, Nil), badd(Cons(Nil, Nil), badd(z0, z2)))), BADD(z0, Cons(x2, Cons(z1, z2)))) BADD(z0, Cons(x1, Cons(x2, Nil))) -> c(BADD(Cons(Nil, Nil), badd(Cons(Nil, Nil), z0)), BADD(z0, Cons(x2, Nil))) K tuples:none Defined Rule Symbols: badd_2 Defined Pair Symbols: BADD_2 Compound Symbols: c_1, c_2 ---------------------------------------- (33) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID)) Use forward instantiation to replace BADD(z0, Cons(x1, Nil)) -> c(BADD(Cons(Nil, Nil), z0)) by BADD(Cons(y1, Nil), Cons(z1, Nil)) -> c(BADD(Cons(Nil, Nil), Cons(y1, Nil))) BADD(Cons(y1, Cons(y2, Cons(y3, y4))), Cons(z1, Nil)) -> c(BADD(Cons(Nil, Nil), Cons(y1, Cons(y2, Cons(y3, y4))))) BADD(Cons(y1, Cons(y2, Nil)), Cons(z1, Nil)) -> c(BADD(Cons(Nil, Nil), Cons(y1, Cons(y2, Nil)))) ---------------------------------------- (34) Obligation: Complexity Dependency Tuples Problem Rules: badd(z0, Cons(z1, z2)) -> badd(Cons(Nil, Nil), badd(z0, z2)) badd(z0, Nil) -> z0 Tuples: BADD(z0, Cons(x1, Cons(x2, Cons(z1, z2)))) -> c(BADD(Cons(Nil, Nil), badd(Cons(Nil, Nil), badd(Cons(Nil, Nil), badd(z0, z2)))), BADD(z0, Cons(x2, Cons(z1, z2)))) BADD(z0, Cons(x1, Cons(x2, Nil))) -> c(BADD(Cons(Nil, Nil), badd(Cons(Nil, Nil), z0)), BADD(z0, Cons(x2, Nil))) BADD(Cons(y1, Nil), Cons(z1, Nil)) -> c(BADD(Cons(Nil, Nil), Cons(y1, Nil))) BADD(Cons(y1, Cons(y2, Cons(y3, y4))), Cons(z1, Nil)) -> c(BADD(Cons(Nil, Nil), Cons(y1, Cons(y2, Cons(y3, y4))))) BADD(Cons(y1, Cons(y2, Nil)), Cons(z1, Nil)) -> c(BADD(Cons(Nil, Nil), Cons(y1, Cons(y2, Nil)))) S tuples: BADD(z0, Cons(x1, Cons(x2, Cons(z1, z2)))) -> c(BADD(Cons(Nil, Nil), badd(Cons(Nil, Nil), badd(Cons(Nil, Nil), badd(z0, z2)))), BADD(z0, Cons(x2, Cons(z1, z2)))) BADD(z0, Cons(x1, Cons(x2, Nil))) -> c(BADD(Cons(Nil, Nil), badd(Cons(Nil, Nil), z0)), BADD(z0, Cons(x2, Nil))) BADD(Cons(y1, Nil), Cons(z1, Nil)) -> c(BADD(Cons(Nil, Nil), Cons(y1, Nil))) BADD(Cons(y1, Cons(y2, Cons(y3, y4))), Cons(z1, Nil)) -> c(BADD(Cons(Nil, Nil), Cons(y1, Cons(y2, Cons(y3, y4))))) BADD(Cons(y1, Cons(y2, Nil)), Cons(z1, Nil)) -> c(BADD(Cons(Nil, Nil), Cons(y1, Cons(y2, Nil)))) K tuples:none Defined Rule Symbols: badd_2 Defined Pair Symbols: BADD_2 Compound Symbols: c_2, c_1 ---------------------------------------- (35) CdtRuleRemovalProof (UPPER BOUND(ADD(n^2))) Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S. BADD(Cons(y1, Cons(y2, Cons(y3, y4))), Cons(z1, Nil)) -> c(BADD(Cons(Nil, Nil), Cons(y1, Cons(y2, Cons(y3, y4))))) BADD(Cons(y1, Cons(y2, Nil)), Cons(z1, Nil)) -> c(BADD(Cons(Nil, Nil), Cons(y1, Cons(y2, Nil)))) We considered the (Usable) Rules:none And the Tuples: BADD(z0, Cons(x1, Cons(x2, Cons(z1, z2)))) -> c(BADD(Cons(Nil, Nil), badd(Cons(Nil, Nil), badd(Cons(Nil, Nil), badd(z0, z2)))), BADD(z0, Cons(x2, Cons(z1, z2)))) BADD(z0, Cons(x1, Cons(x2, Nil))) -> c(BADD(Cons(Nil, Nil), badd(Cons(Nil, Nil), z0)), BADD(z0, Cons(x2, Nil))) BADD(Cons(y1, Nil), Cons(z1, Nil)) -> c(BADD(Cons(Nil, Nil), Cons(y1, Nil))) BADD(Cons(y1, Cons(y2, Cons(y3, y4))), Cons(z1, Nil)) -> c(BADD(Cons(Nil, Nil), Cons(y1, Cons(y2, Cons(y3, y4))))) BADD(Cons(y1, Cons(y2, Nil)), Cons(z1, Nil)) -> c(BADD(Cons(Nil, Nil), Cons(y1, Cons(y2, Nil)))) The order we found is given by the following interpretation: Matrix interpretation [MATRO]: Non-tuple symbols: <<< M( badd_2(x_1, x_2) ) = [[0], [0]] + [[0, 0], [0, 0]] * x_1 + [[0, 0], [0, 0]] * x_2 >>> <<< M( Cons_2(x_1, x_2) ) = [[0], [4]] + [[0, 0], [0, 0]] * x_1 + [[0, 4], [0, 0]] * x_2 >>> <<< M( Nil ) = [[0], [0]] >>> Tuple symbols: <<< M( c_2(x_1, x_2) ) = [[0], [0]] + [[1, 0], [0, 0]] * x_1 + [[1, 0], [0, 0]] * x_2 >>> <<< M( c_1(x_1) ) = [[0], [0]] + [[1, 0], [0, 0]] * x_1 >>> <<< M( BADD_2(x_1, x_2) ) = [[0], [2]] + [[1, 0], [0, 0]] * x_1 + [[0, 0], [0, 0]] * x_2 >>> 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. ---------------------------------------- (36) Obligation: Complexity Dependency Tuples Problem Rules: badd(z0, Cons(z1, z2)) -> badd(Cons(Nil, Nil), badd(z0, z2)) badd(z0, Nil) -> z0 Tuples: BADD(z0, Cons(x1, Cons(x2, Cons(z1, z2)))) -> c(BADD(Cons(Nil, Nil), badd(Cons(Nil, Nil), badd(Cons(Nil, Nil), badd(z0, z2)))), BADD(z0, Cons(x2, Cons(z1, z2)))) BADD(z0, Cons(x1, Cons(x2, Nil))) -> c(BADD(Cons(Nil, Nil), badd(Cons(Nil, Nil), z0)), BADD(z0, Cons(x2, Nil))) BADD(Cons(y1, Nil), Cons(z1, Nil)) -> c(BADD(Cons(Nil, Nil), Cons(y1, Nil))) BADD(Cons(y1, Cons(y2, Cons(y3, y4))), Cons(z1, Nil)) -> c(BADD(Cons(Nil, Nil), Cons(y1, Cons(y2, Cons(y3, y4))))) BADD(Cons(y1, Cons(y2, Nil)), Cons(z1, Nil)) -> c(BADD(Cons(Nil, Nil), Cons(y1, Cons(y2, Nil)))) S tuples: BADD(z0, Cons(x1, Cons(x2, Cons(z1, z2)))) -> c(BADD(Cons(Nil, Nil), badd(Cons(Nil, Nil), badd(Cons(Nil, Nil), badd(z0, z2)))), BADD(z0, Cons(x2, Cons(z1, z2)))) BADD(z0, Cons(x1, Cons(x2, Nil))) -> c(BADD(Cons(Nil, Nil), badd(Cons(Nil, Nil), z0)), BADD(z0, Cons(x2, Nil))) BADD(Cons(y1, Nil), Cons(z1, Nil)) -> c(BADD(Cons(Nil, Nil), Cons(y1, Nil))) K tuples: BADD(Cons(y1, Cons(y2, Cons(y3, y4))), Cons(z1, Nil)) -> c(BADD(Cons(Nil, Nil), Cons(y1, Cons(y2, Cons(y3, y4))))) BADD(Cons(y1, Cons(y2, Nil)), Cons(z1, Nil)) -> c(BADD(Cons(Nil, Nil), Cons(y1, Cons(y2, Nil)))) Defined Rule Symbols: badd_2 Defined Pair Symbols: BADD_2 Compound Symbols: c_2, c_1 ---------------------------------------- (37) CdtRuleRemovalProof (UPPER BOUND(ADD(n^2))) Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S. BADD(z0, Cons(x1, Cons(x2, Cons(z1, z2)))) -> c(BADD(Cons(Nil, Nil), badd(Cons(Nil, Nil), badd(Cons(Nil, Nil), badd(z0, z2)))), BADD(z0, Cons(x2, Cons(z1, z2)))) BADD(z0, Cons(x1, Cons(x2, Nil))) -> c(BADD(Cons(Nil, Nil), badd(Cons(Nil, Nil), z0)), BADD(z0, Cons(x2, Nil))) We considered the (Usable) Rules: badd(z0, Cons(z1, z2)) -> badd(Cons(Nil, Nil), badd(z0, z2)) badd(z0, Nil) -> z0 And the Tuples: BADD(z0, Cons(x1, Cons(x2, Cons(z1, z2)))) -> c(BADD(Cons(Nil, Nil), badd(Cons(Nil, Nil), badd(Cons(Nil, Nil), badd(z0, z2)))), BADD(z0, Cons(x2, Cons(z1, z2)))) BADD(z0, Cons(x1, Cons(x2, Nil))) -> c(BADD(Cons(Nil, Nil), badd(Cons(Nil, Nil), z0)), BADD(z0, Cons(x2, Nil))) BADD(Cons(y1, Nil), Cons(z1, Nil)) -> c(BADD(Cons(Nil, Nil), Cons(y1, Nil))) BADD(Cons(y1, Cons(y2, Cons(y3, y4))), Cons(z1, Nil)) -> c(BADD(Cons(Nil, Nil), Cons(y1, Cons(y2, Cons(y3, y4))))) BADD(Cons(y1, Cons(y2, Nil)), Cons(z1, Nil)) -> c(BADD(Cons(Nil, Nil), Cons(y1, Cons(y2, Nil)))) The order we found is given by the following interpretation: Matrix interpretation [MATRO]: Non-tuple symbols: <<< M( badd_2(x_1, x_2) ) = [[0], [0]] + [[2, 0], [0, 1]] * x_1 + [[0, 0], [0, 1]] * x_2 >>> <<< M( Cons_2(x_1, x_2) ) = [[0], [2]] + [[0, 0], [0, 0]] * x_1 + [[0, 4], [0, 1]] * x_2 >>> <<< M( Nil ) = [[0], [0]] >>> Tuple symbols: <<< M( c_2(x_1, x_2) ) = [[0], [0]] + [[1, 0], [0, 0]] * x_1 + [[1, 0], [0, 0]] * x_2 >>> <<< M( c_1(x_1) ) = [[0], [0]] + [[1, 0], [0, 0]] * x_1 >>> <<< M( BADD_2(x_1, x_2) ) = [[0], [0]] + [[1, 0], [0, 0]] * x_1 + [[1, 0], [0, 0]] * x_2 >>> 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. ---------------------------------------- (38) Obligation: Complexity Dependency Tuples Problem Rules: badd(z0, Cons(z1, z2)) -> badd(Cons(Nil, Nil), badd(z0, z2)) badd(z0, Nil) -> z0 Tuples: BADD(z0, Cons(x1, Cons(x2, Cons(z1, z2)))) -> c(BADD(Cons(Nil, Nil), badd(Cons(Nil, Nil), badd(Cons(Nil, Nil), badd(z0, z2)))), BADD(z0, Cons(x2, Cons(z1, z2)))) BADD(z0, Cons(x1, Cons(x2, Nil))) -> c(BADD(Cons(Nil, Nil), badd(Cons(Nil, Nil), z0)), BADD(z0, Cons(x2, Nil))) BADD(Cons(y1, Nil), Cons(z1, Nil)) -> c(BADD(Cons(Nil, Nil), Cons(y1, Nil))) BADD(Cons(y1, Cons(y2, Cons(y3, y4))), Cons(z1, Nil)) -> c(BADD(Cons(Nil, Nil), Cons(y1, Cons(y2, Cons(y3, y4))))) BADD(Cons(y1, Cons(y2, Nil)), Cons(z1, Nil)) -> c(BADD(Cons(Nil, Nil), Cons(y1, Cons(y2, Nil)))) S tuples: BADD(Cons(y1, Nil), Cons(z1, Nil)) -> c(BADD(Cons(Nil, Nil), Cons(y1, Nil))) K tuples: BADD(Cons(y1, Cons(y2, Cons(y3, y4))), Cons(z1, Nil)) -> c(BADD(Cons(Nil, Nil), Cons(y1, Cons(y2, Cons(y3, y4))))) BADD(Cons(y1, Cons(y2, Nil)), Cons(z1, Nil)) -> c(BADD(Cons(Nil, Nil), Cons(y1, Cons(y2, Nil)))) BADD(z0, Cons(x1, Cons(x2, Cons(z1, z2)))) -> c(BADD(Cons(Nil, Nil), badd(Cons(Nil, Nil), badd(Cons(Nil, Nil), badd(z0, z2)))), BADD(z0, Cons(x2, Cons(z1, z2)))) BADD(z0, Cons(x1, Cons(x2, Nil))) -> c(BADD(Cons(Nil, Nil), badd(Cons(Nil, Nil), z0)), BADD(z0, Cons(x2, Nil))) Defined Rule Symbols: badd_2 Defined Pair Symbols: BADD_2 Compound Symbols: c_2, c_1