KILLED
proof of input_qDPuZGaoeN.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) NarrowingProof [BOTH BOUNDS(ID, ID), 0 ms]
        (12) CpxTypedWeightedCompleteTrs
        (13) CpxTypedWeightedTrsToRntsProof [UPPER BOUND(ID), 0 ms]
        (14) CpxRNTS
        (15) InliningProof [UPPER BOUND(ID), 124 ms]
        (16) CpxRNTS
        (17) SimplificationProof [BOTH BOUNDS(ID, ID), 0 ms]
        (18) CpxRNTS
        (19) CpxRntsAnalysisOrderProof [BOTH BOUNDS(ID, ID), 0 ms]
        (20) CpxRNTS
        (21) ResultPropagationProof [UPPER BOUND(ID), 0 ms]
        (22) CpxRNTS
        (23) IntTrsBoundProof [UPPER BOUND(ID), 224 ms]
        (24) CpxRNTS
        (25) IntTrsBoundProof [UPPER BOUND(ID), 27 ms]
        (26) CpxRNTS
        (27) ResultPropagationProof [UPPER BOUND(ID), 0 ms]
        (28) CpxRNTS
        (29) IntTrsBoundProof [UPPER BOUND(ID), 108 ms]
        (30) CpxRNTS
        (31) IntTrsBoundProof [UPPER BOUND(ID), 34 ms]
        (32) CpxRNTS
        (33) ResultPropagationProof [UPPER BOUND(ID), 0 ms]
        (34) CpxRNTS
        (35) IntTrsBoundProof [UPPER BOUND(ID), 629 ms]
        (36) CpxRNTS
        (37) IntTrsBoundProof [UPPER BOUND(ID), 392 ms]
        (38) CpxRNTS
    (39) CompletionProof [UPPER BOUND(ID), 0 ms]
    (40) CpxTypedWeightedCompleteTrs
        (41) CpxTypedWeightedTrsToRntsProof [UPPER BOUND(ID), 0 ms]
        (42) CpxRNTS
(43) CpxTrsToCdtProof [UPPER BOUND(ID), 0 ms]
(44) CdtProblem
    (45) CdtLeafRemovalProof [BOTH BOUNDS(ID, ID), 0 ms]
    (46) CdtProblem
    (47) CdtRhsSimplificationProcessorProof [BOTH BOUNDS(ID, ID), 0 ms]
    (48) CdtProblem
    (49) CdtUsableRulesProof [BOTH BOUNDS(ID, ID), 0 ms]
    (50) CdtProblem
    (51) CdtNarrowingProof [BOTH BOUNDS(ID, ID), 0 ms]
    (52) CdtProblem
    (53) CdtNarrowingProof [BOTH BOUNDS(ID, ID), 0 ms]
    (54) CdtProblem
    (55) CdtRuleRemovalProof [UPPER BOUND(ADD(n^1)), 19 ms]
    (56) CdtProblem
    (57) CdtNarrowingProof [BOTH BOUNDS(ID, ID), 0 ms]
    (58) CdtProblem
    (59) CdtKnowledgeProof [BOTH BOUNDS(ID, ID), 0 ms]
    (60) CdtProblem
    (61) CdtForwardInstantiationProof [BOTH BOUNDS(ID, ID), 0 ms]
    (62) CdtProblem
    (63) CdtForwardInstantiationProof [BOTH BOUNDS(ID, ID), 0 ms]
    (64) CdtProblem
    (65) CdtForwardInstantiationProof [BOTH BOUNDS(ID, ID), 0 ms]
    (66) CdtProblem
    (67) CdtForwardInstantiationProof [BOTH BOUNDS(ID, ID), 0 ms]
    (68) CdtProblem
    (69) CdtForwardInstantiationProof [BOTH BOUNDS(ID, ID), 0 ms]
    (70) CdtProblem
    (71) CdtForwardInstantiationProof [BOTH BOUNDS(ID, ID), 0 ms]
    (72) CdtProblem
    (73) CdtForwardInstantiationProof [BOTH BOUNDS(ID, ID), 0 ms]
    (74) CdtProblem
    (75) CdtForwardInstantiationProof [BOTH BOUNDS(ID, ID), 0 ms]
    (76) CdtProblem
    (77) CdtForwardInstantiationProof [BOTH BOUNDS(ID, ID), 0 ms]
    (78) 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:

   f(node(s(n), xs)) -> f(addchild(select(xs), node(n, xs)))
   select(cons(ap, xs)) -> ap
   select(cons(ap, xs)) -> select(xs)
   addchild(node(y, ys), node(n, xs)) -> node(y, cons(node(n, xs), ys))

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:

   f(node(s(n), xs)) -> f(addchild(select(xs), node(n, xs)))
   select(cons(ap, xs)) -> ap
   select(cons(ap, xs)) -> select(xs)
   addchild(node(y, ys), node(n, xs)) -> node(y, cons(node(n, xs), ys))

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:

   f(node(s(n), xs)) -> f(addchild(select(xs), node(n, xs)))
   select(cons(ap, xs)) -> ap
   select(cons(ap, xs)) -> select(xs)
   addchild(node(y, ys), node(n, xs)) -> node(y, cons(node(n, xs), ys))

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:

   f(node(s(n), xs)) -> f(addchild(select(xs), node(n, xs))) [1]
   select(cons(ap, xs)) -> ap [1]
   select(cons(ap, xs)) -> select(xs) [1]
   addchild(node(y, ys), node(n, xs)) -> node(y, cons(node(n, xs), ys)) [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:

   f(node(s(n), xs)) -> f(addchild(select(xs), node(n, xs))) [1]
   select(cons(ap, xs)) -> ap [1]
   select(cons(ap, xs)) -> select(xs) [1]
   addchild(node(y, ys), node(n, xs)) -> node(y, cons(node(n, xs), ys)) [1]

The TRS has the following type information:
f :: node -> f
node :: s -> cons -> node
s :: s -> s
addchild :: node -> node -> node
select :: cons -> node
cons :: node -> cons -> cons

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

(9) 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:

   f_1

(c) The following functions are completely defined:

   addchild_2
   select_1

Due to the following rules being added:

   addchild(v0, v1) -> const1 [0]
   select(v0) -> const1 [0]

And the following fresh constants:    const1, const, const2, const3

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

(10)
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:

   f(node(s(n), xs)) -> f(addchild(select(xs), node(n, xs))) [1]
   select(cons(ap, xs)) -> ap [1]
   select(cons(ap, xs)) -> select(xs) [1]
   addchild(node(y, ys), node(n, xs)) -> node(y, cons(node(n, xs), ys)) [1]
   addchild(v0, v1) -> const1 [0]
   select(v0) -> const1 [0]

The TRS has the following type information:
f :: node:const1 -> f
node :: s -> cons -> node:const1
s :: s -> s
addchild :: node:const1 -> node:const1 -> node:const1
select :: cons -> node:const1
cons :: node:const1 -> cons -> cons
const1 :: node:const1
const :: f
const2 :: s
const3 :: cons

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

(11) NarrowingProof (BOTH BOUNDS(ID, ID))
Narrowed the inner basic terms of all right-hand sides by a single narrowing step.
----------------------------------------

(12)
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:

   f(node(s(n), cons(ap', xs'))) -> f(addchild(ap', node(n, cons(ap', xs')))) [2]
   f(node(s(n), cons(ap'', xs''))) -> f(addchild(select(xs''), node(n, cons(ap'', xs'')))) [2]
   f(node(s(n), xs)) -> f(addchild(const1, node(n, xs))) [1]
   select(cons(ap, xs)) -> ap [1]
   select(cons(ap, xs)) -> select(xs) [1]
   addchild(node(y, ys), node(n, xs)) -> node(y, cons(node(n, xs), ys)) [1]
   addchild(v0, v1) -> const1 [0]
   select(v0) -> const1 [0]

The TRS has the following type information:
f :: node:const1 -> f
node :: s -> cons -> node:const1
s :: s -> s
addchild :: node:const1 -> node:const1 -> node:const1
select :: cons -> node:const1
cons :: node:const1 -> cons -> cons
const1 :: node:const1
const :: f
const2 :: s
const3 :: cons

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

(13) CpxTypedWeightedTrsToRntsProof (UPPER BOUND(ID))
Transformed the TRS into an over-approximating RNTS by (improved) Size Abstraction.
The constant constructors are abstracted as follows:

   const1 => 0
   const => 0
   const2 => 0
   const3 => 0

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

(14)
Obligation:
Complexity RNTS consisting of the following rules:

   addchild(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
   addchild(z, z') -{ 1 }-> 1 + y + (1 + (1 + n + xs) + ys) :|: n >= 0, xs >= 0, z' = 1 + n + xs, ys >= 0, y >= 0, z = 1 + y + ys
   f(z) -{ 2 }-> f(addchild(ap', 1 + n + (1 + ap' + xs'))) :|: n >= 0, xs' >= 0, z = 1 + (1 + n) + (1 + ap' + xs'), ap' >= 0
   f(z) -{ 2 }-> f(addchild(select(xs''), 1 + n + (1 + ap'' + xs''))) :|: n >= 0, ap'' >= 0, xs'' >= 0, z = 1 + (1 + n) + (1 + ap'' + xs'')
   f(z) -{ 1 }-> f(addchild(0, 1 + n + xs)) :|: n >= 0, xs >= 0, z = 1 + (1 + n) + xs
   select(z) -{ 1 }-> ap :|: z = 1 + ap + xs, ap >= 0, xs >= 0
   select(z) -{ 1 }-> select(xs) :|: z = 1 + ap + xs, ap >= 0, xs >= 0
   select(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0


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

(15) InliningProof (UPPER BOUND(ID))
Inlined the following terminating rules on right-hand sides where appropriate:

   addchild(z, z') -{ 1 }-> 1 + y + (1 + (1 + n + xs) + ys) :|: n >= 0, xs >= 0, z' = 1 + n + xs, ys >= 0, y >= 0, z = 1 + y + ys
   addchild(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1

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

(16)
Obligation:
Complexity RNTS consisting of the following rules:

   addchild(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
   addchild(z, z') -{ 1 }-> 1 + y + (1 + (1 + n + xs) + ys) :|: n >= 0, xs >= 0, z' = 1 + n + xs, ys >= 0, y >= 0, z = 1 + y + ys
   f(z) -{ 2 }-> f(addchild(select(xs''), 1 + n + (1 + ap'' + xs''))) :|: n >= 0, ap'' >= 0, xs'' >= 0, z = 1 + (1 + n) + (1 + ap'' + xs'')
   f(z) -{ 2 }-> f(0) :|: n >= 0, xs' >= 0, z = 1 + (1 + n) + (1 + ap' + xs'), ap' >= 0, v0 >= 0, v1 >= 0, ap' = v0, 1 + n + (1 + ap' + xs') = v1
   f(z) -{ 1 }-> f(0) :|: n >= 0, xs >= 0, z = 1 + (1 + n) + xs, v0 >= 0, v1 >= 0, 0 = v0, 1 + n + xs = v1
   f(z) -{ 3 }-> f(1 + y + (1 + (1 + n' + xs) + ys)) :|: n >= 0, xs' >= 0, z = 1 + (1 + n) + (1 + ap' + xs'), ap' >= 0, n' >= 0, xs >= 0, 1 + n + (1 + ap' + xs') = 1 + n' + xs, ys >= 0, y >= 0, ap' = 1 + y + ys
   select(z) -{ 1 }-> ap :|: z = 1 + ap + xs, ap >= 0, xs >= 0
   select(z) -{ 1 }-> select(xs) :|: z = 1 + ap + xs, ap >= 0, xs >= 0
   select(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0


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

(17) SimplificationProof (BOTH BOUNDS(ID, ID))
Simplified the RNTS by moving equalities from the constraints into the right-hand sides.
----------------------------------------

(18)
Obligation:
Complexity RNTS consisting of the following rules:

   addchild(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   addchild(z, z') -{ 1 }-> 1 + y + (1 + (1 + n + xs) + ys) :|: n >= 0, xs >= 0, z' = 1 + n + xs, ys >= 0, y >= 0, z = 1 + y + ys
   f(z) -{ 2 }-> f(addchild(select(xs''), 1 + n + (1 + ap'' + xs''))) :|: n >= 0, ap'' >= 0, xs'' >= 0, z = 1 + (1 + n) + (1 + ap'' + xs'')
   f(z) -{ 2 }-> f(0) :|: n >= 0, xs' >= 0, z = 1 + (1 + n) + (1 + ap' + xs'), ap' >= 0, v0 >= 0, v1 >= 0, ap' = v0, 1 + n + (1 + ap' + xs') = v1
   f(z) -{ 1 }-> f(0) :|: n >= 0, xs >= 0, z = 1 + (1 + n) + xs, v0 >= 0, v1 >= 0, 0 = v0, 1 + n + xs = v1
   f(z) -{ 3 }-> f(1 + y + (1 + (1 + n' + xs) + ys)) :|: n >= 0, xs' >= 0, z = 1 + (1 + n) + (1 + ap' + xs'), ap' >= 0, n' >= 0, xs >= 0, 1 + n + (1 + ap' + xs') = 1 + n' + xs, ys >= 0, y >= 0, ap' = 1 + y + ys
   select(z) -{ 1 }-> ap :|: z = 1 + ap + xs, ap >= 0, xs >= 0
   select(z) -{ 1 }-> select(xs) :|: z = 1 + ap + xs, ap >= 0, xs >= 0
   select(z) -{ 0 }-> 0 :|: z >= 0


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

(19) CpxRntsAnalysisOrderProof (BOTH BOUNDS(ID, ID))
Found the following analysis order by SCC decomposition:

   { select }
   { addchild }
   { f }

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

(20)
Obligation:
Complexity RNTS consisting of the following rules:

   addchild(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   addchild(z, z') -{ 1 }-> 1 + y + (1 + (1 + n + xs) + ys) :|: n >= 0, xs >= 0, z' = 1 + n + xs, ys >= 0, y >= 0, z = 1 + y + ys
   f(z) -{ 2 }-> f(addchild(select(xs''), 1 + n + (1 + ap'' + xs''))) :|: n >= 0, ap'' >= 0, xs'' >= 0, z = 1 + (1 + n) + (1 + ap'' + xs'')
   f(z) -{ 2 }-> f(0) :|: n >= 0, xs' >= 0, z = 1 + (1 + n) + (1 + ap' + xs'), ap' >= 0, v0 >= 0, v1 >= 0, ap' = v0, 1 + n + (1 + ap' + xs') = v1
   f(z) -{ 1 }-> f(0) :|: n >= 0, xs >= 0, z = 1 + (1 + n) + xs, v0 >= 0, v1 >= 0, 0 = v0, 1 + n + xs = v1
   f(z) -{ 3 }-> f(1 + y + (1 + (1 + n' + xs) + ys)) :|: n >= 0, xs' >= 0, z = 1 + (1 + n) + (1 + ap' + xs'), ap' >= 0, n' >= 0, xs >= 0, 1 + n + (1 + ap' + xs') = 1 + n' + xs, ys >= 0, y >= 0, ap' = 1 + y + ys
   select(z) -{ 1 }-> ap :|: z = 1 + ap + xs, ap >= 0, xs >= 0
   select(z) -{ 1 }-> select(xs) :|: z = 1 + ap + xs, ap >= 0, xs >= 0
   select(z) -{ 0 }-> 0 :|: z >= 0

Function symbols to be analyzed: {select}, {addchild}, {f}

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

(21) ResultPropagationProof (UPPER BOUND(ID))
Applied inner abstraction using the recently inferred runtime/size bounds where possible.
----------------------------------------

(22)
Obligation:
Complexity RNTS consisting of the following rules:

   addchild(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   addchild(z, z') -{ 1 }-> 1 + y + (1 + (1 + n + xs) + ys) :|: n >= 0, xs >= 0, z' = 1 + n + xs, ys >= 0, y >= 0, z = 1 + y + ys
   f(z) -{ 2 }-> f(addchild(select(xs''), 1 + n + (1 + ap'' + xs''))) :|: n >= 0, ap'' >= 0, xs'' >= 0, z = 1 + (1 + n) + (1 + ap'' + xs'')
   f(z) -{ 2 }-> f(0) :|: n >= 0, xs' >= 0, z = 1 + (1 + n) + (1 + ap' + xs'), ap' >= 0, v0 >= 0, v1 >= 0, ap' = v0, 1 + n + (1 + ap' + xs') = v1
   f(z) -{ 1 }-> f(0) :|: n >= 0, xs >= 0, z = 1 + (1 + n) + xs, v0 >= 0, v1 >= 0, 0 = v0, 1 + n + xs = v1
   f(z) -{ 3 }-> f(1 + y + (1 + (1 + n' + xs) + ys)) :|: n >= 0, xs' >= 0, z = 1 + (1 + n) + (1 + ap' + xs'), ap' >= 0, n' >= 0, xs >= 0, 1 + n + (1 + ap' + xs') = 1 + n' + xs, ys >= 0, y >= 0, ap' = 1 + y + ys
   select(z) -{ 1 }-> ap :|: z = 1 + ap + xs, ap >= 0, xs >= 0
   select(z) -{ 1 }-> select(xs) :|: z = 1 + ap + xs, ap >= 0, xs >= 0
   select(z) -{ 0 }-> 0 :|: z >= 0

Function symbols to be analyzed: {select}, {addchild}, {f}

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

(23) IntTrsBoundProof (UPPER BOUND(ID))

Computed SIZE bound using KoAT for: select
after applying outer abstraction to obtain an ITS,
resulting in: O(n^1) with polynomial bound: z

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

(24)
Obligation:
Complexity RNTS consisting of the following rules:

   addchild(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   addchild(z, z') -{ 1 }-> 1 + y + (1 + (1 + n + xs) + ys) :|: n >= 0, xs >= 0, z' = 1 + n + xs, ys >= 0, y >= 0, z = 1 + y + ys
   f(z) -{ 2 }-> f(addchild(select(xs''), 1 + n + (1 + ap'' + xs''))) :|: n >= 0, ap'' >= 0, xs'' >= 0, z = 1 + (1 + n) + (1 + ap'' + xs'')
   f(z) -{ 2 }-> f(0) :|: n >= 0, xs' >= 0, z = 1 + (1 + n) + (1 + ap' + xs'), ap' >= 0, v0 >= 0, v1 >= 0, ap' = v0, 1 + n + (1 + ap' + xs') = v1
   f(z) -{ 1 }-> f(0) :|: n >= 0, xs >= 0, z = 1 + (1 + n) + xs, v0 >= 0, v1 >= 0, 0 = v0, 1 + n + xs = v1
   f(z) -{ 3 }-> f(1 + y + (1 + (1 + n' + xs) + ys)) :|: n >= 0, xs' >= 0, z = 1 + (1 + n) + (1 + ap' + xs'), ap' >= 0, n' >= 0, xs >= 0, 1 + n + (1 + ap' + xs') = 1 + n' + xs, ys >= 0, y >= 0, ap' = 1 + y + ys
   select(z) -{ 1 }-> ap :|: z = 1 + ap + xs, ap >= 0, xs >= 0
   select(z) -{ 1 }-> select(xs) :|: z = 1 + ap + xs, ap >= 0, xs >= 0
   select(z) -{ 0 }-> 0 :|: z >= 0

Function symbols to be analyzed: {select}, {addchild}, {f}
Previous analysis results are:
  select: runtime: ?, size: O(n^1) [z]

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

(25) IntTrsBoundProof (UPPER BOUND(ID))

Computed RUNTIME bound using KoAT for: select
after applying outer abstraction to obtain an ITS,
resulting in: O(n^1) with polynomial bound: 1 + z

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

(26)
Obligation:
Complexity RNTS consisting of the following rules:

   addchild(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   addchild(z, z') -{ 1 }-> 1 + y + (1 + (1 + n + xs) + ys) :|: n >= 0, xs >= 0, z' = 1 + n + xs, ys >= 0, y >= 0, z = 1 + y + ys
   f(z) -{ 2 }-> f(addchild(select(xs''), 1 + n + (1 + ap'' + xs''))) :|: n >= 0, ap'' >= 0, xs'' >= 0, z = 1 + (1 + n) + (1 + ap'' + xs'')
   f(z) -{ 2 }-> f(0) :|: n >= 0, xs' >= 0, z = 1 + (1 + n) + (1 + ap' + xs'), ap' >= 0, v0 >= 0, v1 >= 0, ap' = v0, 1 + n + (1 + ap' + xs') = v1
   f(z) -{ 1 }-> f(0) :|: n >= 0, xs >= 0, z = 1 + (1 + n) + xs, v0 >= 0, v1 >= 0, 0 = v0, 1 + n + xs = v1
   f(z) -{ 3 }-> f(1 + y + (1 + (1 + n' + xs) + ys)) :|: n >= 0, xs' >= 0, z = 1 + (1 + n) + (1 + ap' + xs'), ap' >= 0, n' >= 0, xs >= 0, 1 + n + (1 + ap' + xs') = 1 + n' + xs, ys >= 0, y >= 0, ap' = 1 + y + ys
   select(z) -{ 1 }-> ap :|: z = 1 + ap + xs, ap >= 0, xs >= 0
   select(z) -{ 1 }-> select(xs) :|: z = 1 + ap + xs, ap >= 0, xs >= 0
   select(z) -{ 0 }-> 0 :|: z >= 0

Function symbols to be analyzed: {addchild}, {f}
Previous analysis results are:
  select: runtime: O(n^1) [1 + z], size: O(n^1) [z]

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

(27) ResultPropagationProof (UPPER BOUND(ID))
Applied inner abstraction using the recently inferred runtime/size bounds where possible.
----------------------------------------

(28)
Obligation:
Complexity RNTS consisting of the following rules:

   addchild(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   addchild(z, z') -{ 1 }-> 1 + y + (1 + (1 + n + xs) + ys) :|: n >= 0, xs >= 0, z' = 1 + n + xs, ys >= 0, y >= 0, z = 1 + y + ys
   f(z) -{ 3 + xs'' }-> f(addchild(s', 1 + n + (1 + ap'' + xs''))) :|: s' >= 0, s' <= xs'', n >= 0, ap'' >= 0, xs'' >= 0, z = 1 + (1 + n) + (1 + ap'' + xs'')
   f(z) -{ 2 }-> f(0) :|: n >= 0, xs' >= 0, z = 1 + (1 + n) + (1 + ap' + xs'), ap' >= 0, v0 >= 0, v1 >= 0, ap' = v0, 1 + n + (1 + ap' + xs') = v1
   f(z) -{ 1 }-> f(0) :|: n >= 0, xs >= 0, z = 1 + (1 + n) + xs, v0 >= 0, v1 >= 0, 0 = v0, 1 + n + xs = v1
   f(z) -{ 3 }-> f(1 + y + (1 + (1 + n' + xs) + ys)) :|: n >= 0, xs' >= 0, z = 1 + (1 + n) + (1 + ap' + xs'), ap' >= 0, n' >= 0, xs >= 0, 1 + n + (1 + ap' + xs') = 1 + n' + xs, ys >= 0, y >= 0, ap' = 1 + y + ys
   select(z) -{ 1 }-> ap :|: z = 1 + ap + xs, ap >= 0, xs >= 0
   select(z) -{ 2 + xs }-> s :|: s >= 0, s <= xs, z = 1 + ap + xs, ap >= 0, xs >= 0
   select(z) -{ 0 }-> 0 :|: z >= 0

Function symbols to be analyzed: {addchild}, {f}
Previous analysis results are:
  select: runtime: O(n^1) [1 + z], size: O(n^1) [z]

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

(29) IntTrsBoundProof (UPPER BOUND(ID))

Computed SIZE bound using CoFloCo for: addchild
after applying outer abstraction to obtain an ITS,
resulting in: O(n^1) with polynomial bound: 1 + z + z'

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

(30)
Obligation:
Complexity RNTS consisting of the following rules:

   addchild(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   addchild(z, z') -{ 1 }-> 1 + y + (1 + (1 + n + xs) + ys) :|: n >= 0, xs >= 0, z' = 1 + n + xs, ys >= 0, y >= 0, z = 1 + y + ys
   f(z) -{ 3 + xs'' }-> f(addchild(s', 1 + n + (1 + ap'' + xs''))) :|: s' >= 0, s' <= xs'', n >= 0, ap'' >= 0, xs'' >= 0, z = 1 + (1 + n) + (1 + ap'' + xs'')
   f(z) -{ 2 }-> f(0) :|: n >= 0, xs' >= 0, z = 1 + (1 + n) + (1 + ap' + xs'), ap' >= 0, v0 >= 0, v1 >= 0, ap' = v0, 1 + n + (1 + ap' + xs') = v1
   f(z) -{ 1 }-> f(0) :|: n >= 0, xs >= 0, z = 1 + (1 + n) + xs, v0 >= 0, v1 >= 0, 0 = v0, 1 + n + xs = v1
   f(z) -{ 3 }-> f(1 + y + (1 + (1 + n' + xs) + ys)) :|: n >= 0, xs' >= 0, z = 1 + (1 + n) + (1 + ap' + xs'), ap' >= 0, n' >= 0, xs >= 0, 1 + n + (1 + ap' + xs') = 1 + n' + xs, ys >= 0, y >= 0, ap' = 1 + y + ys
   select(z) -{ 1 }-> ap :|: z = 1 + ap + xs, ap >= 0, xs >= 0
   select(z) -{ 2 + xs }-> s :|: s >= 0, s <= xs, z = 1 + ap + xs, ap >= 0, xs >= 0
   select(z) -{ 0 }-> 0 :|: z >= 0

Function symbols to be analyzed: {addchild}, {f}
Previous analysis results are:
  select: runtime: O(n^1) [1 + z], size: O(n^1) [z]
  addchild: runtime: ?, size: O(n^1) [1 + z + z']

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

(31) IntTrsBoundProof (UPPER BOUND(ID))

Computed RUNTIME bound using CoFloCo for: addchild
after applying outer abstraction to obtain an ITS,
resulting in: O(1) with polynomial bound: 1

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

(32)
Obligation:
Complexity RNTS consisting of the following rules:

   addchild(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   addchild(z, z') -{ 1 }-> 1 + y + (1 + (1 + n + xs) + ys) :|: n >= 0, xs >= 0, z' = 1 + n + xs, ys >= 0, y >= 0, z = 1 + y + ys
   f(z) -{ 3 + xs'' }-> f(addchild(s', 1 + n + (1 + ap'' + xs''))) :|: s' >= 0, s' <= xs'', n >= 0, ap'' >= 0, xs'' >= 0, z = 1 + (1 + n) + (1 + ap'' + xs'')
   f(z) -{ 2 }-> f(0) :|: n >= 0, xs' >= 0, z = 1 + (1 + n) + (1 + ap' + xs'), ap' >= 0, v0 >= 0, v1 >= 0, ap' = v0, 1 + n + (1 + ap' + xs') = v1
   f(z) -{ 1 }-> f(0) :|: n >= 0, xs >= 0, z = 1 + (1 + n) + xs, v0 >= 0, v1 >= 0, 0 = v0, 1 + n + xs = v1
   f(z) -{ 3 }-> f(1 + y + (1 + (1 + n' + xs) + ys)) :|: n >= 0, xs' >= 0, z = 1 + (1 + n) + (1 + ap' + xs'), ap' >= 0, n' >= 0, xs >= 0, 1 + n + (1 + ap' + xs') = 1 + n' + xs, ys >= 0, y >= 0, ap' = 1 + y + ys
   select(z) -{ 1 }-> ap :|: z = 1 + ap + xs, ap >= 0, xs >= 0
   select(z) -{ 2 + xs }-> s :|: s >= 0, s <= xs, z = 1 + ap + xs, ap >= 0, xs >= 0
   select(z) -{ 0 }-> 0 :|: z >= 0

Function symbols to be analyzed: {f}
Previous analysis results are:
  select: runtime: O(n^1) [1 + z], size: O(n^1) [z]
  addchild: runtime: O(1) [1], size: O(n^1) [1 + z + z']

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

(33) ResultPropagationProof (UPPER BOUND(ID))
Applied inner abstraction using the recently inferred runtime/size bounds where possible.
----------------------------------------

(34)
Obligation:
Complexity RNTS consisting of the following rules:

   addchild(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   addchild(z, z') -{ 1 }-> 1 + y + (1 + (1 + n + xs) + ys) :|: n >= 0, xs >= 0, z' = 1 + n + xs, ys >= 0, y >= 0, z = 1 + y + ys
   f(z) -{ 4 + xs'' }-> f(s'') :|: s'' >= 0, s'' <= s' + (1 + n + (1 + ap'' + xs'')) + 1, s' >= 0, s' <= xs'', n >= 0, ap'' >= 0, xs'' >= 0, z = 1 + (1 + n) + (1 + ap'' + xs'')
   f(z) -{ 2 }-> f(0) :|: n >= 0, xs' >= 0, z = 1 + (1 + n) + (1 + ap' + xs'), ap' >= 0, v0 >= 0, v1 >= 0, ap' = v0, 1 + n + (1 + ap' + xs') = v1
   f(z) -{ 1 }-> f(0) :|: n >= 0, xs >= 0, z = 1 + (1 + n) + xs, v0 >= 0, v1 >= 0, 0 = v0, 1 + n + xs = v1
   f(z) -{ 3 }-> f(1 + y + (1 + (1 + n' + xs) + ys)) :|: n >= 0, xs' >= 0, z = 1 + (1 + n) + (1 + ap' + xs'), ap' >= 0, n' >= 0, xs >= 0, 1 + n + (1 + ap' + xs') = 1 + n' + xs, ys >= 0, y >= 0, ap' = 1 + y + ys
   select(z) -{ 1 }-> ap :|: z = 1 + ap + xs, ap >= 0, xs >= 0
   select(z) -{ 2 + xs }-> s :|: s >= 0, s <= xs, z = 1 + ap + xs, ap >= 0, xs >= 0
   select(z) -{ 0 }-> 0 :|: z >= 0

Function symbols to be analyzed: {f}
Previous analysis results are:
  select: runtime: O(n^1) [1 + z], size: O(n^1) [z]
  addchild: runtime: O(1) [1], size: O(n^1) [1 + z + z']

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

(35) IntTrsBoundProof (UPPER BOUND(ID))

Computed SIZE bound using CoFloCo for: f
after applying outer abstraction to obtain an ITS,
resulting in: O(1) with polynomial bound: 0

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

(36)
Obligation:
Complexity RNTS consisting of the following rules:

   addchild(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   addchild(z, z') -{ 1 }-> 1 + y + (1 + (1 + n + xs) + ys) :|: n >= 0, xs >= 0, z' = 1 + n + xs, ys >= 0, y >= 0, z = 1 + y + ys
   f(z) -{ 4 + xs'' }-> f(s'') :|: s'' >= 0, s'' <= s' + (1 + n + (1 + ap'' + xs'')) + 1, s' >= 0, s' <= xs'', n >= 0, ap'' >= 0, xs'' >= 0, z = 1 + (1 + n) + (1 + ap'' + xs'')
   f(z) -{ 2 }-> f(0) :|: n >= 0, xs' >= 0, z = 1 + (1 + n) + (1 + ap' + xs'), ap' >= 0, v0 >= 0, v1 >= 0, ap' = v0, 1 + n + (1 + ap' + xs') = v1
   f(z) -{ 1 }-> f(0) :|: n >= 0, xs >= 0, z = 1 + (1 + n) + xs, v0 >= 0, v1 >= 0, 0 = v0, 1 + n + xs = v1
   f(z) -{ 3 }-> f(1 + y + (1 + (1 + n' + xs) + ys)) :|: n >= 0, xs' >= 0, z = 1 + (1 + n) + (1 + ap' + xs'), ap' >= 0, n' >= 0, xs >= 0, 1 + n + (1 + ap' + xs') = 1 + n' + xs, ys >= 0, y >= 0, ap' = 1 + y + ys
   select(z) -{ 1 }-> ap :|: z = 1 + ap + xs, ap >= 0, xs >= 0
   select(z) -{ 2 + xs }-> s :|: s >= 0, s <= xs, z = 1 + ap + xs, ap >= 0, xs >= 0
   select(z) -{ 0 }-> 0 :|: z >= 0

Function symbols to be analyzed: {f}
Previous analysis results are:
  select: runtime: O(n^1) [1 + z], size: O(n^1) [z]
  addchild: runtime: O(1) [1], size: O(n^1) [1 + z + z']
  f: runtime: ?, size: O(1) [0]

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

(37) IntTrsBoundProof (UPPER BOUND(ID))

Computed RUNTIME bound using CoFloCo for: f
after applying outer abstraction to obtain an ITS,
resulting in: INF with polynomial bound: ?

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

(38)
Obligation:
Complexity RNTS consisting of the following rules:

   addchild(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   addchild(z, z') -{ 1 }-> 1 + y + (1 + (1 + n + xs) + ys) :|: n >= 0, xs >= 0, z' = 1 + n + xs, ys >= 0, y >= 0, z = 1 + y + ys
   f(z) -{ 4 + xs'' }-> f(s'') :|: s'' >= 0, s'' <= s' + (1 + n + (1 + ap'' + xs'')) + 1, s' >= 0, s' <= xs'', n >= 0, ap'' >= 0, xs'' >= 0, z = 1 + (1 + n) + (1 + ap'' + xs'')
   f(z) -{ 2 }-> f(0) :|: n >= 0, xs' >= 0, z = 1 + (1 + n) + (1 + ap' + xs'), ap' >= 0, v0 >= 0, v1 >= 0, ap' = v0, 1 + n + (1 + ap' + xs') = v1
   f(z) -{ 1 }-> f(0) :|: n >= 0, xs >= 0, z = 1 + (1 + n) + xs, v0 >= 0, v1 >= 0, 0 = v0, 1 + n + xs = v1
   f(z) -{ 3 }-> f(1 + y + (1 + (1 + n' + xs) + ys)) :|: n >= 0, xs' >= 0, z = 1 + (1 + n) + (1 + ap' + xs'), ap' >= 0, n' >= 0, xs >= 0, 1 + n + (1 + ap' + xs') = 1 + n' + xs, ys >= 0, y >= 0, ap' = 1 + y + ys
   select(z) -{ 1 }-> ap :|: z = 1 + ap + xs, ap >= 0, xs >= 0
   select(z) -{ 2 + xs }-> s :|: s >= 0, s <= xs, z = 1 + ap + xs, ap >= 0, xs >= 0
   select(z) -{ 0 }-> 0 :|: z >= 0

Function symbols to be analyzed: {f}
Previous analysis results are:
  select: runtime: O(n^1) [1 + z], size: O(n^1) [z]
  addchild: runtime: O(1) [1], size: O(n^1) [1 + z + z']
  f: runtime: INF, size: O(1) [0]

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

(39) 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:

   f(v0) -> null_f [0]
   select(v0) -> null_select [0]
   addchild(v0, v1) -> null_addchild [0]

And the following fresh constants:    null_f, null_select, null_addchild, const, const1

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

(40)
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:

   f(node(s(n), xs)) -> f(addchild(select(xs), node(n, xs))) [1]
   select(cons(ap, xs)) -> ap [1]
   select(cons(ap, xs)) -> select(xs) [1]
   addchild(node(y, ys), node(n, xs)) -> node(y, cons(node(n, xs), ys)) [1]
   f(v0) -> null_f [0]
   select(v0) -> null_select [0]
   addchild(v0, v1) -> null_addchild [0]

The TRS has the following type information:
f :: node:null_select:null_addchild -> null_f
node :: s -> cons -> node:null_select:null_addchild
s :: s -> s
addchild :: node:null_select:null_addchild -> node:null_select:null_addchild -> node:null_select:null_addchild
select :: cons -> node:null_select:null_addchild
cons :: node:null_select:null_addchild -> cons -> cons
null_f :: null_f
null_select :: node:null_select:null_addchild
null_addchild :: node:null_select:null_addchild
const :: s
const1 :: cons

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

(41) CpxTypedWeightedTrsToRntsProof (UPPER BOUND(ID))
Transformed the TRS into an over-approximating RNTS by (improved) Size Abstraction.
The constant constructors are abstracted as follows:

   null_f => 0
   null_select => 0
   null_addchild => 0
   const => 0
   const1 => 0

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

(42)
Obligation:
Complexity RNTS consisting of the following rules:

   addchild(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
   addchild(z, z') -{ 1 }-> 1 + y + (1 + (1 + n + xs) + ys) :|: n >= 0, xs >= 0, z' = 1 + n + xs, ys >= 0, y >= 0, z = 1 + y + ys
   f(z) -{ 1 }-> f(addchild(select(xs), 1 + n + xs)) :|: n >= 0, xs >= 0, z = 1 + (1 + n) + xs
   f(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0
   select(z) -{ 1 }-> ap :|: z = 1 + ap + xs, ap >= 0, xs >= 0
   select(z) -{ 1 }-> select(xs) :|: z = 1 + ap + xs, ap >= 0, xs >= 0
   select(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0

Only complete derivations are relevant for the runtime complexity.

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

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

(44)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   f(node(s(z0), z1)) -> f(addchild(select(z1), node(z0, z1)))
   select(cons(z0, z1)) -> z0
   select(cons(z0, z1)) -> select(z1)
   addchild(node(z0, z1), node(z2, z3)) -> node(z0, cons(node(z2, z3), z1))
Tuples:
   F(node(s(z0), z1)) -> c(F(addchild(select(z1), node(z0, z1))), ADDCHILD(select(z1), node(z0, z1)), SELECT(z1))
   SELECT(cons(z0, z1)) -> c1
   SELECT(cons(z0, z1)) -> c2(SELECT(z1))
   ADDCHILD(node(z0, z1), node(z2, z3)) -> c3
S tuples:
   F(node(s(z0), z1)) -> c(F(addchild(select(z1), node(z0, z1))), ADDCHILD(select(z1), node(z0, z1)), SELECT(z1))
   SELECT(cons(z0, z1)) -> c1
   SELECT(cons(z0, z1)) -> c2(SELECT(z1))
   ADDCHILD(node(z0, z1), node(z2, z3)) -> c3
K tuples:none
Defined Rule Symbols:   f_1, select_1, addchild_2

Defined Pair Symbols:   F_1, SELECT_1, ADDCHILD_2

Compound Symbols:   c_3, c1, c2_1, c3


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

(45) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID))
Removed 2 trailing nodes:
   SELECT(cons(z0, z1)) -> c1
   ADDCHILD(node(z0, z1), node(z2, z3)) -> c3

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

(46)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   f(node(s(z0), z1)) -> f(addchild(select(z1), node(z0, z1)))
   select(cons(z0, z1)) -> z0
   select(cons(z0, z1)) -> select(z1)
   addchild(node(z0, z1), node(z2, z3)) -> node(z0, cons(node(z2, z3), z1))
Tuples:
   F(node(s(z0), z1)) -> c(F(addchild(select(z1), node(z0, z1))), ADDCHILD(select(z1), node(z0, z1)), SELECT(z1))
   SELECT(cons(z0, z1)) -> c2(SELECT(z1))
S tuples:
   F(node(s(z0), z1)) -> c(F(addchild(select(z1), node(z0, z1))), ADDCHILD(select(z1), node(z0, z1)), SELECT(z1))
   SELECT(cons(z0, z1)) -> c2(SELECT(z1))
K tuples:none
Defined Rule Symbols:   f_1, select_1, addchild_2

Defined Pair Symbols:   F_1, SELECT_1

Compound Symbols:   c_3, c2_1


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

(47) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID))
Removed 1 trailing tuple parts
----------------------------------------

(48)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   f(node(s(z0), z1)) -> f(addchild(select(z1), node(z0, z1)))
   select(cons(z0, z1)) -> z0
   select(cons(z0, z1)) -> select(z1)
   addchild(node(z0, z1), node(z2, z3)) -> node(z0, cons(node(z2, z3), z1))
Tuples:
   SELECT(cons(z0, z1)) -> c2(SELECT(z1))
   F(node(s(z0), z1)) -> c(F(addchild(select(z1), node(z0, z1))), SELECT(z1))
S tuples:
   SELECT(cons(z0, z1)) -> c2(SELECT(z1))
   F(node(s(z0), z1)) -> c(F(addchild(select(z1), node(z0, z1))), SELECT(z1))
K tuples:none
Defined Rule Symbols:   f_1, select_1, addchild_2

Defined Pair Symbols:   SELECT_1, F_1

Compound Symbols:   c2_1, c_2


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

(49) CdtUsableRulesProof (BOTH BOUNDS(ID, ID))
The following rules are not usable and were removed:
   f(node(s(z0), z1)) -> f(addchild(select(z1), node(z0, z1)))

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

(50)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   addchild(node(z0, z1), node(z2, z3)) -> node(z0, cons(node(z2, z3), z1))
   select(cons(z0, z1)) -> z0
   select(cons(z0, z1)) -> select(z1)
Tuples:
   SELECT(cons(z0, z1)) -> c2(SELECT(z1))
   F(node(s(z0), z1)) -> c(F(addchild(select(z1), node(z0, z1))), SELECT(z1))
S tuples:
   SELECT(cons(z0, z1)) -> c2(SELECT(z1))
   F(node(s(z0), z1)) -> c(F(addchild(select(z1), node(z0, z1))), SELECT(z1))
K tuples:none
Defined Rule Symbols:   addchild_2, select_1

Defined Pair Symbols:   SELECT_1, F_1

Compound Symbols:   c2_1, c_2


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

(51) CdtNarrowingProof (BOTH BOUNDS(ID, ID))
Use narrowing to replace F(node(s(z0), z1)) -> c(F(addchild(select(z1), node(z0, z1))), SELECT(z1)) by 
   F(node(s(x0), cons(z0, z1))) -> c(F(addchild(z0, node(x0, cons(z0, z1)))), SELECT(cons(z0, z1)))
   F(node(s(x0), cons(z0, z1))) -> c(F(addchild(select(z1), node(x0, cons(z0, z1)))), SELECT(cons(z0, z1)))

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

(52)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   addchild(node(z0, z1), node(z2, z3)) -> node(z0, cons(node(z2, z3), z1))
   select(cons(z0, z1)) -> z0
   select(cons(z0, z1)) -> select(z1)
Tuples:
   SELECT(cons(z0, z1)) -> c2(SELECT(z1))
   F(node(s(x0), cons(z0, z1))) -> c(F(addchild(z0, node(x0, cons(z0, z1)))), SELECT(cons(z0, z1)))
   F(node(s(x0), cons(z0, z1))) -> c(F(addchild(select(z1), node(x0, cons(z0, z1)))), SELECT(cons(z0, z1)))
S tuples:
   SELECT(cons(z0, z1)) -> c2(SELECT(z1))
   F(node(s(x0), cons(z0, z1))) -> c(F(addchild(z0, node(x0, cons(z0, z1)))), SELECT(cons(z0, z1)))
   F(node(s(x0), cons(z0, z1))) -> c(F(addchild(select(z1), node(x0, cons(z0, z1)))), SELECT(cons(z0, z1)))
K tuples:none
Defined Rule Symbols:   addchild_2, select_1

Defined Pair Symbols:   SELECT_1, F_1

Compound Symbols:   c2_1, c_2


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

(53) CdtNarrowingProof (BOTH BOUNDS(ID, ID))
Use narrowing to replace F(node(s(x0), cons(z0, z1))) -> c(F(addchild(z0, node(x0, cons(z0, z1)))), SELECT(cons(z0, z1))) by 
   F(node(s(z2), cons(node(z0, z1), x2))) -> c(F(node(z0, cons(node(z2, cons(node(z0, z1), x2)), z1))), SELECT(cons(node(z0, z1), x2)))
   F(node(s(x0), cons(x1, x2))) -> c(SELECT(cons(x1, x2)))

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

(54)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   addchild(node(z0, z1), node(z2, z3)) -> node(z0, cons(node(z2, z3), z1))
   select(cons(z0, z1)) -> z0
   select(cons(z0, z1)) -> select(z1)
Tuples:
   SELECT(cons(z0, z1)) -> c2(SELECT(z1))
   F(node(s(x0), cons(z0, z1))) -> c(F(addchild(select(z1), node(x0, cons(z0, z1)))), SELECT(cons(z0, z1)))
   F(node(s(z2), cons(node(z0, z1), x2))) -> c(F(node(z0, cons(node(z2, cons(node(z0, z1), x2)), z1))), SELECT(cons(node(z0, z1), x2)))
   F(node(s(x0), cons(x1, x2))) -> c(SELECT(cons(x1, x2)))
S tuples:
   SELECT(cons(z0, z1)) -> c2(SELECT(z1))
   F(node(s(x0), cons(z0, z1))) -> c(F(addchild(select(z1), node(x0, cons(z0, z1)))), SELECT(cons(z0, z1)))
   F(node(s(z2), cons(node(z0, z1), x2))) -> c(F(node(z0, cons(node(z2, cons(node(z0, z1), x2)), z1))), SELECT(cons(node(z0, z1), x2)))
   F(node(s(x0), cons(x1, x2))) -> c(SELECT(cons(x1, x2)))
K tuples:none
Defined Rule Symbols:   addchild_2, select_1

Defined Pair Symbols:   SELECT_1, F_1

Compound Symbols:   c2_1, c_2, c_1


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

(55) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)))
Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.
   F(node(s(x0), cons(x1, x2))) -> c(SELECT(cons(x1, x2)))
We considered the (Usable) Rules:none
And the Tuples:
   SELECT(cons(z0, z1)) -> c2(SELECT(z1))
   F(node(s(x0), cons(z0, z1))) -> c(F(addchild(select(z1), node(x0, cons(z0, z1)))), SELECT(cons(z0, z1)))
   F(node(s(z2), cons(node(z0, z1), x2))) -> c(F(node(z0, cons(node(z2, cons(node(z0, z1), x2)), z1))), SELECT(cons(node(z0, z1), x2)))
   F(node(s(x0), cons(x1, x2))) -> c(SELECT(cons(x1, x2)))
The order we found is given by the following interpretation:

Polynomial interpretation :

   POL(F(x_1)) = [1]
   POL(SELECT(x_1)) = 0
   POL(addchild(x_1, x_2)) = [1] + x_1
   POL(c(x_1)) = x_1
   POL(c(x_1, x_2)) = x_1 + x_2
   POL(c2(x_1)) = x_1
   POL(cons(x_1, x_2)) = [1] + x_1 + x_2
   POL(node(x_1, x_2)) = [1] + x_1 + x_2
   POL(s(x_1)) = [1] + x_1
   POL(select(x_1)) = [1] + x_1

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

(56)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   addchild(node(z0, z1), node(z2, z3)) -> node(z0, cons(node(z2, z3), z1))
   select(cons(z0, z1)) -> z0
   select(cons(z0, z1)) -> select(z1)
Tuples:
   SELECT(cons(z0, z1)) -> c2(SELECT(z1))
   F(node(s(x0), cons(z0, z1))) -> c(F(addchild(select(z1), node(x0, cons(z0, z1)))), SELECT(cons(z0, z1)))
   F(node(s(z2), cons(node(z0, z1), x2))) -> c(F(node(z0, cons(node(z2, cons(node(z0, z1), x2)), z1))), SELECT(cons(node(z0, z1), x2)))
   F(node(s(x0), cons(x1, x2))) -> c(SELECT(cons(x1, x2)))
S tuples:
   SELECT(cons(z0, z1)) -> c2(SELECT(z1))
   F(node(s(x0), cons(z0, z1))) -> c(F(addchild(select(z1), node(x0, cons(z0, z1)))), SELECT(cons(z0, z1)))
   F(node(s(z2), cons(node(z0, z1), x2))) -> c(F(node(z0, cons(node(z2, cons(node(z0, z1), x2)), z1))), SELECT(cons(node(z0, z1), x2)))
K tuples:
   F(node(s(x0), cons(x1, x2))) -> c(SELECT(cons(x1, x2)))
Defined Rule Symbols:   addchild_2, select_1

Defined Pair Symbols:   SELECT_1, F_1

Compound Symbols:   c2_1, c_2, c_1


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

(57) CdtNarrowingProof (BOTH BOUNDS(ID, ID))
Use narrowing to replace F(node(s(x0), cons(z0, z1))) -> c(F(addchild(select(z1), node(x0, cons(z0, z1)))), SELECT(cons(z0, z1))) by 
   F(node(s(x0), cons(x1, cons(z0, z1)))) -> c(F(addchild(z0, node(x0, cons(x1, cons(z0, z1))))), SELECT(cons(x1, cons(z0, z1))))
   F(node(s(x0), cons(x1, cons(z0, z1)))) -> c(F(addchild(select(z1), node(x0, cons(x1, cons(z0, z1))))), SELECT(cons(x1, cons(z0, z1))))
   F(node(s(x0), cons(x1, x2))) -> c(SELECT(cons(x1, x2)))

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

(58)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   addchild(node(z0, z1), node(z2, z3)) -> node(z0, cons(node(z2, z3), z1))
   select(cons(z0, z1)) -> z0
   select(cons(z0, z1)) -> select(z1)
Tuples:
   SELECT(cons(z0, z1)) -> c2(SELECT(z1))
   F(node(s(z2), cons(node(z0, z1), x2))) -> c(F(node(z0, cons(node(z2, cons(node(z0, z1), x2)), z1))), SELECT(cons(node(z0, z1), x2)))
   F(node(s(x0), cons(x1, x2))) -> c(SELECT(cons(x1, x2)))
   F(node(s(x0), cons(x1, cons(z0, z1)))) -> c(F(addchild(z0, node(x0, cons(x1, cons(z0, z1))))), SELECT(cons(x1, cons(z0, z1))))
   F(node(s(x0), cons(x1, cons(z0, z1)))) -> c(F(addchild(select(z1), node(x0, cons(x1, cons(z0, z1))))), SELECT(cons(x1, cons(z0, z1))))
S tuples:
   SELECT(cons(z0, z1)) -> c2(SELECT(z1))
   F(node(s(z2), cons(node(z0, z1), x2))) -> c(F(node(z0, cons(node(z2, cons(node(z0, z1), x2)), z1))), SELECT(cons(node(z0, z1), x2)))
   F(node(s(x0), cons(x1, cons(z0, z1)))) -> c(F(addchild(z0, node(x0, cons(x1, cons(z0, z1))))), SELECT(cons(x1, cons(z0, z1))))
   F(node(s(x0), cons(x1, cons(z0, z1)))) -> c(F(addchild(select(z1), node(x0, cons(x1, cons(z0, z1))))), SELECT(cons(x1, cons(z0, z1))))
   F(node(s(x0), cons(x1, x2))) -> c(SELECT(cons(x1, x2)))
K tuples:
   F(node(s(x0), cons(x1, x2))) -> c(SELECT(cons(x1, x2)))
Defined Rule Symbols:   addchild_2, select_1

Defined Pair Symbols:   SELECT_1, F_1

Compound Symbols:   c2_1, c_2, c_1


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

(59) CdtKnowledgeProof (BOTH BOUNDS(ID, ID))
The following tuples could be moved from S to K by knowledge propagation:
   F(node(s(x0), cons(x1, x2))) -> c(SELECT(cons(x1, x2)))
   F(node(s(x0), cons(x1, x2))) -> c(SELECT(cons(x1, x2)))

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

(60)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   addchild(node(z0, z1), node(z2, z3)) -> node(z0, cons(node(z2, z3), z1))
   select(cons(z0, z1)) -> z0
   select(cons(z0, z1)) -> select(z1)
Tuples:
   SELECT(cons(z0, z1)) -> c2(SELECT(z1))
   F(node(s(z2), cons(node(z0, z1), x2))) -> c(F(node(z0, cons(node(z2, cons(node(z0, z1), x2)), z1))), SELECT(cons(node(z0, z1), x2)))
   F(node(s(x0), cons(x1, x2))) -> c(SELECT(cons(x1, x2)))
   F(node(s(x0), cons(x1, cons(z0, z1)))) -> c(F(addchild(z0, node(x0, cons(x1, cons(z0, z1))))), SELECT(cons(x1, cons(z0, z1))))
   F(node(s(x0), cons(x1, cons(z0, z1)))) -> c(F(addchild(select(z1), node(x0, cons(x1, cons(z0, z1))))), SELECT(cons(x1, cons(z0, z1))))
S tuples:
   SELECT(cons(z0, z1)) -> c2(SELECT(z1))
   F(node(s(z2), cons(node(z0, z1), x2))) -> c(F(node(z0, cons(node(z2, cons(node(z0, z1), x2)), z1))), SELECT(cons(node(z0, z1), x2)))
   F(node(s(x0), cons(x1, cons(z0, z1)))) -> c(F(addchild(z0, node(x0, cons(x1, cons(z0, z1))))), SELECT(cons(x1, cons(z0, z1))))
   F(node(s(x0), cons(x1, cons(z0, z1)))) -> c(F(addchild(select(z1), node(x0, cons(x1, cons(z0, z1))))), SELECT(cons(x1, cons(z0, z1))))
K tuples:
   F(node(s(x0), cons(x1, x2))) -> c(SELECT(cons(x1, x2)))
Defined Rule Symbols:   addchild_2, select_1

Defined Pair Symbols:   SELECT_1, F_1

Compound Symbols:   c2_1, c_2, c_1


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

(61) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID))
Use forward instantiation to replace SELECT(cons(z0, z1)) -> c2(SELECT(z1)) by 
   SELECT(cons(z0, cons(y0, y1))) -> c2(SELECT(cons(y0, y1)))

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

(62)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   addchild(node(z0, z1), node(z2, z3)) -> node(z0, cons(node(z2, z3), z1))
   select(cons(z0, z1)) -> z0
   select(cons(z0, z1)) -> select(z1)
Tuples:
   F(node(s(z2), cons(node(z0, z1), x2))) -> c(F(node(z0, cons(node(z2, cons(node(z0, z1), x2)), z1))), SELECT(cons(node(z0, z1), x2)))
   F(node(s(x0), cons(x1, x2))) -> c(SELECT(cons(x1, x2)))
   F(node(s(x0), cons(x1, cons(z0, z1)))) -> c(F(addchild(z0, node(x0, cons(x1, cons(z0, z1))))), SELECT(cons(x1, cons(z0, z1))))
   F(node(s(x0), cons(x1, cons(z0, z1)))) -> c(F(addchild(select(z1), node(x0, cons(x1, cons(z0, z1))))), SELECT(cons(x1, cons(z0, z1))))
   SELECT(cons(z0, cons(y0, y1))) -> c2(SELECT(cons(y0, y1)))
S tuples:
   F(node(s(z2), cons(node(z0, z1), x2))) -> c(F(node(z0, cons(node(z2, cons(node(z0, z1), x2)), z1))), SELECT(cons(node(z0, z1), x2)))
   F(node(s(x0), cons(x1, cons(z0, z1)))) -> c(F(addchild(z0, node(x0, cons(x1, cons(z0, z1))))), SELECT(cons(x1, cons(z0, z1))))
   F(node(s(x0), cons(x1, cons(z0, z1)))) -> c(F(addchild(select(z1), node(x0, cons(x1, cons(z0, z1))))), SELECT(cons(x1, cons(z0, z1))))
   SELECT(cons(z0, cons(y0, y1))) -> c2(SELECT(cons(y0, y1)))
K tuples:
   F(node(s(x0), cons(x1, x2))) -> c(SELECT(cons(x1, x2)))
Defined Rule Symbols:   addchild_2, select_1

Defined Pair Symbols:   F_1, SELECT_1

Compound Symbols:   c_2, c_1, c2_1


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

(63) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID))
Use forward instantiation to replace F(node(s(z2), cons(node(z0, z1), x2))) -> c(F(node(z0, cons(node(z2, cons(node(z0, z1), x2)), z1))), SELECT(cons(node(z0, z1), x2))) by 
   F(node(s(z0), cons(node(s(y0), z2), z3))) -> c(F(node(s(y0), cons(node(z0, cons(node(s(y0), z2), z3)), z2))), SELECT(cons(node(s(y0), z2), z3)))
   F(node(s(z0), cons(node(s(y0), cons(y2, y3)), z3))) -> c(F(node(s(y0), cons(node(z0, cons(node(s(y0), cons(y2, y3)), z3)), cons(y2, y3)))), SELECT(cons(node(s(y0), cons(y2, y3)), z3)))
   F(node(s(z0), cons(node(z1, z2), cons(y1, y2)))) -> c(F(node(z1, cons(node(z0, cons(node(z1, z2), cons(y1, y2))), z2))), SELECT(cons(node(z1, z2), cons(y1, y2))))

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

(64)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   addchild(node(z0, z1), node(z2, z3)) -> node(z0, cons(node(z2, z3), z1))
   select(cons(z0, z1)) -> z0
   select(cons(z0, z1)) -> select(z1)
Tuples:
   F(node(s(x0), cons(x1, x2))) -> c(SELECT(cons(x1, x2)))
   F(node(s(x0), cons(x1, cons(z0, z1)))) -> c(F(addchild(z0, node(x0, cons(x1, cons(z0, z1))))), SELECT(cons(x1, cons(z0, z1))))
   F(node(s(x0), cons(x1, cons(z0, z1)))) -> c(F(addchild(select(z1), node(x0, cons(x1, cons(z0, z1))))), SELECT(cons(x1, cons(z0, z1))))
   SELECT(cons(z0, cons(y0, y1))) -> c2(SELECT(cons(y0, y1)))
   F(node(s(z0), cons(node(s(y0), z2), z3))) -> c(F(node(s(y0), cons(node(z0, cons(node(s(y0), z2), z3)), z2))), SELECT(cons(node(s(y0), z2), z3)))
   F(node(s(z0), cons(node(s(y0), cons(y2, y3)), z3))) -> c(F(node(s(y0), cons(node(z0, cons(node(s(y0), cons(y2, y3)), z3)), cons(y2, y3)))), SELECT(cons(node(s(y0), cons(y2, y3)), z3)))
   F(node(s(z0), cons(node(z1, z2), cons(y1, y2)))) -> c(F(node(z1, cons(node(z0, cons(node(z1, z2), cons(y1, y2))), z2))), SELECT(cons(node(z1, z2), cons(y1, y2))))
S tuples:
   F(node(s(x0), cons(x1, cons(z0, z1)))) -> c(F(addchild(z0, node(x0, cons(x1, cons(z0, z1))))), SELECT(cons(x1, cons(z0, z1))))
   F(node(s(x0), cons(x1, cons(z0, z1)))) -> c(F(addchild(select(z1), node(x0, cons(x1, cons(z0, z1))))), SELECT(cons(x1, cons(z0, z1))))
   SELECT(cons(z0, cons(y0, y1))) -> c2(SELECT(cons(y0, y1)))
   F(node(s(z0), cons(node(s(y0), z2), z3))) -> c(F(node(s(y0), cons(node(z0, cons(node(s(y0), z2), z3)), z2))), SELECT(cons(node(s(y0), z2), z3)))
   F(node(s(z0), cons(node(s(y0), cons(y2, y3)), z3))) -> c(F(node(s(y0), cons(node(z0, cons(node(s(y0), cons(y2, y3)), z3)), cons(y2, y3)))), SELECT(cons(node(s(y0), cons(y2, y3)), z3)))
   F(node(s(z0), cons(node(z1, z2), cons(y1, y2)))) -> c(F(node(z1, cons(node(z0, cons(node(z1, z2), cons(y1, y2))), z2))), SELECT(cons(node(z1, z2), cons(y1, y2))))
K tuples:
   F(node(s(x0), cons(x1, x2))) -> c(SELECT(cons(x1, x2)))
Defined Rule Symbols:   addchild_2, select_1

Defined Pair Symbols:   F_1, SELECT_1

Compound Symbols:   c_1, c_2, c2_1


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

(65) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID))
Use forward instantiation to replace F(node(s(x0), cons(x1, x2))) -> c(SELECT(cons(x1, x2))) by 
   F(node(s(z0), cons(z1, cons(y1, y2)))) -> c(SELECT(cons(z1, cons(y1, y2))))

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

(66)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   addchild(node(z0, z1), node(z2, z3)) -> node(z0, cons(node(z2, z3), z1))
   select(cons(z0, z1)) -> z0
   select(cons(z0, z1)) -> select(z1)
Tuples:
   F(node(s(x0), cons(x1, x2))) -> c(SELECT(cons(x1, x2)))
   F(node(s(x0), cons(x1, cons(z0, z1)))) -> c(F(addchild(z0, node(x0, cons(x1, cons(z0, z1))))), SELECT(cons(x1, cons(z0, z1))))
   F(node(s(x0), cons(x1, cons(z0, z1)))) -> c(F(addchild(select(z1), node(x0, cons(x1, cons(z0, z1))))), SELECT(cons(x1, cons(z0, z1))))
   SELECT(cons(z0, cons(y0, y1))) -> c2(SELECT(cons(y0, y1)))
   F(node(s(z0), cons(node(s(y0), z2), z3))) -> c(F(node(s(y0), cons(node(z0, cons(node(s(y0), z2), z3)), z2))), SELECT(cons(node(s(y0), z2), z3)))
   F(node(s(z0), cons(node(s(y0), cons(y2, y3)), z3))) -> c(F(node(s(y0), cons(node(z0, cons(node(s(y0), cons(y2, y3)), z3)), cons(y2, y3)))), SELECT(cons(node(s(y0), cons(y2, y3)), z3)))
   F(node(s(z0), cons(node(z1, z2), cons(y1, y2)))) -> c(F(node(z1, cons(node(z0, cons(node(z1, z2), cons(y1, y2))), z2))), SELECT(cons(node(z1, z2), cons(y1, y2))))
   F(node(s(z0), cons(z1, cons(y1, y2)))) -> c(SELECT(cons(z1, cons(y1, y2))))
S tuples:
   F(node(s(x0), cons(x1, cons(z0, z1)))) -> c(F(addchild(z0, node(x0, cons(x1, cons(z0, z1))))), SELECT(cons(x1, cons(z0, z1))))
   F(node(s(x0), cons(x1, cons(z0, z1)))) -> c(F(addchild(select(z1), node(x0, cons(x1, cons(z0, z1))))), SELECT(cons(x1, cons(z0, z1))))
   SELECT(cons(z0, cons(y0, y1))) -> c2(SELECT(cons(y0, y1)))
   F(node(s(z0), cons(node(s(y0), z2), z3))) -> c(F(node(s(y0), cons(node(z0, cons(node(s(y0), z2), z3)), z2))), SELECT(cons(node(s(y0), z2), z3)))
   F(node(s(z0), cons(node(s(y0), cons(y2, y3)), z3))) -> c(F(node(s(y0), cons(node(z0, cons(node(s(y0), cons(y2, y3)), z3)), cons(y2, y3)))), SELECT(cons(node(s(y0), cons(y2, y3)), z3)))
   F(node(s(z0), cons(node(z1, z2), cons(y1, y2)))) -> c(F(node(z1, cons(node(z0, cons(node(z1, z2), cons(y1, y2))), z2))), SELECT(cons(node(z1, z2), cons(y1, y2))))
K tuples:
   F(node(s(z0), cons(z1, cons(y1, y2)))) -> c(SELECT(cons(z1, cons(y1, y2))))
Defined Rule Symbols:   addchild_2, select_1

Defined Pair Symbols:   F_1, SELECT_1

Compound Symbols:   c_1, c_2, c2_1


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

(67) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID))
Use forward instantiation to replace F(node(s(x0), cons(x1, x2))) -> c(SELECT(cons(x1, x2))) by 
   F(node(s(z0), cons(z1, cons(y1, y2)))) -> c(SELECT(cons(z1, cons(y1, y2))))

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

(68)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   addchild(node(z0, z1), node(z2, z3)) -> node(z0, cons(node(z2, z3), z1))
   select(cons(z0, z1)) -> z0
   select(cons(z0, z1)) -> select(z1)
Tuples:
   F(node(s(x0), cons(x1, cons(z0, z1)))) -> c(F(addchild(z0, node(x0, cons(x1, cons(z0, z1))))), SELECT(cons(x1, cons(z0, z1))))
   F(node(s(x0), cons(x1, cons(z0, z1)))) -> c(F(addchild(select(z1), node(x0, cons(x1, cons(z0, z1))))), SELECT(cons(x1, cons(z0, z1))))
   SELECT(cons(z0, cons(y0, y1))) -> c2(SELECT(cons(y0, y1)))
   F(node(s(z0), cons(node(s(y0), z2), z3))) -> c(F(node(s(y0), cons(node(z0, cons(node(s(y0), z2), z3)), z2))), SELECT(cons(node(s(y0), z2), z3)))
   F(node(s(z0), cons(node(s(y0), cons(y2, y3)), z3))) -> c(F(node(s(y0), cons(node(z0, cons(node(s(y0), cons(y2, y3)), z3)), cons(y2, y3)))), SELECT(cons(node(s(y0), cons(y2, y3)), z3)))
   F(node(s(z0), cons(node(z1, z2), cons(y1, y2)))) -> c(F(node(z1, cons(node(z0, cons(node(z1, z2), cons(y1, y2))), z2))), SELECT(cons(node(z1, z2), cons(y1, y2))))
   F(node(s(z0), cons(z1, cons(y1, y2)))) -> c(SELECT(cons(z1, cons(y1, y2))))
S tuples:
   F(node(s(x0), cons(x1, cons(z0, z1)))) -> c(F(addchild(z0, node(x0, cons(x1, cons(z0, z1))))), SELECT(cons(x1, cons(z0, z1))))
   F(node(s(x0), cons(x1, cons(z0, z1)))) -> c(F(addchild(select(z1), node(x0, cons(x1, cons(z0, z1))))), SELECT(cons(x1, cons(z0, z1))))
   SELECT(cons(z0, cons(y0, y1))) -> c2(SELECT(cons(y0, y1)))
   F(node(s(z0), cons(node(s(y0), z2), z3))) -> c(F(node(s(y0), cons(node(z0, cons(node(s(y0), z2), z3)), z2))), SELECT(cons(node(s(y0), z2), z3)))
   F(node(s(z0), cons(node(s(y0), cons(y2, y3)), z3))) -> c(F(node(s(y0), cons(node(z0, cons(node(s(y0), cons(y2, y3)), z3)), cons(y2, y3)))), SELECT(cons(node(s(y0), cons(y2, y3)), z3)))
   F(node(s(z0), cons(node(z1, z2), cons(y1, y2)))) -> c(F(node(z1, cons(node(z0, cons(node(z1, z2), cons(y1, y2))), z2))), SELECT(cons(node(z1, z2), cons(y1, y2))))
K tuples:
   F(node(s(z0), cons(z1, cons(y1, y2)))) -> c(SELECT(cons(z1, cons(y1, y2))))
Defined Rule Symbols:   addchild_2, select_1

Defined Pair Symbols:   F_1, SELECT_1

Compound Symbols:   c_2, c2_1, c_1


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

(69) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID))
Use forward instantiation to replace SELECT(cons(z0, cons(y0, y1))) -> c2(SELECT(cons(y0, y1))) by 
   SELECT(cons(z0, cons(z1, cons(y1, y2)))) -> c2(SELECT(cons(z1, cons(y1, y2))))

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

(70)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   addchild(node(z0, z1), node(z2, z3)) -> node(z0, cons(node(z2, z3), z1))
   select(cons(z0, z1)) -> z0
   select(cons(z0, z1)) -> select(z1)
Tuples:
   F(node(s(x0), cons(x1, cons(z0, z1)))) -> c(F(addchild(z0, node(x0, cons(x1, cons(z0, z1))))), SELECT(cons(x1, cons(z0, z1))))
   F(node(s(x0), cons(x1, cons(z0, z1)))) -> c(F(addchild(select(z1), node(x0, cons(x1, cons(z0, z1))))), SELECT(cons(x1, cons(z0, z1))))
   F(node(s(z0), cons(node(s(y0), z2), z3))) -> c(F(node(s(y0), cons(node(z0, cons(node(s(y0), z2), z3)), z2))), SELECT(cons(node(s(y0), z2), z3)))
   F(node(s(z0), cons(node(s(y0), cons(y2, y3)), z3))) -> c(F(node(s(y0), cons(node(z0, cons(node(s(y0), cons(y2, y3)), z3)), cons(y2, y3)))), SELECT(cons(node(s(y0), cons(y2, y3)), z3)))
   F(node(s(z0), cons(node(z1, z2), cons(y1, y2)))) -> c(F(node(z1, cons(node(z0, cons(node(z1, z2), cons(y1, y2))), z2))), SELECT(cons(node(z1, z2), cons(y1, y2))))
   F(node(s(z0), cons(z1, cons(y1, y2)))) -> c(SELECT(cons(z1, cons(y1, y2))))
   SELECT(cons(z0, cons(z1, cons(y1, y2)))) -> c2(SELECT(cons(z1, cons(y1, y2))))
S tuples:
   F(node(s(x0), cons(x1, cons(z0, z1)))) -> c(F(addchild(z0, node(x0, cons(x1, cons(z0, z1))))), SELECT(cons(x1, cons(z0, z1))))
   F(node(s(x0), cons(x1, cons(z0, z1)))) -> c(F(addchild(select(z1), node(x0, cons(x1, cons(z0, z1))))), SELECT(cons(x1, cons(z0, z1))))
   F(node(s(z0), cons(node(s(y0), z2), z3))) -> c(F(node(s(y0), cons(node(z0, cons(node(s(y0), z2), z3)), z2))), SELECT(cons(node(s(y0), z2), z3)))
   F(node(s(z0), cons(node(s(y0), cons(y2, y3)), z3))) -> c(F(node(s(y0), cons(node(z0, cons(node(s(y0), cons(y2, y3)), z3)), cons(y2, y3)))), SELECT(cons(node(s(y0), cons(y2, y3)), z3)))
   F(node(s(z0), cons(node(z1, z2), cons(y1, y2)))) -> c(F(node(z1, cons(node(z0, cons(node(z1, z2), cons(y1, y2))), z2))), SELECT(cons(node(z1, z2), cons(y1, y2))))
   SELECT(cons(z0, cons(z1, cons(y1, y2)))) -> c2(SELECT(cons(z1, cons(y1, y2))))
K tuples:
   F(node(s(z0), cons(z1, cons(y1, y2)))) -> c(SELECT(cons(z1, cons(y1, y2))))
Defined Rule Symbols:   addchild_2, select_1

Defined Pair Symbols:   F_1, SELECT_1

Compound Symbols:   c_2, c_1, c2_1


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

(71) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID))
Use forward instantiation to replace F(node(s(z0), cons(node(s(y0), z2), z3))) -> c(F(node(s(y0), cons(node(z0, cons(node(s(y0), z2), z3)), z2))), SELECT(cons(node(s(y0), z2), z3))) by 
   F(node(s(z0), cons(node(s(z1), cons(y2, y3)), z3))) -> c(F(node(s(z1), cons(node(z0, cons(node(s(z1), cons(y2, y3)), z3)), cons(y2, y3)))), SELECT(cons(node(s(z1), cons(y2, y3)), z3)))
   F(node(s(s(y1)), cons(node(s(z1), z2), z3))) -> c(F(node(s(z1), cons(node(s(y1), cons(node(s(z1), z2), z3)), z2))), SELECT(cons(node(s(z1), z2), z3)))
   F(node(s(z0), cons(node(s(z1), z2), cons(y1, cons(y2, y3))))) -> c(F(node(s(z1), cons(node(z0, cons(node(s(z1), z2), cons(y1, cons(y2, y3)))), z2))), SELECT(cons(node(s(z1), z2), cons(y1, cons(y2, y3)))))

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

(72)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   addchild(node(z0, z1), node(z2, z3)) -> node(z0, cons(node(z2, z3), z1))
   select(cons(z0, z1)) -> z0
   select(cons(z0, z1)) -> select(z1)
Tuples:
   F(node(s(x0), cons(x1, cons(z0, z1)))) -> c(F(addchild(z0, node(x0, cons(x1, cons(z0, z1))))), SELECT(cons(x1, cons(z0, z1))))
   F(node(s(x0), cons(x1, cons(z0, z1)))) -> c(F(addchild(select(z1), node(x0, cons(x1, cons(z0, z1))))), SELECT(cons(x1, cons(z0, z1))))
   F(node(s(z0), cons(node(s(y0), cons(y2, y3)), z3))) -> c(F(node(s(y0), cons(node(z0, cons(node(s(y0), cons(y2, y3)), z3)), cons(y2, y3)))), SELECT(cons(node(s(y0), cons(y2, y3)), z3)))
   F(node(s(z0), cons(node(z1, z2), cons(y1, y2)))) -> c(F(node(z1, cons(node(z0, cons(node(z1, z2), cons(y1, y2))), z2))), SELECT(cons(node(z1, z2), cons(y1, y2))))
   F(node(s(z0), cons(z1, cons(y1, y2)))) -> c(SELECT(cons(z1, cons(y1, y2))))
   SELECT(cons(z0, cons(z1, cons(y1, y2)))) -> c2(SELECT(cons(z1, cons(y1, y2))))
   F(node(s(s(y1)), cons(node(s(z1), z2), z3))) -> c(F(node(s(z1), cons(node(s(y1), cons(node(s(z1), z2), z3)), z2))), SELECT(cons(node(s(z1), z2), z3)))
   F(node(s(z0), cons(node(s(z1), z2), cons(y1, cons(y2, y3))))) -> c(F(node(s(z1), cons(node(z0, cons(node(s(z1), z2), cons(y1, cons(y2, y3)))), z2))), SELECT(cons(node(s(z1), z2), cons(y1, cons(y2, y3)))))
S tuples:
   F(node(s(x0), cons(x1, cons(z0, z1)))) -> c(F(addchild(z0, node(x0, cons(x1, cons(z0, z1))))), SELECT(cons(x1, cons(z0, z1))))
   F(node(s(x0), cons(x1, cons(z0, z1)))) -> c(F(addchild(select(z1), node(x0, cons(x1, cons(z0, z1))))), SELECT(cons(x1, cons(z0, z1))))
   F(node(s(z0), cons(node(s(y0), cons(y2, y3)), z3))) -> c(F(node(s(y0), cons(node(z0, cons(node(s(y0), cons(y2, y3)), z3)), cons(y2, y3)))), SELECT(cons(node(s(y0), cons(y2, y3)), z3)))
   F(node(s(z0), cons(node(z1, z2), cons(y1, y2)))) -> c(F(node(z1, cons(node(z0, cons(node(z1, z2), cons(y1, y2))), z2))), SELECT(cons(node(z1, z2), cons(y1, y2))))
   SELECT(cons(z0, cons(z1, cons(y1, y2)))) -> c2(SELECT(cons(z1, cons(y1, y2))))
   F(node(s(s(y1)), cons(node(s(z1), z2), z3))) -> c(F(node(s(z1), cons(node(s(y1), cons(node(s(z1), z2), z3)), z2))), SELECT(cons(node(s(z1), z2), z3)))
   F(node(s(z0), cons(node(s(z1), z2), cons(y1, cons(y2, y3))))) -> c(F(node(s(z1), cons(node(z0, cons(node(s(z1), z2), cons(y1, cons(y2, y3)))), z2))), SELECT(cons(node(s(z1), z2), cons(y1, cons(y2, y3)))))
K tuples:
   F(node(s(z0), cons(z1, cons(y1, y2)))) -> c(SELECT(cons(z1, cons(y1, y2))))
Defined Rule Symbols:   addchild_2, select_1

Defined Pair Symbols:   F_1, SELECT_1

Compound Symbols:   c_2, c_1, c2_1


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

(73) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID))
Use forward instantiation to replace F(node(s(z0), cons(node(z1, z2), cons(y1, y2)))) -> c(F(node(z1, cons(node(z0, cons(node(z1, z2), cons(y1, y2))), z2))), SELECT(cons(node(z1, z2), cons(y1, y2)))) by 
   F(node(s(z0), cons(node(s(y0), cons(y2, y3)), cons(z3, z4)))) -> c(F(node(s(y0), cons(node(z0, cons(node(s(y0), cons(y2, y3)), cons(z3, z4))), cons(y2, y3)))), SELECT(cons(node(s(y0), cons(y2, y3)), cons(z3, z4))))
   F(node(s(s(y1)), cons(node(s(y0), z2), cons(z3, z4)))) -> c(F(node(s(y0), cons(node(s(y1), cons(node(s(y0), z2), cons(z3, z4))), z2))), SELECT(cons(node(s(y0), z2), cons(z3, z4))))
   F(node(s(z0), cons(node(z1, z2), cons(z3, cons(y2, y3))))) -> c(F(node(z1, cons(node(z0, cons(node(z1, z2), cons(z3, cons(y2, y3)))), z2))), SELECT(cons(node(z1, z2), cons(z3, cons(y2, y3)))))
   F(node(s(s(y1)), cons(node(s(s(y0)), z2), cons(z3, z4)))) -> c(F(node(s(s(y0)), cons(node(s(y1), cons(node(s(s(y0)), z2), cons(z3, z4))), z2))), SELECT(cons(node(s(s(y0)), z2), cons(z3, z4))))
   F(node(s(s(y1)), cons(node(s(y0), cons(y3, cons(y4, y5))), cons(z3, z4)))) -> c(F(node(s(y0), cons(node(s(y1), cons(node(s(y0), cons(y3, cons(y4, y5))), cons(z3, z4))), cons(y3, cons(y4, y5))))), SELECT(cons(node(s(y0), cons(y3, cons(y4, y5))), cons(z3, z4))))

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

(74)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   addchild(node(z0, z1), node(z2, z3)) -> node(z0, cons(node(z2, z3), z1))
   select(cons(z0, z1)) -> z0
   select(cons(z0, z1)) -> select(z1)
Tuples:
   F(node(s(x0), cons(x1, cons(z0, z1)))) -> c(F(addchild(z0, node(x0, cons(x1, cons(z0, z1))))), SELECT(cons(x1, cons(z0, z1))))
   F(node(s(x0), cons(x1, cons(z0, z1)))) -> c(F(addchild(select(z1), node(x0, cons(x1, cons(z0, z1))))), SELECT(cons(x1, cons(z0, z1))))
   F(node(s(z0), cons(node(s(y0), cons(y2, y3)), z3))) -> c(F(node(s(y0), cons(node(z0, cons(node(s(y0), cons(y2, y3)), z3)), cons(y2, y3)))), SELECT(cons(node(s(y0), cons(y2, y3)), z3)))
   F(node(s(z0), cons(z1, cons(y1, y2)))) -> c(SELECT(cons(z1, cons(y1, y2))))
   SELECT(cons(z0, cons(z1, cons(y1, y2)))) -> c2(SELECT(cons(z1, cons(y1, y2))))
   F(node(s(s(y1)), cons(node(s(z1), z2), z3))) -> c(F(node(s(z1), cons(node(s(y1), cons(node(s(z1), z2), z3)), z2))), SELECT(cons(node(s(z1), z2), z3)))
   F(node(s(z0), cons(node(s(z1), z2), cons(y1, cons(y2, y3))))) -> c(F(node(s(z1), cons(node(z0, cons(node(s(z1), z2), cons(y1, cons(y2, y3)))), z2))), SELECT(cons(node(s(z1), z2), cons(y1, cons(y2, y3)))))
   F(node(s(z0), cons(node(s(y0), cons(y2, y3)), cons(z3, z4)))) -> c(F(node(s(y0), cons(node(z0, cons(node(s(y0), cons(y2, y3)), cons(z3, z4))), cons(y2, y3)))), SELECT(cons(node(s(y0), cons(y2, y3)), cons(z3, z4))))
   F(node(s(s(y1)), cons(node(s(y0), z2), cons(z3, z4)))) -> c(F(node(s(y0), cons(node(s(y1), cons(node(s(y0), z2), cons(z3, z4))), z2))), SELECT(cons(node(s(y0), z2), cons(z3, z4))))
   F(node(s(z0), cons(node(z1, z2), cons(z3, cons(y2, y3))))) -> c(F(node(z1, cons(node(z0, cons(node(z1, z2), cons(z3, cons(y2, y3)))), z2))), SELECT(cons(node(z1, z2), cons(z3, cons(y2, y3)))))
   F(node(s(s(y1)), cons(node(s(s(y0)), z2), cons(z3, z4)))) -> c(F(node(s(s(y0)), cons(node(s(y1), cons(node(s(s(y0)), z2), cons(z3, z4))), z2))), SELECT(cons(node(s(s(y0)), z2), cons(z3, z4))))
   F(node(s(s(y1)), cons(node(s(y0), cons(y3, cons(y4, y5))), cons(z3, z4)))) -> c(F(node(s(y0), cons(node(s(y1), cons(node(s(y0), cons(y3, cons(y4, y5))), cons(z3, z4))), cons(y3, cons(y4, y5))))), SELECT(cons(node(s(y0), cons(y3, cons(y4, y5))), cons(z3, z4))))
S tuples:
   F(node(s(x0), cons(x1, cons(z0, z1)))) -> c(F(addchild(z0, node(x0, cons(x1, cons(z0, z1))))), SELECT(cons(x1, cons(z0, z1))))
   F(node(s(x0), cons(x1, cons(z0, z1)))) -> c(F(addchild(select(z1), node(x0, cons(x1, cons(z0, z1))))), SELECT(cons(x1, cons(z0, z1))))
   F(node(s(z0), cons(node(s(y0), cons(y2, y3)), z3))) -> c(F(node(s(y0), cons(node(z0, cons(node(s(y0), cons(y2, y3)), z3)), cons(y2, y3)))), SELECT(cons(node(s(y0), cons(y2, y3)), z3)))
   SELECT(cons(z0, cons(z1, cons(y1, y2)))) -> c2(SELECT(cons(z1, cons(y1, y2))))
   F(node(s(s(y1)), cons(node(s(z1), z2), z3))) -> c(F(node(s(z1), cons(node(s(y1), cons(node(s(z1), z2), z3)), z2))), SELECT(cons(node(s(z1), z2), z3)))
   F(node(s(z0), cons(node(s(z1), z2), cons(y1, cons(y2, y3))))) -> c(F(node(s(z1), cons(node(z0, cons(node(s(z1), z2), cons(y1, cons(y2, y3)))), z2))), SELECT(cons(node(s(z1), z2), cons(y1, cons(y2, y3)))))
   F(node(s(z0), cons(node(s(y0), cons(y2, y3)), cons(z3, z4)))) -> c(F(node(s(y0), cons(node(z0, cons(node(s(y0), cons(y2, y3)), cons(z3, z4))), cons(y2, y3)))), SELECT(cons(node(s(y0), cons(y2, y3)), cons(z3, z4))))
   F(node(s(s(y1)), cons(node(s(y0), z2), cons(z3, z4)))) -> c(F(node(s(y0), cons(node(s(y1), cons(node(s(y0), z2), cons(z3, z4))), z2))), SELECT(cons(node(s(y0), z2), cons(z3, z4))))
   F(node(s(z0), cons(node(z1, z2), cons(z3, cons(y2, y3))))) -> c(F(node(z1, cons(node(z0, cons(node(z1, z2), cons(z3, cons(y2, y3)))), z2))), SELECT(cons(node(z1, z2), cons(z3, cons(y2, y3)))))
   F(node(s(s(y1)), cons(node(s(s(y0)), z2), cons(z3, z4)))) -> c(F(node(s(s(y0)), cons(node(s(y1), cons(node(s(s(y0)), z2), cons(z3, z4))), z2))), SELECT(cons(node(s(s(y0)), z2), cons(z3, z4))))
   F(node(s(s(y1)), cons(node(s(y0), cons(y3, cons(y4, y5))), cons(z3, z4)))) -> c(F(node(s(y0), cons(node(s(y1), cons(node(s(y0), cons(y3, cons(y4, y5))), cons(z3, z4))), cons(y3, cons(y4, y5))))), SELECT(cons(node(s(y0), cons(y3, cons(y4, y5))), cons(z3, z4))))
K tuples:
   F(node(s(z0), cons(z1, cons(y1, y2)))) -> c(SELECT(cons(z1, cons(y1, y2))))
Defined Rule Symbols:   addchild_2, select_1

Defined Pair Symbols:   F_1, SELECT_1

Compound Symbols:   c_2, c_1, c2_1


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

(75) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID))
Use forward instantiation to replace F(node(s(z0), cons(z1, cons(y1, y2)))) -> c(SELECT(cons(z1, cons(y1, y2)))) by 
   F(node(s(z0), cons(z1, cons(z2, cons(y2, y3))))) -> c(SELECT(cons(z1, cons(z2, cons(y2, y3)))))

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

(76)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   addchild(node(z0, z1), node(z2, z3)) -> node(z0, cons(node(z2, z3), z1))
   select(cons(z0, z1)) -> z0
   select(cons(z0, z1)) -> select(z1)
Tuples:
   F(node(s(x0), cons(x1, cons(z0, z1)))) -> c(F(addchild(z0, node(x0, cons(x1, cons(z0, z1))))), SELECT(cons(x1, cons(z0, z1))))
   F(node(s(x0), cons(x1, cons(z0, z1)))) -> c(F(addchild(select(z1), node(x0, cons(x1, cons(z0, z1))))), SELECT(cons(x1, cons(z0, z1))))
   F(node(s(z0), cons(node(s(y0), cons(y2, y3)), z3))) -> c(F(node(s(y0), cons(node(z0, cons(node(s(y0), cons(y2, y3)), z3)), cons(y2, y3)))), SELECT(cons(node(s(y0), cons(y2, y3)), z3)))
   F(node(s(z0), cons(z1, cons(y1, y2)))) -> c(SELECT(cons(z1, cons(y1, y2))))
   SELECT(cons(z0, cons(z1, cons(y1, y2)))) -> c2(SELECT(cons(z1, cons(y1, y2))))
   F(node(s(s(y1)), cons(node(s(z1), z2), z3))) -> c(F(node(s(z1), cons(node(s(y1), cons(node(s(z1), z2), z3)), z2))), SELECT(cons(node(s(z1), z2), z3)))
   F(node(s(z0), cons(node(s(z1), z2), cons(y1, cons(y2, y3))))) -> c(F(node(s(z1), cons(node(z0, cons(node(s(z1), z2), cons(y1, cons(y2, y3)))), z2))), SELECT(cons(node(s(z1), z2), cons(y1, cons(y2, y3)))))
   F(node(s(z0), cons(node(s(y0), cons(y2, y3)), cons(z3, z4)))) -> c(F(node(s(y0), cons(node(z0, cons(node(s(y0), cons(y2, y3)), cons(z3, z4))), cons(y2, y3)))), SELECT(cons(node(s(y0), cons(y2, y3)), cons(z3, z4))))
   F(node(s(s(y1)), cons(node(s(y0), z2), cons(z3, z4)))) -> c(F(node(s(y0), cons(node(s(y1), cons(node(s(y0), z2), cons(z3, z4))), z2))), SELECT(cons(node(s(y0), z2), cons(z3, z4))))
   F(node(s(z0), cons(node(z1, z2), cons(z3, cons(y2, y3))))) -> c(F(node(z1, cons(node(z0, cons(node(z1, z2), cons(z3, cons(y2, y3)))), z2))), SELECT(cons(node(z1, z2), cons(z3, cons(y2, y3)))))
   F(node(s(s(y1)), cons(node(s(s(y0)), z2), cons(z3, z4)))) -> c(F(node(s(s(y0)), cons(node(s(y1), cons(node(s(s(y0)), z2), cons(z3, z4))), z2))), SELECT(cons(node(s(s(y0)), z2), cons(z3, z4))))
   F(node(s(s(y1)), cons(node(s(y0), cons(y3, cons(y4, y5))), cons(z3, z4)))) -> c(F(node(s(y0), cons(node(s(y1), cons(node(s(y0), cons(y3, cons(y4, y5))), cons(z3, z4))), cons(y3, cons(y4, y5))))), SELECT(cons(node(s(y0), cons(y3, cons(y4, y5))), cons(z3, z4))))
   F(node(s(z0), cons(z1, cons(z2, cons(y2, y3))))) -> c(SELECT(cons(z1, cons(z2, cons(y2, y3)))))
S tuples:
   F(node(s(x0), cons(x1, cons(z0, z1)))) -> c(F(addchild(z0, node(x0, cons(x1, cons(z0, z1))))), SELECT(cons(x1, cons(z0, z1))))
   F(node(s(x0), cons(x1, cons(z0, z1)))) -> c(F(addchild(select(z1), node(x0, cons(x1, cons(z0, z1))))), SELECT(cons(x1, cons(z0, z1))))
   F(node(s(z0), cons(node(s(y0), cons(y2, y3)), z3))) -> c(F(node(s(y0), cons(node(z0, cons(node(s(y0), cons(y2, y3)), z3)), cons(y2, y3)))), SELECT(cons(node(s(y0), cons(y2, y3)), z3)))
   SELECT(cons(z0, cons(z1, cons(y1, y2)))) -> c2(SELECT(cons(z1, cons(y1, y2))))
   F(node(s(s(y1)), cons(node(s(z1), z2), z3))) -> c(F(node(s(z1), cons(node(s(y1), cons(node(s(z1), z2), z3)), z2))), SELECT(cons(node(s(z1), z2), z3)))
   F(node(s(z0), cons(node(s(z1), z2), cons(y1, cons(y2, y3))))) -> c(F(node(s(z1), cons(node(z0, cons(node(s(z1), z2), cons(y1, cons(y2, y3)))), z2))), SELECT(cons(node(s(z1), z2), cons(y1, cons(y2, y3)))))
   F(node(s(z0), cons(node(s(y0), cons(y2, y3)), cons(z3, z4)))) -> c(F(node(s(y0), cons(node(z0, cons(node(s(y0), cons(y2, y3)), cons(z3, z4))), cons(y2, y3)))), SELECT(cons(node(s(y0), cons(y2, y3)), cons(z3, z4))))
   F(node(s(s(y1)), cons(node(s(y0), z2), cons(z3, z4)))) -> c(F(node(s(y0), cons(node(s(y1), cons(node(s(y0), z2), cons(z3, z4))), z2))), SELECT(cons(node(s(y0), z2), cons(z3, z4))))
   F(node(s(z0), cons(node(z1, z2), cons(z3, cons(y2, y3))))) -> c(F(node(z1, cons(node(z0, cons(node(z1, z2), cons(z3, cons(y2, y3)))), z2))), SELECT(cons(node(z1, z2), cons(z3, cons(y2, y3)))))
   F(node(s(s(y1)), cons(node(s(s(y0)), z2), cons(z3, z4)))) -> c(F(node(s(s(y0)), cons(node(s(y1), cons(node(s(s(y0)), z2), cons(z3, z4))), z2))), SELECT(cons(node(s(s(y0)), z2), cons(z3, z4))))
   F(node(s(s(y1)), cons(node(s(y0), cons(y3, cons(y4, y5))), cons(z3, z4)))) -> c(F(node(s(y0), cons(node(s(y1), cons(node(s(y0), cons(y3, cons(y4, y5))), cons(z3, z4))), cons(y3, cons(y4, y5))))), SELECT(cons(node(s(y0), cons(y3, cons(y4, y5))), cons(z3, z4))))
K tuples:
   F(node(s(z0), cons(z1, cons(z2, cons(y2, y3))))) -> c(SELECT(cons(z1, cons(z2, cons(y2, y3)))))
Defined Rule Symbols:   addchild_2, select_1

Defined Pair Symbols:   F_1, SELECT_1

Compound Symbols:   c_2, c_1, c2_1


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

(77) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID))
Use forward instantiation to replace F(node(s(z0), cons(z1, cons(y1, y2)))) -> c(SELECT(cons(z1, cons(y1, y2)))) by 
   F(node(s(z0), cons(z1, cons(z2, cons(y2, y3))))) -> c(SELECT(cons(z1, cons(z2, cons(y2, y3)))))

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

(78)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   addchild(node(z0, z1), node(z2, z3)) -> node(z0, cons(node(z2, z3), z1))
   select(cons(z0, z1)) -> z0
   select(cons(z0, z1)) -> select(z1)
Tuples:
   F(node(s(x0), cons(x1, cons(z0, z1)))) -> c(F(addchild(z0, node(x0, cons(x1, cons(z0, z1))))), SELECT(cons(x1, cons(z0, z1))))
   F(node(s(x0), cons(x1, cons(z0, z1)))) -> c(F(addchild(select(z1), node(x0, cons(x1, cons(z0, z1))))), SELECT(cons(x1, cons(z0, z1))))
   F(node(s(z0), cons(node(s(y0), cons(y2, y3)), z3))) -> c(F(node(s(y0), cons(node(z0, cons(node(s(y0), cons(y2, y3)), z3)), cons(y2, y3)))), SELECT(cons(node(s(y0), cons(y2, y3)), z3)))
   SELECT(cons(z0, cons(z1, cons(y1, y2)))) -> c2(SELECT(cons(z1, cons(y1, y2))))
   F(node(s(s(y1)), cons(node(s(z1), z2), z3))) -> c(F(node(s(z1), cons(node(s(y1), cons(node(s(z1), z2), z3)), z2))), SELECT(cons(node(s(z1), z2), z3)))
   F(node(s(z0), cons(node(s(z1), z2), cons(y1, cons(y2, y3))))) -> c(F(node(s(z1), cons(node(z0, cons(node(s(z1), z2), cons(y1, cons(y2, y3)))), z2))), SELECT(cons(node(s(z1), z2), cons(y1, cons(y2, y3)))))
   F(node(s(z0), cons(node(s(y0), cons(y2, y3)), cons(z3, z4)))) -> c(F(node(s(y0), cons(node(z0, cons(node(s(y0), cons(y2, y3)), cons(z3, z4))), cons(y2, y3)))), SELECT(cons(node(s(y0), cons(y2, y3)), cons(z3, z4))))
   F(node(s(s(y1)), cons(node(s(y0), z2), cons(z3, z4)))) -> c(F(node(s(y0), cons(node(s(y1), cons(node(s(y0), z2), cons(z3, z4))), z2))), SELECT(cons(node(s(y0), z2), cons(z3, z4))))
   F(node(s(z0), cons(node(z1, z2), cons(z3, cons(y2, y3))))) -> c(F(node(z1, cons(node(z0, cons(node(z1, z2), cons(z3, cons(y2, y3)))), z2))), SELECT(cons(node(z1, z2), cons(z3, cons(y2, y3)))))
   F(node(s(s(y1)), cons(node(s(s(y0)), z2), cons(z3, z4)))) -> c(F(node(s(s(y0)), cons(node(s(y1), cons(node(s(s(y0)), z2), cons(z3, z4))), z2))), SELECT(cons(node(s(s(y0)), z2), cons(z3, z4))))
   F(node(s(s(y1)), cons(node(s(y0), cons(y3, cons(y4, y5))), cons(z3, z4)))) -> c(F(node(s(y0), cons(node(s(y1), cons(node(s(y0), cons(y3, cons(y4, y5))), cons(z3, z4))), cons(y3, cons(y4, y5))))), SELECT(cons(node(s(y0), cons(y3, cons(y4, y5))), cons(z3, z4))))
   F(node(s(z0), cons(z1, cons(z2, cons(y2, y3))))) -> c(SELECT(cons(z1, cons(z2, cons(y2, y3)))))
S tuples:
   F(node(s(x0), cons(x1, cons(z0, z1)))) -> c(F(addchild(z0, node(x0, cons(x1, cons(z0, z1))))), SELECT(cons(x1, cons(z0, z1))))
   F(node(s(x0), cons(x1, cons(z0, z1)))) -> c(F(addchild(select(z1), node(x0, cons(x1, cons(z0, z1))))), SELECT(cons(x1, cons(z0, z1))))
   F(node(s(z0), cons(node(s(y0), cons(y2, y3)), z3))) -> c(F(node(s(y0), cons(node(z0, cons(node(s(y0), cons(y2, y3)), z3)), cons(y2, y3)))), SELECT(cons(node(s(y0), cons(y2, y3)), z3)))
   SELECT(cons(z0, cons(z1, cons(y1, y2)))) -> c2(SELECT(cons(z1, cons(y1, y2))))
   F(node(s(s(y1)), cons(node(s(z1), z2), z3))) -> c(F(node(s(z1), cons(node(s(y1), cons(node(s(z1), z2), z3)), z2))), SELECT(cons(node(s(z1), z2), z3)))
   F(node(s(z0), cons(node(s(z1), z2), cons(y1, cons(y2, y3))))) -> c(F(node(s(z1), cons(node(z0, cons(node(s(z1), z2), cons(y1, cons(y2, y3)))), z2))), SELECT(cons(node(s(z1), z2), cons(y1, cons(y2, y3)))))
   F(node(s(z0), cons(node(s(y0), cons(y2, y3)), cons(z3, z4)))) -> c(F(node(s(y0), cons(node(z0, cons(node(s(y0), cons(y2, y3)), cons(z3, z4))), cons(y2, y3)))), SELECT(cons(node(s(y0), cons(y2, y3)), cons(z3, z4))))
   F(node(s(s(y1)), cons(node(s(y0), z2), cons(z3, z4)))) -> c(F(node(s(y0), cons(node(s(y1), cons(node(s(y0), z2), cons(z3, z4))), z2))), SELECT(cons(node(s(y0), z2), cons(z3, z4))))
   F(node(s(z0), cons(node(z1, z2), cons(z3, cons(y2, y3))))) -> c(F(node(z1, cons(node(z0, cons(node(z1, z2), cons(z3, cons(y2, y3)))), z2))), SELECT(cons(node(z1, z2), cons(z3, cons(y2, y3)))))
   F(node(s(s(y1)), cons(node(s(s(y0)), z2), cons(z3, z4)))) -> c(F(node(s(s(y0)), cons(node(s(y1), cons(node(s(s(y0)), z2), cons(z3, z4))), z2))), SELECT(cons(node(s(s(y0)), z2), cons(z3, z4))))
   F(node(s(s(y1)), cons(node(s(y0), cons(y3, cons(y4, y5))), cons(z3, z4)))) -> c(F(node(s(y0), cons(node(s(y1), cons(node(s(y0), cons(y3, cons(y4, y5))), cons(z3, z4))), cons(y3, cons(y4, y5))))), SELECT(cons(node(s(y0), cons(y3, cons(y4, y5))), cons(z3, z4))))
K tuples:
   F(node(s(z0), cons(z1, cons(z2, cons(y2, y3))))) -> c(SELECT(cons(z1, cons(z2, cons(y2, y3)))))
Defined Rule Symbols:   addchild_2, select_1

Defined Pair Symbols:   F_1, SELECT_1

Compound Symbols:   c_2, c2_1, c_1