WORST_CASE(Omega(n^1),O(n^2))
proof of input_q0tsI1r30D.trs
# AProVE Commit ID: aff8ecad908e01718a4c36e68d2e55d5e0f16e15 fuhs 20220216 unpublished


The Runtime Complexity (parallel-innermost) of the given CpxTRS could be proven to be BOUNDS(n^1, n^2).

(0) CpxTRS
(1) CpxTrsToCdtProof [UPPER BOUND(ID), 0 ms]
(2) CdtProblem
    (3) CdtLeafRemovalProof [BOTH BOUNDS(ID, ID), 0 ms]
    (4) CdtProblem
    (5) CdtRuleRemovalProof [UPPER BOUND(ADD(n^1)), 140 ms]
    (6) CdtProblem
    (7) CdtKnowledgeProof [BOTH BOUNDS(ID, ID), 0 ms]
    (8) CdtProblem
    (9) CdtRuleRemovalProof [UPPER BOUND(ADD(n^2)), 103 ms]
    (10) CdtProblem
    (11) CdtKnowledgeProof [FINISHED, 0 ms]
    (12) BOUNDS(1, 1)
(13) CpxTrsToCdtProof [BOTH BOUNDS(ID, ID), 0 ms]
(14) CdtProblem
    (15) CdtToCpxRelTrsProof [BOTH BOUNDS(ID, ID), 0 ms]
    (16) CpxRelTRS
    (17) RenamingProof [BOTH BOUNDS(ID, ID), 0 ms]
    (18) CpxRelTRS
    (19) TypeInferenceProof [BOTH BOUNDS(ID, ID), 0 ms]
    (20) typed CpxTrs
    (21) OrderProof [LOWER BOUND(ID), 21 ms]
    (22) typed CpxTrs
    (23) RewriteLemmaProof [LOWER BOUND(ID), 246 ms]
    (24) typed CpxTrs
    (25) RewriteLemmaProof [LOWER BOUND(ID), 438 ms]
    (26) typed CpxTrs
    (27) RewriteLemmaProof [LOWER BOUND(ID), 1429 ms]
    (28) BEST
        (29) proven lower bound
            (30) LowerBoundPropagationProof [FINISHED, 0 ms]
            (31) BOUNDS(n^1, INF)
        (32) typed CpxTrs
            (33) RewriteLemmaProof [LOWER BOUND(ID), 504 ms]
            (34) typed CpxTrs
            (35) RewriteLemmaProof [LOWER BOUND(ID), 427 ms]
            (36) BOUNDS(1, INF)


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

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


The TRS R consists of the following rules:

   append(@l1, @l2) -> append#1(@l1, @l2)
   append#1(::(@x, @xs), @l2) -> ::(@x, append(@xs, @l2))
   append#1(nil, @l2) -> @l2
   subtrees(@t) -> subtrees#1(@t)
   subtrees#1(leaf) -> nil
   subtrees#1(node(@x, @t1, @t2)) -> subtrees#2(subtrees(@t1), @t1, @t2, @x)
   subtrees#2(@l1, @t1, @t2, @x) -> subtrees#3(subtrees(@t2), @l1, @t1, @t2, @x)
   subtrees#3(@l2, @l1, @t1, @t2, @x) -> ::(node(@x, @t1, @t2), append(@l1, @l2))

S is empty.
Rewrite Strategy: PARALLEL_INNERMOST
----------------------------------------

(1) CpxTrsToCdtProof (UPPER BOUND(ID))
Converted Cpx (relative) TRS with rewrite strategy PARALLEL_INNERMOST to CDT
----------------------------------------

(2)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   append(z0, z1) -> append#1(z0, z1)
   append#1(::(z0, z1), z2) -> ::(z0, append(z1, z2))
   append#1(nil, z0) -> z0
   subtrees(z0) -> subtrees#1(z0)
   subtrees#1(leaf) -> nil
   subtrees#1(node(z0, z1, z2)) -> subtrees#2(subtrees(z1), z1, z2, z0)
   subtrees#2(z0, z1, z2, z3) -> subtrees#3(subtrees(z2), z0, z1, z2, z3)
   subtrees#3(z0, z1, z2, z3, z4) -> ::(node(z4, z2, z3), append(z1, z0))
Tuples:
   APPEND(z0, z1) -> c(APPEND#1(z0, z1))
   APPEND#1(::(z0, z1), z2) -> c1(APPEND(z1, z2))
   APPEND#1(nil, z0) -> c2
   SUBTREES(z0) -> c3(SUBTREES#1(z0))
   SUBTREES#1(leaf) -> c4
   SUBTREES#1(node(z0, z1, z2)) -> c5(SUBTREES#2(subtrees(z1), z1, z2, z0), SUBTREES(z1))
   SUBTREES#2(z0, z1, z2, z3) -> c6(SUBTREES#3(subtrees(z2), z0, z1, z2, z3), SUBTREES(z2))
   SUBTREES#3(z0, z1, z2, z3, z4) -> c7(APPEND(z1, z0))
S tuples:
   APPEND(z0, z1) -> c(APPEND#1(z0, z1))
   APPEND#1(::(z0, z1), z2) -> c1(APPEND(z1, z2))
   APPEND#1(nil, z0) -> c2
   SUBTREES(z0) -> c3(SUBTREES#1(z0))
   SUBTREES#1(leaf) -> c4
   SUBTREES#1(node(z0, z1, z2)) -> c5(SUBTREES#2(subtrees(z1), z1, z2, z0), SUBTREES(z1))
   SUBTREES#2(z0, z1, z2, z3) -> c6(SUBTREES#3(subtrees(z2), z0, z1, z2, z3), SUBTREES(z2))
   SUBTREES#3(z0, z1, z2, z3, z4) -> c7(APPEND(z1, z0))
K tuples:none
Defined Rule Symbols:   append_2, append#1_2, subtrees_1, subtrees#1_1, subtrees#2_4, subtrees#3_5

Defined Pair Symbols:   APPEND_2, APPEND#1_2, SUBTREES_1, SUBTREES#1_1, SUBTREES#2_4, SUBTREES#3_5

Compound Symbols:   c_1, c1_1, c2, c3_1, c4, c5_2, c6_2, c7_1


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

(3) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID))
Removed 2 trailing nodes:
   APPEND#1(nil, z0) -> c2
   SUBTREES#1(leaf) -> c4

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

(4)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   append(z0, z1) -> append#1(z0, z1)
   append#1(::(z0, z1), z2) -> ::(z0, append(z1, z2))
   append#1(nil, z0) -> z0
   subtrees(z0) -> subtrees#1(z0)
   subtrees#1(leaf) -> nil
   subtrees#1(node(z0, z1, z2)) -> subtrees#2(subtrees(z1), z1, z2, z0)
   subtrees#2(z0, z1, z2, z3) -> subtrees#3(subtrees(z2), z0, z1, z2, z3)
   subtrees#3(z0, z1, z2, z3, z4) -> ::(node(z4, z2, z3), append(z1, z0))
Tuples:
   APPEND(z0, z1) -> c(APPEND#1(z0, z1))
   APPEND#1(::(z0, z1), z2) -> c1(APPEND(z1, z2))
   SUBTREES(z0) -> c3(SUBTREES#1(z0))
   SUBTREES#1(node(z0, z1, z2)) -> c5(SUBTREES#2(subtrees(z1), z1, z2, z0), SUBTREES(z1))
   SUBTREES#2(z0, z1, z2, z3) -> c6(SUBTREES#3(subtrees(z2), z0, z1, z2, z3), SUBTREES(z2))
   SUBTREES#3(z0, z1, z2, z3, z4) -> c7(APPEND(z1, z0))
S tuples:
   APPEND(z0, z1) -> c(APPEND#1(z0, z1))
   APPEND#1(::(z0, z1), z2) -> c1(APPEND(z1, z2))
   SUBTREES(z0) -> c3(SUBTREES#1(z0))
   SUBTREES#1(node(z0, z1, z2)) -> c5(SUBTREES#2(subtrees(z1), z1, z2, z0), SUBTREES(z1))
   SUBTREES#2(z0, z1, z2, z3) -> c6(SUBTREES#3(subtrees(z2), z0, z1, z2, z3), SUBTREES(z2))
   SUBTREES#3(z0, z1, z2, z3, z4) -> c7(APPEND(z1, z0))
K tuples:none
Defined Rule Symbols:   append_2, append#1_2, subtrees_1, subtrees#1_1, subtrees#2_4, subtrees#3_5

Defined Pair Symbols:   APPEND_2, APPEND#1_2, SUBTREES_1, SUBTREES#1_1, SUBTREES#2_4, SUBTREES#3_5

Compound Symbols:   c_1, c1_1, c3_1, c5_2, c6_2, c7_1


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

(5) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)))
Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.
   SUBTREES#1(node(z0, z1, z2)) -> c5(SUBTREES#2(subtrees(z1), z1, z2, z0), SUBTREES(z1))
We considered the (Usable) Rules:none
And the Tuples:
   APPEND(z0, z1) -> c(APPEND#1(z0, z1))
   APPEND#1(::(z0, z1), z2) -> c1(APPEND(z1, z2))
   SUBTREES(z0) -> c3(SUBTREES#1(z0))
   SUBTREES#1(node(z0, z1, z2)) -> c5(SUBTREES#2(subtrees(z1), z1, z2, z0), SUBTREES(z1))
   SUBTREES#2(z0, z1, z2, z3) -> c6(SUBTREES#3(subtrees(z2), z0, z1, z2, z3), SUBTREES(z2))
   SUBTREES#3(z0, z1, z2, z3, z4) -> c7(APPEND(z1, z0))
The order we found is given by the following interpretation:

Polynomial interpretation :

   POL(::(x_1, x_2)) = [2]
   POL(APPEND(x_1, x_2)) = 0
   POL(APPEND#1(x_1, x_2)) = 0
   POL(SUBTREES(x_1)) = [2]x_1
   POL(SUBTREES#1(x_1)) = [2]x_1
   POL(SUBTREES#2(x_1, x_2, x_3, x_4)) = [2]x_3 + [2]x_4
   POL(SUBTREES#3(x_1, x_2, x_3, x_4, x_5)) = [2]x_5
   POL(append(x_1, x_2)) = [3]x_1 + [3]x_2
   POL(append#1(x_1, x_2)) = [2]x_1 + [3]x_2
   POL(c(x_1)) = x_1
   POL(c1(x_1)) = x_1
   POL(c3(x_1)) = x_1
   POL(c5(x_1, x_2)) = x_1 + x_2
   POL(c6(x_1, x_2)) = x_1 + x_2
   POL(c7(x_1)) = x_1
   POL(leaf) = [3]
   POL(nil) = [3]
   POL(node(x_1, x_2, x_3)) = [1] + x_1 + x_2 + x_3
   POL(subtrees(x_1)) = 0
   POL(subtrees#1(x_1)) = [3] + [3]x_1
   POL(subtrees#2(x_1, x_2, x_3, x_4)) = [3] + [3]x_1 + [3]x_2 + [3]x_3 + [3]x_4
   POL(subtrees#3(x_1, x_2, x_3, x_4, x_5)) = [3] + [3]x_1 + [3]x_2 + [3]x_3 + [3]x_4 + [3]x_5

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

(6)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   append(z0, z1) -> append#1(z0, z1)
   append#1(::(z0, z1), z2) -> ::(z0, append(z1, z2))
   append#1(nil, z0) -> z0
   subtrees(z0) -> subtrees#1(z0)
   subtrees#1(leaf) -> nil
   subtrees#1(node(z0, z1, z2)) -> subtrees#2(subtrees(z1), z1, z2, z0)
   subtrees#2(z0, z1, z2, z3) -> subtrees#3(subtrees(z2), z0, z1, z2, z3)
   subtrees#3(z0, z1, z2, z3, z4) -> ::(node(z4, z2, z3), append(z1, z0))
Tuples:
   APPEND(z0, z1) -> c(APPEND#1(z0, z1))
   APPEND#1(::(z0, z1), z2) -> c1(APPEND(z1, z2))
   SUBTREES(z0) -> c3(SUBTREES#1(z0))
   SUBTREES#1(node(z0, z1, z2)) -> c5(SUBTREES#2(subtrees(z1), z1, z2, z0), SUBTREES(z1))
   SUBTREES#2(z0, z1, z2, z3) -> c6(SUBTREES#3(subtrees(z2), z0, z1, z2, z3), SUBTREES(z2))
   SUBTREES#3(z0, z1, z2, z3, z4) -> c7(APPEND(z1, z0))
S tuples:
   APPEND(z0, z1) -> c(APPEND#1(z0, z1))
   APPEND#1(::(z0, z1), z2) -> c1(APPEND(z1, z2))
   SUBTREES(z0) -> c3(SUBTREES#1(z0))
   SUBTREES#2(z0, z1, z2, z3) -> c6(SUBTREES#3(subtrees(z2), z0, z1, z2, z3), SUBTREES(z2))
   SUBTREES#3(z0, z1, z2, z3, z4) -> c7(APPEND(z1, z0))
K tuples:
   SUBTREES#1(node(z0, z1, z2)) -> c5(SUBTREES#2(subtrees(z1), z1, z2, z0), SUBTREES(z1))
Defined Rule Symbols:   append_2, append#1_2, subtrees_1, subtrees#1_1, subtrees#2_4, subtrees#3_5

Defined Pair Symbols:   APPEND_2, APPEND#1_2, SUBTREES_1, SUBTREES#1_1, SUBTREES#2_4, SUBTREES#3_5

Compound Symbols:   c_1, c1_1, c3_1, c5_2, c6_2, c7_1


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

(7) CdtKnowledgeProof (BOTH BOUNDS(ID, ID))
The following tuples could be moved from S to K by knowledge propagation:
   SUBTREES#2(z0, z1, z2, z3) -> c6(SUBTREES#3(subtrees(z2), z0, z1, z2, z3), SUBTREES(z2))
   SUBTREES#3(z0, z1, z2, z3, z4) -> c7(APPEND(z1, z0))
   SUBTREES#3(z0, z1, z2, z3, z4) -> c7(APPEND(z1, z0))
   SUBTREES(z0) -> c3(SUBTREES#1(z0))
   SUBTREES#1(node(z0, z1, z2)) -> c5(SUBTREES#2(subtrees(z1), z1, z2, z0), SUBTREES(z1))

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

(8)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   append(z0, z1) -> append#1(z0, z1)
   append#1(::(z0, z1), z2) -> ::(z0, append(z1, z2))
   append#1(nil, z0) -> z0
   subtrees(z0) -> subtrees#1(z0)
   subtrees#1(leaf) -> nil
   subtrees#1(node(z0, z1, z2)) -> subtrees#2(subtrees(z1), z1, z2, z0)
   subtrees#2(z0, z1, z2, z3) -> subtrees#3(subtrees(z2), z0, z1, z2, z3)
   subtrees#3(z0, z1, z2, z3, z4) -> ::(node(z4, z2, z3), append(z1, z0))
Tuples:
   APPEND(z0, z1) -> c(APPEND#1(z0, z1))
   APPEND#1(::(z0, z1), z2) -> c1(APPEND(z1, z2))
   SUBTREES(z0) -> c3(SUBTREES#1(z0))
   SUBTREES#1(node(z0, z1, z2)) -> c5(SUBTREES#2(subtrees(z1), z1, z2, z0), SUBTREES(z1))
   SUBTREES#2(z0, z1, z2, z3) -> c6(SUBTREES#3(subtrees(z2), z0, z1, z2, z3), SUBTREES(z2))
   SUBTREES#3(z0, z1, z2, z3, z4) -> c7(APPEND(z1, z0))
S tuples:
   APPEND(z0, z1) -> c(APPEND#1(z0, z1))
   APPEND#1(::(z0, z1), z2) -> c1(APPEND(z1, z2))
K tuples:
   SUBTREES#1(node(z0, z1, z2)) -> c5(SUBTREES#2(subtrees(z1), z1, z2, z0), SUBTREES(z1))
   SUBTREES#2(z0, z1, z2, z3) -> c6(SUBTREES#3(subtrees(z2), z0, z1, z2, z3), SUBTREES(z2))
   SUBTREES#3(z0, z1, z2, z3, z4) -> c7(APPEND(z1, z0))
   SUBTREES(z0) -> c3(SUBTREES#1(z0))
Defined Rule Symbols:   append_2, append#1_2, subtrees_1, subtrees#1_1, subtrees#2_4, subtrees#3_5

Defined Pair Symbols:   APPEND_2, APPEND#1_2, SUBTREES_1, SUBTREES#1_1, SUBTREES#2_4, SUBTREES#3_5

Compound Symbols:   c_1, c1_1, c3_1, c5_2, c6_2, c7_1


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

(9) CdtRuleRemovalProof (UPPER BOUND(ADD(n^2)))
Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.
   APPEND#1(::(z0, z1), z2) -> c1(APPEND(z1, z2))
We considered the (Usable) Rules:
   subtrees#3(z0, z1, z2, z3, z4) -> ::(node(z4, z2, z3), append(z1, z0))
   subtrees#2(z0, z1, z2, z3) -> subtrees#3(subtrees(z2), z0, z1, z2, z3)
   append(z0, z1) -> append#1(z0, z1)
   append#1(nil, z0) -> z0
   subtrees(z0) -> subtrees#1(z0)
   subtrees#1(node(z0, z1, z2)) -> subtrees#2(subtrees(z1), z1, z2, z0)
   subtrees#1(leaf) -> nil
   append#1(::(z0, z1), z2) -> ::(z0, append(z1, z2))
And the Tuples:
   APPEND(z0, z1) -> c(APPEND#1(z0, z1))
   APPEND#1(::(z0, z1), z2) -> c1(APPEND(z1, z2))
   SUBTREES(z0) -> c3(SUBTREES#1(z0))
   SUBTREES#1(node(z0, z1, z2)) -> c5(SUBTREES#2(subtrees(z1), z1, z2, z0), SUBTREES(z1))
   SUBTREES#2(z0, z1, z2, z3) -> c6(SUBTREES#3(subtrees(z2), z0, z1, z2, z3), SUBTREES(z2))
   SUBTREES#3(z0, z1, z2, z3, z4) -> c7(APPEND(z1, z0))
The order we found is given by the following interpretation:

Polynomial interpretation :

   POL(::(x_1, x_2)) = [2] + x_2
   POL(APPEND(x_1, x_2)) = [2]x_1
   POL(APPEND#1(x_1, x_2)) = [2]x_1
   POL(SUBTREES(x_1)) = x_1^2
   POL(SUBTREES#1(x_1)) = x_1^2
   POL(SUBTREES#2(x_1, x_2, x_3, x_4)) = [2]x_1 + x_3^2 + [2]x_2*x_3
   POL(SUBTREES#3(x_1, x_2, x_3, x_4, x_5)) = [2]x_2 + x_3*x_4
   POL(append(x_1, x_2)) = x_1 + x_2
   POL(append#1(x_1, x_2)) = x_1 + x_2
   POL(c(x_1)) = x_1
   POL(c1(x_1)) = x_1
   POL(c3(x_1)) = x_1
   POL(c5(x_1, x_2)) = x_1 + x_2
   POL(c6(x_1, x_2)) = x_1 + x_2
   POL(c7(x_1)) = x_1
   POL(leaf) = 0
   POL(nil) = 0
   POL(node(x_1, x_2, x_3)) = [2] + x_2 + x_3
   POL(subtrees(x_1)) = [2]x_1
   POL(subtrees#1(x_1)) = [2]x_1
   POL(subtrees#2(x_1, x_2, x_3, x_4)) = [2] + x_1 + [2]x_3
   POL(subtrees#3(x_1, x_2, x_3, x_4, x_5)) = [2] + x_1 + x_2

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

(10)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   append(z0, z1) -> append#1(z0, z1)
   append#1(::(z0, z1), z2) -> ::(z0, append(z1, z2))
   append#1(nil, z0) -> z0
   subtrees(z0) -> subtrees#1(z0)
   subtrees#1(leaf) -> nil
   subtrees#1(node(z0, z1, z2)) -> subtrees#2(subtrees(z1), z1, z2, z0)
   subtrees#2(z0, z1, z2, z3) -> subtrees#3(subtrees(z2), z0, z1, z2, z3)
   subtrees#3(z0, z1, z2, z3, z4) -> ::(node(z4, z2, z3), append(z1, z0))
Tuples:
   APPEND(z0, z1) -> c(APPEND#1(z0, z1))
   APPEND#1(::(z0, z1), z2) -> c1(APPEND(z1, z2))
   SUBTREES(z0) -> c3(SUBTREES#1(z0))
   SUBTREES#1(node(z0, z1, z2)) -> c5(SUBTREES#2(subtrees(z1), z1, z2, z0), SUBTREES(z1))
   SUBTREES#2(z0, z1, z2, z3) -> c6(SUBTREES#3(subtrees(z2), z0, z1, z2, z3), SUBTREES(z2))
   SUBTREES#3(z0, z1, z2, z3, z4) -> c7(APPEND(z1, z0))
S tuples:
   APPEND(z0, z1) -> c(APPEND#1(z0, z1))
K tuples:
   SUBTREES#1(node(z0, z1, z2)) -> c5(SUBTREES#2(subtrees(z1), z1, z2, z0), SUBTREES(z1))
   SUBTREES#2(z0, z1, z2, z3) -> c6(SUBTREES#3(subtrees(z2), z0, z1, z2, z3), SUBTREES(z2))
   SUBTREES#3(z0, z1, z2, z3, z4) -> c7(APPEND(z1, z0))
   SUBTREES(z0) -> c3(SUBTREES#1(z0))
   APPEND#1(::(z0, z1), z2) -> c1(APPEND(z1, z2))
Defined Rule Symbols:   append_2, append#1_2, subtrees_1, subtrees#1_1, subtrees#2_4, subtrees#3_5

Defined Pair Symbols:   APPEND_2, APPEND#1_2, SUBTREES_1, SUBTREES#1_1, SUBTREES#2_4, SUBTREES#3_5

Compound Symbols:   c_1, c1_1, c3_1, c5_2, c6_2, c7_1


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

(11) CdtKnowledgeProof (FINISHED)
The following tuples could be moved from S to K by knowledge propagation:
   APPEND(z0, z1) -> c(APPEND#1(z0, z1))
   APPEND#1(::(z0, z1), z2) -> c1(APPEND(z1, z2))
Now S is empty
----------------------------------------

(12)
BOUNDS(1, 1)

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

(13) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID))
Converted Cpx (relative) TRS with rewrite strategy PARALLEL_INNERMOST to CDT
----------------------------------------

(14)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   append(z0, z1) -> append#1(z0, z1)
   append#1(::(z0, z1), z2) -> ::(z0, append(z1, z2))
   append#1(nil, z0) -> z0
   subtrees(z0) -> subtrees#1(z0)
   subtrees#1(leaf) -> nil
   subtrees#1(node(z0, z1, z2)) -> subtrees#2(subtrees(z1), z1, z2, z0)
   subtrees#2(z0, z1, z2, z3) -> subtrees#3(subtrees(z2), z0, z1, z2, z3)
   subtrees#3(z0, z1, z2, z3, z4) -> ::(node(z4, z2, z3), append(z1, z0))
Tuples:
   APPEND(z0, z1) -> c(APPEND#1(z0, z1))
   APPEND#1(::(z0, z1), z2) -> c1(APPEND(z1, z2))
   APPEND#1(nil, z0) -> c2
   SUBTREES(z0) -> c3(SUBTREES#1(z0))
   SUBTREES#1(leaf) -> c4
   SUBTREES#1(node(z0, z1, z2)) -> c5(SUBTREES#2(subtrees(z1), z1, z2, z0), SUBTREES(z1))
   SUBTREES#2(z0, z1, z2, z3) -> c6(SUBTREES#3(subtrees(z2), z0, z1, z2, z3), SUBTREES(z2))
   SUBTREES#3(z0, z1, z2, z3, z4) -> c7(APPEND(z1, z0))
S tuples:
   APPEND(z0, z1) -> c(APPEND#1(z0, z1))
   APPEND#1(::(z0, z1), z2) -> c1(APPEND(z1, z2))
   APPEND#1(nil, z0) -> c2
   SUBTREES(z0) -> c3(SUBTREES#1(z0))
   SUBTREES#1(leaf) -> c4
   SUBTREES#1(node(z0, z1, z2)) -> c5(SUBTREES#2(subtrees(z1), z1, z2, z0), SUBTREES(z1))
   SUBTREES#2(z0, z1, z2, z3) -> c6(SUBTREES#3(subtrees(z2), z0, z1, z2, z3), SUBTREES(z2))
   SUBTREES#3(z0, z1, z2, z3, z4) -> c7(APPEND(z1, z0))
K tuples:none
Defined Rule Symbols:   append_2, append#1_2, subtrees_1, subtrees#1_1, subtrees#2_4, subtrees#3_5

Defined Pair Symbols:   APPEND_2, APPEND#1_2, SUBTREES_1, SUBTREES#1_1, SUBTREES#2_4, SUBTREES#3_5

Compound Symbols:   c_1, c1_1, c2, c3_1, c4, c5_2, c6_2, c7_1


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

(15) CdtToCpxRelTrsProof (BOTH BOUNDS(ID, ID))
Converted S to standard rules, and D \ S as well as R to relative rules.
----------------------------------------

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


The TRS R consists of the following rules:

   APPEND(z0, z1) -> c(APPEND#1(z0, z1))
   APPEND#1(::(z0, z1), z2) -> c1(APPEND(z1, z2))
   APPEND#1(nil, z0) -> c2
   SUBTREES(z0) -> c3(SUBTREES#1(z0))
   SUBTREES#1(leaf) -> c4
   SUBTREES#1(node(z0, z1, z2)) -> c5(SUBTREES#2(subtrees(z1), z1, z2, z0), SUBTREES(z1))
   SUBTREES#2(z0, z1, z2, z3) -> c6(SUBTREES#3(subtrees(z2), z0, z1, z2, z3), SUBTREES(z2))
   SUBTREES#3(z0, z1, z2, z3, z4) -> c7(APPEND(z1, z0))

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

   append(z0, z1) -> append#1(z0, z1)
   append#1(::(z0, z1), z2) -> ::(z0, append(z1, z2))
   append#1(nil, z0) -> z0
   subtrees(z0) -> subtrees#1(z0)
   subtrees#1(leaf) -> nil
   subtrees#1(node(z0, z1, z2)) -> subtrees#2(subtrees(z1), z1, z2, z0)
   subtrees#2(z0, z1, z2, z3) -> subtrees#3(subtrees(z2), z0, z1, z2, z3)
   subtrees#3(z0, z1, z2, z3, z4) -> ::(node(z4, z2, z3), append(z1, z0))

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

(17) RenamingProof (BOTH BOUNDS(ID, ID))
Renamed function symbols to avoid clashes with predefined symbol.
----------------------------------------

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


The TRS R consists of the following rules:

   APPEND(z0, z1) -> c(APPEND#1(z0, z1))
   APPEND#1(::(z0, z1), z2) -> c1(APPEND(z1, z2))
   APPEND#1(nil, z0) -> c2
   SUBTREES(z0) -> c3(SUBTREES#1(z0))
   SUBTREES#1(leaf) -> c4
   SUBTREES#1(node(z0, z1, z2)) -> c5(SUBTREES#2(subtrees(z1), z1, z2, z0), SUBTREES(z1))
   SUBTREES#2(z0, z1, z2, z3) -> c6(SUBTREES#3(subtrees(z2), z0, z1, z2, z3), SUBTREES(z2))
   SUBTREES#3(z0, z1, z2, z3, z4) -> c7(APPEND(z1, z0))

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

   append(z0, z1) -> append#1(z0, z1)
   append#1(::(z0, z1), z2) -> ::(z0, append(z1, z2))
   append#1(nil, z0) -> z0
   subtrees(z0) -> subtrees#1(z0)
   subtrees#1(leaf) -> nil
   subtrees#1(node(z0, z1, z2)) -> subtrees#2(subtrees(z1), z1, z2, z0)
   subtrees#2(z0, z1, z2, z3) -> subtrees#3(subtrees(z2), z0, z1, z2, z3)
   subtrees#3(z0, z1, z2, z3, z4) -> ::(node(z4, z2, z3), append(z1, z0))

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

(19) TypeInferenceProof (BOTH BOUNDS(ID, ID))
Inferred types.
----------------------------------------

(20)
Obligation:
Innermost TRS:
Rules:
APPEND(z0, z1) -> c(APPEND#1(z0, z1))
APPEND#1(::(z0, z1), z2) -> c1(APPEND(z1, z2))
APPEND#1(nil, z0) -> c2
SUBTREES(z0) -> c3(SUBTREES#1(z0))
SUBTREES#1(leaf) -> c4
SUBTREES#1(node(z0, z1, z2)) -> c5(SUBTREES#2(subtrees(z1), z1, z2, z0), SUBTREES(z1))
SUBTREES#2(z0, z1, z2, z3) -> c6(SUBTREES#3(subtrees(z2), z0, z1, z2, z3), SUBTREES(z2))
SUBTREES#3(z0, z1, z2, z3, z4) -> c7(APPEND(z1, z0))
append(z0, z1) -> append#1(z0, z1)
append#1(::(z0, z1), z2) -> ::(z0, append(z1, z2))
append#1(nil, z0) -> z0
subtrees(z0) -> subtrees#1(z0)
subtrees#1(leaf) -> nil
subtrees#1(node(z0, z1, z2)) -> subtrees#2(subtrees(z1), z1, z2, z0)
subtrees#2(z0, z1, z2, z3) -> subtrees#3(subtrees(z2), z0, z1, z2, z3)
subtrees#3(z0, z1, z2, z3, z4) -> ::(node(z4, z2, z3), append(z1, z0))

Types:
APPEND :: :::nil -> :::nil -> c
c :: c1:c2 -> c
APPEND#1 :: :::nil -> :::nil -> c1:c2
:: :: leaf:node -> :::nil -> :::nil
c1 :: c -> c1:c2
nil :: :::nil
c2 :: c1:c2
SUBTREES :: leaf:node -> c3
c3 :: c4:c5 -> c3
SUBTREES#1 :: leaf:node -> c4:c5
leaf :: leaf:node
c4 :: c4:c5
node :: a -> leaf:node -> leaf:node -> leaf:node
c5 :: c6 -> c3 -> c4:c5
SUBTREES#2 :: :::nil -> leaf:node -> leaf:node -> a -> c6
subtrees :: leaf:node -> :::nil
c6 :: c7 -> c3 -> c6
SUBTREES#3 :: :::nil -> :::nil -> leaf:node -> leaf:node -> a -> c7
c7 :: c -> c7
append :: :::nil -> :::nil -> :::nil
append#1 :: :::nil -> :::nil -> :::nil
subtrees#1 :: leaf:node -> :::nil
subtrees#2 :: :::nil -> leaf:node -> leaf:node -> a -> :::nil
subtrees#3 :: :::nil -> :::nil -> leaf:node -> leaf:node -> a -> :::nil
hole_c1_8 :: c
hole_:::nil2_8 :: :::nil
hole_c1:c23_8 :: c1:c2
hole_leaf:node4_8 :: leaf:node
hole_c35_8 :: c3
hole_c4:c56_8 :: c4:c5
hole_a7_8 :: a
hole_c68_8 :: c6
hole_c79_8 :: c7
gen_:::nil10_8 :: Nat -> :::nil
gen_leaf:node11_8 :: Nat -> leaf:node

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

(21) OrderProof (LOWER BOUND(ID))
Heuristically decided to analyse the following defined symbols:
APPEND, APPEND#1, SUBTREES, SUBTREES#1, subtrees, append, append#1, subtrees#1

They will be analysed ascendingly in the following order:
APPEND = APPEND#1
SUBTREES = SUBTREES#1
subtrees < SUBTREES#1
subtrees = subtrees#1
append = append#1

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

(22)
Obligation:
Innermost TRS:
Rules:
APPEND(z0, z1) -> c(APPEND#1(z0, z1))
APPEND#1(::(z0, z1), z2) -> c1(APPEND(z1, z2))
APPEND#1(nil, z0) -> c2
SUBTREES(z0) -> c3(SUBTREES#1(z0))
SUBTREES#1(leaf) -> c4
SUBTREES#1(node(z0, z1, z2)) -> c5(SUBTREES#2(subtrees(z1), z1, z2, z0), SUBTREES(z1))
SUBTREES#2(z0, z1, z2, z3) -> c6(SUBTREES#3(subtrees(z2), z0, z1, z2, z3), SUBTREES(z2))
SUBTREES#3(z0, z1, z2, z3, z4) -> c7(APPEND(z1, z0))
append(z0, z1) -> append#1(z0, z1)
append#1(::(z0, z1), z2) -> ::(z0, append(z1, z2))
append#1(nil, z0) -> z0
subtrees(z0) -> subtrees#1(z0)
subtrees#1(leaf) -> nil
subtrees#1(node(z0, z1, z2)) -> subtrees#2(subtrees(z1), z1, z2, z0)
subtrees#2(z0, z1, z2, z3) -> subtrees#3(subtrees(z2), z0, z1, z2, z3)
subtrees#3(z0, z1, z2, z3, z4) -> ::(node(z4, z2, z3), append(z1, z0))

Types:
APPEND :: :::nil -> :::nil -> c
c :: c1:c2 -> c
APPEND#1 :: :::nil -> :::nil -> c1:c2
:: :: leaf:node -> :::nil -> :::nil
c1 :: c -> c1:c2
nil :: :::nil
c2 :: c1:c2
SUBTREES :: leaf:node -> c3
c3 :: c4:c5 -> c3
SUBTREES#1 :: leaf:node -> c4:c5
leaf :: leaf:node
c4 :: c4:c5
node :: a -> leaf:node -> leaf:node -> leaf:node
c5 :: c6 -> c3 -> c4:c5
SUBTREES#2 :: :::nil -> leaf:node -> leaf:node -> a -> c6
subtrees :: leaf:node -> :::nil
c6 :: c7 -> c3 -> c6
SUBTREES#3 :: :::nil -> :::nil -> leaf:node -> leaf:node -> a -> c7
c7 :: c -> c7
append :: :::nil -> :::nil -> :::nil
append#1 :: :::nil -> :::nil -> :::nil
subtrees#1 :: leaf:node -> :::nil
subtrees#2 :: :::nil -> leaf:node -> leaf:node -> a -> :::nil
subtrees#3 :: :::nil -> :::nil -> leaf:node -> leaf:node -> a -> :::nil
hole_c1_8 :: c
hole_:::nil2_8 :: :::nil
hole_c1:c23_8 :: c1:c2
hole_leaf:node4_8 :: leaf:node
hole_c35_8 :: c3
hole_c4:c56_8 :: c4:c5
hole_a7_8 :: a
hole_c68_8 :: c6
hole_c79_8 :: c7
gen_:::nil10_8 :: Nat -> :::nil
gen_leaf:node11_8 :: Nat -> leaf:node


Generator Equations:
gen_:::nil10_8(0) <=> nil
gen_:::nil10_8(+(x, 1)) <=> ::(leaf, gen_:::nil10_8(x))
gen_leaf:node11_8(0) <=> leaf
gen_leaf:node11_8(+(x, 1)) <=> node(hole_a7_8, leaf, gen_leaf:node11_8(x))


The following defined symbols remain to be analysed:
append#1, APPEND, APPEND#1, SUBTREES, SUBTREES#1, subtrees, append, subtrees#1

They will be analysed ascendingly in the following order:
APPEND = APPEND#1
SUBTREES = SUBTREES#1
subtrees < SUBTREES#1
subtrees = subtrees#1
append = append#1

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

(23) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
append#1(gen_:::nil10_8(n13_8), gen_:::nil10_8(b)) -> gen_:::nil10_8(+(n13_8, b)), rt in Omega(0)

Induction Base:
append#1(gen_:::nil10_8(0), gen_:::nil10_8(b)) ->_R^Omega(0)
gen_:::nil10_8(b)

Induction Step:
append#1(gen_:::nil10_8(+(n13_8, 1)), gen_:::nil10_8(b)) ->_R^Omega(0)
::(leaf, append(gen_:::nil10_8(n13_8), gen_:::nil10_8(b))) ->_R^Omega(0)
::(leaf, append#1(gen_:::nil10_8(n13_8), gen_:::nil10_8(b))) ->_IH
::(leaf, gen_:::nil10_8(+(b, c14_8)))

We have rt in Omega(1) and sz in O(n). Thus, we have irc_R in Omega(n^0).
----------------------------------------

(24)
Obligation:
Innermost TRS:
Rules:
APPEND(z0, z1) -> c(APPEND#1(z0, z1))
APPEND#1(::(z0, z1), z2) -> c1(APPEND(z1, z2))
APPEND#1(nil, z0) -> c2
SUBTREES(z0) -> c3(SUBTREES#1(z0))
SUBTREES#1(leaf) -> c4
SUBTREES#1(node(z0, z1, z2)) -> c5(SUBTREES#2(subtrees(z1), z1, z2, z0), SUBTREES(z1))
SUBTREES#2(z0, z1, z2, z3) -> c6(SUBTREES#3(subtrees(z2), z0, z1, z2, z3), SUBTREES(z2))
SUBTREES#3(z0, z1, z2, z3, z4) -> c7(APPEND(z1, z0))
append(z0, z1) -> append#1(z0, z1)
append#1(::(z0, z1), z2) -> ::(z0, append(z1, z2))
append#1(nil, z0) -> z0
subtrees(z0) -> subtrees#1(z0)
subtrees#1(leaf) -> nil
subtrees#1(node(z0, z1, z2)) -> subtrees#2(subtrees(z1), z1, z2, z0)
subtrees#2(z0, z1, z2, z3) -> subtrees#3(subtrees(z2), z0, z1, z2, z3)
subtrees#3(z0, z1, z2, z3, z4) -> ::(node(z4, z2, z3), append(z1, z0))

Types:
APPEND :: :::nil -> :::nil -> c
c :: c1:c2 -> c
APPEND#1 :: :::nil -> :::nil -> c1:c2
:: :: leaf:node -> :::nil -> :::nil
c1 :: c -> c1:c2
nil :: :::nil
c2 :: c1:c2
SUBTREES :: leaf:node -> c3
c3 :: c4:c5 -> c3
SUBTREES#1 :: leaf:node -> c4:c5
leaf :: leaf:node
c4 :: c4:c5
node :: a -> leaf:node -> leaf:node -> leaf:node
c5 :: c6 -> c3 -> c4:c5
SUBTREES#2 :: :::nil -> leaf:node -> leaf:node -> a -> c6
subtrees :: leaf:node -> :::nil
c6 :: c7 -> c3 -> c6
SUBTREES#3 :: :::nil -> :::nil -> leaf:node -> leaf:node -> a -> c7
c7 :: c -> c7
append :: :::nil -> :::nil -> :::nil
append#1 :: :::nil -> :::nil -> :::nil
subtrees#1 :: leaf:node -> :::nil
subtrees#2 :: :::nil -> leaf:node -> leaf:node -> a -> :::nil
subtrees#3 :: :::nil -> :::nil -> leaf:node -> leaf:node -> a -> :::nil
hole_c1_8 :: c
hole_:::nil2_8 :: :::nil
hole_c1:c23_8 :: c1:c2
hole_leaf:node4_8 :: leaf:node
hole_c35_8 :: c3
hole_c4:c56_8 :: c4:c5
hole_a7_8 :: a
hole_c68_8 :: c6
hole_c79_8 :: c7
gen_:::nil10_8 :: Nat -> :::nil
gen_leaf:node11_8 :: Nat -> leaf:node


Lemmas:
append#1(gen_:::nil10_8(n13_8), gen_:::nil10_8(b)) -> gen_:::nil10_8(+(n13_8, b)), rt in Omega(0)


Generator Equations:
gen_:::nil10_8(0) <=> nil
gen_:::nil10_8(+(x, 1)) <=> ::(leaf, gen_:::nil10_8(x))
gen_leaf:node11_8(0) <=> leaf
gen_leaf:node11_8(+(x, 1)) <=> node(hole_a7_8, leaf, gen_leaf:node11_8(x))


The following defined symbols remain to be analysed:
append, APPEND, APPEND#1, SUBTREES, SUBTREES#1, subtrees, subtrees#1

They will be analysed ascendingly in the following order:
APPEND = APPEND#1
SUBTREES = SUBTREES#1
subtrees < SUBTREES#1
subtrees = subtrees#1
append = append#1

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

(25) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
subtrees#1(gen_leaf:node11_8(n804_8)) -> *12_8, rt in Omega(0)

Induction Base:
subtrees#1(gen_leaf:node11_8(0))

Induction Step:
subtrees#1(gen_leaf:node11_8(+(n804_8, 1))) ->_R^Omega(0)
subtrees#2(subtrees(leaf), leaf, gen_leaf:node11_8(n804_8), hole_a7_8) ->_R^Omega(0)
subtrees#2(subtrees#1(leaf), leaf, gen_leaf:node11_8(n804_8), hole_a7_8) ->_R^Omega(0)
subtrees#2(nil, leaf, gen_leaf:node11_8(n804_8), hole_a7_8) ->_R^Omega(0)
subtrees#3(subtrees(gen_leaf:node11_8(n804_8)), nil, leaf, gen_leaf:node11_8(n804_8), hole_a7_8) ->_R^Omega(0)
subtrees#3(subtrees#1(gen_leaf:node11_8(n804_8)), nil, leaf, gen_leaf:node11_8(n804_8), hole_a7_8) ->_IH
subtrees#3(*12_8, nil, leaf, gen_leaf:node11_8(n804_8), hole_a7_8)

We have rt in Omega(1) and sz in O(n). Thus, we have irc_R in Omega(n^0).
----------------------------------------

(26)
Obligation:
Innermost TRS:
Rules:
APPEND(z0, z1) -> c(APPEND#1(z0, z1))
APPEND#1(::(z0, z1), z2) -> c1(APPEND(z1, z2))
APPEND#1(nil, z0) -> c2
SUBTREES(z0) -> c3(SUBTREES#1(z0))
SUBTREES#1(leaf) -> c4
SUBTREES#1(node(z0, z1, z2)) -> c5(SUBTREES#2(subtrees(z1), z1, z2, z0), SUBTREES(z1))
SUBTREES#2(z0, z1, z2, z3) -> c6(SUBTREES#3(subtrees(z2), z0, z1, z2, z3), SUBTREES(z2))
SUBTREES#3(z0, z1, z2, z3, z4) -> c7(APPEND(z1, z0))
append(z0, z1) -> append#1(z0, z1)
append#1(::(z0, z1), z2) -> ::(z0, append(z1, z2))
append#1(nil, z0) -> z0
subtrees(z0) -> subtrees#1(z0)
subtrees#1(leaf) -> nil
subtrees#1(node(z0, z1, z2)) -> subtrees#2(subtrees(z1), z1, z2, z0)
subtrees#2(z0, z1, z2, z3) -> subtrees#3(subtrees(z2), z0, z1, z2, z3)
subtrees#3(z0, z1, z2, z3, z4) -> ::(node(z4, z2, z3), append(z1, z0))

Types:
APPEND :: :::nil -> :::nil -> c
c :: c1:c2 -> c
APPEND#1 :: :::nil -> :::nil -> c1:c2
:: :: leaf:node -> :::nil -> :::nil
c1 :: c -> c1:c2
nil :: :::nil
c2 :: c1:c2
SUBTREES :: leaf:node -> c3
c3 :: c4:c5 -> c3
SUBTREES#1 :: leaf:node -> c4:c5
leaf :: leaf:node
c4 :: c4:c5
node :: a -> leaf:node -> leaf:node -> leaf:node
c5 :: c6 -> c3 -> c4:c5
SUBTREES#2 :: :::nil -> leaf:node -> leaf:node -> a -> c6
subtrees :: leaf:node -> :::nil
c6 :: c7 -> c3 -> c6
SUBTREES#3 :: :::nil -> :::nil -> leaf:node -> leaf:node -> a -> c7
c7 :: c -> c7
append :: :::nil -> :::nil -> :::nil
append#1 :: :::nil -> :::nil -> :::nil
subtrees#1 :: leaf:node -> :::nil
subtrees#2 :: :::nil -> leaf:node -> leaf:node -> a -> :::nil
subtrees#3 :: :::nil -> :::nil -> leaf:node -> leaf:node -> a -> :::nil
hole_c1_8 :: c
hole_:::nil2_8 :: :::nil
hole_c1:c23_8 :: c1:c2
hole_leaf:node4_8 :: leaf:node
hole_c35_8 :: c3
hole_c4:c56_8 :: c4:c5
hole_a7_8 :: a
hole_c68_8 :: c6
hole_c79_8 :: c7
gen_:::nil10_8 :: Nat -> :::nil
gen_leaf:node11_8 :: Nat -> leaf:node


Lemmas:
append#1(gen_:::nil10_8(n13_8), gen_:::nil10_8(b)) -> gen_:::nil10_8(+(n13_8, b)), rt in Omega(0)
subtrees#1(gen_leaf:node11_8(n804_8)) -> *12_8, rt in Omega(0)


Generator Equations:
gen_:::nil10_8(0) <=> nil
gen_:::nil10_8(+(x, 1)) <=> ::(leaf, gen_:::nil10_8(x))
gen_leaf:node11_8(0) <=> leaf
gen_leaf:node11_8(+(x, 1)) <=> node(hole_a7_8, leaf, gen_leaf:node11_8(x))


The following defined symbols remain to be analysed:
subtrees, APPEND, APPEND#1, SUBTREES, SUBTREES#1

They will be analysed ascendingly in the following order:
APPEND = APPEND#1
SUBTREES = SUBTREES#1
subtrees < SUBTREES#1
subtrees = subtrees#1

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

(27) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
APPEND#1(gen_:::nil10_8(+(1, n13082_8)), gen_:::nil10_8(b)) -> *12_8, rt in Omega(n13082_8)

Induction Base:
APPEND#1(gen_:::nil10_8(+(1, 0)), gen_:::nil10_8(b))

Induction Step:
APPEND#1(gen_:::nil10_8(+(1, +(n13082_8, 1))), gen_:::nil10_8(b)) ->_R^Omega(1)
c1(APPEND(gen_:::nil10_8(+(1, n13082_8)), gen_:::nil10_8(b))) ->_R^Omega(1)
c1(c(APPEND#1(gen_:::nil10_8(+(1, n13082_8)), gen_:::nil10_8(b)))) ->_IH
c1(c(*12_8))

We have rt in Omega(n^1) and sz in O(n). Thus, we have irc_R in Omega(n).
----------------------------------------

(28)
Complex Obligation (BEST)

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

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

Innermost TRS:
Rules:
APPEND(z0, z1) -> c(APPEND#1(z0, z1))
APPEND#1(::(z0, z1), z2) -> c1(APPEND(z1, z2))
APPEND#1(nil, z0) -> c2
SUBTREES(z0) -> c3(SUBTREES#1(z0))
SUBTREES#1(leaf) -> c4
SUBTREES#1(node(z0, z1, z2)) -> c5(SUBTREES#2(subtrees(z1), z1, z2, z0), SUBTREES(z1))
SUBTREES#2(z0, z1, z2, z3) -> c6(SUBTREES#3(subtrees(z2), z0, z1, z2, z3), SUBTREES(z2))
SUBTREES#3(z0, z1, z2, z3, z4) -> c7(APPEND(z1, z0))
append(z0, z1) -> append#1(z0, z1)
append#1(::(z0, z1), z2) -> ::(z0, append(z1, z2))
append#1(nil, z0) -> z0
subtrees(z0) -> subtrees#1(z0)
subtrees#1(leaf) -> nil
subtrees#1(node(z0, z1, z2)) -> subtrees#2(subtrees(z1), z1, z2, z0)
subtrees#2(z0, z1, z2, z3) -> subtrees#3(subtrees(z2), z0, z1, z2, z3)
subtrees#3(z0, z1, z2, z3, z4) -> ::(node(z4, z2, z3), append(z1, z0))

Types:
APPEND :: :::nil -> :::nil -> c
c :: c1:c2 -> c
APPEND#1 :: :::nil -> :::nil -> c1:c2
:: :: leaf:node -> :::nil -> :::nil
c1 :: c -> c1:c2
nil :: :::nil
c2 :: c1:c2
SUBTREES :: leaf:node -> c3
c3 :: c4:c5 -> c3
SUBTREES#1 :: leaf:node -> c4:c5
leaf :: leaf:node
c4 :: c4:c5
node :: a -> leaf:node -> leaf:node -> leaf:node
c5 :: c6 -> c3 -> c4:c5
SUBTREES#2 :: :::nil -> leaf:node -> leaf:node -> a -> c6
subtrees :: leaf:node -> :::nil
c6 :: c7 -> c3 -> c6
SUBTREES#3 :: :::nil -> :::nil -> leaf:node -> leaf:node -> a -> c7
c7 :: c -> c7
append :: :::nil -> :::nil -> :::nil
append#1 :: :::nil -> :::nil -> :::nil
subtrees#1 :: leaf:node -> :::nil
subtrees#2 :: :::nil -> leaf:node -> leaf:node -> a -> :::nil
subtrees#3 :: :::nil -> :::nil -> leaf:node -> leaf:node -> a -> :::nil
hole_c1_8 :: c
hole_:::nil2_8 :: :::nil
hole_c1:c23_8 :: c1:c2
hole_leaf:node4_8 :: leaf:node
hole_c35_8 :: c3
hole_c4:c56_8 :: c4:c5
hole_a7_8 :: a
hole_c68_8 :: c6
hole_c79_8 :: c7
gen_:::nil10_8 :: Nat -> :::nil
gen_leaf:node11_8 :: Nat -> leaf:node


Lemmas:
append#1(gen_:::nil10_8(n13_8), gen_:::nil10_8(b)) -> gen_:::nil10_8(+(n13_8, b)), rt in Omega(0)
subtrees#1(gen_leaf:node11_8(n804_8)) -> *12_8, rt in Omega(0)


Generator Equations:
gen_:::nil10_8(0) <=> nil
gen_:::nil10_8(+(x, 1)) <=> ::(leaf, gen_:::nil10_8(x))
gen_leaf:node11_8(0) <=> leaf
gen_leaf:node11_8(+(x, 1)) <=> node(hole_a7_8, leaf, gen_leaf:node11_8(x))


The following defined symbols remain to be analysed:
APPEND#1, APPEND

They will be analysed ascendingly in the following order:
APPEND = APPEND#1

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

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

(31)
BOUNDS(n^1, INF)

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

(32)
Obligation:
Innermost TRS:
Rules:
APPEND(z0, z1) -> c(APPEND#1(z0, z1))
APPEND#1(::(z0, z1), z2) -> c1(APPEND(z1, z2))
APPEND#1(nil, z0) -> c2
SUBTREES(z0) -> c3(SUBTREES#1(z0))
SUBTREES#1(leaf) -> c4
SUBTREES#1(node(z0, z1, z2)) -> c5(SUBTREES#2(subtrees(z1), z1, z2, z0), SUBTREES(z1))
SUBTREES#2(z0, z1, z2, z3) -> c6(SUBTREES#3(subtrees(z2), z0, z1, z2, z3), SUBTREES(z2))
SUBTREES#3(z0, z1, z2, z3, z4) -> c7(APPEND(z1, z0))
append(z0, z1) -> append#1(z0, z1)
append#1(::(z0, z1), z2) -> ::(z0, append(z1, z2))
append#1(nil, z0) -> z0
subtrees(z0) -> subtrees#1(z0)
subtrees#1(leaf) -> nil
subtrees#1(node(z0, z1, z2)) -> subtrees#2(subtrees(z1), z1, z2, z0)
subtrees#2(z0, z1, z2, z3) -> subtrees#3(subtrees(z2), z0, z1, z2, z3)
subtrees#3(z0, z1, z2, z3, z4) -> ::(node(z4, z2, z3), append(z1, z0))

Types:
APPEND :: :::nil -> :::nil -> c
c :: c1:c2 -> c
APPEND#1 :: :::nil -> :::nil -> c1:c2
:: :: leaf:node -> :::nil -> :::nil
c1 :: c -> c1:c2
nil :: :::nil
c2 :: c1:c2
SUBTREES :: leaf:node -> c3
c3 :: c4:c5 -> c3
SUBTREES#1 :: leaf:node -> c4:c5
leaf :: leaf:node
c4 :: c4:c5
node :: a -> leaf:node -> leaf:node -> leaf:node
c5 :: c6 -> c3 -> c4:c5
SUBTREES#2 :: :::nil -> leaf:node -> leaf:node -> a -> c6
subtrees :: leaf:node -> :::nil
c6 :: c7 -> c3 -> c6
SUBTREES#3 :: :::nil -> :::nil -> leaf:node -> leaf:node -> a -> c7
c7 :: c -> c7
append :: :::nil -> :::nil -> :::nil
append#1 :: :::nil -> :::nil -> :::nil
subtrees#1 :: leaf:node -> :::nil
subtrees#2 :: :::nil -> leaf:node -> leaf:node -> a -> :::nil
subtrees#3 :: :::nil -> :::nil -> leaf:node -> leaf:node -> a -> :::nil
hole_c1_8 :: c
hole_:::nil2_8 :: :::nil
hole_c1:c23_8 :: c1:c2
hole_leaf:node4_8 :: leaf:node
hole_c35_8 :: c3
hole_c4:c56_8 :: c4:c5
hole_a7_8 :: a
hole_c68_8 :: c6
hole_c79_8 :: c7
gen_:::nil10_8 :: Nat -> :::nil
gen_leaf:node11_8 :: Nat -> leaf:node


Lemmas:
append#1(gen_:::nil10_8(n13_8), gen_:::nil10_8(b)) -> gen_:::nil10_8(+(n13_8, b)), rt in Omega(0)
subtrees#1(gen_leaf:node11_8(n804_8)) -> *12_8, rt in Omega(0)
APPEND#1(gen_:::nil10_8(+(1, n13082_8)), gen_:::nil10_8(b)) -> *12_8, rt in Omega(n13082_8)


Generator Equations:
gen_:::nil10_8(0) <=> nil
gen_:::nil10_8(+(x, 1)) <=> ::(leaf, gen_:::nil10_8(x))
gen_leaf:node11_8(0) <=> leaf
gen_leaf:node11_8(+(x, 1)) <=> node(hole_a7_8, leaf, gen_leaf:node11_8(x))


The following defined symbols remain to be analysed:
APPEND

They will be analysed ascendingly in the following order:
APPEND = APPEND#1

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

(33) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
APPEND(gen_:::nil10_8(n14715_8), gen_:::nil10_8(b)) -> *12_8, rt in Omega(n14715_8)

Induction Base:
APPEND(gen_:::nil10_8(0), gen_:::nil10_8(b))

Induction Step:
APPEND(gen_:::nil10_8(+(n14715_8, 1)), gen_:::nil10_8(b)) ->_R^Omega(1)
c(APPEND#1(gen_:::nil10_8(+(n14715_8, 1)), gen_:::nil10_8(b))) ->_R^Omega(1)
c(c1(APPEND(gen_:::nil10_8(n14715_8), gen_:::nil10_8(b)))) ->_IH
c(c1(*12_8))

We have rt in Omega(n^1) and sz in O(n). Thus, we have irc_R in Omega(n).
----------------------------------------

(34)
Obligation:
Innermost TRS:
Rules:
APPEND(z0, z1) -> c(APPEND#1(z0, z1))
APPEND#1(::(z0, z1), z2) -> c1(APPEND(z1, z2))
APPEND#1(nil, z0) -> c2
SUBTREES(z0) -> c3(SUBTREES#1(z0))
SUBTREES#1(leaf) -> c4
SUBTREES#1(node(z0, z1, z2)) -> c5(SUBTREES#2(subtrees(z1), z1, z2, z0), SUBTREES(z1))
SUBTREES#2(z0, z1, z2, z3) -> c6(SUBTREES#3(subtrees(z2), z0, z1, z2, z3), SUBTREES(z2))
SUBTREES#3(z0, z1, z2, z3, z4) -> c7(APPEND(z1, z0))
append(z0, z1) -> append#1(z0, z1)
append#1(::(z0, z1), z2) -> ::(z0, append(z1, z2))
append#1(nil, z0) -> z0
subtrees(z0) -> subtrees#1(z0)
subtrees#1(leaf) -> nil
subtrees#1(node(z0, z1, z2)) -> subtrees#2(subtrees(z1), z1, z2, z0)
subtrees#2(z0, z1, z2, z3) -> subtrees#3(subtrees(z2), z0, z1, z2, z3)
subtrees#3(z0, z1, z2, z3, z4) -> ::(node(z4, z2, z3), append(z1, z0))

Types:
APPEND :: :::nil -> :::nil -> c
c :: c1:c2 -> c
APPEND#1 :: :::nil -> :::nil -> c1:c2
:: :: leaf:node -> :::nil -> :::nil
c1 :: c -> c1:c2
nil :: :::nil
c2 :: c1:c2
SUBTREES :: leaf:node -> c3
c3 :: c4:c5 -> c3
SUBTREES#1 :: leaf:node -> c4:c5
leaf :: leaf:node
c4 :: c4:c5
node :: a -> leaf:node -> leaf:node -> leaf:node
c5 :: c6 -> c3 -> c4:c5
SUBTREES#2 :: :::nil -> leaf:node -> leaf:node -> a -> c6
subtrees :: leaf:node -> :::nil
c6 :: c7 -> c3 -> c6
SUBTREES#3 :: :::nil -> :::nil -> leaf:node -> leaf:node -> a -> c7
c7 :: c -> c7
append :: :::nil -> :::nil -> :::nil
append#1 :: :::nil -> :::nil -> :::nil
subtrees#1 :: leaf:node -> :::nil
subtrees#2 :: :::nil -> leaf:node -> leaf:node -> a -> :::nil
subtrees#3 :: :::nil -> :::nil -> leaf:node -> leaf:node -> a -> :::nil
hole_c1_8 :: c
hole_:::nil2_8 :: :::nil
hole_c1:c23_8 :: c1:c2
hole_leaf:node4_8 :: leaf:node
hole_c35_8 :: c3
hole_c4:c56_8 :: c4:c5
hole_a7_8 :: a
hole_c68_8 :: c6
hole_c79_8 :: c7
gen_:::nil10_8 :: Nat -> :::nil
gen_leaf:node11_8 :: Nat -> leaf:node


Lemmas:
append#1(gen_:::nil10_8(n13_8), gen_:::nil10_8(b)) -> gen_:::nil10_8(+(n13_8, b)), rt in Omega(0)
subtrees#1(gen_leaf:node11_8(n804_8)) -> *12_8, rt in Omega(0)
APPEND#1(gen_:::nil10_8(+(1, n13082_8)), gen_:::nil10_8(b)) -> *12_8, rt in Omega(n13082_8)
APPEND(gen_:::nil10_8(n14715_8), gen_:::nil10_8(b)) -> *12_8, rt in Omega(n14715_8)


Generator Equations:
gen_:::nil10_8(0) <=> nil
gen_:::nil10_8(+(x, 1)) <=> ::(leaf, gen_:::nil10_8(x))
gen_leaf:node11_8(0) <=> leaf
gen_leaf:node11_8(+(x, 1)) <=> node(hole_a7_8, leaf, gen_leaf:node11_8(x))


The following defined symbols remain to be analysed:
APPEND#1

They will be analysed ascendingly in the following order:
APPEND = APPEND#1

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

(35) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
APPEND#1(gen_:::nil10_8(+(1, n17765_8)), gen_:::nil10_8(b)) -> *12_8, rt in Omega(n17765_8)

Induction Base:
APPEND#1(gen_:::nil10_8(+(1, 0)), gen_:::nil10_8(b))

Induction Step:
APPEND#1(gen_:::nil10_8(+(1, +(n17765_8, 1))), gen_:::nil10_8(b)) ->_R^Omega(1)
c1(APPEND(gen_:::nil10_8(+(1, n17765_8)), gen_:::nil10_8(b))) ->_R^Omega(1)
c1(c(APPEND#1(gen_:::nil10_8(+(1, n17765_8)), gen_:::nil10_8(b)))) ->_IH
c1(c(*12_8))

We have rt in Omega(n^1) and sz in O(n). Thus, we have irc_R in Omega(n).
----------------------------------------

(36)
BOUNDS(1, INF)