KILLED
proof of input_XVOirIkaDH.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) CpxTrsToCdtProof [BOTH BOUNDS(ID, ID), 0 ms]
(6) CdtProblem
    (7) CdtToCpxRelTrsProof [BOTH BOUNDS(ID, ID), 0 ms]
    (8) CpxRelTRS
    (9) RelTrsToDecreasingLoopProblemProof [LOWER BOUND(ID), 0 ms]
    (10) TRS for Loop Detection
    (11) RenamingProof [BOTH BOUNDS(ID, ID), 0 ms]
    (12) CpxRelTRS
        (13) TypeInferenceProof [BOTH BOUNDS(ID, ID), 7 ms]
        (14) typed CpxTrs
        (15) OrderProof [LOWER BOUND(ID), 0 ms]
        (16) typed CpxTrs
(17) CpxTrsToCdtProof [UPPER BOUND(ID), 0 ms]
(18) CdtProblem
    (19) CdtLeafRemovalProof [BOTH BOUNDS(ID, ID), 0 ms]
    (20) CdtProblem
    (21) CdtRhsSimplificationProcessorProof [BOTH BOUNDS(ID, ID), 0 ms]
    (22) CdtProblem
    (23) CdtUsableRulesProof [BOTH BOUNDS(ID, ID), 0 ms]
    (24) CdtProblem
    (25) CdtToCpxRelTrsProof [BOTH BOUNDS(ID, ID), 0 ms]
    (26) CpxRelTRS
        (27) RelTrsToTrsProof [UPPER BOUND(ID), 0 ms]
        (28) CpxTRS
        (29) RelTrsToWeightedTrsProof [BOTH BOUNDS(ID, ID), 0 ms]
        (30) CpxWeightedTrs
            (31) TypeInferenceProof [BOTH BOUNDS(ID, ID), 0 ms]
            (32) CpxTypedWeightedTrs
            (33) CompletionProof [UPPER BOUND(ID), 0 ms]
            (34) CpxTypedWeightedCompleteTrs
                (35) NarrowingProof [BOTH BOUNDS(ID, ID), 0 ms]
                (36) CpxTypedWeightedCompleteTrs
                (37) CpxTypedWeightedTrsToRntsProof [UPPER BOUND(ID), 0 ms]
                (38) CpxRNTS
                (39) SimplificationProof [BOTH BOUNDS(ID, ID), 0 ms]
                (40) CpxRNTS
            (41) CompletionProof [UPPER BOUND(ID), 0 ms]
            (42) CpxTypedWeightedCompleteTrs
                (43) CpxTypedWeightedTrsToRntsProof [UPPER BOUND(ID), 0 ms]
                (44) CpxRNTS
    (45) CdtNarrowingProof [BOTH BOUNDS(ID, ID), 0 ms]
    (46) CdtProblem
        (47) CdtLeafRemovalProof [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) CdtLeafRemovalProof [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) CdtLeafRemovalProof [BOTH BOUNDS(ID, ID), 0 ms]
        (60) CdtProblem
        (61) CdtUsableRulesProof [BOTH BOUNDS(ID, ID), 0 ms]
        (62) CdtProblem
        (63) CdtRuleRemovalProof [UPPER BOUND(ADD(n^1)), 15 ms]
        (64) CdtProblem
        (65) CdtNarrowingProof [BOTH BOUNDS(ID, ID), 0 ms]
        (66) CdtProblem
        (67) CdtNarrowingProof [BOTH BOUNDS(ID, ID), 0 ms]
        (68) CdtProblem
        (69) CdtRuleRemovalProof [UPPER BOUND(ADD(n^1)), 0 ms]
        (70) CdtProblem
        (71) CdtNarrowingProof [BOTH BOUNDS(ID, ID), 0 ms]
        (72) CdtProblem
        (73) CdtUsableRulesProof [BOTH BOUNDS(ID, ID), 0 ms]
        (74) CdtProblem
        (75) CdtNarrowingProof [BOTH BOUNDS(ID, ID), 0 ms]
        (76) CdtProblem
        (77) CdtUsableRulesProof [BOTH BOUNDS(ID, ID), 0 ms]
        (78) CdtProblem
        (79) CdtRuleRemovalProof [UPPER BOUND(ADD(n^1)), 9 ms]
        (80) CdtProblem
        (81) CdtKnowledgeProof [BOTH BOUNDS(ID, ID), 0 ms]
        (82) CdtProblem
        (83) CdtForwardInstantiationProof [BOTH BOUNDS(ID, ID), 0 ms]
        (84) CdtProblem
        (85) CdtNarrowingProof [BOTH BOUNDS(ID, ID), 0 ms]
        (86) CdtProblem
        (87) CdtLeafRemovalProof [BOTH BOUNDS(ID, ID), 0 ms]
        (88) CdtProblem
        (89) CdtNarrowingProof [BOTH BOUNDS(ID, ID), 0 ms]
        (90) CdtProblem
        (91) CdtRhsSimplificationProcessorProof [BOTH BOUNDS(ID, ID), 0 ms]
        (92) CdtProblem
        (93) CdtForwardInstantiationProof [BOTH BOUNDS(ID, ID), 0 ms]
        (94) CdtProblem
        (95) CdtRewritingProof [BOTH BOUNDS(ID, ID), 0 ms]
        (96) CdtProblem
        (97) CdtRewritingProof [BOTH BOUNDS(ID, ID), 0 ms]
        (98) CdtProblem
        (99) CdtRewritingProof [BOTH BOUNDS(ID, ID), 0 ms]
        (100) CdtProblem
        (101) CdtRewritingProof [BOTH BOUNDS(ID, ID), 0 ms]
        (102) CdtProblem
        (103) CdtInstantiationProof [BOTH BOUNDS(ID, ID), 0 ms]
        (104) CdtProblem
        (105) CdtLeafRemovalProof [BOTH BOUNDS(ID, ID), 0 ms]
        (106) CdtProblem
        (107) CdtForwardInstantiationProof [BOTH BOUNDS(ID, ID), 0 ms]
        (108) CdtProblem
        (109) CdtForwardInstantiationProof [BOTH BOUNDS(ID, ID), 0 ms]
        (110) CdtProblem
        (111) CdtForwardInstantiationProof [BOTH BOUNDS(ID, ID), 0 ms]
        (112) CdtProblem
        (113) CdtForwardInstantiationProof [BOTH BOUNDS(ID, ID), 0 ms]
        (114) CdtProblem
        (115) CdtLeafRemovalProof [BOTH BOUNDS(ID, ID), 0 ms]
        (116) CdtProblem
        (117) CdtForwardInstantiationProof [BOTH BOUNDS(ID, ID), 0 ms]
        (118) CdtProblem
        (119) CdtForwardInstantiationProof [BOTH BOUNDS(ID, ID), 0 ms]
        (120) CdtProblem
(121) RelTrsToWeightedTrsProof [UPPER BOUND(ID), 0 ms]
(122) CpxWeightedTrs
    (123) TypeInferenceProof [BOTH BOUNDS(ID, ID), 0 ms]
    (124) CpxTypedWeightedTrs
    (125) CompletionProof [UPPER BOUND(ID), 0 ms]
    (126) CpxTypedWeightedCompleteTrs
        (127) NarrowingProof [BOTH BOUNDS(ID, ID), 0 ms]
        (128) CpxTypedWeightedCompleteTrs
        (129) CpxTypedWeightedTrsToRntsProof [UPPER BOUND(ID), 2 ms]
        (130) CpxRNTS
        (131) SimplificationProof [BOTH BOUNDS(ID, ID), 0 ms]
        (132) CpxRNTS
    (133) CompletionProof [UPPER BOUND(ID), 0 ms]
    (134) CpxTypedWeightedCompleteTrs
        (135) CpxTypedWeightedTrsToRntsProof [UPPER BOUND(ID), 9 ms]
        (136) CpxRNTS


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

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

   empty(nil) -> true
   empty(cons(x, l)) -> false
   head(cons(x, l)) -> x
   tail(nil) -> nil
   tail(cons(x, l)) -> l
   rev(nil) -> nil
   rev(cons(x, l)) -> cons(rev1(x, l), rev2(x, l))
   last(x, l) -> if(empty(l), x, l)
   if(true, x, l) -> x
   if(false, x, l) -> last(head(l), tail(l))
   rev2(x, nil) -> nil
   rev2(x, cons(y, l)) -> rev(cons(x, rev2(y, l)))

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:

   empty(nil) -> true
   empty(cons(x, l)) -> false
   head(cons(x, l)) -> x
   tail(nil) -> nil
   tail(cons(x, l)) -> l
   rev(nil) -> nil
   rev(cons(x, l)) -> cons(rev1(x, l), rev2(x, l))
   last(x, l) -> if(empty(l), x, l)
   if(true, x, l) -> x
   if(false, x, l) -> last(head(l), tail(l))
   rev2(x, nil) -> nil
   rev2(x, cons(y, l)) -> rev(cons(x, rev2(y, l)))

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:

   empty(nil) -> true
   empty(cons(x, l)) -> false
   head(cons(x, l)) -> x
   tail(nil) -> nil
   tail(cons(x, l)) -> l
   rev(nil) -> nil
   rev(cons(x, l)) -> cons(rev1(x, l), rev2(x, l))
   last(x, l) -> if(empty(l), x, l)
   if(true, x, l) -> x
   if(false, x, l) -> last(head(l), tail(l))
   rev2(x, nil) -> nil
   rev2(x, cons(y, l)) -> rev(cons(x, rev2(y, l)))

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

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

(6)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   empty(nil) -> true
   empty(cons(z0, z1)) -> false
   head(cons(z0, z1)) -> z0
   tail(nil) -> nil
   tail(cons(z0, z1)) -> z1
   rev(nil) -> nil
   rev(cons(z0, z1)) -> cons(rev1(z0, z1), rev2(z0, z1))
   last(z0, z1) -> if(empty(z1), z0, z1)
   if(true, z0, z1) -> z0
   if(false, z0, z1) -> last(head(z1), tail(z1))
   rev2(z0, nil) -> nil
   rev2(z0, cons(z1, z2)) -> rev(cons(z0, rev2(z1, z2)))
Tuples:
   EMPTY(nil) -> c
   EMPTY(cons(z0, z1)) -> c1
   HEAD(cons(z0, z1)) -> c2
   TAIL(nil) -> c3
   TAIL(cons(z0, z1)) -> c4
   REV(nil) -> c5
   REV(cons(z0, z1)) -> c6(REV2(z0, z1))
   LAST(z0, z1) -> c7(IF(empty(z1), z0, z1), EMPTY(z1))
   IF(true, z0, z1) -> c8
   IF(false, z0, z1) -> c9(LAST(head(z1), tail(z1)), HEAD(z1))
   IF(false, z0, z1) -> c10(LAST(head(z1), tail(z1)), TAIL(z1))
   REV2(z0, nil) -> c11
   REV2(z0, cons(z1, z2)) -> c12(REV(cons(z0, rev2(z1, z2))), REV2(z1, z2))
S tuples:
   EMPTY(nil) -> c
   EMPTY(cons(z0, z1)) -> c1
   HEAD(cons(z0, z1)) -> c2
   TAIL(nil) -> c3
   TAIL(cons(z0, z1)) -> c4
   REV(nil) -> c5
   REV(cons(z0, z1)) -> c6(REV2(z0, z1))
   LAST(z0, z1) -> c7(IF(empty(z1), z0, z1), EMPTY(z1))
   IF(true, z0, z1) -> c8
   IF(false, z0, z1) -> c9(LAST(head(z1), tail(z1)), HEAD(z1))
   IF(false, z0, z1) -> c10(LAST(head(z1), tail(z1)), TAIL(z1))
   REV2(z0, nil) -> c11
   REV2(z0, cons(z1, z2)) -> c12(REV(cons(z0, rev2(z1, z2))), REV2(z1, z2))
K tuples:none
Defined Rule Symbols:   empty_1, head_1, tail_1, rev_1, last_2, if_3, rev2_2

Defined Pair Symbols:   EMPTY_1, HEAD_1, TAIL_1, REV_1, LAST_2, IF_3, REV2_2

Compound Symbols:   c, c1, c2, c3, c4, c5, c6_1, c7_2, c8, c9_2, c10_2, c11, c12_2


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

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

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


The TRS R consists of the following rules:

   EMPTY(nil) -> c
   EMPTY(cons(z0, z1)) -> c1
   HEAD(cons(z0, z1)) -> c2
   TAIL(nil) -> c3
   TAIL(cons(z0, z1)) -> c4
   REV(nil) -> c5
   REV(cons(z0, z1)) -> c6(REV2(z0, z1))
   LAST(z0, z1) -> c7(IF(empty(z1), z0, z1), EMPTY(z1))
   IF(true, z0, z1) -> c8
   IF(false, z0, z1) -> c9(LAST(head(z1), tail(z1)), HEAD(z1))
   IF(false, z0, z1) -> c10(LAST(head(z1), tail(z1)), TAIL(z1))
   REV2(z0, nil) -> c11
   REV2(z0, cons(z1, z2)) -> c12(REV(cons(z0, rev2(z1, z2))), REV2(z1, z2))

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

   empty(nil) -> true
   empty(cons(z0, z1)) -> false
   head(cons(z0, z1)) -> z0
   tail(nil) -> nil
   tail(cons(z0, z1)) -> z1
   rev(nil) -> nil
   rev(cons(z0, z1)) -> cons(rev1(z0, z1), rev2(z0, z1))
   last(z0, z1) -> if(empty(z1), z0, z1)
   if(true, z0, z1) -> z0
   if(false, z0, z1) -> last(head(z1), tail(z1))
   rev2(z0, nil) -> nil
   rev2(z0, cons(z1, z2)) -> rev(cons(z0, rev2(z1, z2)))

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

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

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

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


The TRS R consists of the following rules:

   EMPTY(nil) -> c
   EMPTY(cons(z0, z1)) -> c1
   HEAD(cons(z0, z1)) -> c2
   TAIL(nil) -> c3
   TAIL(cons(z0, z1)) -> c4
   REV(nil) -> c5
   REV(cons(z0, z1)) -> c6(REV2(z0, z1))
   LAST(z0, z1) -> c7(IF(empty(z1), z0, z1), EMPTY(z1))
   IF(true, z0, z1) -> c8
   IF(false, z0, z1) -> c9(LAST(head(z1), tail(z1)), HEAD(z1))
   IF(false, z0, z1) -> c10(LAST(head(z1), tail(z1)), TAIL(z1))
   REV2(z0, nil) -> c11
   REV2(z0, cons(z1, z2)) -> c12(REV(cons(z0, rev2(z1, z2))), REV2(z1, z2))

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

   empty(nil) -> true
   empty(cons(z0, z1)) -> false
   head(cons(z0, z1)) -> z0
   tail(nil) -> nil
   tail(cons(z0, z1)) -> z1
   rev(nil) -> nil
   rev(cons(z0, z1)) -> cons(rev1(z0, z1), rev2(z0, z1))
   last(z0, z1) -> if(empty(z1), z0, z1)
   if(true, z0, z1) -> z0
   if(false, z0, z1) -> last(head(z1), tail(z1))
   rev2(z0, nil) -> nil
   rev2(z0, cons(z1, z2)) -> rev(cons(z0, rev2(z1, z2)))

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

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

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


The TRS R consists of the following rules:

   EMPTY(nil) -> c
   EMPTY(cons(z0, z1)) -> c1
   HEAD(cons(z0, z1)) -> c2
   TAIL(nil) -> c3
   TAIL(cons(z0, z1)) -> c4
   REV(nil) -> c5
   REV(cons(z0, z1)) -> c6(REV2(z0, z1))
   LAST(z0, z1) -> c7(IF(empty(z1), z0, z1), EMPTY(z1))
   IF(true, z0, z1) -> c8
   IF(false, z0, z1) -> c9(LAST(head(z1), tail(z1)), HEAD(z1))
   IF(false, z0, z1) -> c10(LAST(head(z1), tail(z1)), TAIL(z1))
   REV2(z0, nil) -> c11
   REV2(z0, cons(z1, z2)) -> c12(REV(cons(z0, rev2(z1, z2))), REV2(z1, z2))

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

   empty(nil) -> true
   empty(cons(z0, z1)) -> false
   head(cons(z0, z1)) -> z0
   tail(nil) -> nil
   tail(cons(z0, z1)) -> z1
   rev(nil) -> nil
   rev(cons(z0, z1)) -> cons(rev1(z0, z1), rev2(z0, z1))
   last(z0, z1) -> if(empty(z1), z0, z1)
   if(true, z0, z1) -> z0
   if(false, z0, z1) -> last(head(z1), tail(z1))
   rev2(z0, nil) -> nil
   rev2(z0, cons(z1, z2)) -> rev(cons(z0, rev2(z1, z2)))

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

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

(14)
Obligation:
Innermost TRS:
Rules:
EMPTY(nil) -> c
EMPTY(cons(z0, z1)) -> c1
HEAD(cons(z0, z1)) -> c2
TAIL(nil) -> c3
TAIL(cons(z0, z1)) -> c4
REV(nil) -> c5
REV(cons(z0, z1)) -> c6(REV2(z0, z1))
LAST(z0, z1) -> c7(IF(empty(z1), z0, z1), EMPTY(z1))
IF(true, z0, z1) -> c8
IF(false, z0, z1) -> c9(LAST(head(z1), tail(z1)), HEAD(z1))
IF(false, z0, z1) -> c10(LAST(head(z1), tail(z1)), TAIL(z1))
REV2(z0, nil) -> c11
REV2(z0, cons(z1, z2)) -> c12(REV(cons(z0, rev2(z1, z2))), REV2(z1, z2))
empty(nil) -> true
empty(cons(z0, z1)) -> false
head(cons(z0, z1)) -> z0
tail(nil) -> nil
tail(cons(z0, z1)) -> z1
rev(nil) -> nil
rev(cons(z0, z1)) -> cons(rev1(z0, z1), rev2(z0, z1))
last(z0, z1) -> if(empty(z1), z0, z1)
if(true, z0, z1) -> z0
if(false, z0, z1) -> last(head(z1), tail(z1))
rev2(z0, nil) -> nil
rev2(z0, cons(z1, z2)) -> rev(cons(z0, rev2(z1, z2)))

Types:
EMPTY :: nil:cons -> c:c1
nil :: nil:cons
c :: c:c1
cons :: rev1 -> nil:cons -> nil:cons
c1 :: c:c1
HEAD :: nil:cons -> c2
c2 :: c2
TAIL :: nil:cons -> c3:c4
c3 :: c3:c4
c4 :: c3:c4
REV :: nil:cons -> c5:c6
c5 :: c5:c6
c6 :: c11:c12 -> c5:c6
REV2 :: rev1 -> nil:cons -> c11:c12
LAST :: rev1 -> nil:cons -> c7
c7 :: c8:c9:c10 -> c:c1 -> c7
IF :: true:false -> rev1 -> nil:cons -> c8:c9:c10
empty :: nil:cons -> true:false
true :: true:false
c8 :: c8:c9:c10
false :: true:false
c9 :: c7 -> c2 -> c8:c9:c10
head :: nil:cons -> rev1
tail :: nil:cons -> nil:cons
c10 :: c7 -> c3:c4 -> c8:c9:c10
c11 :: c11:c12
c12 :: c5:c6 -> c11:c12 -> c11:c12
rev2 :: rev1 -> nil:cons -> nil:cons
rev :: nil:cons -> nil:cons
rev1 :: rev1 -> nil:cons -> rev1
last :: rev1 -> nil:cons -> rev1
if :: true:false -> rev1 -> nil:cons -> rev1
hole_c:c11_13 :: c:c1
hole_nil:cons2_13 :: nil:cons
hole_rev13_13 :: rev1
hole_c24_13 :: c2
hole_c3:c45_13 :: c3:c4
hole_c5:c66_13 :: c5:c6
hole_c11:c127_13 :: c11:c12
hole_c78_13 :: c7
hole_c8:c9:c109_13 :: c8:c9:c10
hole_true:false10_13 :: true:false
gen_nil:cons11_13 :: Nat -> nil:cons
gen_rev112_13 :: Nat -> rev1
gen_c11:c1213_13 :: Nat -> c11:c12

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

(15) OrderProof (LOWER BOUND(ID))
Heuristically decided to analyse the following defined symbols:
REV, REV2, LAST, rev2, rev, last

They will be analysed ascendingly in the following order:
REV = REV2
rev2 < REV2
rev2 = rev

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

(16)
Obligation:
Innermost TRS:
Rules:
EMPTY(nil) -> c
EMPTY(cons(z0, z1)) -> c1
HEAD(cons(z0, z1)) -> c2
TAIL(nil) -> c3
TAIL(cons(z0, z1)) -> c4
REV(nil) -> c5
REV(cons(z0, z1)) -> c6(REV2(z0, z1))
LAST(z0, z1) -> c7(IF(empty(z1), z0, z1), EMPTY(z1))
IF(true, z0, z1) -> c8
IF(false, z0, z1) -> c9(LAST(head(z1), tail(z1)), HEAD(z1))
IF(false, z0, z1) -> c10(LAST(head(z1), tail(z1)), TAIL(z1))
REV2(z0, nil) -> c11
REV2(z0, cons(z1, z2)) -> c12(REV(cons(z0, rev2(z1, z2))), REV2(z1, z2))
empty(nil) -> true
empty(cons(z0, z1)) -> false
head(cons(z0, z1)) -> z0
tail(nil) -> nil
tail(cons(z0, z1)) -> z1
rev(nil) -> nil
rev(cons(z0, z1)) -> cons(rev1(z0, z1), rev2(z0, z1))
last(z0, z1) -> if(empty(z1), z0, z1)
if(true, z0, z1) -> z0
if(false, z0, z1) -> last(head(z1), tail(z1))
rev2(z0, nil) -> nil
rev2(z0, cons(z1, z2)) -> rev(cons(z0, rev2(z1, z2)))

Types:
EMPTY :: nil:cons -> c:c1
nil :: nil:cons
c :: c:c1
cons :: rev1 -> nil:cons -> nil:cons
c1 :: c:c1
HEAD :: nil:cons -> c2
c2 :: c2
TAIL :: nil:cons -> c3:c4
c3 :: c3:c4
c4 :: c3:c4
REV :: nil:cons -> c5:c6
c5 :: c5:c6
c6 :: c11:c12 -> c5:c6
REV2 :: rev1 -> nil:cons -> c11:c12
LAST :: rev1 -> nil:cons -> c7
c7 :: c8:c9:c10 -> c:c1 -> c7
IF :: true:false -> rev1 -> nil:cons -> c8:c9:c10
empty :: nil:cons -> true:false
true :: true:false
c8 :: c8:c9:c10
false :: true:false
c9 :: c7 -> c2 -> c8:c9:c10
head :: nil:cons -> rev1
tail :: nil:cons -> nil:cons
c10 :: c7 -> c3:c4 -> c8:c9:c10
c11 :: c11:c12
c12 :: c5:c6 -> c11:c12 -> c11:c12
rev2 :: rev1 -> nil:cons -> nil:cons
rev :: nil:cons -> nil:cons
rev1 :: rev1 -> nil:cons -> rev1
last :: rev1 -> nil:cons -> rev1
if :: true:false -> rev1 -> nil:cons -> rev1
hole_c:c11_13 :: c:c1
hole_nil:cons2_13 :: nil:cons
hole_rev13_13 :: rev1
hole_c24_13 :: c2
hole_c3:c45_13 :: c3:c4
hole_c5:c66_13 :: c5:c6
hole_c11:c127_13 :: c11:c12
hole_c78_13 :: c7
hole_c8:c9:c109_13 :: c8:c9:c10
hole_true:false10_13 :: true:false
gen_nil:cons11_13 :: Nat -> nil:cons
gen_rev112_13 :: Nat -> rev1
gen_c11:c1213_13 :: Nat -> c11:c12


Generator Equations:
gen_nil:cons11_13(0) <=> nil
gen_nil:cons11_13(+(x, 1)) <=> cons(hole_rev13_13, gen_nil:cons11_13(x))
gen_rev112_13(0) <=> hole_rev13_13
gen_rev112_13(+(x, 1)) <=> rev1(gen_rev112_13(x), nil)
gen_c11:c1213_13(0) <=> c11
gen_c11:c1213_13(+(x, 1)) <=> c12(c5, gen_c11:c1213_13(x))


The following defined symbols remain to be analysed:
LAST, REV, REV2, rev2, rev, last

They will be analysed ascendingly in the following order:
REV = REV2
rev2 < REV2
rev2 = rev

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

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

(18)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   empty(nil) -> true
   empty(cons(z0, z1)) -> false
   head(cons(z0, z1)) -> z0
   tail(nil) -> nil
   tail(cons(z0, z1)) -> z1
   rev(nil) -> nil
   rev(cons(z0, z1)) -> cons(rev1(z0, z1), rev2(z0, z1))
   last(z0, z1) -> if(empty(z1), z0, z1)
   if(true, z0, z1) -> z0
   if(false, z0, z1) -> last(head(z1), tail(z1))
   rev2(z0, nil) -> nil
   rev2(z0, cons(z1, z2)) -> rev(cons(z0, rev2(z1, z2)))
Tuples:
   EMPTY(nil) -> c
   EMPTY(cons(z0, z1)) -> c1
   HEAD(cons(z0, z1)) -> c2
   TAIL(nil) -> c3
   TAIL(cons(z0, z1)) -> c4
   REV(nil) -> c5
   REV(cons(z0, z1)) -> c6(REV2(z0, z1))
   LAST(z0, z1) -> c7(IF(empty(z1), z0, z1), EMPTY(z1))
   IF(true, z0, z1) -> c8
   IF(false, z0, z1) -> c9(LAST(head(z1), tail(z1)), HEAD(z1))
   IF(false, z0, z1) -> c10(LAST(head(z1), tail(z1)), TAIL(z1))
   REV2(z0, nil) -> c11
   REV2(z0, cons(z1, z2)) -> c12(REV(cons(z0, rev2(z1, z2))), REV2(z1, z2))
S tuples:
   EMPTY(nil) -> c
   EMPTY(cons(z0, z1)) -> c1
   HEAD(cons(z0, z1)) -> c2
   TAIL(nil) -> c3
   TAIL(cons(z0, z1)) -> c4
   REV(nil) -> c5
   REV(cons(z0, z1)) -> c6(REV2(z0, z1))
   LAST(z0, z1) -> c7(IF(empty(z1), z0, z1), EMPTY(z1))
   IF(true, z0, z1) -> c8
   IF(false, z0, z1) -> c9(LAST(head(z1), tail(z1)), HEAD(z1))
   IF(false, z0, z1) -> c10(LAST(head(z1), tail(z1)), TAIL(z1))
   REV2(z0, nil) -> c11
   REV2(z0, cons(z1, z2)) -> c12(REV(cons(z0, rev2(z1, z2))), REV2(z1, z2))
K tuples:none
Defined Rule Symbols:   empty_1, head_1, tail_1, rev_1, last_2, if_3, rev2_2

Defined Pair Symbols:   EMPTY_1, HEAD_1, TAIL_1, REV_1, LAST_2, IF_3, REV2_2

Compound Symbols:   c, c1, c2, c3, c4, c5, c6_1, c7_2, c8, c9_2, c10_2, c11, c12_2


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

(19) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID))
Removed 8 trailing nodes:
   TAIL(cons(z0, z1)) -> c4
   EMPTY(nil) -> c
   HEAD(cons(z0, z1)) -> c2
   REV2(z0, nil) -> c11
   TAIL(nil) -> c3
   IF(true, z0, z1) -> c8
   EMPTY(cons(z0, z1)) -> c1
   REV(nil) -> c5

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

(20)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   empty(nil) -> true
   empty(cons(z0, z1)) -> false
   head(cons(z0, z1)) -> z0
   tail(nil) -> nil
   tail(cons(z0, z1)) -> z1
   rev(nil) -> nil
   rev(cons(z0, z1)) -> cons(rev1(z0, z1), rev2(z0, z1))
   last(z0, z1) -> if(empty(z1), z0, z1)
   if(true, z0, z1) -> z0
   if(false, z0, z1) -> last(head(z1), tail(z1))
   rev2(z0, nil) -> nil
   rev2(z0, cons(z1, z2)) -> rev(cons(z0, rev2(z1, z2)))
Tuples:
   REV(cons(z0, z1)) -> c6(REV2(z0, z1))
   LAST(z0, z1) -> c7(IF(empty(z1), z0, z1), EMPTY(z1))
   IF(false, z0, z1) -> c9(LAST(head(z1), tail(z1)), HEAD(z1))
   IF(false, z0, z1) -> c10(LAST(head(z1), tail(z1)), TAIL(z1))
   REV2(z0, cons(z1, z2)) -> c12(REV(cons(z0, rev2(z1, z2))), REV2(z1, z2))
S tuples:
   REV(cons(z0, z1)) -> c6(REV2(z0, z1))
   LAST(z0, z1) -> c7(IF(empty(z1), z0, z1), EMPTY(z1))
   IF(false, z0, z1) -> c9(LAST(head(z1), tail(z1)), HEAD(z1))
   IF(false, z0, z1) -> c10(LAST(head(z1), tail(z1)), TAIL(z1))
   REV2(z0, cons(z1, z2)) -> c12(REV(cons(z0, rev2(z1, z2))), REV2(z1, z2))
K tuples:none
Defined Rule Symbols:   empty_1, head_1, tail_1, rev_1, last_2, if_3, rev2_2

Defined Pair Symbols:   REV_1, LAST_2, IF_3, REV2_2

Compound Symbols:   c6_1, c7_2, c9_2, c10_2, c12_2


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

(21) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID))
Removed 3 trailing tuple parts
----------------------------------------

(22)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   empty(nil) -> true
   empty(cons(z0, z1)) -> false
   head(cons(z0, z1)) -> z0
   tail(nil) -> nil
   tail(cons(z0, z1)) -> z1
   rev(nil) -> nil
   rev(cons(z0, z1)) -> cons(rev1(z0, z1), rev2(z0, z1))
   last(z0, z1) -> if(empty(z1), z0, z1)
   if(true, z0, z1) -> z0
   if(false, z0, z1) -> last(head(z1), tail(z1))
   rev2(z0, nil) -> nil
   rev2(z0, cons(z1, z2)) -> rev(cons(z0, rev2(z1, z2)))
Tuples:
   REV(cons(z0, z1)) -> c6(REV2(z0, z1))
   REV2(z0, cons(z1, z2)) -> c12(REV(cons(z0, rev2(z1, z2))), REV2(z1, z2))
   LAST(z0, z1) -> c7(IF(empty(z1), z0, z1))
   IF(false, z0, z1) -> c9(LAST(head(z1), tail(z1)))
   IF(false, z0, z1) -> c10(LAST(head(z1), tail(z1)))
S tuples:
   REV(cons(z0, z1)) -> c6(REV2(z0, z1))
   REV2(z0, cons(z1, z2)) -> c12(REV(cons(z0, rev2(z1, z2))), REV2(z1, z2))
   LAST(z0, z1) -> c7(IF(empty(z1), z0, z1))
   IF(false, z0, z1) -> c9(LAST(head(z1), tail(z1)))
   IF(false, z0, z1) -> c10(LAST(head(z1), tail(z1)))
K tuples:none
Defined Rule Symbols:   empty_1, head_1, tail_1, rev_1, last_2, if_3, rev2_2

Defined Pair Symbols:   REV_1, REV2_2, LAST_2, IF_3

Compound Symbols:   c6_1, c12_2, c7_1, c9_1, c10_1


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

(23) CdtUsableRulesProof (BOTH BOUNDS(ID, ID))
The following rules are not usable and were removed:
   rev(nil) -> nil
   last(z0, z1) -> if(empty(z1), z0, z1)
   if(true, z0, z1) -> z0
   if(false, z0, z1) -> last(head(z1), tail(z1))

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

(24)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   rev2(z0, nil) -> nil
   rev2(z0, cons(z1, z2)) -> rev(cons(z0, rev2(z1, z2)))
   rev(cons(z0, z1)) -> cons(rev1(z0, z1), rev2(z0, z1))
   empty(nil) -> true
   empty(cons(z0, z1)) -> false
   head(cons(z0, z1)) -> z0
   tail(nil) -> nil
   tail(cons(z0, z1)) -> z1
Tuples:
   REV(cons(z0, z1)) -> c6(REV2(z0, z1))
   REV2(z0, cons(z1, z2)) -> c12(REV(cons(z0, rev2(z1, z2))), REV2(z1, z2))
   LAST(z0, z1) -> c7(IF(empty(z1), z0, z1))
   IF(false, z0, z1) -> c9(LAST(head(z1), tail(z1)))
   IF(false, z0, z1) -> c10(LAST(head(z1), tail(z1)))
S tuples:
   REV(cons(z0, z1)) -> c6(REV2(z0, z1))
   REV2(z0, cons(z1, z2)) -> c12(REV(cons(z0, rev2(z1, z2))), REV2(z1, z2))
   LAST(z0, z1) -> c7(IF(empty(z1), z0, z1))
   IF(false, z0, z1) -> c9(LAST(head(z1), tail(z1)))
   IF(false, z0, z1) -> c10(LAST(head(z1), tail(z1)))
K tuples:none
Defined Rule Symbols:   rev2_2, rev_1, empty_1, head_1, tail_1

Defined Pair Symbols:   REV_1, REV2_2, LAST_2, IF_3

Compound Symbols:   c6_1, c12_2, c7_1, c9_1, c10_1


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

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

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


The TRS R consists of the following rules:

   REV(cons(z0, z1)) -> c6(REV2(z0, z1))
   REV2(z0, cons(z1, z2)) -> c12(REV(cons(z0, rev2(z1, z2))), REV2(z1, z2))
   LAST(z0, z1) -> c7(IF(empty(z1), z0, z1))
   IF(false, z0, z1) -> c9(LAST(head(z1), tail(z1)))
   IF(false, z0, z1) -> c10(LAST(head(z1), tail(z1)))

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

   rev2(z0, nil) -> nil
   rev2(z0, cons(z1, z2)) -> rev(cons(z0, rev2(z1, z2)))
   rev(cons(z0, z1)) -> cons(rev1(z0, z1), rev2(z0, z1))
   empty(nil) -> true
   empty(cons(z0, z1)) -> false
   head(cons(z0, z1)) -> z0
   tail(nil) -> nil
   tail(cons(z0, z1)) -> z1

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

(27) RelTrsToTrsProof (UPPER BOUND(ID))
transformed relative TRS to TRS
----------------------------------------

(28)
Obligation:
The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(1, INF).


The TRS R consists of the following rules:

   REV(cons(z0, z1)) -> c6(REV2(z0, z1))
   REV2(z0, cons(z1, z2)) -> c12(REV(cons(z0, rev2(z1, z2))), REV2(z1, z2))
   LAST(z0, z1) -> c7(IF(empty(z1), z0, z1))
   IF(false, z0, z1) -> c9(LAST(head(z1), tail(z1)))
   IF(false, z0, z1) -> c10(LAST(head(z1), tail(z1)))
   rev2(z0, nil) -> nil
   rev2(z0, cons(z1, z2)) -> rev(cons(z0, rev2(z1, z2)))
   rev(cons(z0, z1)) -> cons(rev1(z0, z1), rev2(z0, z1))
   empty(nil) -> true
   empty(cons(z0, z1)) -> false
   head(cons(z0, z1)) -> z0
   tail(nil) -> nil
   tail(cons(z0, z1)) -> z1

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

(29) RelTrsToWeightedTrsProof (BOTH BOUNDS(ID, ID))
Transformed relative TRS to weighted TRS
----------------------------------------

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

   REV(cons(z0, z1)) -> c6(REV2(z0, z1)) [1]
   REV2(z0, cons(z1, z2)) -> c12(REV(cons(z0, rev2(z1, z2))), REV2(z1, z2)) [1]
   LAST(z0, z1) -> c7(IF(empty(z1), z0, z1)) [1]
   IF(false, z0, z1) -> c9(LAST(head(z1), tail(z1))) [1]
   IF(false, z0, z1) -> c10(LAST(head(z1), tail(z1))) [1]
   rev2(z0, nil) -> nil [0]
   rev2(z0, cons(z1, z2)) -> rev(cons(z0, rev2(z1, z2))) [0]
   rev(cons(z0, z1)) -> cons(rev1(z0, z1), rev2(z0, z1)) [0]
   empty(nil) -> true [0]
   empty(cons(z0, z1)) -> false [0]
   head(cons(z0, z1)) -> z0 [0]
   tail(nil) -> nil [0]
   tail(cons(z0, z1)) -> z1 [0]

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

(31) TypeInferenceProof (BOTH BOUNDS(ID, ID))
Infered types.
----------------------------------------

(32)
Obligation:
Runtime Complexity Weighted TRS with Types.
The TRS R consists of the following rules:

   REV(cons(z0, z1)) -> c6(REV2(z0, z1)) [1]
   REV2(z0, cons(z1, z2)) -> c12(REV(cons(z0, rev2(z1, z2))), REV2(z1, z2)) [1]
   LAST(z0, z1) -> c7(IF(empty(z1), z0, z1)) [1]
   IF(false, z0, z1) -> c9(LAST(head(z1), tail(z1))) [1]
   IF(false, z0, z1) -> c10(LAST(head(z1), tail(z1))) [1]
   rev2(z0, nil) -> nil [0]
   rev2(z0, cons(z1, z2)) -> rev(cons(z0, rev2(z1, z2))) [0]
   rev(cons(z0, z1)) -> cons(rev1(z0, z1), rev2(z0, z1)) [0]
   empty(nil) -> true [0]
   empty(cons(z0, z1)) -> false [0]
   head(cons(z0, z1)) -> z0 [0]
   tail(nil) -> nil [0]
   tail(cons(z0, z1)) -> z1 [0]

The TRS has the following type information:
REV :: cons:nil -> c6
cons :: rev1 -> cons:nil -> cons:nil
c6 :: c12 -> c6
REV2 :: rev1 -> cons:nil -> c12
c12 :: c6 -> c12 -> c12
rev2 :: rev1 -> cons:nil -> cons:nil
LAST :: rev1 -> cons:nil -> c7
c7 :: c9:c10 -> c7
IF :: false:true -> rev1 -> cons:nil -> c9:c10
empty :: cons:nil -> false:true
false :: false:true
c9 :: c7 -> c9:c10
head :: cons:nil -> rev1
tail :: cons:nil -> cons:nil
c10 :: c7 -> c9:c10
nil :: cons:nil
rev :: cons:nil -> cons:nil
rev1 :: rev1 -> cons:nil -> rev1
true :: false:true

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

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

   REV_1
   REV2_2
   LAST_2
   IF_3

(c) The following functions are completely defined:

   rev2_2
   rev_1
   empty_1
   head_1
   tail_1

Due to the following rules being added:

   rev2(v0, v1) -> nil [0]
   rev(v0) -> nil [0]
   empty(v0) -> null_empty [0]
   head(v0) -> const1 [0]
   tail(v0) -> nil [0]

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

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

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

   REV(cons(z0, z1)) -> c6(REV2(z0, z1)) [1]
   REV2(z0, cons(z1, z2)) -> c12(REV(cons(z0, rev2(z1, z2))), REV2(z1, z2)) [1]
   LAST(z0, z1) -> c7(IF(empty(z1), z0, z1)) [1]
   IF(false, z0, z1) -> c9(LAST(head(z1), tail(z1))) [1]
   IF(false, z0, z1) -> c10(LAST(head(z1), tail(z1))) [1]
   rev2(z0, nil) -> nil [0]
   rev2(z0, cons(z1, z2)) -> rev(cons(z0, rev2(z1, z2))) [0]
   rev(cons(z0, z1)) -> cons(rev1(z0, z1), rev2(z0, z1)) [0]
   empty(nil) -> true [0]
   empty(cons(z0, z1)) -> false [0]
   head(cons(z0, z1)) -> z0 [0]
   tail(nil) -> nil [0]
   tail(cons(z0, z1)) -> z1 [0]
   rev2(v0, v1) -> nil [0]
   rev(v0) -> nil [0]
   empty(v0) -> null_empty [0]
   head(v0) -> const1 [0]
   tail(v0) -> nil [0]

The TRS has the following type information:
REV :: cons:nil -> c6
cons :: rev1:const1 -> cons:nil -> cons:nil
c6 :: c12 -> c6
REV2 :: rev1:const1 -> cons:nil -> c12
c12 :: c6 -> c12 -> c12
rev2 :: rev1:const1 -> cons:nil -> cons:nil
LAST :: rev1:const1 -> cons:nil -> c7
c7 :: c9:c10 -> c7
IF :: false:true:null_empty -> rev1:const1 -> cons:nil -> c9:c10
empty :: cons:nil -> false:true:null_empty
false :: false:true:null_empty
c9 :: c7 -> c9:c10
head :: cons:nil -> rev1:const1
tail :: cons:nil -> cons:nil
c10 :: c7 -> c9:c10
nil :: cons:nil
rev :: cons:nil -> cons:nil
rev1 :: rev1:const1 -> cons:nil -> rev1:const1
true :: false:true:null_empty
null_empty :: false:true:null_empty
const1 :: rev1:const1
const :: c6
const2 :: c12
const3 :: c7
const4 :: c9:c10

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

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

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

   REV(cons(z0, z1)) -> c6(REV2(z0, z1)) [1]
   REV2(z0, cons(z1, nil)) -> c12(REV(cons(z0, nil)), REV2(z1, nil)) [1]
   REV2(z0, cons(z1, cons(z1', z2'))) -> c12(REV(cons(z0, rev(cons(z1, rev2(z1', z2'))))), REV2(z1, cons(z1', z2'))) [1]
   REV2(z0, cons(z1, z2)) -> c12(REV(cons(z0, nil)), REV2(z1, z2)) [1]
   LAST(z0, nil) -> c7(IF(true, z0, nil)) [1]
   LAST(z0, cons(z0', z1'')) -> c7(IF(false, z0, cons(z0', z1''))) [1]
   LAST(z0, z1) -> c7(IF(null_empty, z0, z1)) [1]
   IF(false, z0, cons(z0'', z11)) -> c9(LAST(z0'', z11)) [1]
   IF(false, z0, cons(z0'', z11)) -> c9(LAST(z0'', nil)) [1]
   IF(false, z0, nil) -> c9(LAST(const1, nil)) [1]
   IF(false, z0, cons(z01, z12)) -> c9(LAST(const1, z12)) [1]
   IF(false, z0, z1) -> c9(LAST(const1, nil)) [1]
   IF(false, z0, cons(z02, z13)) -> c10(LAST(z02, z13)) [1]
   IF(false, z0, cons(z02, z13)) -> c10(LAST(z02, nil)) [1]
   IF(false, z0, nil) -> c10(LAST(const1, nil)) [1]
   IF(false, z0, cons(z03, z14)) -> c10(LAST(const1, z14)) [1]
   IF(false, z0, z1) -> c10(LAST(const1, nil)) [1]
   rev2(z0, nil) -> nil [0]
   rev2(z0, cons(z1, nil)) -> rev(cons(z0, nil)) [0]
   rev2(z0, cons(z1, cons(z15, z2''))) -> rev(cons(z0, rev(cons(z1, rev2(z15, z2''))))) [0]
   rev2(z0, cons(z1, z2)) -> rev(cons(z0, nil)) [0]
   rev(cons(z0, z1)) -> cons(rev1(z0, z1), rev2(z0, z1)) [0]
   empty(nil) -> true [0]
   empty(cons(z0, z1)) -> false [0]
   head(cons(z0, z1)) -> z0 [0]
   tail(nil) -> nil [0]
   tail(cons(z0, z1)) -> z1 [0]
   rev2(v0, v1) -> nil [0]
   rev(v0) -> nil [0]
   empty(v0) -> null_empty [0]
   head(v0) -> const1 [0]
   tail(v0) -> nil [0]

The TRS has the following type information:
REV :: cons:nil -> c6
cons :: rev1:const1 -> cons:nil -> cons:nil
c6 :: c12 -> c6
REV2 :: rev1:const1 -> cons:nil -> c12
c12 :: c6 -> c12 -> c12
rev2 :: rev1:const1 -> cons:nil -> cons:nil
LAST :: rev1:const1 -> cons:nil -> c7
c7 :: c9:c10 -> c7
IF :: false:true:null_empty -> rev1:const1 -> cons:nil -> c9:c10
empty :: cons:nil -> false:true:null_empty
false :: false:true:null_empty
c9 :: c7 -> c9:c10
head :: cons:nil -> rev1:const1
tail :: cons:nil -> cons:nil
c10 :: c7 -> c9:c10
nil :: cons:nil
rev :: cons:nil -> cons:nil
rev1 :: rev1:const1 -> cons:nil -> rev1:const1
true :: false:true:null_empty
null_empty :: false:true:null_empty
const1 :: rev1:const1
const :: c6
const2 :: c12
const3 :: c7
const4 :: c9:c10

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

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

   false => 1
   nil => 0
   true => 2
   null_empty => 0
   const1 => 0
   const => 0
   const2 => 0
   const3 => 0
   const4 => 0

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

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

   IF(z, z', z'') -{ 1 }-> 1 + LAST(z0'', z11) :|: z11 >= 0, z = 1, z0 >= 0, z0'' >= 0, z'' = 1 + z0'' + z11, z' = z0
   IF(z, z', z'') -{ 1 }-> 1 + LAST(z0'', 0) :|: z11 >= 0, z = 1, z0 >= 0, z0'' >= 0, z'' = 1 + z0'' + z11, z' = z0
   IF(z, z', z'') -{ 1 }-> 1 + LAST(z02, z13) :|: z'' = 1 + z02 + z13, z = 1, z02 >= 0, z0 >= 0, z' = z0, z13 >= 0
   IF(z, z', z'') -{ 1 }-> 1 + LAST(z02, 0) :|: z'' = 1 + z02 + z13, z = 1, z02 >= 0, z0 >= 0, z' = z0, z13 >= 0
   IF(z, z', z'') -{ 1 }-> 1 + LAST(0, z12) :|: z01 >= 0, z = 1, z0 >= 0, z12 >= 0, z' = z0, z'' = 1 + z01 + z12
   IF(z, z', z'') -{ 1 }-> 1 + LAST(0, z14) :|: z = 1, z'' = 1 + z03 + z14, z0 >= 0, z03 >= 0, z' = z0, z14 >= 0
   IF(z, z', z'') -{ 1 }-> 1 + LAST(0, 0) :|: z'' = 0, z = 1, z0 >= 0, z' = z0
   IF(z, z', z'') -{ 1 }-> 1 + LAST(0, 0) :|: z1 >= 0, z = 1, z0 >= 0, z' = z0, z'' = z1
   LAST(z, z') -{ 1 }-> 1 + IF(2, z0, 0) :|: z = z0, z0 >= 0, z' = 0
   LAST(z, z') -{ 1 }-> 1 + IF(1, z0, 1 + z0' + z1'') :|: z = z0, z0' >= 0, z0 >= 0, z' = 1 + z0' + z1'', z1'' >= 0
   LAST(z, z') -{ 1 }-> 1 + IF(0, z0, z1) :|: z = z0, z1 >= 0, z' = z1, z0 >= 0
   REV(z) -{ 1 }-> 1 + REV2(z0, z1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   REV2(z, z') -{ 1 }-> 1 + REV(1 + z0 + rev(1 + z1 + rev2(z1', z2'))) + REV2(z1, 1 + z1' + z2') :|: z = z0, z1 >= 0, z1' >= 0, z2' >= 0, z' = 1 + z1 + (1 + z1' + z2'), z0 >= 0
   REV2(z, z') -{ 1 }-> 1 + REV(1 + z0 + 0) + REV2(z1, z2) :|: z = z0, z1 >= 0, z' = 1 + z1 + z2, z0 >= 0, z2 >= 0
   REV2(z, z') -{ 1 }-> 1 + REV(1 + z0 + 0) + REV2(z1, 0) :|: z = z0, z1 >= 0, z0 >= 0, z' = 1 + z1 + 0
   empty(z) -{ 0 }-> 2 :|: z = 0
   empty(z) -{ 0 }-> 1 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   empty(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0
   head(z) -{ 0 }-> z0 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   head(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0
   rev(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0
   rev(z) -{ 0 }-> 1 + (1 + z0 + z1) + rev2(z0, z1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   rev2(z, z') -{ 0 }-> rev(1 + z0 + rev(1 + z1 + rev2(z15, z2''))) :|: z = z0, z1 >= 0, z15 >= 0, z' = 1 + z1 + (1 + z15 + z2''), z0 >= 0, z2'' >= 0
   rev2(z, z') -{ 0 }-> rev(1 + z0 + 0) :|: z = z0, z1 >= 0, z0 >= 0, z' = 1 + z1 + 0
   rev2(z, z') -{ 0 }-> rev(1 + z0 + 0) :|: z = z0, z1 >= 0, z' = 1 + z1 + z2, z0 >= 0, z2 >= 0
   rev2(z, z') -{ 0 }-> 0 :|: z = z0, z0 >= 0, z' = 0
   rev2(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
   tail(z) -{ 0 }-> z1 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   tail(z) -{ 0 }-> 0 :|: z = 0
   tail(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0


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

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

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

   IF(z, z', z'') -{ 1 }-> 1 + LAST(z0'', z11) :|: z11 >= 0, z = 1, z' >= 0, z0'' >= 0, z'' = 1 + z0'' + z11
   IF(z, z', z'') -{ 1 }-> 1 + LAST(z0'', 0) :|: z11 >= 0, z = 1, z' >= 0, z0'' >= 0, z'' = 1 + z0'' + z11
   IF(z, z', z'') -{ 1 }-> 1 + LAST(z02, z13) :|: z'' = 1 + z02 + z13, z = 1, z02 >= 0, z' >= 0, z13 >= 0
   IF(z, z', z'') -{ 1 }-> 1 + LAST(z02, 0) :|: z'' = 1 + z02 + z13, z = 1, z02 >= 0, z' >= 0, z13 >= 0
   IF(z, z', z'') -{ 1 }-> 1 + LAST(0, z12) :|: z01 >= 0, z = 1, z' >= 0, z12 >= 0, z'' = 1 + z01 + z12
   IF(z, z', z'') -{ 1 }-> 1 + LAST(0, z14) :|: z = 1, z'' = 1 + z03 + z14, z' >= 0, z03 >= 0, z14 >= 0
   IF(z, z', z'') -{ 1 }-> 1 + LAST(0, 0) :|: z'' = 0, z = 1, z' >= 0
   IF(z, z', z'') -{ 1 }-> 1 + LAST(0, 0) :|: z'' >= 0, z = 1, z' >= 0
   LAST(z, z') -{ 1 }-> 1 + IF(2, z, 0) :|: z >= 0, z' = 0
   LAST(z, z') -{ 1 }-> 1 + IF(1, z, 1 + z0' + z1'') :|: z0' >= 0, z >= 0, z' = 1 + z0' + z1'', z1'' >= 0
   LAST(z, z') -{ 1 }-> 1 + IF(0, z, z') :|: z' >= 0, z >= 0
   REV(z) -{ 1 }-> 1 + REV2(z0, z1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   REV2(z, z') -{ 1 }-> 1 + REV(1 + z + rev(1 + z1 + rev2(z1', z2'))) + REV2(z1, 1 + z1' + z2') :|: z1 >= 0, z1' >= 0, z2' >= 0, z' = 1 + z1 + (1 + z1' + z2'), z >= 0
   REV2(z, z') -{ 1 }-> 1 + REV(1 + z + 0) + REV2(z1, z2) :|: z1 >= 0, z' = 1 + z1 + z2, z >= 0, z2 >= 0
   REV2(z, z') -{ 1 }-> 1 + REV(1 + z + 0) + REV2(z' - 1, 0) :|: z' - 1 >= 0, z >= 0
   empty(z) -{ 0 }-> 2 :|: z = 0
   empty(z) -{ 0 }-> 1 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   empty(z) -{ 0 }-> 0 :|: z >= 0
   head(z) -{ 0 }-> z0 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   head(z) -{ 0 }-> 0 :|: z >= 0
   rev(z) -{ 0 }-> 0 :|: z >= 0
   rev(z) -{ 0 }-> 1 + (1 + z0 + z1) + rev2(z0, z1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   rev2(z, z') -{ 0 }-> rev(1 + z + rev(1 + z1 + rev2(z15, z2''))) :|: z1 >= 0, z15 >= 0, z' = 1 + z1 + (1 + z15 + z2''), z >= 0, z2'' >= 0
   rev2(z, z') -{ 0 }-> rev(1 + z + 0) :|: z' - 1 >= 0, z >= 0
   rev2(z, z') -{ 0 }-> rev(1 + z + 0) :|: z1 >= 0, z' = 1 + z1 + z2, z >= 0, z2 >= 0
   rev2(z, z') -{ 0 }-> 0 :|: z >= 0, z' = 0
   rev2(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   tail(z) -{ 0 }-> z1 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   tail(z) -{ 0 }-> 0 :|: z = 0
   tail(z) -{ 0 }-> 0 :|: z >= 0


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

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

   rev2(v0, v1) -> null_rev2 [0]
   rev(v0) -> null_rev [0]
   empty(v0) -> null_empty [0]
   head(v0) -> null_head [0]
   tail(v0) -> null_tail [0]
   REV(v0) -> null_REV [0]
   REV2(v0, v1) -> null_REV2 [0]
   IF(v0, v1, v2) -> null_IF [0]

And the following fresh constants:    null_rev2, null_rev, null_empty, null_head, null_tail, null_REV, null_REV2, null_IF, const

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

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

   REV(cons(z0, z1)) -> c6(REV2(z0, z1)) [1]
   REV2(z0, cons(z1, z2)) -> c12(REV(cons(z0, rev2(z1, z2))), REV2(z1, z2)) [1]
   LAST(z0, z1) -> c7(IF(empty(z1), z0, z1)) [1]
   IF(false, z0, z1) -> c9(LAST(head(z1), tail(z1))) [1]
   IF(false, z0, z1) -> c10(LAST(head(z1), tail(z1))) [1]
   rev2(z0, nil) -> nil [0]
   rev2(z0, cons(z1, z2)) -> rev(cons(z0, rev2(z1, z2))) [0]
   rev(cons(z0, z1)) -> cons(rev1(z0, z1), rev2(z0, z1)) [0]
   empty(nil) -> true [0]
   empty(cons(z0, z1)) -> false [0]
   head(cons(z0, z1)) -> z0 [0]
   tail(nil) -> nil [0]
   tail(cons(z0, z1)) -> z1 [0]
   rev2(v0, v1) -> null_rev2 [0]
   rev(v0) -> null_rev [0]
   empty(v0) -> null_empty [0]
   head(v0) -> null_head [0]
   tail(v0) -> null_tail [0]
   REV(v0) -> null_REV [0]
   REV2(v0, v1) -> null_REV2 [0]
   IF(v0, v1, v2) -> null_IF [0]

The TRS has the following type information:
REV :: cons:nil:null_rev2:null_rev:null_tail -> c6:null_REV
cons :: rev1:null_head -> cons:nil:null_rev2:null_rev:null_tail -> cons:nil:null_rev2:null_rev:null_tail
c6 :: c12:null_REV2 -> c6:null_REV
REV2 :: rev1:null_head -> cons:nil:null_rev2:null_rev:null_tail -> c12:null_REV2
c12 :: c6:null_REV -> c12:null_REV2 -> c12:null_REV2
rev2 :: rev1:null_head -> cons:nil:null_rev2:null_rev:null_tail -> cons:nil:null_rev2:null_rev:null_tail
LAST :: rev1:null_head -> cons:nil:null_rev2:null_rev:null_tail -> c7
c7 :: c9:c10:null_IF -> c7
IF :: false:true:null_empty -> rev1:null_head -> cons:nil:null_rev2:null_rev:null_tail -> c9:c10:null_IF
empty :: cons:nil:null_rev2:null_rev:null_tail -> false:true:null_empty
false :: false:true:null_empty
c9 :: c7 -> c9:c10:null_IF
head :: cons:nil:null_rev2:null_rev:null_tail -> rev1:null_head
tail :: cons:nil:null_rev2:null_rev:null_tail -> cons:nil:null_rev2:null_rev:null_tail
c10 :: c7 -> c9:c10:null_IF
nil :: cons:nil:null_rev2:null_rev:null_tail
rev :: cons:nil:null_rev2:null_rev:null_tail -> cons:nil:null_rev2:null_rev:null_tail
rev1 :: rev1:null_head -> cons:nil:null_rev2:null_rev:null_tail -> rev1:null_head
true :: false:true:null_empty
null_rev2 :: cons:nil:null_rev2:null_rev:null_tail
null_rev :: cons:nil:null_rev2:null_rev:null_tail
null_empty :: false:true:null_empty
null_head :: rev1:null_head
null_tail :: cons:nil:null_rev2:null_rev:null_tail
null_REV :: c6:null_REV
null_REV2 :: c12:null_REV2
null_IF :: c9:c10:null_IF
const :: c7

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

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

   false => 1
   nil => 0
   true => 2
   null_rev2 => 0
   null_rev => 0
   null_empty => 0
   null_head => 0
   null_tail => 0
   null_REV => 0
   null_REV2 => 0
   null_IF => 0
   const => 0

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

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

   IF(z, z', z'') -{ 0 }-> 0 :|: v0 >= 0, z'' = v2, v1 >= 0, z = v0, z' = v1, v2 >= 0
   IF(z, z', z'') -{ 1 }-> 1 + LAST(head(z1), tail(z1)) :|: z1 >= 0, z = 1, z0 >= 0, z' = z0, z'' = z1
   LAST(z, z') -{ 1 }-> 1 + IF(empty(z1), z0, z1) :|: z = z0, z1 >= 0, z' = z1, z0 >= 0
   REV(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0
   REV(z) -{ 1 }-> 1 + REV2(z0, z1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   REV2(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
   REV2(z, z') -{ 1 }-> 1 + REV(1 + z0 + rev2(z1, z2)) + REV2(z1, z2) :|: z = z0, z1 >= 0, z' = 1 + z1 + z2, z0 >= 0, z2 >= 0
   empty(z) -{ 0 }-> 2 :|: z = 0
   empty(z) -{ 0 }-> 1 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   empty(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0
   head(z) -{ 0 }-> z0 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   head(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0
   rev(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0
   rev(z) -{ 0 }-> 1 + (1 + z0 + z1) + rev2(z0, z1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   rev2(z, z') -{ 0 }-> rev(1 + z0 + rev2(z1, z2)) :|: z = z0, z1 >= 0, z' = 1 + z1 + z2, z0 >= 0, z2 >= 0
   rev2(z, z') -{ 0 }-> 0 :|: z = z0, z0 >= 0, z' = 0
   rev2(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
   tail(z) -{ 0 }-> z1 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   tail(z) -{ 0 }-> 0 :|: z = 0
   tail(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0

Only complete derivations are relevant for the runtime complexity.

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

(45) CdtNarrowingProof (BOTH BOUNDS(ID, ID))
Use narrowing to replace LAST(z0, z1) -> c7(IF(empty(z1), z0, z1)) by 
   LAST(x0, nil) -> c7(IF(true, x0, nil))
   LAST(x0, cons(z0, z1)) -> c7(IF(false, x0, cons(z0, z1)))

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

(46)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   rev2(z0, nil) -> nil
   rev2(z0, cons(z1, z2)) -> rev(cons(z0, rev2(z1, z2)))
   rev(cons(z0, z1)) -> cons(rev1(z0, z1), rev2(z0, z1))
   empty(nil) -> true
   empty(cons(z0, z1)) -> false
   head(cons(z0, z1)) -> z0
   tail(nil) -> nil
   tail(cons(z0, z1)) -> z1
Tuples:
   REV(cons(z0, z1)) -> c6(REV2(z0, z1))
   REV2(z0, cons(z1, z2)) -> c12(REV(cons(z0, rev2(z1, z2))), REV2(z1, z2))
   IF(false, z0, z1) -> c9(LAST(head(z1), tail(z1)))
   IF(false, z0, z1) -> c10(LAST(head(z1), tail(z1)))
   LAST(x0, nil) -> c7(IF(true, x0, nil))
   LAST(x0, cons(z0, z1)) -> c7(IF(false, x0, cons(z0, z1)))
S tuples:
   REV(cons(z0, z1)) -> c6(REV2(z0, z1))
   REV2(z0, cons(z1, z2)) -> c12(REV(cons(z0, rev2(z1, z2))), REV2(z1, z2))
   IF(false, z0, z1) -> c9(LAST(head(z1), tail(z1)))
   IF(false, z0, z1) -> c10(LAST(head(z1), tail(z1)))
   LAST(x0, nil) -> c7(IF(true, x0, nil))
   LAST(x0, cons(z0, z1)) -> c7(IF(false, x0, cons(z0, z1)))
K tuples:none
Defined Rule Symbols:   rev2_2, rev_1, empty_1, head_1, tail_1

Defined Pair Symbols:   REV_1, REV2_2, IF_3, LAST_2

Compound Symbols:   c6_1, c12_2, c9_1, c10_1, c7_1


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

(47) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID))
Removed 1 trailing nodes:
   LAST(x0, nil) -> c7(IF(true, x0, nil))

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

(48)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   rev2(z0, nil) -> nil
   rev2(z0, cons(z1, z2)) -> rev(cons(z0, rev2(z1, z2)))
   rev(cons(z0, z1)) -> cons(rev1(z0, z1), rev2(z0, z1))
   empty(nil) -> true
   empty(cons(z0, z1)) -> false
   head(cons(z0, z1)) -> z0
   tail(nil) -> nil
   tail(cons(z0, z1)) -> z1
Tuples:
   REV(cons(z0, z1)) -> c6(REV2(z0, z1))
   REV2(z0, cons(z1, z2)) -> c12(REV(cons(z0, rev2(z1, z2))), REV2(z1, z2))
   IF(false, z0, z1) -> c9(LAST(head(z1), tail(z1)))
   IF(false, z0, z1) -> c10(LAST(head(z1), tail(z1)))
   LAST(x0, cons(z0, z1)) -> c7(IF(false, x0, cons(z0, z1)))
S tuples:
   REV(cons(z0, z1)) -> c6(REV2(z0, z1))
   REV2(z0, cons(z1, z2)) -> c12(REV(cons(z0, rev2(z1, z2))), REV2(z1, z2))
   IF(false, z0, z1) -> c9(LAST(head(z1), tail(z1)))
   IF(false, z0, z1) -> c10(LAST(head(z1), tail(z1)))
   LAST(x0, cons(z0, z1)) -> c7(IF(false, x0, cons(z0, z1)))
K tuples:none
Defined Rule Symbols:   rev2_2, rev_1, empty_1, head_1, tail_1

Defined Pair Symbols:   REV_1, REV2_2, IF_3, LAST_2

Compound Symbols:   c6_1, c12_2, c9_1, c10_1, c7_1


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

(49) CdtUsableRulesProof (BOTH BOUNDS(ID, ID))
The following rules are not usable and were removed:
   empty(nil) -> true
   empty(cons(z0, z1)) -> false

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

(50)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   rev2(z0, nil) -> nil
   rev2(z0, cons(z1, z2)) -> rev(cons(z0, rev2(z1, z2)))
   rev(cons(z0, z1)) -> cons(rev1(z0, z1), rev2(z0, z1))
   head(cons(z0, z1)) -> z0
   tail(nil) -> nil
   tail(cons(z0, z1)) -> z1
Tuples:
   REV(cons(z0, z1)) -> c6(REV2(z0, z1))
   REV2(z0, cons(z1, z2)) -> c12(REV(cons(z0, rev2(z1, z2))), REV2(z1, z2))
   IF(false, z0, z1) -> c9(LAST(head(z1), tail(z1)))
   IF(false, z0, z1) -> c10(LAST(head(z1), tail(z1)))
   LAST(x0, cons(z0, z1)) -> c7(IF(false, x0, cons(z0, z1)))
S tuples:
   REV(cons(z0, z1)) -> c6(REV2(z0, z1))
   REV2(z0, cons(z1, z2)) -> c12(REV(cons(z0, rev2(z1, z2))), REV2(z1, z2))
   IF(false, z0, z1) -> c9(LAST(head(z1), tail(z1)))
   IF(false, z0, z1) -> c10(LAST(head(z1), tail(z1)))
   LAST(x0, cons(z0, z1)) -> c7(IF(false, x0, cons(z0, z1)))
K tuples:none
Defined Rule Symbols:   rev2_2, rev_1, head_1, tail_1

Defined Pair Symbols:   REV_1, REV2_2, IF_3, LAST_2

Compound Symbols:   c6_1, c12_2, c9_1, c10_1, c7_1


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

(51) CdtNarrowingProof (BOTH BOUNDS(ID, ID))
Use narrowing to replace IF(false, z0, z1) -> c9(LAST(head(z1), tail(z1))) by 
   IF(false, x0, nil) -> c9(LAST(head(nil), nil))
   IF(false, x0, cons(z0, z1)) -> c9(LAST(head(cons(z0, z1)), z1))
   IF(false, x0, cons(z0, z1)) -> c9(LAST(z0, tail(cons(z0, z1))))

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

(52)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   rev2(z0, nil) -> nil
   rev2(z0, cons(z1, z2)) -> rev(cons(z0, rev2(z1, z2)))
   rev(cons(z0, z1)) -> cons(rev1(z0, z1), rev2(z0, z1))
   head(cons(z0, z1)) -> z0
   tail(nil) -> nil
   tail(cons(z0, z1)) -> z1
Tuples:
   REV(cons(z0, z1)) -> c6(REV2(z0, z1))
   REV2(z0, cons(z1, z2)) -> c12(REV(cons(z0, rev2(z1, z2))), REV2(z1, z2))
   IF(false, z0, z1) -> c10(LAST(head(z1), tail(z1)))
   LAST(x0, cons(z0, z1)) -> c7(IF(false, x0, cons(z0, z1)))
   IF(false, x0, nil) -> c9(LAST(head(nil), nil))
   IF(false, x0, cons(z0, z1)) -> c9(LAST(head(cons(z0, z1)), z1))
   IF(false, x0, cons(z0, z1)) -> c9(LAST(z0, tail(cons(z0, z1))))
S tuples:
   REV(cons(z0, z1)) -> c6(REV2(z0, z1))
   REV2(z0, cons(z1, z2)) -> c12(REV(cons(z0, rev2(z1, z2))), REV2(z1, z2))
   IF(false, z0, z1) -> c10(LAST(head(z1), tail(z1)))
   LAST(x0, cons(z0, z1)) -> c7(IF(false, x0, cons(z0, z1)))
   IF(false, x0, nil) -> c9(LAST(head(nil), nil))
   IF(false, x0, cons(z0, z1)) -> c9(LAST(head(cons(z0, z1)), z1))
   IF(false, x0, cons(z0, z1)) -> c9(LAST(z0, tail(cons(z0, z1))))
K tuples:none
Defined Rule Symbols:   rev2_2, rev_1, head_1, tail_1

Defined Pair Symbols:   REV_1, REV2_2, IF_3, LAST_2

Compound Symbols:   c6_1, c12_2, c10_1, c7_1, c9_1


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

(53) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID))
Removed 1 trailing nodes:
   IF(false, x0, nil) -> c9(LAST(head(nil), nil))

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

(54)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   rev2(z0, nil) -> nil
   rev2(z0, cons(z1, z2)) -> rev(cons(z0, rev2(z1, z2)))
   rev(cons(z0, z1)) -> cons(rev1(z0, z1), rev2(z0, z1))
   head(cons(z0, z1)) -> z0
   tail(nil) -> nil
   tail(cons(z0, z1)) -> z1
Tuples:
   REV(cons(z0, z1)) -> c6(REV2(z0, z1))
   REV2(z0, cons(z1, z2)) -> c12(REV(cons(z0, rev2(z1, z2))), REV2(z1, z2))
   IF(false, z0, z1) -> c10(LAST(head(z1), tail(z1)))
   LAST(x0, cons(z0, z1)) -> c7(IF(false, x0, cons(z0, z1)))
   IF(false, x0, cons(z0, z1)) -> c9(LAST(head(cons(z0, z1)), z1))
   IF(false, x0, cons(z0, z1)) -> c9(LAST(z0, tail(cons(z0, z1))))
S tuples:
   REV(cons(z0, z1)) -> c6(REV2(z0, z1))
   REV2(z0, cons(z1, z2)) -> c12(REV(cons(z0, rev2(z1, z2))), REV2(z1, z2))
   IF(false, z0, z1) -> c10(LAST(head(z1), tail(z1)))
   LAST(x0, cons(z0, z1)) -> c7(IF(false, x0, cons(z0, z1)))
   IF(false, x0, cons(z0, z1)) -> c9(LAST(head(cons(z0, z1)), z1))
   IF(false, x0, cons(z0, z1)) -> c9(LAST(z0, tail(cons(z0, z1))))
K tuples:none
Defined Rule Symbols:   rev2_2, rev_1, head_1, tail_1

Defined Pair Symbols:   REV_1, REV2_2, IF_3, LAST_2

Compound Symbols:   c6_1, c12_2, c10_1, c7_1, c9_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.
   IF(false, x0, cons(z0, z1)) -> c9(LAST(head(cons(z0, z1)), z1))
We considered the (Usable) Rules:
   tail(cons(z0, z1)) -> z1
   tail(nil) -> nil
And the Tuples:
   REV(cons(z0, z1)) -> c6(REV2(z0, z1))
   REV2(z0, cons(z1, z2)) -> c12(REV(cons(z0, rev2(z1, z2))), REV2(z1, z2))
   IF(false, z0, z1) -> c10(LAST(head(z1), tail(z1)))
   LAST(x0, cons(z0, z1)) -> c7(IF(false, x0, cons(z0, z1)))
   IF(false, x0, cons(z0, z1)) -> c9(LAST(head(cons(z0, z1)), z1))
   IF(false, x0, cons(z0, z1)) -> c9(LAST(z0, tail(cons(z0, z1))))
The order we found is given by the following interpretation:

Polynomial interpretation :

   POL(IF(x_1, x_2, x_3)) = x_3
   POL(LAST(x_1, x_2)) = x_2
   POL(REV(x_1)) = 0
   POL(REV2(x_1, x_2)) = 0
   POL(c10(x_1)) = x_1
   POL(c12(x_1, x_2)) = x_1 + x_2
   POL(c6(x_1)) = x_1
   POL(c7(x_1)) = x_1
   POL(c9(x_1)) = x_1
   POL(cons(x_1, x_2)) = [1] + x_1 + x_2
   POL(false) = [1]
   POL(head(x_1)) = [1] + x_1
   POL(nil) = [1]
   POL(rev(x_1)) = [1]
   POL(rev1(x_1, x_2)) = [1] + x_1 + x_2
   POL(rev2(x_1, x_2)) = [1] + x_1 + x_2
   POL(tail(x_1)) = x_1

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

(56)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   rev2(z0, nil) -> nil
   rev2(z0, cons(z1, z2)) -> rev(cons(z0, rev2(z1, z2)))
   rev(cons(z0, z1)) -> cons(rev1(z0, z1), rev2(z0, z1))
   head(cons(z0, z1)) -> z0
   tail(nil) -> nil
   tail(cons(z0, z1)) -> z1
Tuples:
   REV(cons(z0, z1)) -> c6(REV2(z0, z1))
   REV2(z0, cons(z1, z2)) -> c12(REV(cons(z0, rev2(z1, z2))), REV2(z1, z2))
   IF(false, z0, z1) -> c10(LAST(head(z1), tail(z1)))
   LAST(x0, cons(z0, z1)) -> c7(IF(false, x0, cons(z0, z1)))
   IF(false, x0, cons(z0, z1)) -> c9(LAST(head(cons(z0, z1)), z1))
   IF(false, x0, cons(z0, z1)) -> c9(LAST(z0, tail(cons(z0, z1))))
S tuples:
   REV(cons(z0, z1)) -> c6(REV2(z0, z1))
   REV2(z0, cons(z1, z2)) -> c12(REV(cons(z0, rev2(z1, z2))), REV2(z1, z2))
   IF(false, z0, z1) -> c10(LAST(head(z1), tail(z1)))
   LAST(x0, cons(z0, z1)) -> c7(IF(false, x0, cons(z0, z1)))
   IF(false, x0, cons(z0, z1)) -> c9(LAST(z0, tail(cons(z0, z1))))
K tuples:
   IF(false, x0, cons(z0, z1)) -> c9(LAST(head(cons(z0, z1)), z1))
Defined Rule Symbols:   rev2_2, rev_1, head_1, tail_1

Defined Pair Symbols:   REV_1, REV2_2, IF_3, LAST_2

Compound Symbols:   c6_1, c12_2, c10_1, c7_1, c9_1


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

(57) CdtNarrowingProof (BOTH BOUNDS(ID, ID))
Use narrowing to replace IF(false, z0, z1) -> c10(LAST(head(z1), tail(z1))) by 
   IF(false, x0, nil) -> c10(LAST(head(nil), nil))
   IF(false, x0, cons(z0, z1)) -> c10(LAST(head(cons(z0, z1)), z1))
   IF(false, x0, cons(z0, z1)) -> c10(LAST(z0, tail(cons(z0, z1))))

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

(58)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   rev2(z0, nil) -> nil
   rev2(z0, cons(z1, z2)) -> rev(cons(z0, rev2(z1, z2)))
   rev(cons(z0, z1)) -> cons(rev1(z0, z1), rev2(z0, z1))
   head(cons(z0, z1)) -> z0
   tail(nil) -> nil
   tail(cons(z0, z1)) -> z1
Tuples:
   REV(cons(z0, z1)) -> c6(REV2(z0, z1))
   REV2(z0, cons(z1, z2)) -> c12(REV(cons(z0, rev2(z1, z2))), REV2(z1, z2))
   LAST(x0, cons(z0, z1)) -> c7(IF(false, x0, cons(z0, z1)))
   IF(false, x0, cons(z0, z1)) -> c9(LAST(head(cons(z0, z1)), z1))
   IF(false, x0, cons(z0, z1)) -> c9(LAST(z0, tail(cons(z0, z1))))
   IF(false, x0, nil) -> c10(LAST(head(nil), nil))
   IF(false, x0, cons(z0, z1)) -> c10(LAST(head(cons(z0, z1)), z1))
   IF(false, x0, cons(z0, z1)) -> c10(LAST(z0, tail(cons(z0, z1))))
S tuples:
   REV(cons(z0, z1)) -> c6(REV2(z0, z1))
   REV2(z0, cons(z1, z2)) -> c12(REV(cons(z0, rev2(z1, z2))), REV2(z1, z2))
   LAST(x0, cons(z0, z1)) -> c7(IF(false, x0, cons(z0, z1)))
   IF(false, x0, cons(z0, z1)) -> c9(LAST(z0, tail(cons(z0, z1))))
   IF(false, x0, nil) -> c10(LAST(head(nil), nil))
   IF(false, x0, cons(z0, z1)) -> c10(LAST(head(cons(z0, z1)), z1))
   IF(false, x0, cons(z0, z1)) -> c10(LAST(z0, tail(cons(z0, z1))))
K tuples:
   IF(false, x0, cons(z0, z1)) -> c9(LAST(head(cons(z0, z1)), z1))
Defined Rule Symbols:   rev2_2, rev_1, head_1, tail_1

Defined Pair Symbols:   REV_1, REV2_2, LAST_2, IF_3

Compound Symbols:   c6_1, c12_2, c7_1, c9_1, c10_1


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

(59) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID))
Removed 1 trailing nodes:
   IF(false, x0, nil) -> c10(LAST(head(nil), nil))

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

(60)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   rev2(z0, nil) -> nil
   rev2(z0, cons(z1, z2)) -> rev(cons(z0, rev2(z1, z2)))
   rev(cons(z0, z1)) -> cons(rev1(z0, z1), rev2(z0, z1))
   head(cons(z0, z1)) -> z0
   tail(nil) -> nil
   tail(cons(z0, z1)) -> z1
Tuples:
   REV(cons(z0, z1)) -> c6(REV2(z0, z1))
   REV2(z0, cons(z1, z2)) -> c12(REV(cons(z0, rev2(z1, z2))), REV2(z1, z2))
   LAST(x0, cons(z0, z1)) -> c7(IF(false, x0, cons(z0, z1)))
   IF(false, x0, cons(z0, z1)) -> c9(LAST(head(cons(z0, z1)), z1))
   IF(false, x0, cons(z0, z1)) -> c9(LAST(z0, tail(cons(z0, z1))))
   IF(false, x0, cons(z0, z1)) -> c10(LAST(head(cons(z0, z1)), z1))
   IF(false, x0, cons(z0, z1)) -> c10(LAST(z0, tail(cons(z0, z1))))
S tuples:
   REV(cons(z0, z1)) -> c6(REV2(z0, z1))
   REV2(z0, cons(z1, z2)) -> c12(REV(cons(z0, rev2(z1, z2))), REV2(z1, z2))
   LAST(x0, cons(z0, z1)) -> c7(IF(false, x0, cons(z0, z1)))
   IF(false, x0, cons(z0, z1)) -> c9(LAST(z0, tail(cons(z0, z1))))
   IF(false, x0, cons(z0, z1)) -> c10(LAST(head(cons(z0, z1)), z1))
   IF(false, x0, cons(z0, z1)) -> c10(LAST(z0, tail(cons(z0, z1))))
K tuples:
   IF(false, x0, cons(z0, z1)) -> c9(LAST(head(cons(z0, z1)), z1))
Defined Rule Symbols:   rev2_2, rev_1, head_1, tail_1

Defined Pair Symbols:   REV_1, REV2_2, LAST_2, IF_3

Compound Symbols:   c6_1, c12_2, c7_1, c9_1, c10_1


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

(61) CdtUsableRulesProof (BOTH BOUNDS(ID, ID))
The following rules are not usable and were removed:
   tail(nil) -> nil

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

(62)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   rev2(z0, nil) -> nil
   rev2(z0, cons(z1, z2)) -> rev(cons(z0, rev2(z1, z2)))
   rev(cons(z0, z1)) -> cons(rev1(z0, z1), rev2(z0, z1))
   head(cons(z0, z1)) -> z0
   tail(cons(z0, z1)) -> z1
Tuples:
   REV(cons(z0, z1)) -> c6(REV2(z0, z1))
   REV2(z0, cons(z1, z2)) -> c12(REV(cons(z0, rev2(z1, z2))), REV2(z1, z2))
   LAST(x0, cons(z0, z1)) -> c7(IF(false, x0, cons(z0, z1)))
   IF(false, x0, cons(z0, z1)) -> c9(LAST(head(cons(z0, z1)), z1))
   IF(false, x0, cons(z0, z1)) -> c9(LAST(z0, tail(cons(z0, z1))))
   IF(false, x0, cons(z0, z1)) -> c10(LAST(head(cons(z0, z1)), z1))
   IF(false, x0, cons(z0, z1)) -> c10(LAST(z0, tail(cons(z0, z1))))
S tuples:
   REV(cons(z0, z1)) -> c6(REV2(z0, z1))
   REV2(z0, cons(z1, z2)) -> c12(REV(cons(z0, rev2(z1, z2))), REV2(z1, z2))
   LAST(x0, cons(z0, z1)) -> c7(IF(false, x0, cons(z0, z1)))
   IF(false, x0, cons(z0, z1)) -> c9(LAST(z0, tail(cons(z0, z1))))
   IF(false, x0, cons(z0, z1)) -> c10(LAST(head(cons(z0, z1)), z1))
   IF(false, x0, cons(z0, z1)) -> c10(LAST(z0, tail(cons(z0, z1))))
K tuples:
   IF(false, x0, cons(z0, z1)) -> c9(LAST(head(cons(z0, z1)), z1))
Defined Rule Symbols:   rev2_2, rev_1, head_1, tail_1

Defined Pair Symbols:   REV_1, REV2_2, LAST_2, IF_3

Compound Symbols:   c6_1, c12_2, c7_1, c9_1, c10_1


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

(63) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)))
Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.
   IF(false, x0, cons(z0, z1)) -> c10(LAST(head(cons(z0, z1)), z1))
We considered the (Usable) Rules:
   tail(cons(z0, z1)) -> z1
And the Tuples:
   REV(cons(z0, z1)) -> c6(REV2(z0, z1))
   REV2(z0, cons(z1, z2)) -> c12(REV(cons(z0, rev2(z1, z2))), REV2(z1, z2))
   LAST(x0, cons(z0, z1)) -> c7(IF(false, x0, cons(z0, z1)))
   IF(false, x0, cons(z0, z1)) -> c9(LAST(head(cons(z0, z1)), z1))
   IF(false, x0, cons(z0, z1)) -> c9(LAST(z0, tail(cons(z0, z1))))
   IF(false, x0, cons(z0, z1)) -> c10(LAST(head(cons(z0, z1)), z1))
   IF(false, x0, cons(z0, z1)) -> c10(LAST(z0, tail(cons(z0, z1))))
The order we found is given by the following interpretation:

Polynomial interpretation :

   POL(IF(x_1, x_2, x_3)) = x_3
   POL(LAST(x_1, x_2)) = x_2
   POL(REV(x_1)) = 0
   POL(REV2(x_1, x_2)) = 0
   POL(c10(x_1)) = x_1
   POL(c12(x_1, x_2)) = x_1 + x_2
   POL(c6(x_1)) = x_1
   POL(c7(x_1)) = x_1
   POL(c9(x_1)) = x_1
   POL(cons(x_1, x_2)) = [1] + x_1 + x_2
   POL(false) = [1]
   POL(head(x_1)) = [1] + x_1
   POL(nil) = [1]
   POL(rev(x_1)) = [1]
   POL(rev1(x_1, x_2)) = [1] + x_1 + x_2
   POL(rev2(x_1, x_2)) = [1] + x_1 + x_2
   POL(tail(x_1)) = x_1

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

(64)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   rev2(z0, nil) -> nil
   rev2(z0, cons(z1, z2)) -> rev(cons(z0, rev2(z1, z2)))
   rev(cons(z0, z1)) -> cons(rev1(z0, z1), rev2(z0, z1))
   head(cons(z0, z1)) -> z0
   tail(cons(z0, z1)) -> z1
Tuples:
   REV(cons(z0, z1)) -> c6(REV2(z0, z1))
   REV2(z0, cons(z1, z2)) -> c12(REV(cons(z0, rev2(z1, z2))), REV2(z1, z2))
   LAST(x0, cons(z0, z1)) -> c7(IF(false, x0, cons(z0, z1)))
   IF(false, x0, cons(z0, z1)) -> c9(LAST(head(cons(z0, z1)), z1))
   IF(false, x0, cons(z0, z1)) -> c9(LAST(z0, tail(cons(z0, z1))))
   IF(false, x0, cons(z0, z1)) -> c10(LAST(head(cons(z0, z1)), z1))
   IF(false, x0, cons(z0, z1)) -> c10(LAST(z0, tail(cons(z0, z1))))
S tuples:
   REV(cons(z0, z1)) -> c6(REV2(z0, z1))
   REV2(z0, cons(z1, z2)) -> c12(REV(cons(z0, rev2(z1, z2))), REV2(z1, z2))
   LAST(x0, cons(z0, z1)) -> c7(IF(false, x0, cons(z0, z1)))
   IF(false, x0, cons(z0, z1)) -> c9(LAST(z0, tail(cons(z0, z1))))
   IF(false, x0, cons(z0, z1)) -> c10(LAST(z0, tail(cons(z0, z1))))
K tuples:
   IF(false, x0, cons(z0, z1)) -> c9(LAST(head(cons(z0, z1)), z1))
   IF(false, x0, cons(z0, z1)) -> c10(LAST(head(cons(z0, z1)), z1))
Defined Rule Symbols:   rev2_2, rev_1, head_1, tail_1

Defined Pair Symbols:   REV_1, REV2_2, LAST_2, IF_3

Compound Symbols:   c6_1, c12_2, c7_1, c9_1, c10_1


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

(65) CdtNarrowingProof (BOTH BOUNDS(ID, ID))
Use narrowing to replace IF(false, x0, cons(z0, z1)) -> c9(LAST(head(cons(z0, z1)), z1)) by 
   IF(false, x0, cons(z0, z1)) -> c9(LAST(z0, z1))

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

(66)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   rev2(z0, nil) -> nil
   rev2(z0, cons(z1, z2)) -> rev(cons(z0, rev2(z1, z2)))
   rev(cons(z0, z1)) -> cons(rev1(z0, z1), rev2(z0, z1))
   head(cons(z0, z1)) -> z0
   tail(cons(z0, z1)) -> z1
Tuples:
   REV(cons(z0, z1)) -> c6(REV2(z0, z1))
   REV2(z0, cons(z1, z2)) -> c12(REV(cons(z0, rev2(z1, z2))), REV2(z1, z2))
   LAST(x0, cons(z0, z1)) -> c7(IF(false, x0, cons(z0, z1)))
   IF(false, x0, cons(z0, z1)) -> c9(LAST(z0, tail(cons(z0, z1))))
   IF(false, x0, cons(z0, z1)) -> c10(LAST(head(cons(z0, z1)), z1))
   IF(false, x0, cons(z0, z1)) -> c10(LAST(z0, tail(cons(z0, z1))))
   IF(false, x0, cons(z0, z1)) -> c9(LAST(z0, z1))
S tuples:
   REV(cons(z0, z1)) -> c6(REV2(z0, z1))
   REV2(z0, cons(z1, z2)) -> c12(REV(cons(z0, rev2(z1, z2))), REV2(z1, z2))
   LAST(x0, cons(z0, z1)) -> c7(IF(false, x0, cons(z0, z1)))
   IF(false, x0, cons(z0, z1)) -> c9(LAST(z0, tail(cons(z0, z1))))
   IF(false, x0, cons(z0, z1)) -> c10(LAST(z0, tail(cons(z0, z1))))
K tuples:
   IF(false, x0, cons(z0, z1)) -> c9(LAST(head(cons(z0, z1)), z1))
   IF(false, x0, cons(z0, z1)) -> c10(LAST(head(cons(z0, z1)), z1))
Defined Rule Symbols:   rev2_2, rev_1, head_1, tail_1

Defined Pair Symbols:   REV_1, REV2_2, LAST_2, IF_3

Compound Symbols:   c6_1, c12_2, c7_1, c9_1, c10_1


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

(67) CdtNarrowingProof (BOTH BOUNDS(ID, ID))
Use narrowing to replace IF(false, x0, cons(z0, z1)) -> c9(LAST(z0, tail(cons(z0, z1)))) by 
   IF(false, x0, cons(z0, z1)) -> c9(LAST(z0, z1))

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

(68)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   rev2(z0, nil) -> nil
   rev2(z0, cons(z1, z2)) -> rev(cons(z0, rev2(z1, z2)))
   rev(cons(z0, z1)) -> cons(rev1(z0, z1), rev2(z0, z1))
   head(cons(z0, z1)) -> z0
   tail(cons(z0, z1)) -> z1
Tuples:
   REV(cons(z0, z1)) -> c6(REV2(z0, z1))
   REV2(z0, cons(z1, z2)) -> c12(REV(cons(z0, rev2(z1, z2))), REV2(z1, z2))
   LAST(x0, cons(z0, z1)) -> c7(IF(false, x0, cons(z0, z1)))
   IF(false, x0, cons(z0, z1)) -> c10(LAST(head(cons(z0, z1)), z1))
   IF(false, x0, cons(z0, z1)) -> c10(LAST(z0, tail(cons(z0, z1))))
   IF(false, x0, cons(z0, z1)) -> c9(LAST(z0, z1))
S tuples:
   REV(cons(z0, z1)) -> c6(REV2(z0, z1))
   REV2(z0, cons(z1, z2)) -> c12(REV(cons(z0, rev2(z1, z2))), REV2(z1, z2))
   LAST(x0, cons(z0, z1)) -> c7(IF(false, x0, cons(z0, z1)))
   IF(false, x0, cons(z0, z1)) -> c10(LAST(z0, tail(cons(z0, z1))))
   IF(false, x0, cons(z0, z1)) -> c9(LAST(z0, z1))
K tuples:
   IF(false, x0, cons(z0, z1)) -> c9(LAST(head(cons(z0, z1)), z1))
   IF(false, x0, cons(z0, z1)) -> c10(LAST(head(cons(z0, z1)), z1))
Defined Rule Symbols:   rev2_2, rev_1, head_1, tail_1

Defined Pair Symbols:   REV_1, REV2_2, LAST_2, IF_3

Compound Symbols:   c6_1, c12_2, c7_1, c10_1, c9_1


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

(69) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)))
Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.
   IF(false, x0, cons(z0, z1)) -> c9(LAST(z0, z1))
We considered the (Usable) Rules:
   tail(cons(z0, z1)) -> z1
And the Tuples:
   REV(cons(z0, z1)) -> c6(REV2(z0, z1))
   REV2(z0, cons(z1, z2)) -> c12(REV(cons(z0, rev2(z1, z2))), REV2(z1, z2))
   LAST(x0, cons(z0, z1)) -> c7(IF(false, x0, cons(z0, z1)))
   IF(false, x0, cons(z0, z1)) -> c10(LAST(head(cons(z0, z1)), z1))
   IF(false, x0, cons(z0, z1)) -> c10(LAST(z0, tail(cons(z0, z1))))
   IF(false, x0, cons(z0, z1)) -> c9(LAST(z0, z1))
The order we found is given by the following interpretation:

Polynomial interpretation :

   POL(IF(x_1, x_2, x_3)) = x_3
   POL(LAST(x_1, x_2)) = x_2
   POL(REV(x_1)) = 0
   POL(REV2(x_1, x_2)) = 0
   POL(c10(x_1)) = x_1
   POL(c12(x_1, x_2)) = x_1 + x_2
   POL(c6(x_1)) = x_1
   POL(c7(x_1)) = x_1
   POL(c9(x_1)) = x_1
   POL(cons(x_1, x_2)) = [1] + x_1 + x_2
   POL(false) = [1]
   POL(head(x_1)) = [1] + x_1
   POL(nil) = [1]
   POL(rev(x_1)) = [1] + x_1
   POL(rev1(x_1, x_2)) = [1] + x_1 + x_2
   POL(rev2(x_1, x_2)) = [1] + x_1 + x_2
   POL(tail(x_1)) = x_1

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

(70)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   rev2(z0, nil) -> nil
   rev2(z0, cons(z1, z2)) -> rev(cons(z0, rev2(z1, z2)))
   rev(cons(z0, z1)) -> cons(rev1(z0, z1), rev2(z0, z1))
   head(cons(z0, z1)) -> z0
   tail(cons(z0, z1)) -> z1
Tuples:
   REV(cons(z0, z1)) -> c6(REV2(z0, z1))
   REV2(z0, cons(z1, z2)) -> c12(REV(cons(z0, rev2(z1, z2))), REV2(z1, z2))
   LAST(x0, cons(z0, z1)) -> c7(IF(false, x0, cons(z0, z1)))
   IF(false, x0, cons(z0, z1)) -> c10(LAST(head(cons(z0, z1)), z1))
   IF(false, x0, cons(z0, z1)) -> c10(LAST(z0, tail(cons(z0, z1))))
   IF(false, x0, cons(z0, z1)) -> c9(LAST(z0, z1))
S tuples:
   REV(cons(z0, z1)) -> c6(REV2(z0, z1))
   REV2(z0, cons(z1, z2)) -> c12(REV(cons(z0, rev2(z1, z2))), REV2(z1, z2))
   LAST(x0, cons(z0, z1)) -> c7(IF(false, x0, cons(z0, z1)))
   IF(false, x0, cons(z0, z1)) -> c10(LAST(z0, tail(cons(z0, z1))))
K tuples:
   IF(false, x0, cons(z0, z1)) -> c9(LAST(head(cons(z0, z1)), z1))
   IF(false, x0, cons(z0, z1)) -> c10(LAST(head(cons(z0, z1)), z1))
   IF(false, x0, cons(z0, z1)) -> c9(LAST(z0, z1))
Defined Rule Symbols:   rev2_2, rev_1, head_1, tail_1

Defined Pair Symbols:   REV_1, REV2_2, LAST_2, IF_3

Compound Symbols:   c6_1, c12_2, c7_1, c10_1, c9_1


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

(71) CdtNarrowingProof (BOTH BOUNDS(ID, ID))
Use narrowing to replace IF(false, x0, cons(z0, z1)) -> c10(LAST(head(cons(z0, z1)), z1)) by 
   IF(false, x0, cons(z0, z1)) -> c10(LAST(z0, z1))

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

(72)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   rev2(z0, nil) -> nil
   rev2(z0, cons(z1, z2)) -> rev(cons(z0, rev2(z1, z2)))
   rev(cons(z0, z1)) -> cons(rev1(z0, z1), rev2(z0, z1))
   head(cons(z0, z1)) -> z0
   tail(cons(z0, z1)) -> z1
Tuples:
   REV(cons(z0, z1)) -> c6(REV2(z0, z1))
   REV2(z0, cons(z1, z2)) -> c12(REV(cons(z0, rev2(z1, z2))), REV2(z1, z2))
   LAST(x0, cons(z0, z1)) -> c7(IF(false, x0, cons(z0, z1)))
   IF(false, x0, cons(z0, z1)) -> c10(LAST(z0, tail(cons(z0, z1))))
   IF(false, x0, cons(z0, z1)) -> c9(LAST(z0, z1))
   IF(false, x0, cons(z0, z1)) -> c10(LAST(z0, z1))
S tuples:
   REV(cons(z0, z1)) -> c6(REV2(z0, z1))
   REV2(z0, cons(z1, z2)) -> c12(REV(cons(z0, rev2(z1, z2))), REV2(z1, z2))
   LAST(x0, cons(z0, z1)) -> c7(IF(false, x0, cons(z0, z1)))
   IF(false, x0, cons(z0, z1)) -> c10(LAST(z0, tail(cons(z0, z1))))
K tuples:
   IF(false, x0, cons(z0, z1)) -> c9(LAST(head(cons(z0, z1)), z1))
   IF(false, x0, cons(z0, z1)) -> c10(LAST(head(cons(z0, z1)), z1))
   IF(false, x0, cons(z0, z1)) -> c9(LAST(z0, z1))
Defined Rule Symbols:   rev2_2, rev_1, head_1, tail_1

Defined Pair Symbols:   REV_1, REV2_2, LAST_2, IF_3

Compound Symbols:   c6_1, c12_2, c7_1, c10_1, c9_1


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

(73) CdtUsableRulesProof (BOTH BOUNDS(ID, ID))
The following rules are not usable and were removed:
   head(cons(z0, z1)) -> z0

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

(74)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   rev2(z0, nil) -> nil
   rev2(z0, cons(z1, z2)) -> rev(cons(z0, rev2(z1, z2)))
   rev(cons(z0, z1)) -> cons(rev1(z0, z1), rev2(z0, z1))
   tail(cons(z0, z1)) -> z1
Tuples:
   REV(cons(z0, z1)) -> c6(REV2(z0, z1))
   REV2(z0, cons(z1, z2)) -> c12(REV(cons(z0, rev2(z1, z2))), REV2(z1, z2))
   LAST(x0, cons(z0, z1)) -> c7(IF(false, x0, cons(z0, z1)))
   IF(false, x0, cons(z0, z1)) -> c10(LAST(z0, tail(cons(z0, z1))))
   IF(false, x0, cons(z0, z1)) -> c9(LAST(z0, z1))
   IF(false, x0, cons(z0, z1)) -> c10(LAST(z0, z1))
S tuples:
   REV(cons(z0, z1)) -> c6(REV2(z0, z1))
   REV2(z0, cons(z1, z2)) -> c12(REV(cons(z0, rev2(z1, z2))), REV2(z1, z2))
   LAST(x0, cons(z0, z1)) -> c7(IF(false, x0, cons(z0, z1)))
   IF(false, x0, cons(z0, z1)) -> c10(LAST(z0, tail(cons(z0, z1))))
K tuples:
   IF(false, x0, cons(z0, z1)) -> c9(LAST(head(cons(z0, z1)), z1))
   IF(false, x0, cons(z0, z1)) -> c10(LAST(head(cons(z0, z1)), z1))
   IF(false, x0, cons(z0, z1)) -> c9(LAST(z0, z1))
Defined Rule Symbols:   rev2_2, rev_1, tail_1

Defined Pair Symbols:   REV_1, REV2_2, LAST_2, IF_3

Compound Symbols:   c6_1, c12_2, c7_1, c10_1, c9_1


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

(75) CdtNarrowingProof (BOTH BOUNDS(ID, ID))
Use narrowing to replace IF(false, x0, cons(z0, z1)) -> c10(LAST(z0, tail(cons(z0, z1)))) by 
   IF(false, x0, cons(z0, z1)) -> c10(LAST(z0, z1))

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

(76)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   rev2(z0, nil) -> nil
   rev2(z0, cons(z1, z2)) -> rev(cons(z0, rev2(z1, z2)))
   rev(cons(z0, z1)) -> cons(rev1(z0, z1), rev2(z0, z1))
   tail(cons(z0, z1)) -> z1
Tuples:
   REV(cons(z0, z1)) -> c6(REV2(z0, z1))
   REV2(z0, cons(z1, z2)) -> c12(REV(cons(z0, rev2(z1, z2))), REV2(z1, z2))
   LAST(x0, cons(z0, z1)) -> c7(IF(false, x0, cons(z0, z1)))
   IF(false, x0, cons(z0, z1)) -> c9(LAST(z0, z1))
   IF(false, x0, cons(z0, z1)) -> c10(LAST(z0, z1))
S tuples:
   REV(cons(z0, z1)) -> c6(REV2(z0, z1))
   REV2(z0, cons(z1, z2)) -> c12(REV(cons(z0, rev2(z1, z2))), REV2(z1, z2))
   LAST(x0, cons(z0, z1)) -> c7(IF(false, x0, cons(z0, z1)))
   IF(false, x0, cons(z0, z1)) -> c10(LAST(z0, z1))
K tuples:
   IF(false, x0, cons(z0, z1)) -> c9(LAST(head(cons(z0, z1)), z1))
   IF(false, x0, cons(z0, z1)) -> c10(LAST(head(cons(z0, z1)), z1))
   IF(false, x0, cons(z0, z1)) -> c9(LAST(z0, z1))
Defined Rule Symbols:   rev2_2, rev_1, tail_1

Defined Pair Symbols:   REV_1, REV2_2, LAST_2, IF_3

Compound Symbols:   c6_1, c12_2, c7_1, c9_1, c10_1


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

(77) CdtUsableRulesProof (BOTH BOUNDS(ID, ID))
The following rules are not usable and were removed:
   tail(cons(z0, z1)) -> z1

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

(78)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   rev2(z0, nil) -> nil
   rev2(z0, cons(z1, z2)) -> rev(cons(z0, rev2(z1, z2)))
   rev(cons(z0, z1)) -> cons(rev1(z0, z1), rev2(z0, z1))
Tuples:
   REV(cons(z0, z1)) -> c6(REV2(z0, z1))
   REV2(z0, cons(z1, z2)) -> c12(REV(cons(z0, rev2(z1, z2))), REV2(z1, z2))
   LAST(x0, cons(z0, z1)) -> c7(IF(false, x0, cons(z0, z1)))
   IF(false, x0, cons(z0, z1)) -> c9(LAST(z0, z1))
   IF(false, x0, cons(z0, z1)) -> c10(LAST(z0, z1))
S tuples:
   REV(cons(z0, z1)) -> c6(REV2(z0, z1))
   REV2(z0, cons(z1, z2)) -> c12(REV(cons(z0, rev2(z1, z2))), REV2(z1, z2))
   LAST(x0, cons(z0, z1)) -> c7(IF(false, x0, cons(z0, z1)))
   IF(false, x0, cons(z0, z1)) -> c10(LAST(z0, z1))
K tuples:
   IF(false, x0, cons(z0, z1)) -> c9(LAST(head(cons(z0, z1)), z1))
   IF(false, x0, cons(z0, z1)) -> c10(LAST(head(cons(z0, z1)), z1))
   IF(false, x0, cons(z0, z1)) -> c9(LAST(z0, z1))
Defined Rule Symbols:   rev2_2, rev_1

Defined Pair Symbols:   REV_1, REV2_2, LAST_2, IF_3

Compound Symbols:   c6_1, c12_2, c7_1, c9_1, c10_1


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

(79) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)))
Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.
   IF(false, x0, cons(z0, z1)) -> c10(LAST(z0, z1))
We considered the (Usable) Rules:none
And the Tuples:
   REV(cons(z0, z1)) -> c6(REV2(z0, z1))
   REV2(z0, cons(z1, z2)) -> c12(REV(cons(z0, rev2(z1, z2))), REV2(z1, z2))
   LAST(x0, cons(z0, z1)) -> c7(IF(false, x0, cons(z0, z1)))
   IF(false, x0, cons(z0, z1)) -> c9(LAST(z0, z1))
   IF(false, x0, cons(z0, z1)) -> c10(LAST(z0, z1))
The order we found is given by the following interpretation:

Polynomial interpretation :

   POL(IF(x_1, x_2, x_3)) = x_3
   POL(LAST(x_1, x_2)) = x_2
   POL(REV(x_1)) = 0
   POL(REV2(x_1, x_2)) = 0
   POL(c10(x_1)) = x_1
   POL(c12(x_1, x_2)) = x_1 + x_2
   POL(c6(x_1)) = x_1
   POL(c7(x_1)) = x_1
   POL(c9(x_1)) = x_1
   POL(cons(x_1, x_2)) = [2] + x_2
   POL(false) = [3]
   POL(nil) = [3]
   POL(rev(x_1)) = [3]
   POL(rev1(x_1, x_2)) = [3] + x_1 + x_2
   POL(rev2(x_1, x_2)) = [2]x_1

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

(80)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   rev2(z0, nil) -> nil
   rev2(z0, cons(z1, z2)) -> rev(cons(z0, rev2(z1, z2)))
   rev(cons(z0, z1)) -> cons(rev1(z0, z1), rev2(z0, z1))
Tuples:
   REV(cons(z0, z1)) -> c6(REV2(z0, z1))
   REV2(z0, cons(z1, z2)) -> c12(REV(cons(z0, rev2(z1, z2))), REV2(z1, z2))
   LAST(x0, cons(z0, z1)) -> c7(IF(false, x0, cons(z0, z1)))
   IF(false, x0, cons(z0, z1)) -> c9(LAST(z0, z1))
   IF(false, x0, cons(z0, z1)) -> c10(LAST(z0, z1))
S tuples:
   REV(cons(z0, z1)) -> c6(REV2(z0, z1))
   REV2(z0, cons(z1, z2)) -> c12(REV(cons(z0, rev2(z1, z2))), REV2(z1, z2))
   LAST(x0, cons(z0, z1)) -> c7(IF(false, x0, cons(z0, z1)))
K tuples:
   IF(false, x0, cons(z0, z1)) -> c9(LAST(head(cons(z0, z1)), z1))
   IF(false, x0, cons(z0, z1)) -> c10(LAST(head(cons(z0, z1)), z1))
   IF(false, x0, cons(z0, z1)) -> c9(LAST(z0, z1))
   IF(false, x0, cons(z0, z1)) -> c10(LAST(z0, z1))
Defined Rule Symbols:   rev2_2, rev_1

Defined Pair Symbols:   REV_1, REV2_2, LAST_2, IF_3

Compound Symbols:   c6_1, c12_2, c7_1, c9_1, c10_1


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

(81) CdtKnowledgeProof (BOTH BOUNDS(ID, ID))
The following tuples could be moved from S to K by knowledge propagation:
   LAST(x0, cons(z0, z1)) -> c7(IF(false, x0, cons(z0, z1)))
   IF(false, x0, cons(z0, z1)) -> c9(LAST(z0, z1))
   IF(false, x0, cons(z0, z1)) -> c10(LAST(z0, z1))

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

(82)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   rev2(z0, nil) -> nil
   rev2(z0, cons(z1, z2)) -> rev(cons(z0, rev2(z1, z2)))
   rev(cons(z0, z1)) -> cons(rev1(z0, z1), rev2(z0, z1))
Tuples:
   REV(cons(z0, z1)) -> c6(REV2(z0, z1))
   REV2(z0, cons(z1, z2)) -> c12(REV(cons(z0, rev2(z1, z2))), REV2(z1, z2))
   LAST(x0, cons(z0, z1)) -> c7(IF(false, x0, cons(z0, z1)))
   IF(false, x0, cons(z0, z1)) -> c9(LAST(z0, z1))
   IF(false, x0, cons(z0, z1)) -> c10(LAST(z0, z1))
S tuples:
   REV(cons(z0, z1)) -> c6(REV2(z0, z1))
   REV2(z0, cons(z1, z2)) -> c12(REV(cons(z0, rev2(z1, z2))), REV2(z1, z2))
K tuples:
   IF(false, x0, cons(z0, z1)) -> c9(LAST(head(cons(z0, z1)), z1))
   IF(false, x0, cons(z0, z1)) -> c10(LAST(head(cons(z0, z1)), z1))
   IF(false, x0, cons(z0, z1)) -> c9(LAST(z0, z1))
   IF(false, x0, cons(z0, z1)) -> c10(LAST(z0, z1))
   LAST(x0, cons(z0, z1)) -> c7(IF(false, x0, cons(z0, z1)))
Defined Rule Symbols:   rev2_2, rev_1

Defined Pair Symbols:   REV_1, REV2_2, LAST_2, IF_3

Compound Symbols:   c6_1, c12_2, c7_1, c9_1, c10_1


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

(83) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID))
Use forward instantiation to replace REV(cons(z0, z1)) -> c6(REV2(z0, z1)) by 
   REV(cons(z0, cons(y1, y2))) -> c6(REV2(z0, cons(y1, y2)))

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

(84)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   rev2(z0, nil) -> nil
   rev2(z0, cons(z1, z2)) -> rev(cons(z0, rev2(z1, z2)))
   rev(cons(z0, z1)) -> cons(rev1(z0, z1), rev2(z0, z1))
Tuples:
   REV2(z0, cons(z1, z2)) -> c12(REV(cons(z0, rev2(z1, z2))), REV2(z1, z2))
   LAST(x0, cons(z0, z1)) -> c7(IF(false, x0, cons(z0, z1)))
   IF(false, x0, cons(z0, z1)) -> c9(LAST(z0, z1))
   IF(false, x0, cons(z0, z1)) -> c10(LAST(z0, z1))
   REV(cons(z0, cons(y1, y2))) -> c6(REV2(z0, cons(y1, y2)))
S tuples:
   REV2(z0, cons(z1, z2)) -> c12(REV(cons(z0, rev2(z1, z2))), REV2(z1, z2))
   REV(cons(z0, cons(y1, y2))) -> c6(REV2(z0, cons(y1, y2)))
K tuples:
   IF(false, x0, cons(z0, z1)) -> c9(LAST(head(cons(z0, z1)), z1))
   IF(false, x0, cons(z0, z1)) -> c10(LAST(head(cons(z0, z1)), z1))
   IF(false, x0, cons(z0, z1)) -> c9(LAST(z0, z1))
   IF(false, x0, cons(z0, z1)) -> c10(LAST(z0, z1))
   LAST(x0, cons(z0, z1)) -> c7(IF(false, x0, cons(z0, z1)))
Defined Rule Symbols:   rev2_2, rev_1

Defined Pair Symbols:   REV2_2, LAST_2, IF_3, REV_1

Compound Symbols:   c12_2, c7_1, c9_1, c10_1, c6_1


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

(85) CdtNarrowingProof (BOTH BOUNDS(ID, ID))
Use narrowing to replace REV2(z0, cons(z1, z2)) -> c12(REV(cons(z0, rev2(z1, z2))), REV2(z1, z2)) by 
   REV2(x0, cons(z0, nil)) -> c12(REV(cons(x0, nil)), REV2(z0, nil))
   REV2(x0, cons(z0, cons(z1, z2))) -> c12(REV(cons(x0, rev(cons(z0, rev2(z1, z2))))), REV2(z0, cons(z1, z2)))

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

(86)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   rev2(z0, nil) -> nil
   rev2(z0, cons(z1, z2)) -> rev(cons(z0, rev2(z1, z2)))
   rev(cons(z0, z1)) -> cons(rev1(z0, z1), rev2(z0, z1))
Tuples:
   LAST(x0, cons(z0, z1)) -> c7(IF(false, x0, cons(z0, z1)))
   IF(false, x0, cons(z0, z1)) -> c9(LAST(z0, z1))
   IF(false, x0, cons(z0, z1)) -> c10(LAST(z0, z1))
   REV(cons(z0, cons(y1, y2))) -> c6(REV2(z0, cons(y1, y2)))
   REV2(x0, cons(z0, nil)) -> c12(REV(cons(x0, nil)), REV2(z0, nil))
   REV2(x0, cons(z0, cons(z1, z2))) -> c12(REV(cons(x0, rev(cons(z0, rev2(z1, z2))))), REV2(z0, cons(z1, z2)))
S tuples:
   REV(cons(z0, cons(y1, y2))) -> c6(REV2(z0, cons(y1, y2)))
   REV2(x0, cons(z0, nil)) -> c12(REV(cons(x0, nil)), REV2(z0, nil))
   REV2(x0, cons(z0, cons(z1, z2))) -> c12(REV(cons(x0, rev(cons(z0, rev2(z1, z2))))), REV2(z0, cons(z1, z2)))
K tuples:
   IF(false, x0, cons(z0, z1)) -> c9(LAST(head(cons(z0, z1)), z1))
   IF(false, x0, cons(z0, z1)) -> c10(LAST(head(cons(z0, z1)), z1))
   IF(false, x0, cons(z0, z1)) -> c9(LAST(z0, z1))
   IF(false, x0, cons(z0, z1)) -> c10(LAST(z0, z1))
   LAST(x0, cons(z0, z1)) -> c7(IF(false, x0, cons(z0, z1)))
Defined Rule Symbols:   rev2_2, rev_1

Defined Pair Symbols:   LAST_2, IF_3, REV_1, REV2_2

Compound Symbols:   c7_1, c9_1, c10_1, c6_1, c12_2


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

(87) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID))
Removed 1 trailing nodes:
   REV2(x0, cons(z0, nil)) -> c12(REV(cons(x0, nil)), REV2(z0, nil))

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

(88)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   rev2(z0, nil) -> nil
   rev2(z0, cons(z1, z2)) -> rev(cons(z0, rev2(z1, z2)))
   rev(cons(z0, z1)) -> cons(rev1(z0, z1), rev2(z0, z1))
Tuples:
   LAST(x0, cons(z0, z1)) -> c7(IF(false, x0, cons(z0, z1)))
   IF(false, x0, cons(z0, z1)) -> c9(LAST(z0, z1))
   IF(false, x0, cons(z0, z1)) -> c10(LAST(z0, z1))
   REV(cons(z0, cons(y1, y2))) -> c6(REV2(z0, cons(y1, y2)))
   REV2(x0, cons(z0, cons(z1, z2))) -> c12(REV(cons(x0, rev(cons(z0, rev2(z1, z2))))), REV2(z0, cons(z1, z2)))
S tuples:
   REV(cons(z0, cons(y1, y2))) -> c6(REV2(z0, cons(y1, y2)))
   REV2(x0, cons(z0, cons(z1, z2))) -> c12(REV(cons(x0, rev(cons(z0, rev2(z1, z2))))), REV2(z0, cons(z1, z2)))
K tuples:
   IF(false, x0, cons(z0, z1)) -> c9(LAST(z0, z1))
   IF(false, x0, cons(z0, z1)) -> c10(LAST(z0, z1))
   LAST(x0, cons(z0, z1)) -> c7(IF(false, x0, cons(z0, z1)))
Defined Rule Symbols:   rev2_2, rev_1

Defined Pair Symbols:   LAST_2, IF_3, REV_1, REV2_2

Compound Symbols:   c7_1, c9_1, c10_1, c6_1, c12_2


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

(89) CdtNarrowingProof (BOTH BOUNDS(ID, ID))
Use narrowing to replace REV2(x0, cons(z0, cons(z1, z2))) -> c12(REV(cons(x0, rev(cons(z0, rev2(z1, z2))))), REV2(z0, cons(z1, z2))) by 
   REV2(x0, cons(z0, cons(x2, x3))) -> c12(REV(cons(x0, cons(rev1(z0, rev2(x2, x3)), rev2(z0, rev2(x2, x3))))), REV2(z0, cons(x2, x3)))
   REV2(x0, cons(x1, cons(z0, nil))) -> c12(REV(cons(x0, rev(cons(x1, nil)))), REV2(x1, cons(z0, nil)))
   REV2(x0, cons(x1, cons(z0, cons(z1, z2)))) -> c12(REV(cons(x0, rev(cons(x1, rev(cons(z0, rev2(z1, z2))))))), REV2(x1, cons(z0, cons(z1, z2))))

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

(90)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   rev2(z0, nil) -> nil
   rev2(z0, cons(z1, z2)) -> rev(cons(z0, rev2(z1, z2)))
   rev(cons(z0, z1)) -> cons(rev1(z0, z1), rev2(z0, z1))
Tuples:
   LAST(x0, cons(z0, z1)) -> c7(IF(false, x0, cons(z0, z1)))
   IF(false, x0, cons(z0, z1)) -> c9(LAST(z0, z1))
   IF(false, x0, cons(z0, z1)) -> c10(LAST(z0, z1))
   REV(cons(z0, cons(y1, y2))) -> c6(REV2(z0, cons(y1, y2)))
   REV2(x0, cons(z0, cons(x2, x3))) -> c12(REV(cons(x0, cons(rev1(z0, rev2(x2, x3)), rev2(z0, rev2(x2, x3))))), REV2(z0, cons(x2, x3)))
   REV2(x0, cons(x1, cons(z0, nil))) -> c12(REV(cons(x0, rev(cons(x1, nil)))), REV2(x1, cons(z0, nil)))
   REV2(x0, cons(x1, cons(z0, cons(z1, z2)))) -> c12(REV(cons(x0, rev(cons(x1, rev(cons(z0, rev2(z1, z2))))))), REV2(x1, cons(z0, cons(z1, z2))))
S tuples:
   REV(cons(z0, cons(y1, y2))) -> c6(REV2(z0, cons(y1, y2)))
   REV2(x0, cons(z0, cons(x2, x3))) -> c12(REV(cons(x0, cons(rev1(z0, rev2(x2, x3)), rev2(z0, rev2(x2, x3))))), REV2(z0, cons(x2, x3)))
   REV2(x0, cons(x1, cons(z0, nil))) -> c12(REV(cons(x0, rev(cons(x1, nil)))), REV2(x1, cons(z0, nil)))
   REV2(x0, cons(x1, cons(z0, cons(z1, z2)))) -> c12(REV(cons(x0, rev(cons(x1, rev(cons(z0, rev2(z1, z2))))))), REV2(x1, cons(z0, cons(z1, z2))))
K tuples:
   IF(false, x0, cons(z0, z1)) -> c9(LAST(z0, z1))
   IF(false, x0, cons(z0, z1)) -> c10(LAST(z0, z1))
   LAST(x0, cons(z0, z1)) -> c7(IF(false, x0, cons(z0, z1)))
Defined Rule Symbols:   rev2_2, rev_1

Defined Pair Symbols:   LAST_2, IF_3, REV_1, REV2_2

Compound Symbols:   c7_1, c9_1, c10_1, c6_1, c12_2


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

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

(92)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   rev2(z0, nil) -> nil
   rev2(z0, cons(z1, z2)) -> rev(cons(z0, rev2(z1, z2)))
   rev(cons(z0, z1)) -> cons(rev1(z0, z1), rev2(z0, z1))
Tuples:
   LAST(x0, cons(z0, z1)) -> c7(IF(false, x0, cons(z0, z1)))
   IF(false, x0, cons(z0, z1)) -> c9(LAST(z0, z1))
   IF(false, x0, cons(z0, z1)) -> c10(LAST(z0, z1))
   REV(cons(z0, cons(y1, y2))) -> c6(REV2(z0, cons(y1, y2)))
   REV2(x0, cons(z0, cons(x2, x3))) -> c12(REV(cons(x0, cons(rev1(z0, rev2(x2, x3)), rev2(z0, rev2(x2, x3))))), REV2(z0, cons(x2, x3)))
   REV2(x0, cons(x1, cons(z0, cons(z1, z2)))) -> c12(REV(cons(x0, rev(cons(x1, rev(cons(z0, rev2(z1, z2))))))), REV2(x1, cons(z0, cons(z1, z2))))
   REV2(x0, cons(x1, cons(z0, nil))) -> c12(REV(cons(x0, rev(cons(x1, nil)))))
S tuples:
   REV(cons(z0, cons(y1, y2))) -> c6(REV2(z0, cons(y1, y2)))
   REV2(x0, cons(z0, cons(x2, x3))) -> c12(REV(cons(x0, cons(rev1(z0, rev2(x2, x3)), rev2(z0, rev2(x2, x3))))), REV2(z0, cons(x2, x3)))
   REV2(x0, cons(x1, cons(z0, cons(z1, z2)))) -> c12(REV(cons(x0, rev(cons(x1, rev(cons(z0, rev2(z1, z2))))))), REV2(x1, cons(z0, cons(z1, z2))))
   REV2(x0, cons(x1, cons(z0, nil))) -> c12(REV(cons(x0, rev(cons(x1, nil)))))
K tuples:
   IF(false, x0, cons(z0, z1)) -> c9(LAST(z0, z1))
   IF(false, x0, cons(z0, z1)) -> c10(LAST(z0, z1))
   LAST(x0, cons(z0, z1)) -> c7(IF(false, x0, cons(z0, z1)))
Defined Rule Symbols:   rev2_2, rev_1

Defined Pair Symbols:   LAST_2, IF_3, REV_1, REV2_2

Compound Symbols:   c7_1, c9_1, c10_1, c6_1, c12_2, c12_1


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

(93) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID))
Use forward instantiation to replace IF(false, x0, cons(z0, z1)) -> c9(LAST(z0, z1)) by 
   IF(false, z0, cons(z1, cons(y1, y2))) -> c9(LAST(z1, cons(y1, y2)))

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

(94)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   rev2(z0, nil) -> nil
   rev2(z0, cons(z1, z2)) -> rev(cons(z0, rev2(z1, z2)))
   rev(cons(z0, z1)) -> cons(rev1(z0, z1), rev2(z0, z1))
Tuples:
   LAST(x0, cons(z0, z1)) -> c7(IF(false, x0, cons(z0, z1)))
   IF(false, x0, cons(z0, z1)) -> c10(LAST(z0, z1))
   REV(cons(z0, cons(y1, y2))) -> c6(REV2(z0, cons(y1, y2)))
   REV2(x0, cons(z0, cons(x2, x3))) -> c12(REV(cons(x0, cons(rev1(z0, rev2(x2, x3)), rev2(z0, rev2(x2, x3))))), REV2(z0, cons(x2, x3)))
   REV2(x0, cons(x1, cons(z0, cons(z1, z2)))) -> c12(REV(cons(x0, rev(cons(x1, rev(cons(z0, rev2(z1, z2))))))), REV2(x1, cons(z0, cons(z1, z2))))
   REV2(x0, cons(x1, cons(z0, nil))) -> c12(REV(cons(x0, rev(cons(x1, nil)))))
   IF(false, z0, cons(z1, cons(y1, y2))) -> c9(LAST(z1, cons(y1, y2)))
S tuples:
   REV(cons(z0, cons(y1, y2))) -> c6(REV2(z0, cons(y1, y2)))
   REV2(x0, cons(z0, cons(x2, x3))) -> c12(REV(cons(x0, cons(rev1(z0, rev2(x2, x3)), rev2(z0, rev2(x2, x3))))), REV2(z0, cons(x2, x3)))
   REV2(x0, cons(x1, cons(z0, cons(z1, z2)))) -> c12(REV(cons(x0, rev(cons(x1, rev(cons(z0, rev2(z1, z2))))))), REV2(x1, cons(z0, cons(z1, z2))))
   REV2(x0, cons(x1, cons(z0, nil))) -> c12(REV(cons(x0, rev(cons(x1, nil)))))
K tuples:
   IF(false, x0, cons(z0, z1)) -> c10(LAST(z0, z1))
   LAST(x0, cons(z0, z1)) -> c7(IF(false, x0, cons(z0, z1)))
   IF(false, z0, cons(z1, cons(y1, y2))) -> c9(LAST(z1, cons(y1, y2)))
Defined Rule Symbols:   rev2_2, rev_1

Defined Pair Symbols:   LAST_2, IF_3, REV_1, REV2_2

Compound Symbols:   c7_1, c10_1, c6_1, c12_2, c12_1, c9_1


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

(95) CdtRewritingProof (BOTH BOUNDS(ID, ID))
Used rewriting to replace REV2(x0, cons(x1, cons(z0, cons(z1, z2)))) -> c12(REV(cons(x0, rev(cons(x1, rev(cons(z0, rev2(z1, z2))))))), REV2(x1, cons(z0, cons(z1, z2)))) by REV2(z0, cons(z1, cons(z2, cons(z3, z4)))) -> c12(REV(cons(z0, cons(rev1(z1, rev(cons(z2, rev2(z3, z4)))), rev2(z1, rev(cons(z2, rev2(z3, z4))))))), REV2(z1, cons(z2, cons(z3, z4))))
----------------------------------------

(96)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   rev2(z0, nil) -> nil
   rev2(z0, cons(z1, z2)) -> rev(cons(z0, rev2(z1, z2)))
   rev(cons(z0, z1)) -> cons(rev1(z0, z1), rev2(z0, z1))
Tuples:
   LAST(x0, cons(z0, z1)) -> c7(IF(false, x0, cons(z0, z1)))
   IF(false, x0, cons(z0, z1)) -> c10(LAST(z0, z1))
   REV(cons(z0, cons(y1, y2))) -> c6(REV2(z0, cons(y1, y2)))
   REV2(x0, cons(z0, cons(x2, x3))) -> c12(REV(cons(x0, cons(rev1(z0, rev2(x2, x3)), rev2(z0, rev2(x2, x3))))), REV2(z0, cons(x2, x3)))
   REV2(x0, cons(x1, cons(z0, nil))) -> c12(REV(cons(x0, rev(cons(x1, nil)))))
   IF(false, z0, cons(z1, cons(y1, y2))) -> c9(LAST(z1, cons(y1, y2)))
   REV2(z0, cons(z1, cons(z2, cons(z3, z4)))) -> c12(REV(cons(z0, cons(rev1(z1, rev(cons(z2, rev2(z3, z4)))), rev2(z1, rev(cons(z2, rev2(z3, z4))))))), REV2(z1, cons(z2, cons(z3, z4))))
S tuples:
   REV(cons(z0, cons(y1, y2))) -> c6(REV2(z0, cons(y1, y2)))
   REV2(x0, cons(z0, cons(x2, x3))) -> c12(REV(cons(x0, cons(rev1(z0, rev2(x2, x3)), rev2(z0, rev2(x2, x3))))), REV2(z0, cons(x2, x3)))
   REV2(x0, cons(x1, cons(z0, nil))) -> c12(REV(cons(x0, rev(cons(x1, nil)))))
   REV2(z0, cons(z1, cons(z2, cons(z3, z4)))) -> c12(REV(cons(z0, cons(rev1(z1, rev(cons(z2, rev2(z3, z4)))), rev2(z1, rev(cons(z2, rev2(z3, z4))))))), REV2(z1, cons(z2, cons(z3, z4))))
K tuples:
   IF(false, x0, cons(z0, z1)) -> c10(LAST(z0, z1))
   LAST(x0, cons(z0, z1)) -> c7(IF(false, x0, cons(z0, z1)))
   IF(false, z0, cons(z1, cons(y1, y2))) -> c9(LAST(z1, cons(y1, y2)))
Defined Rule Symbols:   rev2_2, rev_1

Defined Pair Symbols:   LAST_2, IF_3, REV_1, REV2_2

Compound Symbols:   c7_1, c10_1, c6_1, c12_2, c12_1, c9_1


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

(97) CdtRewritingProof (BOTH BOUNDS(ID, ID))
Used rewriting to replace REV2(x0, cons(x1, cons(z0, nil))) -> c12(REV(cons(x0, rev(cons(x1, nil))))) by REV2(z0, cons(z1, cons(z2, nil))) -> c12(REV(cons(z0, cons(rev1(z1, nil), rev2(z1, nil)))))
----------------------------------------

(98)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   rev2(z0, nil) -> nil
   rev2(z0, cons(z1, z2)) -> rev(cons(z0, rev2(z1, z2)))
   rev(cons(z0, z1)) -> cons(rev1(z0, z1), rev2(z0, z1))
Tuples:
   LAST(x0, cons(z0, z1)) -> c7(IF(false, x0, cons(z0, z1)))
   IF(false, x0, cons(z0, z1)) -> c10(LAST(z0, z1))
   REV(cons(z0, cons(y1, y2))) -> c6(REV2(z0, cons(y1, y2)))
   REV2(x0, cons(z0, cons(x2, x3))) -> c12(REV(cons(x0, cons(rev1(z0, rev2(x2, x3)), rev2(z0, rev2(x2, x3))))), REV2(z0, cons(x2, x3)))
   IF(false, z0, cons(z1, cons(y1, y2))) -> c9(LAST(z1, cons(y1, y2)))
   REV2(z0, cons(z1, cons(z2, cons(z3, z4)))) -> c12(REV(cons(z0, cons(rev1(z1, rev(cons(z2, rev2(z3, z4)))), rev2(z1, rev(cons(z2, rev2(z3, z4))))))), REV2(z1, cons(z2, cons(z3, z4))))
   REV2(z0, cons(z1, cons(z2, nil))) -> c12(REV(cons(z0, cons(rev1(z1, nil), rev2(z1, nil)))))
S tuples:
   REV(cons(z0, cons(y1, y2))) -> c6(REV2(z0, cons(y1, y2)))
   REV2(x0, cons(z0, cons(x2, x3))) -> c12(REV(cons(x0, cons(rev1(z0, rev2(x2, x3)), rev2(z0, rev2(x2, x3))))), REV2(z0, cons(x2, x3)))
   REV2(z0, cons(z1, cons(z2, cons(z3, z4)))) -> c12(REV(cons(z0, cons(rev1(z1, rev(cons(z2, rev2(z3, z4)))), rev2(z1, rev(cons(z2, rev2(z3, z4))))))), REV2(z1, cons(z2, cons(z3, z4))))
   REV2(z0, cons(z1, cons(z2, nil))) -> c12(REV(cons(z0, cons(rev1(z1, nil), rev2(z1, nil)))))
K tuples:
   IF(false, x0, cons(z0, z1)) -> c10(LAST(z0, z1))
   LAST(x0, cons(z0, z1)) -> c7(IF(false, x0, cons(z0, z1)))
   IF(false, z0, cons(z1, cons(y1, y2))) -> c9(LAST(z1, cons(y1, y2)))
Defined Rule Symbols:   rev2_2, rev_1

Defined Pair Symbols:   LAST_2, IF_3, REV_1, REV2_2

Compound Symbols:   c7_1, c10_1, c6_1, c12_2, c9_1, c12_1


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

(99) CdtRewritingProof (BOTH BOUNDS(ID, ID))
Used rewriting to replace REV2(z0, cons(z1, cons(z2, cons(z3, z4)))) -> c12(REV(cons(z0, cons(rev1(z1, rev(cons(z2, rev2(z3, z4)))), rev2(z1, rev(cons(z2, rev2(z3, z4))))))), REV2(z1, cons(z2, cons(z3, z4)))) by REV2(z0, cons(z1, cons(z2, cons(z3, z4)))) -> c12(REV(cons(z0, cons(rev1(z1, rev(cons(z2, rev2(z3, z4)))), rev2(z1, cons(rev1(z2, rev2(z3, z4)), rev2(z2, rev2(z3, z4))))))), REV2(z1, cons(z2, cons(z3, z4))))
----------------------------------------

(100)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   rev2(z0, nil) -> nil
   rev2(z0, cons(z1, z2)) -> rev(cons(z0, rev2(z1, z2)))
   rev(cons(z0, z1)) -> cons(rev1(z0, z1), rev2(z0, z1))
Tuples:
   LAST(x0, cons(z0, z1)) -> c7(IF(false, x0, cons(z0, z1)))
   IF(false, x0, cons(z0, z1)) -> c10(LAST(z0, z1))
   REV(cons(z0, cons(y1, y2))) -> c6(REV2(z0, cons(y1, y2)))
   REV2(x0, cons(z0, cons(x2, x3))) -> c12(REV(cons(x0, cons(rev1(z0, rev2(x2, x3)), rev2(z0, rev2(x2, x3))))), REV2(z0, cons(x2, x3)))
   IF(false, z0, cons(z1, cons(y1, y2))) -> c9(LAST(z1, cons(y1, y2)))
   REV2(z0, cons(z1, cons(z2, nil))) -> c12(REV(cons(z0, cons(rev1(z1, nil), rev2(z1, nil)))))
   REV2(z0, cons(z1, cons(z2, cons(z3, z4)))) -> c12(REV(cons(z0, cons(rev1(z1, rev(cons(z2, rev2(z3, z4)))), rev2(z1, cons(rev1(z2, rev2(z3, z4)), rev2(z2, rev2(z3, z4))))))), REV2(z1, cons(z2, cons(z3, z4))))
S tuples:
   REV(cons(z0, cons(y1, y2))) -> c6(REV2(z0, cons(y1, y2)))
   REV2(x0, cons(z0, cons(x2, x3))) -> c12(REV(cons(x0, cons(rev1(z0, rev2(x2, x3)), rev2(z0, rev2(x2, x3))))), REV2(z0, cons(x2, x3)))
   REV2(z0, cons(z1, cons(z2, nil))) -> c12(REV(cons(z0, cons(rev1(z1, nil), rev2(z1, nil)))))
   REV2(z0, cons(z1, cons(z2, cons(z3, z4)))) -> c12(REV(cons(z0, cons(rev1(z1, rev(cons(z2, rev2(z3, z4)))), rev2(z1, cons(rev1(z2, rev2(z3, z4)), rev2(z2, rev2(z3, z4))))))), REV2(z1, cons(z2, cons(z3, z4))))
K tuples:
   IF(false, x0, cons(z0, z1)) -> c10(LAST(z0, z1))
   LAST(x0, cons(z0, z1)) -> c7(IF(false, x0, cons(z0, z1)))
   IF(false, z0, cons(z1, cons(y1, y2))) -> c9(LAST(z1, cons(y1, y2)))
Defined Rule Symbols:   rev2_2, rev_1

Defined Pair Symbols:   LAST_2, IF_3, REV_1, REV2_2

Compound Symbols:   c7_1, c10_1, c6_1, c12_2, c9_1, c12_1


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

(101) CdtRewritingProof (BOTH BOUNDS(ID, ID))
Used rewriting to replace REV2(z0, cons(z1, cons(z2, nil))) -> c12(REV(cons(z0, cons(rev1(z1, nil), rev2(z1, nil))))) by REV2(z0, cons(z1, cons(z2, nil))) -> c12(REV(cons(z0, cons(rev1(z1, nil), nil))))
----------------------------------------

(102)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   rev2(z0, nil) -> nil
   rev2(z0, cons(z1, z2)) -> rev(cons(z0, rev2(z1, z2)))
   rev(cons(z0, z1)) -> cons(rev1(z0, z1), rev2(z0, z1))
Tuples:
   LAST(x0, cons(z0, z1)) -> c7(IF(false, x0, cons(z0, z1)))
   IF(false, x0, cons(z0, z1)) -> c10(LAST(z0, z1))
   REV(cons(z0, cons(y1, y2))) -> c6(REV2(z0, cons(y1, y2)))
   REV2(x0, cons(z0, cons(x2, x3))) -> c12(REV(cons(x0, cons(rev1(z0, rev2(x2, x3)), rev2(z0, rev2(x2, x3))))), REV2(z0, cons(x2, x3)))
   IF(false, z0, cons(z1, cons(y1, y2))) -> c9(LAST(z1, cons(y1, y2)))
   REV2(z0, cons(z1, cons(z2, cons(z3, z4)))) -> c12(REV(cons(z0, cons(rev1(z1, rev(cons(z2, rev2(z3, z4)))), rev2(z1, cons(rev1(z2, rev2(z3, z4)), rev2(z2, rev2(z3, z4))))))), REV2(z1, cons(z2, cons(z3, z4))))
   REV2(z0, cons(z1, cons(z2, nil))) -> c12(REV(cons(z0, cons(rev1(z1, nil), nil))))
S tuples:
   REV(cons(z0, cons(y1, y2))) -> c6(REV2(z0, cons(y1, y2)))
   REV2(x0, cons(z0, cons(x2, x3))) -> c12(REV(cons(x0, cons(rev1(z0, rev2(x2, x3)), rev2(z0, rev2(x2, x3))))), REV2(z0, cons(x2, x3)))
   REV2(z0, cons(z1, cons(z2, cons(z3, z4)))) -> c12(REV(cons(z0, cons(rev1(z1, rev(cons(z2, rev2(z3, z4)))), rev2(z1, cons(rev1(z2, rev2(z3, z4)), rev2(z2, rev2(z3, z4))))))), REV2(z1, cons(z2, cons(z3, z4))))
   REV2(z0, cons(z1, cons(z2, nil))) -> c12(REV(cons(z0, cons(rev1(z1, nil), nil))))
K tuples:
   IF(false, x0, cons(z0, z1)) -> c10(LAST(z0, z1))
   LAST(x0, cons(z0, z1)) -> c7(IF(false, x0, cons(z0, z1)))
   IF(false, z0, cons(z1, cons(y1, y2))) -> c9(LAST(z1, cons(y1, y2)))
Defined Rule Symbols:   rev2_2, rev_1

Defined Pair Symbols:   LAST_2, IF_3, REV_1, REV2_2

Compound Symbols:   c7_1, c10_1, c6_1, c12_2, c9_1, c12_1


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

(103) CdtInstantiationProof (BOTH BOUNDS(ID, ID))
Use instantiation to replace REV(cons(z0, cons(y1, y2))) -> c6(REV2(z0, cons(y1, y2))) by 
   REV(cons(x0, cons(rev1(x1, y0), y2))) -> c6(REV2(x0, cons(rev1(x1, y0), y2)))
   REV(cons(x0, cons(rev1(x1, nil), nil))) -> c6(REV2(x0, cons(rev1(x1, nil), nil)))

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

(104)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   rev2(z0, nil) -> nil
   rev2(z0, cons(z1, z2)) -> rev(cons(z0, rev2(z1, z2)))
   rev(cons(z0, z1)) -> cons(rev1(z0, z1), rev2(z0, z1))
Tuples:
   LAST(x0, cons(z0, z1)) -> c7(IF(false, x0, cons(z0, z1)))
   IF(false, x0, cons(z0, z1)) -> c10(LAST(z0, z1))
   REV2(x0, cons(z0, cons(x2, x3))) -> c12(REV(cons(x0, cons(rev1(z0, rev2(x2, x3)), rev2(z0, rev2(x2, x3))))), REV2(z0, cons(x2, x3)))
   IF(false, z0, cons(z1, cons(y1, y2))) -> c9(LAST(z1, cons(y1, y2)))
   REV2(z0, cons(z1, cons(z2, cons(z3, z4)))) -> c12(REV(cons(z0, cons(rev1(z1, rev(cons(z2, rev2(z3, z4)))), rev2(z1, cons(rev1(z2, rev2(z3, z4)), rev2(z2, rev2(z3, z4))))))), REV2(z1, cons(z2, cons(z3, z4))))
   REV2(z0, cons(z1, cons(z2, nil))) -> c12(REV(cons(z0, cons(rev1(z1, nil), nil))))
   REV(cons(x0, cons(rev1(x1, y0), y2))) -> c6(REV2(x0, cons(rev1(x1, y0), y2)))
   REV(cons(x0, cons(rev1(x1, nil), nil))) -> c6(REV2(x0, cons(rev1(x1, nil), nil)))
S tuples:
   REV2(x0, cons(z0, cons(x2, x3))) -> c12(REV(cons(x0, cons(rev1(z0, rev2(x2, x3)), rev2(z0, rev2(x2, x3))))), REV2(z0, cons(x2, x3)))
   REV2(z0, cons(z1, cons(z2, cons(z3, z4)))) -> c12(REV(cons(z0, cons(rev1(z1, rev(cons(z2, rev2(z3, z4)))), rev2(z1, cons(rev1(z2, rev2(z3, z4)), rev2(z2, rev2(z3, z4))))))), REV2(z1, cons(z2, cons(z3, z4))))
   REV2(z0, cons(z1, cons(z2, nil))) -> c12(REV(cons(z0, cons(rev1(z1, nil), nil))))
   REV(cons(x0, cons(rev1(x1, y0), y2))) -> c6(REV2(x0, cons(rev1(x1, y0), y2)))
   REV(cons(x0, cons(rev1(x1, nil), nil))) -> c6(REV2(x0, cons(rev1(x1, nil), nil)))
K tuples:
   IF(false, x0, cons(z0, z1)) -> c10(LAST(z0, z1))
   LAST(x0, cons(z0, z1)) -> c7(IF(false, x0, cons(z0, z1)))
   IF(false, z0, cons(z1, cons(y1, y2))) -> c9(LAST(z1, cons(y1, y2)))
Defined Rule Symbols:   rev2_2, rev_1

Defined Pair Symbols:   LAST_2, IF_3, REV2_2, REV_1

Compound Symbols:   c7_1, c10_1, c12_2, c9_1, c12_1, c6_1


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

(105) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID))
Removed 1 trailing nodes:
   REV(cons(x0, cons(rev1(x1, nil), nil))) -> c6(REV2(x0, cons(rev1(x1, nil), nil)))

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

(106)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   rev2(z0, nil) -> nil
   rev2(z0, cons(z1, z2)) -> rev(cons(z0, rev2(z1, z2)))
   rev(cons(z0, z1)) -> cons(rev1(z0, z1), rev2(z0, z1))
Tuples:
   LAST(x0, cons(z0, z1)) -> c7(IF(false, x0, cons(z0, z1)))
   IF(false, x0, cons(z0, z1)) -> c10(LAST(z0, z1))
   REV2(x0, cons(z0, cons(x2, x3))) -> c12(REV(cons(x0, cons(rev1(z0, rev2(x2, x3)), rev2(z0, rev2(x2, x3))))), REV2(z0, cons(x2, x3)))
   IF(false, z0, cons(z1, cons(y1, y2))) -> c9(LAST(z1, cons(y1, y2)))
   REV2(z0, cons(z1, cons(z2, cons(z3, z4)))) -> c12(REV(cons(z0, cons(rev1(z1, rev(cons(z2, rev2(z3, z4)))), rev2(z1, cons(rev1(z2, rev2(z3, z4)), rev2(z2, rev2(z3, z4))))))), REV2(z1, cons(z2, cons(z3, z4))))
   REV2(z0, cons(z1, cons(z2, nil))) -> c12(REV(cons(z0, cons(rev1(z1, nil), nil))))
   REV(cons(x0, cons(rev1(x1, y0), y2))) -> c6(REV2(x0, cons(rev1(x1, y0), y2)))
S tuples:
   REV2(x0, cons(z0, cons(x2, x3))) -> c12(REV(cons(x0, cons(rev1(z0, rev2(x2, x3)), rev2(z0, rev2(x2, x3))))), REV2(z0, cons(x2, x3)))
   REV2(z0, cons(z1, cons(z2, cons(z3, z4)))) -> c12(REV(cons(z0, cons(rev1(z1, rev(cons(z2, rev2(z3, z4)))), rev2(z1, cons(rev1(z2, rev2(z3, z4)), rev2(z2, rev2(z3, z4))))))), REV2(z1, cons(z2, cons(z3, z4))))
   REV2(z0, cons(z1, cons(z2, nil))) -> c12(REV(cons(z0, cons(rev1(z1, nil), nil))))
   REV(cons(x0, cons(rev1(x1, y0), y2))) -> c6(REV2(x0, cons(rev1(x1, y0), y2)))
K tuples:
   IF(false, x0, cons(z0, z1)) -> c10(LAST(z0, z1))
   LAST(x0, cons(z0, z1)) -> c7(IF(false, x0, cons(z0, z1)))
   IF(false, z0, cons(z1, cons(y1, y2))) -> c9(LAST(z1, cons(y1, y2)))
Defined Rule Symbols:   rev2_2, rev_1

Defined Pair Symbols:   LAST_2, IF_3, REV2_2, REV_1

Compound Symbols:   c7_1, c10_1, c12_2, c9_1, c12_1, c6_1


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

(107) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID))
Use forward instantiation to replace IF(false, x0, cons(z0, z1)) -> c10(LAST(z0, z1)) by 
   IF(false, z0, cons(z1, cons(y1, y2))) -> c10(LAST(z1, cons(y1, y2)))

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

(108)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   rev2(z0, nil) -> nil
   rev2(z0, cons(z1, z2)) -> rev(cons(z0, rev2(z1, z2)))
   rev(cons(z0, z1)) -> cons(rev1(z0, z1), rev2(z0, z1))
Tuples:
   LAST(x0, cons(z0, z1)) -> c7(IF(false, x0, cons(z0, z1)))
   REV2(x0, cons(z0, cons(x2, x3))) -> c12(REV(cons(x0, cons(rev1(z0, rev2(x2, x3)), rev2(z0, rev2(x2, x3))))), REV2(z0, cons(x2, x3)))
   IF(false, z0, cons(z1, cons(y1, y2))) -> c9(LAST(z1, cons(y1, y2)))
   REV2(z0, cons(z1, cons(z2, cons(z3, z4)))) -> c12(REV(cons(z0, cons(rev1(z1, rev(cons(z2, rev2(z3, z4)))), rev2(z1, cons(rev1(z2, rev2(z3, z4)), rev2(z2, rev2(z3, z4))))))), REV2(z1, cons(z2, cons(z3, z4))))
   REV2(z0, cons(z1, cons(z2, nil))) -> c12(REV(cons(z0, cons(rev1(z1, nil), nil))))
   REV(cons(x0, cons(rev1(x1, y0), y2))) -> c6(REV2(x0, cons(rev1(x1, y0), y2)))
   IF(false, z0, cons(z1, cons(y1, y2))) -> c10(LAST(z1, cons(y1, y2)))
S tuples:
   REV2(x0, cons(z0, cons(x2, x3))) -> c12(REV(cons(x0, cons(rev1(z0, rev2(x2, x3)), rev2(z0, rev2(x2, x3))))), REV2(z0, cons(x2, x3)))
   REV2(z0, cons(z1, cons(z2, cons(z3, z4)))) -> c12(REV(cons(z0, cons(rev1(z1, rev(cons(z2, rev2(z3, z4)))), rev2(z1, cons(rev1(z2, rev2(z3, z4)), rev2(z2, rev2(z3, z4))))))), REV2(z1, cons(z2, cons(z3, z4))))
   REV2(z0, cons(z1, cons(z2, nil))) -> c12(REV(cons(z0, cons(rev1(z1, nil), nil))))
   REV(cons(x0, cons(rev1(x1, y0), y2))) -> c6(REV2(x0, cons(rev1(x1, y0), y2)))
K tuples:
   LAST(x0, cons(z0, z1)) -> c7(IF(false, x0, cons(z0, z1)))
   IF(false, z0, cons(z1, cons(y1, y2))) -> c9(LAST(z1, cons(y1, y2)))
   IF(false, z0, cons(z1, cons(y1, y2))) -> c10(LAST(z1, cons(y1, y2)))
Defined Rule Symbols:   rev2_2, rev_1

Defined Pair Symbols:   LAST_2, REV2_2, IF_3, REV_1

Compound Symbols:   c7_1, c12_2, c9_1, c12_1, c6_1, c10_1


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

(109) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID))
Use forward instantiation to replace LAST(x0, cons(z0, z1)) -> c7(IF(false, x0, cons(z0, z1))) by 
   LAST(z0, cons(z1, cons(y2, y3))) -> c7(IF(false, z0, cons(z1, cons(y2, y3))))

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

(110)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   rev2(z0, nil) -> nil
   rev2(z0, cons(z1, z2)) -> rev(cons(z0, rev2(z1, z2)))
   rev(cons(z0, z1)) -> cons(rev1(z0, z1), rev2(z0, z1))
Tuples:
   REV2(x0, cons(z0, cons(x2, x3))) -> c12(REV(cons(x0, cons(rev1(z0, rev2(x2, x3)), rev2(z0, rev2(x2, x3))))), REV2(z0, cons(x2, x3)))
   IF(false, z0, cons(z1, cons(y1, y2))) -> c9(LAST(z1, cons(y1, y2)))
   REV2(z0, cons(z1, cons(z2, cons(z3, z4)))) -> c12(REV(cons(z0, cons(rev1(z1, rev(cons(z2, rev2(z3, z4)))), rev2(z1, cons(rev1(z2, rev2(z3, z4)), rev2(z2, rev2(z3, z4))))))), REV2(z1, cons(z2, cons(z3, z4))))
   REV2(z0, cons(z1, cons(z2, nil))) -> c12(REV(cons(z0, cons(rev1(z1, nil), nil))))
   REV(cons(x0, cons(rev1(x1, y0), y2))) -> c6(REV2(x0, cons(rev1(x1, y0), y2)))
   IF(false, z0, cons(z1, cons(y1, y2))) -> c10(LAST(z1, cons(y1, y2)))
   LAST(z0, cons(z1, cons(y2, y3))) -> c7(IF(false, z0, cons(z1, cons(y2, y3))))
S tuples:
   REV2(x0, cons(z0, cons(x2, x3))) -> c12(REV(cons(x0, cons(rev1(z0, rev2(x2, x3)), rev2(z0, rev2(x2, x3))))), REV2(z0, cons(x2, x3)))
   REV2(z0, cons(z1, cons(z2, cons(z3, z4)))) -> c12(REV(cons(z0, cons(rev1(z1, rev(cons(z2, rev2(z3, z4)))), rev2(z1, cons(rev1(z2, rev2(z3, z4)), rev2(z2, rev2(z3, z4))))))), REV2(z1, cons(z2, cons(z3, z4))))
   REV2(z0, cons(z1, cons(z2, nil))) -> c12(REV(cons(z0, cons(rev1(z1, nil), nil))))
   REV(cons(x0, cons(rev1(x1, y0), y2))) -> c6(REV2(x0, cons(rev1(x1, y0), y2)))
K tuples:
   IF(false, z0, cons(z1, cons(y1, y2))) -> c9(LAST(z1, cons(y1, y2)))
   IF(false, z0, cons(z1, cons(y1, y2))) -> c10(LAST(z1, cons(y1, y2)))
   LAST(z0, cons(z1, cons(y2, y3))) -> c7(IF(false, z0, cons(z1, cons(y2, y3))))
Defined Rule Symbols:   rev2_2, rev_1

Defined Pair Symbols:   REV2_2, IF_3, REV_1, LAST_2

Compound Symbols:   c12_2, c9_1, c12_1, c6_1, c10_1, c7_1


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

(111) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID))
Use forward instantiation to replace IF(false, z0, cons(z1, cons(y1, y2))) -> c9(LAST(z1, cons(y1, y2))) by 
   IF(false, z0, cons(z1, cons(z2, cons(y2, y3)))) -> c9(LAST(z1, cons(z2, cons(y2, y3))))

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

(112)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   rev2(z0, nil) -> nil
   rev2(z0, cons(z1, z2)) -> rev(cons(z0, rev2(z1, z2)))
   rev(cons(z0, z1)) -> cons(rev1(z0, z1), rev2(z0, z1))
Tuples:
   REV2(x0, cons(z0, cons(x2, x3))) -> c12(REV(cons(x0, cons(rev1(z0, rev2(x2, x3)), rev2(z0, rev2(x2, x3))))), REV2(z0, cons(x2, x3)))
   REV2(z0, cons(z1, cons(z2, cons(z3, z4)))) -> c12(REV(cons(z0, cons(rev1(z1, rev(cons(z2, rev2(z3, z4)))), rev2(z1, cons(rev1(z2, rev2(z3, z4)), rev2(z2, rev2(z3, z4))))))), REV2(z1, cons(z2, cons(z3, z4))))
   REV2(z0, cons(z1, cons(z2, nil))) -> c12(REV(cons(z0, cons(rev1(z1, nil), nil))))
   REV(cons(x0, cons(rev1(x1, y0), y2))) -> c6(REV2(x0, cons(rev1(x1, y0), y2)))
   IF(false, z0, cons(z1, cons(y1, y2))) -> c10(LAST(z1, cons(y1, y2)))
   LAST(z0, cons(z1, cons(y2, y3))) -> c7(IF(false, z0, cons(z1, cons(y2, y3))))
   IF(false, z0, cons(z1, cons(z2, cons(y2, y3)))) -> c9(LAST(z1, cons(z2, cons(y2, y3))))
S tuples:
   REV2(x0, cons(z0, cons(x2, x3))) -> c12(REV(cons(x0, cons(rev1(z0, rev2(x2, x3)), rev2(z0, rev2(x2, x3))))), REV2(z0, cons(x2, x3)))
   REV2(z0, cons(z1, cons(z2, cons(z3, z4)))) -> c12(REV(cons(z0, cons(rev1(z1, rev(cons(z2, rev2(z3, z4)))), rev2(z1, cons(rev1(z2, rev2(z3, z4)), rev2(z2, rev2(z3, z4))))))), REV2(z1, cons(z2, cons(z3, z4))))
   REV2(z0, cons(z1, cons(z2, nil))) -> c12(REV(cons(z0, cons(rev1(z1, nil), nil))))
   REV(cons(x0, cons(rev1(x1, y0), y2))) -> c6(REV2(x0, cons(rev1(x1, y0), y2)))
K tuples:
   IF(false, z0, cons(z1, cons(y1, y2))) -> c10(LAST(z1, cons(y1, y2)))
   LAST(z0, cons(z1, cons(y2, y3))) -> c7(IF(false, z0, cons(z1, cons(y2, y3))))
   IF(false, z0, cons(z1, cons(z2, cons(y2, y3)))) -> c9(LAST(z1, cons(z2, cons(y2, y3))))
Defined Rule Symbols:   rev2_2, rev_1

Defined Pair Symbols:   REV2_2, REV_1, IF_3, LAST_2

Compound Symbols:   c12_2, c12_1, c6_1, c10_1, c7_1, c9_1


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

(113) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID))
Use forward instantiation to replace REV(cons(x0, cons(rev1(x1, y0), y2))) -> c6(REV2(x0, cons(rev1(x1, y0), y2))) by 
   REV(cons(z0, cons(rev1(z1, z2), cons(y2, y3)))) -> c6(REV2(z0, cons(rev1(z1, z2), cons(y2, y3))))
   REV(cons(z0, cons(rev1(z1, z2), cons(y2, cons(y3, y4))))) -> c6(REV2(z0, cons(rev1(z1, z2), cons(y2, cons(y3, y4)))))
   REV(cons(z0, cons(rev1(z1, z2), cons(y2, nil)))) -> c6(REV2(z0, cons(rev1(z1, z2), cons(y2, nil))))

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

(114)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   rev2(z0, nil) -> nil
   rev2(z0, cons(z1, z2)) -> rev(cons(z0, rev2(z1, z2)))
   rev(cons(z0, z1)) -> cons(rev1(z0, z1), rev2(z0, z1))
Tuples:
   REV2(x0, cons(z0, cons(x2, x3))) -> c12(REV(cons(x0, cons(rev1(z0, rev2(x2, x3)), rev2(z0, rev2(x2, x3))))), REV2(z0, cons(x2, x3)))
   REV2(z0, cons(z1, cons(z2, cons(z3, z4)))) -> c12(REV(cons(z0, cons(rev1(z1, rev(cons(z2, rev2(z3, z4)))), rev2(z1, cons(rev1(z2, rev2(z3, z4)), rev2(z2, rev2(z3, z4))))))), REV2(z1, cons(z2, cons(z3, z4))))
   REV2(z0, cons(z1, cons(z2, nil))) -> c12(REV(cons(z0, cons(rev1(z1, nil), nil))))
   IF(false, z0, cons(z1, cons(y1, y2))) -> c10(LAST(z1, cons(y1, y2)))
   LAST(z0, cons(z1, cons(y2, y3))) -> c7(IF(false, z0, cons(z1, cons(y2, y3))))
   IF(false, z0, cons(z1, cons(z2, cons(y2, y3)))) -> c9(LAST(z1, cons(z2, cons(y2, y3))))
   REV(cons(z0, cons(rev1(z1, z2), cons(y2, y3)))) -> c6(REV2(z0, cons(rev1(z1, z2), cons(y2, y3))))
   REV(cons(z0, cons(rev1(z1, z2), cons(y2, cons(y3, y4))))) -> c6(REV2(z0, cons(rev1(z1, z2), cons(y2, cons(y3, y4)))))
   REV(cons(z0, cons(rev1(z1, z2), cons(y2, nil)))) -> c6(REV2(z0, cons(rev1(z1, z2), cons(y2, nil))))
S tuples:
   REV2(x0, cons(z0, cons(x2, x3))) -> c12(REV(cons(x0, cons(rev1(z0, rev2(x2, x3)), rev2(z0, rev2(x2, x3))))), REV2(z0, cons(x2, x3)))
   REV2(z0, cons(z1, cons(z2, cons(z3, z4)))) -> c12(REV(cons(z0, cons(rev1(z1, rev(cons(z2, rev2(z3, z4)))), rev2(z1, cons(rev1(z2, rev2(z3, z4)), rev2(z2, rev2(z3, z4))))))), REV2(z1, cons(z2, cons(z3, z4))))
   REV2(z0, cons(z1, cons(z2, nil))) -> c12(REV(cons(z0, cons(rev1(z1, nil), nil))))
   REV(cons(z0, cons(rev1(z1, z2), cons(y2, y3)))) -> c6(REV2(z0, cons(rev1(z1, z2), cons(y2, y3))))
   REV(cons(z0, cons(rev1(z1, z2), cons(y2, cons(y3, y4))))) -> c6(REV2(z0, cons(rev1(z1, z2), cons(y2, cons(y3, y4)))))
   REV(cons(z0, cons(rev1(z1, z2), cons(y2, nil)))) -> c6(REV2(z0, cons(rev1(z1, z2), cons(y2, nil))))
K tuples:
   IF(false, z0, cons(z1, cons(y1, y2))) -> c10(LAST(z1, cons(y1, y2)))
   LAST(z0, cons(z1, cons(y2, y3))) -> c7(IF(false, z0, cons(z1, cons(y2, y3))))
   IF(false, z0, cons(z1, cons(z2, cons(y2, y3)))) -> c9(LAST(z1, cons(z2, cons(y2, y3))))
Defined Rule Symbols:   rev2_2, rev_1

Defined Pair Symbols:   REV2_2, IF_3, LAST_2, REV_1

Compound Symbols:   c12_2, c12_1, c10_1, c7_1, c9_1, c6_1


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

(115) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID))
Removed 1 trailing nodes:
   REV2(z0, cons(z1, cons(z2, nil))) -> c12(REV(cons(z0, cons(rev1(z1, nil), nil))))

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

(116)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   rev2(z0, nil) -> nil
   rev2(z0, cons(z1, z2)) -> rev(cons(z0, rev2(z1, z2)))
   rev(cons(z0, z1)) -> cons(rev1(z0, z1), rev2(z0, z1))
Tuples:
   REV2(x0, cons(z0, cons(x2, x3))) -> c12(REV(cons(x0, cons(rev1(z0, rev2(x2, x3)), rev2(z0, rev2(x2, x3))))), REV2(z0, cons(x2, x3)))
   REV2(z0, cons(z1, cons(z2, cons(z3, z4)))) -> c12(REV(cons(z0, cons(rev1(z1, rev(cons(z2, rev2(z3, z4)))), rev2(z1, cons(rev1(z2, rev2(z3, z4)), rev2(z2, rev2(z3, z4))))))), REV2(z1, cons(z2, cons(z3, z4))))
   IF(false, z0, cons(z1, cons(y1, y2))) -> c10(LAST(z1, cons(y1, y2)))
   LAST(z0, cons(z1, cons(y2, y3))) -> c7(IF(false, z0, cons(z1, cons(y2, y3))))
   IF(false, z0, cons(z1, cons(z2, cons(y2, y3)))) -> c9(LAST(z1, cons(z2, cons(y2, y3))))
   REV(cons(z0, cons(rev1(z1, z2), cons(y2, y3)))) -> c6(REV2(z0, cons(rev1(z1, z2), cons(y2, y3))))
   REV(cons(z0, cons(rev1(z1, z2), cons(y2, cons(y3, y4))))) -> c6(REV2(z0, cons(rev1(z1, z2), cons(y2, cons(y3, y4)))))
   REV(cons(z0, cons(rev1(z1, z2), cons(y2, nil)))) -> c6(REV2(z0, cons(rev1(z1, z2), cons(y2, nil))))
S tuples:
   REV2(x0, cons(z0, cons(x2, x3))) -> c12(REV(cons(x0, cons(rev1(z0, rev2(x2, x3)), rev2(z0, rev2(x2, x3))))), REV2(z0, cons(x2, x3)))
   REV2(z0, cons(z1, cons(z2, cons(z3, z4)))) -> c12(REV(cons(z0, cons(rev1(z1, rev(cons(z2, rev2(z3, z4)))), rev2(z1, cons(rev1(z2, rev2(z3, z4)), rev2(z2, rev2(z3, z4))))))), REV2(z1, cons(z2, cons(z3, z4))))
   REV(cons(z0, cons(rev1(z1, z2), cons(y2, y3)))) -> c6(REV2(z0, cons(rev1(z1, z2), cons(y2, y3))))
   REV(cons(z0, cons(rev1(z1, z2), cons(y2, cons(y3, y4))))) -> c6(REV2(z0, cons(rev1(z1, z2), cons(y2, cons(y3, y4)))))
   REV(cons(z0, cons(rev1(z1, z2), cons(y2, nil)))) -> c6(REV2(z0, cons(rev1(z1, z2), cons(y2, nil))))
K tuples:
   IF(false, z0, cons(z1, cons(y1, y2))) -> c10(LAST(z1, cons(y1, y2)))
   LAST(z0, cons(z1, cons(y2, y3))) -> c7(IF(false, z0, cons(z1, cons(y2, y3))))
   IF(false, z0, cons(z1, cons(z2, cons(y2, y3)))) -> c9(LAST(z1, cons(z2, cons(y2, y3))))
Defined Rule Symbols:   rev2_2, rev_1

Defined Pair Symbols:   REV2_2, IF_3, LAST_2, REV_1

Compound Symbols:   c12_2, c10_1, c7_1, c9_1, c6_1


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

(117) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID))
Use forward instantiation to replace IF(false, z0, cons(z1, cons(y1, y2))) -> c10(LAST(z1, cons(y1, y2))) by 
   IF(false, z0, cons(z1, cons(z2, cons(y2, y3)))) -> c10(LAST(z1, cons(z2, cons(y2, y3))))

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

(118)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   rev2(z0, nil) -> nil
   rev2(z0, cons(z1, z2)) -> rev(cons(z0, rev2(z1, z2)))
   rev(cons(z0, z1)) -> cons(rev1(z0, z1), rev2(z0, z1))
Tuples:
   REV2(x0, cons(z0, cons(x2, x3))) -> c12(REV(cons(x0, cons(rev1(z0, rev2(x2, x3)), rev2(z0, rev2(x2, x3))))), REV2(z0, cons(x2, x3)))
   REV2(z0, cons(z1, cons(z2, cons(z3, z4)))) -> c12(REV(cons(z0, cons(rev1(z1, rev(cons(z2, rev2(z3, z4)))), rev2(z1, cons(rev1(z2, rev2(z3, z4)), rev2(z2, rev2(z3, z4))))))), REV2(z1, cons(z2, cons(z3, z4))))
   LAST(z0, cons(z1, cons(y2, y3))) -> c7(IF(false, z0, cons(z1, cons(y2, y3))))
   IF(false, z0, cons(z1, cons(z2, cons(y2, y3)))) -> c9(LAST(z1, cons(z2, cons(y2, y3))))
   REV(cons(z0, cons(rev1(z1, z2), cons(y2, y3)))) -> c6(REV2(z0, cons(rev1(z1, z2), cons(y2, y3))))
   REV(cons(z0, cons(rev1(z1, z2), cons(y2, cons(y3, y4))))) -> c6(REV2(z0, cons(rev1(z1, z2), cons(y2, cons(y3, y4)))))
   REV(cons(z0, cons(rev1(z1, z2), cons(y2, nil)))) -> c6(REV2(z0, cons(rev1(z1, z2), cons(y2, nil))))
   IF(false, z0, cons(z1, cons(z2, cons(y2, y3)))) -> c10(LAST(z1, cons(z2, cons(y2, y3))))
S tuples:
   REV2(x0, cons(z0, cons(x2, x3))) -> c12(REV(cons(x0, cons(rev1(z0, rev2(x2, x3)), rev2(z0, rev2(x2, x3))))), REV2(z0, cons(x2, x3)))
   REV2(z0, cons(z1, cons(z2, cons(z3, z4)))) -> c12(REV(cons(z0, cons(rev1(z1, rev(cons(z2, rev2(z3, z4)))), rev2(z1, cons(rev1(z2, rev2(z3, z4)), rev2(z2, rev2(z3, z4))))))), REV2(z1, cons(z2, cons(z3, z4))))
   REV(cons(z0, cons(rev1(z1, z2), cons(y2, y3)))) -> c6(REV2(z0, cons(rev1(z1, z2), cons(y2, y3))))
   REV(cons(z0, cons(rev1(z1, z2), cons(y2, cons(y3, y4))))) -> c6(REV2(z0, cons(rev1(z1, z2), cons(y2, cons(y3, y4)))))
   REV(cons(z0, cons(rev1(z1, z2), cons(y2, nil)))) -> c6(REV2(z0, cons(rev1(z1, z2), cons(y2, nil))))
K tuples:
   LAST(z0, cons(z1, cons(y2, y3))) -> c7(IF(false, z0, cons(z1, cons(y2, y3))))
   IF(false, z0, cons(z1, cons(z2, cons(y2, y3)))) -> c9(LAST(z1, cons(z2, cons(y2, y3))))
   IF(false, z0, cons(z1, cons(z2, cons(y2, y3)))) -> c10(LAST(z1, cons(z2, cons(y2, y3))))
Defined Rule Symbols:   rev2_2, rev_1

Defined Pair Symbols:   REV2_2, LAST_2, IF_3, REV_1

Compound Symbols:   c12_2, c7_1, c9_1, c6_1, c10_1


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

(119) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID))
Use forward instantiation to replace LAST(z0, cons(z1, cons(y2, y3))) -> c7(IF(false, z0, cons(z1, cons(y2, y3)))) by 
   LAST(z0, cons(z1, cons(z2, cons(y3, y4)))) -> c7(IF(false, z0, cons(z1, cons(z2, cons(y3, y4)))))

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

(120)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   rev2(z0, nil) -> nil
   rev2(z0, cons(z1, z2)) -> rev(cons(z0, rev2(z1, z2)))
   rev(cons(z0, z1)) -> cons(rev1(z0, z1), rev2(z0, z1))
Tuples:
   REV2(x0, cons(z0, cons(x2, x3))) -> c12(REV(cons(x0, cons(rev1(z0, rev2(x2, x3)), rev2(z0, rev2(x2, x3))))), REV2(z0, cons(x2, x3)))
   REV2(z0, cons(z1, cons(z2, cons(z3, z4)))) -> c12(REV(cons(z0, cons(rev1(z1, rev(cons(z2, rev2(z3, z4)))), rev2(z1, cons(rev1(z2, rev2(z3, z4)), rev2(z2, rev2(z3, z4))))))), REV2(z1, cons(z2, cons(z3, z4))))
   IF(false, z0, cons(z1, cons(z2, cons(y2, y3)))) -> c9(LAST(z1, cons(z2, cons(y2, y3))))
   REV(cons(z0, cons(rev1(z1, z2), cons(y2, y3)))) -> c6(REV2(z0, cons(rev1(z1, z2), cons(y2, y3))))
   REV(cons(z0, cons(rev1(z1, z2), cons(y2, cons(y3, y4))))) -> c6(REV2(z0, cons(rev1(z1, z2), cons(y2, cons(y3, y4)))))
   REV(cons(z0, cons(rev1(z1, z2), cons(y2, nil)))) -> c6(REV2(z0, cons(rev1(z1, z2), cons(y2, nil))))
   IF(false, z0, cons(z1, cons(z2, cons(y2, y3)))) -> c10(LAST(z1, cons(z2, cons(y2, y3))))
   LAST(z0, cons(z1, cons(z2, cons(y3, y4)))) -> c7(IF(false, z0, cons(z1, cons(z2, cons(y3, y4)))))
S tuples:
   REV2(x0, cons(z0, cons(x2, x3))) -> c12(REV(cons(x0, cons(rev1(z0, rev2(x2, x3)), rev2(z0, rev2(x2, x3))))), REV2(z0, cons(x2, x3)))
   REV2(z0, cons(z1, cons(z2, cons(z3, z4)))) -> c12(REV(cons(z0, cons(rev1(z1, rev(cons(z2, rev2(z3, z4)))), rev2(z1, cons(rev1(z2, rev2(z3, z4)), rev2(z2, rev2(z3, z4))))))), REV2(z1, cons(z2, cons(z3, z4))))
   REV(cons(z0, cons(rev1(z1, z2), cons(y2, y3)))) -> c6(REV2(z0, cons(rev1(z1, z2), cons(y2, y3))))
   REV(cons(z0, cons(rev1(z1, z2), cons(y2, cons(y3, y4))))) -> c6(REV2(z0, cons(rev1(z1, z2), cons(y2, cons(y3, y4)))))
   REV(cons(z0, cons(rev1(z1, z2), cons(y2, nil)))) -> c6(REV2(z0, cons(rev1(z1, z2), cons(y2, nil))))
K tuples:
   IF(false, z0, cons(z1, cons(z2, cons(y2, y3)))) -> c9(LAST(z1, cons(z2, cons(y2, y3))))
   IF(false, z0, cons(z1, cons(z2, cons(y2, y3)))) -> c10(LAST(z1, cons(z2, cons(y2, y3))))
   LAST(z0, cons(z1, cons(z2, cons(y3, y4)))) -> c7(IF(false, z0, cons(z1, cons(z2, cons(y3, y4)))))
Defined Rule Symbols:   rev2_2, rev_1

Defined Pair Symbols:   REV2_2, IF_3, REV_1, LAST_2

Compound Symbols:   c12_2, c9_1, c6_1, c10_1, c7_1


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

(121) RelTrsToWeightedTrsProof (UPPER BOUND(ID))
Transformed relative TRS to weighted TRS
----------------------------------------

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

   empty(nil) -> true [1]
   empty(cons(x, l)) -> false [1]
   head(cons(x, l)) -> x [1]
   tail(nil) -> nil [1]
   tail(cons(x, l)) -> l [1]
   rev(nil) -> nil [1]
   rev(cons(x, l)) -> cons(rev1(x, l), rev2(x, l)) [1]
   last(x, l) -> if(empty(l), x, l) [1]
   if(true, x, l) -> x [1]
   if(false, x, l) -> last(head(l), tail(l)) [1]
   rev2(x, nil) -> nil [1]
   rev2(x, cons(y, l)) -> rev(cons(x, rev2(y, l))) [1]

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

(123) TypeInferenceProof (BOTH BOUNDS(ID, ID))
Infered types.
----------------------------------------

(124)
Obligation:
Runtime Complexity Weighted TRS with Types.
The TRS R consists of the following rules:

   empty(nil) -> true [1]
   empty(cons(x, l)) -> false [1]
   head(cons(x, l)) -> x [1]
   tail(nil) -> nil [1]
   tail(cons(x, l)) -> l [1]
   rev(nil) -> nil [1]
   rev(cons(x, l)) -> cons(rev1(x, l), rev2(x, l)) [1]
   last(x, l) -> if(empty(l), x, l) [1]
   if(true, x, l) -> x [1]
   if(false, x, l) -> last(head(l), tail(l)) [1]
   rev2(x, nil) -> nil [1]
   rev2(x, cons(y, l)) -> rev(cons(x, rev2(y, l))) [1]

The TRS has the following type information:
empty :: nil:cons -> true:false
nil :: nil:cons
true :: true:false
cons :: rev1 -> nil:cons -> nil:cons
false :: true:false
head :: nil:cons -> rev1
tail :: nil:cons -> nil:cons
rev :: nil:cons -> nil:cons
rev1 :: rev1 -> nil:cons -> rev1
rev2 :: rev1 -> nil:cons -> nil:cons
last :: rev1 -> nil:cons -> rev1
if :: true:false -> rev1 -> nil:cons -> rev1

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

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

   last_2
   if_3

(c) The following functions are completely defined:

   rev2_2
   head_1
   tail_1
   empty_1
   rev_1

Due to the following rules being added:

   head(v0) -> const [0]

And the following fresh constants:    const

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

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

   empty(nil) -> true [1]
   empty(cons(x, l)) -> false [1]
   head(cons(x, l)) -> x [1]
   tail(nil) -> nil [1]
   tail(cons(x, l)) -> l [1]
   rev(nil) -> nil [1]
   rev(cons(x, l)) -> cons(rev1(x, l), rev2(x, l)) [1]
   last(x, l) -> if(empty(l), x, l) [1]
   if(true, x, l) -> x [1]
   if(false, x, l) -> last(head(l), tail(l)) [1]
   rev2(x, nil) -> nil [1]
   rev2(x, cons(y, l)) -> rev(cons(x, rev2(y, l))) [1]
   head(v0) -> const [0]

The TRS has the following type information:
empty :: nil:cons -> true:false
nil :: nil:cons
true :: true:false
cons :: rev1:const -> nil:cons -> nil:cons
false :: true:false
head :: nil:cons -> rev1:const
tail :: nil:cons -> nil:cons
rev :: nil:cons -> nil:cons
rev1 :: rev1:const -> nil:cons -> rev1:const
rev2 :: rev1:const -> nil:cons -> nil:cons
last :: rev1:const -> nil:cons -> rev1:const
if :: true:false -> rev1:const -> nil:cons -> rev1:const
const :: rev1:const

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

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

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

   empty(nil) -> true [1]
   empty(cons(x, l)) -> false [1]
   head(cons(x, l)) -> x [1]
   tail(nil) -> nil [1]
   tail(cons(x, l)) -> l [1]
   rev(nil) -> nil [1]
   rev(cons(x, l)) -> cons(rev1(x, l), rev2(x, l)) [1]
   last(x, nil) -> if(true, x, nil) [2]
   last(x, cons(x', l')) -> if(false, x, cons(x', l')) [2]
   if(true, x, l) -> x [1]
   if(false, x, cons(x'', l'')) -> last(x'', l'') [3]
   if(false, x, nil) -> last(const, nil) [2]
   if(false, x, cons(x1, l1)) -> last(const, l1) [2]
   rev2(x, nil) -> nil [1]
   rev2(x, cons(y, nil)) -> rev(cons(x, nil)) [2]
   rev2(x, cons(y, cons(y', l2))) -> rev(cons(x, rev(cons(y, rev2(y', l2))))) [2]
   head(v0) -> const [0]

The TRS has the following type information:
empty :: nil:cons -> true:false
nil :: nil:cons
true :: true:false
cons :: rev1:const -> nil:cons -> nil:cons
false :: true:false
head :: nil:cons -> rev1:const
tail :: nil:cons -> nil:cons
rev :: nil:cons -> nil:cons
rev1 :: rev1:const -> nil:cons -> rev1:const
rev2 :: rev1:const -> nil:cons -> nil:cons
last :: rev1:const -> nil:cons -> rev1:const
if :: true:false -> rev1:const -> nil:cons -> rev1:const
const :: rev1:const

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

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

   nil => 0
   true => 1
   false => 0
   const => 0

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

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

   empty(z) -{ 1 }-> 1 :|: z = 0
   empty(z) -{ 1 }-> 0 :|: x >= 0, l >= 0, z = 1 + x + l
   head(z) -{ 1 }-> x :|: x >= 0, l >= 0, z = 1 + x + l
   head(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0
   if(z, z', z'') -{ 1 }-> x :|: z' = x, z = 1, x >= 0, l >= 0, z'' = l
   if(z, z', z'') -{ 3 }-> last(x'', l'') :|: z' = x, l'' >= 0, z'' = 1 + x'' + l'', x >= 0, x'' >= 0, z = 0
   if(z, z', z'') -{ 2 }-> last(0, l1) :|: x1 >= 0, z' = x, x >= 0, l1 >= 0, z = 0, z'' = 1 + x1 + l1
   if(z, z', z'') -{ 2 }-> last(0, 0) :|: z'' = 0, z' = x, x >= 0, z = 0
   last(z, z') -{ 2 }-> if(1, x, 0) :|: x >= 0, z = x, z' = 0
   last(z, z') -{ 2 }-> if(0, x, 1 + x' + l') :|: x >= 0, x' >= 0, l' >= 0, z' = 1 + x' + l', z = x
   rev(z) -{ 1 }-> 0 :|: z = 0
   rev(z) -{ 1 }-> 1 + (1 + x + l) + rev2(x, l) :|: x >= 0, l >= 0, z = 1 + x + l
   rev2(z, z') -{ 2 }-> rev(1 + x + rev(1 + y + rev2(y', l2))) :|: x >= 0, y >= 0, y' >= 0, z = x, l2 >= 0, z' = 1 + y + (1 + y' + l2)
   rev2(z, z') -{ 2 }-> rev(1 + x + 0) :|: x >= 0, y >= 0, z' = 1 + y + 0, z = x
   rev2(z, z') -{ 1 }-> 0 :|: x >= 0, z = x, z' = 0
   tail(z) -{ 1 }-> l :|: x >= 0, l >= 0, z = 1 + x + l
   tail(z) -{ 1 }-> 0 :|: z = 0


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

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

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

   empty(z) -{ 1 }-> 1 :|: z = 0
   empty(z) -{ 1 }-> 0 :|: x >= 0, l >= 0, z = 1 + x + l
   head(z) -{ 1 }-> x :|: x >= 0, l >= 0, z = 1 + x + l
   head(z) -{ 0 }-> 0 :|: z >= 0
   if(z, z', z'') -{ 1 }-> z' :|: z = 1, z' >= 0, z'' >= 0
   if(z, z', z'') -{ 3 }-> last(x'', l'') :|: l'' >= 0, z'' = 1 + x'' + l'', z' >= 0, x'' >= 0, z = 0
   if(z, z', z'') -{ 2 }-> last(0, l1) :|: x1 >= 0, z' >= 0, l1 >= 0, z = 0, z'' = 1 + x1 + l1
   if(z, z', z'') -{ 2 }-> last(0, 0) :|: z'' = 0, z' >= 0, z = 0
   last(z, z') -{ 2 }-> if(1, z, 0) :|: z >= 0, z' = 0
   last(z, z') -{ 2 }-> if(0, z, 1 + x' + l') :|: z >= 0, x' >= 0, l' >= 0, z' = 1 + x' + l'
   rev(z) -{ 1 }-> 0 :|: z = 0
   rev(z) -{ 1 }-> 1 + (1 + x + l) + rev2(x, l) :|: x >= 0, l >= 0, z = 1 + x + l
   rev2(z, z') -{ 2 }-> rev(1 + z + rev(1 + y + rev2(y', l2))) :|: z >= 0, y >= 0, y' >= 0, l2 >= 0, z' = 1 + y + (1 + y' + l2)
   rev2(z, z') -{ 2 }-> rev(1 + z + 0) :|: z >= 0, z' - 1 >= 0
   rev2(z, z') -{ 1 }-> 0 :|: z >= 0, z' = 0
   tail(z) -{ 1 }-> l :|: x >= 0, l >= 0, z = 1 + x + l
   tail(z) -{ 1 }-> 0 :|: z = 0


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

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

   head(v0) -> null_head [0]

And the following fresh constants:    null_head

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

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

   empty(nil) -> true [1]
   empty(cons(x, l)) -> false [1]
   head(cons(x, l)) -> x [1]
   tail(nil) -> nil [1]
   tail(cons(x, l)) -> l [1]
   rev(nil) -> nil [1]
   rev(cons(x, l)) -> cons(rev1(x, l), rev2(x, l)) [1]
   last(x, l) -> if(empty(l), x, l) [1]
   if(true, x, l) -> x [1]
   if(false, x, l) -> last(head(l), tail(l)) [1]
   rev2(x, nil) -> nil [1]
   rev2(x, cons(y, l)) -> rev(cons(x, rev2(y, l))) [1]
   head(v0) -> null_head [0]

The TRS has the following type information:
empty :: nil:cons -> true:false
nil :: nil:cons
true :: true:false
cons :: rev1:null_head -> nil:cons -> nil:cons
false :: true:false
head :: nil:cons -> rev1:null_head
tail :: nil:cons -> nil:cons
rev :: nil:cons -> nil:cons
rev1 :: rev1:null_head -> nil:cons -> rev1:null_head
rev2 :: rev1:null_head -> nil:cons -> nil:cons
last :: rev1:null_head -> nil:cons -> rev1:null_head
if :: true:false -> rev1:null_head -> nil:cons -> rev1:null_head
null_head :: rev1:null_head

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

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

   nil => 0
   true => 1
   false => 0
   null_head => 0

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

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

   empty(z) -{ 1 }-> 1 :|: z = 0
   empty(z) -{ 1 }-> 0 :|: x >= 0, l >= 0, z = 1 + x + l
   head(z) -{ 1 }-> x :|: x >= 0, l >= 0, z = 1 + x + l
   head(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0
   if(z, z', z'') -{ 1 }-> x :|: z' = x, z = 1, x >= 0, l >= 0, z'' = l
   if(z, z', z'') -{ 1 }-> last(head(l), tail(l)) :|: z' = x, x >= 0, l >= 0, z = 0, z'' = l
   last(z, z') -{ 1 }-> if(empty(l), x, l) :|: z' = l, x >= 0, l >= 0, z = x
   rev(z) -{ 1 }-> 0 :|: z = 0
   rev(z) -{ 1 }-> 1 + (1 + x + l) + rev2(x, l) :|: x >= 0, l >= 0, z = 1 + x + l
   rev2(z, z') -{ 1 }-> rev(1 + x + rev2(y, l)) :|: x >= 0, y >= 0, z' = 1 + y + l, l >= 0, z = x
   rev2(z, z') -{ 1 }-> 0 :|: x >= 0, z = x, z' = 0
   tail(z) -{ 1 }-> l :|: x >= 0, l >= 0, z = 1 + x + l
   tail(z) -{ 1 }-> 0 :|: z = 0

Only complete derivations are relevant for the runtime complexity.