MAYBE proof of input_MrCh5JFMOh.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) CpxTrsToCdtProof [UPPER BOUND(ID), 0 ms] (6) CdtProblem (7) CdtToCpxRelTrsProof [BOTH BOUNDS(ID, ID), 0 ms] (8) CpxRelTRS (9) RelTrsToDecreasingLoopProblemProof [LOWER BOUND(ID), 0 ms] (10) TRS for Loop Detection (11) RenamingProof [BOTH BOUNDS(ID, ID), 0 ms] (12) CpxRelTRS (13) TypeInferenceProof [BOTH BOUNDS(ID, ID), 0 ms] (14) typed CpxTrs (15) OrderProof [LOWER BOUND(ID), 19 ms] (16) typed CpxTrs (17) CpxTrsToCdtProof [UPPER BOUND(ID), 0 ms] (18) CdtProblem (19) CdtLeafRemovalProof [BOTH BOUNDS(ID, ID), 0 ms] (20) CdtProblem (21) CdtToCpxRelTrsProof [BOTH BOUNDS(ID, ID), 0 ms] (22) CpxRelTRS (23) RelTrsToTrsProof [UPPER BOUND(ID), 0 ms] (24) CpxTRS (25) RelTrsToWeightedTrsProof [BOTH BOUNDS(ID, ID), 0 ms] (26) CpxWeightedTrs (27) TypeInferenceProof [BOTH BOUNDS(ID, ID), 0 ms] (28) CpxTypedWeightedTrs (29) CompletionProof [UPPER BOUND(ID), 0 ms] (30) CpxTypedWeightedCompleteTrs (31) NarrowingProof [BOTH BOUNDS(ID, ID), 0 ms] (32) CpxTypedWeightedCompleteTrs (33) CpxTypedWeightedTrsToRntsProof [UPPER BOUND(ID), 0 ms] (34) CpxRNTS (35) SimplificationProof [BOTH BOUNDS(ID, ID), 0 ms] (36) CpxRNTS (37) CompletionProof [UPPER BOUND(ID), 0 ms] (38) CpxTypedWeightedCompleteTrs (39) CpxTypedWeightedTrsToRntsProof [UPPER BOUND(ID), 0 ms] (40) CpxRNTS (41) CdtNarrowingProof [BOTH BOUNDS(ID, ID), 0 ms] (42) CdtProblem (43) CdtNarrowingProof [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 (49) CdtForwardInstantiationProof [BOTH BOUNDS(ID, ID), 0 ms] (50) CdtProblem (51) CdtForwardInstantiationProof [BOTH BOUNDS(ID, ID), 0 ms] (52) CdtProblem (53) CdtForwardInstantiationProof [BOTH BOUNDS(ID, ID), 0 ms] (54) CdtProblem (55) CdtForwardInstantiationProof [BOTH BOUNDS(ID, ID), 0 ms] (56) CdtProblem (57) CdtForwardInstantiationProof [BOTH BOUNDS(ID, ID), 3 ms] (58) CdtProblem (59) CdtForwardInstantiationProof [BOTH BOUNDS(ID, ID), 20 ms] (60) CdtProblem (61) CdtForwardInstantiationProof [BOTH BOUNDS(ID, ID), 15 ms] (62) CdtProblem (63) RelTrsToWeightedTrsProof [UPPER BOUND(ID), 0 ms] (64) CpxWeightedTrs (65) TypeInferenceProof [BOTH BOUNDS(ID, ID), 0 ms] (66) CpxTypedWeightedTrs (67) CompletionProof [UPPER BOUND(ID), 0 ms] (68) CpxTypedWeightedCompleteTrs (69) NarrowingProof [BOTH BOUNDS(ID, ID), 0 ms] (70) CpxTypedWeightedCompleteTrs (71) CpxTypedWeightedTrsToRntsProof [UPPER BOUND(ID), 0 ms] (72) CpxRNTS (73) SimplificationProof [BOTH BOUNDS(ID, ID), 0 ms] (74) CpxRNTS (75) CompletionProof [UPPER BOUND(ID), 0 ms] (76) CpxTypedWeightedCompleteTrs (77) CpxTypedWeightedTrsToRntsProof [UPPER BOUND(ID), 0 ms] (78) CpxRNTS ---------------------------------------- (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(g(X), Y) -> f(X, n__f(g(X), activate(Y))) f(X1, X2) -> n__f(X1, X2) activate(n__f(X1, X2)) -> f(X1, X2) activate(X) -> X 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(g(X), Y) -> f(X, n__f(g(X), activate(Y))) f(X1, X2) -> n__f(X1, X2) activate(n__f(X1, X2)) -> f(X1, X2) activate(X) -> X 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(g(X), Y) -> f(X, n__f(g(X), activate(Y))) f(X1, X2) -> n__f(X1, X2) activate(n__f(X1, X2)) -> f(X1, X2) activate(X) -> X S is empty. Rewrite Strategy: PARALLEL_INNERMOST ---------------------------------------- (5) CpxTrsToCdtProof (UPPER BOUND(ID)) Converted Cpx (relative) TRS with rewrite strategy PARALLEL_INNERMOST to CDT ---------------------------------------- (6) Obligation: Complexity Dependency Tuples Problem Rules: f(g(z0), z1) -> f(z0, n__f(g(z0), activate(z1))) f(z0, z1) -> n__f(z0, z1) activate(n__f(z0, z1)) -> f(z0, z1) activate(z0) -> z0 Tuples: F(g(z0), z1) -> c(F(z0, n__f(g(z0), activate(z1))), ACTIVATE(z1)) F(z0, z1) -> c1 ACTIVATE(n__f(z0, z1)) -> c2(F(z0, z1)) ACTIVATE(z0) -> c3 S tuples: F(g(z0), z1) -> c(F(z0, n__f(g(z0), activate(z1))), ACTIVATE(z1)) F(z0, z1) -> c1 ACTIVATE(n__f(z0, z1)) -> c2(F(z0, z1)) ACTIVATE(z0) -> c3 K tuples:none Defined Rule Symbols: f_2, activate_1 Defined Pair Symbols: F_2, ACTIVATE_1 Compound Symbols: c_2, c1, c2_1, c3 ---------------------------------------- (7) CdtToCpxRelTrsProof (BOTH BOUNDS(ID, ID)) Converted S to standard rules, and D \ S as well as R to relative rules. ---------------------------------------- (8) Obligation: The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(1, INF). The TRS R consists of the following rules: F(g(z0), z1) -> c(F(z0, n__f(g(z0), activate(z1))), ACTIVATE(z1)) F(z0, z1) -> c1 ACTIVATE(n__f(z0, z1)) -> c2(F(z0, z1)) ACTIVATE(z0) -> c3 The (relative) TRS S consists of the following rules: f(g(z0), z1) -> f(z0, n__f(g(z0), activate(z1))) f(z0, z1) -> n__f(z0, z1) activate(n__f(z0, z1)) -> f(z0, z1) activate(z0) -> z0 Rewrite Strategy: INNERMOST ---------------------------------------- (9) RelTrsToDecreasingLoopProblemProof (LOWER BOUND(ID)) Transformed a relative TRS into a decreasing-loop problem. ---------------------------------------- (10) Obligation: Analyzing the following TRS for decreasing loops: The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(1, INF). The TRS R consists of the following rules: F(g(z0), z1) -> c(F(z0, n__f(g(z0), activate(z1))), ACTIVATE(z1)) F(z0, z1) -> c1 ACTIVATE(n__f(z0, z1)) -> c2(F(z0, z1)) ACTIVATE(z0) -> c3 The (relative) TRS S consists of the following rules: f(g(z0), z1) -> f(z0, n__f(g(z0), activate(z1))) f(z0, z1) -> n__f(z0, z1) activate(n__f(z0, z1)) -> f(z0, z1) activate(z0) -> z0 Rewrite Strategy: INNERMOST ---------------------------------------- (11) RenamingProof (BOTH BOUNDS(ID, ID)) Renamed function symbols to avoid clashes with predefined symbol. ---------------------------------------- (12) Obligation: The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(1, INF). The TRS R consists of the following rules: F(g(z0), z1) -> c(F(z0, n__f(g(z0), activate(z1))), ACTIVATE(z1)) F(z0, z1) -> c1 ACTIVATE(n__f(z0, z1)) -> c2(F(z0, z1)) ACTIVATE(z0) -> c3 The (relative) TRS S consists of the following rules: f(g(z0), z1) -> f(z0, n__f(g(z0), activate(z1))) f(z0, z1) -> n__f(z0, z1) activate(n__f(z0, z1)) -> f(z0, z1) activate(z0) -> z0 Rewrite Strategy: INNERMOST ---------------------------------------- (13) TypeInferenceProof (BOTH BOUNDS(ID, ID)) Inferred types. ---------------------------------------- (14) Obligation: Innermost TRS: Rules: F(g(z0), z1) -> c(F(z0, n__f(g(z0), activate(z1))), ACTIVATE(z1)) F(z0, z1) -> c1 ACTIVATE(n__f(z0, z1)) -> c2(F(z0, z1)) ACTIVATE(z0) -> c3 f(g(z0), z1) -> f(z0, n__f(g(z0), activate(z1))) f(z0, z1) -> n__f(z0, z1) activate(n__f(z0, z1)) -> f(z0, z1) activate(z0) -> z0 Types: F :: g -> n__f -> c:c1 g :: g -> g c :: c:c1 -> c2:c3 -> c:c1 n__f :: g -> n__f -> n__f activate :: n__f -> n__f ACTIVATE :: n__f -> c2:c3 c1 :: c:c1 c2 :: c:c1 -> c2:c3 c3 :: c2:c3 f :: g -> n__f -> n__f hole_c:c11_4 :: c:c1 hole_g2_4 :: g hole_n__f3_4 :: n__f hole_c2:c34_4 :: c2:c3 gen_c:c15_4 :: Nat -> c:c1 gen_g6_4 :: Nat -> g gen_n__f7_4 :: Nat -> n__f ---------------------------------------- (15) OrderProof (LOWER BOUND(ID)) Heuristically decided to analyse the following defined symbols: F, activate, ACTIVATE, f They will be analysed ascendingly in the following order: activate < F F = ACTIVATE activate = f ---------------------------------------- (16) Obligation: Innermost TRS: Rules: F(g(z0), z1) -> c(F(z0, n__f(g(z0), activate(z1))), ACTIVATE(z1)) F(z0, z1) -> c1 ACTIVATE(n__f(z0, z1)) -> c2(F(z0, z1)) ACTIVATE(z0) -> c3 f(g(z0), z1) -> f(z0, n__f(g(z0), activate(z1))) f(z0, z1) -> n__f(z0, z1) activate(n__f(z0, z1)) -> f(z0, z1) activate(z0) -> z0 Types: F :: g -> n__f -> c:c1 g :: g -> g c :: c:c1 -> c2:c3 -> c:c1 n__f :: g -> n__f -> n__f activate :: n__f -> n__f ACTIVATE :: n__f -> c2:c3 c1 :: c:c1 c2 :: c:c1 -> c2:c3 c3 :: c2:c3 f :: g -> n__f -> n__f hole_c:c11_4 :: c:c1 hole_g2_4 :: g hole_n__f3_4 :: n__f hole_c2:c34_4 :: c2:c3 gen_c:c15_4 :: Nat -> c:c1 gen_g6_4 :: Nat -> g gen_n__f7_4 :: Nat -> n__f Generator Equations: gen_c:c15_4(0) <=> c1 gen_c:c15_4(+(x, 1)) <=> c(gen_c:c15_4(x), c2(c1)) gen_g6_4(0) <=> hole_g2_4 gen_g6_4(+(x, 1)) <=> g(gen_g6_4(x)) gen_n__f7_4(0) <=> hole_n__f3_4 gen_n__f7_4(+(x, 1)) <=> n__f(hole_g2_4, gen_n__f7_4(x)) The following defined symbols remain to be analysed: f, F, activate, ACTIVATE They will be analysed ascendingly in the following order: activate < F F = ACTIVATE activate = f ---------------------------------------- (17) CpxTrsToCdtProof (UPPER BOUND(ID)) Converted Cpx (relative) TRS with rewrite strategy PARALLEL_INNERMOST to CDT ---------------------------------------- (18) Obligation: Complexity Dependency Tuples Problem Rules: f(g(z0), z1) -> f(z0, n__f(g(z0), activate(z1))) f(z0, z1) -> n__f(z0, z1) activate(n__f(z0, z1)) -> f(z0, z1) activate(z0) -> z0 Tuples: F(g(z0), z1) -> c(F(z0, n__f(g(z0), activate(z1))), ACTIVATE(z1)) F(z0, z1) -> c1 ACTIVATE(n__f(z0, z1)) -> c2(F(z0, z1)) ACTIVATE(z0) -> c3 S tuples: F(g(z0), z1) -> c(F(z0, n__f(g(z0), activate(z1))), ACTIVATE(z1)) F(z0, z1) -> c1 ACTIVATE(n__f(z0, z1)) -> c2(F(z0, z1)) ACTIVATE(z0) -> c3 K tuples:none Defined Rule Symbols: f_2, activate_1 Defined Pair Symbols: F_2, ACTIVATE_1 Compound Symbols: c_2, c1, c2_1, c3 ---------------------------------------- (19) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID)) Removed 2 trailing nodes: ACTIVATE(z0) -> c3 F(z0, z1) -> c1 ---------------------------------------- (20) Obligation: Complexity Dependency Tuples Problem Rules: f(g(z0), z1) -> f(z0, n__f(g(z0), activate(z1))) f(z0, z1) -> n__f(z0, z1) activate(n__f(z0, z1)) -> f(z0, z1) activate(z0) -> z0 Tuples: F(g(z0), z1) -> c(F(z0, n__f(g(z0), activate(z1))), ACTIVATE(z1)) ACTIVATE(n__f(z0, z1)) -> c2(F(z0, z1)) S tuples: F(g(z0), z1) -> c(F(z0, n__f(g(z0), activate(z1))), ACTIVATE(z1)) ACTIVATE(n__f(z0, z1)) -> c2(F(z0, z1)) K tuples:none Defined Rule Symbols: f_2, activate_1 Defined Pair Symbols: F_2, ACTIVATE_1 Compound Symbols: c_2, c2_1 ---------------------------------------- (21) CdtToCpxRelTrsProof (BOTH BOUNDS(ID, ID)) Converted S to standard rules, and D \ S as well as R to relative rules. ---------------------------------------- (22) Obligation: The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(1, INF). The TRS R consists of the following rules: F(g(z0), z1) -> c(F(z0, n__f(g(z0), activate(z1))), ACTIVATE(z1)) ACTIVATE(n__f(z0, z1)) -> c2(F(z0, z1)) The (relative) TRS S consists of the following rules: f(g(z0), z1) -> f(z0, n__f(g(z0), activate(z1))) f(z0, z1) -> n__f(z0, z1) activate(n__f(z0, z1)) -> f(z0, z1) activate(z0) -> z0 Rewrite Strategy: INNERMOST ---------------------------------------- (23) RelTrsToTrsProof (UPPER BOUND(ID)) transformed relative TRS to TRS ---------------------------------------- (24) Obligation: The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(1, INF). The TRS R consists of the following rules: F(g(z0), z1) -> c(F(z0, n__f(g(z0), activate(z1))), ACTIVATE(z1)) ACTIVATE(n__f(z0, z1)) -> c2(F(z0, z1)) f(g(z0), z1) -> f(z0, n__f(g(z0), activate(z1))) f(z0, z1) -> n__f(z0, z1) activate(n__f(z0, z1)) -> f(z0, z1) activate(z0) -> z0 S is empty. Rewrite Strategy: INNERMOST ---------------------------------------- (25) RelTrsToWeightedTrsProof (BOTH BOUNDS(ID, ID)) Transformed relative TRS to weighted TRS ---------------------------------------- (26) 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(g(z0), z1) -> c(F(z0, n__f(g(z0), activate(z1))), ACTIVATE(z1)) [1] ACTIVATE(n__f(z0, z1)) -> c2(F(z0, z1)) [1] f(g(z0), z1) -> f(z0, n__f(g(z0), activate(z1))) [0] f(z0, z1) -> n__f(z0, z1) [0] activate(n__f(z0, z1)) -> f(z0, z1) [0] activate(z0) -> z0 [0] Rewrite Strategy: INNERMOST ---------------------------------------- (27) TypeInferenceProof (BOTH BOUNDS(ID, ID)) Infered types. ---------------------------------------- (28) Obligation: Runtime Complexity Weighted TRS with Types. The TRS R consists of the following rules: F(g(z0), z1) -> c(F(z0, n__f(g(z0), activate(z1))), ACTIVATE(z1)) [1] ACTIVATE(n__f(z0, z1)) -> c2(F(z0, z1)) [1] f(g(z0), z1) -> f(z0, n__f(g(z0), activate(z1))) [0] f(z0, z1) -> n__f(z0, z1) [0] activate(n__f(z0, z1)) -> f(z0, z1) [0] activate(z0) -> z0 [0] The TRS has the following type information: F :: g -> n__f -> c g :: g -> g c :: c -> c2 -> c n__f :: g -> n__f -> n__f activate :: n__f -> n__f ACTIVATE :: n__f -> c2 c2 :: c -> c2 f :: g -> n__f -> n__f Rewrite Strategy: INNERMOST ---------------------------------------- (29) 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: F_2 ACTIVATE_1 (c) The following functions are completely defined: f_2 activate_1 Due to the following rules being added: f(v0, v1) -> const2 [0] activate(v0) -> const2 [0] And the following fresh constants: const2, const, const1, const3 ---------------------------------------- (30) 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(g(z0), z1) -> c(F(z0, n__f(g(z0), activate(z1))), ACTIVATE(z1)) [1] ACTIVATE(n__f(z0, z1)) -> c2(F(z0, z1)) [1] f(g(z0), z1) -> f(z0, n__f(g(z0), activate(z1))) [0] f(z0, z1) -> n__f(z0, z1) [0] activate(n__f(z0, z1)) -> f(z0, z1) [0] activate(z0) -> z0 [0] f(v0, v1) -> const2 [0] activate(v0) -> const2 [0] The TRS has the following type information: F :: g -> n__f:const2 -> c g :: g -> g c :: c -> c2 -> c n__f :: g -> n__f:const2 -> n__f:const2 activate :: n__f:const2 -> n__f:const2 ACTIVATE :: n__f:const2 -> c2 c2 :: c -> c2 f :: g -> n__f:const2 -> n__f:const2 const2 :: n__f:const2 const :: c const1 :: g const3 :: c2 Rewrite Strategy: INNERMOST ---------------------------------------- (31) NarrowingProof (BOTH BOUNDS(ID, ID)) Narrowed the inner basic terms of all right-hand sides by a single narrowing step. ---------------------------------------- (32) 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(g(z0), n__f(z0', z1')) -> c(F(z0, n__f(g(z0), f(z0', z1'))), ACTIVATE(n__f(z0', z1'))) [1] F(g(z0), z1) -> c(F(z0, n__f(g(z0), z1)), ACTIVATE(z1)) [1] F(g(z0), z1) -> c(F(z0, n__f(g(z0), const2)), ACTIVATE(z1)) [1] ACTIVATE(n__f(z0, z1)) -> c2(F(z0, z1)) [1] f(g(z0), n__f(z0'', z1'')) -> f(z0, n__f(g(z0), f(z0'', z1''))) [0] f(g(z0), z1) -> f(z0, n__f(g(z0), z1)) [0] f(g(z0), z1) -> f(z0, n__f(g(z0), const2)) [0] f(z0, z1) -> n__f(z0, z1) [0] activate(n__f(z0, z1)) -> f(z0, z1) [0] activate(z0) -> z0 [0] f(v0, v1) -> const2 [0] activate(v0) -> const2 [0] The TRS has the following type information: F :: g -> n__f:const2 -> c g :: g -> g c :: c -> c2 -> c n__f :: g -> n__f:const2 -> n__f:const2 activate :: n__f:const2 -> n__f:const2 ACTIVATE :: n__f:const2 -> c2 c2 :: c -> c2 f :: g -> n__f:const2 -> n__f:const2 const2 :: n__f:const2 const :: c const1 :: g const3 :: c2 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: const2 => 0 const => 0 const1 => 0 const3 => 0 ---------------------------------------- (34) Obligation: Complexity RNTS consisting of the following rules: ACTIVATE(z) -{ 1 }-> 1 + F(z0, z1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1 F(z, z') -{ 1 }-> 1 + F(z0, 1 + (1 + z0) + z1) + ACTIVATE(z1) :|: z1 >= 0, z = 1 + z0, z' = z1, z0 >= 0 F(z, z') -{ 1 }-> 1 + F(z0, 1 + (1 + z0) + f(z0', z1')) + ACTIVATE(1 + z0' + z1') :|: z0' >= 0, z = 1 + z0, z1' >= 0, z0 >= 0, z' = 1 + z0' + z1' F(z, z') -{ 1 }-> 1 + F(z0, 1 + (1 + z0) + 0) + ACTIVATE(z1) :|: z1 >= 0, z = 1 + z0, z' = z1, z0 >= 0 activate(z) -{ 0 }-> z0 :|: z = z0, z0 >= 0 activate(z) -{ 0 }-> f(z0, z1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1 activate(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0 f(z, z') -{ 0 }-> f(z0, 1 + (1 + z0) + z1) :|: z1 >= 0, z = 1 + z0, z' = z1, z0 >= 0 f(z, z') -{ 0 }-> f(z0, 1 + (1 + z0) + f(z0'', z1'')) :|: z = 1 + z0, z0 >= 0, z0'' >= 0, z' = 1 + z0'' + z1'', z1'' >= 0 f(z, z') -{ 0 }-> f(z0, 1 + (1 + z0) + 0) :|: z1 >= 0, z = 1 + z0, z' = z1, z0 >= 0 f(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1 f(z, z') -{ 0 }-> 1 + z0 + z1 :|: z = z0, z1 >= 0, z' = z1, z0 >= 0 ---------------------------------------- (35) SimplificationProof (BOTH BOUNDS(ID, ID)) Simplified the RNTS by moving equalities from the constraints into the right-hand sides. ---------------------------------------- (36) Obligation: Complexity RNTS consisting of the following rules: ACTIVATE(z) -{ 1 }-> 1 + F(z0, z1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1 F(z, z') -{ 1 }-> 1 + F(z - 1, 1 + (1 + (z - 1)) + z') + ACTIVATE(z') :|: z' >= 0, z - 1 >= 0 F(z, z') -{ 1 }-> 1 + F(z - 1, 1 + (1 + (z - 1)) + f(z0', z1')) + ACTIVATE(1 + z0' + z1') :|: z0' >= 0, z1' >= 0, z - 1 >= 0, z' = 1 + z0' + z1' F(z, z') -{ 1 }-> 1 + F(z - 1, 1 + (1 + (z - 1)) + 0) + ACTIVATE(z') :|: z' >= 0, z - 1 >= 0 activate(z) -{ 0 }-> z :|: z >= 0 activate(z) -{ 0 }-> f(z0, z1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1 activate(z) -{ 0 }-> 0 :|: z >= 0 f(z, z') -{ 0 }-> f(z - 1, 1 + (1 + (z - 1)) + z') :|: z' >= 0, z - 1 >= 0 f(z, z') -{ 0 }-> f(z - 1, 1 + (1 + (z - 1)) + f(z0'', z1'')) :|: z - 1 >= 0, z0'' >= 0, z' = 1 + z0'' + z1'', z1'' >= 0 f(z, z') -{ 0 }-> f(z - 1, 1 + (1 + (z - 1)) + 0) :|: z' >= 0, z - 1 >= 0 f(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0 f(z, z') -{ 0 }-> 1 + z + z' :|: z' >= 0, z >= 0 ---------------------------------------- (37) 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] activate(v0) -> null_activate [0] F(v0, v1) -> null_F [0] ACTIVATE(v0) -> null_ACTIVATE [0] And the following fresh constants: null_f, null_activate, null_F, null_ACTIVATE, const ---------------------------------------- (38) 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(g(z0), z1) -> c(F(z0, n__f(g(z0), activate(z1))), ACTIVATE(z1)) [1] ACTIVATE(n__f(z0, z1)) -> c2(F(z0, z1)) [1] f(g(z0), z1) -> f(z0, n__f(g(z0), activate(z1))) [0] f(z0, z1) -> n__f(z0, z1) [0] activate(n__f(z0, z1)) -> f(z0, z1) [0] activate(z0) -> z0 [0] f(v0, v1) -> null_f [0] activate(v0) -> null_activate [0] F(v0, v1) -> null_F [0] ACTIVATE(v0) -> null_ACTIVATE [0] The TRS has the following type information: F :: g -> n__f:null_f:null_activate -> c:null_F g :: g -> g c :: c:null_F -> c2:null_ACTIVATE -> c:null_F n__f :: g -> n__f:null_f:null_activate -> n__f:null_f:null_activate activate :: n__f:null_f:null_activate -> n__f:null_f:null_activate ACTIVATE :: n__f:null_f:null_activate -> c2:null_ACTIVATE c2 :: c:null_F -> c2:null_ACTIVATE f :: g -> n__f:null_f:null_activate -> n__f:null_f:null_activate null_f :: n__f:null_f:null_activate null_activate :: n__f:null_f:null_activate null_F :: c:null_F null_ACTIVATE :: c2:null_ACTIVATE const :: g Rewrite Strategy: INNERMOST ---------------------------------------- (39) CpxTypedWeightedTrsToRntsProof (UPPER BOUND(ID)) Transformed the TRS into an over-approximating RNTS by (improved) Size Abstraction. The constant constructors are abstracted as follows: null_f => 0 null_activate => 0 null_F => 0 null_ACTIVATE => 0 const => 0 ---------------------------------------- (40) Obligation: Complexity RNTS consisting of the following rules: ACTIVATE(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0 ACTIVATE(z) -{ 1 }-> 1 + F(z0, z1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1 F(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1 F(z, z') -{ 1 }-> 1 + F(z0, 1 + (1 + z0) + activate(z1)) + ACTIVATE(z1) :|: z1 >= 0, z = 1 + z0, z' = z1, z0 >= 0 activate(z) -{ 0 }-> z0 :|: z = z0, z0 >= 0 activate(z) -{ 0 }-> f(z0, z1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1 activate(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0 f(z, z') -{ 0 }-> f(z0, 1 + (1 + z0) + activate(z1)) :|: z1 >= 0, z = 1 + z0, z' = z1, z0 >= 0 f(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1 f(z, z') -{ 0 }-> 1 + z0 + z1 :|: z = z0, z1 >= 0, z' = z1, z0 >= 0 Only complete derivations are relevant for the runtime complexity. ---------------------------------------- (41) CdtNarrowingProof (BOTH BOUNDS(ID, ID)) Use narrowing to replace F(g(z0), z1) -> c(F(z0, n__f(g(z0), activate(z1))), ACTIVATE(z1)) by F(g(x0), n__f(z0, z1)) -> c(F(x0, n__f(g(x0), f(z0, z1))), ACTIVATE(n__f(z0, z1))) F(g(x0), z0) -> c(F(x0, n__f(g(x0), z0)), ACTIVATE(z0)) ---------------------------------------- (42) Obligation: Complexity Dependency Tuples Problem Rules: f(g(z0), z1) -> f(z0, n__f(g(z0), activate(z1))) f(z0, z1) -> n__f(z0, z1) activate(n__f(z0, z1)) -> f(z0, z1) activate(z0) -> z0 Tuples: ACTIVATE(n__f(z0, z1)) -> c2(F(z0, z1)) F(g(x0), n__f(z0, z1)) -> c(F(x0, n__f(g(x0), f(z0, z1))), ACTIVATE(n__f(z0, z1))) F(g(x0), z0) -> c(F(x0, n__f(g(x0), z0)), ACTIVATE(z0)) S tuples: ACTIVATE(n__f(z0, z1)) -> c2(F(z0, z1)) F(g(x0), n__f(z0, z1)) -> c(F(x0, n__f(g(x0), f(z0, z1))), ACTIVATE(n__f(z0, z1))) F(g(x0), z0) -> c(F(x0, n__f(g(x0), z0)), ACTIVATE(z0)) K tuples:none Defined Rule Symbols: f_2, activate_1 Defined Pair Symbols: ACTIVATE_1, F_2 Compound Symbols: c2_1, c_2 ---------------------------------------- (43) CdtNarrowingProof (BOTH BOUNDS(ID, ID)) Use narrowing to replace F(g(x0), n__f(z0, z1)) -> c(F(x0, n__f(g(x0), f(z0, z1))), ACTIVATE(n__f(z0, z1))) by F(g(x0), n__f(g(z0), z1)) -> c(F(x0, n__f(g(x0), f(z0, n__f(g(z0), activate(z1))))), ACTIVATE(n__f(g(z0), z1))) F(g(x0), n__f(z0, z1)) -> c(F(x0, n__f(g(x0), n__f(z0, z1))), ACTIVATE(n__f(z0, z1))) ---------------------------------------- (44) Obligation: Complexity Dependency Tuples Problem Rules: f(g(z0), z1) -> f(z0, n__f(g(z0), activate(z1))) f(z0, z1) -> n__f(z0, z1) activate(n__f(z0, z1)) -> f(z0, z1) activate(z0) -> z0 Tuples: ACTIVATE(n__f(z0, z1)) -> c2(F(z0, z1)) F(g(x0), z0) -> c(F(x0, n__f(g(x0), z0)), ACTIVATE(z0)) F(g(x0), n__f(g(z0), z1)) -> c(F(x0, n__f(g(x0), f(z0, n__f(g(z0), activate(z1))))), ACTIVATE(n__f(g(z0), z1))) F(g(x0), n__f(z0, z1)) -> c(F(x0, n__f(g(x0), n__f(z0, z1))), ACTIVATE(n__f(z0, z1))) S tuples: ACTIVATE(n__f(z0, z1)) -> c2(F(z0, z1)) F(g(x0), z0) -> c(F(x0, n__f(g(x0), z0)), ACTIVATE(z0)) F(g(x0), n__f(g(z0), z1)) -> c(F(x0, n__f(g(x0), f(z0, n__f(g(z0), activate(z1))))), ACTIVATE(n__f(g(z0), z1))) F(g(x0), n__f(z0, z1)) -> c(F(x0, n__f(g(x0), n__f(z0, z1))), ACTIVATE(n__f(z0, z1))) K tuples:none Defined Rule Symbols: f_2, activate_1 Defined Pair Symbols: ACTIVATE_1, F_2 Compound Symbols: c2_1, c_2 ---------------------------------------- (45) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID)) Use forward instantiation to replace ACTIVATE(n__f(z0, z1)) -> c2(F(z0, z1)) by ACTIVATE(n__f(g(y0), z1)) -> c2(F(g(y0), z1)) ACTIVATE(n__f(g(y0), n__f(g(y1), y2))) -> c2(F(g(y0), n__f(g(y1), y2))) ACTIVATE(n__f(g(y0), n__f(y1, y2))) -> c2(F(g(y0), n__f(y1, y2))) ---------------------------------------- (46) Obligation: Complexity Dependency Tuples Problem Rules: f(g(z0), z1) -> f(z0, n__f(g(z0), activate(z1))) f(z0, z1) -> n__f(z0, z1) activate(n__f(z0, z1)) -> f(z0, z1) activate(z0) -> z0 Tuples: F(g(x0), z0) -> c(F(x0, n__f(g(x0), z0)), ACTIVATE(z0)) F(g(x0), n__f(g(z0), z1)) -> c(F(x0, n__f(g(x0), f(z0, n__f(g(z0), activate(z1))))), ACTIVATE(n__f(g(z0), z1))) F(g(x0), n__f(z0, z1)) -> c(F(x0, n__f(g(x0), n__f(z0, z1))), ACTIVATE(n__f(z0, z1))) ACTIVATE(n__f(g(y0), z1)) -> c2(F(g(y0), z1)) ACTIVATE(n__f(g(y0), n__f(g(y1), y2))) -> c2(F(g(y0), n__f(g(y1), y2))) ACTIVATE(n__f(g(y0), n__f(y1, y2))) -> c2(F(g(y0), n__f(y1, y2))) S tuples: F(g(x0), z0) -> c(F(x0, n__f(g(x0), z0)), ACTIVATE(z0)) F(g(x0), n__f(g(z0), z1)) -> c(F(x0, n__f(g(x0), f(z0, n__f(g(z0), activate(z1))))), ACTIVATE(n__f(g(z0), z1))) F(g(x0), n__f(z0, z1)) -> c(F(x0, n__f(g(x0), n__f(z0, z1))), ACTIVATE(n__f(z0, z1))) ACTIVATE(n__f(g(y0), z1)) -> c2(F(g(y0), z1)) ACTIVATE(n__f(g(y0), n__f(g(y1), y2))) -> c2(F(g(y0), n__f(g(y1), y2))) ACTIVATE(n__f(g(y0), n__f(y1, y2))) -> c2(F(g(y0), n__f(y1, y2))) K tuples:none Defined Rule Symbols: f_2, activate_1 Defined Pair Symbols: F_2, ACTIVATE_1 Compound Symbols: c_2, c2_1 ---------------------------------------- (47) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID)) Use forward instantiation to replace F(g(x0), z0) -> c(F(x0, n__f(g(x0), z0)), ACTIVATE(z0)) by F(g(g(y0)), z1) -> c(F(g(y0), n__f(g(g(y0)), z1)), ACTIVATE(z1)) F(g(z0), n__f(g(y0), y1)) -> c(F(z0, n__f(g(z0), n__f(g(y0), y1))), ACTIVATE(n__f(g(y0), y1))) F(g(z0), n__f(g(y0), n__f(g(y1), y2))) -> c(F(z0, n__f(g(z0), n__f(g(y0), n__f(g(y1), y2)))), ACTIVATE(n__f(g(y0), n__f(g(y1), y2)))) F(g(z0), n__f(g(y0), n__f(y1, y2))) -> c(F(z0, n__f(g(z0), n__f(g(y0), n__f(y1, y2)))), ACTIVATE(n__f(g(y0), n__f(y1, y2)))) ---------------------------------------- (48) Obligation: Complexity Dependency Tuples Problem Rules: f(g(z0), z1) -> f(z0, n__f(g(z0), activate(z1))) f(z0, z1) -> n__f(z0, z1) activate(n__f(z0, z1)) -> f(z0, z1) activate(z0) -> z0 Tuples: F(g(x0), n__f(g(z0), z1)) -> c(F(x0, n__f(g(x0), f(z0, n__f(g(z0), activate(z1))))), ACTIVATE(n__f(g(z0), z1))) F(g(x0), n__f(z0, z1)) -> c(F(x0, n__f(g(x0), n__f(z0, z1))), ACTIVATE(n__f(z0, z1))) ACTIVATE(n__f(g(y0), z1)) -> c2(F(g(y0), z1)) ACTIVATE(n__f(g(y0), n__f(g(y1), y2))) -> c2(F(g(y0), n__f(g(y1), y2))) ACTIVATE(n__f(g(y0), n__f(y1, y2))) -> c2(F(g(y0), n__f(y1, y2))) F(g(g(y0)), z1) -> c(F(g(y0), n__f(g(g(y0)), z1)), ACTIVATE(z1)) F(g(z0), n__f(g(y0), y1)) -> c(F(z0, n__f(g(z0), n__f(g(y0), y1))), ACTIVATE(n__f(g(y0), y1))) F(g(z0), n__f(g(y0), n__f(g(y1), y2))) -> c(F(z0, n__f(g(z0), n__f(g(y0), n__f(g(y1), y2)))), ACTIVATE(n__f(g(y0), n__f(g(y1), y2)))) F(g(z0), n__f(g(y0), n__f(y1, y2))) -> c(F(z0, n__f(g(z0), n__f(g(y0), n__f(y1, y2)))), ACTIVATE(n__f(g(y0), n__f(y1, y2)))) S tuples: F(g(x0), n__f(g(z0), z1)) -> c(F(x0, n__f(g(x0), f(z0, n__f(g(z0), activate(z1))))), ACTIVATE(n__f(g(z0), z1))) F(g(x0), n__f(z0, z1)) -> c(F(x0, n__f(g(x0), n__f(z0, z1))), ACTIVATE(n__f(z0, z1))) ACTIVATE(n__f(g(y0), z1)) -> c2(F(g(y0), z1)) ACTIVATE(n__f(g(y0), n__f(g(y1), y2))) -> c2(F(g(y0), n__f(g(y1), y2))) ACTIVATE(n__f(g(y0), n__f(y1, y2))) -> c2(F(g(y0), n__f(y1, y2))) F(g(g(y0)), z1) -> c(F(g(y0), n__f(g(g(y0)), z1)), ACTIVATE(z1)) F(g(z0), n__f(g(y0), y1)) -> c(F(z0, n__f(g(z0), n__f(g(y0), y1))), ACTIVATE(n__f(g(y0), y1))) F(g(z0), n__f(g(y0), n__f(g(y1), y2))) -> c(F(z0, n__f(g(z0), n__f(g(y0), n__f(g(y1), y2)))), ACTIVATE(n__f(g(y0), n__f(g(y1), y2)))) F(g(z0), n__f(g(y0), n__f(y1, y2))) -> c(F(z0, n__f(g(z0), n__f(g(y0), n__f(y1, y2)))), ACTIVATE(n__f(g(y0), n__f(y1, y2)))) K tuples:none Defined Rule Symbols: f_2, activate_1 Defined Pair Symbols: F_2, ACTIVATE_1 Compound Symbols: c_2, c2_1 ---------------------------------------- (49) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID)) Use forward instantiation to replace F(g(x0), n__f(z0, z1)) -> c(F(x0, n__f(g(x0), n__f(z0, z1))), ACTIVATE(n__f(z0, z1))) by F(g(g(y0)), n__f(z1, z2)) -> c(F(g(y0), n__f(g(g(y0)), n__f(z1, z2))), ACTIVATE(n__f(z1, z2))) F(g(z0), n__f(g(y0), z2)) -> c(F(z0, n__f(g(z0), n__f(g(y0), z2))), ACTIVATE(n__f(g(y0), z2))) F(g(z0), n__f(g(y0), n__f(g(y1), y2))) -> c(F(z0, n__f(g(z0), n__f(g(y0), n__f(g(y1), y2)))), ACTIVATE(n__f(g(y0), n__f(g(y1), y2)))) F(g(z0), n__f(g(y0), n__f(y1, y2))) -> c(F(z0, n__f(g(z0), n__f(g(y0), n__f(y1, y2)))), ACTIVATE(n__f(g(y0), n__f(y1, y2)))) F(g(g(g(y0))), n__f(z1, z2)) -> c(F(g(g(y0)), n__f(g(g(g(y0))), n__f(z1, z2))), ACTIVATE(n__f(z1, z2))) F(g(g(y0)), n__f(g(y2), z2)) -> c(F(g(y0), n__f(g(g(y0)), n__f(g(y2), z2))), ACTIVATE(n__f(g(y2), z2))) ---------------------------------------- (50) Obligation: Complexity Dependency Tuples Problem Rules: f(g(z0), z1) -> f(z0, n__f(g(z0), activate(z1))) f(z0, z1) -> n__f(z0, z1) activate(n__f(z0, z1)) -> f(z0, z1) activate(z0) -> z0 Tuples: F(g(x0), n__f(g(z0), z1)) -> c(F(x0, n__f(g(x0), f(z0, n__f(g(z0), activate(z1))))), ACTIVATE(n__f(g(z0), z1))) ACTIVATE(n__f(g(y0), z1)) -> c2(F(g(y0), z1)) ACTIVATE(n__f(g(y0), n__f(g(y1), y2))) -> c2(F(g(y0), n__f(g(y1), y2))) ACTIVATE(n__f(g(y0), n__f(y1, y2))) -> c2(F(g(y0), n__f(y1, y2))) F(g(g(y0)), z1) -> c(F(g(y0), n__f(g(g(y0)), z1)), ACTIVATE(z1)) F(g(z0), n__f(g(y0), y1)) -> c(F(z0, n__f(g(z0), n__f(g(y0), y1))), ACTIVATE(n__f(g(y0), y1))) F(g(z0), n__f(g(y0), n__f(g(y1), y2))) -> c(F(z0, n__f(g(z0), n__f(g(y0), n__f(g(y1), y2)))), ACTIVATE(n__f(g(y0), n__f(g(y1), y2)))) F(g(z0), n__f(g(y0), n__f(y1, y2))) -> c(F(z0, n__f(g(z0), n__f(g(y0), n__f(y1, y2)))), ACTIVATE(n__f(g(y0), n__f(y1, y2)))) F(g(g(y0)), n__f(z1, z2)) -> c(F(g(y0), n__f(g(g(y0)), n__f(z1, z2))), ACTIVATE(n__f(z1, z2))) F(g(g(g(y0))), n__f(z1, z2)) -> c(F(g(g(y0)), n__f(g(g(g(y0))), n__f(z1, z2))), ACTIVATE(n__f(z1, z2))) F(g(g(y0)), n__f(g(y2), z2)) -> c(F(g(y0), n__f(g(g(y0)), n__f(g(y2), z2))), ACTIVATE(n__f(g(y2), z2))) S tuples: F(g(x0), n__f(g(z0), z1)) -> c(F(x0, n__f(g(x0), f(z0, n__f(g(z0), activate(z1))))), ACTIVATE(n__f(g(z0), z1))) ACTIVATE(n__f(g(y0), z1)) -> c2(F(g(y0), z1)) ACTIVATE(n__f(g(y0), n__f(g(y1), y2))) -> c2(F(g(y0), n__f(g(y1), y2))) ACTIVATE(n__f(g(y0), n__f(y1, y2))) -> c2(F(g(y0), n__f(y1, y2))) F(g(g(y0)), z1) -> c(F(g(y0), n__f(g(g(y0)), z1)), ACTIVATE(z1)) F(g(z0), n__f(g(y0), y1)) -> c(F(z0, n__f(g(z0), n__f(g(y0), y1))), ACTIVATE(n__f(g(y0), y1))) F(g(z0), n__f(g(y0), n__f(g(y1), y2))) -> c(F(z0, n__f(g(z0), n__f(g(y0), n__f(g(y1), y2)))), ACTIVATE(n__f(g(y0), n__f(g(y1), y2)))) F(g(z0), n__f(g(y0), n__f(y1, y2))) -> c(F(z0, n__f(g(z0), n__f(g(y0), n__f(y1, y2)))), ACTIVATE(n__f(g(y0), n__f(y1, y2)))) F(g(g(y0)), n__f(z1, z2)) -> c(F(g(y0), n__f(g(g(y0)), n__f(z1, z2))), ACTIVATE(n__f(z1, z2))) F(g(g(g(y0))), n__f(z1, z2)) -> c(F(g(g(y0)), n__f(g(g(g(y0))), n__f(z1, z2))), ACTIVATE(n__f(z1, z2))) F(g(g(y0)), n__f(g(y2), z2)) -> c(F(g(y0), n__f(g(g(y0)), n__f(g(y2), z2))), ACTIVATE(n__f(g(y2), z2))) K tuples:none Defined Rule Symbols: f_2, activate_1 Defined Pair Symbols: F_2, ACTIVATE_1 Compound Symbols: c_2, c2_1 ---------------------------------------- (51) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID)) Use forward instantiation to replace ACTIVATE(n__f(g(y0), z1)) -> c2(F(g(y0), z1)) by ACTIVATE(n__f(g(z0), n__f(g(y1), y2))) -> c2(F(g(z0), n__f(g(y1), y2))) ACTIVATE(n__f(g(g(y0)), z1)) -> c2(F(g(g(y0)), z1)) ACTIVATE(n__f(g(z0), n__f(g(y1), n__f(g(y2), y3)))) -> c2(F(g(z0), n__f(g(y1), n__f(g(y2), y3)))) ACTIVATE(n__f(g(z0), n__f(g(y1), n__f(y2, y3)))) -> c2(F(g(z0), n__f(g(y1), n__f(y2, y3)))) ACTIVATE(n__f(g(g(y0)), n__f(y1, y2))) -> c2(F(g(g(y0)), n__f(y1, y2))) ACTIVATE(n__f(g(g(g(y0))), n__f(y1, y2))) -> c2(F(g(g(g(y0))), n__f(y1, y2))) ACTIVATE(n__f(g(g(y0)), n__f(g(y1), y2))) -> c2(F(g(g(y0)), n__f(g(y1), y2))) ---------------------------------------- (52) Obligation: Complexity Dependency Tuples Problem Rules: f(g(z0), z1) -> f(z0, n__f(g(z0), activate(z1))) f(z0, z1) -> n__f(z0, z1) activate(n__f(z0, z1)) -> f(z0, z1) activate(z0) -> z0 Tuples: F(g(x0), n__f(g(z0), z1)) -> c(F(x0, n__f(g(x0), f(z0, n__f(g(z0), activate(z1))))), ACTIVATE(n__f(g(z0), z1))) ACTIVATE(n__f(g(y0), n__f(g(y1), y2))) -> c2(F(g(y0), n__f(g(y1), y2))) ACTIVATE(n__f(g(y0), n__f(y1, y2))) -> c2(F(g(y0), n__f(y1, y2))) F(g(g(y0)), z1) -> c(F(g(y0), n__f(g(g(y0)), z1)), ACTIVATE(z1)) F(g(z0), n__f(g(y0), y1)) -> c(F(z0, n__f(g(z0), n__f(g(y0), y1))), ACTIVATE(n__f(g(y0), y1))) F(g(z0), n__f(g(y0), n__f(g(y1), y2))) -> c(F(z0, n__f(g(z0), n__f(g(y0), n__f(g(y1), y2)))), ACTIVATE(n__f(g(y0), n__f(g(y1), y2)))) F(g(z0), n__f(g(y0), n__f(y1, y2))) -> c(F(z0, n__f(g(z0), n__f(g(y0), n__f(y1, y2)))), ACTIVATE(n__f(g(y0), n__f(y1, y2)))) F(g(g(y0)), n__f(z1, z2)) -> c(F(g(y0), n__f(g(g(y0)), n__f(z1, z2))), ACTIVATE(n__f(z1, z2))) F(g(g(g(y0))), n__f(z1, z2)) -> c(F(g(g(y0)), n__f(g(g(g(y0))), n__f(z1, z2))), ACTIVATE(n__f(z1, z2))) F(g(g(y0)), n__f(g(y2), z2)) -> c(F(g(y0), n__f(g(g(y0)), n__f(g(y2), z2))), ACTIVATE(n__f(g(y2), z2))) ACTIVATE(n__f(g(g(y0)), z1)) -> c2(F(g(g(y0)), z1)) ACTIVATE(n__f(g(z0), n__f(g(y1), n__f(g(y2), y3)))) -> c2(F(g(z0), n__f(g(y1), n__f(g(y2), y3)))) ACTIVATE(n__f(g(z0), n__f(g(y1), n__f(y2, y3)))) -> c2(F(g(z0), n__f(g(y1), n__f(y2, y3)))) ACTIVATE(n__f(g(g(y0)), n__f(y1, y2))) -> c2(F(g(g(y0)), n__f(y1, y2))) ACTIVATE(n__f(g(g(g(y0))), n__f(y1, y2))) -> c2(F(g(g(g(y0))), n__f(y1, y2))) ACTIVATE(n__f(g(g(y0)), n__f(g(y1), y2))) -> c2(F(g(g(y0)), n__f(g(y1), y2))) S tuples: F(g(x0), n__f(g(z0), z1)) -> c(F(x0, n__f(g(x0), f(z0, n__f(g(z0), activate(z1))))), ACTIVATE(n__f(g(z0), z1))) ACTIVATE(n__f(g(y0), n__f(g(y1), y2))) -> c2(F(g(y0), n__f(g(y1), y2))) ACTIVATE(n__f(g(y0), n__f(y1, y2))) -> c2(F(g(y0), n__f(y1, y2))) F(g(g(y0)), z1) -> c(F(g(y0), n__f(g(g(y0)), z1)), ACTIVATE(z1)) F(g(z0), n__f(g(y0), y1)) -> c(F(z0, n__f(g(z0), n__f(g(y0), y1))), ACTIVATE(n__f(g(y0), y1))) F(g(z0), n__f(g(y0), n__f(g(y1), y2))) -> c(F(z0, n__f(g(z0), n__f(g(y0), n__f(g(y1), y2)))), ACTIVATE(n__f(g(y0), n__f(g(y1), y2)))) F(g(z0), n__f(g(y0), n__f(y1, y2))) -> c(F(z0, n__f(g(z0), n__f(g(y0), n__f(y1, y2)))), ACTIVATE(n__f(g(y0), n__f(y1, y2)))) F(g(g(y0)), n__f(z1, z2)) -> c(F(g(y0), n__f(g(g(y0)), n__f(z1, z2))), ACTIVATE(n__f(z1, z2))) F(g(g(g(y0))), n__f(z1, z2)) -> c(F(g(g(y0)), n__f(g(g(g(y0))), n__f(z1, z2))), ACTIVATE(n__f(z1, z2))) F(g(g(y0)), n__f(g(y2), z2)) -> c(F(g(y0), n__f(g(g(y0)), n__f(g(y2), z2))), ACTIVATE(n__f(g(y2), z2))) ACTIVATE(n__f(g(g(y0)), z1)) -> c2(F(g(g(y0)), z1)) ACTIVATE(n__f(g(z0), n__f(g(y1), n__f(g(y2), y3)))) -> c2(F(g(z0), n__f(g(y1), n__f(g(y2), y3)))) ACTIVATE(n__f(g(z0), n__f(g(y1), n__f(y2, y3)))) -> c2(F(g(z0), n__f(g(y1), n__f(y2, y3)))) ACTIVATE(n__f(g(g(y0)), n__f(y1, y2))) -> c2(F(g(g(y0)), n__f(y1, y2))) ACTIVATE(n__f(g(g(g(y0))), n__f(y1, y2))) -> c2(F(g(g(g(y0))), n__f(y1, y2))) ACTIVATE(n__f(g(g(y0)), n__f(g(y1), y2))) -> c2(F(g(g(y0)), n__f(g(y1), y2))) K tuples:none Defined Rule Symbols: f_2, activate_1 Defined Pair Symbols: F_2, ACTIVATE_1 Compound Symbols: c_2, c2_1 ---------------------------------------- (53) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID)) Use forward instantiation to replace ACTIVATE(n__f(g(y0), n__f(y1, y2))) -> c2(F(g(y0), n__f(y1, y2))) by ACTIVATE(n__f(g(z0), n__f(g(y1), z2))) -> c2(F(g(z0), n__f(g(y1), z2))) ACTIVATE(n__f(g(g(y0)), n__f(z1, z2))) -> c2(F(g(g(y0)), n__f(z1, z2))) ACTIVATE(n__f(g(z0), n__f(g(y1), n__f(g(y2), y3)))) -> c2(F(g(z0), n__f(g(y1), n__f(g(y2), y3)))) ACTIVATE(n__f(g(z0), n__f(g(y1), n__f(y2, y3)))) -> c2(F(g(z0), n__f(g(y1), n__f(y2, y3)))) ACTIVATE(n__f(g(g(g(y0))), n__f(z1, z2))) -> c2(F(g(g(g(y0))), n__f(z1, z2))) ACTIVATE(n__f(g(g(y0)), n__f(g(y1), z2))) -> c2(F(g(g(y0)), n__f(g(y1), z2))) ---------------------------------------- (54) Obligation: Complexity Dependency Tuples Problem Rules: f(g(z0), z1) -> f(z0, n__f(g(z0), activate(z1))) f(z0, z1) -> n__f(z0, z1) activate(n__f(z0, z1)) -> f(z0, z1) activate(z0) -> z0 Tuples: F(g(x0), n__f(g(z0), z1)) -> c(F(x0, n__f(g(x0), f(z0, n__f(g(z0), activate(z1))))), ACTIVATE(n__f(g(z0), z1))) ACTIVATE(n__f(g(y0), n__f(g(y1), y2))) -> c2(F(g(y0), n__f(g(y1), y2))) F(g(g(y0)), z1) -> c(F(g(y0), n__f(g(g(y0)), z1)), ACTIVATE(z1)) F(g(z0), n__f(g(y0), y1)) -> c(F(z0, n__f(g(z0), n__f(g(y0), y1))), ACTIVATE(n__f(g(y0), y1))) F(g(z0), n__f(g(y0), n__f(g(y1), y2))) -> c(F(z0, n__f(g(z0), n__f(g(y0), n__f(g(y1), y2)))), ACTIVATE(n__f(g(y0), n__f(g(y1), y2)))) F(g(z0), n__f(g(y0), n__f(y1, y2))) -> c(F(z0, n__f(g(z0), n__f(g(y0), n__f(y1, y2)))), ACTIVATE(n__f(g(y0), n__f(y1, y2)))) F(g(g(y0)), n__f(z1, z2)) -> c(F(g(y0), n__f(g(g(y0)), n__f(z1, z2))), ACTIVATE(n__f(z1, z2))) F(g(g(g(y0))), n__f(z1, z2)) -> c(F(g(g(y0)), n__f(g(g(g(y0))), n__f(z1, z2))), ACTIVATE(n__f(z1, z2))) F(g(g(y0)), n__f(g(y2), z2)) -> c(F(g(y0), n__f(g(g(y0)), n__f(g(y2), z2))), ACTIVATE(n__f(g(y2), z2))) ACTIVATE(n__f(g(g(y0)), z1)) -> c2(F(g(g(y0)), z1)) ACTIVATE(n__f(g(z0), n__f(g(y1), n__f(g(y2), y3)))) -> c2(F(g(z0), n__f(g(y1), n__f(g(y2), y3)))) ACTIVATE(n__f(g(z0), n__f(g(y1), n__f(y2, y3)))) -> c2(F(g(z0), n__f(g(y1), n__f(y2, y3)))) ACTIVATE(n__f(g(g(y0)), n__f(y1, y2))) -> c2(F(g(g(y0)), n__f(y1, y2))) ACTIVATE(n__f(g(g(g(y0))), n__f(y1, y2))) -> c2(F(g(g(g(y0))), n__f(y1, y2))) ACTIVATE(n__f(g(g(y0)), n__f(g(y1), y2))) -> c2(F(g(g(y0)), n__f(g(y1), y2))) S tuples: F(g(x0), n__f(g(z0), z1)) -> c(F(x0, n__f(g(x0), f(z0, n__f(g(z0), activate(z1))))), ACTIVATE(n__f(g(z0), z1))) ACTIVATE(n__f(g(y0), n__f(g(y1), y2))) -> c2(F(g(y0), n__f(g(y1), y2))) F(g(g(y0)), z1) -> c(F(g(y0), n__f(g(g(y0)), z1)), ACTIVATE(z1)) F(g(z0), n__f(g(y0), y1)) -> c(F(z0, n__f(g(z0), n__f(g(y0), y1))), ACTIVATE(n__f(g(y0), y1))) F(g(z0), n__f(g(y0), n__f(g(y1), y2))) -> c(F(z0, n__f(g(z0), n__f(g(y0), n__f(g(y1), y2)))), ACTIVATE(n__f(g(y0), n__f(g(y1), y2)))) F(g(z0), n__f(g(y0), n__f(y1, y2))) -> c(F(z0, n__f(g(z0), n__f(g(y0), n__f(y1, y2)))), ACTIVATE(n__f(g(y0), n__f(y1, y2)))) F(g(g(y0)), n__f(z1, z2)) -> c(F(g(y0), n__f(g(g(y0)), n__f(z1, z2))), ACTIVATE(n__f(z1, z2))) F(g(g(g(y0))), n__f(z1, z2)) -> c(F(g(g(y0)), n__f(g(g(g(y0))), n__f(z1, z2))), ACTIVATE(n__f(z1, z2))) F(g(g(y0)), n__f(g(y2), z2)) -> c(F(g(y0), n__f(g(g(y0)), n__f(g(y2), z2))), ACTIVATE(n__f(g(y2), z2))) ACTIVATE(n__f(g(g(y0)), z1)) -> c2(F(g(g(y0)), z1)) ACTIVATE(n__f(g(z0), n__f(g(y1), n__f(g(y2), y3)))) -> c2(F(g(z0), n__f(g(y1), n__f(g(y2), y3)))) ACTIVATE(n__f(g(z0), n__f(g(y1), n__f(y2, y3)))) -> c2(F(g(z0), n__f(g(y1), n__f(y2, y3)))) ACTIVATE(n__f(g(g(y0)), n__f(y1, y2))) -> c2(F(g(g(y0)), n__f(y1, y2))) ACTIVATE(n__f(g(g(g(y0))), n__f(y1, y2))) -> c2(F(g(g(g(y0))), n__f(y1, y2))) ACTIVATE(n__f(g(g(y0)), n__f(g(y1), y2))) -> c2(F(g(g(y0)), n__f(g(y1), y2))) K tuples:none Defined Rule Symbols: f_2, activate_1 Defined Pair Symbols: F_2, ACTIVATE_1 Compound Symbols: c_2, c2_1 ---------------------------------------- (55) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID)) Use forward instantiation to replace F(g(z0), n__f(g(y0), y1)) -> c(F(z0, n__f(g(z0), n__f(g(y0), y1))), ACTIVATE(n__f(g(y0), y1))) by F(g(g(y0)), n__f(g(z1), z2)) -> c(F(g(y0), n__f(g(g(y0)), n__f(g(z1), z2))), ACTIVATE(n__f(g(z1), z2))) F(g(z0), n__f(g(z1), n__f(g(y1), y2))) -> c(F(z0, n__f(g(z0), n__f(g(z1), n__f(g(y1), y2)))), ACTIVATE(n__f(g(z1), n__f(g(y1), y2)))) F(g(g(g(y0))), n__f(g(z1), z2)) -> c(F(g(g(y0)), n__f(g(g(g(y0))), n__f(g(z1), z2))), ACTIVATE(n__f(g(z1), z2))) F(g(g(g(g(y0)))), n__f(g(z1), z2)) -> c(F(g(g(g(y0))), n__f(g(g(g(g(y0)))), n__f(g(z1), z2))), ACTIVATE(n__f(g(z1), z2))) F(g(z0), n__f(g(g(y0)), z2)) -> c(F(z0, n__f(g(z0), n__f(g(g(y0)), z2))), ACTIVATE(n__f(g(g(y0)), z2))) F(g(z0), n__f(g(z1), n__f(g(y1), n__f(g(y2), y3)))) -> c(F(z0, n__f(g(z0), n__f(g(z1), n__f(g(y1), n__f(g(y2), y3))))), ACTIVATE(n__f(g(z1), n__f(g(y1), n__f(g(y2), y3))))) F(g(z0), n__f(g(z1), n__f(g(y1), n__f(y2, y3)))) -> c(F(z0, n__f(g(z0), n__f(g(z1), n__f(g(y1), n__f(y2, y3))))), ACTIVATE(n__f(g(z1), n__f(g(y1), n__f(y2, y3))))) F(g(z0), n__f(g(g(y0)), n__f(y1, y2))) -> c(F(z0, n__f(g(z0), n__f(g(g(y0)), n__f(y1, y2)))), ACTIVATE(n__f(g(g(y0)), n__f(y1, y2)))) F(g(z0), n__f(g(g(g(y0))), n__f(y1, y2))) -> c(F(z0, n__f(g(z0), n__f(g(g(g(y0))), n__f(y1, y2)))), ACTIVATE(n__f(g(g(g(y0))), n__f(y1, y2)))) F(g(z0), n__f(g(g(y0)), n__f(g(y1), y2))) -> c(F(z0, n__f(g(z0), n__f(g(g(y0)), n__f(g(y1), y2)))), ACTIVATE(n__f(g(g(y0)), n__f(g(y1), y2)))) ---------------------------------------- (56) Obligation: Complexity Dependency Tuples Problem Rules: f(g(z0), z1) -> f(z0, n__f(g(z0), activate(z1))) f(z0, z1) -> n__f(z0, z1) activate(n__f(z0, z1)) -> f(z0, z1) activate(z0) -> z0 Tuples: F(g(x0), n__f(g(z0), z1)) -> c(F(x0, n__f(g(x0), f(z0, n__f(g(z0), activate(z1))))), ACTIVATE(n__f(g(z0), z1))) ACTIVATE(n__f(g(y0), n__f(g(y1), y2))) -> c2(F(g(y0), n__f(g(y1), y2))) F(g(g(y0)), z1) -> c(F(g(y0), n__f(g(g(y0)), z1)), ACTIVATE(z1)) F(g(z0), n__f(g(y0), y1)) -> c(F(z0, n__f(g(z0), n__f(g(y0), y1))), ACTIVATE(n__f(g(y0), y1))) F(g(z0), n__f(g(y0), n__f(g(y1), y2))) -> c(F(z0, n__f(g(z0), n__f(g(y0), n__f(g(y1), y2)))), ACTIVATE(n__f(g(y0), n__f(g(y1), y2)))) F(g(z0), n__f(g(y0), n__f(y1, y2))) -> c(F(z0, n__f(g(z0), n__f(g(y0), n__f(y1, y2)))), ACTIVATE(n__f(g(y0), n__f(y1, y2)))) F(g(g(y0)), n__f(z1, z2)) -> c(F(g(y0), n__f(g(g(y0)), n__f(z1, z2))), ACTIVATE(n__f(z1, z2))) F(g(g(g(y0))), n__f(z1, z2)) -> c(F(g(g(y0)), n__f(g(g(g(y0))), n__f(z1, z2))), ACTIVATE(n__f(z1, z2))) F(g(g(y0)), n__f(g(y2), z2)) -> c(F(g(y0), n__f(g(g(y0)), n__f(g(y2), z2))), ACTIVATE(n__f(g(y2), z2))) ACTIVATE(n__f(g(g(y0)), z1)) -> c2(F(g(g(y0)), z1)) ACTIVATE(n__f(g(z0), n__f(g(y1), n__f(g(y2), y3)))) -> c2(F(g(z0), n__f(g(y1), n__f(g(y2), y3)))) ACTIVATE(n__f(g(z0), n__f(g(y1), n__f(y2, y3)))) -> c2(F(g(z0), n__f(g(y1), n__f(y2, y3)))) ACTIVATE(n__f(g(g(y0)), n__f(y1, y2))) -> c2(F(g(g(y0)), n__f(y1, y2))) ACTIVATE(n__f(g(g(g(y0))), n__f(y1, y2))) -> c2(F(g(g(g(y0))), n__f(y1, y2))) ACTIVATE(n__f(g(g(y0)), n__f(g(y1), y2))) -> c2(F(g(g(y0)), n__f(g(y1), y2))) F(g(g(g(y0))), n__f(g(z1), z2)) -> c(F(g(g(y0)), n__f(g(g(g(y0))), n__f(g(z1), z2))), ACTIVATE(n__f(g(z1), z2))) F(g(g(g(g(y0)))), n__f(g(z1), z2)) -> c(F(g(g(g(y0))), n__f(g(g(g(g(y0)))), n__f(g(z1), z2))), ACTIVATE(n__f(g(z1), z2))) F(g(z0), n__f(g(g(y0)), z2)) -> c(F(z0, n__f(g(z0), n__f(g(g(y0)), z2))), ACTIVATE(n__f(g(g(y0)), z2))) F(g(z0), n__f(g(z1), n__f(g(y1), n__f(g(y2), y3)))) -> c(F(z0, n__f(g(z0), n__f(g(z1), n__f(g(y1), n__f(g(y2), y3))))), ACTIVATE(n__f(g(z1), n__f(g(y1), n__f(g(y2), y3))))) F(g(z0), n__f(g(z1), n__f(g(y1), n__f(y2, y3)))) -> c(F(z0, n__f(g(z0), n__f(g(z1), n__f(g(y1), n__f(y2, y3))))), ACTIVATE(n__f(g(z1), n__f(g(y1), n__f(y2, y3))))) F(g(z0), n__f(g(g(y0)), n__f(y1, y2))) -> c(F(z0, n__f(g(z0), n__f(g(g(y0)), n__f(y1, y2)))), ACTIVATE(n__f(g(g(y0)), n__f(y1, y2)))) F(g(z0), n__f(g(g(g(y0))), n__f(y1, y2))) -> c(F(z0, n__f(g(z0), n__f(g(g(g(y0))), n__f(y1, y2)))), ACTIVATE(n__f(g(g(g(y0))), n__f(y1, y2)))) F(g(z0), n__f(g(g(y0)), n__f(g(y1), y2))) -> c(F(z0, n__f(g(z0), n__f(g(g(y0)), n__f(g(y1), y2)))), ACTIVATE(n__f(g(g(y0)), n__f(g(y1), y2)))) S tuples: F(g(x0), n__f(g(z0), z1)) -> c(F(x0, n__f(g(x0), f(z0, n__f(g(z0), activate(z1))))), ACTIVATE(n__f(g(z0), z1))) ACTIVATE(n__f(g(y0), n__f(g(y1), y2))) -> c2(F(g(y0), n__f(g(y1), y2))) F(g(g(y0)), z1) -> c(F(g(y0), n__f(g(g(y0)), z1)), ACTIVATE(z1)) F(g(z0), n__f(g(y0), n__f(g(y1), y2))) -> c(F(z0, n__f(g(z0), n__f(g(y0), n__f(g(y1), y2)))), ACTIVATE(n__f(g(y0), n__f(g(y1), y2)))) F(g(z0), n__f(g(y0), n__f(y1, y2))) -> c(F(z0, n__f(g(z0), n__f(g(y0), n__f(y1, y2)))), ACTIVATE(n__f(g(y0), n__f(y1, y2)))) F(g(g(y0)), n__f(z1, z2)) -> c(F(g(y0), n__f(g(g(y0)), n__f(z1, z2))), ACTIVATE(n__f(z1, z2))) F(g(g(g(y0))), n__f(z1, z2)) -> c(F(g(g(y0)), n__f(g(g(g(y0))), n__f(z1, z2))), ACTIVATE(n__f(z1, z2))) F(g(g(y0)), n__f(g(y2), z2)) -> c(F(g(y0), n__f(g(g(y0)), n__f(g(y2), z2))), ACTIVATE(n__f(g(y2), z2))) ACTIVATE(n__f(g(g(y0)), z1)) -> c2(F(g(g(y0)), z1)) ACTIVATE(n__f(g(z0), n__f(g(y1), n__f(g(y2), y3)))) -> c2(F(g(z0), n__f(g(y1), n__f(g(y2), y3)))) ACTIVATE(n__f(g(z0), n__f(g(y1), n__f(y2, y3)))) -> c2(F(g(z0), n__f(g(y1), n__f(y2, y3)))) ACTIVATE(n__f(g(g(y0)), n__f(y1, y2))) -> c2(F(g(g(y0)), n__f(y1, y2))) ACTIVATE(n__f(g(g(g(y0))), n__f(y1, y2))) -> c2(F(g(g(g(y0))), n__f(y1, y2))) ACTIVATE(n__f(g(g(y0)), n__f(g(y1), y2))) -> c2(F(g(g(y0)), n__f(g(y1), y2))) F(g(g(g(y0))), n__f(g(z1), z2)) -> c(F(g(g(y0)), n__f(g(g(g(y0))), n__f(g(z1), z2))), ACTIVATE(n__f(g(z1), z2))) F(g(g(g(g(y0)))), n__f(g(z1), z2)) -> c(F(g(g(g(y0))), n__f(g(g(g(g(y0)))), n__f(g(z1), z2))), ACTIVATE(n__f(g(z1), z2))) F(g(z0), n__f(g(g(y0)), z2)) -> c(F(z0, n__f(g(z0), n__f(g(g(y0)), z2))), ACTIVATE(n__f(g(g(y0)), z2))) F(g(z0), n__f(g(z1), n__f(g(y1), n__f(g(y2), y3)))) -> c(F(z0, n__f(g(z0), n__f(g(z1), n__f(g(y1), n__f(g(y2), y3))))), ACTIVATE(n__f(g(z1), n__f(g(y1), n__f(g(y2), y3))))) F(g(z0), n__f(g(z1), n__f(g(y1), n__f(y2, y3)))) -> c(F(z0, n__f(g(z0), n__f(g(z1), n__f(g(y1), n__f(y2, y3))))), ACTIVATE(n__f(g(z1), n__f(g(y1), n__f(y2, y3))))) F(g(z0), n__f(g(g(y0)), n__f(y1, y2))) -> c(F(z0, n__f(g(z0), n__f(g(g(y0)), n__f(y1, y2)))), ACTIVATE(n__f(g(g(y0)), n__f(y1, y2)))) F(g(z0), n__f(g(g(g(y0))), n__f(y1, y2))) -> c(F(z0, n__f(g(z0), n__f(g(g(g(y0))), n__f(y1, y2)))), ACTIVATE(n__f(g(g(g(y0))), n__f(y1, y2)))) F(g(z0), n__f(g(g(y0)), n__f(g(y1), y2))) -> c(F(z0, n__f(g(z0), n__f(g(g(y0)), n__f(g(y1), y2)))), ACTIVATE(n__f(g(g(y0)), n__f(g(y1), y2)))) K tuples:none Defined Rule Symbols: f_2, activate_1 Defined Pair Symbols: F_2, ACTIVATE_1 Compound Symbols: c_2, c2_1 ---------------------------------------- (57) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID)) Use forward instantiation to replace F(g(z0), n__f(g(y0), n__f(y1, y2))) -> c(F(z0, n__f(g(z0), n__f(g(y0), n__f(y1, y2)))), ACTIVATE(n__f(g(y0), n__f(y1, y2)))) by F(g(g(y0)), n__f(g(z1), n__f(z2, z3))) -> c(F(g(y0), n__f(g(g(y0)), n__f(g(z1), n__f(z2, z3)))), ACTIVATE(n__f(g(z1), n__f(z2, z3)))) F(g(z0), n__f(g(z1), n__f(g(y1), z3))) -> c(F(z0, n__f(g(z0), n__f(g(z1), n__f(g(y1), z3)))), ACTIVATE(n__f(g(z1), n__f(g(y1), z3)))) F(g(g(g(y0))), n__f(g(z1), n__f(z2, z3))) -> c(F(g(g(y0)), n__f(g(g(g(y0))), n__f(g(z1), n__f(z2, z3)))), ACTIVATE(n__f(g(z1), n__f(z2, z3)))) F(g(g(g(g(y0)))), n__f(g(z1), n__f(z2, z3))) -> c(F(g(g(g(y0))), n__f(g(g(g(g(y0)))), n__f(g(z1), n__f(z2, z3)))), ACTIVATE(n__f(g(z1), n__f(z2, z3)))) F(g(z0), n__f(g(g(y0)), n__f(z2, z3))) -> c(F(z0, n__f(g(z0), n__f(g(g(y0)), n__f(z2, z3)))), ACTIVATE(n__f(g(g(y0)), n__f(z2, z3)))) F(g(z0), n__f(g(z1), n__f(g(y1), n__f(g(y2), y3)))) -> c(F(z0, n__f(g(z0), n__f(g(z1), n__f(g(y1), n__f(g(y2), y3))))), ACTIVATE(n__f(g(z1), n__f(g(y1), n__f(g(y2), y3))))) F(g(z0), n__f(g(z1), n__f(g(y1), n__f(y2, y3)))) -> c(F(z0, n__f(g(z0), n__f(g(z1), n__f(g(y1), n__f(y2, y3))))), ACTIVATE(n__f(g(z1), n__f(g(y1), n__f(y2, y3))))) F(g(z0), n__f(g(g(g(y0))), n__f(z2, z3))) -> c(F(z0, n__f(g(z0), n__f(g(g(g(y0))), n__f(z2, z3)))), ACTIVATE(n__f(g(g(g(y0))), n__f(z2, z3)))) F(g(z0), n__f(g(g(y0)), n__f(g(y1), z3))) -> c(F(z0, n__f(g(z0), n__f(g(g(y0)), n__f(g(y1), z3)))), ACTIVATE(n__f(g(g(y0)), n__f(g(y1), z3)))) F(g(g(g(g(g(y0))))), n__f(g(z1), n__f(z2, z3))) -> c(F(g(g(g(g(y0)))), n__f(g(g(g(g(g(y0))))), n__f(g(z1), n__f(z2, z3)))), ACTIVATE(n__f(g(z1), n__f(z2, z3)))) F(g(g(y0)), n__f(g(z1), n__f(g(y3), z3))) -> c(F(g(y0), n__f(g(g(y0)), n__f(g(z1), n__f(g(y3), z3)))), ACTIVATE(n__f(g(z1), n__f(g(y3), z3)))) ---------------------------------------- (58) Obligation: Complexity Dependency Tuples Problem Rules: f(g(z0), z1) -> f(z0, n__f(g(z0), activate(z1))) f(z0, z1) -> n__f(z0, z1) activate(n__f(z0, z1)) -> f(z0, z1) activate(z0) -> z0 Tuples: F(g(x0), n__f(g(z0), z1)) -> c(F(x0, n__f(g(x0), f(z0, n__f(g(z0), activate(z1))))), ACTIVATE(n__f(g(z0), z1))) ACTIVATE(n__f(g(y0), n__f(g(y1), y2))) -> c2(F(g(y0), n__f(g(y1), y2))) F(g(g(y0)), z1) -> c(F(g(y0), n__f(g(g(y0)), z1)), ACTIVATE(z1)) F(g(z0), n__f(g(y0), y1)) -> c(F(z0, n__f(g(z0), n__f(g(y0), y1))), ACTIVATE(n__f(g(y0), y1))) F(g(z0), n__f(g(y0), n__f(g(y1), y2))) -> c(F(z0, n__f(g(z0), n__f(g(y0), n__f(g(y1), y2)))), ACTIVATE(n__f(g(y0), n__f(g(y1), y2)))) F(g(z0), n__f(g(y0), n__f(y1, y2))) -> c(F(z0, n__f(g(z0), n__f(g(y0), n__f(y1, y2)))), ACTIVATE(n__f(g(y0), n__f(y1, y2)))) F(g(g(y0)), n__f(z1, z2)) -> c(F(g(y0), n__f(g(g(y0)), n__f(z1, z2))), ACTIVATE(n__f(z1, z2))) F(g(g(g(y0))), n__f(z1, z2)) -> c(F(g(g(y0)), n__f(g(g(g(y0))), n__f(z1, z2))), ACTIVATE(n__f(z1, z2))) F(g(g(y0)), n__f(g(y2), z2)) -> c(F(g(y0), n__f(g(g(y0)), n__f(g(y2), z2))), ACTIVATE(n__f(g(y2), z2))) ACTIVATE(n__f(g(g(y0)), z1)) -> c2(F(g(g(y0)), z1)) ACTIVATE(n__f(g(z0), n__f(g(y1), n__f(g(y2), y3)))) -> c2(F(g(z0), n__f(g(y1), n__f(g(y2), y3)))) ACTIVATE(n__f(g(z0), n__f(g(y1), n__f(y2, y3)))) -> c2(F(g(z0), n__f(g(y1), n__f(y2, y3)))) ACTIVATE(n__f(g(g(y0)), n__f(y1, y2))) -> c2(F(g(g(y0)), n__f(y1, y2))) ACTIVATE(n__f(g(g(g(y0))), n__f(y1, y2))) -> c2(F(g(g(g(y0))), n__f(y1, y2))) ACTIVATE(n__f(g(g(y0)), n__f(g(y1), y2))) -> c2(F(g(g(y0)), n__f(g(y1), y2))) F(g(g(g(y0))), n__f(g(z1), z2)) -> c(F(g(g(y0)), n__f(g(g(g(y0))), n__f(g(z1), z2))), ACTIVATE(n__f(g(z1), z2))) F(g(g(g(g(y0)))), n__f(g(z1), z2)) -> c(F(g(g(g(y0))), n__f(g(g(g(g(y0)))), n__f(g(z1), z2))), ACTIVATE(n__f(g(z1), z2))) F(g(z0), n__f(g(g(y0)), z2)) -> c(F(z0, n__f(g(z0), n__f(g(g(y0)), z2))), ACTIVATE(n__f(g(g(y0)), z2))) F(g(z0), n__f(g(z1), n__f(g(y1), n__f(g(y2), y3)))) -> c(F(z0, n__f(g(z0), n__f(g(z1), n__f(g(y1), n__f(g(y2), y3))))), ACTIVATE(n__f(g(z1), n__f(g(y1), n__f(g(y2), y3))))) F(g(z0), n__f(g(z1), n__f(g(y1), n__f(y2, y3)))) -> c(F(z0, n__f(g(z0), n__f(g(z1), n__f(g(y1), n__f(y2, y3))))), ACTIVATE(n__f(g(z1), n__f(g(y1), n__f(y2, y3))))) F(g(z0), n__f(g(g(y0)), n__f(y1, y2))) -> c(F(z0, n__f(g(z0), n__f(g(g(y0)), n__f(y1, y2)))), ACTIVATE(n__f(g(g(y0)), n__f(y1, y2)))) F(g(z0), n__f(g(g(g(y0))), n__f(y1, y2))) -> c(F(z0, n__f(g(z0), n__f(g(g(g(y0))), n__f(y1, y2)))), ACTIVATE(n__f(g(g(g(y0))), n__f(y1, y2)))) F(g(z0), n__f(g(g(y0)), n__f(g(y1), y2))) -> c(F(z0, n__f(g(z0), n__f(g(g(y0)), n__f(g(y1), y2)))), ACTIVATE(n__f(g(g(y0)), n__f(g(y1), y2)))) F(g(g(y0)), n__f(g(z1), n__f(z2, z3))) -> c(F(g(y0), n__f(g(g(y0)), n__f(g(z1), n__f(z2, z3)))), ACTIVATE(n__f(g(z1), n__f(z2, z3)))) F(g(g(g(y0))), n__f(g(z1), n__f(z2, z3))) -> c(F(g(g(y0)), n__f(g(g(g(y0))), n__f(g(z1), n__f(z2, z3)))), ACTIVATE(n__f(g(z1), n__f(z2, z3)))) F(g(g(g(g(y0)))), n__f(g(z1), n__f(z2, z3))) -> c(F(g(g(g(y0))), n__f(g(g(g(g(y0)))), n__f(g(z1), n__f(z2, z3)))), ACTIVATE(n__f(g(z1), n__f(z2, z3)))) F(g(g(g(g(g(y0))))), n__f(g(z1), n__f(z2, z3))) -> c(F(g(g(g(g(y0)))), n__f(g(g(g(g(g(y0))))), n__f(g(z1), n__f(z2, z3)))), ACTIVATE(n__f(g(z1), n__f(z2, z3)))) F(g(g(y0)), n__f(g(z1), n__f(g(y3), z3))) -> c(F(g(y0), n__f(g(g(y0)), n__f(g(z1), n__f(g(y3), z3)))), ACTIVATE(n__f(g(z1), n__f(g(y3), z3)))) S tuples: F(g(x0), n__f(g(z0), z1)) -> c(F(x0, n__f(g(x0), f(z0, n__f(g(z0), activate(z1))))), ACTIVATE(n__f(g(z0), z1))) ACTIVATE(n__f(g(y0), n__f(g(y1), y2))) -> c2(F(g(y0), n__f(g(y1), y2))) F(g(g(y0)), z1) -> c(F(g(y0), n__f(g(g(y0)), z1)), ACTIVATE(z1)) F(g(z0), n__f(g(y0), n__f(g(y1), y2))) -> c(F(z0, n__f(g(z0), n__f(g(y0), n__f(g(y1), y2)))), ACTIVATE(n__f(g(y0), n__f(g(y1), y2)))) F(g(g(y0)), n__f(z1, z2)) -> c(F(g(y0), n__f(g(g(y0)), n__f(z1, z2))), ACTIVATE(n__f(z1, z2))) F(g(g(g(y0))), n__f(z1, z2)) -> c(F(g(g(y0)), n__f(g(g(g(y0))), n__f(z1, z2))), ACTIVATE(n__f(z1, z2))) F(g(g(y0)), n__f(g(y2), z2)) -> c(F(g(y0), n__f(g(g(y0)), n__f(g(y2), z2))), ACTIVATE(n__f(g(y2), z2))) ACTIVATE(n__f(g(g(y0)), z1)) -> c2(F(g(g(y0)), z1)) ACTIVATE(n__f(g(z0), n__f(g(y1), n__f(g(y2), y3)))) -> c2(F(g(z0), n__f(g(y1), n__f(g(y2), y3)))) ACTIVATE(n__f(g(z0), n__f(g(y1), n__f(y2, y3)))) -> c2(F(g(z0), n__f(g(y1), n__f(y2, y3)))) ACTIVATE(n__f(g(g(y0)), n__f(y1, y2))) -> c2(F(g(g(y0)), n__f(y1, y2))) ACTIVATE(n__f(g(g(g(y0))), n__f(y1, y2))) -> c2(F(g(g(g(y0))), n__f(y1, y2))) ACTIVATE(n__f(g(g(y0)), n__f(g(y1), y2))) -> c2(F(g(g(y0)), n__f(g(y1), y2))) F(g(g(g(y0))), n__f(g(z1), z2)) -> c(F(g(g(y0)), n__f(g(g(g(y0))), n__f(g(z1), z2))), ACTIVATE(n__f(g(z1), z2))) F(g(g(g(g(y0)))), n__f(g(z1), z2)) -> c(F(g(g(g(y0))), n__f(g(g(g(g(y0)))), n__f(g(z1), z2))), ACTIVATE(n__f(g(z1), z2))) F(g(z0), n__f(g(g(y0)), z2)) -> c(F(z0, n__f(g(z0), n__f(g(g(y0)), z2))), ACTIVATE(n__f(g(g(y0)), z2))) F(g(z0), n__f(g(z1), n__f(g(y1), n__f(g(y2), y3)))) -> c(F(z0, n__f(g(z0), n__f(g(z1), n__f(g(y1), n__f(g(y2), y3))))), ACTIVATE(n__f(g(z1), n__f(g(y1), n__f(g(y2), y3))))) F(g(z0), n__f(g(z1), n__f(g(y1), n__f(y2, y3)))) -> c(F(z0, n__f(g(z0), n__f(g(z1), n__f(g(y1), n__f(y2, y3))))), ACTIVATE(n__f(g(z1), n__f(g(y1), n__f(y2, y3))))) F(g(z0), n__f(g(g(y0)), n__f(y1, y2))) -> c(F(z0, n__f(g(z0), n__f(g(g(y0)), n__f(y1, y2)))), ACTIVATE(n__f(g(g(y0)), n__f(y1, y2)))) F(g(z0), n__f(g(g(g(y0))), n__f(y1, y2))) -> c(F(z0, n__f(g(z0), n__f(g(g(g(y0))), n__f(y1, y2)))), ACTIVATE(n__f(g(g(g(y0))), n__f(y1, y2)))) F(g(z0), n__f(g(g(y0)), n__f(g(y1), y2))) -> c(F(z0, n__f(g(z0), n__f(g(g(y0)), n__f(g(y1), y2)))), ACTIVATE(n__f(g(g(y0)), n__f(g(y1), y2)))) F(g(g(y0)), n__f(g(z1), n__f(z2, z3))) -> c(F(g(y0), n__f(g(g(y0)), n__f(g(z1), n__f(z2, z3)))), ACTIVATE(n__f(g(z1), n__f(z2, z3)))) F(g(g(g(y0))), n__f(g(z1), n__f(z2, z3))) -> c(F(g(g(y0)), n__f(g(g(g(y0))), n__f(g(z1), n__f(z2, z3)))), ACTIVATE(n__f(g(z1), n__f(z2, z3)))) F(g(g(g(g(y0)))), n__f(g(z1), n__f(z2, z3))) -> c(F(g(g(g(y0))), n__f(g(g(g(g(y0)))), n__f(g(z1), n__f(z2, z3)))), ACTIVATE(n__f(g(z1), n__f(z2, z3)))) F(g(g(g(g(g(y0))))), n__f(g(z1), n__f(z2, z3))) -> c(F(g(g(g(g(y0)))), n__f(g(g(g(g(g(y0))))), n__f(g(z1), n__f(z2, z3)))), ACTIVATE(n__f(g(z1), n__f(z2, z3)))) F(g(g(y0)), n__f(g(z1), n__f(g(y3), z3))) -> c(F(g(y0), n__f(g(g(y0)), n__f(g(z1), n__f(g(y3), z3)))), ACTIVATE(n__f(g(z1), n__f(g(y3), z3)))) K tuples:none Defined Rule Symbols: f_2, activate_1 Defined Pair Symbols: F_2, ACTIVATE_1 Compound Symbols: c_2, c2_1 ---------------------------------------- (59) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID)) Use forward instantiation to replace F(g(z0), n__f(g(y0), z2)) -> c(F(z0, n__f(g(z0), n__f(g(y0), z2))), ACTIVATE(n__f(g(y0), z2))) by F(g(g(y0)), n__f(g(z1), z2)) -> c(F(g(y0), n__f(g(g(y0)), n__f(g(z1), z2))), ACTIVATE(n__f(g(z1), z2))) F(g(z0), n__f(g(z1), n__f(g(y1), y2))) -> c(F(z0, n__f(g(z0), n__f(g(z1), n__f(g(y1), y2)))), ACTIVATE(n__f(g(z1), n__f(g(y1), y2)))) F(g(g(g(y0))), n__f(g(z1), z2)) -> c(F(g(g(y0)), n__f(g(g(g(y0))), n__f(g(z1), z2))), ACTIVATE(n__f(g(z1), z2))) F(g(g(g(g(y0)))), n__f(g(z1), z2)) -> c(F(g(g(g(y0))), n__f(g(g(g(g(y0)))), n__f(g(z1), z2))), ACTIVATE(n__f(g(z1), z2))) F(g(z0), n__f(g(g(y0)), z2)) -> c(F(z0, n__f(g(z0), n__f(g(g(y0)), z2))), ACTIVATE(n__f(g(g(y0)), z2))) F(g(z0), n__f(g(z1), n__f(g(y1), n__f(g(y2), y3)))) -> c(F(z0, n__f(g(z0), n__f(g(z1), n__f(g(y1), n__f(g(y2), y3))))), ACTIVATE(n__f(g(z1), n__f(g(y1), n__f(g(y2), y3))))) F(g(z0), n__f(g(z1), n__f(g(y1), n__f(y2, y3)))) -> c(F(z0, n__f(g(z0), n__f(g(z1), n__f(g(y1), n__f(y2, y3))))), ACTIVATE(n__f(g(z1), n__f(g(y1), n__f(y2, y3))))) F(g(z0), n__f(g(g(y0)), n__f(y1, y2))) -> c(F(z0, n__f(g(z0), n__f(g(g(y0)), n__f(y1, y2)))), ACTIVATE(n__f(g(g(y0)), n__f(y1, y2)))) F(g(z0), n__f(g(g(g(y0))), n__f(y1, y2))) -> c(F(z0, n__f(g(z0), n__f(g(g(g(y0))), n__f(y1, y2)))), ACTIVATE(n__f(g(g(g(y0))), n__f(y1, y2)))) F(g(z0), n__f(g(g(y0)), n__f(g(y1), y2))) -> c(F(z0, n__f(g(z0), n__f(g(g(y0)), n__f(g(y1), y2)))), ACTIVATE(n__f(g(g(y0)), n__f(g(y1), y2)))) F(g(g(g(g(g(y0))))), n__f(g(z1), z2)) -> c(F(g(g(g(g(y0)))), n__f(g(g(g(g(g(y0))))), n__f(g(z1), z2))), ACTIVATE(n__f(g(z1), z2))) F(g(g(y0)), n__f(g(z1), n__f(g(y3), y4))) -> c(F(g(y0), n__f(g(g(y0)), n__f(g(z1), n__f(g(y3), y4)))), ACTIVATE(n__f(g(z1), n__f(g(y3), y4)))) F(g(g(y0)), n__f(g(z1), n__f(y3, y4))) -> c(F(g(y0), n__f(g(g(y0)), n__f(g(z1), n__f(y3, y4)))), ACTIVATE(n__f(g(z1), n__f(y3, y4)))) F(g(g(g(g(g(g(y0)))))), n__f(g(z1), z2)) -> c(F(g(g(g(g(g(y0))))), n__f(g(g(g(g(g(g(y0)))))), n__f(g(z1), z2))), ACTIVATE(n__f(g(z1), z2))) ---------------------------------------- (60) Obligation: Complexity Dependency Tuples Problem Rules: f(g(z0), z1) -> f(z0, n__f(g(z0), activate(z1))) f(z0, z1) -> n__f(z0, z1) activate(n__f(z0, z1)) -> f(z0, z1) activate(z0) -> z0 Tuples: F(g(x0), n__f(g(z0), z1)) -> c(F(x0, n__f(g(x0), f(z0, n__f(g(z0), activate(z1))))), ACTIVATE(n__f(g(z0), z1))) ACTIVATE(n__f(g(y0), n__f(g(y1), y2))) -> c2(F(g(y0), n__f(g(y1), y2))) F(g(g(y0)), z1) -> c(F(g(y0), n__f(g(g(y0)), z1)), ACTIVATE(z1)) F(g(z0), n__f(g(y0), n__f(g(y1), y2))) -> c(F(z0, n__f(g(z0), n__f(g(y0), n__f(g(y1), y2)))), ACTIVATE(n__f(g(y0), n__f(g(y1), y2)))) F(g(z0), n__f(g(y0), n__f(y1, y2))) -> c(F(z0, n__f(g(z0), n__f(g(y0), n__f(y1, y2)))), ACTIVATE(n__f(g(y0), n__f(y1, y2)))) F(g(g(y0)), n__f(z1, z2)) -> c(F(g(y0), n__f(g(g(y0)), n__f(z1, z2))), ACTIVATE(n__f(z1, z2))) F(g(g(g(y0))), n__f(z1, z2)) -> c(F(g(g(y0)), n__f(g(g(g(y0))), n__f(z1, z2))), ACTIVATE(n__f(z1, z2))) F(g(g(y0)), n__f(g(y2), z2)) -> c(F(g(y0), n__f(g(g(y0)), n__f(g(y2), z2))), ACTIVATE(n__f(g(y2), z2))) ACTIVATE(n__f(g(g(y0)), z1)) -> c2(F(g(g(y0)), z1)) ACTIVATE(n__f(g(z0), n__f(g(y1), n__f(g(y2), y3)))) -> c2(F(g(z0), n__f(g(y1), n__f(g(y2), y3)))) ACTIVATE(n__f(g(z0), n__f(g(y1), n__f(y2, y3)))) -> c2(F(g(z0), n__f(g(y1), n__f(y2, y3)))) ACTIVATE(n__f(g(g(y0)), n__f(y1, y2))) -> c2(F(g(g(y0)), n__f(y1, y2))) ACTIVATE(n__f(g(g(g(y0))), n__f(y1, y2))) -> c2(F(g(g(g(y0))), n__f(y1, y2))) ACTIVATE(n__f(g(g(y0)), n__f(g(y1), y2))) -> c2(F(g(g(y0)), n__f(g(y1), y2))) F(g(g(g(y0))), n__f(g(z1), z2)) -> c(F(g(g(y0)), n__f(g(g(g(y0))), n__f(g(z1), z2))), ACTIVATE(n__f(g(z1), z2))) F(g(g(g(g(y0)))), n__f(g(z1), z2)) -> c(F(g(g(g(y0))), n__f(g(g(g(g(y0)))), n__f(g(z1), z2))), ACTIVATE(n__f(g(z1), z2))) F(g(z0), n__f(g(g(y0)), z2)) -> c(F(z0, n__f(g(z0), n__f(g(g(y0)), z2))), ACTIVATE(n__f(g(g(y0)), z2))) F(g(z0), n__f(g(z1), n__f(g(y1), n__f(g(y2), y3)))) -> c(F(z0, n__f(g(z0), n__f(g(z1), n__f(g(y1), n__f(g(y2), y3))))), ACTIVATE(n__f(g(z1), n__f(g(y1), n__f(g(y2), y3))))) F(g(z0), n__f(g(z1), n__f(g(y1), n__f(y2, y3)))) -> c(F(z0, n__f(g(z0), n__f(g(z1), n__f(g(y1), n__f(y2, y3))))), ACTIVATE(n__f(g(z1), n__f(g(y1), n__f(y2, y3))))) F(g(z0), n__f(g(g(y0)), n__f(y1, y2))) -> c(F(z0, n__f(g(z0), n__f(g(g(y0)), n__f(y1, y2)))), ACTIVATE(n__f(g(g(y0)), n__f(y1, y2)))) F(g(z0), n__f(g(g(g(y0))), n__f(y1, y2))) -> c(F(z0, n__f(g(z0), n__f(g(g(g(y0))), n__f(y1, y2)))), ACTIVATE(n__f(g(g(g(y0))), n__f(y1, y2)))) F(g(z0), n__f(g(g(y0)), n__f(g(y1), y2))) -> c(F(z0, n__f(g(z0), n__f(g(g(y0)), n__f(g(y1), y2)))), ACTIVATE(n__f(g(g(y0)), n__f(g(y1), y2)))) F(g(g(y0)), n__f(g(z1), n__f(z2, z3))) -> c(F(g(y0), n__f(g(g(y0)), n__f(g(z1), n__f(z2, z3)))), ACTIVATE(n__f(g(z1), n__f(z2, z3)))) F(g(g(g(y0))), n__f(g(z1), n__f(z2, z3))) -> c(F(g(g(y0)), n__f(g(g(g(y0))), n__f(g(z1), n__f(z2, z3)))), ACTIVATE(n__f(g(z1), n__f(z2, z3)))) F(g(g(g(g(y0)))), n__f(g(z1), n__f(z2, z3))) -> c(F(g(g(g(y0))), n__f(g(g(g(g(y0)))), n__f(g(z1), n__f(z2, z3)))), ACTIVATE(n__f(g(z1), n__f(z2, z3)))) F(g(g(g(g(g(y0))))), n__f(g(z1), n__f(z2, z3))) -> c(F(g(g(g(g(y0)))), n__f(g(g(g(g(g(y0))))), n__f(g(z1), n__f(z2, z3)))), ACTIVATE(n__f(g(z1), n__f(z2, z3)))) F(g(g(y0)), n__f(g(z1), n__f(g(y3), z3))) -> c(F(g(y0), n__f(g(g(y0)), n__f(g(z1), n__f(g(y3), z3)))), ACTIVATE(n__f(g(z1), n__f(g(y3), z3)))) F(g(g(g(g(g(y0))))), n__f(g(z1), z2)) -> c(F(g(g(g(g(y0)))), n__f(g(g(g(g(g(y0))))), n__f(g(z1), z2))), ACTIVATE(n__f(g(z1), z2))) F(g(g(g(g(g(g(y0)))))), n__f(g(z1), z2)) -> c(F(g(g(g(g(g(y0))))), n__f(g(g(g(g(g(g(y0)))))), n__f(g(z1), z2))), ACTIVATE(n__f(g(z1), z2))) S tuples: F(g(x0), n__f(g(z0), z1)) -> c(F(x0, n__f(g(x0), f(z0, n__f(g(z0), activate(z1))))), ACTIVATE(n__f(g(z0), z1))) ACTIVATE(n__f(g(y0), n__f(g(y1), y2))) -> c2(F(g(y0), n__f(g(y1), y2))) F(g(g(y0)), z1) -> c(F(g(y0), n__f(g(g(y0)), z1)), ACTIVATE(z1)) F(g(z0), n__f(g(y0), n__f(g(y1), y2))) -> c(F(z0, n__f(g(z0), n__f(g(y0), n__f(g(y1), y2)))), ACTIVATE(n__f(g(y0), n__f(g(y1), y2)))) F(g(g(y0)), n__f(z1, z2)) -> c(F(g(y0), n__f(g(g(y0)), n__f(z1, z2))), ACTIVATE(n__f(z1, z2))) F(g(g(g(y0))), n__f(z1, z2)) -> c(F(g(g(y0)), n__f(g(g(g(y0))), n__f(z1, z2))), ACTIVATE(n__f(z1, z2))) F(g(g(y0)), n__f(g(y2), z2)) -> c(F(g(y0), n__f(g(g(y0)), n__f(g(y2), z2))), ACTIVATE(n__f(g(y2), z2))) ACTIVATE(n__f(g(g(y0)), z1)) -> c2(F(g(g(y0)), z1)) ACTIVATE(n__f(g(z0), n__f(g(y1), n__f(g(y2), y3)))) -> c2(F(g(z0), n__f(g(y1), n__f(g(y2), y3)))) ACTIVATE(n__f(g(z0), n__f(g(y1), n__f(y2, y3)))) -> c2(F(g(z0), n__f(g(y1), n__f(y2, y3)))) ACTIVATE(n__f(g(g(y0)), n__f(y1, y2))) -> c2(F(g(g(y0)), n__f(y1, y2))) ACTIVATE(n__f(g(g(g(y0))), n__f(y1, y2))) -> c2(F(g(g(g(y0))), n__f(y1, y2))) ACTIVATE(n__f(g(g(y0)), n__f(g(y1), y2))) -> c2(F(g(g(y0)), n__f(g(y1), y2))) F(g(g(g(y0))), n__f(g(z1), z2)) -> c(F(g(g(y0)), n__f(g(g(g(y0))), n__f(g(z1), z2))), ACTIVATE(n__f(g(z1), z2))) F(g(g(g(g(y0)))), n__f(g(z1), z2)) -> c(F(g(g(g(y0))), n__f(g(g(g(g(y0)))), n__f(g(z1), z2))), ACTIVATE(n__f(g(z1), z2))) F(g(z0), n__f(g(g(y0)), z2)) -> c(F(z0, n__f(g(z0), n__f(g(g(y0)), z2))), ACTIVATE(n__f(g(g(y0)), z2))) F(g(z0), n__f(g(z1), n__f(g(y1), n__f(g(y2), y3)))) -> c(F(z0, n__f(g(z0), n__f(g(z1), n__f(g(y1), n__f(g(y2), y3))))), ACTIVATE(n__f(g(z1), n__f(g(y1), n__f(g(y2), y3))))) F(g(z0), n__f(g(z1), n__f(g(y1), n__f(y2, y3)))) -> c(F(z0, n__f(g(z0), n__f(g(z1), n__f(g(y1), n__f(y2, y3))))), ACTIVATE(n__f(g(z1), n__f(g(y1), n__f(y2, y3))))) F(g(z0), n__f(g(g(y0)), n__f(y1, y2))) -> c(F(z0, n__f(g(z0), n__f(g(g(y0)), n__f(y1, y2)))), ACTIVATE(n__f(g(g(y0)), n__f(y1, y2)))) F(g(z0), n__f(g(g(g(y0))), n__f(y1, y2))) -> c(F(z0, n__f(g(z0), n__f(g(g(g(y0))), n__f(y1, y2)))), ACTIVATE(n__f(g(g(g(y0))), n__f(y1, y2)))) F(g(z0), n__f(g(g(y0)), n__f(g(y1), y2))) -> c(F(z0, n__f(g(z0), n__f(g(g(y0)), n__f(g(y1), y2)))), ACTIVATE(n__f(g(g(y0)), n__f(g(y1), y2)))) F(g(g(y0)), n__f(g(z1), n__f(z2, z3))) -> c(F(g(y0), n__f(g(g(y0)), n__f(g(z1), n__f(z2, z3)))), ACTIVATE(n__f(g(z1), n__f(z2, z3)))) F(g(g(g(y0))), n__f(g(z1), n__f(z2, z3))) -> c(F(g(g(y0)), n__f(g(g(g(y0))), n__f(g(z1), n__f(z2, z3)))), ACTIVATE(n__f(g(z1), n__f(z2, z3)))) F(g(g(g(g(y0)))), n__f(g(z1), n__f(z2, z3))) -> c(F(g(g(g(y0))), n__f(g(g(g(g(y0)))), n__f(g(z1), n__f(z2, z3)))), ACTIVATE(n__f(g(z1), n__f(z2, z3)))) F(g(g(g(g(g(y0))))), n__f(g(z1), n__f(z2, z3))) -> c(F(g(g(g(g(y0)))), n__f(g(g(g(g(g(y0))))), n__f(g(z1), n__f(z2, z3)))), ACTIVATE(n__f(g(z1), n__f(z2, z3)))) F(g(g(y0)), n__f(g(z1), n__f(g(y3), z3))) -> c(F(g(y0), n__f(g(g(y0)), n__f(g(z1), n__f(g(y3), z3)))), ACTIVATE(n__f(g(z1), n__f(g(y3), z3)))) K tuples:none Defined Rule Symbols: f_2, activate_1 Defined Pair Symbols: F_2, ACTIVATE_1 Compound Symbols: c_2, c2_1 ---------------------------------------- (61) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID)) Use forward instantiation to replace F(g(z0), n__f(g(y0), n__f(y1, y2))) -> c(F(z0, n__f(g(z0), n__f(g(y0), n__f(y1, y2)))), ACTIVATE(n__f(g(y0), n__f(y1, y2)))) by F(g(g(y0)), n__f(g(z1), n__f(z2, z3))) -> c(F(g(y0), n__f(g(g(y0)), n__f(g(z1), n__f(z2, z3)))), ACTIVATE(n__f(g(z1), n__f(z2, z3)))) F(g(z0), n__f(g(z1), n__f(g(y1), z3))) -> c(F(z0, n__f(g(z0), n__f(g(z1), n__f(g(y1), z3)))), ACTIVATE(n__f(g(z1), n__f(g(y1), z3)))) F(g(g(g(y0))), n__f(g(z1), n__f(z2, z3))) -> c(F(g(g(y0)), n__f(g(g(g(y0))), n__f(g(z1), n__f(z2, z3)))), ACTIVATE(n__f(g(z1), n__f(z2, z3)))) F(g(g(g(g(y0)))), n__f(g(z1), n__f(z2, z3))) -> c(F(g(g(g(y0))), n__f(g(g(g(g(y0)))), n__f(g(z1), n__f(z2, z3)))), ACTIVATE(n__f(g(z1), n__f(z2, z3)))) F(g(z0), n__f(g(g(y0)), n__f(z2, z3))) -> c(F(z0, n__f(g(z0), n__f(g(g(y0)), n__f(z2, z3)))), ACTIVATE(n__f(g(g(y0)), n__f(z2, z3)))) F(g(z0), n__f(g(z1), n__f(g(y1), n__f(g(y2), y3)))) -> c(F(z0, n__f(g(z0), n__f(g(z1), n__f(g(y1), n__f(g(y2), y3))))), ACTIVATE(n__f(g(z1), n__f(g(y1), n__f(g(y2), y3))))) F(g(z0), n__f(g(z1), n__f(g(y1), n__f(y2, y3)))) -> c(F(z0, n__f(g(z0), n__f(g(z1), n__f(g(y1), n__f(y2, y3))))), ACTIVATE(n__f(g(z1), n__f(g(y1), n__f(y2, y3))))) F(g(z0), n__f(g(g(g(y0))), n__f(z2, z3))) -> c(F(z0, n__f(g(z0), n__f(g(g(g(y0))), n__f(z2, z3)))), ACTIVATE(n__f(g(g(g(y0))), n__f(z2, z3)))) F(g(z0), n__f(g(g(y0)), n__f(g(y1), z3))) -> c(F(z0, n__f(g(z0), n__f(g(g(y0)), n__f(g(y1), z3)))), ACTIVATE(n__f(g(g(y0)), n__f(g(y1), z3)))) F(g(g(g(g(g(y0))))), n__f(g(z1), n__f(z2, z3))) -> c(F(g(g(g(g(y0)))), n__f(g(g(g(g(g(y0))))), n__f(g(z1), n__f(z2, z3)))), ACTIVATE(n__f(g(z1), n__f(z2, z3)))) F(g(g(y0)), n__f(g(z1), n__f(g(y3), z3))) -> c(F(g(y0), n__f(g(g(y0)), n__f(g(z1), n__f(g(y3), z3)))), ACTIVATE(n__f(g(z1), n__f(g(y3), z3)))) F(g(g(g(g(g(g(y0)))))), n__f(g(z1), n__f(z2, z3))) -> c(F(g(g(g(g(g(y0))))), n__f(g(g(g(g(g(g(y0)))))), n__f(g(z1), n__f(z2, z3)))), ACTIVATE(n__f(g(z1), n__f(z2, z3)))) F(g(g(g(g(g(g(g(y0))))))), n__f(g(z1), n__f(z2, z3))) -> c(F(g(g(g(g(g(g(y0)))))), n__f(g(g(g(g(g(g(g(y0))))))), n__f(g(z1), n__f(z2, z3)))), ACTIVATE(n__f(g(z1), n__f(z2, z3)))) ---------------------------------------- (62) Obligation: Complexity Dependency Tuples Problem Rules: f(g(z0), z1) -> f(z0, n__f(g(z0), activate(z1))) f(z0, z1) -> n__f(z0, z1) activate(n__f(z0, z1)) -> f(z0, z1) activate(z0) -> z0 Tuples: F(g(x0), n__f(g(z0), z1)) -> c(F(x0, n__f(g(x0), f(z0, n__f(g(z0), activate(z1))))), ACTIVATE(n__f(g(z0), z1))) ACTIVATE(n__f(g(y0), n__f(g(y1), y2))) -> c2(F(g(y0), n__f(g(y1), y2))) F(g(g(y0)), z1) -> c(F(g(y0), n__f(g(g(y0)), z1)), ACTIVATE(z1)) F(g(z0), n__f(g(y0), n__f(g(y1), y2))) -> c(F(z0, n__f(g(z0), n__f(g(y0), n__f(g(y1), y2)))), ACTIVATE(n__f(g(y0), n__f(g(y1), y2)))) F(g(g(y0)), n__f(z1, z2)) -> c(F(g(y0), n__f(g(g(y0)), n__f(z1, z2))), ACTIVATE(n__f(z1, z2))) F(g(g(g(y0))), n__f(z1, z2)) -> c(F(g(g(y0)), n__f(g(g(g(y0))), n__f(z1, z2))), ACTIVATE(n__f(z1, z2))) F(g(g(y0)), n__f(g(y2), z2)) -> c(F(g(y0), n__f(g(g(y0)), n__f(g(y2), z2))), ACTIVATE(n__f(g(y2), z2))) ACTIVATE(n__f(g(g(y0)), z1)) -> c2(F(g(g(y0)), z1)) ACTIVATE(n__f(g(z0), n__f(g(y1), n__f(g(y2), y3)))) -> c2(F(g(z0), n__f(g(y1), n__f(g(y2), y3)))) ACTIVATE(n__f(g(z0), n__f(g(y1), n__f(y2, y3)))) -> c2(F(g(z0), n__f(g(y1), n__f(y2, y3)))) ACTIVATE(n__f(g(g(y0)), n__f(y1, y2))) -> c2(F(g(g(y0)), n__f(y1, y2))) ACTIVATE(n__f(g(g(g(y0))), n__f(y1, y2))) -> c2(F(g(g(g(y0))), n__f(y1, y2))) ACTIVATE(n__f(g(g(y0)), n__f(g(y1), y2))) -> c2(F(g(g(y0)), n__f(g(y1), y2))) F(g(g(g(y0))), n__f(g(z1), z2)) -> c(F(g(g(y0)), n__f(g(g(g(y0))), n__f(g(z1), z2))), ACTIVATE(n__f(g(z1), z2))) F(g(g(g(g(y0)))), n__f(g(z1), z2)) -> c(F(g(g(g(y0))), n__f(g(g(g(g(y0)))), n__f(g(z1), z2))), ACTIVATE(n__f(g(z1), z2))) F(g(z0), n__f(g(g(y0)), z2)) -> c(F(z0, n__f(g(z0), n__f(g(g(y0)), z2))), ACTIVATE(n__f(g(g(y0)), z2))) F(g(z0), n__f(g(z1), n__f(g(y1), n__f(g(y2), y3)))) -> c(F(z0, n__f(g(z0), n__f(g(z1), n__f(g(y1), n__f(g(y2), y3))))), ACTIVATE(n__f(g(z1), n__f(g(y1), n__f(g(y2), y3))))) F(g(z0), n__f(g(z1), n__f(g(y1), n__f(y2, y3)))) -> c(F(z0, n__f(g(z0), n__f(g(z1), n__f(g(y1), n__f(y2, y3))))), ACTIVATE(n__f(g(z1), n__f(g(y1), n__f(y2, y3))))) F(g(z0), n__f(g(g(y0)), n__f(y1, y2))) -> c(F(z0, n__f(g(z0), n__f(g(g(y0)), n__f(y1, y2)))), ACTIVATE(n__f(g(g(y0)), n__f(y1, y2)))) F(g(z0), n__f(g(g(g(y0))), n__f(y1, y2))) -> c(F(z0, n__f(g(z0), n__f(g(g(g(y0))), n__f(y1, y2)))), ACTIVATE(n__f(g(g(g(y0))), n__f(y1, y2)))) F(g(z0), n__f(g(g(y0)), n__f(g(y1), y2))) -> c(F(z0, n__f(g(z0), n__f(g(g(y0)), n__f(g(y1), y2)))), ACTIVATE(n__f(g(g(y0)), n__f(g(y1), y2)))) F(g(g(y0)), n__f(g(z1), n__f(z2, z3))) -> c(F(g(y0), n__f(g(g(y0)), n__f(g(z1), n__f(z2, z3)))), ACTIVATE(n__f(g(z1), n__f(z2, z3)))) F(g(g(g(y0))), n__f(g(z1), n__f(z2, z3))) -> c(F(g(g(y0)), n__f(g(g(g(y0))), n__f(g(z1), n__f(z2, z3)))), ACTIVATE(n__f(g(z1), n__f(z2, z3)))) F(g(g(g(g(y0)))), n__f(g(z1), n__f(z2, z3))) -> c(F(g(g(g(y0))), n__f(g(g(g(g(y0)))), n__f(g(z1), n__f(z2, z3)))), ACTIVATE(n__f(g(z1), n__f(z2, z3)))) F(g(g(g(g(g(y0))))), n__f(g(z1), n__f(z2, z3))) -> c(F(g(g(g(g(y0)))), n__f(g(g(g(g(g(y0))))), n__f(g(z1), n__f(z2, z3)))), ACTIVATE(n__f(g(z1), n__f(z2, z3)))) F(g(g(y0)), n__f(g(z1), n__f(g(y3), z3))) -> c(F(g(y0), n__f(g(g(y0)), n__f(g(z1), n__f(g(y3), z3)))), ACTIVATE(n__f(g(z1), n__f(g(y3), z3)))) F(g(g(g(g(g(y0))))), n__f(g(z1), z2)) -> c(F(g(g(g(g(y0)))), n__f(g(g(g(g(g(y0))))), n__f(g(z1), z2))), ACTIVATE(n__f(g(z1), z2))) F(g(g(g(g(g(g(y0)))))), n__f(g(z1), z2)) -> c(F(g(g(g(g(g(y0))))), n__f(g(g(g(g(g(g(y0)))))), n__f(g(z1), z2))), ACTIVATE(n__f(g(z1), z2))) F(g(g(g(g(g(g(y0)))))), n__f(g(z1), n__f(z2, z3))) -> c(F(g(g(g(g(g(y0))))), n__f(g(g(g(g(g(g(y0)))))), n__f(g(z1), n__f(z2, z3)))), ACTIVATE(n__f(g(z1), n__f(z2, z3)))) F(g(g(g(g(g(g(g(y0))))))), n__f(g(z1), n__f(z2, z3))) -> c(F(g(g(g(g(g(g(y0)))))), n__f(g(g(g(g(g(g(g(y0))))))), n__f(g(z1), n__f(z2, z3)))), ACTIVATE(n__f(g(z1), n__f(z2, z3)))) S tuples: F(g(x0), n__f(g(z0), z1)) -> c(F(x0, n__f(g(x0), f(z0, n__f(g(z0), activate(z1))))), ACTIVATE(n__f(g(z0), z1))) ACTIVATE(n__f(g(y0), n__f(g(y1), y2))) -> c2(F(g(y0), n__f(g(y1), y2))) F(g(g(y0)), z1) -> c(F(g(y0), n__f(g(g(y0)), z1)), ACTIVATE(z1)) F(g(z0), n__f(g(y0), n__f(g(y1), y2))) -> c(F(z0, n__f(g(z0), n__f(g(y0), n__f(g(y1), y2)))), ACTIVATE(n__f(g(y0), n__f(g(y1), y2)))) F(g(g(y0)), n__f(z1, z2)) -> c(F(g(y0), n__f(g(g(y0)), n__f(z1, z2))), ACTIVATE(n__f(z1, z2))) F(g(g(g(y0))), n__f(z1, z2)) -> c(F(g(g(y0)), n__f(g(g(g(y0))), n__f(z1, z2))), ACTIVATE(n__f(z1, z2))) F(g(g(y0)), n__f(g(y2), z2)) -> c(F(g(y0), n__f(g(g(y0)), n__f(g(y2), z2))), ACTIVATE(n__f(g(y2), z2))) ACTIVATE(n__f(g(g(y0)), z1)) -> c2(F(g(g(y0)), z1)) ACTIVATE(n__f(g(z0), n__f(g(y1), n__f(g(y2), y3)))) -> c2(F(g(z0), n__f(g(y1), n__f(g(y2), y3)))) ACTIVATE(n__f(g(z0), n__f(g(y1), n__f(y2, y3)))) -> c2(F(g(z0), n__f(g(y1), n__f(y2, y3)))) ACTIVATE(n__f(g(g(y0)), n__f(y1, y2))) -> c2(F(g(g(y0)), n__f(y1, y2))) ACTIVATE(n__f(g(g(g(y0))), n__f(y1, y2))) -> c2(F(g(g(g(y0))), n__f(y1, y2))) ACTIVATE(n__f(g(g(y0)), n__f(g(y1), y2))) -> c2(F(g(g(y0)), n__f(g(y1), y2))) F(g(g(g(y0))), n__f(g(z1), z2)) -> c(F(g(g(y0)), n__f(g(g(g(y0))), n__f(g(z1), z2))), ACTIVATE(n__f(g(z1), z2))) F(g(g(g(g(y0)))), n__f(g(z1), z2)) -> c(F(g(g(g(y0))), n__f(g(g(g(g(y0)))), n__f(g(z1), z2))), ACTIVATE(n__f(g(z1), z2))) F(g(z0), n__f(g(g(y0)), z2)) -> c(F(z0, n__f(g(z0), n__f(g(g(y0)), z2))), ACTIVATE(n__f(g(g(y0)), z2))) F(g(z0), n__f(g(z1), n__f(g(y1), n__f(g(y2), y3)))) -> c(F(z0, n__f(g(z0), n__f(g(z1), n__f(g(y1), n__f(g(y2), y3))))), ACTIVATE(n__f(g(z1), n__f(g(y1), n__f(g(y2), y3))))) F(g(z0), n__f(g(z1), n__f(g(y1), n__f(y2, y3)))) -> c(F(z0, n__f(g(z0), n__f(g(z1), n__f(g(y1), n__f(y2, y3))))), ACTIVATE(n__f(g(z1), n__f(g(y1), n__f(y2, y3))))) F(g(z0), n__f(g(g(y0)), n__f(y1, y2))) -> c(F(z0, n__f(g(z0), n__f(g(g(y0)), n__f(y1, y2)))), ACTIVATE(n__f(g(g(y0)), n__f(y1, y2)))) F(g(z0), n__f(g(g(g(y0))), n__f(y1, y2))) -> c(F(z0, n__f(g(z0), n__f(g(g(g(y0))), n__f(y1, y2)))), ACTIVATE(n__f(g(g(g(y0))), n__f(y1, y2)))) F(g(z0), n__f(g(g(y0)), n__f(g(y1), y2))) -> c(F(z0, n__f(g(z0), n__f(g(g(y0)), n__f(g(y1), y2)))), ACTIVATE(n__f(g(g(y0)), n__f(g(y1), y2)))) F(g(g(y0)), n__f(g(z1), n__f(z2, z3))) -> c(F(g(y0), n__f(g(g(y0)), n__f(g(z1), n__f(z2, z3)))), ACTIVATE(n__f(g(z1), n__f(z2, z3)))) F(g(g(g(y0))), n__f(g(z1), n__f(z2, z3))) -> c(F(g(g(y0)), n__f(g(g(g(y0))), n__f(g(z1), n__f(z2, z3)))), ACTIVATE(n__f(g(z1), n__f(z2, z3)))) F(g(g(g(g(y0)))), n__f(g(z1), n__f(z2, z3))) -> c(F(g(g(g(y0))), n__f(g(g(g(g(y0)))), n__f(g(z1), n__f(z2, z3)))), ACTIVATE(n__f(g(z1), n__f(z2, z3)))) F(g(g(g(g(g(y0))))), n__f(g(z1), n__f(z2, z3))) -> c(F(g(g(g(g(y0)))), n__f(g(g(g(g(g(y0))))), n__f(g(z1), n__f(z2, z3)))), ACTIVATE(n__f(g(z1), n__f(z2, z3)))) F(g(g(y0)), n__f(g(z1), n__f(g(y3), z3))) -> c(F(g(y0), n__f(g(g(y0)), n__f(g(z1), n__f(g(y3), z3)))), ACTIVATE(n__f(g(z1), n__f(g(y3), z3)))) K tuples:none Defined Rule Symbols: f_2, activate_1 Defined Pair Symbols: F_2, ACTIVATE_1 Compound Symbols: c_2, c2_1 ---------------------------------------- (63) RelTrsToWeightedTrsProof (UPPER BOUND(ID)) Transformed relative TRS to weighted TRS ---------------------------------------- (64) 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(g(X), Y) -> f(X, n__f(g(X), activate(Y))) [1] f(X1, X2) -> n__f(X1, X2) [1] activate(n__f(X1, X2)) -> f(X1, X2) [1] activate(X) -> X [1] Rewrite Strategy: INNERMOST ---------------------------------------- (65) TypeInferenceProof (BOTH BOUNDS(ID, ID)) Infered types. ---------------------------------------- (66) Obligation: Runtime Complexity Weighted TRS with Types. The TRS R consists of the following rules: f(g(X), Y) -> f(X, n__f(g(X), activate(Y))) [1] f(X1, X2) -> n__f(X1, X2) [1] activate(n__f(X1, X2)) -> f(X1, X2) [1] activate(X) -> X [1] The TRS has the following type information: f :: g -> n__f -> n__f g :: g -> g n__f :: g -> n__f -> n__f activate :: n__f -> n__f Rewrite Strategy: INNERMOST ---------------------------------------- (67) 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: activate_1 f_2 Due to the following rules being added: none And the following fresh constants: const, const1 ---------------------------------------- (68) 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(g(X), Y) -> f(X, n__f(g(X), activate(Y))) [1] f(X1, X2) -> n__f(X1, X2) [1] activate(n__f(X1, X2)) -> f(X1, X2) [1] activate(X) -> X [1] The TRS has the following type information: f :: g -> n__f -> n__f g :: g -> g n__f :: g -> n__f -> n__f activate :: n__f -> n__f const :: n__f const1 :: g Rewrite Strategy: INNERMOST ---------------------------------------- (69) NarrowingProof (BOTH BOUNDS(ID, ID)) Narrowed the inner basic terms of all right-hand sides by a single narrowing step. ---------------------------------------- (70) 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(g(X), n__f(X1', X2')) -> f(X, n__f(g(X), f(X1', X2'))) [2] f(g(X), Y) -> f(X, n__f(g(X), Y)) [2] f(X1, X2) -> n__f(X1, X2) [1] activate(n__f(X1, X2)) -> f(X1, X2) [1] activate(X) -> X [1] The TRS has the following type information: f :: g -> n__f -> n__f g :: g -> g n__f :: g -> n__f -> n__f activate :: n__f -> n__f const :: n__f const1 :: g Rewrite Strategy: INNERMOST ---------------------------------------- (71) CpxTypedWeightedTrsToRntsProof (UPPER BOUND(ID)) Transformed the TRS into an over-approximating RNTS by (improved) Size Abstraction. The constant constructors are abstracted as follows: const => 0 const1 => 0 ---------------------------------------- (72) Obligation: Complexity RNTS consisting of the following rules: activate(z) -{ 1 }-> X :|: X >= 0, z = X activate(z) -{ 1 }-> f(X1, X2) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2 f(z, z') -{ 2 }-> f(X, 1 + (1 + X) + Y) :|: z = 1 + X, z' = Y, Y >= 0, X >= 0 f(z, z') -{ 2 }-> f(X, 1 + (1 + X) + f(X1', X2')) :|: z = 1 + X, z' = 1 + X1' + X2', X2' >= 0, X1' >= 0, X >= 0 f(z, z') -{ 1 }-> 1 + X1 + X2 :|: X1 >= 0, X2 >= 0, z = X1, z' = X2 ---------------------------------------- (73) SimplificationProof (BOTH BOUNDS(ID, ID)) Simplified the RNTS by moving equalities from the constraints into the right-hand sides. ---------------------------------------- (74) Obligation: Complexity RNTS consisting of the following rules: activate(z) -{ 1 }-> z :|: z >= 0 activate(z) -{ 1 }-> f(X1, X2) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2 f(z, z') -{ 2 }-> f(z - 1, 1 + (1 + (z - 1)) + z') :|: z' >= 0, z - 1 >= 0 f(z, z') -{ 2 }-> f(z - 1, 1 + (1 + (z - 1)) + f(X1', X2')) :|: z' = 1 + X1' + X2', X2' >= 0, X1' >= 0, z - 1 >= 0 f(z, z') -{ 1 }-> 1 + z + z' :|: z >= 0, z' >= 0 ---------------------------------------- (75) 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: const, const1 ---------------------------------------- (76) 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(g(X), Y) -> f(X, n__f(g(X), activate(Y))) [1] f(X1, X2) -> n__f(X1, X2) [1] activate(n__f(X1, X2)) -> f(X1, X2) [1] activate(X) -> X [1] The TRS has the following type information: f :: g -> n__f -> n__f g :: g -> g n__f :: g -> n__f -> n__f activate :: n__f -> n__f const :: n__f const1 :: g Rewrite Strategy: INNERMOST ---------------------------------------- (77) CpxTypedWeightedTrsToRntsProof (UPPER BOUND(ID)) Transformed the TRS into an over-approximating RNTS by (improved) Size Abstraction. The constant constructors are abstracted as follows: const => 0 const1 => 0 ---------------------------------------- (78) Obligation: Complexity RNTS consisting of the following rules: activate(z) -{ 1 }-> X :|: X >= 0, z = X activate(z) -{ 1 }-> f(X1, X2) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2 f(z, z') -{ 1 }-> f(X, 1 + (1 + X) + activate(Y)) :|: z = 1 + X, z' = Y, Y >= 0, X >= 0 f(z, z') -{ 1 }-> 1 + X1 + X2 :|: X1 >= 0, X2 >= 0, z = X1, z' = X2 Only complete derivations are relevant for the runtime complexity.