WORST_CASE(Omega(n^1),O(n^1))
proof of /export/starexec/sandbox2/benchmark/theBenchmark.trs
# AProVE Commit ID: c69e44bd14796315568835c1ffa2502984884775 mhark 20210624 unpublished


The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, n^1).

(0) CpxRelTRS
(1) SInnermostTerminationProof [BOTH CONCRETE BOUNDS(ID, ID), 319 ms]
(2) CpxRelTRS
(3) CpxTrsToCdtProof [UPPER BOUND(ID), 0 ms]
(4) CdtProblem
    (5) CdtLeafRemovalProof [ComplexityIfPolyImplication, 0 ms]
    (6) CdtProblem
    (7) CdtUsableRulesProof [BOTH BOUNDS(ID, ID), 0 ms]
    (8) CdtProblem
    (9) CdtRuleRemovalProof [UPPER BOUND(ADD(n^1)), 29 ms]
    (10) CdtProblem
    (11) CdtRuleRemovalProof [UPPER BOUND(ADD(n^1)), 18 ms]
    (12) CdtProblem
    (13) SIsEmptyProof [BOTH BOUNDS(ID, ID), 0 ms]
    (14) BOUNDS(1, 1)
(15) RelTrsToDecreasingLoopProblemProof [LOWER BOUND(ID), 0 ms]
(16) TRS for Loop Detection
    (17) DecreasingLoopProof [LOWER BOUND(ID), 0 ms]
    (18) BEST
        (19) proven lower bound
            (20) LowerBoundPropagationProof [FINISHED, 0 ms]
            (21) BOUNDS(n^1, INF)
        (22) TRS for Loop Detection


----------------------------------------

(0)
Obligation:
The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, n^1).


The TRS R consists of the following rules:

   MAP(Cons(z0, z1)) -> c4(F(z0))
   MAP(Cons(z0, z1)) -> c5(MAP(z1))
   MAP(Nil) -> c6
   GOAL(z0) -> c7(MAP(z0))
   F(z0) -> c8(*'(z0, z0))
   +FULL(S(z0), z1) -> c9(+FULL(z0, S(z1)))
   +FULL(0, z0) -> c10

The (relative) TRS S consists of the following rules:

   *'(z0, S(S(z1))) -> c(*'(z0, S(z1)))
   *'(z0, S(0)) -> c1
   *'(z0, 0) -> c2
   *'(0, z0) -> c3
   *(z0, S(S(z1))) -> +(z0, *(z0, S(z1)))
   *(z0, S(0)) -> z0
   *(z0, 0) -> 0
   *(0, z0) -> 0
   map(Cons(z0, z1)) -> Cons(f(z0), map(z1))
   map(Nil) -> Nil
   goal(z0) -> map(z0)
   f(z0) -> *(z0, z0)
   +Full(S(z0), z1) -> +Full(z0, S(z1))
   +Full(0, z0) -> z0

Rewrite Strategy: INNERMOST
----------------------------------------

(1) SInnermostTerminationProof (BOTH CONCRETE BOUNDS(ID, ID))
proved innermost termination of relative rules
----------------------------------------

(2)
Obligation:
The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, n^1).


The TRS R consists of the following rules:

   MAP(Cons(z0, z1)) -> c4(F(z0))
   MAP(Cons(z0, z1)) -> c5(MAP(z1))
   MAP(Nil) -> c6
   GOAL(z0) -> c7(MAP(z0))
   F(z0) -> c8(*'(z0, z0))
   +FULL(S(z0), z1) -> c9(+FULL(z0, S(z1)))
   +FULL(0, z0) -> c10

The (relative) TRS S consists of the following rules:

   *'(z0, S(S(z1))) -> c(*'(z0, S(z1)))
   *'(z0, S(0)) -> c1
   *'(z0, 0) -> c2
   *'(0, z0) -> c3
   *(z0, S(S(z1))) -> +(z0, *(z0, S(z1)))
   *(z0, S(0)) -> z0
   *(z0, 0) -> 0
   *(0, z0) -> 0
   map(Cons(z0, z1)) -> Cons(f(z0), map(z1))
   map(Nil) -> Nil
   goal(z0) -> map(z0)
   f(z0) -> *(z0, z0)
   +Full(S(z0), z1) -> +Full(z0, S(z1))
   +Full(0, z0) -> z0

Rewrite Strategy: INNERMOST
----------------------------------------

(3) CpxTrsToCdtProof (UPPER BOUND(ID))
Converted Cpx (relative) TRS to CDT
----------------------------------------

(4)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   *'(z0, S(S(z1))) -> c(*'(z0, S(z1)))
   *'(z0, S(0)) -> c1
   *'(z0, 0) -> c2
   *'(0, z0) -> c3
   *(z0, S(S(z1))) -> +(z0, *(z0, S(z1)))
   *(z0, S(0)) -> z0
   *(z0, 0) -> 0
   *(0, z0) -> 0
   map(Cons(z0, z1)) -> Cons(f(z0), map(z1))
   map(Nil) -> Nil
   goal(z0) -> map(z0)
   f(z0) -> *(z0, z0)
   +Full(S(z0), z1) -> +Full(z0, S(z1))
   +Full(0, z0) -> z0
   MAP(Cons(z0, z1)) -> c4(F(z0))
   MAP(Cons(z0, z1)) -> c5(MAP(z1))
   MAP(Nil) -> c6
   GOAL(z0) -> c7(MAP(z0))
   F(z0) -> c8(*'(z0, z0))
   +FULL(S(z0), z1) -> c9(+FULL(z0, S(z1)))
   +FULL(0, z0) -> c10
Tuples:
   *''(z0, S(S(z1))) -> c11(*''(z0, S(z1)))
   *''(z0, S(0)) -> c12
   *''(z0, 0) -> c13
   *''(0, z0) -> c14
   *1(z0, S(S(z1))) -> c15(*1(z0, S(z1)))
   *1(z0, S(0)) -> c16
   *1(z0, 0) -> c17
   *1(0, z0) -> c18
   MAP'(Cons(z0, z1)) -> c19(F'(z0), MAP'(z1))
   MAP'(Nil) -> c20
   GOAL'(z0) -> c21(MAP'(z0))
   F'(z0) -> c22(*1(z0, z0))
   +FULL'(S(z0), z1) -> c23(+FULL'(z0, S(z1)))
   +FULL'(0, z0) -> c24
   MAP''(Cons(z0, z1)) -> c25(F''(z0))
   MAP''(Cons(z0, z1)) -> c26(MAP''(z1))
   MAP''(Nil) -> c27
   GOAL''(z0) -> c28(MAP''(z0))
   F''(z0) -> c29(*''(z0, z0))
   +FULL''(S(z0), z1) -> c30(+FULL''(z0, S(z1)))
   +FULL''(0, z0) -> c31
S tuples:
   MAP''(Cons(z0, z1)) -> c25(F''(z0))
   MAP''(Cons(z0, z1)) -> c26(MAP''(z1))
   MAP''(Nil) -> c27
   GOAL''(z0) -> c28(MAP''(z0))
   F''(z0) -> c29(*''(z0, z0))
   +FULL''(S(z0), z1) -> c30(+FULL''(z0, S(z1)))
   +FULL''(0, z0) -> c31
K tuples:none
Defined Rule Symbols:   MAP_1, GOAL_1, F_1, +FULL_2, *'_2, *_2, map_1, goal_1, f_1, +Full_2

Defined Pair Symbols:   *''_2, *1_2, MAP'_1, GOAL'_1, F'_1, +FULL'_2, MAP''_1, GOAL''_1, F''_1, +FULL''_2

Compound Symbols:   c11_1, c12, c13, c14, c15_1, c16, c17, c18, c19_2, c20, c21_1, c22_1, c23_1, c24, c25_1, c26_1, c27, c28_1, c29_1, c30_1, c31


----------------------------------------

(5) CdtLeafRemovalProof (ComplexityIfPolyImplication)
Removed 2 leading nodes:
   GOAL''(z0) -> c28(MAP''(z0))
   GOAL'(z0) -> c21(MAP'(z0))
Removed 10 trailing nodes:
   *1(0, z0) -> c18
   +FULL'(0, z0) -> c24
   *1(z0, S(0)) -> c16
   +FULL''(0, z0) -> c31
   MAP''(Nil) -> c27
   *1(z0, 0) -> c17
   MAP'(Nil) -> c20
   *''(0, z0) -> c14
   *''(z0, 0) -> c13
   *''(z0, S(0)) -> c12

----------------------------------------

(6)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   *'(z0, S(S(z1))) -> c(*'(z0, S(z1)))
   *'(z0, S(0)) -> c1
   *'(z0, 0) -> c2
   *'(0, z0) -> c3
   *(z0, S(S(z1))) -> +(z0, *(z0, S(z1)))
   *(z0, S(0)) -> z0
   *(z0, 0) -> 0
   *(0, z0) -> 0
   map(Cons(z0, z1)) -> Cons(f(z0), map(z1))
   map(Nil) -> Nil
   goal(z0) -> map(z0)
   f(z0) -> *(z0, z0)
   +Full(S(z0), z1) -> +Full(z0, S(z1))
   +Full(0, z0) -> z0
   MAP(Cons(z0, z1)) -> c4(F(z0))
   MAP(Cons(z0, z1)) -> c5(MAP(z1))
   MAP(Nil) -> c6
   GOAL(z0) -> c7(MAP(z0))
   F(z0) -> c8(*'(z0, z0))
   +FULL(S(z0), z1) -> c9(+FULL(z0, S(z1)))
   +FULL(0, z0) -> c10
Tuples:
   *''(z0, S(S(z1))) -> c11(*''(z0, S(z1)))
   *1(z0, S(S(z1))) -> c15(*1(z0, S(z1)))
   MAP'(Cons(z0, z1)) -> c19(F'(z0), MAP'(z1))
   F'(z0) -> c22(*1(z0, z0))
   +FULL'(S(z0), z1) -> c23(+FULL'(z0, S(z1)))
   MAP''(Cons(z0, z1)) -> c25(F''(z0))
   MAP''(Cons(z0, z1)) -> c26(MAP''(z1))
   F''(z0) -> c29(*''(z0, z0))
   +FULL''(S(z0), z1) -> c30(+FULL''(z0, S(z1)))
S tuples:
   MAP''(Cons(z0, z1)) -> c25(F''(z0))
   MAP''(Cons(z0, z1)) -> c26(MAP''(z1))
   F''(z0) -> c29(*''(z0, z0))
   +FULL''(S(z0), z1) -> c30(+FULL''(z0, S(z1)))
K tuples:none
Defined Rule Symbols:   MAP_1, GOAL_1, F_1, +FULL_2, *'_2, *_2, map_1, goal_1, f_1, +Full_2

Defined Pair Symbols:   *''_2, *1_2, MAP'_1, F'_1, +FULL'_2, MAP''_1, F''_1, +FULL''_2

Compound Symbols:   c11_1, c15_1, c19_2, c22_1, c23_1, c25_1, c26_1, c29_1, c30_1


----------------------------------------

(7) CdtUsableRulesProof (BOTH BOUNDS(ID, ID))
The following rules are not usable and were removed:
   *'(z0, S(S(z1))) -> c(*'(z0, S(z1)))
   *'(z0, S(0)) -> c1
   *'(z0, 0) -> c2
   *'(0, z0) -> c3
   *(z0, S(S(z1))) -> +(z0, *(z0, S(z1)))
   *(z0, S(0)) -> z0
   *(z0, 0) -> 0
   *(0, z0) -> 0
   map(Cons(z0, z1)) -> Cons(f(z0), map(z1))
   map(Nil) -> Nil
   goal(z0) -> map(z0)
   f(z0) -> *(z0, z0)
   +Full(S(z0), z1) -> +Full(z0, S(z1))
   +Full(0, z0) -> z0
   MAP(Cons(z0, z1)) -> c4(F(z0))
   MAP(Cons(z0, z1)) -> c5(MAP(z1))
   MAP(Nil) -> c6
   GOAL(z0) -> c7(MAP(z0))
   F(z0) -> c8(*'(z0, z0))
   +FULL(S(z0), z1) -> c9(+FULL(z0, S(z1)))
   +FULL(0, z0) -> c10

----------------------------------------

(8)
Obligation:
Complexity Dependency Tuples Problem

Rules:none
Tuples:
   *''(z0, S(S(z1))) -> c11(*''(z0, S(z1)))
   *1(z0, S(S(z1))) -> c15(*1(z0, S(z1)))
   MAP'(Cons(z0, z1)) -> c19(F'(z0), MAP'(z1))
   F'(z0) -> c22(*1(z0, z0))
   +FULL'(S(z0), z1) -> c23(+FULL'(z0, S(z1)))
   MAP''(Cons(z0, z1)) -> c25(F''(z0))
   MAP''(Cons(z0, z1)) -> c26(MAP''(z1))
   F''(z0) -> c29(*''(z0, z0))
   +FULL''(S(z0), z1) -> c30(+FULL''(z0, S(z1)))
S tuples:
   MAP''(Cons(z0, z1)) -> c25(F''(z0))
   MAP''(Cons(z0, z1)) -> c26(MAP''(z1))
   F''(z0) -> c29(*''(z0, z0))
   +FULL''(S(z0), z1) -> c30(+FULL''(z0, S(z1)))
K tuples:none
Defined Rule Symbols:none

Defined Pair Symbols:   *''_2, *1_2, MAP'_1, F'_1, +FULL'_2, MAP''_1, F''_1, +FULL''_2

Compound Symbols:   c11_1, c15_1, c19_2, c22_1, c23_1, c25_1, c26_1, c29_1, c30_1


----------------------------------------

(9) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)))
Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.
   MAP''(Cons(z0, z1)) -> c25(F''(z0))
   MAP''(Cons(z0, z1)) -> c26(MAP''(z1))
   F''(z0) -> c29(*''(z0, z0))
We considered the (Usable) Rules:none
And the Tuples:
   *''(z0, S(S(z1))) -> c11(*''(z0, S(z1)))
   *1(z0, S(S(z1))) -> c15(*1(z0, S(z1)))
   MAP'(Cons(z0, z1)) -> c19(F'(z0), MAP'(z1))
   F'(z0) -> c22(*1(z0, z0))
   +FULL'(S(z0), z1) -> c23(+FULL'(z0, S(z1)))
   MAP''(Cons(z0, z1)) -> c25(F''(z0))
   MAP''(Cons(z0, z1)) -> c26(MAP''(z1))
   F''(z0) -> c29(*''(z0, z0))
   +FULL''(S(z0), z1) -> c30(+FULL''(z0, S(z1)))
The order we found is given by the following interpretation:

Polynomial interpretation :

   POL(*''(x_1, x_2)) = x_2
   POL(*1(x_1, x_2)) = [1] + x_2
   POL(+FULL'(x_1, x_2)) = x_1 + x_2
   POL(+FULL''(x_1, x_2)) = x_1 + x_2
   POL(Cons(x_1, x_2)) = [1] + x_1 + x_2
   POL(F'(x_1)) = [1] + x_1
   POL(F''(x_1)) = [1] + x_1
   POL(MAP'(x_1)) = x_1
   POL(MAP''(x_1)) = [1] + x_1
   POL(S(x_1)) = [1] + x_1
   POL(c11(x_1)) = x_1
   POL(c15(x_1)) = x_1
   POL(c19(x_1, x_2)) = x_1 + x_2
   POL(c22(x_1)) = x_1
   POL(c23(x_1)) = x_1
   POL(c25(x_1)) = x_1
   POL(c26(x_1)) = x_1
   POL(c29(x_1)) = x_1
   POL(c30(x_1)) = x_1

----------------------------------------

(10)
Obligation:
Complexity Dependency Tuples Problem

Rules:none
Tuples:
   *''(z0, S(S(z1))) -> c11(*''(z0, S(z1)))
   *1(z0, S(S(z1))) -> c15(*1(z0, S(z1)))
   MAP'(Cons(z0, z1)) -> c19(F'(z0), MAP'(z1))
   F'(z0) -> c22(*1(z0, z0))
   +FULL'(S(z0), z1) -> c23(+FULL'(z0, S(z1)))
   MAP''(Cons(z0, z1)) -> c25(F''(z0))
   MAP''(Cons(z0, z1)) -> c26(MAP''(z1))
   F''(z0) -> c29(*''(z0, z0))
   +FULL''(S(z0), z1) -> c30(+FULL''(z0, S(z1)))
S tuples:
   +FULL''(S(z0), z1) -> c30(+FULL''(z0, S(z1)))
K tuples:
   MAP''(Cons(z0, z1)) -> c25(F''(z0))
   MAP''(Cons(z0, z1)) -> c26(MAP''(z1))
   F''(z0) -> c29(*''(z0, z0))
Defined Rule Symbols:none

Defined Pair Symbols:   *''_2, *1_2, MAP'_1, F'_1, +FULL'_2, MAP''_1, F''_1, +FULL''_2

Compound Symbols:   c11_1, c15_1, c19_2, c22_1, c23_1, c25_1, c26_1, c29_1, c30_1


----------------------------------------

(11) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)))
Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.
   +FULL''(S(z0), z1) -> c30(+FULL''(z0, S(z1)))
We considered the (Usable) Rules:none
And the Tuples:
   *''(z0, S(S(z1))) -> c11(*''(z0, S(z1)))
   *1(z0, S(S(z1))) -> c15(*1(z0, S(z1)))
   MAP'(Cons(z0, z1)) -> c19(F'(z0), MAP'(z1))
   F'(z0) -> c22(*1(z0, z0))
   +FULL'(S(z0), z1) -> c23(+FULL'(z0, S(z1)))
   MAP''(Cons(z0, z1)) -> c25(F''(z0))
   MAP''(Cons(z0, z1)) -> c26(MAP''(z1))
   F''(z0) -> c29(*''(z0, z0))
   +FULL''(S(z0), z1) -> c30(+FULL''(z0, S(z1)))
The order we found is given by the following interpretation:

Polynomial interpretation :

   POL(*''(x_1, x_2)) = x_2
   POL(*1(x_1, x_2)) = [1] + x_1
   POL(+FULL'(x_1, x_2)) = x_1 + x_2
   POL(+FULL''(x_1, x_2)) = x_1
   POL(Cons(x_1, x_2)) = [1] + x_1 + x_2
   POL(F'(x_1)) = [1] + x_1
   POL(F''(x_1)) = x_1
   POL(MAP'(x_1)) = x_1
   POL(MAP''(x_1)) = [1] + x_1
   POL(S(x_1)) = [1] + x_1
   POL(c11(x_1)) = x_1
   POL(c15(x_1)) = x_1
   POL(c19(x_1, x_2)) = x_1 + x_2
   POL(c22(x_1)) = x_1
   POL(c23(x_1)) = x_1
   POL(c25(x_1)) = x_1
   POL(c26(x_1)) = x_1
   POL(c29(x_1)) = x_1
   POL(c30(x_1)) = x_1

----------------------------------------

(12)
Obligation:
Complexity Dependency Tuples Problem

Rules:none
Tuples:
   *''(z0, S(S(z1))) -> c11(*''(z0, S(z1)))
   *1(z0, S(S(z1))) -> c15(*1(z0, S(z1)))
   MAP'(Cons(z0, z1)) -> c19(F'(z0), MAP'(z1))
   F'(z0) -> c22(*1(z0, z0))
   +FULL'(S(z0), z1) -> c23(+FULL'(z0, S(z1)))
   MAP''(Cons(z0, z1)) -> c25(F''(z0))
   MAP''(Cons(z0, z1)) -> c26(MAP''(z1))
   F''(z0) -> c29(*''(z0, z0))
   +FULL''(S(z0), z1) -> c30(+FULL''(z0, S(z1)))
S tuples:none
K tuples:
   MAP''(Cons(z0, z1)) -> c25(F''(z0))
   MAP''(Cons(z0, z1)) -> c26(MAP''(z1))
   F''(z0) -> c29(*''(z0, z0))
   +FULL''(S(z0), z1) -> c30(+FULL''(z0, S(z1)))
Defined Rule Symbols:none

Defined Pair Symbols:   *''_2, *1_2, MAP'_1, F'_1, +FULL'_2, MAP''_1, F''_1, +FULL''_2

Compound Symbols:   c11_1, c15_1, c19_2, c22_1, c23_1, c25_1, c26_1, c29_1, c30_1


----------------------------------------

(13) SIsEmptyProof (BOTH BOUNDS(ID, ID))
The set S is empty
----------------------------------------

(14)
BOUNDS(1, 1)

----------------------------------------

(15) RelTrsToDecreasingLoopProblemProof (LOWER BOUND(ID))
Transformed a relative TRS into a decreasing-loop problem.
----------------------------------------

(16)
Obligation:
Analyzing the following TRS for decreasing loops:

The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, n^1).


The TRS R consists of the following rules:

   MAP(Cons(z0, z1)) -> c4(F(z0))
   MAP(Cons(z0, z1)) -> c5(MAP(z1))
   MAP(Nil) -> c6
   GOAL(z0) -> c7(MAP(z0))
   F(z0) -> c8(*'(z0, z0))
   +FULL(S(z0), z1) -> c9(+FULL(z0, S(z1)))
   +FULL(0, z0) -> c10

The (relative) TRS S consists of the following rules:

   *'(z0, S(S(z1))) -> c(*'(z0, S(z1)))
   *'(z0, S(0)) -> c1
   *'(z0, 0) -> c2
   *'(0, z0) -> c3
   *(z0, S(S(z1))) -> +(z0, *(z0, S(z1)))
   *(z0, S(0)) -> z0
   *(z0, 0) -> 0
   *(0, z0) -> 0
   map(Cons(z0, z1)) -> Cons(f(z0), map(z1))
   map(Nil) -> Nil
   goal(z0) -> map(z0)
   f(z0) -> *(z0, z0)
   +Full(S(z0), z1) -> +Full(z0, S(z1))
   +Full(0, z0) -> z0

Rewrite Strategy: INNERMOST
----------------------------------------

(17) DecreasingLoopProof (LOWER BOUND(ID))
The following loop(s) give(s) rise to the lower bound Omega(n^1):

The rewrite sequence

MAP(Cons(z0, z1)) ->^+ c5(MAP(z1))

gives rise to a decreasing loop by considering the right hand sides subterm at position [0].

The pumping substitution is [z1 / Cons(z0, z1)].

The result substitution is [ ].




----------------------------------------

(18)
Complex Obligation (BEST)

----------------------------------------

(19)
Obligation:
Proved the lower bound n^1 for the following obligation:

The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, n^1).


The TRS R consists of the following rules:

   MAP(Cons(z0, z1)) -> c4(F(z0))
   MAP(Cons(z0, z1)) -> c5(MAP(z1))
   MAP(Nil) -> c6
   GOAL(z0) -> c7(MAP(z0))
   F(z0) -> c8(*'(z0, z0))
   +FULL(S(z0), z1) -> c9(+FULL(z0, S(z1)))
   +FULL(0, z0) -> c10

The (relative) TRS S consists of the following rules:

   *'(z0, S(S(z1))) -> c(*'(z0, S(z1)))
   *'(z0, S(0)) -> c1
   *'(z0, 0) -> c2
   *'(0, z0) -> c3
   *(z0, S(S(z1))) -> +(z0, *(z0, S(z1)))
   *(z0, S(0)) -> z0
   *(z0, 0) -> 0
   *(0, z0) -> 0
   map(Cons(z0, z1)) -> Cons(f(z0), map(z1))
   map(Nil) -> Nil
   goal(z0) -> map(z0)
   f(z0) -> *(z0, z0)
   +Full(S(z0), z1) -> +Full(z0, S(z1))
   +Full(0, z0) -> z0

Rewrite Strategy: INNERMOST
----------------------------------------

(20) LowerBoundPropagationProof (FINISHED)
Propagated lower bound.
----------------------------------------

(21)
BOUNDS(n^1, INF)

----------------------------------------

(22)
Obligation:
Analyzing the following TRS for decreasing loops:

The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, n^1).


The TRS R consists of the following rules:

   MAP(Cons(z0, z1)) -> c4(F(z0))
   MAP(Cons(z0, z1)) -> c5(MAP(z1))
   MAP(Nil) -> c6
   GOAL(z0) -> c7(MAP(z0))
   F(z0) -> c8(*'(z0, z0))
   +FULL(S(z0), z1) -> c9(+FULL(z0, S(z1)))
   +FULL(0, z0) -> c10

The (relative) TRS S consists of the following rules:

   *'(z0, S(S(z1))) -> c(*'(z0, S(z1)))
   *'(z0, S(0)) -> c1
   *'(z0, 0) -> c2
   *'(0, z0) -> c3
   *(z0, S(S(z1))) -> +(z0, *(z0, S(z1)))
   *(z0, S(0)) -> z0
   *(z0, 0) -> 0
   *(0, z0) -> 0
   map(Cons(z0, z1)) -> Cons(f(z0), map(z1))
   map(Nil) -> Nil
   goal(z0) -> map(z0)
   f(z0) -> *(z0, z0)
   +Full(S(z0), z1) -> +Full(z0, S(z1))
   +Full(0, z0) -> z0

Rewrite Strategy: INNERMOST