KILLED proof of input_N9Lmg1LjH2.trs # AProVE Commit ID: aff8ecad908e01718a4c36e68d2e55d5e0f16e15 fuhs 20220216 unpublished The Runtime Complexity (parallel-innermost) of the given CpxTRS could be proven to be BOUNDS(1, INF). (0) CpxTRS (1) RenamingProof [BOTH BOUNDS(ID, ID), 0 ms] (2) CpxTRS (3) RelTrsToTrsProof [UPPER BOUND(ID), 0 ms] (4) CpxTRS (5) RelTrsToWeightedTrsProof [UPPER BOUND(ID), 0 ms] (6) CpxWeightedTrs (7) TypeInferenceProof [BOTH BOUNDS(ID, ID), 0 ms] (8) CpxTypedWeightedTrs (9) CompletionProof [UPPER BOUND(ID), 0 ms] (10) CpxTypedWeightedCompleteTrs (11) CpxTypedWeightedTrsToRntsProof [UPPER BOUND(ID), 0 ms] (12) CpxRNTS (13) CompletionProof [UPPER BOUND(ID), 0 ms] (14) CpxTypedWeightedCompleteTrs (15) NarrowingProof [BOTH BOUNDS(ID, ID), 0 ms] (16) CpxTypedWeightedCompleteTrs (17) CpxTypedWeightedTrsToRntsProof [UPPER BOUND(ID), 0 ms] (18) CpxRNTS (19) SimplificationProof [BOTH BOUNDS(ID, ID), 0 ms] (20) CpxRNTS (21) CpxRntsAnalysisOrderProof [BOTH BOUNDS(ID, ID), 0 ms] (22) CpxRNTS (23) ResultPropagationProof [UPPER BOUND(ID), 0 ms] (24) CpxRNTS (25) IntTrsBoundProof [UPPER BOUND(ID), 213 ms] (26) CpxRNTS (27) IntTrsBoundProof [UPPER BOUND(ID), 7 ms] (28) CpxRNTS (29) ResultPropagationProof [UPPER BOUND(ID), 0 ms] (30) CpxRNTS (31) IntTrsBoundProof [UPPER BOUND(ID), 166 ms] (32) CpxRNTS (33) IntTrsBoundProof [UPPER BOUND(ID), 34 ms] (34) CpxRNTS (35) ResultPropagationProof [UPPER BOUND(ID), 0 ms] (36) CpxRNTS (37) IntTrsBoundProof [UPPER BOUND(ID), 470 ms] (38) CpxRNTS (39) IntTrsBoundProof [UPPER BOUND(ID), 98 ms] (40) CpxRNTS (41) ResultPropagationProof [UPPER BOUND(ID), 0 ms] (42) CpxRNTS (43) IntTrsBoundProof [UPPER BOUND(ID), 366 ms] (44) CpxRNTS (45) IntTrsBoundProof [UPPER BOUND(ID), 107 ms] (46) CpxRNTS (47) ResultPropagationProof [UPPER BOUND(ID), 0 ms] (48) CpxRNTS (49) IntTrsBoundProof [UPPER BOUND(ID), 600 ms] (50) CpxRNTS (51) IntTrsBoundProof [UPPER BOUND(ID), 3 ms] (52) CpxRNTS (53) ResultPropagationProof [UPPER BOUND(ID), 0 ms] (54) CpxRNTS (55) IntTrsBoundProof [UPPER BOUND(ID), 593 ms] (56) CpxRNTS (57) IntTrsBoundProof [UPPER BOUND(ID), 0 ms] (58) CpxRNTS (59) CpxTrsToCdtProof [UPPER BOUND(ID), 0 ms] (60) CdtProblem (61) CdtLeafRemovalProof [BOTH BOUNDS(ID, ID), 0 ms] (62) CdtProblem (63) CdtGraphSplitRhsProof [BOTH BOUNDS(ID, ID), 0 ms] (64) CdtProblem (65) CdtLeafRemovalProof [ComplexityIfPolyImplication, 0 ms] (66) CdtProblem (67) CdtKnowledgeProof [BOTH BOUNDS(ID, ID), 0 ms] (68) CdtProblem (69) CdtUsableRulesProof [BOTH BOUNDS(ID, ID), 0 ms] (70) CdtProblem (71) CdtRuleRemovalProof [UPPER BOUND(ADD(n^1)), 152 ms] (72) CdtProblem (73) CdtRuleRemovalProof [UPPER BOUND(ADD(n^1)), 42 ms] (74) CdtProblem (75) CdtRuleRemovalProof [UPPER BOUND(ADD(n^1)), 30 ms] (76) CdtProblem (77) CdtRuleRemovalProof [UPPER BOUND(ADD(n^1)), 29 ms] (78) CdtProblem (79) CdtRuleRemovalProof [UPPER BOUND(ADD(n^2)), 774 ms] (80) CdtProblem (81) CdtNarrowingProof [BOTH BOUNDS(ID, ID), 0 ms] (82) CdtProblem (83) CdtNarrowingProof [BOTH BOUNDS(ID, ID), 0 ms] (84) CdtProblem (85) CdtNarrowingProof [BOTH BOUNDS(ID, ID), 0 ms] (86) CdtProblem (87) CdtNarrowingProof [BOTH BOUNDS(ID, ID), 0 ms] (88) CdtProblem (89) CdtForwardInstantiationProof [BOTH BOUNDS(ID, ID), 0 ms] (90) CdtProblem (91) CdtRewritingProof [BOTH BOUNDS(ID, ID), 0 ms] (92) CdtProblem (93) CdtForwardInstantiationProof [BOTH BOUNDS(ID, ID), 0 ms] (94) CdtProblem (95) CdtRewritingProof [BOTH BOUNDS(ID, ID), 0 ms] (96) CdtProblem (97) CdtForwardInstantiationProof [BOTH BOUNDS(ID, ID), 0 ms] (98) CdtProblem (99) CdtRewritingProof [BOTH BOUNDS(ID, ID), 0 ms] (100) CdtProblem (101) CdtForwardInstantiationProof [BOTH BOUNDS(ID, ID), 0 ms] (102) CdtProblem (103) CdtRewritingProof [BOTH BOUNDS(ID, ID), 0 ms] (104) CdtProblem (105) CdtRewritingProof [BOTH BOUNDS(ID, ID), 0 ms] (106) CdtProblem (107) CdtRewritingProof [BOTH BOUNDS(ID, ID), 0 ms] (108) CdtProblem (109) CdtRewritingProof [BOTH BOUNDS(ID, ID), 0 ms] (110) CdtProblem (111) CdtRewritingProof [BOTH BOUNDS(ID, ID), 0 ms] (112) CdtProblem (113) CdtForwardInstantiationProof [BOTH BOUNDS(ID, ID), 0 ms] (114) CdtProblem (115) CdtRewritingProof [BOTH BOUNDS(ID, ID), 0 ms] (116) CdtProblem (117) CdtRewritingProof [BOTH BOUNDS(ID, ID), 0 ms] (118) CdtProblem (119) CdtForwardInstantiationProof [BOTH BOUNDS(ID, ID), 0 ms] (120) CdtProblem (121) CdtForwardInstantiationProof [BOTH BOUNDS(ID, ID), 0 ms] (122) CdtProblem ---------------------------------------- (0) Obligation: The Runtime Complexity (parallel-innermost) of the given CpxTRS could be proven to be BOUNDS(1, INF). The TRS R consists of the following rules: sum#1(Nil) -> 0 sum#1(Cons(x2, x1)) -> plus#2(x2, sum#1(x1)) map#2(Nil) -> Nil map#2(Cons(x2, x5)) -> Cons(mult#2(x2, x2), map#2(x5)) unfoldr#2(0) -> Nil unfoldr#2(S(x2)) -> Cons(x2, unfoldr#2(x2)) mult#2(0, x2) -> 0 mult#2(S(x4), x2) -> plus#2(x2, mult#2(x4, x2)) plus#2(0, x8) -> x8 plus#2(S(x4), x2) -> S(plus#2(x4, x2)) main(0) -> 0 main(S(x1)) -> sum#1(map#2(Cons(S(x1), unfoldr#2(S(x1))))) 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: sum#1(Nil) -> 0' sum#1(Cons(x2, x1)) -> plus#2(x2, sum#1(x1)) map#2(Nil) -> Nil map#2(Cons(x2, x5)) -> Cons(mult#2(x2, x2), map#2(x5)) unfoldr#2(0') -> Nil unfoldr#2(S(x2)) -> Cons(x2, unfoldr#2(x2)) mult#2(0', x2) -> 0' mult#2(S(x4), x2) -> plus#2(x2, mult#2(x4, x2)) plus#2(0', x8) -> x8 plus#2(S(x4), x2) -> S(plus#2(x4, x2)) main(0') -> 0' main(S(x1)) -> sum#1(map#2(Cons(S(x1), unfoldr#2(S(x1))))) 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: sum#1(Nil) -> 0 sum#1(Cons(x2, x1)) -> plus#2(x2, sum#1(x1)) map#2(Nil) -> Nil map#2(Cons(x2, x5)) -> Cons(mult#2(x2, x2), map#2(x5)) unfoldr#2(0) -> Nil unfoldr#2(S(x2)) -> Cons(x2, unfoldr#2(x2)) mult#2(0, x2) -> 0 mult#2(S(x4), x2) -> plus#2(x2, mult#2(x4, x2)) plus#2(0, x8) -> x8 plus#2(S(x4), x2) -> S(plus#2(x4, x2)) main(0) -> 0 main(S(x1)) -> sum#1(map#2(Cons(S(x1), unfoldr#2(S(x1))))) S is empty. Rewrite Strategy: PARALLEL_INNERMOST ---------------------------------------- (5) RelTrsToWeightedTrsProof (UPPER BOUND(ID)) Transformed relative TRS to weighted TRS ---------------------------------------- (6) Obligation: The Runtime Complexity (innermost) of the given CpxWeightedTrs could be proven to be BOUNDS(1, INF). The TRS R consists of the following rules: sum#1(Nil) -> 0 [1] sum#1(Cons(x2, x1)) -> plus#2(x2, sum#1(x1)) [1] map#2(Nil) -> Nil [1] map#2(Cons(x2, x5)) -> Cons(mult#2(x2, x2), map#2(x5)) [1] unfoldr#2(0) -> Nil [1] unfoldr#2(S(x2)) -> Cons(x2, unfoldr#2(x2)) [1] mult#2(0, x2) -> 0 [1] mult#2(S(x4), x2) -> plus#2(x2, mult#2(x4, x2)) [1] plus#2(0, x8) -> x8 [1] plus#2(S(x4), x2) -> S(plus#2(x4, x2)) [1] main(0) -> 0 [1] main(S(x1)) -> sum#1(map#2(Cons(S(x1), unfoldr#2(S(x1))))) [1] Rewrite Strategy: INNERMOST ---------------------------------------- (7) TypeInferenceProof (BOTH BOUNDS(ID, ID)) Infered types. ---------------------------------------- (8) Obligation: Runtime Complexity Weighted TRS with Types. The TRS R consists of the following rules: sum#1(Nil) -> 0 [1] sum#1(Cons(x2, x1)) -> plus#2(x2, sum#1(x1)) [1] map#2(Nil) -> Nil [1] map#2(Cons(x2, x5)) -> Cons(mult#2(x2, x2), map#2(x5)) [1] unfoldr#2(0) -> Nil [1] unfoldr#2(S(x2)) -> Cons(x2, unfoldr#2(x2)) [1] mult#2(0, x2) -> 0 [1] mult#2(S(x4), x2) -> plus#2(x2, mult#2(x4, x2)) [1] plus#2(0, x8) -> x8 [1] plus#2(S(x4), x2) -> S(plus#2(x4, x2)) [1] main(0) -> 0 [1] main(S(x1)) -> sum#1(map#2(Cons(S(x1), unfoldr#2(S(x1))))) [1] The TRS has the following type information: sum#1 :: Nil:Cons -> 0:S Nil :: Nil:Cons 0 :: 0:S Cons :: 0:S -> Nil:Cons -> Nil:Cons plus#2 :: 0:S -> 0:S -> 0:S map#2 :: Nil:Cons -> Nil:Cons mult#2 :: 0:S -> 0:S -> 0:S unfoldr#2 :: 0:S -> Nil:Cons S :: 0:S -> 0:S main :: 0:S -> 0:S Rewrite Strategy: INNERMOST ---------------------------------------- (9) 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 ---------------------------------------- (10) 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: sum#1(Nil) -> 0 [1] sum#1(Cons(x2, x1)) -> plus#2(x2, sum#1(x1)) [1] map#2(Nil) -> Nil [1] map#2(Cons(x2, x5)) -> Cons(mult#2(x2, x2), map#2(x5)) [1] unfoldr#2(0) -> Nil [1] unfoldr#2(S(x2)) -> Cons(x2, unfoldr#2(x2)) [1] mult#2(0, x2) -> 0 [1] mult#2(S(x4), x2) -> plus#2(x2, mult#2(x4, x2)) [1] plus#2(0, x8) -> x8 [1] plus#2(S(x4), x2) -> S(plus#2(x4, x2)) [1] main(0) -> 0 [1] main(S(x1)) -> sum#1(map#2(Cons(S(x1), unfoldr#2(S(x1))))) [1] The TRS has the following type information: sum#1 :: Nil:Cons -> 0:S Nil :: Nil:Cons 0 :: 0:S Cons :: 0:S -> Nil:Cons -> Nil:Cons plus#2 :: 0:S -> 0:S -> 0:S map#2 :: Nil:Cons -> Nil:Cons mult#2 :: 0:S -> 0:S -> 0:S unfoldr#2 :: 0:S -> Nil:Cons S :: 0:S -> 0:S main :: 0:S -> 0:S Rewrite Strategy: INNERMOST ---------------------------------------- (11) CpxTypedWeightedTrsToRntsProof (UPPER BOUND(ID)) Transformed the TRS into an over-approximating RNTS by (improved) Size Abstraction. The constant constructors are abstracted as follows: Nil => 0 0 => 0 ---------------------------------------- (12) Obligation: Complexity RNTS consisting of the following rules: main(z) -{ 1 }-> sum#1(map#2(1 + (1 + x1) + unfoldr#2(1 + x1))) :|: x1 >= 0, z = 1 + x1 main(z) -{ 1 }-> 0 :|: z = 0 map#2(z) -{ 1 }-> 0 :|: z = 0 map#2(z) -{ 1 }-> 1 + mult#2(x2, x2) + map#2(x5) :|: x5 >= 0, z = 1 + x2 + x5, x2 >= 0 mult#2(z, z') -{ 1 }-> plus#2(x2, mult#2(x4, x2)) :|: z' = x2, x4 >= 0, z = 1 + x4, x2 >= 0 mult#2(z, z') -{ 1 }-> 0 :|: z' = x2, z = 0, x2 >= 0 plus#2(z, z') -{ 1 }-> x8 :|: x8 >= 0, z = 0, z' = x8 plus#2(z, z') -{ 1 }-> 1 + plus#2(x4, x2) :|: z' = x2, x4 >= 0, z = 1 + x4, x2 >= 0 sum#1(z) -{ 1 }-> plus#2(x2, sum#1(x1)) :|: x1 >= 0, z = 1 + x2 + x1, x2 >= 0 sum#1(z) -{ 1 }-> 0 :|: z = 0 unfoldr#2(z) -{ 1 }-> 0 :|: z = 0 unfoldr#2(z) -{ 1 }-> 1 + x2 + unfoldr#2(x2) :|: z = 1 + x2, x2 >= 0 Only complete derivations are relevant for the runtime complexity. ---------------------------------------- (13) 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: main_1 (c) The following functions are completely defined: sum#1_1 mult#2_2 map#2_1 unfoldr#2_1 plus#2_2 Due to the following rules being added: none And the following fresh constants: none ---------------------------------------- (14) 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: sum#1(Nil) -> 0 [1] sum#1(Cons(x2, x1)) -> plus#2(x2, sum#1(x1)) [1] map#2(Nil) -> Nil [1] map#2(Cons(x2, x5)) -> Cons(mult#2(x2, x2), map#2(x5)) [1] unfoldr#2(0) -> Nil [1] unfoldr#2(S(x2)) -> Cons(x2, unfoldr#2(x2)) [1] mult#2(0, x2) -> 0 [1] mult#2(S(x4), x2) -> plus#2(x2, mult#2(x4, x2)) [1] plus#2(0, x8) -> x8 [1] plus#2(S(x4), x2) -> S(plus#2(x4, x2)) [1] main(0) -> 0 [1] main(S(x1)) -> sum#1(map#2(Cons(S(x1), unfoldr#2(S(x1))))) [1] The TRS has the following type information: sum#1 :: Nil:Cons -> 0:S Nil :: Nil:Cons 0 :: 0:S Cons :: 0:S -> Nil:Cons -> Nil:Cons plus#2 :: 0:S -> 0:S -> 0:S map#2 :: Nil:Cons -> Nil:Cons mult#2 :: 0:S -> 0:S -> 0:S unfoldr#2 :: 0:S -> Nil:Cons S :: 0:S -> 0:S main :: 0:S -> 0:S Rewrite Strategy: INNERMOST ---------------------------------------- (15) NarrowingProof (BOTH BOUNDS(ID, ID)) Narrowed the inner basic terms of all right-hand sides by a single narrowing step. ---------------------------------------- (16) 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: sum#1(Nil) -> 0 [1] sum#1(Cons(x2, Nil)) -> plus#2(x2, 0) [2] sum#1(Cons(x2, Cons(x2', x1'))) -> plus#2(x2, plus#2(x2', sum#1(x1'))) [2] map#2(Nil) -> Nil [1] map#2(Cons(x2, x5)) -> Cons(mult#2(x2, x2), map#2(x5)) [1] unfoldr#2(0) -> Nil [1] unfoldr#2(S(x2)) -> Cons(x2, unfoldr#2(x2)) [1] mult#2(0, x2) -> 0 [1] mult#2(S(0), x2) -> plus#2(x2, 0) [2] mult#2(S(S(x4')), x2) -> plus#2(x2, plus#2(x2, mult#2(x4', x2))) [2] plus#2(0, x8) -> x8 [1] plus#2(S(x4), x2) -> S(plus#2(x4, x2)) [1] main(0) -> 0 [1] main(S(x1)) -> sum#1(map#2(Cons(S(x1), Cons(x1, unfoldr#2(x1))))) [2] The TRS has the following type information: sum#1 :: Nil:Cons -> 0:S Nil :: Nil:Cons 0 :: 0:S Cons :: 0:S -> Nil:Cons -> Nil:Cons plus#2 :: 0:S -> 0:S -> 0:S map#2 :: Nil:Cons -> Nil:Cons mult#2 :: 0:S -> 0:S -> 0:S unfoldr#2 :: 0:S -> Nil:Cons S :: 0:S -> 0:S main :: 0:S -> 0:S Rewrite Strategy: INNERMOST ---------------------------------------- (17) CpxTypedWeightedTrsToRntsProof (UPPER BOUND(ID)) Transformed the TRS into an over-approximating RNTS by (improved) Size Abstraction. The constant constructors are abstracted as follows: Nil => 0 0 => 0 ---------------------------------------- (18) Obligation: Complexity RNTS consisting of the following rules: main(z) -{ 2 }-> sum#1(map#2(1 + (1 + x1) + (1 + x1 + unfoldr#2(x1)))) :|: x1 >= 0, z = 1 + x1 main(z) -{ 1 }-> 0 :|: z = 0 map#2(z) -{ 1 }-> 0 :|: z = 0 map#2(z) -{ 1 }-> 1 + mult#2(x2, x2) + map#2(x5) :|: x5 >= 0, z = 1 + x2 + x5, x2 >= 0 mult#2(z, z') -{ 2 }-> plus#2(x2, plus#2(x2, mult#2(x4', x2))) :|: z' = x2, z = 1 + (1 + x4'), x4' >= 0, x2 >= 0 mult#2(z, z') -{ 2 }-> plus#2(x2, 0) :|: z' = x2, z = 1 + 0, x2 >= 0 mult#2(z, z') -{ 1 }-> 0 :|: z' = x2, z = 0, x2 >= 0 plus#2(z, z') -{ 1 }-> x8 :|: x8 >= 0, z = 0, z' = x8 plus#2(z, z') -{ 1 }-> 1 + plus#2(x4, x2) :|: z' = x2, x4 >= 0, z = 1 + x4, x2 >= 0 sum#1(z) -{ 2 }-> plus#2(x2, plus#2(x2', sum#1(x1'))) :|: x2' >= 0, x1' >= 0, z = 1 + x2 + (1 + x2' + x1'), x2 >= 0 sum#1(z) -{ 2 }-> plus#2(x2, 0) :|: z = 1 + x2 + 0, x2 >= 0 sum#1(z) -{ 1 }-> 0 :|: z = 0 unfoldr#2(z) -{ 1 }-> 0 :|: z = 0 unfoldr#2(z) -{ 1 }-> 1 + x2 + unfoldr#2(x2) :|: z = 1 + x2, x2 >= 0 ---------------------------------------- (19) SimplificationProof (BOTH BOUNDS(ID, ID)) Simplified the RNTS by moving equalities from the constraints into the right-hand sides. ---------------------------------------- (20) Obligation: Complexity RNTS consisting of the following rules: main(z) -{ 2 }-> sum#1(map#2(1 + (1 + (z - 1)) + (1 + (z - 1) + unfoldr#2(z - 1)))) :|: z - 1 >= 0 main(z) -{ 1 }-> 0 :|: z = 0 map#2(z) -{ 1 }-> 0 :|: z = 0 map#2(z) -{ 1 }-> 1 + mult#2(x2, x2) + map#2(x5) :|: x5 >= 0, z = 1 + x2 + x5, x2 >= 0 mult#2(z, z') -{ 2 }-> plus#2(z', plus#2(z', mult#2(z - 2, z'))) :|: z - 2 >= 0, z' >= 0 mult#2(z, z') -{ 2 }-> plus#2(z', 0) :|: z = 1 + 0, z' >= 0 mult#2(z, z') -{ 1 }-> 0 :|: z = 0, z' >= 0 plus#2(z, z') -{ 1 }-> z' :|: z' >= 0, z = 0 plus#2(z, z') -{ 1 }-> 1 + plus#2(z - 1, z') :|: z - 1 >= 0, z' >= 0 sum#1(z) -{ 2 }-> plus#2(x2, plus#2(x2', sum#1(x1'))) :|: x2' >= 0, x1' >= 0, z = 1 + x2 + (1 + x2' + x1'), x2 >= 0 sum#1(z) -{ 2 }-> plus#2(z - 1, 0) :|: z - 1 >= 0 sum#1(z) -{ 1 }-> 0 :|: z = 0 unfoldr#2(z) -{ 1 }-> 0 :|: z = 0 unfoldr#2(z) -{ 1 }-> 1 + (z - 1) + unfoldr#2(z - 1) :|: z - 1 >= 0 ---------------------------------------- (21) CpxRntsAnalysisOrderProof (BOTH BOUNDS(ID, ID)) Found the following analysis order by SCC decomposition: { plus#2 } { unfoldr#2 } { mult#2 } { sum#1 } { map#2 } { main } ---------------------------------------- (22) Obligation: Complexity RNTS consisting of the following rules: main(z) -{ 2 }-> sum#1(map#2(1 + (1 + (z - 1)) + (1 + (z - 1) + unfoldr#2(z - 1)))) :|: z - 1 >= 0 main(z) -{ 1 }-> 0 :|: z = 0 map#2(z) -{ 1 }-> 0 :|: z = 0 map#2(z) -{ 1 }-> 1 + mult#2(x2, x2) + map#2(x5) :|: x5 >= 0, z = 1 + x2 + x5, x2 >= 0 mult#2(z, z') -{ 2 }-> plus#2(z', plus#2(z', mult#2(z - 2, z'))) :|: z - 2 >= 0, z' >= 0 mult#2(z, z') -{ 2 }-> plus#2(z', 0) :|: z = 1 + 0, z' >= 0 mult#2(z, z') -{ 1 }-> 0 :|: z = 0, z' >= 0 plus#2(z, z') -{ 1 }-> z' :|: z' >= 0, z = 0 plus#2(z, z') -{ 1 }-> 1 + plus#2(z - 1, z') :|: z - 1 >= 0, z' >= 0 sum#1(z) -{ 2 }-> plus#2(x2, plus#2(x2', sum#1(x1'))) :|: x2' >= 0, x1' >= 0, z = 1 + x2 + (1 + x2' + x1'), x2 >= 0 sum#1(z) -{ 2 }-> plus#2(z - 1, 0) :|: z - 1 >= 0 sum#1(z) -{ 1 }-> 0 :|: z = 0 unfoldr#2(z) -{ 1 }-> 0 :|: z = 0 unfoldr#2(z) -{ 1 }-> 1 + (z - 1) + unfoldr#2(z - 1) :|: z - 1 >= 0 Function symbols to be analyzed: {plus#2}, {unfoldr#2}, {mult#2}, {sum#1}, {map#2}, {main} ---------------------------------------- (23) ResultPropagationProof (UPPER BOUND(ID)) Applied inner abstraction using the recently inferred runtime/size bounds where possible. ---------------------------------------- (24) Obligation: Complexity RNTS consisting of the following rules: main(z) -{ 2 }-> sum#1(map#2(1 + (1 + (z - 1)) + (1 + (z - 1) + unfoldr#2(z - 1)))) :|: z - 1 >= 0 main(z) -{ 1 }-> 0 :|: z = 0 map#2(z) -{ 1 }-> 0 :|: z = 0 map#2(z) -{ 1 }-> 1 + mult#2(x2, x2) + map#2(x5) :|: x5 >= 0, z = 1 + x2 + x5, x2 >= 0 mult#2(z, z') -{ 2 }-> plus#2(z', plus#2(z', mult#2(z - 2, z'))) :|: z - 2 >= 0, z' >= 0 mult#2(z, z') -{ 2 }-> plus#2(z', 0) :|: z = 1 + 0, z' >= 0 mult#2(z, z') -{ 1 }-> 0 :|: z = 0, z' >= 0 plus#2(z, z') -{ 1 }-> z' :|: z' >= 0, z = 0 plus#2(z, z') -{ 1 }-> 1 + plus#2(z - 1, z') :|: z - 1 >= 0, z' >= 0 sum#1(z) -{ 2 }-> plus#2(x2, plus#2(x2', sum#1(x1'))) :|: x2' >= 0, x1' >= 0, z = 1 + x2 + (1 + x2' + x1'), x2 >= 0 sum#1(z) -{ 2 }-> plus#2(z - 1, 0) :|: z - 1 >= 0 sum#1(z) -{ 1 }-> 0 :|: z = 0 unfoldr#2(z) -{ 1 }-> 0 :|: z = 0 unfoldr#2(z) -{ 1 }-> 1 + (z - 1) + unfoldr#2(z - 1) :|: z - 1 >= 0 Function symbols to be analyzed: {plus#2}, {unfoldr#2}, {mult#2}, {sum#1}, {map#2}, {main} ---------------------------------------- (25) IntTrsBoundProof (UPPER BOUND(ID)) Computed SIZE bound using CoFloCo for: plus#2 after applying outer abstraction to obtain an ITS, resulting in: O(n^1) with polynomial bound: z + z' ---------------------------------------- (26) Obligation: Complexity RNTS consisting of the following rules: main(z) -{ 2 }-> sum#1(map#2(1 + (1 + (z - 1)) + (1 + (z - 1) + unfoldr#2(z - 1)))) :|: z - 1 >= 0 main(z) -{ 1 }-> 0 :|: z = 0 map#2(z) -{ 1 }-> 0 :|: z = 0 map#2(z) -{ 1 }-> 1 + mult#2(x2, x2) + map#2(x5) :|: x5 >= 0, z = 1 + x2 + x5, x2 >= 0 mult#2(z, z') -{ 2 }-> plus#2(z', plus#2(z', mult#2(z - 2, z'))) :|: z - 2 >= 0, z' >= 0 mult#2(z, z') -{ 2 }-> plus#2(z', 0) :|: z = 1 + 0, z' >= 0 mult#2(z, z') -{ 1 }-> 0 :|: z = 0, z' >= 0 plus#2(z, z') -{ 1 }-> z' :|: z' >= 0, z = 0 plus#2(z, z') -{ 1 }-> 1 + plus#2(z - 1, z') :|: z - 1 >= 0, z' >= 0 sum#1(z) -{ 2 }-> plus#2(x2, plus#2(x2', sum#1(x1'))) :|: x2' >= 0, x1' >= 0, z = 1 + x2 + (1 + x2' + x1'), x2 >= 0 sum#1(z) -{ 2 }-> plus#2(z - 1, 0) :|: z - 1 >= 0 sum#1(z) -{ 1 }-> 0 :|: z = 0 unfoldr#2(z) -{ 1 }-> 0 :|: z = 0 unfoldr#2(z) -{ 1 }-> 1 + (z - 1) + unfoldr#2(z - 1) :|: z - 1 >= 0 Function symbols to be analyzed: {plus#2}, {unfoldr#2}, {mult#2}, {sum#1}, {map#2}, {main} Previous analysis results are: plus#2: runtime: ?, size: O(n^1) [z + z'] ---------------------------------------- (27) IntTrsBoundProof (UPPER BOUND(ID)) Computed RUNTIME bound using CoFloCo for: plus#2 after applying outer abstraction to obtain an ITS, resulting in: O(n^1) with polynomial bound: 1 + z ---------------------------------------- (28) Obligation: Complexity RNTS consisting of the following rules: main(z) -{ 2 }-> sum#1(map#2(1 + (1 + (z - 1)) + (1 + (z - 1) + unfoldr#2(z - 1)))) :|: z - 1 >= 0 main(z) -{ 1 }-> 0 :|: z = 0 map#2(z) -{ 1 }-> 0 :|: z = 0 map#2(z) -{ 1 }-> 1 + mult#2(x2, x2) + map#2(x5) :|: x5 >= 0, z = 1 + x2 + x5, x2 >= 0 mult#2(z, z') -{ 2 }-> plus#2(z', plus#2(z', mult#2(z - 2, z'))) :|: z - 2 >= 0, z' >= 0 mult#2(z, z') -{ 2 }-> plus#2(z', 0) :|: z = 1 + 0, z' >= 0 mult#2(z, z') -{ 1 }-> 0 :|: z = 0, z' >= 0 plus#2(z, z') -{ 1 }-> z' :|: z' >= 0, z = 0 plus#2(z, z') -{ 1 }-> 1 + plus#2(z - 1, z') :|: z - 1 >= 0, z' >= 0 sum#1(z) -{ 2 }-> plus#2(x2, plus#2(x2', sum#1(x1'))) :|: x2' >= 0, x1' >= 0, z = 1 + x2 + (1 + x2' + x1'), x2 >= 0 sum#1(z) -{ 2 }-> plus#2(z - 1, 0) :|: z - 1 >= 0 sum#1(z) -{ 1 }-> 0 :|: z = 0 unfoldr#2(z) -{ 1 }-> 0 :|: z = 0 unfoldr#2(z) -{ 1 }-> 1 + (z - 1) + unfoldr#2(z - 1) :|: z - 1 >= 0 Function symbols to be analyzed: {unfoldr#2}, {mult#2}, {sum#1}, {map#2}, {main} Previous analysis results are: plus#2: runtime: O(n^1) [1 + z], size: O(n^1) [z + z'] ---------------------------------------- (29) ResultPropagationProof (UPPER BOUND(ID)) Applied inner abstraction using the recently inferred runtime/size bounds where possible. ---------------------------------------- (30) Obligation: Complexity RNTS consisting of the following rules: main(z) -{ 2 }-> sum#1(map#2(1 + (1 + (z - 1)) + (1 + (z - 1) + unfoldr#2(z - 1)))) :|: z - 1 >= 0 main(z) -{ 1 }-> 0 :|: z = 0 map#2(z) -{ 1 }-> 0 :|: z = 0 map#2(z) -{ 1 }-> 1 + mult#2(x2, x2) + map#2(x5) :|: x5 >= 0, z = 1 + x2 + x5, x2 >= 0 mult#2(z, z') -{ 3 + z' }-> s' :|: s' >= 0, s' <= z' + 0, z = 1 + 0, z' >= 0 mult#2(z, z') -{ 2 }-> plus#2(z', plus#2(z', mult#2(z - 2, z'))) :|: z - 2 >= 0, z' >= 0 mult#2(z, z') -{ 1 }-> 0 :|: z = 0, z' >= 0 plus#2(z, z') -{ 1 }-> z' :|: z' >= 0, z = 0 plus#2(z, z') -{ 1 + z }-> 1 + s'' :|: s'' >= 0, s'' <= z - 1 + z', z - 1 >= 0, z' >= 0 sum#1(z) -{ 2 + z }-> s :|: s >= 0, s <= z - 1 + 0, z - 1 >= 0 sum#1(z) -{ 2 }-> plus#2(x2, plus#2(x2', sum#1(x1'))) :|: x2' >= 0, x1' >= 0, z = 1 + x2 + (1 + x2' + x1'), x2 >= 0 sum#1(z) -{ 1 }-> 0 :|: z = 0 unfoldr#2(z) -{ 1 }-> 0 :|: z = 0 unfoldr#2(z) -{ 1 }-> 1 + (z - 1) + unfoldr#2(z - 1) :|: z - 1 >= 0 Function symbols to be analyzed: {unfoldr#2}, {mult#2}, {sum#1}, {map#2}, {main} Previous analysis results are: plus#2: runtime: O(n^1) [1 + z], size: O(n^1) [z + z'] ---------------------------------------- (31) IntTrsBoundProof (UPPER BOUND(ID)) Computed SIZE bound using CoFloCo for: unfoldr#2 after applying outer abstraction to obtain an ITS, resulting in: O(n^2) with polynomial bound: z^2 ---------------------------------------- (32) Obligation: Complexity RNTS consisting of the following rules: main(z) -{ 2 }-> sum#1(map#2(1 + (1 + (z - 1)) + (1 + (z - 1) + unfoldr#2(z - 1)))) :|: z - 1 >= 0 main(z) -{ 1 }-> 0 :|: z = 0 map#2(z) -{ 1 }-> 0 :|: z = 0 map#2(z) -{ 1 }-> 1 + mult#2(x2, x2) + map#2(x5) :|: x5 >= 0, z = 1 + x2 + x5, x2 >= 0 mult#2(z, z') -{ 3 + z' }-> s' :|: s' >= 0, s' <= z' + 0, z = 1 + 0, z' >= 0 mult#2(z, z') -{ 2 }-> plus#2(z', plus#2(z', mult#2(z - 2, z'))) :|: z - 2 >= 0, z' >= 0 mult#2(z, z') -{ 1 }-> 0 :|: z = 0, z' >= 0 plus#2(z, z') -{ 1 }-> z' :|: z' >= 0, z = 0 plus#2(z, z') -{ 1 + z }-> 1 + s'' :|: s'' >= 0, s'' <= z - 1 + z', z - 1 >= 0, z' >= 0 sum#1(z) -{ 2 + z }-> s :|: s >= 0, s <= z - 1 + 0, z - 1 >= 0 sum#1(z) -{ 2 }-> plus#2(x2, plus#2(x2', sum#1(x1'))) :|: x2' >= 0, x1' >= 0, z = 1 + x2 + (1 + x2' + x1'), x2 >= 0 sum#1(z) -{ 1 }-> 0 :|: z = 0 unfoldr#2(z) -{ 1 }-> 0 :|: z = 0 unfoldr#2(z) -{ 1 }-> 1 + (z - 1) + unfoldr#2(z - 1) :|: z - 1 >= 0 Function symbols to be analyzed: {unfoldr#2}, {mult#2}, {sum#1}, {map#2}, {main} Previous analysis results are: plus#2: runtime: O(n^1) [1 + z], size: O(n^1) [z + z'] unfoldr#2: runtime: ?, size: O(n^2) [z^2] ---------------------------------------- (33) IntTrsBoundProof (UPPER BOUND(ID)) Computed RUNTIME bound using CoFloCo for: unfoldr#2 after applying outer abstraction to obtain an ITS, resulting in: O(n^1) with polynomial bound: 1 + z ---------------------------------------- (34) Obligation: Complexity RNTS consisting of the following rules: main(z) -{ 2 }-> sum#1(map#2(1 + (1 + (z - 1)) + (1 + (z - 1) + unfoldr#2(z - 1)))) :|: z - 1 >= 0 main(z) -{ 1 }-> 0 :|: z = 0 map#2(z) -{ 1 }-> 0 :|: z = 0 map#2(z) -{ 1 }-> 1 + mult#2(x2, x2) + map#2(x5) :|: x5 >= 0, z = 1 + x2 + x5, x2 >= 0 mult#2(z, z') -{ 3 + z' }-> s' :|: s' >= 0, s' <= z' + 0, z = 1 + 0, z' >= 0 mult#2(z, z') -{ 2 }-> plus#2(z', plus#2(z', mult#2(z - 2, z'))) :|: z - 2 >= 0, z' >= 0 mult#2(z, z') -{ 1 }-> 0 :|: z = 0, z' >= 0 plus#2(z, z') -{ 1 }-> z' :|: z' >= 0, z = 0 plus#2(z, z') -{ 1 + z }-> 1 + s'' :|: s'' >= 0, s'' <= z - 1 + z', z - 1 >= 0, z' >= 0 sum#1(z) -{ 2 + z }-> s :|: s >= 0, s <= z - 1 + 0, z - 1 >= 0 sum#1(z) -{ 2 }-> plus#2(x2, plus#2(x2', sum#1(x1'))) :|: x2' >= 0, x1' >= 0, z = 1 + x2 + (1 + x2' + x1'), x2 >= 0 sum#1(z) -{ 1 }-> 0 :|: z = 0 unfoldr#2(z) -{ 1 }-> 0 :|: z = 0 unfoldr#2(z) -{ 1 }-> 1 + (z - 1) + unfoldr#2(z - 1) :|: z - 1 >= 0 Function symbols to be analyzed: {mult#2}, {sum#1}, {map#2}, {main} Previous analysis results are: plus#2: runtime: O(n^1) [1 + z], size: O(n^1) [z + z'] unfoldr#2: runtime: O(n^1) [1 + z], size: O(n^2) [z^2] ---------------------------------------- (35) ResultPropagationProof (UPPER BOUND(ID)) Applied inner abstraction using the recently inferred runtime/size bounds where possible. ---------------------------------------- (36) Obligation: Complexity RNTS consisting of the following rules: main(z) -{ 2 + z }-> sum#1(map#2(1 + (1 + (z - 1)) + (1 + (z - 1) + s2))) :|: s2 >= 0, s2 <= (z - 1) * (z - 1), z - 1 >= 0 main(z) -{ 1 }-> 0 :|: z = 0 map#2(z) -{ 1 }-> 0 :|: z = 0 map#2(z) -{ 1 }-> 1 + mult#2(x2, x2) + map#2(x5) :|: x5 >= 0, z = 1 + x2 + x5, x2 >= 0 mult#2(z, z') -{ 3 + z' }-> s' :|: s' >= 0, s' <= z' + 0, z = 1 + 0, z' >= 0 mult#2(z, z') -{ 2 }-> plus#2(z', plus#2(z', mult#2(z - 2, z'))) :|: z - 2 >= 0, z' >= 0 mult#2(z, z') -{ 1 }-> 0 :|: z = 0, z' >= 0 plus#2(z, z') -{ 1 }-> z' :|: z' >= 0, z = 0 plus#2(z, z') -{ 1 + z }-> 1 + s'' :|: s'' >= 0, s'' <= z - 1 + z', z - 1 >= 0, z' >= 0 sum#1(z) -{ 2 + z }-> s :|: s >= 0, s <= z - 1 + 0, z - 1 >= 0 sum#1(z) -{ 2 }-> plus#2(x2, plus#2(x2', sum#1(x1'))) :|: x2' >= 0, x1' >= 0, z = 1 + x2 + (1 + x2' + x1'), x2 >= 0 sum#1(z) -{ 1 }-> 0 :|: z = 0 unfoldr#2(z) -{ 1 }-> 0 :|: z = 0 unfoldr#2(z) -{ 1 + z }-> 1 + (z - 1) + s1 :|: s1 >= 0, s1 <= (z - 1) * (z - 1), z - 1 >= 0 Function symbols to be analyzed: {mult#2}, {sum#1}, {map#2}, {main} Previous analysis results are: plus#2: runtime: O(n^1) [1 + z], size: O(n^1) [z + z'] unfoldr#2: runtime: O(n^1) [1 + z], size: O(n^2) [z^2] ---------------------------------------- (37) IntTrsBoundProof (UPPER BOUND(ID)) Computed SIZE bound using KoAT for: mult#2 after applying outer abstraction to obtain an ITS, resulting in: O(n^2) with polynomial bound: 2*z*z' + z' ---------------------------------------- (38) Obligation: Complexity RNTS consisting of the following rules: main(z) -{ 2 + z }-> sum#1(map#2(1 + (1 + (z - 1)) + (1 + (z - 1) + s2))) :|: s2 >= 0, s2 <= (z - 1) * (z - 1), z - 1 >= 0 main(z) -{ 1 }-> 0 :|: z = 0 map#2(z) -{ 1 }-> 0 :|: z = 0 map#2(z) -{ 1 }-> 1 + mult#2(x2, x2) + map#2(x5) :|: x5 >= 0, z = 1 + x2 + x5, x2 >= 0 mult#2(z, z') -{ 3 + z' }-> s' :|: s' >= 0, s' <= z' + 0, z = 1 + 0, z' >= 0 mult#2(z, z') -{ 2 }-> plus#2(z', plus#2(z', mult#2(z - 2, z'))) :|: z - 2 >= 0, z' >= 0 mult#2(z, z') -{ 1 }-> 0 :|: z = 0, z' >= 0 plus#2(z, z') -{ 1 }-> z' :|: z' >= 0, z = 0 plus#2(z, z') -{ 1 + z }-> 1 + s'' :|: s'' >= 0, s'' <= z - 1 + z', z - 1 >= 0, z' >= 0 sum#1(z) -{ 2 + z }-> s :|: s >= 0, s <= z - 1 + 0, z - 1 >= 0 sum#1(z) -{ 2 }-> plus#2(x2, plus#2(x2', sum#1(x1'))) :|: x2' >= 0, x1' >= 0, z = 1 + x2 + (1 + x2' + x1'), x2 >= 0 sum#1(z) -{ 1 }-> 0 :|: z = 0 unfoldr#2(z) -{ 1 }-> 0 :|: z = 0 unfoldr#2(z) -{ 1 + z }-> 1 + (z - 1) + s1 :|: s1 >= 0, s1 <= (z - 1) * (z - 1), z - 1 >= 0 Function symbols to be analyzed: {mult#2}, {sum#1}, {map#2}, {main} Previous analysis results are: plus#2: runtime: O(n^1) [1 + z], size: O(n^1) [z + z'] unfoldr#2: runtime: O(n^1) [1 + z], size: O(n^2) [z^2] mult#2: runtime: ?, size: O(n^2) [2*z*z' + z'] ---------------------------------------- (39) IntTrsBoundProof (UPPER BOUND(ID)) Computed RUNTIME bound using KoAT for: mult#2 after applying outer abstraction to obtain an ITS, resulting in: O(n^2) with polynomial bound: 4 + 4*z + 2*z*z' + z' ---------------------------------------- (40) Obligation: Complexity RNTS consisting of the following rules: main(z) -{ 2 + z }-> sum#1(map#2(1 + (1 + (z - 1)) + (1 + (z - 1) + s2))) :|: s2 >= 0, s2 <= (z - 1) * (z - 1), z - 1 >= 0 main(z) -{ 1 }-> 0 :|: z = 0 map#2(z) -{ 1 }-> 0 :|: z = 0 map#2(z) -{ 1 }-> 1 + mult#2(x2, x2) + map#2(x5) :|: x5 >= 0, z = 1 + x2 + x5, x2 >= 0 mult#2(z, z') -{ 3 + z' }-> s' :|: s' >= 0, s' <= z' + 0, z = 1 + 0, z' >= 0 mult#2(z, z') -{ 2 }-> plus#2(z', plus#2(z', mult#2(z - 2, z'))) :|: z - 2 >= 0, z' >= 0 mult#2(z, z') -{ 1 }-> 0 :|: z = 0, z' >= 0 plus#2(z, z') -{ 1 }-> z' :|: z' >= 0, z = 0 plus#2(z, z') -{ 1 + z }-> 1 + s'' :|: s'' >= 0, s'' <= z - 1 + z', z - 1 >= 0, z' >= 0 sum#1(z) -{ 2 + z }-> s :|: s >= 0, s <= z - 1 + 0, z - 1 >= 0 sum#1(z) -{ 2 }-> plus#2(x2, plus#2(x2', sum#1(x1'))) :|: x2' >= 0, x1' >= 0, z = 1 + x2 + (1 + x2' + x1'), x2 >= 0 sum#1(z) -{ 1 }-> 0 :|: z = 0 unfoldr#2(z) -{ 1 }-> 0 :|: z = 0 unfoldr#2(z) -{ 1 + z }-> 1 + (z - 1) + s1 :|: s1 >= 0, s1 <= (z - 1) * (z - 1), z - 1 >= 0 Function symbols to be analyzed: {sum#1}, {map#2}, {main} Previous analysis results are: plus#2: runtime: O(n^1) [1 + z], size: O(n^1) [z + z'] unfoldr#2: runtime: O(n^1) [1 + z], size: O(n^2) [z^2] mult#2: runtime: O(n^2) [4 + 4*z + 2*z*z' + z'], size: O(n^2) [2*z*z' + z'] ---------------------------------------- (41) ResultPropagationProof (UPPER BOUND(ID)) Applied inner abstraction using the recently inferred runtime/size bounds where possible. ---------------------------------------- (42) Obligation: Complexity RNTS consisting of the following rules: main(z) -{ 2 + z }-> sum#1(map#2(1 + (1 + (z - 1)) + (1 + (z - 1) + s2))) :|: s2 >= 0, s2 <= (z - 1) * (z - 1), z - 1 >= 0 main(z) -{ 1 }-> 0 :|: z = 0 map#2(z) -{ 1 }-> 0 :|: z = 0 map#2(z) -{ 5 + 5*x2 + 2*x2^2 }-> 1 + s3 + map#2(x5) :|: s3 >= 0, s3 <= x2 + 2 * (x2 * x2), x5 >= 0, z = 1 + x2 + x5, x2 >= 0 mult#2(z, z') -{ 3 + z' }-> s' :|: s' >= 0, s' <= z' + 0, z = 1 + 0, z' >= 0 mult#2(z, z') -{ 4*z + 2*z*z' + -1*z' }-> s6 :|: s4 >= 0, s4 <= z' + 2 * (z' * (z - 2)), s5 >= 0, s5 <= z' + s4, s6 >= 0, s6 <= z' + s5, z - 2 >= 0, z' >= 0 mult#2(z, z') -{ 1 }-> 0 :|: z = 0, z' >= 0 plus#2(z, z') -{ 1 }-> z' :|: z' >= 0, z = 0 plus#2(z, z') -{ 1 + z }-> 1 + s'' :|: s'' >= 0, s'' <= z - 1 + z', z - 1 >= 0, z' >= 0 sum#1(z) -{ 2 + z }-> s :|: s >= 0, s <= z - 1 + 0, z - 1 >= 0 sum#1(z) -{ 2 }-> plus#2(x2, plus#2(x2', sum#1(x1'))) :|: x2' >= 0, x1' >= 0, z = 1 + x2 + (1 + x2' + x1'), x2 >= 0 sum#1(z) -{ 1 }-> 0 :|: z = 0 unfoldr#2(z) -{ 1 }-> 0 :|: z = 0 unfoldr#2(z) -{ 1 + z }-> 1 + (z - 1) + s1 :|: s1 >= 0, s1 <= (z - 1) * (z - 1), z - 1 >= 0 Function symbols to be analyzed: {sum#1}, {map#2}, {main} Previous analysis results are: plus#2: runtime: O(n^1) [1 + z], size: O(n^1) [z + z'] unfoldr#2: runtime: O(n^1) [1 + z], size: O(n^2) [z^2] mult#2: runtime: O(n^2) [4 + 4*z + 2*z*z' + z'], size: O(n^2) [2*z*z' + z'] ---------------------------------------- (43) IntTrsBoundProof (UPPER BOUND(ID)) Computed SIZE bound using KoAT for: sum#1 after applying outer abstraction to obtain an ITS, resulting in: O(n^1) with polynomial bound: z ---------------------------------------- (44) Obligation: Complexity RNTS consisting of the following rules: main(z) -{ 2 + z }-> sum#1(map#2(1 + (1 + (z - 1)) + (1 + (z - 1) + s2))) :|: s2 >= 0, s2 <= (z - 1) * (z - 1), z - 1 >= 0 main(z) -{ 1 }-> 0 :|: z = 0 map#2(z) -{ 1 }-> 0 :|: z = 0 map#2(z) -{ 5 + 5*x2 + 2*x2^2 }-> 1 + s3 + map#2(x5) :|: s3 >= 0, s3 <= x2 + 2 * (x2 * x2), x5 >= 0, z = 1 + x2 + x5, x2 >= 0 mult#2(z, z') -{ 3 + z' }-> s' :|: s' >= 0, s' <= z' + 0, z = 1 + 0, z' >= 0 mult#2(z, z') -{ 4*z + 2*z*z' + -1*z' }-> s6 :|: s4 >= 0, s4 <= z' + 2 * (z' * (z - 2)), s5 >= 0, s5 <= z' + s4, s6 >= 0, s6 <= z' + s5, z - 2 >= 0, z' >= 0 mult#2(z, z') -{ 1 }-> 0 :|: z = 0, z' >= 0 plus#2(z, z') -{ 1 }-> z' :|: z' >= 0, z = 0 plus#2(z, z') -{ 1 + z }-> 1 + s'' :|: s'' >= 0, s'' <= z - 1 + z', z - 1 >= 0, z' >= 0 sum#1(z) -{ 2 + z }-> s :|: s >= 0, s <= z - 1 + 0, z - 1 >= 0 sum#1(z) -{ 2 }-> plus#2(x2, plus#2(x2', sum#1(x1'))) :|: x2' >= 0, x1' >= 0, z = 1 + x2 + (1 + x2' + x1'), x2 >= 0 sum#1(z) -{ 1 }-> 0 :|: z = 0 unfoldr#2(z) -{ 1 }-> 0 :|: z = 0 unfoldr#2(z) -{ 1 + z }-> 1 + (z - 1) + s1 :|: s1 >= 0, s1 <= (z - 1) * (z - 1), z - 1 >= 0 Function symbols to be analyzed: {sum#1}, {map#2}, {main} Previous analysis results are: plus#2: runtime: O(n^1) [1 + z], size: O(n^1) [z + z'] unfoldr#2: runtime: O(n^1) [1 + z], size: O(n^2) [z^2] mult#2: runtime: O(n^2) [4 + 4*z + 2*z*z' + z'], size: O(n^2) [2*z*z' + z'] sum#1: runtime: ?, size: O(n^1) [z] ---------------------------------------- (45) IntTrsBoundProof (UPPER BOUND(ID)) Computed RUNTIME bound using CoFloCo for: sum#1 after applying outer abstraction to obtain an ITS, resulting in: O(n^1) with polynomial bound: 4 + 2*z ---------------------------------------- (46) Obligation: Complexity RNTS consisting of the following rules: main(z) -{ 2 + z }-> sum#1(map#2(1 + (1 + (z - 1)) + (1 + (z - 1) + s2))) :|: s2 >= 0, s2 <= (z - 1) * (z - 1), z - 1 >= 0 main(z) -{ 1 }-> 0 :|: z = 0 map#2(z) -{ 1 }-> 0 :|: z = 0 map#2(z) -{ 5 + 5*x2 + 2*x2^2 }-> 1 + s3 + map#2(x5) :|: s3 >= 0, s3 <= x2 + 2 * (x2 * x2), x5 >= 0, z = 1 + x2 + x5, x2 >= 0 mult#2(z, z') -{ 3 + z' }-> s' :|: s' >= 0, s' <= z' + 0, z = 1 + 0, z' >= 0 mult#2(z, z') -{ 4*z + 2*z*z' + -1*z' }-> s6 :|: s4 >= 0, s4 <= z' + 2 * (z' * (z - 2)), s5 >= 0, s5 <= z' + s4, s6 >= 0, s6 <= z' + s5, z - 2 >= 0, z' >= 0 mult#2(z, z') -{ 1 }-> 0 :|: z = 0, z' >= 0 plus#2(z, z') -{ 1 }-> z' :|: z' >= 0, z = 0 plus#2(z, z') -{ 1 + z }-> 1 + s'' :|: s'' >= 0, s'' <= z - 1 + z', z - 1 >= 0, z' >= 0 sum#1(z) -{ 2 + z }-> s :|: s >= 0, s <= z - 1 + 0, z - 1 >= 0 sum#1(z) -{ 2 }-> plus#2(x2, plus#2(x2', sum#1(x1'))) :|: x2' >= 0, x1' >= 0, z = 1 + x2 + (1 + x2' + x1'), x2 >= 0 sum#1(z) -{ 1 }-> 0 :|: z = 0 unfoldr#2(z) -{ 1 }-> 0 :|: z = 0 unfoldr#2(z) -{ 1 + z }-> 1 + (z - 1) + s1 :|: s1 >= 0, s1 <= (z - 1) * (z - 1), z - 1 >= 0 Function symbols to be analyzed: {map#2}, {main} Previous analysis results are: plus#2: runtime: O(n^1) [1 + z], size: O(n^1) [z + z'] unfoldr#2: runtime: O(n^1) [1 + z], size: O(n^2) [z^2] mult#2: runtime: O(n^2) [4 + 4*z + 2*z*z' + z'], size: O(n^2) [2*z*z' + z'] sum#1: runtime: O(n^1) [4 + 2*z], size: O(n^1) [z] ---------------------------------------- (47) ResultPropagationProof (UPPER BOUND(ID)) Applied inner abstraction using the recently inferred runtime/size bounds where possible. ---------------------------------------- (48) Obligation: Complexity RNTS consisting of the following rules: main(z) -{ 2 + z }-> sum#1(map#2(1 + (1 + (z - 1)) + (1 + (z - 1) + s2))) :|: s2 >= 0, s2 <= (z - 1) * (z - 1), z - 1 >= 0 main(z) -{ 1 }-> 0 :|: z = 0 map#2(z) -{ 1 }-> 0 :|: z = 0 map#2(z) -{ 5 + 5*x2 + 2*x2^2 }-> 1 + s3 + map#2(x5) :|: s3 >= 0, s3 <= x2 + 2 * (x2 * x2), x5 >= 0, z = 1 + x2 + x5, x2 >= 0 mult#2(z, z') -{ 3 + z' }-> s' :|: s' >= 0, s' <= z' + 0, z = 1 + 0, z' >= 0 mult#2(z, z') -{ 4*z + 2*z*z' + -1*z' }-> s6 :|: s4 >= 0, s4 <= z' + 2 * (z' * (z - 2)), s5 >= 0, s5 <= z' + s4, s6 >= 0, s6 <= z' + s5, z - 2 >= 0, z' >= 0 mult#2(z, z') -{ 1 }-> 0 :|: z = 0, z' >= 0 plus#2(z, z') -{ 1 }-> z' :|: z' >= 0, z = 0 plus#2(z, z') -{ 1 + z }-> 1 + s'' :|: s'' >= 0, s'' <= z - 1 + z', z - 1 >= 0, z' >= 0 sum#1(z) -{ 2 + z }-> s :|: s >= 0, s <= z - 1 + 0, z - 1 >= 0 sum#1(z) -{ 8 + 2*x1' + x2 + x2' }-> s9 :|: s7 >= 0, s7 <= x1', s8 >= 0, s8 <= x2' + s7, s9 >= 0, s9 <= x2 + s8, x2' >= 0, x1' >= 0, z = 1 + x2 + (1 + x2' + x1'), x2 >= 0 sum#1(z) -{ 1 }-> 0 :|: z = 0 unfoldr#2(z) -{ 1 }-> 0 :|: z = 0 unfoldr#2(z) -{ 1 + z }-> 1 + (z - 1) + s1 :|: s1 >= 0, s1 <= (z - 1) * (z - 1), z - 1 >= 0 Function symbols to be analyzed: {map#2}, {main} Previous analysis results are: plus#2: runtime: O(n^1) [1 + z], size: O(n^1) [z + z'] unfoldr#2: runtime: O(n^1) [1 + z], size: O(n^2) [z^2] mult#2: runtime: O(n^2) [4 + 4*z + 2*z*z' + z'], size: O(n^2) [2*z*z' + z'] sum#1: runtime: O(n^1) [4 + 2*z], size: O(n^1) [z] ---------------------------------------- (49) IntTrsBoundProof (UPPER BOUND(ID)) Computed SIZE bound using CoFloCo for: map#2 after applying outer abstraction to obtain an ITS, resulting in: INF with polynomial bound: ? ---------------------------------------- (50) Obligation: Complexity RNTS consisting of the following rules: main(z) -{ 2 + z }-> sum#1(map#2(1 + (1 + (z - 1)) + (1 + (z - 1) + s2))) :|: s2 >= 0, s2 <= (z - 1) * (z - 1), z - 1 >= 0 main(z) -{ 1 }-> 0 :|: z = 0 map#2(z) -{ 1 }-> 0 :|: z = 0 map#2(z) -{ 5 + 5*x2 + 2*x2^2 }-> 1 + s3 + map#2(x5) :|: s3 >= 0, s3 <= x2 + 2 * (x2 * x2), x5 >= 0, z = 1 + x2 + x5, x2 >= 0 mult#2(z, z') -{ 3 + z' }-> s' :|: s' >= 0, s' <= z' + 0, z = 1 + 0, z' >= 0 mult#2(z, z') -{ 4*z + 2*z*z' + -1*z' }-> s6 :|: s4 >= 0, s4 <= z' + 2 * (z' * (z - 2)), s5 >= 0, s5 <= z' + s4, s6 >= 0, s6 <= z' + s5, z - 2 >= 0, z' >= 0 mult#2(z, z') -{ 1 }-> 0 :|: z = 0, z' >= 0 plus#2(z, z') -{ 1 }-> z' :|: z' >= 0, z = 0 plus#2(z, z') -{ 1 + z }-> 1 + s'' :|: s'' >= 0, s'' <= z - 1 + z', z - 1 >= 0, z' >= 0 sum#1(z) -{ 2 + z }-> s :|: s >= 0, s <= z - 1 + 0, z - 1 >= 0 sum#1(z) -{ 8 + 2*x1' + x2 + x2' }-> s9 :|: s7 >= 0, s7 <= x1', s8 >= 0, s8 <= x2' + s7, s9 >= 0, s9 <= x2 + s8, x2' >= 0, x1' >= 0, z = 1 + x2 + (1 + x2' + x1'), x2 >= 0 sum#1(z) -{ 1 }-> 0 :|: z = 0 unfoldr#2(z) -{ 1 }-> 0 :|: z = 0 unfoldr#2(z) -{ 1 + z }-> 1 + (z - 1) + s1 :|: s1 >= 0, s1 <= (z - 1) * (z - 1), z - 1 >= 0 Function symbols to be analyzed: {map#2}, {main} Previous analysis results are: plus#2: runtime: O(n^1) [1 + z], size: O(n^1) [z + z'] unfoldr#2: runtime: O(n^1) [1 + z], size: O(n^2) [z^2] mult#2: runtime: O(n^2) [4 + 4*z + 2*z*z' + z'], size: O(n^2) [2*z*z' + z'] sum#1: runtime: O(n^1) [4 + 2*z], size: O(n^1) [z] map#2: runtime: ?, size: INF ---------------------------------------- (51) IntTrsBoundProof (UPPER BOUND(ID)) Computed RUNTIME bound using KoAT for: map#2 after applying outer abstraction to obtain an ITS, resulting in: O(n^3) with polynomial bound: 1 + 5*z + 5*z^2 + 2*z^3 ---------------------------------------- (52) Obligation: Complexity RNTS consisting of the following rules: main(z) -{ 2 + z }-> sum#1(map#2(1 + (1 + (z - 1)) + (1 + (z - 1) + s2))) :|: s2 >= 0, s2 <= (z - 1) * (z - 1), z - 1 >= 0 main(z) -{ 1 }-> 0 :|: z = 0 map#2(z) -{ 1 }-> 0 :|: z = 0 map#2(z) -{ 5 + 5*x2 + 2*x2^2 }-> 1 + s3 + map#2(x5) :|: s3 >= 0, s3 <= x2 + 2 * (x2 * x2), x5 >= 0, z = 1 + x2 + x5, x2 >= 0 mult#2(z, z') -{ 3 + z' }-> s' :|: s' >= 0, s' <= z' + 0, z = 1 + 0, z' >= 0 mult#2(z, z') -{ 4*z + 2*z*z' + -1*z' }-> s6 :|: s4 >= 0, s4 <= z' + 2 * (z' * (z - 2)), s5 >= 0, s5 <= z' + s4, s6 >= 0, s6 <= z' + s5, z - 2 >= 0, z' >= 0 mult#2(z, z') -{ 1 }-> 0 :|: z = 0, z' >= 0 plus#2(z, z') -{ 1 }-> z' :|: z' >= 0, z = 0 plus#2(z, z') -{ 1 + z }-> 1 + s'' :|: s'' >= 0, s'' <= z - 1 + z', z - 1 >= 0, z' >= 0 sum#1(z) -{ 2 + z }-> s :|: s >= 0, s <= z - 1 + 0, z - 1 >= 0 sum#1(z) -{ 8 + 2*x1' + x2 + x2' }-> s9 :|: s7 >= 0, s7 <= x1', s8 >= 0, s8 <= x2' + s7, s9 >= 0, s9 <= x2 + s8, x2' >= 0, x1' >= 0, z = 1 + x2 + (1 + x2' + x1'), x2 >= 0 sum#1(z) -{ 1 }-> 0 :|: z = 0 unfoldr#2(z) -{ 1 }-> 0 :|: z = 0 unfoldr#2(z) -{ 1 + z }-> 1 + (z - 1) + s1 :|: s1 >= 0, s1 <= (z - 1) * (z - 1), z - 1 >= 0 Function symbols to be analyzed: {main} Previous analysis results are: plus#2: runtime: O(n^1) [1 + z], size: O(n^1) [z + z'] unfoldr#2: runtime: O(n^1) [1 + z], size: O(n^2) [z^2] mult#2: runtime: O(n^2) [4 + 4*z + 2*z*z' + z'], size: O(n^2) [2*z*z' + z'] sum#1: runtime: O(n^1) [4 + 2*z], size: O(n^1) [z] map#2: runtime: O(n^3) [1 + 5*z + 5*z^2 + 2*z^3], size: INF ---------------------------------------- (53) ResultPropagationProof (UPPER BOUND(ID)) Applied inner abstraction using the recently inferred runtime/size bounds where possible. ---------------------------------------- (54) Obligation: Complexity RNTS consisting of the following rules: main(z) -{ 19 + 2*s11 + 21*s2 + 44*s2*z + 24*s2*z^2 + 11*s2^2 + 12*s2^2*z + 2*s2^3 + 43*z + 44*z^2 + 16*z^3 }-> s12 :|: s11 >= 0, s11 <= inf', s12 >= 0, s12 <= s11, s2 >= 0, s2 <= (z - 1) * (z - 1), z - 1 >= 0 main(z) -{ 1 }-> 0 :|: z = 0 map#2(z) -{ 1 }-> 0 :|: z = 0 map#2(z) -{ 6 + 5*x2 + 2*x2^2 + 5*x5 + 5*x5^2 + 2*x5^3 }-> 1 + s3 + s10 :|: s10 >= 0, s10 <= inf, s3 >= 0, s3 <= x2 + 2 * (x2 * x2), x5 >= 0, z = 1 + x2 + x5, x2 >= 0 mult#2(z, z') -{ 3 + z' }-> s' :|: s' >= 0, s' <= z' + 0, z = 1 + 0, z' >= 0 mult#2(z, z') -{ 4*z + 2*z*z' + -1*z' }-> s6 :|: s4 >= 0, s4 <= z' + 2 * (z' * (z - 2)), s5 >= 0, s5 <= z' + s4, s6 >= 0, s6 <= z' + s5, z - 2 >= 0, z' >= 0 mult#2(z, z') -{ 1 }-> 0 :|: z = 0, z' >= 0 plus#2(z, z') -{ 1 }-> z' :|: z' >= 0, z = 0 plus#2(z, z') -{ 1 + z }-> 1 + s'' :|: s'' >= 0, s'' <= z - 1 + z', z - 1 >= 0, z' >= 0 sum#1(z) -{ 2 + z }-> s :|: s >= 0, s <= z - 1 + 0, z - 1 >= 0 sum#1(z) -{ 8 + 2*x1' + x2 + x2' }-> s9 :|: s7 >= 0, s7 <= x1', s8 >= 0, s8 <= x2' + s7, s9 >= 0, s9 <= x2 + s8, x2' >= 0, x1' >= 0, z = 1 + x2 + (1 + x2' + x1'), x2 >= 0 sum#1(z) -{ 1 }-> 0 :|: z = 0 unfoldr#2(z) -{ 1 }-> 0 :|: z = 0 unfoldr#2(z) -{ 1 + z }-> 1 + (z - 1) + s1 :|: s1 >= 0, s1 <= (z - 1) * (z - 1), z - 1 >= 0 Function symbols to be analyzed: {main} Previous analysis results are: plus#2: runtime: O(n^1) [1 + z], size: O(n^1) [z + z'] unfoldr#2: runtime: O(n^1) [1 + z], size: O(n^2) [z^2] mult#2: runtime: O(n^2) [4 + 4*z + 2*z*z' + z'], size: O(n^2) [2*z*z' + z'] sum#1: runtime: O(n^1) [4 + 2*z], size: O(n^1) [z] map#2: runtime: O(n^3) [1 + 5*z + 5*z^2 + 2*z^3], size: INF ---------------------------------------- (55) IntTrsBoundProof (UPPER BOUND(ID)) Computed SIZE bound using CoFloCo for: main after applying outer abstraction to obtain an ITS, resulting in: INF with polynomial bound: ? ---------------------------------------- (56) Obligation: Complexity RNTS consisting of the following rules: main(z) -{ 19 + 2*s11 + 21*s2 + 44*s2*z + 24*s2*z^2 + 11*s2^2 + 12*s2^2*z + 2*s2^3 + 43*z + 44*z^2 + 16*z^3 }-> s12 :|: s11 >= 0, s11 <= inf', s12 >= 0, s12 <= s11, s2 >= 0, s2 <= (z - 1) * (z - 1), z - 1 >= 0 main(z) -{ 1 }-> 0 :|: z = 0 map#2(z) -{ 1 }-> 0 :|: z = 0 map#2(z) -{ 6 + 5*x2 + 2*x2^2 + 5*x5 + 5*x5^2 + 2*x5^3 }-> 1 + s3 + s10 :|: s10 >= 0, s10 <= inf, s3 >= 0, s3 <= x2 + 2 * (x2 * x2), x5 >= 0, z = 1 + x2 + x5, x2 >= 0 mult#2(z, z') -{ 3 + z' }-> s' :|: s' >= 0, s' <= z' + 0, z = 1 + 0, z' >= 0 mult#2(z, z') -{ 4*z + 2*z*z' + -1*z' }-> s6 :|: s4 >= 0, s4 <= z' + 2 * (z' * (z - 2)), s5 >= 0, s5 <= z' + s4, s6 >= 0, s6 <= z' + s5, z - 2 >= 0, z' >= 0 mult#2(z, z') -{ 1 }-> 0 :|: z = 0, z' >= 0 plus#2(z, z') -{ 1 }-> z' :|: z' >= 0, z = 0 plus#2(z, z') -{ 1 + z }-> 1 + s'' :|: s'' >= 0, s'' <= z - 1 + z', z - 1 >= 0, z' >= 0 sum#1(z) -{ 2 + z }-> s :|: s >= 0, s <= z - 1 + 0, z - 1 >= 0 sum#1(z) -{ 8 + 2*x1' + x2 + x2' }-> s9 :|: s7 >= 0, s7 <= x1', s8 >= 0, s8 <= x2' + s7, s9 >= 0, s9 <= x2 + s8, x2' >= 0, x1' >= 0, z = 1 + x2 + (1 + x2' + x1'), x2 >= 0 sum#1(z) -{ 1 }-> 0 :|: z = 0 unfoldr#2(z) -{ 1 }-> 0 :|: z = 0 unfoldr#2(z) -{ 1 + z }-> 1 + (z - 1) + s1 :|: s1 >= 0, s1 <= (z - 1) * (z - 1), z - 1 >= 0 Function symbols to be analyzed: {main} Previous analysis results are: plus#2: runtime: O(n^1) [1 + z], size: O(n^1) [z + z'] unfoldr#2: runtime: O(n^1) [1 + z], size: O(n^2) [z^2] mult#2: runtime: O(n^2) [4 + 4*z + 2*z*z' + z'], size: O(n^2) [2*z*z' + z'] sum#1: runtime: O(n^1) [4 + 2*z], size: O(n^1) [z] map#2: runtime: O(n^3) [1 + 5*z + 5*z^2 + 2*z^3], size: INF main: runtime: ?, size: INF ---------------------------------------- (57) IntTrsBoundProof (UPPER BOUND(ID)) Computed RUNTIME bound using CoFloCo for: main after applying outer abstraction to obtain an ITS, resulting in: INF with polynomial bound: ? ---------------------------------------- (58) Obligation: Complexity RNTS consisting of the following rules: main(z) -{ 19 + 2*s11 + 21*s2 + 44*s2*z + 24*s2*z^2 + 11*s2^2 + 12*s2^2*z + 2*s2^3 + 43*z + 44*z^2 + 16*z^3 }-> s12 :|: s11 >= 0, s11 <= inf', s12 >= 0, s12 <= s11, s2 >= 0, s2 <= (z - 1) * (z - 1), z - 1 >= 0 main(z) -{ 1 }-> 0 :|: z = 0 map#2(z) -{ 1 }-> 0 :|: z = 0 map#2(z) -{ 6 + 5*x2 + 2*x2^2 + 5*x5 + 5*x5^2 + 2*x5^3 }-> 1 + s3 + s10 :|: s10 >= 0, s10 <= inf, s3 >= 0, s3 <= x2 + 2 * (x2 * x2), x5 >= 0, z = 1 + x2 + x5, x2 >= 0 mult#2(z, z') -{ 3 + z' }-> s' :|: s' >= 0, s' <= z' + 0, z = 1 + 0, z' >= 0 mult#2(z, z') -{ 4*z + 2*z*z' + -1*z' }-> s6 :|: s4 >= 0, s4 <= z' + 2 * (z' * (z - 2)), s5 >= 0, s5 <= z' + s4, s6 >= 0, s6 <= z' + s5, z - 2 >= 0, z' >= 0 mult#2(z, z') -{ 1 }-> 0 :|: z = 0, z' >= 0 plus#2(z, z') -{ 1 }-> z' :|: z' >= 0, z = 0 plus#2(z, z') -{ 1 + z }-> 1 + s'' :|: s'' >= 0, s'' <= z - 1 + z', z - 1 >= 0, z' >= 0 sum#1(z) -{ 2 + z }-> s :|: s >= 0, s <= z - 1 + 0, z - 1 >= 0 sum#1(z) -{ 8 + 2*x1' + x2 + x2' }-> s9 :|: s7 >= 0, s7 <= x1', s8 >= 0, s8 <= x2' + s7, s9 >= 0, s9 <= x2 + s8, x2' >= 0, x1' >= 0, z = 1 + x2 + (1 + x2' + x1'), x2 >= 0 sum#1(z) -{ 1 }-> 0 :|: z = 0 unfoldr#2(z) -{ 1 }-> 0 :|: z = 0 unfoldr#2(z) -{ 1 + z }-> 1 + (z - 1) + s1 :|: s1 >= 0, s1 <= (z - 1) * (z - 1), z - 1 >= 0 Function symbols to be analyzed: {main} Previous analysis results are: plus#2: runtime: O(n^1) [1 + z], size: O(n^1) [z + z'] unfoldr#2: runtime: O(n^1) [1 + z], size: O(n^2) [z^2] mult#2: runtime: O(n^2) [4 + 4*z + 2*z*z' + z'], size: O(n^2) [2*z*z' + z'] sum#1: runtime: O(n^1) [4 + 2*z], size: O(n^1) [z] map#2: runtime: O(n^3) [1 + 5*z + 5*z^2 + 2*z^3], size: INF main: runtime: INF, size: INF ---------------------------------------- (59) CpxTrsToCdtProof (UPPER BOUND(ID)) Converted Cpx (relative) TRS with rewrite strategy PARALLEL_INNERMOST to CDT ---------------------------------------- (60) Obligation: Complexity Dependency Tuples Problem Rules: sum#1(Nil) -> 0 sum#1(Cons(z0, z1)) -> plus#2(z0, sum#1(z1)) map#2(Nil) -> Nil map#2(Cons(z0, z1)) -> Cons(mult#2(z0, z0), map#2(z1)) unfoldr#2(0) -> Nil unfoldr#2(S(z0)) -> Cons(z0, unfoldr#2(z0)) mult#2(0, z0) -> 0 mult#2(S(z0), z1) -> plus#2(z1, mult#2(z0, z1)) plus#2(0, z0) -> z0 plus#2(S(z0), z1) -> S(plus#2(z0, z1)) main(0) -> 0 main(S(z0)) -> sum#1(map#2(Cons(S(z0), unfoldr#2(S(z0))))) Tuples: SUM#1(Nil) -> c SUM#1(Cons(z0, z1)) -> c1(PLUS#2(z0, sum#1(z1)), SUM#1(z1)) MAP#2(Nil) -> c2 MAP#2(Cons(z0, z1)) -> c3(MULT#2(z0, z0)) MAP#2(Cons(z0, z1)) -> c4(MAP#2(z1)) UNFOLDR#2(0) -> c5 UNFOLDR#2(S(z0)) -> c6(UNFOLDR#2(z0)) MULT#2(0, z0) -> c7 MULT#2(S(z0), z1) -> c8(PLUS#2(z1, mult#2(z0, z1)), MULT#2(z0, z1)) PLUS#2(0, z0) -> c9 PLUS#2(S(z0), z1) -> c10(PLUS#2(z0, z1)) MAIN(0) -> c11 MAIN(S(z0)) -> c12(SUM#1(map#2(Cons(S(z0), unfoldr#2(S(z0))))), MAP#2(Cons(S(z0), unfoldr#2(S(z0)))), UNFOLDR#2(S(z0))) S tuples: SUM#1(Nil) -> c SUM#1(Cons(z0, z1)) -> c1(PLUS#2(z0, sum#1(z1)), SUM#1(z1)) MAP#2(Nil) -> c2 MAP#2(Cons(z0, z1)) -> c3(MULT#2(z0, z0)) MAP#2(Cons(z0, z1)) -> c4(MAP#2(z1)) UNFOLDR#2(0) -> c5 UNFOLDR#2(S(z0)) -> c6(UNFOLDR#2(z0)) MULT#2(0, z0) -> c7 MULT#2(S(z0), z1) -> c8(PLUS#2(z1, mult#2(z0, z1)), MULT#2(z0, z1)) PLUS#2(0, z0) -> c9 PLUS#2(S(z0), z1) -> c10(PLUS#2(z0, z1)) MAIN(0) -> c11 MAIN(S(z0)) -> c12(SUM#1(map#2(Cons(S(z0), unfoldr#2(S(z0))))), MAP#2(Cons(S(z0), unfoldr#2(S(z0)))), UNFOLDR#2(S(z0))) K tuples:none Defined Rule Symbols: sum#1_1, map#2_1, unfoldr#2_1, mult#2_2, plus#2_2, main_1 Defined Pair Symbols: SUM#1_1, MAP#2_1, UNFOLDR#2_1, MULT#2_2, PLUS#2_2, MAIN_1 Compound Symbols: c, c1_2, c2, c3_1, c4_1, c5, c6_1, c7, c8_2, c9, c10_1, c11, c12_3 ---------------------------------------- (61) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID)) Removed 6 trailing nodes: MAIN(0) -> c11 MAP#2(Nil) -> c2 MULT#2(0, z0) -> c7 PLUS#2(0, z0) -> c9 UNFOLDR#2(0) -> c5 SUM#1(Nil) -> c ---------------------------------------- (62) Obligation: Complexity Dependency Tuples Problem Rules: sum#1(Nil) -> 0 sum#1(Cons(z0, z1)) -> plus#2(z0, sum#1(z1)) map#2(Nil) -> Nil map#2(Cons(z0, z1)) -> Cons(mult#2(z0, z0), map#2(z1)) unfoldr#2(0) -> Nil unfoldr#2(S(z0)) -> Cons(z0, unfoldr#2(z0)) mult#2(0, z0) -> 0 mult#2(S(z0), z1) -> plus#2(z1, mult#2(z0, z1)) plus#2(0, z0) -> z0 plus#2(S(z0), z1) -> S(plus#2(z0, z1)) main(0) -> 0 main(S(z0)) -> sum#1(map#2(Cons(S(z0), unfoldr#2(S(z0))))) Tuples: SUM#1(Cons(z0, z1)) -> c1(PLUS#2(z0, sum#1(z1)), SUM#1(z1)) MAP#2(Cons(z0, z1)) -> c3(MULT#2(z0, z0)) MAP#2(Cons(z0, z1)) -> c4(MAP#2(z1)) UNFOLDR#2(S(z0)) -> c6(UNFOLDR#2(z0)) MULT#2(S(z0), z1) -> c8(PLUS#2(z1, mult#2(z0, z1)), MULT#2(z0, z1)) PLUS#2(S(z0), z1) -> c10(PLUS#2(z0, z1)) MAIN(S(z0)) -> c12(SUM#1(map#2(Cons(S(z0), unfoldr#2(S(z0))))), MAP#2(Cons(S(z0), unfoldr#2(S(z0)))), UNFOLDR#2(S(z0))) S tuples: SUM#1(Cons(z0, z1)) -> c1(PLUS#2(z0, sum#1(z1)), SUM#1(z1)) MAP#2(Cons(z0, z1)) -> c3(MULT#2(z0, z0)) MAP#2(Cons(z0, z1)) -> c4(MAP#2(z1)) UNFOLDR#2(S(z0)) -> c6(UNFOLDR#2(z0)) MULT#2(S(z0), z1) -> c8(PLUS#2(z1, mult#2(z0, z1)), MULT#2(z0, z1)) PLUS#2(S(z0), z1) -> c10(PLUS#2(z0, z1)) MAIN(S(z0)) -> c12(SUM#1(map#2(Cons(S(z0), unfoldr#2(S(z0))))), MAP#2(Cons(S(z0), unfoldr#2(S(z0)))), UNFOLDR#2(S(z0))) K tuples:none Defined Rule Symbols: sum#1_1, map#2_1, unfoldr#2_1, mult#2_2, plus#2_2, main_1 Defined Pair Symbols: SUM#1_1, MAP#2_1, UNFOLDR#2_1, MULT#2_2, PLUS#2_2, MAIN_1 Compound Symbols: c1_2, c3_1, c4_1, c6_1, c8_2, c10_1, c12_3 ---------------------------------------- (63) CdtGraphSplitRhsProof (BOTH BOUNDS(ID, ID)) Split RHS of tuples not part of any SCC ---------------------------------------- (64) Obligation: Complexity Dependency Tuples Problem Rules: sum#1(Nil) -> 0 sum#1(Cons(z0, z1)) -> plus#2(z0, sum#1(z1)) map#2(Nil) -> Nil map#2(Cons(z0, z1)) -> Cons(mult#2(z0, z0), map#2(z1)) unfoldr#2(0) -> Nil unfoldr#2(S(z0)) -> Cons(z0, unfoldr#2(z0)) mult#2(0, z0) -> 0 mult#2(S(z0), z1) -> plus#2(z1, mult#2(z0, z1)) plus#2(0, z0) -> z0 plus#2(S(z0), z1) -> S(plus#2(z0, z1)) main(0) -> 0 main(S(z0)) -> sum#1(map#2(Cons(S(z0), unfoldr#2(S(z0))))) Tuples: SUM#1(Cons(z0, z1)) -> c1(PLUS#2(z0, sum#1(z1)), SUM#1(z1)) MAP#2(Cons(z0, z1)) -> c3(MULT#2(z0, z0)) MAP#2(Cons(z0, z1)) -> c4(MAP#2(z1)) UNFOLDR#2(S(z0)) -> c6(UNFOLDR#2(z0)) MULT#2(S(z0), z1) -> c8(PLUS#2(z1, mult#2(z0, z1)), MULT#2(z0, z1)) PLUS#2(S(z0), z1) -> c10(PLUS#2(z0, z1)) MAIN(S(z0)) -> c(SUM#1(map#2(Cons(S(z0), unfoldr#2(S(z0)))))) MAIN(S(z0)) -> c(MAP#2(Cons(S(z0), unfoldr#2(S(z0))))) MAIN(S(z0)) -> c(UNFOLDR#2(S(z0))) S tuples: SUM#1(Cons(z0, z1)) -> c1(PLUS#2(z0, sum#1(z1)), SUM#1(z1)) MAP#2(Cons(z0, z1)) -> c3(MULT#2(z0, z0)) MAP#2(Cons(z0, z1)) -> c4(MAP#2(z1)) UNFOLDR#2(S(z0)) -> c6(UNFOLDR#2(z0)) MULT#2(S(z0), z1) -> c8(PLUS#2(z1, mult#2(z0, z1)), MULT#2(z0, z1)) PLUS#2(S(z0), z1) -> c10(PLUS#2(z0, z1)) MAIN(S(z0)) -> c(SUM#1(map#2(Cons(S(z0), unfoldr#2(S(z0)))))) MAIN(S(z0)) -> c(MAP#2(Cons(S(z0), unfoldr#2(S(z0))))) MAIN(S(z0)) -> c(UNFOLDR#2(S(z0))) K tuples:none Defined Rule Symbols: sum#1_1, map#2_1, unfoldr#2_1, mult#2_2, plus#2_2, main_1 Defined Pair Symbols: SUM#1_1, MAP#2_1, UNFOLDR#2_1, MULT#2_2, PLUS#2_2, MAIN_1 Compound Symbols: c1_2, c3_1, c4_1, c6_1, c8_2, c10_1, c_1 ---------------------------------------- (65) CdtLeafRemovalProof (ComplexityIfPolyImplication) Removed 1 leading nodes: MAIN(S(z0)) -> c(UNFOLDR#2(S(z0))) ---------------------------------------- (66) Obligation: Complexity Dependency Tuples Problem Rules: sum#1(Nil) -> 0 sum#1(Cons(z0, z1)) -> plus#2(z0, sum#1(z1)) map#2(Nil) -> Nil map#2(Cons(z0, z1)) -> Cons(mult#2(z0, z0), map#2(z1)) unfoldr#2(0) -> Nil unfoldr#2(S(z0)) -> Cons(z0, unfoldr#2(z0)) mult#2(0, z0) -> 0 mult#2(S(z0), z1) -> plus#2(z1, mult#2(z0, z1)) plus#2(0, z0) -> z0 plus#2(S(z0), z1) -> S(plus#2(z0, z1)) main(0) -> 0 main(S(z0)) -> sum#1(map#2(Cons(S(z0), unfoldr#2(S(z0))))) Tuples: SUM#1(Cons(z0, z1)) -> c1(PLUS#2(z0, sum#1(z1)), SUM#1(z1)) MAP#2(Cons(z0, z1)) -> c3(MULT#2(z0, z0)) MAP#2(Cons(z0, z1)) -> c4(MAP#2(z1)) UNFOLDR#2(S(z0)) -> c6(UNFOLDR#2(z0)) MULT#2(S(z0), z1) -> c8(PLUS#2(z1, mult#2(z0, z1)), MULT#2(z0, z1)) PLUS#2(S(z0), z1) -> c10(PLUS#2(z0, z1)) MAIN(S(z0)) -> c(SUM#1(map#2(Cons(S(z0), unfoldr#2(S(z0)))))) MAIN(S(z0)) -> c(MAP#2(Cons(S(z0), unfoldr#2(S(z0))))) S tuples: SUM#1(Cons(z0, z1)) -> c1(PLUS#2(z0, sum#1(z1)), SUM#1(z1)) MAP#2(Cons(z0, z1)) -> c3(MULT#2(z0, z0)) MAP#2(Cons(z0, z1)) -> c4(MAP#2(z1)) UNFOLDR#2(S(z0)) -> c6(UNFOLDR#2(z0)) MULT#2(S(z0), z1) -> c8(PLUS#2(z1, mult#2(z0, z1)), MULT#2(z0, z1)) PLUS#2(S(z0), z1) -> c10(PLUS#2(z0, z1)) MAIN(S(z0)) -> c(SUM#1(map#2(Cons(S(z0), unfoldr#2(S(z0)))))) MAIN(S(z0)) -> c(MAP#2(Cons(S(z0), unfoldr#2(S(z0))))) K tuples:none Defined Rule Symbols: sum#1_1, map#2_1, unfoldr#2_1, mult#2_2, plus#2_2, main_1 Defined Pair Symbols: SUM#1_1, MAP#2_1, UNFOLDR#2_1, MULT#2_2, PLUS#2_2, MAIN_1 Compound Symbols: c1_2, c3_1, c4_1, c6_1, c8_2, c10_1, c_1 ---------------------------------------- (67) CdtKnowledgeProof (BOTH BOUNDS(ID, ID)) The following tuples could be moved from S to K by knowledge propagation: MAIN(S(z0)) -> c(SUM#1(map#2(Cons(S(z0), unfoldr#2(S(z0)))))) MAIN(S(z0)) -> c(MAP#2(Cons(S(z0), unfoldr#2(S(z0))))) ---------------------------------------- (68) Obligation: Complexity Dependency Tuples Problem Rules: sum#1(Nil) -> 0 sum#1(Cons(z0, z1)) -> plus#2(z0, sum#1(z1)) map#2(Nil) -> Nil map#2(Cons(z0, z1)) -> Cons(mult#2(z0, z0), map#2(z1)) unfoldr#2(0) -> Nil unfoldr#2(S(z0)) -> Cons(z0, unfoldr#2(z0)) mult#2(0, z0) -> 0 mult#2(S(z0), z1) -> plus#2(z1, mult#2(z0, z1)) plus#2(0, z0) -> z0 plus#2(S(z0), z1) -> S(plus#2(z0, z1)) main(0) -> 0 main(S(z0)) -> sum#1(map#2(Cons(S(z0), unfoldr#2(S(z0))))) Tuples: SUM#1(Cons(z0, z1)) -> c1(PLUS#2(z0, sum#1(z1)), SUM#1(z1)) MAP#2(Cons(z0, z1)) -> c3(MULT#2(z0, z0)) MAP#2(Cons(z0, z1)) -> c4(MAP#2(z1)) UNFOLDR#2(S(z0)) -> c6(UNFOLDR#2(z0)) MULT#2(S(z0), z1) -> c8(PLUS#2(z1, mult#2(z0, z1)), MULT#2(z0, z1)) PLUS#2(S(z0), z1) -> c10(PLUS#2(z0, z1)) MAIN(S(z0)) -> c(SUM#1(map#2(Cons(S(z0), unfoldr#2(S(z0)))))) MAIN(S(z0)) -> c(MAP#2(Cons(S(z0), unfoldr#2(S(z0))))) S tuples: SUM#1(Cons(z0, z1)) -> c1(PLUS#2(z0, sum#1(z1)), SUM#1(z1)) MAP#2(Cons(z0, z1)) -> c3(MULT#2(z0, z0)) MAP#2(Cons(z0, z1)) -> c4(MAP#2(z1)) UNFOLDR#2(S(z0)) -> c6(UNFOLDR#2(z0)) MULT#2(S(z0), z1) -> c8(PLUS#2(z1, mult#2(z0, z1)), MULT#2(z0, z1)) PLUS#2(S(z0), z1) -> c10(PLUS#2(z0, z1)) K tuples: MAIN(S(z0)) -> c(SUM#1(map#2(Cons(S(z0), unfoldr#2(S(z0)))))) MAIN(S(z0)) -> c(MAP#2(Cons(S(z0), unfoldr#2(S(z0))))) Defined Rule Symbols: sum#1_1, map#2_1, unfoldr#2_1, mult#2_2, plus#2_2, main_1 Defined Pair Symbols: SUM#1_1, MAP#2_1, UNFOLDR#2_1, MULT#2_2, PLUS#2_2, MAIN_1 Compound Symbols: c1_2, c3_1, c4_1, c6_1, c8_2, c10_1, c_1 ---------------------------------------- (69) CdtUsableRulesProof (BOTH BOUNDS(ID, ID)) The following rules are not usable and were removed: main(0) -> 0 main(S(z0)) -> sum#1(map#2(Cons(S(z0), unfoldr#2(S(z0))))) ---------------------------------------- (70) Obligation: Complexity Dependency Tuples Problem Rules: sum#1(Nil) -> 0 sum#1(Cons(z0, z1)) -> plus#2(z0, sum#1(z1)) plus#2(0, z0) -> z0 plus#2(S(z0), z1) -> S(plus#2(z0, z1)) mult#2(0, z0) -> 0 mult#2(S(z0), z1) -> plus#2(z1, mult#2(z0, z1)) map#2(Cons(z0, z1)) -> Cons(mult#2(z0, z0), map#2(z1)) map#2(Nil) -> Nil unfoldr#2(S(z0)) -> Cons(z0, unfoldr#2(z0)) unfoldr#2(0) -> Nil Tuples: SUM#1(Cons(z0, z1)) -> c1(PLUS#2(z0, sum#1(z1)), SUM#1(z1)) MAP#2(Cons(z0, z1)) -> c3(MULT#2(z0, z0)) MAP#2(Cons(z0, z1)) -> c4(MAP#2(z1)) UNFOLDR#2(S(z0)) -> c6(UNFOLDR#2(z0)) MULT#2(S(z0), z1) -> c8(PLUS#2(z1, mult#2(z0, z1)), MULT#2(z0, z1)) PLUS#2(S(z0), z1) -> c10(PLUS#2(z0, z1)) MAIN(S(z0)) -> c(SUM#1(map#2(Cons(S(z0), unfoldr#2(S(z0)))))) MAIN(S(z0)) -> c(MAP#2(Cons(S(z0), unfoldr#2(S(z0))))) S tuples: SUM#1(Cons(z0, z1)) -> c1(PLUS#2(z0, sum#1(z1)), SUM#1(z1)) MAP#2(Cons(z0, z1)) -> c3(MULT#2(z0, z0)) MAP#2(Cons(z0, z1)) -> c4(MAP#2(z1)) UNFOLDR#2(S(z0)) -> c6(UNFOLDR#2(z0)) MULT#2(S(z0), z1) -> c8(PLUS#2(z1, mult#2(z0, z1)), MULT#2(z0, z1)) PLUS#2(S(z0), z1) -> c10(PLUS#2(z0, z1)) K tuples: MAIN(S(z0)) -> c(SUM#1(map#2(Cons(S(z0), unfoldr#2(S(z0)))))) MAIN(S(z0)) -> c(MAP#2(Cons(S(z0), unfoldr#2(S(z0))))) Defined Rule Symbols: sum#1_1, plus#2_2, mult#2_2, map#2_1, unfoldr#2_1 Defined Pair Symbols: SUM#1_1, MAP#2_1, UNFOLDR#2_1, MULT#2_2, PLUS#2_2, MAIN_1 Compound Symbols: c1_2, c3_1, c4_1, c6_1, c8_2, c10_1, c_1 ---------------------------------------- (71) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1))) Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S. MAP#2(Cons(z0, z1)) -> c3(MULT#2(z0, z0)) We considered the (Usable) Rules:none And the Tuples: SUM#1(Cons(z0, z1)) -> c1(PLUS#2(z0, sum#1(z1)), SUM#1(z1)) MAP#2(Cons(z0, z1)) -> c3(MULT#2(z0, z0)) MAP#2(Cons(z0, z1)) -> c4(MAP#2(z1)) UNFOLDR#2(S(z0)) -> c6(UNFOLDR#2(z0)) MULT#2(S(z0), z1) -> c8(PLUS#2(z1, mult#2(z0, z1)), MULT#2(z0, z1)) PLUS#2(S(z0), z1) -> c10(PLUS#2(z0, z1)) MAIN(S(z0)) -> c(SUM#1(map#2(Cons(S(z0), unfoldr#2(S(z0)))))) MAIN(S(z0)) -> c(MAP#2(Cons(S(z0), unfoldr#2(S(z0))))) The order we found is given by the following interpretation: Polynomial interpretation : POL(0) = [1] POL(Cons(x_1, x_2)) = 0 POL(MAIN(x_1)) = [1] + x_1 POL(MAP#2(x_1)) = [1] POL(MULT#2(x_1, x_2)) = 0 POL(Nil) = [1] POL(PLUS#2(x_1, x_2)) = 0 POL(S(x_1)) = 0 POL(SUM#1(x_1)) = 0 POL(UNFOLDR#2(x_1)) = 0 POL(c(x_1)) = x_1 POL(c1(x_1, x_2)) = x_1 + x_2 POL(c10(x_1)) = x_1 POL(c3(x_1)) = x_1 POL(c4(x_1)) = x_1 POL(c6(x_1)) = x_1 POL(c8(x_1, x_2)) = x_1 + x_2 POL(map#2(x_1)) = [1] POL(mult#2(x_1, x_2)) = [1] + x_2 POL(plus#2(x_1, x_2)) = x_2 POL(sum#1(x_1)) = [1] POL(unfoldr#2(x_1)) = [1] + x_1 ---------------------------------------- (72) Obligation: Complexity Dependency Tuples Problem Rules: sum#1(Nil) -> 0 sum#1(Cons(z0, z1)) -> plus#2(z0, sum#1(z1)) plus#2(0, z0) -> z0 plus#2(S(z0), z1) -> S(plus#2(z0, z1)) mult#2(0, z0) -> 0 mult#2(S(z0), z1) -> plus#2(z1, mult#2(z0, z1)) map#2(Cons(z0, z1)) -> Cons(mult#2(z0, z0), map#2(z1)) map#2(Nil) -> Nil unfoldr#2(S(z0)) -> Cons(z0, unfoldr#2(z0)) unfoldr#2(0) -> Nil Tuples: SUM#1(Cons(z0, z1)) -> c1(PLUS#2(z0, sum#1(z1)), SUM#1(z1)) MAP#2(Cons(z0, z1)) -> c3(MULT#2(z0, z0)) MAP#2(Cons(z0, z1)) -> c4(MAP#2(z1)) UNFOLDR#2(S(z0)) -> c6(UNFOLDR#2(z0)) MULT#2(S(z0), z1) -> c8(PLUS#2(z1, mult#2(z0, z1)), MULT#2(z0, z1)) PLUS#2(S(z0), z1) -> c10(PLUS#2(z0, z1)) MAIN(S(z0)) -> c(SUM#1(map#2(Cons(S(z0), unfoldr#2(S(z0)))))) MAIN(S(z0)) -> c(MAP#2(Cons(S(z0), unfoldr#2(S(z0))))) S tuples: SUM#1(Cons(z0, z1)) -> c1(PLUS#2(z0, sum#1(z1)), SUM#1(z1)) MAP#2(Cons(z0, z1)) -> c4(MAP#2(z1)) UNFOLDR#2(S(z0)) -> c6(UNFOLDR#2(z0)) MULT#2(S(z0), z1) -> c8(PLUS#2(z1, mult#2(z0, z1)), MULT#2(z0, z1)) PLUS#2(S(z0), z1) -> c10(PLUS#2(z0, z1)) K tuples: MAIN(S(z0)) -> c(SUM#1(map#2(Cons(S(z0), unfoldr#2(S(z0)))))) MAIN(S(z0)) -> c(MAP#2(Cons(S(z0), unfoldr#2(S(z0))))) MAP#2(Cons(z0, z1)) -> c3(MULT#2(z0, z0)) Defined Rule Symbols: sum#1_1, plus#2_2, mult#2_2, map#2_1, unfoldr#2_1 Defined Pair Symbols: SUM#1_1, MAP#2_1, UNFOLDR#2_1, MULT#2_2, PLUS#2_2, MAIN_1 Compound Symbols: c1_2, c3_1, c4_1, c6_1, c8_2, c10_1, c_1 ---------------------------------------- (73) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1))) Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S. UNFOLDR#2(S(z0)) -> c6(UNFOLDR#2(z0)) We considered the (Usable) Rules:none And the Tuples: SUM#1(Cons(z0, z1)) -> c1(PLUS#2(z0, sum#1(z1)), SUM#1(z1)) MAP#2(Cons(z0, z1)) -> c3(MULT#2(z0, z0)) MAP#2(Cons(z0, z1)) -> c4(MAP#2(z1)) UNFOLDR#2(S(z0)) -> c6(UNFOLDR#2(z0)) MULT#2(S(z0), z1) -> c8(PLUS#2(z1, mult#2(z0, z1)), MULT#2(z0, z1)) PLUS#2(S(z0), z1) -> c10(PLUS#2(z0, z1)) MAIN(S(z0)) -> c(SUM#1(map#2(Cons(S(z0), unfoldr#2(S(z0)))))) MAIN(S(z0)) -> c(MAP#2(Cons(S(z0), unfoldr#2(S(z0))))) The order we found is given by the following interpretation: Polynomial interpretation : POL(0) = [1] POL(Cons(x_1, x_2)) = 0 POL(MAIN(x_1)) = [1] + x_1 POL(MAP#2(x_1)) = [1] POL(MULT#2(x_1, x_2)) = [1] POL(Nil) = [1] POL(PLUS#2(x_1, x_2)) = 0 POL(S(x_1)) = [1] + x_1 POL(SUM#1(x_1)) = 0 POL(UNFOLDR#2(x_1)) = x_1 POL(c(x_1)) = x_1 POL(c1(x_1, x_2)) = x_1 + x_2 POL(c10(x_1)) = x_1 POL(c3(x_1)) = x_1 POL(c4(x_1)) = x_1 POL(c6(x_1)) = x_1 POL(c8(x_1, x_2)) = x_1 + x_2 POL(map#2(x_1)) = [1] POL(mult#2(x_1, x_2)) = [1] + x_1 + x_2 POL(plus#2(x_1, x_2)) = [1] + x_2 POL(sum#1(x_1)) = [1] + x_1 POL(unfoldr#2(x_1)) = [1] + x_1 ---------------------------------------- (74) Obligation: Complexity Dependency Tuples Problem Rules: sum#1(Nil) -> 0 sum#1(Cons(z0, z1)) -> plus#2(z0, sum#1(z1)) plus#2(0, z0) -> z0 plus#2(S(z0), z1) -> S(plus#2(z0, z1)) mult#2(0, z0) -> 0 mult#2(S(z0), z1) -> plus#2(z1, mult#2(z0, z1)) map#2(Cons(z0, z1)) -> Cons(mult#2(z0, z0), map#2(z1)) map#2(Nil) -> Nil unfoldr#2(S(z0)) -> Cons(z0, unfoldr#2(z0)) unfoldr#2(0) -> Nil Tuples: SUM#1(Cons(z0, z1)) -> c1(PLUS#2(z0, sum#1(z1)), SUM#1(z1)) MAP#2(Cons(z0, z1)) -> c3(MULT#2(z0, z0)) MAP#2(Cons(z0, z1)) -> c4(MAP#2(z1)) UNFOLDR#2(S(z0)) -> c6(UNFOLDR#2(z0)) MULT#2(S(z0), z1) -> c8(PLUS#2(z1, mult#2(z0, z1)), MULT#2(z0, z1)) PLUS#2(S(z0), z1) -> c10(PLUS#2(z0, z1)) MAIN(S(z0)) -> c(SUM#1(map#2(Cons(S(z0), unfoldr#2(S(z0)))))) MAIN(S(z0)) -> c(MAP#2(Cons(S(z0), unfoldr#2(S(z0))))) S tuples: SUM#1(Cons(z0, z1)) -> c1(PLUS#2(z0, sum#1(z1)), SUM#1(z1)) MAP#2(Cons(z0, z1)) -> c4(MAP#2(z1)) MULT#2(S(z0), z1) -> c8(PLUS#2(z1, mult#2(z0, z1)), MULT#2(z0, z1)) PLUS#2(S(z0), z1) -> c10(PLUS#2(z0, z1)) K tuples: MAIN(S(z0)) -> c(SUM#1(map#2(Cons(S(z0), unfoldr#2(S(z0)))))) MAIN(S(z0)) -> c(MAP#2(Cons(S(z0), unfoldr#2(S(z0))))) MAP#2(Cons(z0, z1)) -> c3(MULT#2(z0, z0)) UNFOLDR#2(S(z0)) -> c6(UNFOLDR#2(z0)) Defined Rule Symbols: sum#1_1, plus#2_2, mult#2_2, map#2_1, unfoldr#2_1 Defined Pair Symbols: SUM#1_1, MAP#2_1, UNFOLDR#2_1, MULT#2_2, PLUS#2_2, MAIN_1 Compound Symbols: c1_2, c3_1, c4_1, c6_1, c8_2, c10_1, c_1 ---------------------------------------- (75) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1))) Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S. MAP#2(Cons(z0, z1)) -> c4(MAP#2(z1)) We considered the (Usable) Rules: unfoldr#2(0) -> Nil unfoldr#2(S(z0)) -> Cons(z0, unfoldr#2(z0)) And the Tuples: SUM#1(Cons(z0, z1)) -> c1(PLUS#2(z0, sum#1(z1)), SUM#1(z1)) MAP#2(Cons(z0, z1)) -> c3(MULT#2(z0, z0)) MAP#2(Cons(z0, z1)) -> c4(MAP#2(z1)) UNFOLDR#2(S(z0)) -> c6(UNFOLDR#2(z0)) MULT#2(S(z0), z1) -> c8(PLUS#2(z1, mult#2(z0, z1)), MULT#2(z0, z1)) PLUS#2(S(z0), z1) -> c10(PLUS#2(z0, z1)) MAIN(S(z0)) -> c(SUM#1(map#2(Cons(S(z0), unfoldr#2(S(z0)))))) MAIN(S(z0)) -> c(MAP#2(Cons(S(z0), unfoldr#2(S(z0))))) The order we found is given by the following interpretation: Polynomial interpretation : POL(0) = [1] POL(Cons(x_1, x_2)) = [1] + x_2 POL(MAIN(x_1)) = [1] + x_1 POL(MAP#2(x_1)) = x_1 POL(MULT#2(x_1, x_2)) = [1] POL(Nil) = [1] POL(PLUS#2(x_1, x_2)) = 0 POL(S(x_1)) = [1] + x_1 POL(SUM#1(x_1)) = 0 POL(UNFOLDR#2(x_1)) = x_1 POL(c(x_1)) = x_1 POL(c1(x_1, x_2)) = x_1 + x_2 POL(c10(x_1)) = x_1 POL(c3(x_1)) = x_1 POL(c4(x_1)) = x_1 POL(c6(x_1)) = x_1 POL(c8(x_1, x_2)) = x_1 + x_2 POL(map#2(x_1)) = [1] POL(mult#2(x_1, x_2)) = [1] + x_1 + x_2 POL(plus#2(x_1, x_2)) = [1] + x_1 + x_2 POL(sum#1(x_1)) = [1] + x_1 POL(unfoldr#2(x_1)) = x_1 ---------------------------------------- (76) Obligation: Complexity Dependency Tuples Problem Rules: sum#1(Nil) -> 0 sum#1(Cons(z0, z1)) -> plus#2(z0, sum#1(z1)) plus#2(0, z0) -> z0 plus#2(S(z0), z1) -> S(plus#2(z0, z1)) mult#2(0, z0) -> 0 mult#2(S(z0), z1) -> plus#2(z1, mult#2(z0, z1)) map#2(Cons(z0, z1)) -> Cons(mult#2(z0, z0), map#2(z1)) map#2(Nil) -> Nil unfoldr#2(S(z0)) -> Cons(z0, unfoldr#2(z0)) unfoldr#2(0) -> Nil Tuples: SUM#1(Cons(z0, z1)) -> c1(PLUS#2(z0, sum#1(z1)), SUM#1(z1)) MAP#2(Cons(z0, z1)) -> c3(MULT#2(z0, z0)) MAP#2(Cons(z0, z1)) -> c4(MAP#2(z1)) UNFOLDR#2(S(z0)) -> c6(UNFOLDR#2(z0)) MULT#2(S(z0), z1) -> c8(PLUS#2(z1, mult#2(z0, z1)), MULT#2(z0, z1)) PLUS#2(S(z0), z1) -> c10(PLUS#2(z0, z1)) MAIN(S(z0)) -> c(SUM#1(map#2(Cons(S(z0), unfoldr#2(S(z0)))))) MAIN(S(z0)) -> c(MAP#2(Cons(S(z0), unfoldr#2(S(z0))))) S tuples: SUM#1(Cons(z0, z1)) -> c1(PLUS#2(z0, sum#1(z1)), SUM#1(z1)) MULT#2(S(z0), z1) -> c8(PLUS#2(z1, mult#2(z0, z1)), MULT#2(z0, z1)) PLUS#2(S(z0), z1) -> c10(PLUS#2(z0, z1)) K tuples: MAIN(S(z0)) -> c(SUM#1(map#2(Cons(S(z0), unfoldr#2(S(z0)))))) MAIN(S(z0)) -> c(MAP#2(Cons(S(z0), unfoldr#2(S(z0))))) MAP#2(Cons(z0, z1)) -> c3(MULT#2(z0, z0)) UNFOLDR#2(S(z0)) -> c6(UNFOLDR#2(z0)) MAP#2(Cons(z0, z1)) -> c4(MAP#2(z1)) Defined Rule Symbols: sum#1_1, plus#2_2, mult#2_2, map#2_1, unfoldr#2_1 Defined Pair Symbols: SUM#1_1, MAP#2_1, UNFOLDR#2_1, MULT#2_2, PLUS#2_2, MAIN_1 Compound Symbols: c1_2, c3_1, c4_1, c6_1, c8_2, c10_1, c_1 ---------------------------------------- (77) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1))) Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S. SUM#1(Cons(z0, z1)) -> c1(PLUS#2(z0, sum#1(z1)), SUM#1(z1)) We considered the (Usable) Rules: map#2(Nil) -> Nil map#2(Cons(z0, z1)) -> Cons(mult#2(z0, z0), map#2(z1)) unfoldr#2(0) -> Nil unfoldr#2(S(z0)) -> Cons(z0, unfoldr#2(z0)) And the Tuples: SUM#1(Cons(z0, z1)) -> c1(PLUS#2(z0, sum#1(z1)), SUM#1(z1)) MAP#2(Cons(z0, z1)) -> c3(MULT#2(z0, z0)) MAP#2(Cons(z0, z1)) -> c4(MAP#2(z1)) UNFOLDR#2(S(z0)) -> c6(UNFOLDR#2(z0)) MULT#2(S(z0), z1) -> c8(PLUS#2(z1, mult#2(z0, z1)), MULT#2(z0, z1)) PLUS#2(S(z0), z1) -> c10(PLUS#2(z0, z1)) MAIN(S(z0)) -> c(SUM#1(map#2(Cons(S(z0), unfoldr#2(S(z0)))))) MAIN(S(z0)) -> c(MAP#2(Cons(S(z0), unfoldr#2(S(z0))))) The order we found is given by the following interpretation: Polynomial interpretation : POL(0) = [1] POL(Cons(x_1, x_2)) = [1] + x_2 POL(MAIN(x_1)) = [1] + x_1 POL(MAP#2(x_1)) = [1] POL(MULT#2(x_1, x_2)) = [1] POL(Nil) = [1] POL(PLUS#2(x_1, x_2)) = 0 POL(S(x_1)) = [1] + x_1 POL(SUM#1(x_1)) = x_1 POL(UNFOLDR#2(x_1)) = x_1 POL(c(x_1)) = x_1 POL(c1(x_1, x_2)) = x_1 + x_2 POL(c10(x_1)) = x_1 POL(c3(x_1)) = x_1 POL(c4(x_1)) = x_1 POL(c6(x_1)) = x_1 POL(c8(x_1, x_2)) = x_1 + x_2 POL(map#2(x_1)) = x_1 POL(mult#2(x_1, x_2)) = [1] + x_1 + x_2 POL(plus#2(x_1, x_2)) = [1] + x_1 + x_2 POL(sum#1(x_1)) = [1] + x_1 POL(unfoldr#2(x_1)) = x_1 ---------------------------------------- (78) Obligation: Complexity Dependency Tuples Problem Rules: sum#1(Nil) -> 0 sum#1(Cons(z0, z1)) -> plus#2(z0, sum#1(z1)) plus#2(0, z0) -> z0 plus#2(S(z0), z1) -> S(plus#2(z0, z1)) mult#2(0, z0) -> 0 mult#2(S(z0), z1) -> plus#2(z1, mult#2(z0, z1)) map#2(Cons(z0, z1)) -> Cons(mult#2(z0, z0), map#2(z1)) map#2(Nil) -> Nil unfoldr#2(S(z0)) -> Cons(z0, unfoldr#2(z0)) unfoldr#2(0) -> Nil Tuples: SUM#1(Cons(z0, z1)) -> c1(PLUS#2(z0, sum#1(z1)), SUM#1(z1)) MAP#2(Cons(z0, z1)) -> c3(MULT#2(z0, z0)) MAP#2(Cons(z0, z1)) -> c4(MAP#2(z1)) UNFOLDR#2(S(z0)) -> c6(UNFOLDR#2(z0)) MULT#2(S(z0), z1) -> c8(PLUS#2(z1, mult#2(z0, z1)), MULT#2(z0, z1)) PLUS#2(S(z0), z1) -> c10(PLUS#2(z0, z1)) MAIN(S(z0)) -> c(SUM#1(map#2(Cons(S(z0), unfoldr#2(S(z0)))))) MAIN(S(z0)) -> c(MAP#2(Cons(S(z0), unfoldr#2(S(z0))))) S tuples: MULT#2(S(z0), z1) -> c8(PLUS#2(z1, mult#2(z0, z1)), MULT#2(z0, z1)) PLUS#2(S(z0), z1) -> c10(PLUS#2(z0, z1)) K tuples: MAIN(S(z0)) -> c(SUM#1(map#2(Cons(S(z0), unfoldr#2(S(z0)))))) MAIN(S(z0)) -> c(MAP#2(Cons(S(z0), unfoldr#2(S(z0))))) MAP#2(Cons(z0, z1)) -> c3(MULT#2(z0, z0)) UNFOLDR#2(S(z0)) -> c6(UNFOLDR#2(z0)) MAP#2(Cons(z0, z1)) -> c4(MAP#2(z1)) SUM#1(Cons(z0, z1)) -> c1(PLUS#2(z0, sum#1(z1)), SUM#1(z1)) Defined Rule Symbols: sum#1_1, plus#2_2, mult#2_2, map#2_1, unfoldr#2_1 Defined Pair Symbols: SUM#1_1, MAP#2_1, UNFOLDR#2_1, MULT#2_2, PLUS#2_2, MAIN_1 Compound Symbols: c1_2, c3_1, c4_1, c6_1, c8_2, c10_1, c_1 ---------------------------------------- (79) CdtRuleRemovalProof (UPPER BOUND(ADD(n^2))) Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S. MULT#2(S(z0), z1) -> c8(PLUS#2(z1, mult#2(z0, z1)), MULT#2(z0, z1)) We considered the (Usable) Rules: unfoldr#2(0) -> Nil unfoldr#2(S(z0)) -> Cons(z0, unfoldr#2(z0)) And the Tuples: SUM#1(Cons(z0, z1)) -> c1(PLUS#2(z0, sum#1(z1)), SUM#1(z1)) MAP#2(Cons(z0, z1)) -> c3(MULT#2(z0, z0)) MAP#2(Cons(z0, z1)) -> c4(MAP#2(z1)) UNFOLDR#2(S(z0)) -> c6(UNFOLDR#2(z0)) MULT#2(S(z0), z1) -> c8(PLUS#2(z1, mult#2(z0, z1)), MULT#2(z0, z1)) PLUS#2(S(z0), z1) -> c10(PLUS#2(z0, z1)) MAIN(S(z0)) -> c(SUM#1(map#2(Cons(S(z0), unfoldr#2(S(z0)))))) MAIN(S(z0)) -> c(MAP#2(Cons(S(z0), unfoldr#2(S(z0))))) The order we found is given by the following interpretation: Polynomial interpretation : POL(0) = 0 POL(Cons(x_1, x_2)) = [2] + x_1 + x_2 POL(MAIN(x_1)) = [2]x_1 + [2]x_1^2 POL(MAP#2(x_1)) = x_1 POL(MULT#2(x_1, x_2)) = [2] + x_1 POL(Nil) = 0 POL(PLUS#2(x_1, x_2)) = 0 POL(S(x_1)) = [2] + x_1 POL(SUM#1(x_1)) = 0 POL(UNFOLDR#2(x_1)) = [2]x_1 + x_1^2 POL(c(x_1)) = x_1 POL(c1(x_1, x_2)) = x_1 + x_2 POL(c10(x_1)) = x_1 POL(c3(x_1)) = x_1 POL(c4(x_1)) = x_1 POL(c6(x_1)) = x_1 POL(c8(x_1, x_2)) = x_1 + x_2 POL(map#2(x_1)) = [2] + [2]x_1^2 POL(mult#2(x_1, x_2)) = 0 POL(plus#2(x_1, x_2)) = 0 POL(sum#1(x_1)) = 0 POL(unfoldr#2(x_1)) = [2]x_1^2 ---------------------------------------- (80) Obligation: Complexity Dependency Tuples Problem Rules: sum#1(Nil) -> 0 sum#1(Cons(z0, z1)) -> plus#2(z0, sum#1(z1)) plus#2(0, z0) -> z0 plus#2(S(z0), z1) -> S(plus#2(z0, z1)) mult#2(0, z0) -> 0 mult#2(S(z0), z1) -> plus#2(z1, mult#2(z0, z1)) map#2(Cons(z0, z1)) -> Cons(mult#2(z0, z0), map#2(z1)) map#2(Nil) -> Nil unfoldr#2(S(z0)) -> Cons(z0, unfoldr#2(z0)) unfoldr#2(0) -> Nil Tuples: SUM#1(Cons(z0, z1)) -> c1(PLUS#2(z0, sum#1(z1)), SUM#1(z1)) MAP#2(Cons(z0, z1)) -> c3(MULT#2(z0, z0)) MAP#2(Cons(z0, z1)) -> c4(MAP#2(z1)) UNFOLDR#2(S(z0)) -> c6(UNFOLDR#2(z0)) MULT#2(S(z0), z1) -> c8(PLUS#2(z1, mult#2(z0, z1)), MULT#2(z0, z1)) PLUS#2(S(z0), z1) -> c10(PLUS#2(z0, z1)) MAIN(S(z0)) -> c(SUM#1(map#2(Cons(S(z0), unfoldr#2(S(z0)))))) MAIN(S(z0)) -> c(MAP#2(Cons(S(z0), unfoldr#2(S(z0))))) S tuples: PLUS#2(S(z0), z1) -> c10(PLUS#2(z0, z1)) K tuples: MAIN(S(z0)) -> c(SUM#1(map#2(Cons(S(z0), unfoldr#2(S(z0)))))) MAIN(S(z0)) -> c(MAP#2(Cons(S(z0), unfoldr#2(S(z0))))) MAP#2(Cons(z0, z1)) -> c3(MULT#2(z0, z0)) UNFOLDR#2(S(z0)) -> c6(UNFOLDR#2(z0)) MAP#2(Cons(z0, z1)) -> c4(MAP#2(z1)) SUM#1(Cons(z0, z1)) -> c1(PLUS#2(z0, sum#1(z1)), SUM#1(z1)) MULT#2(S(z0), z1) -> c8(PLUS#2(z1, mult#2(z0, z1)), MULT#2(z0, z1)) Defined Rule Symbols: sum#1_1, plus#2_2, mult#2_2, map#2_1, unfoldr#2_1 Defined Pair Symbols: SUM#1_1, MAP#2_1, UNFOLDR#2_1, MULT#2_2, PLUS#2_2, MAIN_1 Compound Symbols: c1_2, c3_1, c4_1, c6_1, c8_2, c10_1, c_1 ---------------------------------------- (81) CdtNarrowingProof (BOTH BOUNDS(ID, ID)) Use narrowing to replace MAIN(S(z0)) -> c(SUM#1(map#2(Cons(S(z0), unfoldr#2(S(z0)))))) by MAIN(S(x0)) -> c(SUM#1(Cons(mult#2(S(x0), S(x0)), map#2(unfoldr#2(S(x0)))))) MAIN(S(z0)) -> c(SUM#1(map#2(Cons(S(z0), Cons(z0, unfoldr#2(z0)))))) ---------------------------------------- (82) Obligation: Complexity Dependency Tuples Problem Rules: sum#1(Nil) -> 0 sum#1(Cons(z0, z1)) -> plus#2(z0, sum#1(z1)) plus#2(0, z0) -> z0 plus#2(S(z0), z1) -> S(plus#2(z0, z1)) mult#2(0, z0) -> 0 mult#2(S(z0), z1) -> plus#2(z1, mult#2(z0, z1)) map#2(Cons(z0, z1)) -> Cons(mult#2(z0, z0), map#2(z1)) map#2(Nil) -> Nil unfoldr#2(S(z0)) -> Cons(z0, unfoldr#2(z0)) unfoldr#2(0) -> Nil Tuples: SUM#1(Cons(z0, z1)) -> c1(PLUS#2(z0, sum#1(z1)), SUM#1(z1)) MAP#2(Cons(z0, z1)) -> c3(MULT#2(z0, z0)) MAP#2(Cons(z0, z1)) -> c4(MAP#2(z1)) UNFOLDR#2(S(z0)) -> c6(UNFOLDR#2(z0)) MULT#2(S(z0), z1) -> c8(PLUS#2(z1, mult#2(z0, z1)), MULT#2(z0, z1)) PLUS#2(S(z0), z1) -> c10(PLUS#2(z0, z1)) MAIN(S(z0)) -> c(MAP#2(Cons(S(z0), unfoldr#2(S(z0))))) MAIN(S(x0)) -> c(SUM#1(Cons(mult#2(S(x0), S(x0)), map#2(unfoldr#2(S(x0)))))) MAIN(S(z0)) -> c(SUM#1(map#2(Cons(S(z0), Cons(z0, unfoldr#2(z0)))))) S tuples: PLUS#2(S(z0), z1) -> c10(PLUS#2(z0, z1)) K tuples: MAIN(S(z0)) -> c(SUM#1(map#2(Cons(S(z0), unfoldr#2(S(z0)))))) MAIN(S(z0)) -> c(MAP#2(Cons(S(z0), unfoldr#2(S(z0))))) MAP#2(Cons(z0, z1)) -> c3(MULT#2(z0, z0)) UNFOLDR#2(S(z0)) -> c6(UNFOLDR#2(z0)) MAP#2(Cons(z0, z1)) -> c4(MAP#2(z1)) SUM#1(Cons(z0, z1)) -> c1(PLUS#2(z0, sum#1(z1)), SUM#1(z1)) MULT#2(S(z0), z1) -> c8(PLUS#2(z1, mult#2(z0, z1)), MULT#2(z0, z1)) Defined Rule Symbols: sum#1_1, plus#2_2, mult#2_2, map#2_1, unfoldr#2_1 Defined Pair Symbols: SUM#1_1, MAP#2_1, UNFOLDR#2_1, MULT#2_2, PLUS#2_2, MAIN_1 Compound Symbols: c1_2, c3_1, c4_1, c6_1, c8_2, c10_1, c_1 ---------------------------------------- (83) CdtNarrowingProof (BOTH BOUNDS(ID, ID)) Use narrowing to replace MAIN(S(z0)) -> c(MAP#2(Cons(S(z0), unfoldr#2(S(z0))))) by MAIN(S(z0)) -> c(MAP#2(Cons(S(z0), Cons(z0, unfoldr#2(z0))))) ---------------------------------------- (84) Obligation: Complexity Dependency Tuples Problem Rules: sum#1(Nil) -> 0 sum#1(Cons(z0, z1)) -> plus#2(z0, sum#1(z1)) plus#2(0, z0) -> z0 plus#2(S(z0), z1) -> S(plus#2(z0, z1)) mult#2(0, z0) -> 0 mult#2(S(z0), z1) -> plus#2(z1, mult#2(z0, z1)) map#2(Cons(z0, z1)) -> Cons(mult#2(z0, z0), map#2(z1)) map#2(Nil) -> Nil unfoldr#2(S(z0)) -> Cons(z0, unfoldr#2(z0)) unfoldr#2(0) -> Nil Tuples: SUM#1(Cons(z0, z1)) -> c1(PLUS#2(z0, sum#1(z1)), SUM#1(z1)) MAP#2(Cons(z0, z1)) -> c3(MULT#2(z0, z0)) MAP#2(Cons(z0, z1)) -> c4(MAP#2(z1)) UNFOLDR#2(S(z0)) -> c6(UNFOLDR#2(z0)) MULT#2(S(z0), z1) -> c8(PLUS#2(z1, mult#2(z0, z1)), MULT#2(z0, z1)) PLUS#2(S(z0), z1) -> c10(PLUS#2(z0, z1)) MAIN(S(x0)) -> c(SUM#1(Cons(mult#2(S(x0), S(x0)), map#2(unfoldr#2(S(x0)))))) MAIN(S(z0)) -> c(SUM#1(map#2(Cons(S(z0), Cons(z0, unfoldr#2(z0)))))) MAIN(S(z0)) -> c(MAP#2(Cons(S(z0), Cons(z0, unfoldr#2(z0))))) S tuples: PLUS#2(S(z0), z1) -> c10(PLUS#2(z0, z1)) K tuples: MAIN(S(z0)) -> c(SUM#1(map#2(Cons(S(z0), unfoldr#2(S(z0)))))) MAIN(S(z0)) -> c(MAP#2(Cons(S(z0), unfoldr#2(S(z0))))) MAP#2(Cons(z0, z1)) -> c3(MULT#2(z0, z0)) UNFOLDR#2(S(z0)) -> c6(UNFOLDR#2(z0)) MAP#2(Cons(z0, z1)) -> c4(MAP#2(z1)) SUM#1(Cons(z0, z1)) -> c1(PLUS#2(z0, sum#1(z1)), SUM#1(z1)) MULT#2(S(z0), z1) -> c8(PLUS#2(z1, mult#2(z0, z1)), MULT#2(z0, z1)) Defined Rule Symbols: sum#1_1, plus#2_2, mult#2_2, map#2_1, unfoldr#2_1 Defined Pair Symbols: SUM#1_1, MAP#2_1, UNFOLDR#2_1, MULT#2_2, PLUS#2_2, MAIN_1 Compound Symbols: c1_2, c3_1, c4_1, c6_1, c8_2, c10_1, c_1 ---------------------------------------- (85) CdtNarrowingProof (BOTH BOUNDS(ID, ID)) Use narrowing to replace MAIN(S(x0)) -> c(SUM#1(Cons(mult#2(S(x0), S(x0)), map#2(unfoldr#2(S(x0)))))) by MAIN(S(z0)) -> c(SUM#1(Cons(mult#2(S(z0), S(z0)), map#2(Cons(z0, unfoldr#2(z0)))))) MAIN(S(z0)) -> c(SUM#1(Cons(plus#2(S(z0), mult#2(z0, S(z0))), map#2(unfoldr#2(S(z0)))))) ---------------------------------------- (86) Obligation: Complexity Dependency Tuples Problem Rules: sum#1(Nil) -> 0 sum#1(Cons(z0, z1)) -> plus#2(z0, sum#1(z1)) plus#2(0, z0) -> z0 plus#2(S(z0), z1) -> S(plus#2(z0, z1)) mult#2(0, z0) -> 0 mult#2(S(z0), z1) -> plus#2(z1, mult#2(z0, z1)) map#2(Cons(z0, z1)) -> Cons(mult#2(z0, z0), map#2(z1)) map#2(Nil) -> Nil unfoldr#2(S(z0)) -> Cons(z0, unfoldr#2(z0)) unfoldr#2(0) -> Nil Tuples: SUM#1(Cons(z0, z1)) -> c1(PLUS#2(z0, sum#1(z1)), SUM#1(z1)) MAP#2(Cons(z0, z1)) -> c3(MULT#2(z0, z0)) MAP#2(Cons(z0, z1)) -> c4(MAP#2(z1)) UNFOLDR#2(S(z0)) -> c6(UNFOLDR#2(z0)) MULT#2(S(z0), z1) -> c8(PLUS#2(z1, mult#2(z0, z1)), MULT#2(z0, z1)) PLUS#2(S(z0), z1) -> c10(PLUS#2(z0, z1)) MAIN(S(z0)) -> c(SUM#1(map#2(Cons(S(z0), Cons(z0, unfoldr#2(z0)))))) MAIN(S(z0)) -> c(MAP#2(Cons(S(z0), Cons(z0, unfoldr#2(z0))))) MAIN(S(z0)) -> c(SUM#1(Cons(mult#2(S(z0), S(z0)), map#2(Cons(z0, unfoldr#2(z0)))))) MAIN(S(z0)) -> c(SUM#1(Cons(plus#2(S(z0), mult#2(z0, S(z0))), map#2(unfoldr#2(S(z0)))))) S tuples: PLUS#2(S(z0), z1) -> c10(PLUS#2(z0, z1)) K tuples: MAIN(S(z0)) -> c(SUM#1(map#2(Cons(S(z0), unfoldr#2(S(z0)))))) MAIN(S(z0)) -> c(MAP#2(Cons(S(z0), unfoldr#2(S(z0))))) MAP#2(Cons(z0, z1)) -> c3(MULT#2(z0, z0)) UNFOLDR#2(S(z0)) -> c6(UNFOLDR#2(z0)) MAP#2(Cons(z0, z1)) -> c4(MAP#2(z1)) SUM#1(Cons(z0, z1)) -> c1(PLUS#2(z0, sum#1(z1)), SUM#1(z1)) MULT#2(S(z0), z1) -> c8(PLUS#2(z1, mult#2(z0, z1)), MULT#2(z0, z1)) Defined Rule Symbols: sum#1_1, plus#2_2, mult#2_2, map#2_1, unfoldr#2_1 Defined Pair Symbols: SUM#1_1, MAP#2_1, UNFOLDR#2_1, MULT#2_2, PLUS#2_2, MAIN_1 Compound Symbols: c1_2, c3_1, c4_1, c6_1, c8_2, c10_1, c_1 ---------------------------------------- (87) CdtNarrowingProof (BOTH BOUNDS(ID, ID)) Use narrowing to replace MAIN(S(z0)) -> c(SUM#1(map#2(Cons(S(z0), Cons(z0, unfoldr#2(z0)))))) by MAIN(S(x0)) -> c(SUM#1(Cons(mult#2(S(x0), S(x0)), map#2(Cons(x0, unfoldr#2(x0)))))) MAIN(S(S(z0))) -> c(SUM#1(map#2(Cons(S(S(z0)), Cons(S(z0), Cons(z0, unfoldr#2(z0))))))) MAIN(S(0)) -> c(SUM#1(map#2(Cons(S(0), Cons(0, Nil))))) ---------------------------------------- (88) Obligation: Complexity Dependency Tuples Problem Rules: sum#1(Nil) -> 0 sum#1(Cons(z0, z1)) -> plus#2(z0, sum#1(z1)) plus#2(0, z0) -> z0 plus#2(S(z0), z1) -> S(plus#2(z0, z1)) mult#2(0, z0) -> 0 mult#2(S(z0), z1) -> plus#2(z1, mult#2(z0, z1)) map#2(Cons(z0, z1)) -> Cons(mult#2(z0, z0), map#2(z1)) map#2(Nil) -> Nil unfoldr#2(S(z0)) -> Cons(z0, unfoldr#2(z0)) unfoldr#2(0) -> Nil Tuples: SUM#1(Cons(z0, z1)) -> c1(PLUS#2(z0, sum#1(z1)), SUM#1(z1)) MAP#2(Cons(z0, z1)) -> c3(MULT#2(z0, z0)) MAP#2(Cons(z0, z1)) -> c4(MAP#2(z1)) UNFOLDR#2(S(z0)) -> c6(UNFOLDR#2(z0)) MULT#2(S(z0), z1) -> c8(PLUS#2(z1, mult#2(z0, z1)), MULT#2(z0, z1)) PLUS#2(S(z0), z1) -> c10(PLUS#2(z0, z1)) MAIN(S(z0)) -> c(MAP#2(Cons(S(z0), Cons(z0, unfoldr#2(z0))))) MAIN(S(z0)) -> c(SUM#1(Cons(mult#2(S(z0), S(z0)), map#2(Cons(z0, unfoldr#2(z0)))))) MAIN(S(z0)) -> c(SUM#1(Cons(plus#2(S(z0), mult#2(z0, S(z0))), map#2(unfoldr#2(S(z0)))))) MAIN(S(S(z0))) -> c(SUM#1(map#2(Cons(S(S(z0)), Cons(S(z0), Cons(z0, unfoldr#2(z0))))))) MAIN(S(0)) -> c(SUM#1(map#2(Cons(S(0), Cons(0, Nil))))) S tuples: PLUS#2(S(z0), z1) -> c10(PLUS#2(z0, z1)) K tuples: MAIN(S(z0)) -> c(SUM#1(map#2(Cons(S(z0), unfoldr#2(S(z0)))))) MAIN(S(z0)) -> c(MAP#2(Cons(S(z0), unfoldr#2(S(z0))))) MAP#2(Cons(z0, z1)) -> c3(MULT#2(z0, z0)) UNFOLDR#2(S(z0)) -> c6(UNFOLDR#2(z0)) MAP#2(Cons(z0, z1)) -> c4(MAP#2(z1)) SUM#1(Cons(z0, z1)) -> c1(PLUS#2(z0, sum#1(z1)), SUM#1(z1)) MULT#2(S(z0), z1) -> c8(PLUS#2(z1, mult#2(z0, z1)), MULT#2(z0, z1)) Defined Rule Symbols: sum#1_1, plus#2_2, mult#2_2, map#2_1, unfoldr#2_1 Defined Pair Symbols: SUM#1_1, MAP#2_1, UNFOLDR#2_1, MULT#2_2, PLUS#2_2, MAIN_1 Compound Symbols: c1_2, c3_1, c4_1, c6_1, c8_2, c10_1, c_1 ---------------------------------------- (89) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID)) Use forward instantiation to replace MAP#2(Cons(z0, z1)) -> c3(MULT#2(z0, z0)) by MAP#2(Cons(S(y0), z1)) -> c3(MULT#2(S(y0), S(y0))) ---------------------------------------- (90) Obligation: Complexity Dependency Tuples Problem Rules: sum#1(Nil) -> 0 sum#1(Cons(z0, z1)) -> plus#2(z0, sum#1(z1)) plus#2(0, z0) -> z0 plus#2(S(z0), z1) -> S(plus#2(z0, z1)) mult#2(0, z0) -> 0 mult#2(S(z0), z1) -> plus#2(z1, mult#2(z0, z1)) map#2(Cons(z0, z1)) -> Cons(mult#2(z0, z0), map#2(z1)) map#2(Nil) -> Nil unfoldr#2(S(z0)) -> Cons(z0, unfoldr#2(z0)) unfoldr#2(0) -> Nil Tuples: SUM#1(Cons(z0, z1)) -> c1(PLUS#2(z0, sum#1(z1)), SUM#1(z1)) MAP#2(Cons(z0, z1)) -> c4(MAP#2(z1)) UNFOLDR#2(S(z0)) -> c6(UNFOLDR#2(z0)) MULT#2(S(z0), z1) -> c8(PLUS#2(z1, mult#2(z0, z1)), MULT#2(z0, z1)) PLUS#2(S(z0), z1) -> c10(PLUS#2(z0, z1)) MAIN(S(z0)) -> c(MAP#2(Cons(S(z0), Cons(z0, unfoldr#2(z0))))) MAIN(S(z0)) -> c(SUM#1(Cons(mult#2(S(z0), S(z0)), map#2(Cons(z0, unfoldr#2(z0)))))) MAIN(S(z0)) -> c(SUM#1(Cons(plus#2(S(z0), mult#2(z0, S(z0))), map#2(unfoldr#2(S(z0)))))) MAIN(S(S(z0))) -> c(SUM#1(map#2(Cons(S(S(z0)), Cons(S(z0), Cons(z0, unfoldr#2(z0))))))) MAIN(S(0)) -> c(SUM#1(map#2(Cons(S(0), Cons(0, Nil))))) MAP#2(Cons(S(y0), z1)) -> c3(MULT#2(S(y0), S(y0))) S tuples: PLUS#2(S(z0), z1) -> c10(PLUS#2(z0, z1)) K tuples: MAIN(S(z0)) -> c(SUM#1(map#2(Cons(S(z0), unfoldr#2(S(z0)))))) MAIN(S(z0)) -> c(MAP#2(Cons(S(z0), unfoldr#2(S(z0))))) UNFOLDR#2(S(z0)) -> c6(UNFOLDR#2(z0)) MAP#2(Cons(z0, z1)) -> c4(MAP#2(z1)) SUM#1(Cons(z0, z1)) -> c1(PLUS#2(z0, sum#1(z1)), SUM#1(z1)) MULT#2(S(z0), z1) -> c8(PLUS#2(z1, mult#2(z0, z1)), MULT#2(z0, z1)) MAP#2(Cons(S(y0), z1)) -> c3(MULT#2(S(y0), S(y0))) Defined Rule Symbols: sum#1_1, plus#2_2, mult#2_2, map#2_1, unfoldr#2_1 Defined Pair Symbols: SUM#1_1, MAP#2_1, UNFOLDR#2_1, MULT#2_2, PLUS#2_2, MAIN_1 Compound Symbols: c1_2, c4_1, c6_1, c8_2, c10_1, c_1, c3_1 ---------------------------------------- (91) CdtRewritingProof (BOTH BOUNDS(ID, ID)) Used rewriting to replace MAIN(S(z0)) -> c(SUM#1(Cons(mult#2(S(z0), S(z0)), map#2(Cons(z0, unfoldr#2(z0)))))) by MAIN(S(z0)) -> c(SUM#1(Cons(mult#2(S(z0), S(z0)), Cons(mult#2(z0, z0), map#2(unfoldr#2(z0)))))) ---------------------------------------- (92) Obligation: Complexity Dependency Tuples Problem Rules: sum#1(Nil) -> 0 sum#1(Cons(z0, z1)) -> plus#2(z0, sum#1(z1)) plus#2(0, z0) -> z0 plus#2(S(z0), z1) -> S(plus#2(z0, z1)) mult#2(0, z0) -> 0 mult#2(S(z0), z1) -> plus#2(z1, mult#2(z0, z1)) map#2(Cons(z0, z1)) -> Cons(mult#2(z0, z0), map#2(z1)) map#2(Nil) -> Nil unfoldr#2(S(z0)) -> Cons(z0, unfoldr#2(z0)) unfoldr#2(0) -> Nil Tuples: SUM#1(Cons(z0, z1)) -> c1(PLUS#2(z0, sum#1(z1)), SUM#1(z1)) MAP#2(Cons(z0, z1)) -> c4(MAP#2(z1)) UNFOLDR#2(S(z0)) -> c6(UNFOLDR#2(z0)) MULT#2(S(z0), z1) -> c8(PLUS#2(z1, mult#2(z0, z1)), MULT#2(z0, z1)) PLUS#2(S(z0), z1) -> c10(PLUS#2(z0, z1)) MAIN(S(z0)) -> c(MAP#2(Cons(S(z0), Cons(z0, unfoldr#2(z0))))) MAIN(S(z0)) -> c(SUM#1(Cons(mult#2(S(z0), S(z0)), map#2(Cons(z0, unfoldr#2(z0)))))) MAIN(S(z0)) -> c(SUM#1(Cons(plus#2(S(z0), mult#2(z0, S(z0))), map#2(unfoldr#2(S(z0)))))) MAIN(S(S(z0))) -> c(SUM#1(map#2(Cons(S(S(z0)), Cons(S(z0), Cons(z0, unfoldr#2(z0))))))) MAIN(S(0)) -> c(SUM#1(map#2(Cons(S(0), Cons(0, Nil))))) MAP#2(Cons(S(y0), z1)) -> c3(MULT#2(S(y0), S(y0))) MAIN(S(z0)) -> c(SUM#1(Cons(mult#2(S(z0), S(z0)), Cons(mult#2(z0, z0), map#2(unfoldr#2(z0)))))) S tuples: PLUS#2(S(z0), z1) -> c10(PLUS#2(z0, z1)) K tuples: MAIN(S(z0)) -> c(SUM#1(map#2(Cons(S(z0), unfoldr#2(S(z0)))))) MAIN(S(z0)) -> c(MAP#2(Cons(S(z0), unfoldr#2(S(z0))))) UNFOLDR#2(S(z0)) -> c6(UNFOLDR#2(z0)) MAP#2(Cons(z0, z1)) -> c4(MAP#2(z1)) SUM#1(Cons(z0, z1)) -> c1(PLUS#2(z0, sum#1(z1)), SUM#1(z1)) MULT#2(S(z0), z1) -> c8(PLUS#2(z1, mult#2(z0, z1)), MULT#2(z0, z1)) MAP#2(Cons(S(y0), z1)) -> c3(MULT#2(S(y0), S(y0))) Defined Rule Symbols: sum#1_1, plus#2_2, mult#2_2, map#2_1, unfoldr#2_1 Defined Pair Symbols: SUM#1_1, MAP#2_1, UNFOLDR#2_1, MULT#2_2, PLUS#2_2, MAIN_1 Compound Symbols: c1_2, c4_1, c6_1, c8_2, c10_1, c_1, c3_1 ---------------------------------------- (93) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID)) Use forward instantiation to replace MAP#2(Cons(z0, z1)) -> c4(MAP#2(z1)) by MAP#2(Cons(z0, Cons(y0, y1))) -> c4(MAP#2(Cons(y0, y1))) MAP#2(Cons(z0, Cons(S(y0), y1))) -> c4(MAP#2(Cons(S(y0), y1))) ---------------------------------------- (94) Obligation: Complexity Dependency Tuples Problem Rules: sum#1(Nil) -> 0 sum#1(Cons(z0, z1)) -> plus#2(z0, sum#1(z1)) plus#2(0, z0) -> z0 plus#2(S(z0), z1) -> S(plus#2(z0, z1)) mult#2(0, z0) -> 0 mult#2(S(z0), z1) -> plus#2(z1, mult#2(z0, z1)) map#2(Cons(z0, z1)) -> Cons(mult#2(z0, z0), map#2(z1)) map#2(Nil) -> Nil unfoldr#2(S(z0)) -> Cons(z0, unfoldr#2(z0)) unfoldr#2(0) -> Nil Tuples: SUM#1(Cons(z0, z1)) -> c1(PLUS#2(z0, sum#1(z1)), SUM#1(z1)) UNFOLDR#2(S(z0)) -> c6(UNFOLDR#2(z0)) MULT#2(S(z0), z1) -> c8(PLUS#2(z1, mult#2(z0, z1)), MULT#2(z0, z1)) PLUS#2(S(z0), z1) -> c10(PLUS#2(z0, z1)) MAIN(S(z0)) -> c(MAP#2(Cons(S(z0), Cons(z0, unfoldr#2(z0))))) MAIN(S(z0)) -> c(SUM#1(Cons(mult#2(S(z0), S(z0)), map#2(Cons(z0, unfoldr#2(z0)))))) MAIN(S(z0)) -> c(SUM#1(Cons(plus#2(S(z0), mult#2(z0, S(z0))), map#2(unfoldr#2(S(z0)))))) MAIN(S(S(z0))) -> c(SUM#1(map#2(Cons(S(S(z0)), Cons(S(z0), Cons(z0, unfoldr#2(z0))))))) MAIN(S(0)) -> c(SUM#1(map#2(Cons(S(0), Cons(0, Nil))))) MAP#2(Cons(S(y0), z1)) -> c3(MULT#2(S(y0), S(y0))) MAIN(S(z0)) -> c(SUM#1(Cons(mult#2(S(z0), S(z0)), Cons(mult#2(z0, z0), map#2(unfoldr#2(z0)))))) MAP#2(Cons(z0, Cons(y0, y1))) -> c4(MAP#2(Cons(y0, y1))) MAP#2(Cons(z0, Cons(S(y0), y1))) -> c4(MAP#2(Cons(S(y0), y1))) S tuples: PLUS#2(S(z0), z1) -> c10(PLUS#2(z0, z1)) K tuples: MAIN(S(z0)) -> c(SUM#1(map#2(Cons(S(z0), unfoldr#2(S(z0)))))) MAIN(S(z0)) -> c(MAP#2(Cons(S(z0), unfoldr#2(S(z0))))) UNFOLDR#2(S(z0)) -> c6(UNFOLDR#2(z0)) SUM#1(Cons(z0, z1)) -> c1(PLUS#2(z0, sum#1(z1)), SUM#1(z1)) MULT#2(S(z0), z1) -> c8(PLUS#2(z1, mult#2(z0, z1)), MULT#2(z0, z1)) MAP#2(Cons(S(y0), z1)) -> c3(MULT#2(S(y0), S(y0))) MAP#2(Cons(z0, Cons(y0, y1))) -> c4(MAP#2(Cons(y0, y1))) MAP#2(Cons(z0, Cons(S(y0), y1))) -> c4(MAP#2(Cons(S(y0), y1))) Defined Rule Symbols: sum#1_1, plus#2_2, mult#2_2, map#2_1, unfoldr#2_1 Defined Pair Symbols: SUM#1_1, UNFOLDR#2_1, MULT#2_2, PLUS#2_2, MAIN_1, MAP#2_1 Compound Symbols: c1_2, c6_1, c8_2, c10_1, c_1, c3_1, c4_1 ---------------------------------------- (95) CdtRewritingProof (BOTH BOUNDS(ID, ID)) Used rewriting to replace MAIN(S(z0)) -> c(SUM#1(Cons(plus#2(S(z0), mult#2(z0, S(z0))), map#2(unfoldr#2(S(z0)))))) by MAIN(S(z0)) -> c(SUM#1(Cons(plus#2(S(z0), mult#2(z0, S(z0))), map#2(Cons(z0, unfoldr#2(z0)))))) ---------------------------------------- (96) Obligation: Complexity Dependency Tuples Problem Rules: sum#1(Nil) -> 0 sum#1(Cons(z0, z1)) -> plus#2(z0, sum#1(z1)) plus#2(0, z0) -> z0 plus#2(S(z0), z1) -> S(plus#2(z0, z1)) mult#2(0, z0) -> 0 mult#2(S(z0), z1) -> plus#2(z1, mult#2(z0, z1)) map#2(Cons(z0, z1)) -> Cons(mult#2(z0, z0), map#2(z1)) map#2(Nil) -> Nil unfoldr#2(S(z0)) -> Cons(z0, unfoldr#2(z0)) unfoldr#2(0) -> Nil Tuples: SUM#1(Cons(z0, z1)) -> c1(PLUS#2(z0, sum#1(z1)), SUM#1(z1)) UNFOLDR#2(S(z0)) -> c6(UNFOLDR#2(z0)) MULT#2(S(z0), z1) -> c8(PLUS#2(z1, mult#2(z0, z1)), MULT#2(z0, z1)) PLUS#2(S(z0), z1) -> c10(PLUS#2(z0, z1)) MAIN(S(z0)) -> c(MAP#2(Cons(S(z0), Cons(z0, unfoldr#2(z0))))) MAIN(S(z0)) -> c(SUM#1(Cons(mult#2(S(z0), S(z0)), map#2(Cons(z0, unfoldr#2(z0)))))) MAIN(S(S(z0))) -> c(SUM#1(map#2(Cons(S(S(z0)), Cons(S(z0), Cons(z0, unfoldr#2(z0))))))) MAIN(S(0)) -> c(SUM#1(map#2(Cons(S(0), Cons(0, Nil))))) MAP#2(Cons(S(y0), z1)) -> c3(MULT#2(S(y0), S(y0))) MAIN(S(z0)) -> c(SUM#1(Cons(mult#2(S(z0), S(z0)), Cons(mult#2(z0, z0), map#2(unfoldr#2(z0)))))) MAP#2(Cons(z0, Cons(y0, y1))) -> c4(MAP#2(Cons(y0, y1))) MAP#2(Cons(z0, Cons(S(y0), y1))) -> c4(MAP#2(Cons(S(y0), y1))) MAIN(S(z0)) -> c(SUM#1(Cons(plus#2(S(z0), mult#2(z0, S(z0))), map#2(Cons(z0, unfoldr#2(z0)))))) S tuples: PLUS#2(S(z0), z1) -> c10(PLUS#2(z0, z1)) K tuples: MAIN(S(z0)) -> c(SUM#1(map#2(Cons(S(z0), unfoldr#2(S(z0)))))) MAIN(S(z0)) -> c(MAP#2(Cons(S(z0), unfoldr#2(S(z0))))) UNFOLDR#2(S(z0)) -> c6(UNFOLDR#2(z0)) SUM#1(Cons(z0, z1)) -> c1(PLUS#2(z0, sum#1(z1)), SUM#1(z1)) MULT#2(S(z0), z1) -> c8(PLUS#2(z1, mult#2(z0, z1)), MULT#2(z0, z1)) MAP#2(Cons(S(y0), z1)) -> c3(MULT#2(S(y0), S(y0))) MAP#2(Cons(z0, Cons(y0, y1))) -> c4(MAP#2(Cons(y0, y1))) MAP#2(Cons(z0, Cons(S(y0), y1))) -> c4(MAP#2(Cons(S(y0), y1))) Defined Rule Symbols: sum#1_1, plus#2_2, mult#2_2, map#2_1, unfoldr#2_1 Defined Pair Symbols: SUM#1_1, UNFOLDR#2_1, MULT#2_2, PLUS#2_2, MAIN_1, MAP#2_1 Compound Symbols: c1_2, c6_1, c8_2, c10_1, c_1, c3_1, c4_1 ---------------------------------------- (97) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID)) Use forward instantiation to replace UNFOLDR#2(S(z0)) -> c6(UNFOLDR#2(z0)) by UNFOLDR#2(S(S(y0))) -> c6(UNFOLDR#2(S(y0))) ---------------------------------------- (98) Obligation: Complexity Dependency Tuples Problem Rules: sum#1(Nil) -> 0 sum#1(Cons(z0, z1)) -> plus#2(z0, sum#1(z1)) plus#2(0, z0) -> z0 plus#2(S(z0), z1) -> S(plus#2(z0, z1)) mult#2(0, z0) -> 0 mult#2(S(z0), z1) -> plus#2(z1, mult#2(z0, z1)) map#2(Cons(z0, z1)) -> Cons(mult#2(z0, z0), map#2(z1)) map#2(Nil) -> Nil unfoldr#2(S(z0)) -> Cons(z0, unfoldr#2(z0)) unfoldr#2(0) -> Nil Tuples: SUM#1(Cons(z0, z1)) -> c1(PLUS#2(z0, sum#1(z1)), SUM#1(z1)) MULT#2(S(z0), z1) -> c8(PLUS#2(z1, mult#2(z0, z1)), MULT#2(z0, z1)) PLUS#2(S(z0), z1) -> c10(PLUS#2(z0, z1)) MAIN(S(z0)) -> c(MAP#2(Cons(S(z0), Cons(z0, unfoldr#2(z0))))) MAIN(S(z0)) -> c(SUM#1(Cons(mult#2(S(z0), S(z0)), map#2(Cons(z0, unfoldr#2(z0)))))) MAIN(S(S(z0))) -> c(SUM#1(map#2(Cons(S(S(z0)), Cons(S(z0), Cons(z0, unfoldr#2(z0))))))) MAIN(S(0)) -> c(SUM#1(map#2(Cons(S(0), Cons(0, Nil))))) MAP#2(Cons(S(y0), z1)) -> c3(MULT#2(S(y0), S(y0))) MAIN(S(z0)) -> c(SUM#1(Cons(mult#2(S(z0), S(z0)), Cons(mult#2(z0, z0), map#2(unfoldr#2(z0)))))) MAP#2(Cons(z0, Cons(y0, y1))) -> c4(MAP#2(Cons(y0, y1))) MAP#2(Cons(z0, Cons(S(y0), y1))) -> c4(MAP#2(Cons(S(y0), y1))) MAIN(S(z0)) -> c(SUM#1(Cons(plus#2(S(z0), mult#2(z0, S(z0))), map#2(Cons(z0, unfoldr#2(z0)))))) UNFOLDR#2(S(S(y0))) -> c6(UNFOLDR#2(S(y0))) S tuples: PLUS#2(S(z0), z1) -> c10(PLUS#2(z0, z1)) K tuples: MAIN(S(z0)) -> c(SUM#1(map#2(Cons(S(z0), unfoldr#2(S(z0)))))) MAIN(S(z0)) -> c(MAP#2(Cons(S(z0), unfoldr#2(S(z0))))) SUM#1(Cons(z0, z1)) -> c1(PLUS#2(z0, sum#1(z1)), SUM#1(z1)) MULT#2(S(z0), z1) -> c8(PLUS#2(z1, mult#2(z0, z1)), MULT#2(z0, z1)) MAP#2(Cons(S(y0), z1)) -> c3(MULT#2(S(y0), S(y0))) MAP#2(Cons(z0, Cons(y0, y1))) -> c4(MAP#2(Cons(y0, y1))) MAP#2(Cons(z0, Cons(S(y0), y1))) -> c4(MAP#2(Cons(S(y0), y1))) UNFOLDR#2(S(S(y0))) -> c6(UNFOLDR#2(S(y0))) Defined Rule Symbols: sum#1_1, plus#2_2, mult#2_2, map#2_1, unfoldr#2_1 Defined Pair Symbols: SUM#1_1, MULT#2_2, PLUS#2_2, MAIN_1, MAP#2_1, UNFOLDR#2_1 Compound Symbols: c1_2, c8_2, c10_1, c_1, c3_1, c4_1, c6_1 ---------------------------------------- (99) CdtRewritingProof (BOTH BOUNDS(ID, ID)) Used rewriting to replace MAIN(S(x0)) -> c(SUM#1(Cons(mult#2(S(x0), S(x0)), map#2(Cons(x0, unfoldr#2(x0)))))) by MAIN(S(z0)) -> c(SUM#1(Cons(mult#2(S(z0), S(z0)), Cons(mult#2(z0, z0), map#2(unfoldr#2(z0)))))) ---------------------------------------- (100) Obligation: Complexity Dependency Tuples Problem Rules: sum#1(Nil) -> 0 sum#1(Cons(z0, z1)) -> plus#2(z0, sum#1(z1)) plus#2(0, z0) -> z0 plus#2(S(z0), z1) -> S(plus#2(z0, z1)) mult#2(0, z0) -> 0 mult#2(S(z0), z1) -> plus#2(z1, mult#2(z0, z1)) map#2(Cons(z0, z1)) -> Cons(mult#2(z0, z0), map#2(z1)) map#2(Nil) -> Nil unfoldr#2(S(z0)) -> Cons(z0, unfoldr#2(z0)) unfoldr#2(0) -> Nil Tuples: SUM#1(Cons(z0, z1)) -> c1(PLUS#2(z0, sum#1(z1)), SUM#1(z1)) MULT#2(S(z0), z1) -> c8(PLUS#2(z1, mult#2(z0, z1)), MULT#2(z0, z1)) PLUS#2(S(z0), z1) -> c10(PLUS#2(z0, z1)) MAIN(S(z0)) -> c(MAP#2(Cons(S(z0), Cons(z0, unfoldr#2(z0))))) MAIN(S(S(z0))) -> c(SUM#1(map#2(Cons(S(S(z0)), Cons(S(z0), Cons(z0, unfoldr#2(z0))))))) MAIN(S(0)) -> c(SUM#1(map#2(Cons(S(0), Cons(0, Nil))))) MAP#2(Cons(S(y0), z1)) -> c3(MULT#2(S(y0), S(y0))) MAIN(S(z0)) -> c(SUM#1(Cons(mult#2(S(z0), S(z0)), Cons(mult#2(z0, z0), map#2(unfoldr#2(z0)))))) MAP#2(Cons(z0, Cons(y0, y1))) -> c4(MAP#2(Cons(y0, y1))) MAP#2(Cons(z0, Cons(S(y0), y1))) -> c4(MAP#2(Cons(S(y0), y1))) MAIN(S(z0)) -> c(SUM#1(Cons(plus#2(S(z0), mult#2(z0, S(z0))), map#2(Cons(z0, unfoldr#2(z0)))))) UNFOLDR#2(S(S(y0))) -> c6(UNFOLDR#2(S(y0))) S tuples: PLUS#2(S(z0), z1) -> c10(PLUS#2(z0, z1)) K tuples: MAIN(S(z0)) -> c(SUM#1(map#2(Cons(S(z0), unfoldr#2(S(z0)))))) MAIN(S(z0)) -> c(MAP#2(Cons(S(z0), unfoldr#2(S(z0))))) SUM#1(Cons(z0, z1)) -> c1(PLUS#2(z0, sum#1(z1)), SUM#1(z1)) MULT#2(S(z0), z1) -> c8(PLUS#2(z1, mult#2(z0, z1)), MULT#2(z0, z1)) MAP#2(Cons(S(y0), z1)) -> c3(MULT#2(S(y0), S(y0))) MAP#2(Cons(z0, Cons(y0, y1))) -> c4(MAP#2(Cons(y0, y1))) MAP#2(Cons(z0, Cons(S(y0), y1))) -> c4(MAP#2(Cons(S(y0), y1))) UNFOLDR#2(S(S(y0))) -> c6(UNFOLDR#2(S(y0))) Defined Rule Symbols: sum#1_1, plus#2_2, mult#2_2, map#2_1, unfoldr#2_1 Defined Pair Symbols: SUM#1_1, MULT#2_2, PLUS#2_2, MAIN_1, MAP#2_1, UNFOLDR#2_1 Compound Symbols: c1_2, c8_2, c10_1, c_1, c3_1, c4_1, c6_1 ---------------------------------------- (101) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID)) Use forward instantiation to replace PLUS#2(S(z0), z1) -> c10(PLUS#2(z0, z1)) by PLUS#2(S(S(y0)), z1) -> c10(PLUS#2(S(y0), z1)) ---------------------------------------- (102) Obligation: Complexity Dependency Tuples Problem Rules: sum#1(Nil) -> 0 sum#1(Cons(z0, z1)) -> plus#2(z0, sum#1(z1)) plus#2(0, z0) -> z0 plus#2(S(z0), z1) -> S(plus#2(z0, z1)) mult#2(0, z0) -> 0 mult#2(S(z0), z1) -> plus#2(z1, mult#2(z0, z1)) map#2(Cons(z0, z1)) -> Cons(mult#2(z0, z0), map#2(z1)) map#2(Nil) -> Nil unfoldr#2(S(z0)) -> Cons(z0, unfoldr#2(z0)) unfoldr#2(0) -> Nil Tuples: SUM#1(Cons(z0, z1)) -> c1(PLUS#2(z0, sum#1(z1)), SUM#1(z1)) MULT#2(S(z0), z1) -> c8(PLUS#2(z1, mult#2(z0, z1)), MULT#2(z0, z1)) MAIN(S(z0)) -> c(MAP#2(Cons(S(z0), Cons(z0, unfoldr#2(z0))))) MAIN(S(S(z0))) -> c(SUM#1(map#2(Cons(S(S(z0)), Cons(S(z0), Cons(z0, unfoldr#2(z0))))))) MAIN(S(0)) -> c(SUM#1(map#2(Cons(S(0), Cons(0, Nil))))) MAP#2(Cons(S(y0), z1)) -> c3(MULT#2(S(y0), S(y0))) MAIN(S(z0)) -> c(SUM#1(Cons(mult#2(S(z0), S(z0)), Cons(mult#2(z0, z0), map#2(unfoldr#2(z0)))))) MAP#2(Cons(z0, Cons(y0, y1))) -> c4(MAP#2(Cons(y0, y1))) MAP#2(Cons(z0, Cons(S(y0), y1))) -> c4(MAP#2(Cons(S(y0), y1))) MAIN(S(z0)) -> c(SUM#1(Cons(plus#2(S(z0), mult#2(z0, S(z0))), map#2(Cons(z0, unfoldr#2(z0)))))) UNFOLDR#2(S(S(y0))) -> c6(UNFOLDR#2(S(y0))) PLUS#2(S(S(y0)), z1) -> c10(PLUS#2(S(y0), z1)) S tuples: PLUS#2(S(S(y0)), z1) -> c10(PLUS#2(S(y0), z1)) K tuples: MAIN(S(z0)) -> c(SUM#1(map#2(Cons(S(z0), unfoldr#2(S(z0)))))) MAIN(S(z0)) -> c(MAP#2(Cons(S(z0), unfoldr#2(S(z0))))) SUM#1(Cons(z0, z1)) -> c1(PLUS#2(z0, sum#1(z1)), SUM#1(z1)) MULT#2(S(z0), z1) -> c8(PLUS#2(z1, mult#2(z0, z1)), MULT#2(z0, z1)) MAP#2(Cons(S(y0), z1)) -> c3(MULT#2(S(y0), S(y0))) MAP#2(Cons(z0, Cons(y0, y1))) -> c4(MAP#2(Cons(y0, y1))) MAP#2(Cons(z0, Cons(S(y0), y1))) -> c4(MAP#2(Cons(S(y0), y1))) UNFOLDR#2(S(S(y0))) -> c6(UNFOLDR#2(S(y0))) Defined Rule Symbols: sum#1_1, plus#2_2, mult#2_2, map#2_1, unfoldr#2_1 Defined Pair Symbols: SUM#1_1, MULT#2_2, MAIN_1, MAP#2_1, UNFOLDR#2_1, PLUS#2_2 Compound Symbols: c1_2, c8_2, c_1, c3_1, c4_1, c6_1, c10_1 ---------------------------------------- (103) CdtRewritingProof (BOTH BOUNDS(ID, ID)) Used rewriting to replace MAIN(S(S(z0))) -> c(SUM#1(map#2(Cons(S(S(z0)), Cons(S(z0), Cons(z0, unfoldr#2(z0))))))) by MAIN(S(S(z0))) -> c(SUM#1(Cons(mult#2(S(S(z0)), S(S(z0))), map#2(Cons(S(z0), Cons(z0, unfoldr#2(z0))))))) ---------------------------------------- (104) Obligation: Complexity Dependency Tuples Problem Rules: sum#1(Nil) -> 0 sum#1(Cons(z0, z1)) -> plus#2(z0, sum#1(z1)) plus#2(0, z0) -> z0 plus#2(S(z0), z1) -> S(plus#2(z0, z1)) mult#2(0, z0) -> 0 mult#2(S(z0), z1) -> plus#2(z1, mult#2(z0, z1)) map#2(Cons(z0, z1)) -> Cons(mult#2(z0, z0), map#2(z1)) map#2(Nil) -> Nil unfoldr#2(S(z0)) -> Cons(z0, unfoldr#2(z0)) unfoldr#2(0) -> Nil Tuples: SUM#1(Cons(z0, z1)) -> c1(PLUS#2(z0, sum#1(z1)), SUM#1(z1)) MULT#2(S(z0), z1) -> c8(PLUS#2(z1, mult#2(z0, z1)), MULT#2(z0, z1)) MAIN(S(z0)) -> c(MAP#2(Cons(S(z0), Cons(z0, unfoldr#2(z0))))) MAIN(S(0)) -> c(SUM#1(map#2(Cons(S(0), Cons(0, Nil))))) MAP#2(Cons(S(y0), z1)) -> c3(MULT#2(S(y0), S(y0))) MAIN(S(z0)) -> c(SUM#1(Cons(mult#2(S(z0), S(z0)), Cons(mult#2(z0, z0), map#2(unfoldr#2(z0)))))) MAP#2(Cons(z0, Cons(y0, y1))) -> c4(MAP#2(Cons(y0, y1))) MAP#2(Cons(z0, Cons(S(y0), y1))) -> c4(MAP#2(Cons(S(y0), y1))) MAIN(S(z0)) -> c(SUM#1(Cons(plus#2(S(z0), mult#2(z0, S(z0))), map#2(Cons(z0, unfoldr#2(z0)))))) UNFOLDR#2(S(S(y0))) -> c6(UNFOLDR#2(S(y0))) PLUS#2(S(S(y0)), z1) -> c10(PLUS#2(S(y0), z1)) MAIN(S(S(z0))) -> c(SUM#1(Cons(mult#2(S(S(z0)), S(S(z0))), map#2(Cons(S(z0), Cons(z0, unfoldr#2(z0))))))) S tuples: PLUS#2(S(S(y0)), z1) -> c10(PLUS#2(S(y0), z1)) K tuples: MAIN(S(z0)) -> c(SUM#1(map#2(Cons(S(z0), unfoldr#2(S(z0)))))) MAIN(S(z0)) -> c(MAP#2(Cons(S(z0), unfoldr#2(S(z0))))) SUM#1(Cons(z0, z1)) -> c1(PLUS#2(z0, sum#1(z1)), SUM#1(z1)) MULT#2(S(z0), z1) -> c8(PLUS#2(z1, mult#2(z0, z1)), MULT#2(z0, z1)) MAP#2(Cons(S(y0), z1)) -> c3(MULT#2(S(y0), S(y0))) MAP#2(Cons(z0, Cons(y0, y1))) -> c4(MAP#2(Cons(y0, y1))) MAP#2(Cons(z0, Cons(S(y0), y1))) -> c4(MAP#2(Cons(S(y0), y1))) UNFOLDR#2(S(S(y0))) -> c6(UNFOLDR#2(S(y0))) Defined Rule Symbols: sum#1_1, plus#2_2, mult#2_2, map#2_1, unfoldr#2_1 Defined Pair Symbols: SUM#1_1, MULT#2_2, MAIN_1, MAP#2_1, UNFOLDR#2_1, PLUS#2_2 Compound Symbols: c1_2, c8_2, c_1, c3_1, c4_1, c6_1, c10_1 ---------------------------------------- (105) CdtRewritingProof (BOTH BOUNDS(ID, ID)) Used rewriting to replace MAIN(S(0)) -> c(SUM#1(map#2(Cons(S(0), Cons(0, Nil))))) by MAIN(S(0)) -> c(SUM#1(Cons(mult#2(S(0), S(0)), map#2(Cons(0, Nil))))) ---------------------------------------- (106) Obligation: Complexity Dependency Tuples Problem Rules: sum#1(Nil) -> 0 sum#1(Cons(z0, z1)) -> plus#2(z0, sum#1(z1)) plus#2(0, z0) -> z0 plus#2(S(z0), z1) -> S(plus#2(z0, z1)) mult#2(0, z0) -> 0 mult#2(S(z0), z1) -> plus#2(z1, mult#2(z0, z1)) map#2(Cons(z0, z1)) -> Cons(mult#2(z0, z0), map#2(z1)) map#2(Nil) -> Nil unfoldr#2(S(z0)) -> Cons(z0, unfoldr#2(z0)) unfoldr#2(0) -> Nil Tuples: SUM#1(Cons(z0, z1)) -> c1(PLUS#2(z0, sum#1(z1)), SUM#1(z1)) MULT#2(S(z0), z1) -> c8(PLUS#2(z1, mult#2(z0, z1)), MULT#2(z0, z1)) MAIN(S(z0)) -> c(MAP#2(Cons(S(z0), Cons(z0, unfoldr#2(z0))))) MAP#2(Cons(S(y0), z1)) -> c3(MULT#2(S(y0), S(y0))) MAIN(S(z0)) -> c(SUM#1(Cons(mult#2(S(z0), S(z0)), Cons(mult#2(z0, z0), map#2(unfoldr#2(z0)))))) MAP#2(Cons(z0, Cons(y0, y1))) -> c4(MAP#2(Cons(y0, y1))) MAP#2(Cons(z0, Cons(S(y0), y1))) -> c4(MAP#2(Cons(S(y0), y1))) MAIN(S(z0)) -> c(SUM#1(Cons(plus#2(S(z0), mult#2(z0, S(z0))), map#2(Cons(z0, unfoldr#2(z0)))))) UNFOLDR#2(S(S(y0))) -> c6(UNFOLDR#2(S(y0))) PLUS#2(S(S(y0)), z1) -> c10(PLUS#2(S(y0), z1)) MAIN(S(S(z0))) -> c(SUM#1(Cons(mult#2(S(S(z0)), S(S(z0))), map#2(Cons(S(z0), Cons(z0, unfoldr#2(z0))))))) MAIN(S(0)) -> c(SUM#1(Cons(mult#2(S(0), S(0)), map#2(Cons(0, Nil))))) S tuples: PLUS#2(S(S(y0)), z1) -> c10(PLUS#2(S(y0), z1)) K tuples: MAIN(S(z0)) -> c(SUM#1(map#2(Cons(S(z0), unfoldr#2(S(z0)))))) MAIN(S(z0)) -> c(MAP#2(Cons(S(z0), unfoldr#2(S(z0))))) SUM#1(Cons(z0, z1)) -> c1(PLUS#2(z0, sum#1(z1)), SUM#1(z1)) MULT#2(S(z0), z1) -> c8(PLUS#2(z1, mult#2(z0, z1)), MULT#2(z0, z1)) MAP#2(Cons(S(y0), z1)) -> c3(MULT#2(S(y0), S(y0))) MAP#2(Cons(z0, Cons(y0, y1))) -> c4(MAP#2(Cons(y0, y1))) MAP#2(Cons(z0, Cons(S(y0), y1))) -> c4(MAP#2(Cons(S(y0), y1))) UNFOLDR#2(S(S(y0))) -> c6(UNFOLDR#2(S(y0))) Defined Rule Symbols: sum#1_1, plus#2_2, mult#2_2, map#2_1, unfoldr#2_1 Defined Pair Symbols: SUM#1_1, MULT#2_2, MAIN_1, MAP#2_1, UNFOLDR#2_1, PLUS#2_2 Compound Symbols: c1_2, c8_2, c_1, c3_1, c4_1, c6_1, c10_1 ---------------------------------------- (107) CdtRewritingProof (BOTH BOUNDS(ID, ID)) Used rewriting to replace MAIN(S(z0)) -> c(SUM#1(Cons(mult#2(S(z0), S(z0)), Cons(mult#2(z0, z0), map#2(unfoldr#2(z0)))))) by MAIN(S(z0)) -> c(SUM#1(Cons(plus#2(S(z0), mult#2(z0, S(z0))), Cons(mult#2(z0, z0), map#2(unfoldr#2(z0)))))) ---------------------------------------- (108) Obligation: Complexity Dependency Tuples Problem Rules: sum#1(Nil) -> 0 sum#1(Cons(z0, z1)) -> plus#2(z0, sum#1(z1)) plus#2(0, z0) -> z0 plus#2(S(z0), z1) -> S(plus#2(z0, z1)) mult#2(0, z0) -> 0 mult#2(S(z0), z1) -> plus#2(z1, mult#2(z0, z1)) map#2(Cons(z0, z1)) -> Cons(mult#2(z0, z0), map#2(z1)) map#2(Nil) -> Nil unfoldr#2(S(z0)) -> Cons(z0, unfoldr#2(z0)) unfoldr#2(0) -> Nil Tuples: SUM#1(Cons(z0, z1)) -> c1(PLUS#2(z0, sum#1(z1)), SUM#1(z1)) MULT#2(S(z0), z1) -> c8(PLUS#2(z1, mult#2(z0, z1)), MULT#2(z0, z1)) MAIN(S(z0)) -> c(MAP#2(Cons(S(z0), Cons(z0, unfoldr#2(z0))))) MAP#2(Cons(S(y0), z1)) -> c3(MULT#2(S(y0), S(y0))) MAIN(S(z0)) -> c(SUM#1(Cons(mult#2(S(z0), S(z0)), Cons(mult#2(z0, z0), map#2(unfoldr#2(z0)))))) MAP#2(Cons(z0, Cons(y0, y1))) -> c4(MAP#2(Cons(y0, y1))) MAP#2(Cons(z0, Cons(S(y0), y1))) -> c4(MAP#2(Cons(S(y0), y1))) MAIN(S(z0)) -> c(SUM#1(Cons(plus#2(S(z0), mult#2(z0, S(z0))), map#2(Cons(z0, unfoldr#2(z0)))))) UNFOLDR#2(S(S(y0))) -> c6(UNFOLDR#2(S(y0))) PLUS#2(S(S(y0)), z1) -> c10(PLUS#2(S(y0), z1)) MAIN(S(S(z0))) -> c(SUM#1(Cons(mult#2(S(S(z0)), S(S(z0))), map#2(Cons(S(z0), Cons(z0, unfoldr#2(z0))))))) MAIN(S(0)) -> c(SUM#1(Cons(mult#2(S(0), S(0)), map#2(Cons(0, Nil))))) MAIN(S(z0)) -> c(SUM#1(Cons(plus#2(S(z0), mult#2(z0, S(z0))), Cons(mult#2(z0, z0), map#2(unfoldr#2(z0)))))) S tuples: PLUS#2(S(S(y0)), z1) -> c10(PLUS#2(S(y0), z1)) K tuples: MAIN(S(z0)) -> c(SUM#1(map#2(Cons(S(z0), unfoldr#2(S(z0)))))) MAIN(S(z0)) -> c(MAP#2(Cons(S(z0), unfoldr#2(S(z0))))) SUM#1(Cons(z0, z1)) -> c1(PLUS#2(z0, sum#1(z1)), SUM#1(z1)) MULT#2(S(z0), z1) -> c8(PLUS#2(z1, mult#2(z0, z1)), MULT#2(z0, z1)) MAP#2(Cons(S(y0), z1)) -> c3(MULT#2(S(y0), S(y0))) MAP#2(Cons(z0, Cons(y0, y1))) -> c4(MAP#2(Cons(y0, y1))) MAP#2(Cons(z0, Cons(S(y0), y1))) -> c4(MAP#2(Cons(S(y0), y1))) UNFOLDR#2(S(S(y0))) -> c6(UNFOLDR#2(S(y0))) Defined Rule Symbols: sum#1_1, plus#2_2, mult#2_2, map#2_1, unfoldr#2_1 Defined Pair Symbols: SUM#1_1, MULT#2_2, MAIN_1, MAP#2_1, UNFOLDR#2_1, PLUS#2_2 Compound Symbols: c1_2, c8_2, c_1, c3_1, c4_1, c6_1, c10_1 ---------------------------------------- (109) CdtRewritingProof (BOTH BOUNDS(ID, ID)) Used rewriting to replace MAIN(S(z0)) -> c(SUM#1(Cons(plus#2(S(z0), mult#2(z0, S(z0))), map#2(Cons(z0, unfoldr#2(z0)))))) by MAIN(S(z0)) -> c(SUM#1(Cons(plus#2(S(z0), mult#2(z0, S(z0))), Cons(mult#2(z0, z0), map#2(unfoldr#2(z0)))))) ---------------------------------------- (110) Obligation: Complexity Dependency Tuples Problem Rules: sum#1(Nil) -> 0 sum#1(Cons(z0, z1)) -> plus#2(z0, sum#1(z1)) plus#2(0, z0) -> z0 plus#2(S(z0), z1) -> S(plus#2(z0, z1)) mult#2(0, z0) -> 0 mult#2(S(z0), z1) -> plus#2(z1, mult#2(z0, z1)) map#2(Cons(z0, z1)) -> Cons(mult#2(z0, z0), map#2(z1)) map#2(Nil) -> Nil unfoldr#2(S(z0)) -> Cons(z0, unfoldr#2(z0)) unfoldr#2(0) -> Nil Tuples: SUM#1(Cons(z0, z1)) -> c1(PLUS#2(z0, sum#1(z1)), SUM#1(z1)) MULT#2(S(z0), z1) -> c8(PLUS#2(z1, mult#2(z0, z1)), MULT#2(z0, z1)) MAIN(S(z0)) -> c(MAP#2(Cons(S(z0), Cons(z0, unfoldr#2(z0))))) MAP#2(Cons(S(y0), z1)) -> c3(MULT#2(S(y0), S(y0))) MAIN(S(z0)) -> c(SUM#1(Cons(mult#2(S(z0), S(z0)), Cons(mult#2(z0, z0), map#2(unfoldr#2(z0)))))) MAP#2(Cons(z0, Cons(y0, y1))) -> c4(MAP#2(Cons(y0, y1))) MAP#2(Cons(z0, Cons(S(y0), y1))) -> c4(MAP#2(Cons(S(y0), y1))) UNFOLDR#2(S(S(y0))) -> c6(UNFOLDR#2(S(y0))) PLUS#2(S(S(y0)), z1) -> c10(PLUS#2(S(y0), z1)) MAIN(S(S(z0))) -> c(SUM#1(Cons(mult#2(S(S(z0)), S(S(z0))), map#2(Cons(S(z0), Cons(z0, unfoldr#2(z0))))))) MAIN(S(0)) -> c(SUM#1(Cons(mult#2(S(0), S(0)), map#2(Cons(0, Nil))))) MAIN(S(z0)) -> c(SUM#1(Cons(plus#2(S(z0), mult#2(z0, S(z0))), Cons(mult#2(z0, z0), map#2(unfoldr#2(z0)))))) S tuples: PLUS#2(S(S(y0)), z1) -> c10(PLUS#2(S(y0), z1)) K tuples: MAIN(S(z0)) -> c(SUM#1(map#2(Cons(S(z0), unfoldr#2(S(z0)))))) MAIN(S(z0)) -> c(MAP#2(Cons(S(z0), unfoldr#2(S(z0))))) SUM#1(Cons(z0, z1)) -> c1(PLUS#2(z0, sum#1(z1)), SUM#1(z1)) MULT#2(S(z0), z1) -> c8(PLUS#2(z1, mult#2(z0, z1)), MULT#2(z0, z1)) MAP#2(Cons(S(y0), z1)) -> c3(MULT#2(S(y0), S(y0))) MAP#2(Cons(z0, Cons(y0, y1))) -> c4(MAP#2(Cons(y0, y1))) MAP#2(Cons(z0, Cons(S(y0), y1))) -> c4(MAP#2(Cons(S(y0), y1))) UNFOLDR#2(S(S(y0))) -> c6(UNFOLDR#2(S(y0))) Defined Rule Symbols: sum#1_1, plus#2_2, mult#2_2, map#2_1, unfoldr#2_1 Defined Pair Symbols: SUM#1_1, MULT#2_2, MAIN_1, MAP#2_1, UNFOLDR#2_1, PLUS#2_2 Compound Symbols: c1_2, c8_2, c_1, c3_1, c4_1, c6_1, c10_1 ---------------------------------------- (111) CdtRewritingProof (BOTH BOUNDS(ID, ID)) Used rewriting to replace MAIN(S(z0)) -> c(SUM#1(Cons(mult#2(S(z0), S(z0)), Cons(mult#2(z0, z0), map#2(unfoldr#2(z0)))))) by MAIN(S(z0)) -> c(SUM#1(Cons(plus#2(S(z0), mult#2(z0, S(z0))), Cons(mult#2(z0, z0), map#2(unfoldr#2(z0)))))) ---------------------------------------- (112) Obligation: Complexity Dependency Tuples Problem Rules: sum#1(Nil) -> 0 sum#1(Cons(z0, z1)) -> plus#2(z0, sum#1(z1)) plus#2(0, z0) -> z0 plus#2(S(z0), z1) -> S(plus#2(z0, z1)) mult#2(0, z0) -> 0 mult#2(S(z0), z1) -> plus#2(z1, mult#2(z0, z1)) map#2(Cons(z0, z1)) -> Cons(mult#2(z0, z0), map#2(z1)) map#2(Nil) -> Nil unfoldr#2(S(z0)) -> Cons(z0, unfoldr#2(z0)) unfoldr#2(0) -> Nil Tuples: SUM#1(Cons(z0, z1)) -> c1(PLUS#2(z0, sum#1(z1)), SUM#1(z1)) MULT#2(S(z0), z1) -> c8(PLUS#2(z1, mult#2(z0, z1)), MULT#2(z0, z1)) MAIN(S(z0)) -> c(MAP#2(Cons(S(z0), Cons(z0, unfoldr#2(z0))))) MAP#2(Cons(S(y0), z1)) -> c3(MULT#2(S(y0), S(y0))) MAP#2(Cons(z0, Cons(y0, y1))) -> c4(MAP#2(Cons(y0, y1))) MAP#2(Cons(z0, Cons(S(y0), y1))) -> c4(MAP#2(Cons(S(y0), y1))) UNFOLDR#2(S(S(y0))) -> c6(UNFOLDR#2(S(y0))) PLUS#2(S(S(y0)), z1) -> c10(PLUS#2(S(y0), z1)) MAIN(S(S(z0))) -> c(SUM#1(Cons(mult#2(S(S(z0)), S(S(z0))), map#2(Cons(S(z0), Cons(z0, unfoldr#2(z0))))))) MAIN(S(0)) -> c(SUM#1(Cons(mult#2(S(0), S(0)), map#2(Cons(0, Nil))))) MAIN(S(z0)) -> c(SUM#1(Cons(plus#2(S(z0), mult#2(z0, S(z0))), Cons(mult#2(z0, z0), map#2(unfoldr#2(z0)))))) S tuples: PLUS#2(S(S(y0)), z1) -> c10(PLUS#2(S(y0), z1)) K tuples: MAIN(S(z0)) -> c(SUM#1(map#2(Cons(S(z0), unfoldr#2(S(z0)))))) MAIN(S(z0)) -> c(MAP#2(Cons(S(z0), unfoldr#2(S(z0))))) SUM#1(Cons(z0, z1)) -> c1(PLUS#2(z0, sum#1(z1)), SUM#1(z1)) MULT#2(S(z0), z1) -> c8(PLUS#2(z1, mult#2(z0, z1)), MULT#2(z0, z1)) MAP#2(Cons(S(y0), z1)) -> c3(MULT#2(S(y0), S(y0))) MAP#2(Cons(z0, Cons(y0, y1))) -> c4(MAP#2(Cons(y0, y1))) MAP#2(Cons(z0, Cons(S(y0), y1))) -> c4(MAP#2(Cons(S(y0), y1))) UNFOLDR#2(S(S(y0))) -> c6(UNFOLDR#2(S(y0))) Defined Rule Symbols: sum#1_1, plus#2_2, mult#2_2, map#2_1, unfoldr#2_1 Defined Pair Symbols: SUM#1_1, MULT#2_2, MAIN_1, MAP#2_1, UNFOLDR#2_1, PLUS#2_2 Compound Symbols: c1_2, c8_2, c_1, c3_1, c4_1, c6_1, c10_1 ---------------------------------------- (113) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID)) Use forward instantiation to replace MAP#2(Cons(z0, Cons(y0, y1))) -> c4(MAP#2(Cons(y0, y1))) by MAP#2(Cons(z0, Cons(S(y0), z2))) -> c4(MAP#2(Cons(S(y0), z2))) MAP#2(Cons(z0, Cons(z1, Cons(y1, y2)))) -> c4(MAP#2(Cons(z1, Cons(y1, y2)))) MAP#2(Cons(z0, Cons(z1, Cons(S(y1), y2)))) -> c4(MAP#2(Cons(z1, Cons(S(y1), y2)))) ---------------------------------------- (114) Obligation: Complexity Dependency Tuples Problem Rules: sum#1(Nil) -> 0 sum#1(Cons(z0, z1)) -> plus#2(z0, sum#1(z1)) plus#2(0, z0) -> z0 plus#2(S(z0), z1) -> S(plus#2(z0, z1)) mult#2(0, z0) -> 0 mult#2(S(z0), z1) -> plus#2(z1, mult#2(z0, z1)) map#2(Cons(z0, z1)) -> Cons(mult#2(z0, z0), map#2(z1)) map#2(Nil) -> Nil unfoldr#2(S(z0)) -> Cons(z0, unfoldr#2(z0)) unfoldr#2(0) -> Nil Tuples: SUM#1(Cons(z0, z1)) -> c1(PLUS#2(z0, sum#1(z1)), SUM#1(z1)) MULT#2(S(z0), z1) -> c8(PLUS#2(z1, mult#2(z0, z1)), MULT#2(z0, z1)) MAIN(S(z0)) -> c(MAP#2(Cons(S(z0), Cons(z0, unfoldr#2(z0))))) MAP#2(Cons(S(y0), z1)) -> c3(MULT#2(S(y0), S(y0))) MAP#2(Cons(z0, Cons(S(y0), y1))) -> c4(MAP#2(Cons(S(y0), y1))) UNFOLDR#2(S(S(y0))) -> c6(UNFOLDR#2(S(y0))) PLUS#2(S(S(y0)), z1) -> c10(PLUS#2(S(y0), z1)) MAIN(S(S(z0))) -> c(SUM#1(Cons(mult#2(S(S(z0)), S(S(z0))), map#2(Cons(S(z0), Cons(z0, unfoldr#2(z0))))))) MAIN(S(0)) -> c(SUM#1(Cons(mult#2(S(0), S(0)), map#2(Cons(0, Nil))))) MAIN(S(z0)) -> c(SUM#1(Cons(plus#2(S(z0), mult#2(z0, S(z0))), Cons(mult#2(z0, z0), map#2(unfoldr#2(z0)))))) MAP#2(Cons(z0, Cons(z1, Cons(y1, y2)))) -> c4(MAP#2(Cons(z1, Cons(y1, y2)))) MAP#2(Cons(z0, Cons(z1, Cons(S(y1), y2)))) -> c4(MAP#2(Cons(z1, Cons(S(y1), y2)))) S tuples: PLUS#2(S(S(y0)), z1) -> c10(PLUS#2(S(y0), z1)) K tuples: MAIN(S(z0)) -> c(SUM#1(map#2(Cons(S(z0), unfoldr#2(S(z0)))))) MAIN(S(z0)) -> c(MAP#2(Cons(S(z0), unfoldr#2(S(z0))))) SUM#1(Cons(z0, z1)) -> c1(PLUS#2(z0, sum#1(z1)), SUM#1(z1)) MULT#2(S(z0), z1) -> c8(PLUS#2(z1, mult#2(z0, z1)), MULT#2(z0, z1)) MAP#2(Cons(S(y0), z1)) -> c3(MULT#2(S(y0), S(y0))) MAP#2(Cons(z0, Cons(S(y0), y1))) -> c4(MAP#2(Cons(S(y0), y1))) UNFOLDR#2(S(S(y0))) -> c6(UNFOLDR#2(S(y0))) MAP#2(Cons(z0, Cons(z1, Cons(y1, y2)))) -> c4(MAP#2(Cons(z1, Cons(y1, y2)))) MAP#2(Cons(z0, Cons(z1, Cons(S(y1), y2)))) -> c4(MAP#2(Cons(z1, Cons(S(y1), y2)))) Defined Rule Symbols: sum#1_1, plus#2_2, mult#2_2, map#2_1, unfoldr#2_1 Defined Pair Symbols: SUM#1_1, MULT#2_2, MAIN_1, MAP#2_1, UNFOLDR#2_1, PLUS#2_2 Compound Symbols: c1_2, c8_2, c_1, c3_1, c4_1, c6_1, c10_1 ---------------------------------------- (115) CdtRewritingProof (BOTH BOUNDS(ID, ID)) Used rewriting to replace MAIN(S(S(z0))) -> c(SUM#1(Cons(mult#2(S(S(z0)), S(S(z0))), map#2(Cons(S(z0), Cons(z0, unfoldr#2(z0))))))) by MAIN(S(S(z0))) -> c(SUM#1(Cons(mult#2(S(S(z0)), S(S(z0))), Cons(mult#2(S(z0), S(z0)), map#2(Cons(z0, unfoldr#2(z0))))))) ---------------------------------------- (116) Obligation: Complexity Dependency Tuples Problem Rules: sum#1(Nil) -> 0 sum#1(Cons(z0, z1)) -> plus#2(z0, sum#1(z1)) plus#2(0, z0) -> z0 plus#2(S(z0), z1) -> S(plus#2(z0, z1)) mult#2(0, z0) -> 0 mult#2(S(z0), z1) -> plus#2(z1, mult#2(z0, z1)) map#2(Cons(z0, z1)) -> Cons(mult#2(z0, z0), map#2(z1)) map#2(Nil) -> Nil unfoldr#2(S(z0)) -> Cons(z0, unfoldr#2(z0)) unfoldr#2(0) -> Nil Tuples: SUM#1(Cons(z0, z1)) -> c1(PLUS#2(z0, sum#1(z1)), SUM#1(z1)) MULT#2(S(z0), z1) -> c8(PLUS#2(z1, mult#2(z0, z1)), MULT#2(z0, z1)) MAIN(S(z0)) -> c(MAP#2(Cons(S(z0), Cons(z0, unfoldr#2(z0))))) MAP#2(Cons(S(y0), z1)) -> c3(MULT#2(S(y0), S(y0))) MAP#2(Cons(z0, Cons(S(y0), y1))) -> c4(MAP#2(Cons(S(y0), y1))) UNFOLDR#2(S(S(y0))) -> c6(UNFOLDR#2(S(y0))) PLUS#2(S(S(y0)), z1) -> c10(PLUS#2(S(y0), z1)) MAIN(S(0)) -> c(SUM#1(Cons(mult#2(S(0), S(0)), map#2(Cons(0, Nil))))) MAIN(S(z0)) -> c(SUM#1(Cons(plus#2(S(z0), mult#2(z0, S(z0))), Cons(mult#2(z0, z0), map#2(unfoldr#2(z0)))))) MAP#2(Cons(z0, Cons(z1, Cons(y1, y2)))) -> c4(MAP#2(Cons(z1, Cons(y1, y2)))) MAP#2(Cons(z0, Cons(z1, Cons(S(y1), y2)))) -> c4(MAP#2(Cons(z1, Cons(S(y1), y2)))) MAIN(S(S(z0))) -> c(SUM#1(Cons(mult#2(S(S(z0)), S(S(z0))), Cons(mult#2(S(z0), S(z0)), map#2(Cons(z0, unfoldr#2(z0))))))) S tuples: PLUS#2(S(S(y0)), z1) -> c10(PLUS#2(S(y0), z1)) K tuples: MAIN(S(z0)) -> c(SUM#1(map#2(Cons(S(z0), unfoldr#2(S(z0)))))) MAIN(S(z0)) -> c(MAP#2(Cons(S(z0), unfoldr#2(S(z0))))) SUM#1(Cons(z0, z1)) -> c1(PLUS#2(z0, sum#1(z1)), SUM#1(z1)) MULT#2(S(z0), z1) -> c8(PLUS#2(z1, mult#2(z0, z1)), MULT#2(z0, z1)) MAP#2(Cons(S(y0), z1)) -> c3(MULT#2(S(y0), S(y0))) MAP#2(Cons(z0, Cons(S(y0), y1))) -> c4(MAP#2(Cons(S(y0), y1))) UNFOLDR#2(S(S(y0))) -> c6(UNFOLDR#2(S(y0))) MAP#2(Cons(z0, Cons(z1, Cons(y1, y2)))) -> c4(MAP#2(Cons(z1, Cons(y1, y2)))) MAP#2(Cons(z0, Cons(z1, Cons(S(y1), y2)))) -> c4(MAP#2(Cons(z1, Cons(S(y1), y2)))) Defined Rule Symbols: sum#1_1, plus#2_2, mult#2_2, map#2_1, unfoldr#2_1 Defined Pair Symbols: SUM#1_1, MULT#2_2, MAIN_1, MAP#2_1, UNFOLDR#2_1, PLUS#2_2 Compound Symbols: c1_2, c8_2, c_1, c3_1, c4_1, c6_1, c10_1 ---------------------------------------- (117) CdtRewritingProof (BOTH BOUNDS(ID, ID)) Used rewriting to replace MAIN(S(0)) -> c(SUM#1(Cons(mult#2(S(0), S(0)), map#2(Cons(0, Nil))))) by MAIN(S(0)) -> c(SUM#1(Cons(mult#2(S(0), S(0)), Cons(mult#2(0, 0), map#2(Nil))))) ---------------------------------------- (118) Obligation: Complexity Dependency Tuples Problem Rules: sum#1(Nil) -> 0 sum#1(Cons(z0, z1)) -> plus#2(z0, sum#1(z1)) plus#2(0, z0) -> z0 plus#2(S(z0), z1) -> S(plus#2(z0, z1)) mult#2(0, z0) -> 0 mult#2(S(z0), z1) -> plus#2(z1, mult#2(z0, z1)) map#2(Cons(z0, z1)) -> Cons(mult#2(z0, z0), map#2(z1)) map#2(Nil) -> Nil unfoldr#2(S(z0)) -> Cons(z0, unfoldr#2(z0)) unfoldr#2(0) -> Nil Tuples: SUM#1(Cons(z0, z1)) -> c1(PLUS#2(z0, sum#1(z1)), SUM#1(z1)) MULT#2(S(z0), z1) -> c8(PLUS#2(z1, mult#2(z0, z1)), MULT#2(z0, z1)) MAIN(S(z0)) -> c(MAP#2(Cons(S(z0), Cons(z0, unfoldr#2(z0))))) MAP#2(Cons(S(y0), z1)) -> c3(MULT#2(S(y0), S(y0))) MAP#2(Cons(z0, Cons(S(y0), y1))) -> c4(MAP#2(Cons(S(y0), y1))) UNFOLDR#2(S(S(y0))) -> c6(UNFOLDR#2(S(y0))) PLUS#2(S(S(y0)), z1) -> c10(PLUS#2(S(y0), z1)) MAIN(S(z0)) -> c(SUM#1(Cons(plus#2(S(z0), mult#2(z0, S(z0))), Cons(mult#2(z0, z0), map#2(unfoldr#2(z0)))))) MAP#2(Cons(z0, Cons(z1, Cons(y1, y2)))) -> c4(MAP#2(Cons(z1, Cons(y1, y2)))) MAP#2(Cons(z0, Cons(z1, Cons(S(y1), y2)))) -> c4(MAP#2(Cons(z1, Cons(S(y1), y2)))) MAIN(S(S(z0))) -> c(SUM#1(Cons(mult#2(S(S(z0)), S(S(z0))), Cons(mult#2(S(z0), S(z0)), map#2(Cons(z0, unfoldr#2(z0))))))) MAIN(S(0)) -> c(SUM#1(Cons(mult#2(S(0), S(0)), Cons(mult#2(0, 0), map#2(Nil))))) S tuples: PLUS#2(S(S(y0)), z1) -> c10(PLUS#2(S(y0), z1)) K tuples: MAIN(S(z0)) -> c(SUM#1(map#2(Cons(S(z0), unfoldr#2(S(z0)))))) MAIN(S(z0)) -> c(MAP#2(Cons(S(z0), unfoldr#2(S(z0))))) SUM#1(Cons(z0, z1)) -> c1(PLUS#2(z0, sum#1(z1)), SUM#1(z1)) MULT#2(S(z0), z1) -> c8(PLUS#2(z1, mult#2(z0, z1)), MULT#2(z0, z1)) MAP#2(Cons(S(y0), z1)) -> c3(MULT#2(S(y0), S(y0))) MAP#2(Cons(z0, Cons(S(y0), y1))) -> c4(MAP#2(Cons(S(y0), y1))) UNFOLDR#2(S(S(y0))) -> c6(UNFOLDR#2(S(y0))) MAP#2(Cons(z0, Cons(z1, Cons(y1, y2)))) -> c4(MAP#2(Cons(z1, Cons(y1, y2)))) MAP#2(Cons(z0, Cons(z1, Cons(S(y1), y2)))) -> c4(MAP#2(Cons(z1, Cons(S(y1), y2)))) Defined Rule Symbols: sum#1_1, plus#2_2, mult#2_2, map#2_1, unfoldr#2_1 Defined Pair Symbols: SUM#1_1, MULT#2_2, MAIN_1, MAP#2_1, UNFOLDR#2_1, PLUS#2_2 Compound Symbols: c1_2, c8_2, c_1, c3_1, c4_1, c6_1, c10_1 ---------------------------------------- (119) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID)) Use forward instantiation to replace UNFOLDR#2(S(S(y0))) -> c6(UNFOLDR#2(S(y0))) by UNFOLDR#2(S(S(S(y0)))) -> c6(UNFOLDR#2(S(S(y0)))) ---------------------------------------- (120) Obligation: Complexity Dependency Tuples Problem Rules: sum#1(Nil) -> 0 sum#1(Cons(z0, z1)) -> plus#2(z0, sum#1(z1)) plus#2(0, z0) -> z0 plus#2(S(z0), z1) -> S(plus#2(z0, z1)) mult#2(0, z0) -> 0 mult#2(S(z0), z1) -> plus#2(z1, mult#2(z0, z1)) map#2(Cons(z0, z1)) -> Cons(mult#2(z0, z0), map#2(z1)) map#2(Nil) -> Nil unfoldr#2(S(z0)) -> Cons(z0, unfoldr#2(z0)) unfoldr#2(0) -> Nil Tuples: SUM#1(Cons(z0, z1)) -> c1(PLUS#2(z0, sum#1(z1)), SUM#1(z1)) MULT#2(S(z0), z1) -> c8(PLUS#2(z1, mult#2(z0, z1)), MULT#2(z0, z1)) MAIN(S(z0)) -> c(MAP#2(Cons(S(z0), Cons(z0, unfoldr#2(z0))))) MAP#2(Cons(S(y0), z1)) -> c3(MULT#2(S(y0), S(y0))) MAP#2(Cons(z0, Cons(S(y0), y1))) -> c4(MAP#2(Cons(S(y0), y1))) PLUS#2(S(S(y0)), z1) -> c10(PLUS#2(S(y0), z1)) MAIN(S(z0)) -> c(SUM#1(Cons(plus#2(S(z0), mult#2(z0, S(z0))), Cons(mult#2(z0, z0), map#2(unfoldr#2(z0)))))) MAP#2(Cons(z0, Cons(z1, Cons(y1, y2)))) -> c4(MAP#2(Cons(z1, Cons(y1, y2)))) MAP#2(Cons(z0, Cons(z1, Cons(S(y1), y2)))) -> c4(MAP#2(Cons(z1, Cons(S(y1), y2)))) MAIN(S(S(z0))) -> c(SUM#1(Cons(mult#2(S(S(z0)), S(S(z0))), Cons(mult#2(S(z0), S(z0)), map#2(Cons(z0, unfoldr#2(z0))))))) MAIN(S(0)) -> c(SUM#1(Cons(mult#2(S(0), S(0)), Cons(mult#2(0, 0), map#2(Nil))))) UNFOLDR#2(S(S(S(y0)))) -> c6(UNFOLDR#2(S(S(y0)))) S tuples: PLUS#2(S(S(y0)), z1) -> c10(PLUS#2(S(y0), z1)) K tuples: MAIN(S(z0)) -> c(SUM#1(map#2(Cons(S(z0), unfoldr#2(S(z0)))))) MAIN(S(z0)) -> c(MAP#2(Cons(S(z0), unfoldr#2(S(z0))))) SUM#1(Cons(z0, z1)) -> c1(PLUS#2(z0, sum#1(z1)), SUM#1(z1)) MULT#2(S(z0), z1) -> c8(PLUS#2(z1, mult#2(z0, z1)), MULT#2(z0, z1)) MAP#2(Cons(S(y0), z1)) -> c3(MULT#2(S(y0), S(y0))) MAP#2(Cons(z0, Cons(S(y0), y1))) -> c4(MAP#2(Cons(S(y0), y1))) MAP#2(Cons(z0, Cons(z1, Cons(y1, y2)))) -> c4(MAP#2(Cons(z1, Cons(y1, y2)))) MAP#2(Cons(z0, Cons(z1, Cons(S(y1), y2)))) -> c4(MAP#2(Cons(z1, Cons(S(y1), y2)))) UNFOLDR#2(S(S(S(y0)))) -> c6(UNFOLDR#2(S(S(y0)))) Defined Rule Symbols: sum#1_1, plus#2_2, mult#2_2, map#2_1, unfoldr#2_1 Defined Pair Symbols: SUM#1_1, MULT#2_2, MAIN_1, MAP#2_1, PLUS#2_2, UNFOLDR#2_1 Compound Symbols: c1_2, c8_2, c_1, c3_1, c4_1, c10_1, c6_1 ---------------------------------------- (121) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID)) Use forward instantiation to replace PLUS#2(S(S(y0)), z1) -> c10(PLUS#2(S(y0), z1)) by PLUS#2(S(S(S(y0))), z1) -> c10(PLUS#2(S(S(y0)), z1)) ---------------------------------------- (122) Obligation: Complexity Dependency Tuples Problem Rules: sum#1(Nil) -> 0 sum#1(Cons(z0, z1)) -> plus#2(z0, sum#1(z1)) plus#2(0, z0) -> z0 plus#2(S(z0), z1) -> S(plus#2(z0, z1)) mult#2(0, z0) -> 0 mult#2(S(z0), z1) -> plus#2(z1, mult#2(z0, z1)) map#2(Cons(z0, z1)) -> Cons(mult#2(z0, z0), map#2(z1)) map#2(Nil) -> Nil unfoldr#2(S(z0)) -> Cons(z0, unfoldr#2(z0)) unfoldr#2(0) -> Nil Tuples: SUM#1(Cons(z0, z1)) -> c1(PLUS#2(z0, sum#1(z1)), SUM#1(z1)) MULT#2(S(z0), z1) -> c8(PLUS#2(z1, mult#2(z0, z1)), MULT#2(z0, z1)) MAIN(S(z0)) -> c(MAP#2(Cons(S(z0), Cons(z0, unfoldr#2(z0))))) MAP#2(Cons(S(y0), z1)) -> c3(MULT#2(S(y0), S(y0))) MAP#2(Cons(z0, Cons(S(y0), y1))) -> c4(MAP#2(Cons(S(y0), y1))) MAIN(S(z0)) -> c(SUM#1(Cons(plus#2(S(z0), mult#2(z0, S(z0))), Cons(mult#2(z0, z0), map#2(unfoldr#2(z0)))))) MAP#2(Cons(z0, Cons(z1, Cons(y1, y2)))) -> c4(MAP#2(Cons(z1, Cons(y1, y2)))) MAP#2(Cons(z0, Cons(z1, Cons(S(y1), y2)))) -> c4(MAP#2(Cons(z1, Cons(S(y1), y2)))) MAIN(S(S(z0))) -> c(SUM#1(Cons(mult#2(S(S(z0)), S(S(z0))), Cons(mult#2(S(z0), S(z0)), map#2(Cons(z0, unfoldr#2(z0))))))) MAIN(S(0)) -> c(SUM#1(Cons(mult#2(S(0), S(0)), Cons(mult#2(0, 0), map#2(Nil))))) UNFOLDR#2(S(S(S(y0)))) -> c6(UNFOLDR#2(S(S(y0)))) PLUS#2(S(S(S(y0))), z1) -> c10(PLUS#2(S(S(y0)), z1)) S tuples: PLUS#2(S(S(S(y0))), z1) -> c10(PLUS#2(S(S(y0)), z1)) K tuples: MAIN(S(z0)) -> c(SUM#1(map#2(Cons(S(z0), unfoldr#2(S(z0)))))) MAIN(S(z0)) -> c(MAP#2(Cons(S(z0), unfoldr#2(S(z0))))) SUM#1(Cons(z0, z1)) -> c1(PLUS#2(z0, sum#1(z1)), SUM#1(z1)) MULT#2(S(z0), z1) -> c8(PLUS#2(z1, mult#2(z0, z1)), MULT#2(z0, z1)) MAP#2(Cons(S(y0), z1)) -> c3(MULT#2(S(y0), S(y0))) MAP#2(Cons(z0, Cons(S(y0), y1))) -> c4(MAP#2(Cons(S(y0), y1))) MAP#2(Cons(z0, Cons(z1, Cons(y1, y2)))) -> c4(MAP#2(Cons(z1, Cons(y1, y2)))) MAP#2(Cons(z0, Cons(z1, Cons(S(y1), y2)))) -> c4(MAP#2(Cons(z1, Cons(S(y1), y2)))) UNFOLDR#2(S(S(S(y0)))) -> c6(UNFOLDR#2(S(S(y0)))) Defined Rule Symbols: sum#1_1, plus#2_2, mult#2_2, map#2_1, unfoldr#2_1 Defined Pair Symbols: SUM#1_1, MULT#2_2, MAIN_1, MAP#2_1, UNFOLDR#2_1, PLUS#2_2 Compound Symbols: c1_2, c8_2, c_1, c3_1, c4_1, c6_1, c10_1