KILLED proof of input_NhW9BAFUoZ.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) CpxTrsToCdtProof [UPPER BOUND(ID), 0 ms] (4) CdtProblem (5) CdtToCpxRelTrsProof [BOTH BOUNDS(ID, ID), 0 ms] (6) CpxRelTRS (7) RenamingProof [BOTH BOUNDS(ID, ID), 0 ms] (8) CpxRelTRS (9) TypeInferenceProof [BOTH BOUNDS(ID, ID), 0 ms] (10) typed CpxTrs (11) OrderProof [LOWER BOUND(ID), 15 ms] (12) typed CpxTrs (13) RewriteLemmaProof [LOWER BOUND(ID), 522 ms] (14) typed CpxTrs (15) RelTrsToDecreasingLoopProblemProof [LOWER BOUND(ID), 0 ms] (16) TRS for Loop Detection (17) RelTrsToTrsProof [UPPER BOUND(ID), 0 ms] (18) CpxTRS (19) CpxTrsToCdtProof [UPPER BOUND(ID), 0 ms] (20) CdtProblem (21) CdtLeafRemovalProof [BOTH BOUNDS(ID, ID), 0 ms] (22) CdtProblem (23) CdtToCpxRelTrsProof [BOTH BOUNDS(ID, ID), 0 ms] (24) CpxRelTRS (25) RelTrsToTrsProof [UPPER BOUND(ID), 0 ms] (26) CpxTRS (27) RelTrsToWeightedTrsProof [BOTH BOUNDS(ID, ID), 0 ms] (28) CpxWeightedTrs (29) TypeInferenceProof [BOTH BOUNDS(ID, ID), 0 ms] (30) CpxTypedWeightedTrs (31) CompletionProof [UPPER BOUND(ID), 0 ms] (32) CpxTypedWeightedCompleteTrs (33) NarrowingProof [BOTH BOUNDS(ID, ID), 0 ms] (34) CpxTypedWeightedCompleteTrs (35) CpxTypedWeightedTrsToRntsProof [UPPER BOUND(ID), 0 ms] (36) CpxRNTS (37) SimplificationProof [BOTH BOUNDS(ID, ID), 0 ms] (38) CpxRNTS (39) CompletionProof [UPPER BOUND(ID), 0 ms] (40) CpxTypedWeightedCompleteTrs (41) CpxTypedWeightedTrsToRntsProof [UPPER BOUND(ID), 0 ms] (42) CpxRNTS (43) CdtNarrowingProof [BOTH BOUNDS(ID, ID), 0 ms] (44) CdtProblem (45) CdtNarrowingProof [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) RelTrsToWeightedTrsProof [UPPER BOUND(ID), 0 ms] (54) CpxWeightedTrs (55) TypeInferenceProof [BOTH BOUNDS(ID, ID), 0 ms] (56) CpxTypedWeightedTrs (57) CompletionProof [UPPER BOUND(ID), 0 ms] (58) CpxTypedWeightedCompleteTrs (59) CpxTypedWeightedTrsToRntsProof [UPPER BOUND(ID), 0 ms] (60) CpxRNTS (61) CompletionProof [UPPER BOUND(ID), 0 ms] (62) CpxTypedWeightedCompleteTrs (63) NarrowingProof [BOTH BOUNDS(ID, ID), 0 ms] (64) CpxTypedWeightedCompleteTrs (65) CpxTypedWeightedTrsToRntsProof [UPPER BOUND(ID), 0 ms] (66) CpxRNTS (67) SimplificationProof [BOTH BOUNDS(ID, ID), 0 ms] (68) 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(x) -> s(x) f(s(s(x))) -> s(f(f(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(x) -> s(x) f(s(s(x))) -> s(f(f(x))) S is empty. Rewrite Strategy: PARALLEL_INNERMOST ---------------------------------------- (3) CpxTrsToCdtProof (UPPER BOUND(ID)) Converted Cpx (relative) TRS with rewrite strategy PARALLEL_INNERMOST to CDT ---------------------------------------- (4) Obligation: Complexity Dependency Tuples Problem Rules: f(z0) -> s(z0) f(s(s(z0))) -> s(f(f(z0))) Tuples: F(z0) -> c F(s(s(z0))) -> c1(F(f(z0)), F(z0)) S tuples: F(z0) -> c F(s(s(z0))) -> c1(F(f(z0)), F(z0)) K tuples:none Defined Rule Symbols: f_1 Defined Pair Symbols: F_1 Compound Symbols: c, c1_2 ---------------------------------------- (5) CdtToCpxRelTrsProof (BOTH BOUNDS(ID, ID)) Converted S to standard rules, and D \ S as well as R to relative rules. ---------------------------------------- (6) 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(z0) -> c F(s(s(z0))) -> c1(F(f(z0)), F(z0)) The (relative) TRS S consists of the following rules: f(z0) -> s(z0) f(s(s(z0))) -> s(f(f(z0))) Rewrite Strategy: INNERMOST ---------------------------------------- (7) RenamingProof (BOTH BOUNDS(ID, ID)) Renamed function symbols to avoid clashes with predefined symbol. ---------------------------------------- (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(z0) -> c F(s(s(z0))) -> c1(F(f(z0)), F(z0)) The (relative) TRS S consists of the following rules: f(z0) -> s(z0) f(s(s(z0))) -> s(f(f(z0))) Rewrite Strategy: INNERMOST ---------------------------------------- (9) TypeInferenceProof (BOTH BOUNDS(ID, ID)) Inferred types. ---------------------------------------- (10) Obligation: Innermost TRS: Rules: F(z0) -> c F(s(s(z0))) -> c1(F(f(z0)), F(z0)) f(z0) -> s(z0) f(s(s(z0))) -> s(f(f(z0))) Types: F :: s -> c:c1 c :: c:c1 s :: s -> s c1 :: c:c1 -> c:c1 -> c:c1 f :: s -> s hole_c:c11_2 :: c:c1 hole_s2_2 :: s gen_c:c13_2 :: Nat -> c:c1 gen_s4_2 :: Nat -> s ---------------------------------------- (11) OrderProof (LOWER BOUND(ID)) Heuristically decided to analyse the following defined symbols: F, f They will be analysed ascendingly in the following order: f < F ---------------------------------------- (12) Obligation: Innermost TRS: Rules: F(z0) -> c F(s(s(z0))) -> c1(F(f(z0)), F(z0)) f(z0) -> s(z0) f(s(s(z0))) -> s(f(f(z0))) Types: F :: s -> c:c1 c :: c:c1 s :: s -> s c1 :: c:c1 -> c:c1 -> c:c1 f :: s -> s hole_c:c11_2 :: c:c1 hole_s2_2 :: s gen_c:c13_2 :: Nat -> c:c1 gen_s4_2 :: Nat -> s Generator Equations: gen_c:c13_2(0) <=> c gen_c:c13_2(+(x, 1)) <=> c1(c, gen_c:c13_2(x)) gen_s4_2(0) <=> hole_s2_2 gen_s4_2(+(x, 1)) <=> s(gen_s4_2(x)) The following defined symbols remain to be analysed: f, F They will be analysed ascendingly in the following order: f < F ---------------------------------------- (13) RewriteLemmaProof (LOWER BOUND(ID)) Proved the following rewrite lemma: f(gen_s4_2(+(2, *(2, n6_2)))) -> *5_2, rt in Omega(0) Induction Base: f(gen_s4_2(+(2, *(2, 0)))) Induction Step: f(gen_s4_2(+(2, *(2, +(n6_2, 1))))) ->_R^Omega(0) s(f(f(gen_s4_2(+(2, *(2, n6_2)))))) ->_IH s(f(*5_2)) We have rt in Omega(1) and sz in O(n). Thus, we have irc_R in Omega(n^0). ---------------------------------------- (14) Obligation: Innermost TRS: Rules: F(z0) -> c F(s(s(z0))) -> c1(F(f(z0)), F(z0)) f(z0) -> s(z0) f(s(s(z0))) -> s(f(f(z0))) Types: F :: s -> c:c1 c :: c:c1 s :: s -> s c1 :: c:c1 -> c:c1 -> c:c1 f :: s -> s hole_c:c11_2 :: c:c1 hole_s2_2 :: s gen_c:c13_2 :: Nat -> c:c1 gen_s4_2 :: Nat -> s Lemmas: f(gen_s4_2(+(2, *(2, n6_2)))) -> *5_2, rt in Omega(0) Generator Equations: gen_c:c13_2(0) <=> c gen_c:c13_2(+(x, 1)) <=> c1(c, gen_c:c13_2(x)) gen_s4_2(0) <=> hole_s2_2 gen_s4_2(+(x, 1)) <=> s(gen_s4_2(x)) The following defined symbols remain to be analysed: F ---------------------------------------- (15) RelTrsToDecreasingLoopProblemProof (LOWER BOUND(ID)) Transformed a relative TRS into a decreasing-loop problem. ---------------------------------------- (16) 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(z0) -> c F(s(s(z0))) -> c1(F(f(z0)), F(z0)) The (relative) TRS S consists of the following rules: f(z0) -> s(z0) f(s(s(z0))) -> s(f(f(z0))) Rewrite Strategy: INNERMOST ---------------------------------------- (17) RelTrsToTrsProof (UPPER BOUND(ID)) transformed relative TRS to TRS ---------------------------------------- (18) 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(x) -> s(x) f(s(s(x))) -> s(f(f(x))) S is empty. Rewrite Strategy: PARALLEL_INNERMOST ---------------------------------------- (19) CpxTrsToCdtProof (UPPER BOUND(ID)) Converted Cpx (relative) TRS with rewrite strategy PARALLEL_INNERMOST to CDT ---------------------------------------- (20) Obligation: Complexity Dependency Tuples Problem Rules: f(z0) -> s(z0) f(s(s(z0))) -> s(f(f(z0))) Tuples: F(z0) -> c F(s(s(z0))) -> c1(F(f(z0)), F(z0)) S tuples: F(z0) -> c F(s(s(z0))) -> c1(F(f(z0)), F(z0)) K tuples:none Defined Rule Symbols: f_1 Defined Pair Symbols: F_1 Compound Symbols: c, c1_2 ---------------------------------------- (21) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID)) Removed 1 trailing nodes: F(z0) -> c ---------------------------------------- (22) Obligation: Complexity Dependency Tuples Problem Rules: f(z0) -> s(z0) f(s(s(z0))) -> s(f(f(z0))) Tuples: F(s(s(z0))) -> c1(F(f(z0)), F(z0)) S tuples: F(s(s(z0))) -> c1(F(f(z0)), F(z0)) K tuples:none Defined Rule Symbols: f_1 Defined Pair Symbols: F_1 Compound Symbols: c1_2 ---------------------------------------- (23) CdtToCpxRelTrsProof (BOTH BOUNDS(ID, ID)) Converted S to standard rules, and D \ S as well as R to relative rules. ---------------------------------------- (24) 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(s(s(z0))) -> c1(F(f(z0)), F(z0)) The (relative) TRS S consists of the following rules: f(z0) -> s(z0) f(s(s(z0))) -> s(f(f(z0))) Rewrite Strategy: INNERMOST ---------------------------------------- (25) RelTrsToTrsProof (UPPER BOUND(ID)) transformed relative TRS to TRS ---------------------------------------- (26) 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(s(s(z0))) -> c1(F(f(z0)), F(z0)) f(z0) -> s(z0) f(s(s(z0))) -> s(f(f(z0))) S is empty. Rewrite Strategy: INNERMOST ---------------------------------------- (27) RelTrsToWeightedTrsProof (BOTH BOUNDS(ID, ID)) Transformed relative TRS to weighted TRS ---------------------------------------- (28) 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(s(s(z0))) -> c1(F(f(z0)), F(z0)) [1] f(z0) -> s(z0) [0] f(s(s(z0))) -> s(f(f(z0))) [0] Rewrite Strategy: INNERMOST ---------------------------------------- (29) TypeInferenceProof (BOTH BOUNDS(ID, ID)) Infered types. ---------------------------------------- (30) Obligation: Runtime Complexity Weighted TRS with Types. The TRS R consists of the following rules: F(s(s(z0))) -> c1(F(f(z0)), F(z0)) [1] f(z0) -> s(z0) [0] f(s(s(z0))) -> s(f(f(z0))) [0] The TRS has the following type information: F :: s -> c1 s :: s -> s c1 :: c1 -> c1 -> c1 f :: s -> s Rewrite Strategy: INNERMOST ---------------------------------------- (31) 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_1 (c) The following functions are completely defined: f_1 Due to the following rules being added: f(v0) -> const1 [0] And the following fresh constants: const1, const ---------------------------------------- (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(s(s(z0))) -> c1(F(f(z0)), F(z0)) [1] f(z0) -> s(z0) [0] f(s(s(z0))) -> s(f(f(z0))) [0] f(v0) -> const1 [0] The TRS has the following type information: F :: s:const1 -> c1 s :: s:const1 -> s:const1 c1 :: c1 -> c1 -> c1 f :: s:const1 -> s:const1 const1 :: s:const1 const :: c1 Rewrite Strategy: INNERMOST ---------------------------------------- (33) NarrowingProof (BOTH BOUNDS(ID, ID)) Narrowed the inner basic terms of all right-hand sides by a single narrowing step. ---------------------------------------- (34) 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(s(s(z0))) -> c1(F(s(z0)), F(z0)) [1] F(s(s(s(s(z0'))))) -> c1(F(s(f(f(z0')))), F(s(s(z0')))) [1] F(s(s(z0))) -> c1(F(const1), F(z0)) [1] f(z0) -> s(z0) [0] f(s(s(z0))) -> s(f(s(z0))) [0] f(s(s(s(s(z0''))))) -> s(f(s(f(f(z0''))))) [0] f(s(s(z0))) -> s(f(const1)) [0] f(v0) -> const1 [0] The TRS has the following type information: F :: s:const1 -> c1 s :: s:const1 -> s:const1 c1 :: c1 -> c1 -> c1 f :: s:const1 -> s:const1 const1 :: s:const1 const :: c1 Rewrite Strategy: INNERMOST ---------------------------------------- (35) CpxTypedWeightedTrsToRntsProof (UPPER BOUND(ID)) Transformed the TRS into an over-approximating RNTS by (improved) Size Abstraction. The constant constructors are abstracted as follows: const1 => 0 const => 0 ---------------------------------------- (36) Obligation: Complexity RNTS consisting of the following rules: F(z) -{ 1 }-> 1 + F(0) + F(z0) :|: z0 >= 0, z = 1 + (1 + z0) F(z) -{ 1 }-> 1 + F(1 + z0) + F(z0) :|: z0 >= 0, z = 1 + (1 + z0) F(z) -{ 1 }-> 1 + F(1 + f(f(z0'))) + F(1 + (1 + z0')) :|: z0' >= 0, z = 1 + (1 + (1 + (1 + z0'))) f(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0 f(z) -{ 0 }-> 1 + z0 :|: z = z0, z0 >= 0 f(z) -{ 0 }-> 1 + f(0) :|: z0 >= 0, z = 1 + (1 + z0) f(z) -{ 0 }-> 1 + f(1 + z0) :|: z0 >= 0, z = 1 + (1 + z0) f(z) -{ 0 }-> 1 + f(1 + f(f(z0''))) :|: z0'' >= 0, z = 1 + (1 + (1 + (1 + z0''))) ---------------------------------------- (37) SimplificationProof (BOTH BOUNDS(ID, ID)) Simplified the RNTS by moving equalities from the constraints into the right-hand sides. ---------------------------------------- (38) Obligation: Complexity RNTS consisting of the following rules: F(z) -{ 1 }-> 1 + F(0) + F(z - 2) :|: z - 2 >= 0 F(z) -{ 1 }-> 1 + F(1 + f(f(z - 4))) + F(1 + (1 + (z - 4))) :|: z - 4 >= 0 F(z) -{ 1 }-> 1 + F(1 + (z - 2)) + F(z - 2) :|: z - 2 >= 0 f(z) -{ 0 }-> 0 :|: z >= 0 f(z) -{ 0 }-> 1 + z :|: z >= 0 f(z) -{ 0 }-> 1 + f(0) :|: z - 2 >= 0 f(z) -{ 0 }-> 1 + f(1 + f(f(z - 4))) :|: z - 4 >= 0 f(z) -{ 0 }-> 1 + f(1 + (z - 2)) :|: z - 2 >= 0 ---------------------------------------- (39) 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) -> null_f [0] F(v0) -> null_F [0] And the following fresh constants: null_f, null_F ---------------------------------------- (40) 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(s(s(z0))) -> c1(F(f(z0)), F(z0)) [1] f(z0) -> s(z0) [0] f(s(s(z0))) -> s(f(f(z0))) [0] f(v0) -> null_f [0] F(v0) -> null_F [0] The TRS has the following type information: F :: s:null_f -> c1:null_F s :: s:null_f -> s:null_f c1 :: c1:null_F -> c1:null_F -> c1:null_F f :: s:null_f -> s:null_f null_f :: s:null_f null_F :: c1:null_F Rewrite Strategy: INNERMOST ---------------------------------------- (41) 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_F => 0 ---------------------------------------- (42) Obligation: Complexity RNTS consisting of the following rules: F(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0 F(z) -{ 1 }-> 1 + F(f(z0)) + F(z0) :|: z0 >= 0, z = 1 + (1 + z0) f(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0 f(z) -{ 0 }-> 1 + z0 :|: z = z0, z0 >= 0 f(z) -{ 0 }-> 1 + f(f(z0)) :|: z0 >= 0, z = 1 + (1 + z0) Only complete derivations are relevant for the runtime complexity. ---------------------------------------- (43) CdtNarrowingProof (BOTH BOUNDS(ID, ID)) Use narrowing to replace F(s(s(z0))) -> c1(F(f(z0)), F(z0)) by F(s(s(z0))) -> c1(F(s(z0)), F(z0)) F(s(s(s(s(z0))))) -> c1(F(s(f(f(z0)))), F(s(s(z0)))) ---------------------------------------- (44) Obligation: Complexity Dependency Tuples Problem Rules: f(z0) -> s(z0) f(s(s(z0))) -> s(f(f(z0))) Tuples: F(s(s(z0))) -> c1(F(s(z0)), F(z0)) F(s(s(s(s(z0))))) -> c1(F(s(f(f(z0)))), F(s(s(z0)))) S tuples: F(s(s(z0))) -> c1(F(s(z0)), F(z0)) F(s(s(s(s(z0))))) -> c1(F(s(f(f(z0)))), F(s(s(z0)))) K tuples:none Defined Rule Symbols: f_1 Defined Pair Symbols: F_1 Compound Symbols: c1_2 ---------------------------------------- (45) CdtNarrowingProof (BOTH BOUNDS(ID, ID)) Use narrowing to replace F(s(s(s(s(z0))))) -> c1(F(s(f(f(z0)))), F(s(s(z0)))) by F(s(s(s(s(x0))))) -> c1(F(s(s(f(x0)))), F(s(s(x0)))) F(s(s(s(s(z0))))) -> c1(F(s(f(s(z0)))), F(s(s(z0)))) F(s(s(s(s(s(s(z0))))))) -> c1(F(s(f(s(f(f(z0)))))), F(s(s(s(s(z0)))))) ---------------------------------------- (46) Obligation: Complexity Dependency Tuples Problem Rules: f(z0) -> s(z0) f(s(s(z0))) -> s(f(f(z0))) Tuples: F(s(s(z0))) -> c1(F(s(z0)), F(z0)) F(s(s(s(s(x0))))) -> c1(F(s(s(f(x0)))), F(s(s(x0)))) F(s(s(s(s(z0))))) -> c1(F(s(f(s(z0)))), F(s(s(z0)))) F(s(s(s(s(s(s(z0))))))) -> c1(F(s(f(s(f(f(z0)))))), F(s(s(s(s(z0)))))) S tuples: F(s(s(z0))) -> c1(F(s(z0)), F(z0)) F(s(s(s(s(x0))))) -> c1(F(s(s(f(x0)))), F(s(s(x0)))) F(s(s(s(s(z0))))) -> c1(F(s(f(s(z0)))), F(s(s(z0)))) F(s(s(s(s(s(s(z0))))))) -> c1(F(s(f(s(f(f(z0)))))), F(s(s(s(s(z0)))))) K tuples:none Defined Rule Symbols: f_1 Defined Pair Symbols: F_1 Compound Symbols: c1_2 ---------------------------------------- (47) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID)) Use forward instantiation to replace F(s(s(z0))) -> c1(F(s(z0)), F(z0)) by F(s(s(s(y0)))) -> c1(F(s(s(y0))), F(s(y0))) F(s(s(s(s(y0))))) -> c1(F(s(s(s(y0)))), F(s(s(y0)))) F(s(s(s(s(s(y0)))))) -> c1(F(s(s(s(s(y0))))), F(s(s(s(y0))))) F(s(s(s(s(s(s(y0))))))) -> c1(F(s(s(s(s(s(y0)))))), F(s(s(s(s(y0)))))) F(s(s(s(s(s(s(s(y0)))))))) -> c1(F(s(s(s(s(s(s(y0))))))), F(s(s(s(s(s(y0))))))) F(s(s(s(s(s(s(s(s(y0))))))))) -> c1(F(s(s(s(s(s(s(s(y0)))))))), F(s(s(s(s(s(s(y0)))))))) ---------------------------------------- (48) Obligation: Complexity Dependency Tuples Problem Rules: f(z0) -> s(z0) f(s(s(z0))) -> s(f(f(z0))) Tuples: F(s(s(s(s(x0))))) -> c1(F(s(s(f(x0)))), F(s(s(x0)))) F(s(s(s(s(z0))))) -> c1(F(s(f(s(z0)))), F(s(s(z0)))) F(s(s(s(s(s(s(z0))))))) -> c1(F(s(f(s(f(f(z0)))))), F(s(s(s(s(z0)))))) F(s(s(s(y0)))) -> c1(F(s(s(y0))), F(s(y0))) F(s(s(s(s(y0))))) -> c1(F(s(s(s(y0)))), F(s(s(y0)))) F(s(s(s(s(s(y0)))))) -> c1(F(s(s(s(s(y0))))), F(s(s(s(y0))))) F(s(s(s(s(s(s(y0))))))) -> c1(F(s(s(s(s(s(y0)))))), F(s(s(s(s(y0)))))) F(s(s(s(s(s(s(s(y0)))))))) -> c1(F(s(s(s(s(s(s(y0))))))), F(s(s(s(s(s(y0))))))) F(s(s(s(s(s(s(s(s(y0))))))))) -> c1(F(s(s(s(s(s(s(s(y0)))))))), F(s(s(s(s(s(s(y0)))))))) S tuples: F(s(s(s(s(x0))))) -> c1(F(s(s(f(x0)))), F(s(s(x0)))) F(s(s(s(s(z0))))) -> c1(F(s(f(s(z0)))), F(s(s(z0)))) F(s(s(s(s(s(s(z0))))))) -> c1(F(s(f(s(f(f(z0)))))), F(s(s(s(s(z0)))))) F(s(s(s(y0)))) -> c1(F(s(s(y0))), F(s(y0))) F(s(s(s(s(y0))))) -> c1(F(s(s(s(y0)))), F(s(s(y0)))) F(s(s(s(s(s(y0)))))) -> c1(F(s(s(s(s(y0))))), F(s(s(s(y0))))) F(s(s(s(s(s(s(y0))))))) -> c1(F(s(s(s(s(s(y0)))))), F(s(s(s(s(y0)))))) F(s(s(s(s(s(s(s(y0)))))))) -> c1(F(s(s(s(s(s(s(y0))))))), F(s(s(s(s(s(y0))))))) F(s(s(s(s(s(s(s(s(y0))))))))) -> c1(F(s(s(s(s(s(s(s(y0)))))))), F(s(s(s(s(s(s(y0)))))))) K tuples:none Defined Rule Symbols: f_1 Defined Pair Symbols: F_1 Compound Symbols: c1_2 ---------------------------------------- (49) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID)) Use forward instantiation to replace F(s(s(s(y0)))) -> c1(F(s(s(y0))), F(s(y0))) by F(s(s(s(s(s(y0)))))) -> c1(F(s(s(s(s(y0))))), F(s(s(s(y0))))) F(s(s(s(s(s(s(y0))))))) -> c1(F(s(s(s(s(s(y0)))))), F(s(s(s(s(y0)))))) F(s(s(s(s(s(s(s(y0)))))))) -> c1(F(s(s(s(s(s(s(y0))))))), F(s(s(s(s(s(y0))))))) F(s(s(s(s(s(s(s(s(y0))))))))) -> c1(F(s(s(s(s(s(s(s(y0)))))))), F(s(s(s(s(s(s(y0)))))))) F(s(s(s(s(y0))))) -> c1(F(s(s(s(y0)))), F(s(s(y0)))) F(s(s(s(s(s(s(s(s(s(y0)))))))))) -> c1(F(s(s(s(s(s(s(s(s(y0))))))))), F(s(s(s(s(s(s(s(y0))))))))) F(s(s(s(s(s(s(s(s(s(s(y0))))))))))) -> c1(F(s(s(s(s(s(s(s(s(s(y0)))))))))), F(s(s(s(s(s(s(s(s(y0)))))))))) ---------------------------------------- (50) Obligation: Complexity Dependency Tuples Problem Rules: f(z0) -> s(z0) f(s(s(z0))) -> s(f(f(z0))) Tuples: F(s(s(s(s(x0))))) -> c1(F(s(s(f(x0)))), F(s(s(x0)))) F(s(s(s(s(z0))))) -> c1(F(s(f(s(z0)))), F(s(s(z0)))) F(s(s(s(s(s(s(z0))))))) -> c1(F(s(f(s(f(f(z0)))))), F(s(s(s(s(z0)))))) F(s(s(s(s(y0))))) -> c1(F(s(s(s(y0)))), F(s(s(y0)))) F(s(s(s(s(s(y0)))))) -> c1(F(s(s(s(s(y0))))), F(s(s(s(y0))))) F(s(s(s(s(s(s(y0))))))) -> c1(F(s(s(s(s(s(y0)))))), F(s(s(s(s(y0)))))) F(s(s(s(s(s(s(s(y0)))))))) -> c1(F(s(s(s(s(s(s(y0))))))), F(s(s(s(s(s(y0))))))) F(s(s(s(s(s(s(s(s(y0))))))))) -> c1(F(s(s(s(s(s(s(s(y0)))))))), F(s(s(s(s(s(s(y0)))))))) F(s(s(s(s(s(s(s(s(s(y0)))))))))) -> c1(F(s(s(s(s(s(s(s(s(y0))))))))), F(s(s(s(s(s(s(s(y0))))))))) F(s(s(s(s(s(s(s(s(s(s(y0))))))))))) -> c1(F(s(s(s(s(s(s(s(s(s(y0)))))))))), F(s(s(s(s(s(s(s(s(y0)))))))))) S tuples: F(s(s(s(s(x0))))) -> c1(F(s(s(f(x0)))), F(s(s(x0)))) F(s(s(s(s(z0))))) -> c1(F(s(f(s(z0)))), F(s(s(z0)))) F(s(s(s(s(s(s(z0))))))) -> c1(F(s(f(s(f(f(z0)))))), F(s(s(s(s(z0)))))) F(s(s(s(s(y0))))) -> c1(F(s(s(s(y0)))), F(s(s(y0)))) F(s(s(s(s(s(y0)))))) -> c1(F(s(s(s(s(y0))))), F(s(s(s(y0))))) F(s(s(s(s(s(s(y0))))))) -> c1(F(s(s(s(s(s(y0)))))), F(s(s(s(s(y0)))))) F(s(s(s(s(s(s(s(y0)))))))) -> c1(F(s(s(s(s(s(s(y0))))))), F(s(s(s(s(s(y0))))))) F(s(s(s(s(s(s(s(s(y0))))))))) -> c1(F(s(s(s(s(s(s(s(y0)))))))), F(s(s(s(s(s(s(y0)))))))) F(s(s(s(s(s(s(s(s(s(y0)))))))))) -> c1(F(s(s(s(s(s(s(s(s(y0))))))))), F(s(s(s(s(s(s(s(y0))))))))) F(s(s(s(s(s(s(s(s(s(s(y0))))))))))) -> c1(F(s(s(s(s(s(s(s(s(s(y0)))))))))), F(s(s(s(s(s(s(s(s(y0)))))))))) K tuples:none Defined Rule Symbols: f_1 Defined Pair Symbols: F_1 Compound Symbols: c1_2 ---------------------------------------- (51) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID)) Use forward instantiation to replace F(s(s(s(s(y0))))) -> c1(F(s(s(s(y0)))), F(s(s(y0)))) by F(s(s(s(s(s(y0)))))) -> c1(F(s(s(s(s(y0))))), F(s(s(s(y0))))) F(s(s(s(s(s(s(y0))))))) -> c1(F(s(s(s(s(s(y0)))))), F(s(s(s(s(y0)))))) F(s(s(s(s(s(s(s(y0)))))))) -> c1(F(s(s(s(s(s(s(y0))))))), F(s(s(s(s(s(y0))))))) F(s(s(s(s(s(s(s(s(y0))))))))) -> c1(F(s(s(s(s(s(s(s(y0)))))))), F(s(s(s(s(s(s(y0)))))))) F(s(s(s(s(s(s(s(s(s(y0)))))))))) -> c1(F(s(s(s(s(s(s(s(s(y0))))))))), F(s(s(s(s(s(s(s(y0))))))))) F(s(s(s(s(s(s(s(s(s(s(y0))))))))))) -> c1(F(s(s(s(s(s(s(s(s(s(y0)))))))))), F(s(s(s(s(s(s(s(s(y0)))))))))) F(s(s(s(s(s(s(s(s(s(s(s(y0)))))))))))) -> c1(F(s(s(s(s(s(s(s(s(s(s(y0))))))))))), F(s(s(s(s(s(s(s(s(s(y0))))))))))) F(s(s(s(s(s(s(s(s(s(s(s(s(y0))))))))))))) -> c1(F(s(s(s(s(s(s(s(s(s(s(s(y0)))))))))))), F(s(s(s(s(s(s(s(s(s(s(y0)))))))))))) ---------------------------------------- (52) Obligation: Complexity Dependency Tuples Problem Rules: f(z0) -> s(z0) f(s(s(z0))) -> s(f(f(z0))) Tuples: F(s(s(s(s(x0))))) -> c1(F(s(s(f(x0)))), F(s(s(x0)))) F(s(s(s(s(z0))))) -> c1(F(s(f(s(z0)))), F(s(s(z0)))) F(s(s(s(s(s(s(z0))))))) -> c1(F(s(f(s(f(f(z0)))))), F(s(s(s(s(z0)))))) F(s(s(s(s(y0))))) -> c1(F(s(s(s(y0)))), F(s(s(y0)))) F(s(s(s(s(s(y0)))))) -> c1(F(s(s(s(s(y0))))), F(s(s(s(y0))))) F(s(s(s(s(s(s(y0))))))) -> c1(F(s(s(s(s(s(y0)))))), F(s(s(s(s(y0)))))) F(s(s(s(s(s(s(s(y0)))))))) -> c1(F(s(s(s(s(s(s(y0))))))), F(s(s(s(s(s(y0))))))) F(s(s(s(s(s(s(s(s(y0))))))))) -> c1(F(s(s(s(s(s(s(s(y0)))))))), F(s(s(s(s(s(s(y0)))))))) F(s(s(s(s(s(s(s(s(s(y0)))))))))) -> c1(F(s(s(s(s(s(s(s(s(y0))))))))), F(s(s(s(s(s(s(s(y0))))))))) F(s(s(s(s(s(s(s(s(s(s(y0))))))))))) -> c1(F(s(s(s(s(s(s(s(s(s(y0)))))))))), F(s(s(s(s(s(s(s(s(y0)))))))))) F(s(s(s(s(s(s(s(s(s(s(s(y0)))))))))))) -> c1(F(s(s(s(s(s(s(s(s(s(s(y0))))))))))), F(s(s(s(s(s(s(s(s(s(y0))))))))))) F(s(s(s(s(s(s(s(s(s(s(s(s(y0))))))))))))) -> c1(F(s(s(s(s(s(s(s(s(s(s(s(y0)))))))))))), F(s(s(s(s(s(s(s(s(s(s(y0)))))))))))) S tuples: F(s(s(s(s(x0))))) -> c1(F(s(s(f(x0)))), F(s(s(x0)))) F(s(s(s(s(z0))))) -> c1(F(s(f(s(z0)))), F(s(s(z0)))) F(s(s(s(s(s(s(z0))))))) -> c1(F(s(f(s(f(f(z0)))))), F(s(s(s(s(z0)))))) F(s(s(s(s(s(y0)))))) -> c1(F(s(s(s(s(y0))))), F(s(s(s(y0))))) F(s(s(s(s(s(s(y0))))))) -> c1(F(s(s(s(s(s(y0)))))), F(s(s(s(s(y0)))))) F(s(s(s(s(s(s(s(y0)))))))) -> c1(F(s(s(s(s(s(s(y0))))))), F(s(s(s(s(s(y0))))))) F(s(s(s(s(s(s(s(s(y0))))))))) -> c1(F(s(s(s(s(s(s(s(y0)))))))), F(s(s(s(s(s(s(y0)))))))) F(s(s(s(s(s(s(s(s(s(y0)))))))))) -> c1(F(s(s(s(s(s(s(s(s(y0))))))))), F(s(s(s(s(s(s(s(y0))))))))) F(s(s(s(s(s(s(s(s(s(s(y0))))))))))) -> c1(F(s(s(s(s(s(s(s(s(s(y0)))))))))), F(s(s(s(s(s(s(s(s(y0)))))))))) F(s(s(s(s(s(s(s(s(s(s(s(y0)))))))))))) -> c1(F(s(s(s(s(s(s(s(s(s(s(y0))))))))))), F(s(s(s(s(s(s(s(s(s(y0))))))))))) F(s(s(s(s(s(s(s(s(s(s(s(s(y0))))))))))))) -> c1(F(s(s(s(s(s(s(s(s(s(s(s(y0)))))))))))), F(s(s(s(s(s(s(s(s(s(s(y0)))))))))))) K tuples:none Defined Rule Symbols: f_1 Defined Pair Symbols: F_1 Compound Symbols: c1_2 ---------------------------------------- (53) RelTrsToWeightedTrsProof (UPPER BOUND(ID)) Transformed relative TRS to weighted TRS ---------------------------------------- (54) 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(x) -> s(x) [1] f(s(s(x))) -> s(f(f(x))) [1] Rewrite Strategy: INNERMOST ---------------------------------------- (55) TypeInferenceProof (BOTH BOUNDS(ID, ID)) Infered types. ---------------------------------------- (56) Obligation: Runtime Complexity Weighted TRS with Types. The TRS R consists of the following rules: f(x) -> s(x) [1] f(s(s(x))) -> s(f(f(x))) [1] The TRS has the following type information: f :: s -> s s :: s -> s Rewrite Strategy: INNERMOST ---------------------------------------- (57) 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 ---------------------------------------- (58) 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(x) -> s(x) [1] f(s(s(x))) -> s(f(f(x))) [1] The TRS has the following type information: f :: s -> s s :: s -> s const :: s Rewrite Strategy: INNERMOST ---------------------------------------- (59) 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 ---------------------------------------- (60) Obligation: Complexity RNTS consisting of the following rules: f(z) -{ 1 }-> 1 + x :|: x >= 0, z = x f(z) -{ 1 }-> 1 + f(f(x)) :|: x >= 0, z = 1 + (1 + x) Only complete derivations are relevant for the runtime complexity. ---------------------------------------- (61) 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: f_1 Due to the following rules being added: none And the following fresh constants: const ---------------------------------------- (62) 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(x) -> s(x) [1] f(s(s(x))) -> s(f(f(x))) [1] The TRS has the following type information: f :: s -> s s :: s -> s const :: s Rewrite Strategy: INNERMOST ---------------------------------------- (63) NarrowingProof (BOTH BOUNDS(ID, ID)) Narrowed the inner basic terms of all right-hand sides by a single narrowing step. ---------------------------------------- (64) 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(x) -> s(x) [1] f(s(s(x))) -> s(f(s(x))) [2] f(s(s(s(s(x'))))) -> s(f(s(f(f(x'))))) [2] The TRS has the following type information: f :: s -> s s :: s -> s const :: s Rewrite Strategy: INNERMOST ---------------------------------------- (65) 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 ---------------------------------------- (66) Obligation: Complexity RNTS consisting of the following rules: f(z) -{ 1 }-> 1 + x :|: x >= 0, z = x f(z) -{ 2 }-> 1 + f(1 + x) :|: x >= 0, z = 1 + (1 + x) f(z) -{ 2 }-> 1 + f(1 + f(f(x'))) :|: z = 1 + (1 + (1 + (1 + x'))), x' >= 0 ---------------------------------------- (67) SimplificationProof (BOTH BOUNDS(ID, ID)) Simplified the RNTS by moving equalities from the constraints into the right-hand sides. ---------------------------------------- (68) Obligation: Complexity RNTS consisting of the following rules: f(z) -{ 1 }-> 1 + z :|: z >= 0 f(z) -{ 2 }-> 1 + f(1 + f(f(z - 4))) :|: z - 4 >= 0 f(z) -{ 2 }-> 1 + f(1 + (z - 2)) :|: z - 2 >= 0