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