KILLED proof of input_hGOONsmclc.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 [BOTH BOUNDS(ID, ID), 0 ms] (24) CdtProblem (25) CdtNarrowingProof [BOTH BOUNDS(ID, ID), 0 ms] (26) CdtProblem (27) CdtRhsSimplificationProcessorProof [BOTH BOUNDS(ID, ID), 0 ms] (28) CdtProblem (29) CdtRuleRemovalProof [UPPER BOUND(ADD(n^1)), 21 ms] (30) CdtProblem (31) CdtNarrowingProof [BOTH BOUNDS(ID, ID), 0 ms] (32) CdtProblem (33) CdtForwardInstantiationProof [BOTH BOUNDS(ID, ID), 0 ms] (34) CdtProblem (35) CdtForwardInstantiationProof [BOTH BOUNDS(ID, ID), 0 ms] (36) CdtProblem (37) CdtForwardInstantiationProof [BOTH BOUNDS(ID, ID), 0 ms] (38) CdtProblem (39) CdtRuleRemovalProof [UPPER BOUND(ADD(n^1)), 25 ms] (40) CdtProblem (41) CdtForwardInstantiationProof [BOTH BOUNDS(ID, ID), 0 ms] (42) CdtProblem (43) CdtForwardInstantiationProof [BOTH BOUNDS(ID, ID), 0 ms] (44) CdtProblem (45) CdtForwardInstantiationProof [BOTH BOUNDS(ID, ID), 0 ms] (46) CdtProblem (47) CdtForwardInstantiationProof [BOTH BOUNDS(ID, ID), 0 ms] (48) 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: f(a, g(y)) -> g(g(y)) f(g(x), a) -> f(x, g(a)) f(g(x), g(y)) -> h(g(y), x, g(y)) h(g(x), y, z) -> f(y, h(x, y, z)) h(a, y, z) -> z 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: f(a, g(y)) -> g(g(y)) f(g(x), a) -> f(x, g(a)) f(g(x), g(y)) -> h(g(y), x, g(y)) h(g(x), y, z) -> f(y, h(x, y, z)) h(a, y, z) -> z 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: f(a, g(y)) -> g(g(y)) f(g(x), a) -> f(x, g(a)) f(g(x), g(y)) -> h(g(y), x, g(y)) h(g(x), y, z) -> f(y, h(x, y, z)) h(a, y, z) -> z 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: f(a, g(y)) -> g(g(y)) [1] f(g(x), a) -> f(x, g(a)) [1] f(g(x), g(y)) -> h(g(y), x, g(y)) [1] h(g(x), y, z) -> f(y, h(x, y, z)) [1] h(a, y, z) -> z [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: f(a, g(y)) -> g(g(y)) [1] f(g(x), a) -> f(x, g(a)) [1] f(g(x), g(y)) -> h(g(y), x, g(y)) [1] h(g(x), y, z) -> f(y, h(x, y, z)) [1] h(a, y, z) -> z [1] The TRS has the following type information: f :: a:g -> a:g -> a:g a :: a:g g :: a:g -> a:g h :: a:g -> a:g -> a:g -> a:g 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: none (c) The following functions are completely defined: h_3 f_2 Due to the following rules being added: f(v0, v1) -> a [0] 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: f(a, g(y)) -> g(g(y)) [1] f(g(x), a) -> f(x, g(a)) [1] f(g(x), g(y)) -> h(g(y), x, g(y)) [1] h(g(x), y, z) -> f(y, h(x, y, z)) [1] h(a, y, z) -> z [1] f(v0, v1) -> a [0] The TRS has the following type information: f :: a:g -> a:g -> a:g a :: a:g g :: a:g -> a:g h :: a:g -> a:g -> a:g -> a:g 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: f(a, g(y)) -> g(g(y)) [1] f(g(x), a) -> f(x, g(a)) [1] f(g(x), g(y)) -> h(g(y), x, g(y)) [1] h(g(g(x')), y, z) -> f(y, f(y, h(x', y, z))) [2] h(g(a), y, z) -> f(y, z) [2] h(a, y, z) -> z [1] f(v0, v1) -> a [0] The TRS has the following type information: f :: a:g -> a:g -> a:g a :: a:g g :: a:g -> a:g h :: a:g -> a:g -> a:g -> a:g 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: a => 0 ---------------------------------------- (14) Obligation: Complexity RNTS consisting of the following rules: f(z', z'') -{ 1 }-> h(1 + y, x, 1 + y) :|: z' = 1 + x, x >= 0, y >= 0, z'' = 1 + y f(z', z'') -{ 1 }-> f(x, 1 + 0) :|: z'' = 0, z' = 1 + x, x >= 0 f(z', z'') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z'' = v1, z' = v0 f(z', z'') -{ 1 }-> 1 + (1 + y) :|: y >= 0, z'' = 1 + y, z' = 0 h(z', z'', z1) -{ 1 }-> z :|: z1 = z, z >= 0, z'' = y, y >= 0, z' = 0 h(z', z'', z1) -{ 2 }-> f(y, z) :|: z1 = z, z >= 0, z'' = y, y >= 0, z' = 1 + 0 h(z', z'', z1) -{ 2 }-> f(y, f(y, h(x', y, z))) :|: z' = 1 + (1 + x'), z1 = z, z >= 0, z'' = y, x' >= 0, y >= 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: f(z', z'') -{ 1 }-> h(1 + (z'' - 1), z' - 1, 1 + (z'' - 1)) :|: z' - 1 >= 0, z'' - 1 >= 0 f(z', z'') -{ 1 }-> f(z' - 1, 1 + 0) :|: z'' = 0, z' - 1 >= 0 f(z', z'') -{ 0 }-> 0 :|: z' >= 0, z'' >= 0 f(z', z'') -{ 1 }-> 1 + (1 + (z'' - 1)) :|: z'' - 1 >= 0, z' = 0 h(z', z'', z1) -{ 1 }-> z1 :|: z1 >= 0, z'' >= 0, z' = 0 h(z', z'', z1) -{ 2 }-> f(z'', z1) :|: z1 >= 0, z'' >= 0, z' = 1 + 0 h(z', z'', z1) -{ 2 }-> f(z'', f(z'', h(z' - 2, z'', z1))) :|: z1 >= 0, z' - 2 >= 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: f(v0, v1) -> null_f [0] h(v0, v1, v2) -> null_h [0] And the following fresh constants: null_f, null_h ---------------------------------------- (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: f(a, g(y)) -> g(g(y)) [1] f(g(x), a) -> f(x, g(a)) [1] f(g(x), g(y)) -> h(g(y), x, g(y)) [1] h(g(x), y, z) -> f(y, h(x, y, z)) [1] h(a, y, z) -> z [1] f(v0, v1) -> null_f [0] h(v0, v1, v2) -> null_h [0] The TRS has the following type information: f :: a:g:null_f:null_h -> a:g:null_f:null_h -> a:g:null_f:null_h a :: a:g:null_f:null_h g :: a:g:null_f:null_h -> a:g:null_f:null_h h :: a:g:null_f:null_h -> a:g:null_f:null_h -> a:g:null_f:null_h -> a:g:null_f:null_h null_f :: a:g:null_f:null_h null_h :: a:g:null_f:null_h 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: a => 0 null_f => 0 null_h => 0 ---------------------------------------- (20) Obligation: Complexity RNTS consisting of the following rules: f(z', z'') -{ 1 }-> h(1 + y, x, 1 + y) :|: z' = 1 + x, x >= 0, y >= 0, z'' = 1 + y f(z', z'') -{ 1 }-> f(x, 1 + 0) :|: z'' = 0, z' = 1 + x, x >= 0 f(z', z'') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z'' = v1, z' = v0 f(z', z'') -{ 1 }-> 1 + (1 + y) :|: y >= 0, z'' = 1 + y, z' = 0 h(z', z'', z1) -{ 1 }-> z :|: z1 = z, z >= 0, z'' = y, y >= 0, z' = 0 h(z', z'', z1) -{ 1 }-> f(y, h(x, y, z)) :|: z' = 1 + x, z1 = z, z >= 0, z'' = y, x >= 0, y >= 0 h(z', z'', z1) -{ 0 }-> 0 :|: v0 >= 0, z1 = v2, v1 >= 0, z'' = v1, v2 >= 0, z' = v0 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: f(a, g(z0)) -> g(g(z0)) f(g(z0), a) -> f(z0, g(a)) f(g(z0), g(z1)) -> h(g(z1), z0, g(z1)) h(g(z0), z1, z2) -> f(z1, h(z0, z1, z2)) h(a, z0, z1) -> z1 Tuples: F(a, g(z0)) -> c F(g(z0), a) -> c1(F(z0, g(a))) F(g(z0), g(z1)) -> c2(H(g(z1), z0, g(z1))) H(g(z0), z1, z2) -> c3(F(z1, h(z0, z1, z2)), H(z0, z1, z2)) H(a, z0, z1) -> c4 S tuples: F(a, g(z0)) -> c F(g(z0), a) -> c1(F(z0, g(a))) F(g(z0), g(z1)) -> c2(H(g(z1), z0, g(z1))) H(g(z0), z1, z2) -> c3(F(z1, h(z0, z1, z2)), H(z0, z1, z2)) H(a, z0, z1) -> c4 K tuples:none Defined Rule Symbols: f_2, h_3 Defined Pair Symbols: F_2, H_3 Compound Symbols: c, c1_1, c2_1, c3_2, c4 ---------------------------------------- (23) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID)) Removed 2 trailing nodes: H(a, z0, z1) -> c4 F(a, g(z0)) -> c ---------------------------------------- (24) Obligation: Complexity Dependency Tuples Problem Rules: f(a, g(z0)) -> g(g(z0)) f(g(z0), a) -> f(z0, g(a)) f(g(z0), g(z1)) -> h(g(z1), z0, g(z1)) h(g(z0), z1, z2) -> f(z1, h(z0, z1, z2)) h(a, z0, z1) -> z1 Tuples: F(g(z0), a) -> c1(F(z0, g(a))) F(g(z0), g(z1)) -> c2(H(g(z1), z0, g(z1))) H(g(z0), z1, z2) -> c3(F(z1, h(z0, z1, z2)), H(z0, z1, z2)) S tuples: F(g(z0), a) -> c1(F(z0, g(a))) F(g(z0), g(z1)) -> c2(H(g(z1), z0, g(z1))) H(g(z0), z1, z2) -> c3(F(z1, h(z0, z1, z2)), H(z0, z1, z2)) K tuples:none Defined Rule Symbols: f_2, h_3 Defined Pair Symbols: F_2, H_3 Compound Symbols: c1_1, c2_1, c3_2 ---------------------------------------- (25) CdtNarrowingProof (BOTH BOUNDS(ID, ID)) Use narrowing to replace H(g(z0), z1, z2) -> c3(F(z1, h(z0, z1, z2)), H(z0, z1, z2)) by H(g(g(z0)), z1, z2) -> c3(F(z1, f(z1, h(z0, z1, z2))), H(g(z0), z1, z2)) H(g(a), z0, z1) -> c3(F(z0, z1), H(a, z0, z1)) ---------------------------------------- (26) Obligation: Complexity Dependency Tuples Problem Rules: f(a, g(z0)) -> g(g(z0)) f(g(z0), a) -> f(z0, g(a)) f(g(z0), g(z1)) -> h(g(z1), z0, g(z1)) h(g(z0), z1, z2) -> f(z1, h(z0, z1, z2)) h(a, z0, z1) -> z1 Tuples: F(g(z0), a) -> c1(F(z0, g(a))) F(g(z0), g(z1)) -> c2(H(g(z1), z0, g(z1))) H(g(g(z0)), z1, z2) -> c3(F(z1, f(z1, h(z0, z1, z2))), H(g(z0), z1, z2)) H(g(a), z0, z1) -> c3(F(z0, z1), H(a, z0, z1)) S tuples: F(g(z0), a) -> c1(F(z0, g(a))) F(g(z0), g(z1)) -> c2(H(g(z1), z0, g(z1))) H(g(g(z0)), z1, z2) -> c3(F(z1, f(z1, h(z0, z1, z2))), H(g(z0), z1, z2)) H(g(a), z0, z1) -> c3(F(z0, z1), H(a, z0, z1)) K tuples:none Defined Rule Symbols: f_2, h_3 Defined Pair Symbols: F_2, H_3 Compound Symbols: c1_1, c2_1, c3_2 ---------------------------------------- (27) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID)) Removed 1 trailing tuple parts ---------------------------------------- (28) Obligation: Complexity Dependency Tuples Problem Rules: f(a, g(z0)) -> g(g(z0)) f(g(z0), a) -> f(z0, g(a)) f(g(z0), g(z1)) -> h(g(z1), z0, g(z1)) h(g(z0), z1, z2) -> f(z1, h(z0, z1, z2)) h(a, z0, z1) -> z1 Tuples: F(g(z0), a) -> c1(F(z0, g(a))) F(g(z0), g(z1)) -> c2(H(g(z1), z0, g(z1))) H(g(g(z0)), z1, z2) -> c3(F(z1, f(z1, h(z0, z1, z2))), H(g(z0), z1, z2)) H(g(a), z0, z1) -> c3(F(z0, z1)) S tuples: F(g(z0), a) -> c1(F(z0, g(a))) F(g(z0), g(z1)) -> c2(H(g(z1), z0, g(z1))) H(g(g(z0)), z1, z2) -> c3(F(z1, f(z1, h(z0, z1, z2))), H(g(z0), z1, z2)) H(g(a), z0, z1) -> c3(F(z0, z1)) K tuples:none Defined Rule Symbols: f_2, h_3 Defined Pair Symbols: F_2, H_3 Compound Symbols: c1_1, c2_1, c3_2, c3_1 ---------------------------------------- (29) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1))) Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S. F(g(z0), a) -> c1(F(z0, g(a))) We considered the (Usable) Rules: f(g(z0), g(z1)) -> h(g(z1), z0, g(z1)) f(a, g(z0)) -> g(g(z0)) h(g(z0), z1, z2) -> f(z1, h(z0, z1, z2)) f(g(z0), a) -> f(z0, g(a)) And the Tuples: F(g(z0), a) -> c1(F(z0, g(a))) F(g(z0), g(z1)) -> c2(H(g(z1), z0, g(z1))) H(g(g(z0)), z1, z2) -> c3(F(z1, f(z1, h(z0, z1, z2))), H(g(z0), z1, z2)) H(g(a), z0, z1) -> c3(F(z0, z1)) The order we found is given by the following interpretation: Polynomial interpretation : POL(F(x_1, x_2)) = x_2 POL(H(x_1, x_2, x_3)) = x_1 + x_3 POL(a) = [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(f(x_1, x_2)) = 0 POL(g(x_1)) = 0 POL(h(x_1, x_2, x_3)) = x_1 + x_3 ---------------------------------------- (30) Obligation: Complexity Dependency Tuples Problem Rules: f(a, g(z0)) -> g(g(z0)) f(g(z0), a) -> f(z0, g(a)) f(g(z0), g(z1)) -> h(g(z1), z0, g(z1)) h(g(z0), z1, z2) -> f(z1, h(z0, z1, z2)) h(a, z0, z1) -> z1 Tuples: F(g(z0), a) -> c1(F(z0, g(a))) F(g(z0), g(z1)) -> c2(H(g(z1), z0, g(z1))) H(g(g(z0)), z1, z2) -> c3(F(z1, f(z1, h(z0, z1, z2))), H(g(z0), z1, z2)) H(g(a), z0, z1) -> c3(F(z0, z1)) S tuples: F(g(z0), g(z1)) -> c2(H(g(z1), z0, g(z1))) H(g(g(z0)), z1, z2) -> c3(F(z1, f(z1, h(z0, z1, z2))), H(g(z0), z1, z2)) H(g(a), z0, z1) -> c3(F(z0, z1)) K tuples: F(g(z0), a) -> c1(F(z0, g(a))) Defined Rule Symbols: f_2, h_3 Defined Pair Symbols: F_2, H_3 Compound Symbols: c1_1, c2_1, c3_2, c3_1 ---------------------------------------- (31) CdtNarrowingProof (BOTH BOUNDS(ID, ID)) Use narrowing to replace H(g(g(z0)), z1, z2) -> c3(F(z1, f(z1, h(z0, z1, z2))), H(g(z0), z1, z2)) by H(g(g(g(z0))), z1, z2) -> c3(F(z1, f(z1, f(z1, h(z0, z1, z2)))), H(g(g(z0)), z1, z2)) H(g(g(a)), z0, z1) -> c3(F(z0, f(z0, z1)), H(g(a), z0, z1)) ---------------------------------------- (32) Obligation: Complexity Dependency Tuples Problem Rules: f(a, g(z0)) -> g(g(z0)) f(g(z0), a) -> f(z0, g(a)) f(g(z0), g(z1)) -> h(g(z1), z0, g(z1)) h(g(z0), z1, z2) -> f(z1, h(z0, z1, z2)) h(a, z0, z1) -> z1 Tuples: F(g(z0), a) -> c1(F(z0, g(a))) F(g(z0), g(z1)) -> c2(H(g(z1), z0, g(z1))) H(g(a), z0, z1) -> c3(F(z0, z1)) H(g(g(g(z0))), z1, z2) -> c3(F(z1, f(z1, f(z1, h(z0, z1, z2)))), H(g(g(z0)), z1, z2)) H(g(g(a)), z0, z1) -> c3(F(z0, f(z0, z1)), H(g(a), z0, z1)) S tuples: F(g(z0), g(z1)) -> c2(H(g(z1), z0, g(z1))) H(g(a), z0, z1) -> c3(F(z0, z1)) H(g(g(g(z0))), z1, z2) -> c3(F(z1, f(z1, f(z1, h(z0, z1, z2)))), H(g(g(z0)), z1, z2)) H(g(g(a)), z0, z1) -> c3(F(z0, f(z0, z1)), H(g(a), z0, z1)) K tuples: F(g(z0), a) -> c1(F(z0, g(a))) Defined Rule Symbols: f_2, h_3 Defined Pair Symbols: F_2, H_3 Compound Symbols: c1_1, c2_1, c3_1, c3_2 ---------------------------------------- (33) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID)) Use forward instantiation to replace F(g(z0), a) -> c1(F(z0, g(a))) by F(g(g(y0)), a) -> c1(F(g(y0), g(a))) ---------------------------------------- (34) Obligation: Complexity Dependency Tuples Problem Rules: f(a, g(z0)) -> g(g(z0)) f(g(z0), a) -> f(z0, g(a)) f(g(z0), g(z1)) -> h(g(z1), z0, g(z1)) h(g(z0), z1, z2) -> f(z1, h(z0, z1, z2)) h(a, z0, z1) -> z1 Tuples: F(g(z0), g(z1)) -> c2(H(g(z1), z0, g(z1))) H(g(a), z0, z1) -> c3(F(z0, z1)) H(g(g(g(z0))), z1, z2) -> c3(F(z1, f(z1, f(z1, h(z0, z1, z2)))), H(g(g(z0)), z1, z2)) H(g(g(a)), z0, z1) -> c3(F(z0, f(z0, z1)), H(g(a), z0, z1)) F(g(g(y0)), a) -> c1(F(g(y0), g(a))) S tuples: F(g(z0), g(z1)) -> c2(H(g(z1), z0, g(z1))) H(g(a), z0, z1) -> c3(F(z0, z1)) H(g(g(g(z0))), z1, z2) -> c3(F(z1, f(z1, f(z1, h(z0, z1, z2)))), H(g(g(z0)), z1, z2)) H(g(g(a)), z0, z1) -> c3(F(z0, f(z0, z1)), H(g(a), z0, z1)) K tuples: F(g(g(y0)), a) -> c1(F(g(y0), g(a))) Defined Rule Symbols: f_2, h_3 Defined Pair Symbols: F_2, H_3 Compound Symbols: c2_1, c3_1, c3_2, c1_1 ---------------------------------------- (35) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID)) Use forward instantiation to replace F(g(z0), g(z1)) -> c2(H(g(z1), z0, g(z1))) by F(g(z0), g(a)) -> c2(H(g(a), z0, g(a))) F(g(z0), g(g(g(y0)))) -> c2(H(g(g(g(y0))), z0, g(g(g(y0))))) F(g(z0), g(g(a))) -> c2(H(g(g(a)), z0, g(g(a)))) ---------------------------------------- (36) Obligation: Complexity Dependency Tuples Problem Rules: f(a, g(z0)) -> g(g(z0)) f(g(z0), a) -> f(z0, g(a)) f(g(z0), g(z1)) -> h(g(z1), z0, g(z1)) h(g(z0), z1, z2) -> f(z1, h(z0, z1, z2)) h(a, z0, z1) -> z1 Tuples: H(g(a), z0, z1) -> c3(F(z0, z1)) H(g(g(g(z0))), z1, z2) -> c3(F(z1, f(z1, f(z1, h(z0, z1, z2)))), H(g(g(z0)), z1, z2)) H(g(g(a)), z0, z1) -> c3(F(z0, f(z0, z1)), H(g(a), z0, z1)) F(g(g(y0)), a) -> c1(F(g(y0), g(a))) F(g(z0), g(a)) -> c2(H(g(a), z0, g(a))) F(g(z0), g(g(g(y0)))) -> c2(H(g(g(g(y0))), z0, g(g(g(y0))))) F(g(z0), g(g(a))) -> c2(H(g(g(a)), z0, g(g(a)))) S tuples: H(g(a), z0, z1) -> c3(F(z0, z1)) H(g(g(g(z0))), z1, z2) -> c3(F(z1, f(z1, f(z1, h(z0, z1, z2)))), H(g(g(z0)), z1, z2)) H(g(g(a)), z0, z1) -> c3(F(z0, f(z0, z1)), H(g(a), z0, z1)) F(g(z0), g(a)) -> c2(H(g(a), z0, g(a))) F(g(z0), g(g(g(y0)))) -> c2(H(g(g(g(y0))), z0, g(g(g(y0))))) F(g(z0), g(g(a))) -> c2(H(g(g(a)), z0, g(g(a)))) K tuples: F(g(g(y0)), a) -> c1(F(g(y0), g(a))) Defined Rule Symbols: f_2, h_3 Defined Pair Symbols: H_3, F_2 Compound Symbols: c3_1, c3_2, c1_1, c2_1 ---------------------------------------- (37) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID)) Use forward instantiation to replace H(g(a), z0, z1) -> c3(F(z0, z1)) by H(g(a), g(g(y0)), a) -> c3(F(g(g(y0)), a)) H(g(a), g(y0), g(a)) -> c3(F(g(y0), g(a))) H(g(a), g(y0), g(g(g(y1)))) -> c3(F(g(y0), g(g(g(y1))))) H(g(a), g(y0), g(g(a))) -> c3(F(g(y0), g(g(a)))) ---------------------------------------- (38) Obligation: Complexity Dependency Tuples Problem Rules: f(a, g(z0)) -> g(g(z0)) f(g(z0), a) -> f(z0, g(a)) f(g(z0), g(z1)) -> h(g(z1), z0, g(z1)) h(g(z0), z1, z2) -> f(z1, h(z0, z1, z2)) h(a, z0, z1) -> z1 Tuples: H(g(g(g(z0))), z1, z2) -> c3(F(z1, f(z1, f(z1, h(z0, z1, z2)))), H(g(g(z0)), z1, z2)) H(g(g(a)), z0, z1) -> c3(F(z0, f(z0, z1)), H(g(a), z0, z1)) F(g(g(y0)), a) -> c1(F(g(y0), g(a))) F(g(z0), g(a)) -> c2(H(g(a), z0, g(a))) F(g(z0), g(g(g(y0)))) -> c2(H(g(g(g(y0))), z0, g(g(g(y0))))) F(g(z0), g(g(a))) -> c2(H(g(g(a)), z0, g(g(a)))) H(g(a), g(g(y0)), a) -> c3(F(g(g(y0)), a)) H(g(a), g(y0), g(a)) -> c3(F(g(y0), g(a))) H(g(a), g(y0), g(g(g(y1)))) -> c3(F(g(y0), g(g(g(y1))))) H(g(a), g(y0), g(g(a))) -> c3(F(g(y0), g(g(a)))) S tuples: H(g(g(g(z0))), z1, z2) -> c3(F(z1, f(z1, f(z1, h(z0, z1, z2)))), H(g(g(z0)), z1, z2)) H(g(g(a)), z0, z1) -> c3(F(z0, f(z0, z1)), H(g(a), z0, z1)) F(g(z0), g(a)) -> c2(H(g(a), z0, g(a))) F(g(z0), g(g(g(y0)))) -> c2(H(g(g(g(y0))), z0, g(g(g(y0))))) F(g(z0), g(g(a))) -> c2(H(g(g(a)), z0, g(g(a)))) H(g(a), g(g(y0)), a) -> c3(F(g(g(y0)), a)) H(g(a), g(y0), g(a)) -> c3(F(g(y0), g(a))) H(g(a), g(y0), g(g(g(y1)))) -> c3(F(g(y0), g(g(g(y1))))) H(g(a), g(y0), g(g(a))) -> c3(F(g(y0), g(g(a)))) K tuples: F(g(g(y0)), a) -> c1(F(g(y0), g(a))) Defined Rule Symbols: f_2, h_3 Defined Pair Symbols: H_3, F_2 Compound Symbols: c3_2, c1_1, c2_1, c3_1 ---------------------------------------- (39) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1))) Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S. H(g(a), g(g(y0)), a) -> c3(F(g(g(y0)), a)) We considered the (Usable) Rules:none And the Tuples: H(g(g(g(z0))), z1, z2) -> c3(F(z1, f(z1, f(z1, h(z0, z1, z2)))), H(g(g(z0)), z1, z2)) H(g(g(a)), z0, z1) -> c3(F(z0, f(z0, z1)), H(g(a), z0, z1)) F(g(g(y0)), a) -> c1(F(g(y0), g(a))) F(g(z0), g(a)) -> c2(H(g(a), z0, g(a))) F(g(z0), g(g(g(y0)))) -> c2(H(g(g(g(y0))), z0, g(g(g(y0))))) F(g(z0), g(g(a))) -> c2(H(g(g(a)), z0, g(g(a)))) H(g(a), g(g(y0)), a) -> c3(F(g(g(y0)), a)) H(g(a), g(y0), g(a)) -> c3(F(g(y0), g(a))) H(g(a), g(y0), g(g(g(y1)))) -> c3(F(g(y0), g(g(g(y1))))) H(g(a), g(y0), g(g(a))) -> c3(F(g(y0), g(g(a)))) The order we found is given by the following interpretation: Polynomial interpretation : POL(F(x_1, x_2)) = 0 POL(H(x_1, x_2, x_3)) = x_3 POL(a) = [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(f(x_1, x_2)) = [3] POL(g(x_1)) = 0 POL(h(x_1, x_2, x_3)) = [3] + [3]x_2 ---------------------------------------- (40) Obligation: Complexity Dependency Tuples Problem Rules: f(a, g(z0)) -> g(g(z0)) f(g(z0), a) -> f(z0, g(a)) f(g(z0), g(z1)) -> h(g(z1), z0, g(z1)) h(g(z0), z1, z2) -> f(z1, h(z0, z1, z2)) h(a, z0, z1) -> z1 Tuples: H(g(g(g(z0))), z1, z2) -> c3(F(z1, f(z1, f(z1, h(z0, z1, z2)))), H(g(g(z0)), z1, z2)) H(g(g(a)), z0, z1) -> c3(F(z0, f(z0, z1)), H(g(a), z0, z1)) F(g(g(y0)), a) -> c1(F(g(y0), g(a))) F(g(z0), g(a)) -> c2(H(g(a), z0, g(a))) F(g(z0), g(g(g(y0)))) -> c2(H(g(g(g(y0))), z0, g(g(g(y0))))) F(g(z0), g(g(a))) -> c2(H(g(g(a)), z0, g(g(a)))) H(g(a), g(g(y0)), a) -> c3(F(g(g(y0)), a)) H(g(a), g(y0), g(a)) -> c3(F(g(y0), g(a))) H(g(a), g(y0), g(g(g(y1)))) -> c3(F(g(y0), g(g(g(y1))))) H(g(a), g(y0), g(g(a))) -> c3(F(g(y0), g(g(a)))) S tuples: H(g(g(g(z0))), z1, z2) -> c3(F(z1, f(z1, f(z1, h(z0, z1, z2)))), H(g(g(z0)), z1, z2)) H(g(g(a)), z0, z1) -> c3(F(z0, f(z0, z1)), H(g(a), z0, z1)) F(g(z0), g(a)) -> c2(H(g(a), z0, g(a))) F(g(z0), g(g(g(y0)))) -> c2(H(g(g(g(y0))), z0, g(g(g(y0))))) F(g(z0), g(g(a))) -> c2(H(g(g(a)), z0, g(g(a)))) H(g(a), g(y0), g(a)) -> c3(F(g(y0), g(a))) H(g(a), g(y0), g(g(g(y1)))) -> c3(F(g(y0), g(g(g(y1))))) H(g(a), g(y0), g(g(a))) -> c3(F(g(y0), g(g(a)))) K tuples: F(g(g(y0)), a) -> c1(F(g(y0), g(a))) H(g(a), g(g(y0)), a) -> c3(F(g(g(y0)), a)) Defined Rule Symbols: f_2, h_3 Defined Pair Symbols: H_3, F_2 Compound Symbols: c3_2, c1_1, c2_1, c3_1 ---------------------------------------- (41) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID)) Use forward instantiation to replace F(g(z0), g(a)) -> c2(H(g(a), z0, g(a))) by F(g(g(y0)), g(a)) -> c2(H(g(a), g(y0), g(a))) ---------------------------------------- (42) Obligation: Complexity Dependency Tuples Problem Rules: f(a, g(z0)) -> g(g(z0)) f(g(z0), a) -> f(z0, g(a)) f(g(z0), g(z1)) -> h(g(z1), z0, g(z1)) h(g(z0), z1, z2) -> f(z1, h(z0, z1, z2)) h(a, z0, z1) -> z1 Tuples: H(g(g(g(z0))), z1, z2) -> c3(F(z1, f(z1, f(z1, h(z0, z1, z2)))), H(g(g(z0)), z1, z2)) H(g(g(a)), z0, z1) -> c3(F(z0, f(z0, z1)), H(g(a), z0, z1)) F(g(g(y0)), a) -> c1(F(g(y0), g(a))) F(g(z0), g(g(g(y0)))) -> c2(H(g(g(g(y0))), z0, g(g(g(y0))))) F(g(z0), g(g(a))) -> c2(H(g(g(a)), z0, g(g(a)))) H(g(a), g(g(y0)), a) -> c3(F(g(g(y0)), a)) H(g(a), g(y0), g(a)) -> c3(F(g(y0), g(a))) H(g(a), g(y0), g(g(g(y1)))) -> c3(F(g(y0), g(g(g(y1))))) H(g(a), g(y0), g(g(a))) -> c3(F(g(y0), g(g(a)))) F(g(g(y0)), g(a)) -> c2(H(g(a), g(y0), g(a))) S tuples: H(g(g(g(z0))), z1, z2) -> c3(F(z1, f(z1, f(z1, h(z0, z1, z2)))), H(g(g(z0)), z1, z2)) H(g(g(a)), z0, z1) -> c3(F(z0, f(z0, z1)), H(g(a), z0, z1)) F(g(z0), g(g(g(y0)))) -> c2(H(g(g(g(y0))), z0, g(g(g(y0))))) F(g(z0), g(g(a))) -> c2(H(g(g(a)), z0, g(g(a)))) H(g(a), g(y0), g(a)) -> c3(F(g(y0), g(a))) H(g(a), g(y0), g(g(g(y1)))) -> c3(F(g(y0), g(g(g(y1))))) H(g(a), g(y0), g(g(a))) -> c3(F(g(y0), g(g(a)))) F(g(g(y0)), g(a)) -> c2(H(g(a), g(y0), g(a))) K tuples: F(g(g(y0)), a) -> c1(F(g(y0), g(a))) H(g(a), g(g(y0)), a) -> c3(F(g(g(y0)), a)) Defined Rule Symbols: f_2, h_3 Defined Pair Symbols: H_3, F_2 Compound Symbols: c3_2, c1_1, c2_1, c3_1 ---------------------------------------- (43) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID)) Use forward instantiation to replace F(g(g(y0)), a) -> c1(F(g(y0), g(a))) by F(g(g(g(y0))), a) -> c1(F(g(g(y0)), g(a))) ---------------------------------------- (44) Obligation: Complexity Dependency Tuples Problem Rules: f(a, g(z0)) -> g(g(z0)) f(g(z0), a) -> f(z0, g(a)) f(g(z0), g(z1)) -> h(g(z1), z0, g(z1)) h(g(z0), z1, z2) -> f(z1, h(z0, z1, z2)) h(a, z0, z1) -> z1 Tuples: H(g(g(g(z0))), z1, z2) -> c3(F(z1, f(z1, f(z1, h(z0, z1, z2)))), H(g(g(z0)), z1, z2)) H(g(g(a)), z0, z1) -> c3(F(z0, f(z0, z1)), H(g(a), z0, z1)) F(g(z0), g(g(g(y0)))) -> c2(H(g(g(g(y0))), z0, g(g(g(y0))))) F(g(z0), g(g(a))) -> c2(H(g(g(a)), z0, g(g(a)))) H(g(a), g(g(y0)), a) -> c3(F(g(g(y0)), a)) H(g(a), g(y0), g(a)) -> c3(F(g(y0), g(a))) H(g(a), g(y0), g(g(g(y1)))) -> c3(F(g(y0), g(g(g(y1))))) H(g(a), g(y0), g(g(a))) -> c3(F(g(y0), g(g(a)))) F(g(g(y0)), g(a)) -> c2(H(g(a), g(y0), g(a))) F(g(g(g(y0))), a) -> c1(F(g(g(y0)), g(a))) S tuples: H(g(g(g(z0))), z1, z2) -> c3(F(z1, f(z1, f(z1, h(z0, z1, z2)))), H(g(g(z0)), z1, z2)) H(g(g(a)), z0, z1) -> c3(F(z0, f(z0, z1)), H(g(a), z0, z1)) F(g(z0), g(g(g(y0)))) -> c2(H(g(g(g(y0))), z0, g(g(g(y0))))) F(g(z0), g(g(a))) -> c2(H(g(g(a)), z0, g(g(a)))) H(g(a), g(y0), g(a)) -> c3(F(g(y0), g(a))) H(g(a), g(y0), g(g(g(y1)))) -> c3(F(g(y0), g(g(g(y1))))) H(g(a), g(y0), g(g(a))) -> c3(F(g(y0), g(g(a)))) F(g(g(y0)), g(a)) -> c2(H(g(a), g(y0), g(a))) K tuples: H(g(a), g(g(y0)), a) -> c3(F(g(g(y0)), a)) F(g(g(g(y0))), a) -> c1(F(g(g(y0)), g(a))) Defined Rule Symbols: f_2, h_3 Defined Pair Symbols: H_3, F_2 Compound Symbols: c3_2, c2_1, c3_1, c1_1 ---------------------------------------- (45) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID)) Use forward instantiation to replace H(g(a), g(g(y0)), a) -> c3(F(g(g(y0)), a)) by H(g(a), g(g(g(y0))), a) -> c3(F(g(g(g(y0))), a)) ---------------------------------------- (46) Obligation: Complexity Dependency Tuples Problem Rules: f(a, g(z0)) -> g(g(z0)) f(g(z0), a) -> f(z0, g(a)) f(g(z0), g(z1)) -> h(g(z1), z0, g(z1)) h(g(z0), z1, z2) -> f(z1, h(z0, z1, z2)) h(a, z0, z1) -> z1 Tuples: H(g(g(g(z0))), z1, z2) -> c3(F(z1, f(z1, f(z1, h(z0, z1, z2)))), H(g(g(z0)), z1, z2)) H(g(g(a)), z0, z1) -> c3(F(z0, f(z0, z1)), H(g(a), z0, z1)) F(g(z0), g(g(g(y0)))) -> c2(H(g(g(g(y0))), z0, g(g(g(y0))))) F(g(z0), g(g(a))) -> c2(H(g(g(a)), z0, g(g(a)))) H(g(a), g(y0), g(a)) -> c3(F(g(y0), g(a))) H(g(a), g(y0), g(g(g(y1)))) -> c3(F(g(y0), g(g(g(y1))))) H(g(a), g(y0), g(g(a))) -> c3(F(g(y0), g(g(a)))) F(g(g(y0)), g(a)) -> c2(H(g(a), g(y0), g(a))) F(g(g(g(y0))), a) -> c1(F(g(g(y0)), g(a))) H(g(a), g(g(g(y0))), a) -> c3(F(g(g(g(y0))), a)) S tuples: H(g(g(g(z0))), z1, z2) -> c3(F(z1, f(z1, f(z1, h(z0, z1, z2)))), H(g(g(z0)), z1, z2)) H(g(g(a)), z0, z1) -> c3(F(z0, f(z0, z1)), H(g(a), z0, z1)) F(g(z0), g(g(g(y0)))) -> c2(H(g(g(g(y0))), z0, g(g(g(y0))))) F(g(z0), g(g(a))) -> c2(H(g(g(a)), z0, g(g(a)))) H(g(a), g(y0), g(a)) -> c3(F(g(y0), g(a))) H(g(a), g(y0), g(g(g(y1)))) -> c3(F(g(y0), g(g(g(y1))))) H(g(a), g(y0), g(g(a))) -> c3(F(g(y0), g(g(a)))) F(g(g(y0)), g(a)) -> c2(H(g(a), g(y0), g(a))) K tuples: F(g(g(g(y0))), a) -> c1(F(g(g(y0)), g(a))) H(g(a), g(g(g(y0))), a) -> c3(F(g(g(g(y0))), a)) Defined Rule Symbols: f_2, h_3 Defined Pair Symbols: H_3, F_2 Compound Symbols: c3_2, c2_1, c3_1, c1_1 ---------------------------------------- (47) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID)) Use forward instantiation to replace H(g(a), g(y0), g(a)) -> c3(F(g(y0), g(a))) by H(g(a), g(g(y0)), g(a)) -> c3(F(g(g(y0)), g(a))) ---------------------------------------- (48) Obligation: Complexity Dependency Tuples Problem Rules: f(a, g(z0)) -> g(g(z0)) f(g(z0), a) -> f(z0, g(a)) f(g(z0), g(z1)) -> h(g(z1), z0, g(z1)) h(g(z0), z1, z2) -> f(z1, h(z0, z1, z2)) h(a, z0, z1) -> z1 Tuples: H(g(g(g(z0))), z1, z2) -> c3(F(z1, f(z1, f(z1, h(z0, z1, z2)))), H(g(g(z0)), z1, z2)) H(g(g(a)), z0, z1) -> c3(F(z0, f(z0, z1)), H(g(a), z0, z1)) F(g(z0), g(g(g(y0)))) -> c2(H(g(g(g(y0))), z0, g(g(g(y0))))) F(g(z0), g(g(a))) -> c2(H(g(g(a)), z0, g(g(a)))) H(g(a), g(y0), g(g(g(y1)))) -> c3(F(g(y0), g(g(g(y1))))) H(g(a), g(y0), g(g(a))) -> c3(F(g(y0), g(g(a)))) F(g(g(y0)), g(a)) -> c2(H(g(a), g(y0), g(a))) F(g(g(g(y0))), a) -> c1(F(g(g(y0)), g(a))) H(g(a), g(g(g(y0))), a) -> c3(F(g(g(g(y0))), a)) H(g(a), g(g(y0)), g(a)) -> c3(F(g(g(y0)), g(a))) S tuples: H(g(g(g(z0))), z1, z2) -> c3(F(z1, f(z1, f(z1, h(z0, z1, z2)))), H(g(g(z0)), z1, z2)) H(g(g(a)), z0, z1) -> c3(F(z0, f(z0, z1)), H(g(a), z0, z1)) F(g(z0), g(g(g(y0)))) -> c2(H(g(g(g(y0))), z0, g(g(g(y0))))) F(g(z0), g(g(a))) -> c2(H(g(g(a)), z0, g(g(a)))) H(g(a), g(y0), g(g(g(y1)))) -> c3(F(g(y0), g(g(g(y1))))) H(g(a), g(y0), g(g(a))) -> c3(F(g(y0), g(g(a)))) F(g(g(y0)), g(a)) -> c2(H(g(a), g(y0), g(a))) H(g(a), g(g(y0)), g(a)) -> c3(F(g(g(y0)), g(a))) K tuples: F(g(g(g(y0))), a) -> c1(F(g(g(y0)), g(a))) H(g(a), g(g(g(y0))), a) -> c3(F(g(g(g(y0))), a)) Defined Rule Symbols: f_2, h_3 Defined Pair Symbols: H_3, F_2 Compound Symbols: c3_2, c2_1, c3_1, c1_1