MAYBE proof of input_VbUwyG1EkQ.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 [BOTH BOUNDS(ID, ID), 0 ms] (6) CdtProblem (7) CdtToCpxRelTrsProof [BOTH BOUNDS(ID, ID), 0 ms] (8) CpxRelTRS (9) RenamingProof [BOTH BOUNDS(ID, ID), 0 ms] (10) CpxRelTRS (11) TypeInferenceProof [BOTH BOUNDS(ID, ID), 0 ms] (12) typed CpxTrs (13) OrderProof [LOWER BOUND(ID), 8 ms] (14) typed CpxTrs (15) RelTrsToDecreasingLoopProblemProof [LOWER BOUND(ID), 0 ms] (16) TRS for Loop Detection (17) CpxTrsToCdtProof [UPPER BOUND(ID), 0 ms] (18) CdtProblem (19) CdtLeafRemovalProof [BOTH BOUNDS(ID, ID), 0 ms] (20) CdtProblem (21) CdtRhsSimplificationProcessorProof [BOTH BOUNDS(ID, ID), 0 ms] (22) CdtProblem (23) CdtUsableRulesProof [BOTH BOUNDS(ID, ID), 0 ms] (24) CdtProblem (25) CdtToCpxRelTrsProof [BOTH BOUNDS(ID, ID), 0 ms] (26) CpxRelTRS (27) RelTrsToTrsProof [UPPER BOUND(ID), 0 ms] (28) CpxTRS (29) RelTrsToWeightedTrsProof [BOTH BOUNDS(ID, ID), 0 ms] (30) CpxWeightedTrs (31) CpxWeightedTrsRenamingProof [BOTH BOUNDS(ID, ID), 0 ms] (32) CpxWeightedTrs (33) TypeInferenceProof [BOTH BOUNDS(ID, ID), 0 ms] (34) CpxTypedWeightedTrs (35) CompletionProof [UPPER BOUND(ID), 0 ms] (36) CpxTypedWeightedCompleteTrs (37) NarrowingProof [BOTH BOUNDS(ID, ID), 0 ms] (38) CpxTypedWeightedCompleteTrs (39) CpxTypedWeightedTrsToRntsProof [UPPER BOUND(ID), 0 ms] (40) CpxRNTS (41) SimplificationProof [BOTH BOUNDS(ID, ID), 0 ms] (42) CpxRNTS (43) CpxRntsAnalysisOrderProof [BOTH BOUNDS(ID, ID), 0 ms] (44) CpxRNTS (45) ResultPropagationProof [UPPER BOUND(ID), 0 ms] (46) CpxRNTS (47) IntTrsBoundProof [UPPER BOUND(ID), 341 ms] (48) CpxRNTS (49) IntTrsBoundProof [UPPER BOUND(ID), 74 ms] (50) CpxRNTS (51) CompletionProof [UPPER BOUND(ID), 0 ms] (52) CpxTypedWeightedCompleteTrs (53) CpxTypedWeightedTrsToRntsProof [UPPER BOUND(ID), 0 ms] (54) CpxRNTS (55) CdtNarrowingProof [BOTH BOUNDS(ID, ID), 0 ms] (56) CdtProblem (57) CdtUsableRulesProof [BOTH BOUNDS(ID, ID), 0 ms] (58) CdtProblem (59) RelTrsToWeightedTrsProof [UPPER BOUND(ID), 0 ms] (60) CpxWeightedTrs (61) CpxWeightedTrsRenamingProof [BOTH BOUNDS(ID, ID), 0 ms] (62) CpxWeightedTrs (63) TypeInferenceProof [BOTH BOUNDS(ID, ID), 0 ms] (64) CpxTypedWeightedTrs (65) CompletionProof [UPPER BOUND(ID), 0 ms] (66) CpxTypedWeightedCompleteTrs (67) NarrowingProof [BOTH BOUNDS(ID, ID), 0 ms] (68) CpxTypedWeightedCompleteTrs (69) CpxTypedWeightedTrsToRntsProof [UPPER BOUND(ID), 0 ms] (70) CpxRNTS (71) SimplificationProof [BOTH BOUNDS(ID, ID), 0 ms] (72) CpxRNTS (73) CpxRntsAnalysisOrderProof [BOTH BOUNDS(ID, ID), 0 ms] (74) CpxRNTS (75) ResultPropagationProof [UPPER BOUND(ID), 0 ms] (76) CpxRNTS (77) IntTrsBoundProof [UPPER BOUND(ID), 885 ms] (78) CpxRNTS (79) IntTrsBoundProof [UPPER BOUND(ID), 140 ms] (80) CpxRNTS (81) CompletionProof [UPPER BOUND(ID), 0 ms] (82) CpxTypedWeightedCompleteTrs (83) CpxTypedWeightedTrsToRntsProof [UPPER BOUND(ID), 0 ms] (84) 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: +(1, x) -> +(+(0, 1), x) +(0, 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: +'(1', x) -> +'(+'(0', 1'), x) +'(0', 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: +(1, x) -> +(+(0, 1), x) +(0, x) -> x S is empty. Rewrite Strategy: PARALLEL_INNERMOST ---------------------------------------- (5) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID)) Converted Cpx (relative) TRS with rewrite strategy PARALLEL_INNERMOST to CDT ---------------------------------------- (6) Obligation: Complexity Dependency Tuples Problem Rules: +(1, z0) -> +(+(0, 1), z0) +(0, z0) -> z0 Tuples: +'(1, z0) -> c(+'(+(0, 1), z0), +'(0, 1)) +'(0, z0) -> c1 S tuples: +'(1, z0) -> c(+'(+(0, 1), z0), +'(0, 1)) +'(0, z0) -> c1 K tuples:none Defined Rule Symbols: +_2 Defined Pair Symbols: +'_2 Compound Symbols: c_2, c1 ---------------------------------------- (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: +'(1, z0) -> c(+'(+(0, 1), z0), +'(0, 1)) +'(0, z0) -> c1 The (relative) TRS S consists of the following rules: +(1, z0) -> +(+(0, 1), z0) +(0, z0) -> z0 Rewrite Strategy: INNERMOST ---------------------------------------- (9) RenamingProof (BOTH BOUNDS(ID, ID)) Renamed function symbols to avoid clashes with predefined symbol. ---------------------------------------- (10) 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: +'(1', z0) -> c(+'(+'(0', 1'), z0), +'(0', 1')) +'(0', z0) -> c1 The (relative) TRS S consists of the following rules: +'(1', z0) -> +'(+'(0', 1'), z0) +'(0', z0) -> z0 Rewrite Strategy: INNERMOST ---------------------------------------- (11) TypeInferenceProof (BOTH BOUNDS(ID, ID)) Inferred types. ---------------------------------------- (12) Obligation: Innermost TRS: Rules: +'(1', z0) -> c(+'(+'(0', 1'), z0), +'(0', 1')) +'(0', z0) -> c1 +'(1', z0) -> +'(+'(0', 1'), z0) +'(0', z0) -> z0 Types: +' :: 1':0':c:c1 -> 1':0':c:c1 -> 1':0':c:c1 1' :: 1':0':c:c1 c :: 1':0':c:c1 -> 1':0':c:c1 -> 1':0':c:c1 0' :: 1':0':c:c1 c1 :: 1':0':c:c1 hole_1':0':c:c11_2 :: 1':0':c:c1 gen_1':0':c:c12_2 :: Nat -> 1':0':c:c1 ---------------------------------------- (13) OrderProof (LOWER BOUND(ID)) Heuristically decided to analyse the following defined symbols: +' ---------------------------------------- (14) Obligation: Innermost TRS: Rules: +'(1', z0) -> c(+'(+'(0', 1'), z0), +'(0', 1')) +'(0', z0) -> c1 +'(1', z0) -> +'(+'(0', 1'), z0) +'(0', z0) -> z0 Types: +' :: 1':0':c:c1 -> 1':0':c:c1 -> 1':0':c:c1 1' :: 1':0':c:c1 c :: 1':0':c:c1 -> 1':0':c:c1 -> 1':0':c:c1 0' :: 1':0':c:c1 c1 :: 1':0':c:c1 hole_1':0':c:c11_2 :: 1':0':c:c1 gen_1':0':c:c12_2 :: Nat -> 1':0':c:c1 Generator Equations: gen_1':0':c:c12_2(0) <=> 0' gen_1':0':c:c12_2(+(x, 1)) <=> c(0', gen_1':0':c:c12_2(x)) The following defined symbols remain to be analysed: +' ---------------------------------------- (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: +'(1, z0) -> c(+'(+(0, 1), z0), +'(0, 1)) +'(0, z0) -> c1 The (relative) TRS S consists of the following rules: +(1, z0) -> +(+(0, 1), z0) +(0, z0) -> z0 Rewrite Strategy: INNERMOST ---------------------------------------- (17) CpxTrsToCdtProof (UPPER BOUND(ID)) Converted Cpx (relative) TRS with rewrite strategy PARALLEL_INNERMOST to CDT ---------------------------------------- (18) Obligation: Complexity Dependency Tuples Problem Rules: +(1, z0) -> +(+(0, 1), z0) +(0, z0) -> z0 Tuples: +'(1, z0) -> c(+'(+(0, 1), z0), +'(0, 1)) +'(0, z0) -> c1 S tuples: +'(1, z0) -> c(+'(+(0, 1), z0), +'(0, 1)) +'(0, z0) -> c1 K tuples:none Defined Rule Symbols: +_2 Defined Pair Symbols: +'_2 Compound Symbols: c_2, c1 ---------------------------------------- (19) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID)) Removed 1 trailing nodes: +'(0, z0) -> c1 ---------------------------------------- (20) Obligation: Complexity Dependency Tuples Problem Rules: +(1, z0) -> +(+(0, 1), z0) +(0, z0) -> z0 Tuples: +'(1, z0) -> c(+'(+(0, 1), z0), +'(0, 1)) S tuples: +'(1, z0) -> c(+'(+(0, 1), z0), +'(0, 1)) K tuples:none Defined Rule Symbols: +_2 Defined Pair Symbols: +'_2 Compound Symbols: c_2 ---------------------------------------- (21) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID)) Removed 1 trailing tuple parts ---------------------------------------- (22) Obligation: Complexity Dependency Tuples Problem Rules: +(1, z0) -> +(+(0, 1), z0) +(0, z0) -> z0 Tuples: +'(1, z0) -> c(+'(+(0, 1), z0)) S tuples: +'(1, z0) -> c(+'(+(0, 1), z0)) K tuples:none Defined Rule Symbols: +_2 Defined Pair Symbols: +'_2 Compound Symbols: c_1 ---------------------------------------- (23) CdtUsableRulesProof (BOTH BOUNDS(ID, ID)) The following rules are not usable and were removed: +(1, z0) -> +(+(0, 1), z0) ---------------------------------------- (24) Obligation: Complexity Dependency Tuples Problem Rules: +(0, z0) -> z0 Tuples: +'(1, z0) -> c(+'(+(0, 1), z0)) S tuples: +'(1, z0) -> c(+'(+(0, 1), z0)) K tuples:none Defined Rule Symbols: +_2 Defined Pair Symbols: +'_2 Compound Symbols: c_1 ---------------------------------------- (25) CdtToCpxRelTrsProof (BOTH BOUNDS(ID, ID)) Converted S to standard rules, and D \ S as well as R to relative rules. ---------------------------------------- (26) 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: +'(1, z0) -> c(+'(+(0, 1), z0)) The (relative) TRS S consists of the following rules: +(0, z0) -> z0 Rewrite Strategy: INNERMOST ---------------------------------------- (27) RelTrsToTrsProof (UPPER BOUND(ID)) transformed relative TRS to TRS ---------------------------------------- (28) 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: +'(1, z0) -> c(+'(+(0, 1), z0)) +(0, z0) -> z0 S is empty. Rewrite Strategy: INNERMOST ---------------------------------------- (29) RelTrsToWeightedTrsProof (BOTH BOUNDS(ID, ID)) Transformed relative TRS to weighted TRS ---------------------------------------- (30) 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: +'(1, z0) -> c(+'(+(0, 1), z0)) [1] +(0, z0) -> z0 [0] Rewrite Strategy: INNERMOST ---------------------------------------- (31) CpxWeightedTrsRenamingProof (BOTH BOUNDS(ID, ID)) Renamed defined symbols to avoid conflicts with arithmetic symbols: + => plus ---------------------------------------- (32) 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: +'(1, z0) -> c(+'(plus(0, 1), z0)) [1] plus(0, z0) -> z0 [0] Rewrite Strategy: INNERMOST ---------------------------------------- (33) TypeInferenceProof (BOTH BOUNDS(ID, ID)) Infered types. ---------------------------------------- (34) Obligation: Runtime Complexity Weighted TRS with Types. The TRS R consists of the following rules: +'(1, z0) -> c(+'(plus(0, 1), z0)) [1] plus(0, z0) -> z0 [0] The TRS has the following type information: +' :: 1 -> a -> c 1 :: 1 c :: c -> c plus :: 0 -> 1 -> 1 0 :: 0 Rewrite Strategy: INNERMOST ---------------------------------------- (35) 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: +'_2 (c) The following functions are completely defined: plus_2 Due to the following rules being added: plus(v0, v1) -> 1 [0] And the following fresh constants: const, const1 ---------------------------------------- (36) 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: +'(1, z0) -> c(+'(plus(0, 1), z0)) [1] plus(0, z0) -> z0 [0] plus(v0, v1) -> 1 [0] The TRS has the following type information: +' :: 1 -> a -> c 1 :: 1 c :: c -> c plus :: 0 -> 1 -> 1 0 :: 0 const :: c const1 :: a Rewrite Strategy: INNERMOST ---------------------------------------- (37) NarrowingProof (BOTH BOUNDS(ID, ID)) Narrowed the inner basic terms of all right-hand sides by a single narrowing step. ---------------------------------------- (38) 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: +'(1, z0) -> c(+'(1, z0)) [1] +'(1, z0) -> c(+'(1, z0)) [1] plus(0, z0) -> z0 [0] plus(v0, v1) -> 1 [0] The TRS has the following type information: +' :: 1 -> a -> c 1 :: 1 c :: c -> c plus :: 0 -> 1 -> 1 0 :: 0 const :: c const1 :: a 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: 1 => 0 0 => 0 const => 0 const1 => 0 ---------------------------------------- (40) Obligation: Complexity RNTS consisting of the following rules: +'(z, z') -{ 1 }-> 1 + +'(0, z0) :|: z0 >= 0, z = 0, z' = z0 plus(z, z') -{ 0 }-> z0 :|: z0 >= 0, z = 0, z' = z0 plus(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1 ---------------------------------------- (41) SimplificationProof (BOTH BOUNDS(ID, ID)) Simplified the RNTS by moving equalities from the constraints into the right-hand sides. ---------------------------------------- (42) Obligation: Complexity RNTS consisting of the following rules: +'(z, z') -{ 1 }-> 1 + +'(0, z') :|: z' >= 0, z = 0 plus(z, z') -{ 0 }-> z' :|: z' >= 0, z = 0 plus(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0 ---------------------------------------- (43) CpxRntsAnalysisOrderProof (BOTH BOUNDS(ID, ID)) Found the following analysis order by SCC decomposition: { +' } { plus } ---------------------------------------- (44) Obligation: Complexity RNTS consisting of the following rules: +'(z, z') -{ 1 }-> 1 + +'(0, z') :|: z' >= 0, z = 0 plus(z, z') -{ 0 }-> z' :|: z' >= 0, z = 0 plus(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0 Function symbols to be analyzed: {+'}, {plus} ---------------------------------------- (45) ResultPropagationProof (UPPER BOUND(ID)) Applied inner abstraction using the recently inferred runtime/size bounds where possible. ---------------------------------------- (46) Obligation: Complexity RNTS consisting of the following rules: +'(z, z') -{ 1 }-> 1 + +'(0, z') :|: z' >= 0, z = 0 plus(z, z') -{ 0 }-> z' :|: z' >= 0, z = 0 plus(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0 Function symbols to be analyzed: {+'}, {plus} ---------------------------------------- (47) IntTrsBoundProof (UPPER BOUND(ID)) Computed SIZE bound using CoFloCo for: +' after applying outer abstraction to obtain an ITS, resulting in: O(1) with polynomial bound: 0 ---------------------------------------- (48) Obligation: Complexity RNTS consisting of the following rules: +'(z, z') -{ 1 }-> 1 + +'(0, z') :|: z' >= 0, z = 0 plus(z, z') -{ 0 }-> z' :|: z' >= 0, z = 0 plus(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0 Function symbols to be analyzed: {+'}, {plus} Previous analysis results are: +': runtime: ?, size: O(1) [0] ---------------------------------------- (49) IntTrsBoundProof (UPPER BOUND(ID)) Computed RUNTIME bound using CoFloCo for: +' after applying outer abstraction to obtain an ITS, resulting in: INF with polynomial bound: ? ---------------------------------------- (50) Obligation: Complexity RNTS consisting of the following rules: +'(z, z') -{ 1 }-> 1 + +'(0, z') :|: z' >= 0, z = 0 plus(z, z') -{ 0 }-> z' :|: z' >= 0, z = 0 plus(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0 Function symbols to be analyzed: {+'}, {plus} Previous analysis results are: +': runtime: INF, size: O(1) [0] ---------------------------------------- (51) 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: plus(v0, v1) -> null_plus [0] +'(v0, v1) -> null_+' [0] And the following fresh constants: null_plus, null_+', const ---------------------------------------- (52) 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: +'(1, z0) -> c(+'(plus(0, 1), z0)) [1] plus(0, z0) -> z0 [0] plus(v0, v1) -> null_plus [0] +'(v0, v1) -> null_+' [0] The TRS has the following type information: +' :: 1:null_plus -> a -> c:null_+' 1 :: 1:null_plus c :: c:null_+' -> c:null_+' plus :: 0 -> 1:null_plus -> 1:null_plus 0 :: 0 null_plus :: 1:null_plus null_+' :: c:null_+' const :: a Rewrite Strategy: INNERMOST ---------------------------------------- (53) CpxTypedWeightedTrsToRntsProof (UPPER BOUND(ID)) Transformed the TRS into an over-approximating RNTS by (improved) Size Abstraction. The constant constructors are abstracted as follows: 1 => 1 0 => 0 null_plus => 0 null_+' => 0 const => 0 ---------------------------------------- (54) Obligation: Complexity RNTS consisting of the following rules: +'(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1 +'(z, z') -{ 1 }-> 1 + +'(plus(0, 1), z0) :|: z = 1, z0 >= 0, z' = z0 plus(z, z') -{ 0 }-> z0 :|: z0 >= 0, z = 0, z' = z0 plus(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1 Only complete derivations are relevant for the runtime complexity. ---------------------------------------- (55) CdtNarrowingProof (BOTH BOUNDS(ID, ID)) Use narrowing to replace +'(1, z0) -> c(+'(+(0, 1), z0)) by +'(1, x0) -> c(+'(1, x0)) ---------------------------------------- (56) Obligation: Complexity Dependency Tuples Problem Rules: +(0, z0) -> z0 Tuples: +'(1, x0) -> c(+'(1, x0)) S tuples: +'(1, x0) -> c(+'(1, x0)) K tuples:none Defined Rule Symbols: +_2 Defined Pair Symbols: +'_2 Compound Symbols: c_1 ---------------------------------------- (57) CdtUsableRulesProof (BOTH BOUNDS(ID, ID)) The following rules are not usable and were removed: +(0, z0) -> z0 ---------------------------------------- (58) Obligation: Complexity Dependency Tuples Problem Rules:none Tuples: +'(1, x0) -> c(+'(1, x0)) S tuples: +'(1, x0) -> c(+'(1, x0)) K tuples:none Defined Rule Symbols:none Defined Pair Symbols: +'_2 Compound Symbols: c_1 ---------------------------------------- (59) RelTrsToWeightedTrsProof (UPPER BOUND(ID)) Transformed relative TRS to weighted TRS ---------------------------------------- (60) 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: +(1, x) -> +(+(0, 1), x) [1] +(0, x) -> x [1] Rewrite Strategy: INNERMOST ---------------------------------------- (61) CpxWeightedTrsRenamingProof (BOTH BOUNDS(ID, ID)) Renamed defined symbols to avoid conflicts with arithmetic symbols: + => plus ---------------------------------------- (62) 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: plus(1, x) -> plus(plus(0, 1), x) [1] plus(0, x) -> x [1] Rewrite Strategy: INNERMOST ---------------------------------------- (63) TypeInferenceProof (BOTH BOUNDS(ID, ID)) Infered types. ---------------------------------------- (64) Obligation: Runtime Complexity Weighted TRS with Types. The TRS R consists of the following rules: plus(1, x) -> plus(plus(0, 1), x) [1] plus(0, x) -> x [1] The TRS has the following type information: plus :: 1:0 -> 1:0 -> 1:0 1 :: 1:0 0 :: 1:0 Rewrite Strategy: INNERMOST ---------------------------------------- (65) 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: plus_2 Due to the following rules being added: none And the following fresh constants: none ---------------------------------------- (66) 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: plus(1, x) -> plus(plus(0, 1), x) [1] plus(0, x) -> x [1] The TRS has the following type information: plus :: 1:0 -> 1:0 -> 1:0 1 :: 1:0 0 :: 1:0 Rewrite Strategy: INNERMOST ---------------------------------------- (67) NarrowingProof (BOTH BOUNDS(ID, ID)) Narrowed the inner basic terms of all right-hand sides by a single narrowing step. ---------------------------------------- (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: plus(1, x) -> plus(1, x) [2] plus(0, x) -> x [1] The TRS has the following type information: plus :: 1:0 -> 1:0 -> 1:0 1 :: 1:0 0 :: 1:0 Rewrite Strategy: INNERMOST ---------------------------------------- (69) CpxTypedWeightedTrsToRntsProof (UPPER BOUND(ID)) Transformed the TRS into an over-approximating RNTS by (improved) Size Abstraction. The constant constructors are abstracted as follows: 1 => 1 0 => 0 ---------------------------------------- (70) Obligation: Complexity RNTS consisting of the following rules: plus(z, z') -{ 1 }-> x :|: z' = x, x >= 0, z = 0 plus(z, z') -{ 2 }-> plus(1, x) :|: z' = x, z = 1, x >= 0 ---------------------------------------- (71) SimplificationProof (BOTH BOUNDS(ID, ID)) Simplified the RNTS by moving equalities from the constraints into the right-hand sides. ---------------------------------------- (72) Obligation: Complexity RNTS consisting of the following rules: plus(z, z') -{ 1 }-> z' :|: z' >= 0, z = 0 plus(z, z') -{ 2 }-> plus(1, z') :|: z = 1, z' >= 0 ---------------------------------------- (73) CpxRntsAnalysisOrderProof (BOTH BOUNDS(ID, ID)) Found the following analysis order by SCC decomposition: { plus } ---------------------------------------- (74) Obligation: Complexity RNTS consisting of the following rules: plus(z, z') -{ 1 }-> z' :|: z' >= 0, z = 0 plus(z, z') -{ 2 }-> plus(1, z') :|: z = 1, z' >= 0 Function symbols to be analyzed: {plus} ---------------------------------------- (75) ResultPropagationProof (UPPER BOUND(ID)) Applied inner abstraction using the recently inferred runtime/size bounds where possible. ---------------------------------------- (76) Obligation: Complexity RNTS consisting of the following rules: plus(z, z') -{ 1 }-> z' :|: z' >= 0, z = 0 plus(z, z') -{ 2 }-> plus(1, z') :|: z = 1, z' >= 0 Function symbols to be analyzed: {plus} ---------------------------------------- (77) IntTrsBoundProof (UPPER BOUND(ID)) Computed SIZE bound using CoFloCo for: plus after applying outer abstraction to obtain an ITS, resulting in: O(n^1) with polynomial bound: z' ---------------------------------------- (78) Obligation: Complexity RNTS consisting of the following rules: plus(z, z') -{ 1 }-> z' :|: z' >= 0, z = 0 plus(z, z') -{ 2 }-> plus(1, z') :|: z = 1, z' >= 0 Function symbols to be analyzed: {plus} Previous analysis results are: plus: runtime: ?, size: O(n^1) [z'] ---------------------------------------- (79) IntTrsBoundProof (UPPER BOUND(ID)) Computed RUNTIME bound using CoFloCo for: plus after applying outer abstraction to obtain an ITS, resulting in: INF with polynomial bound: ? ---------------------------------------- (80) Obligation: Complexity RNTS consisting of the following rules: plus(z, z') -{ 1 }-> z' :|: z' >= 0, z = 0 plus(z, z') -{ 2 }-> plus(1, z') :|: z = 1, z' >= 0 Function symbols to be analyzed: {plus} Previous analysis results are: plus: runtime: INF, size: O(n^1) [z'] ---------------------------------------- (81) CompletionProof (UPPER BOUND(ID)) The TRS is a completely defined constructor system, as every type has a constant constructor and the following rules were added: none And the following fresh constants: none ---------------------------------------- (82) 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: plus(1, x) -> plus(plus(0, 1), x) [1] plus(0, x) -> x [1] The TRS has the following type information: plus :: 1:0 -> 1:0 -> 1:0 1 :: 1:0 0 :: 1:0 Rewrite Strategy: INNERMOST ---------------------------------------- (83) CpxTypedWeightedTrsToRntsProof (UPPER BOUND(ID)) Transformed the TRS into an over-approximating RNTS by (improved) Size Abstraction. The constant constructors are abstracted as follows: 1 => 1 0 => 0 ---------------------------------------- (84) Obligation: Complexity RNTS consisting of the following rules: plus(z, z') -{ 1 }-> x :|: z' = x, x >= 0, z = 0 plus(z, z') -{ 1 }-> plus(plus(0, 1), x) :|: z' = x, z = 1, x >= 0 Only complete derivations are relevant for the runtime complexity.