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


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

(0) CpxRelTRS
(1) SInnermostTerminationProof [BOTH CONCRETE BOUNDS(ID, ID), 375 ms]
(2) CpxRelTRS
(3) CpxTrsToCdtProof [UPPER BOUND(ID), 0 ms]
(4) CdtProblem
    (5) CdtLeafRemovalProof [ComplexityIfPolyImplication, 0 ms]
    (6) CdtProblem
    (7) CdtRhsSimplificationProcessorProof [BOTH BOUNDS(ID, ID), 0 ms]
    (8) CdtProblem
    (9) CdtUsableRulesProof [BOTH BOUNDS(ID, ID), 0 ms]
    (10) CdtProblem
    (11) CdtRuleRemovalProof [UPPER BOUND(ADD(n^1)), 69 ms]
    (12) CdtProblem
    (13) CdtRuleRemovalProof [UPPER BOUND(ADD(n^1)), 34 ms]
    (14) CdtProblem
    (15) CdtRuleRemovalProof [UPPER BOUND(ADD(n^1)), 26 ms]
    (16) CdtProblem
    (17) CdtRuleRemovalProof [UPPER BOUND(ADD(n^1)), 25 ms]
    (18) CdtProblem
    (19) CdtRuleRemovalProof [UPPER BOUND(ADD(n^1)), 22 ms]
    (20) CdtProblem
    (21) CdtRuleRemovalProof [UPPER BOUND(ADD(n^2)), 241 ms]
    (22) CdtProblem
    (23) SIsEmptyProof [BOTH BOUNDS(ID, ID), 0 ms]
    (24) BOUNDS(1, 1)
(25) RenamingProof [BOTH BOUNDS(ID, ID), 0 ms]
(26) CpxRelTRS
    (27) SlicingProof [LOWER BOUND(ID), 0 ms]
    (28) CpxRelTRS
    (29) TypeInferenceProof [BOTH BOUNDS(ID, ID), 0 ms]
    (30) typed CpxTrs
    (31) OrderProof [LOWER BOUND(ID), 0 ms]
    (32) typed CpxTrs
    (33) RewriteLemmaProof [LOWER BOUND(ID), 95.6 s]
    (34) BEST
        (35) proven lower bound
            (36) LowerBoundPropagationProof [FINISHED, 0 ms]
            (37) BOUNDS(n^1, INF)
        (38) typed CpxTrs


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

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


The TRS R consists of the following rules:

   prefix(Cons(x', xs'), Cons(x, xs)) -> and(!EQ(x', x), prefix(xs', xs))
   domatch(Cons(x, xs), Nil, n) -> Nil
   domatch(Nil, Nil, n) -> Cons(n, Nil)
   prefix(Cons(x, xs), Nil) -> False
   prefix(Nil, cs) -> True
   domatch(patcs, Cons(x, xs), n) -> domatch[Ite](prefix(patcs, Cons(x, xs)), patcs, Cons(x, xs), n)
   eqNatList(Cons(x, xs), Cons(y, ys)) -> eqNatList[Ite](!EQ(x, y), y, ys, x, xs)
   eqNatList(Cons(x, xs), Nil) -> False
   eqNatList(Nil, Cons(y, ys)) -> False
   eqNatList(Nil, Nil) -> True
   notEmpty(Cons(x, xs)) -> True
   notEmpty(Nil) -> False
   strmatch(patstr, str) -> domatch(patstr, str, Nil)

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

   and(False, False) -> False
   and(True, False) -> False
   and(False, True) -> False
   and(True, True) -> True
   !EQ(S(x), S(y)) -> !EQ(x, y)
   !EQ(0, S(y)) -> False
   !EQ(S(x), 0) -> False
   !EQ(0, 0) -> True
   domatch[Ite](False, patcs, Cons(x, xs), n) -> domatch(patcs, xs, Cons(n, Cons(Nil, Nil)))
   domatch[Ite](True, patcs, Cons(x, xs), n) -> Cons(n, domatch(patcs, xs, Cons(n, Cons(Nil, Nil))))
   eqNatList[Ite](False, y, ys, x, xs) -> False
   eqNatList[Ite](True, y, ys, x, xs) -> eqNatList(xs, ys)

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

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

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


The TRS R consists of the following rules:

   prefix(Cons(x', xs'), Cons(x, xs)) -> and(!EQ(x', x), prefix(xs', xs))
   domatch(Cons(x, xs), Nil, n) -> Nil
   domatch(Nil, Nil, n) -> Cons(n, Nil)
   prefix(Cons(x, xs), Nil) -> False
   prefix(Nil, cs) -> True
   domatch(patcs, Cons(x, xs), n) -> domatch[Ite](prefix(patcs, Cons(x, xs)), patcs, Cons(x, xs), n)
   eqNatList(Cons(x, xs), Cons(y, ys)) -> eqNatList[Ite](!EQ(x, y), y, ys, x, xs)
   eqNatList(Cons(x, xs), Nil) -> False
   eqNatList(Nil, Cons(y, ys)) -> False
   eqNatList(Nil, Nil) -> True
   notEmpty(Cons(x, xs)) -> True
   notEmpty(Nil) -> False
   strmatch(patstr, str) -> domatch(patstr, str, Nil)

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

   and(False, False) -> False
   and(True, False) -> False
   and(False, True) -> False
   and(True, True) -> True
   !EQ(S(x), S(y)) -> !EQ(x, y)
   !EQ(0, S(y)) -> False
   !EQ(S(x), 0) -> False
   !EQ(0, 0) -> True
   domatch[Ite](False, patcs, Cons(x, xs), n) -> domatch(patcs, xs, Cons(n, Cons(Nil, Nil)))
   domatch[Ite](True, patcs, Cons(x, xs), n) -> Cons(n, domatch(patcs, xs, Cons(n, Cons(Nil, Nil))))
   eqNatList[Ite](False, y, ys, x, xs) -> False
   eqNatList[Ite](True, y, ys, x, xs) -> eqNatList(xs, ys)

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

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

(4)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   and(False, False) -> False
   and(True, False) -> False
   and(False, True) -> False
   and(True, True) -> True
   !EQ(S(z0), S(z1)) -> !EQ(z0, z1)
   !EQ(0, S(z0)) -> False
   !EQ(S(z0), 0) -> False
   !EQ(0, 0) -> True
   domatch[Ite](False, z0, Cons(z1, z2), z3) -> domatch(z0, z2, Cons(z3, Cons(Nil, Nil)))
   domatch[Ite](True, z0, Cons(z1, z2), z3) -> Cons(z3, domatch(z0, z2, Cons(z3, Cons(Nil, Nil))))
   eqNatList[Ite](False, z0, z1, z2, z3) -> False
   eqNatList[Ite](True, z0, z1, z2, z3) -> eqNatList(z3, z1)
   prefix(Cons(z0, z1), Cons(z2, z3)) -> and(!EQ(z0, z2), prefix(z1, z3))
   prefix(Cons(z0, z1), Nil) -> False
   prefix(Nil, z0) -> True
   domatch(Cons(z0, z1), Nil, z2) -> Nil
   domatch(Nil, Nil, z0) -> Cons(z0, Nil)
   domatch(z0, Cons(z1, z2), z3) -> domatch[Ite](prefix(z0, Cons(z1, z2)), z0, Cons(z1, z2), z3)
   eqNatList(Cons(z0, z1), Cons(z2, z3)) -> eqNatList[Ite](!EQ(z0, z2), z2, z3, z0, z1)
   eqNatList(Cons(z0, z1), Nil) -> False
   eqNatList(Nil, Cons(z0, z1)) -> False
   eqNatList(Nil, Nil) -> True
   notEmpty(Cons(z0, z1)) -> True
   notEmpty(Nil) -> False
   strmatch(z0, z1) -> domatch(z0, z1, Nil)
Tuples:
   AND(False, False) -> c
   AND(True, False) -> c1
   AND(False, True) -> c2
   AND(True, True) -> c3
   !EQ'(S(z0), S(z1)) -> c4(!EQ'(z0, z1))
   !EQ'(0, S(z0)) -> c5
   !EQ'(S(z0), 0) -> c6
   !EQ'(0, 0) -> c7
   DOMATCH[ITE](False, z0, Cons(z1, z2), z3) -> c8(DOMATCH(z0, z2, Cons(z3, Cons(Nil, Nil))))
   DOMATCH[ITE](True, z0, Cons(z1, z2), z3) -> c9(DOMATCH(z0, z2, Cons(z3, Cons(Nil, Nil))))
   EQNATLIST[ITE](False, z0, z1, z2, z3) -> c10
   EQNATLIST[ITE](True, z0, z1, z2, z3) -> c11(EQNATLIST(z3, z1))
   PREFIX(Cons(z0, z1), Cons(z2, z3)) -> c12(AND(!EQ(z0, z2), prefix(z1, z3)), !EQ'(z0, z2), PREFIX(z1, z3))
   PREFIX(Cons(z0, z1), Nil) -> c13
   PREFIX(Nil, z0) -> c14
   DOMATCH(Cons(z0, z1), Nil, z2) -> c15
   DOMATCH(Nil, Nil, z0) -> c16
   DOMATCH(z0, Cons(z1, z2), z3) -> c17(DOMATCH[ITE](prefix(z0, Cons(z1, z2)), z0, Cons(z1, z2), z3), PREFIX(z0, Cons(z1, z2)))
   EQNATLIST(Cons(z0, z1), Cons(z2, z3)) -> c18(EQNATLIST[ITE](!EQ(z0, z2), z2, z3, z0, z1), !EQ'(z0, z2))
   EQNATLIST(Cons(z0, z1), Nil) -> c19
   EQNATLIST(Nil, Cons(z0, z1)) -> c20
   EQNATLIST(Nil, Nil) -> c21
   NOTEMPTY(Cons(z0, z1)) -> c22
   NOTEMPTY(Nil) -> c23
   STRMATCH(z0, z1) -> c24(DOMATCH(z0, z1, Nil))
S tuples:
   PREFIX(Cons(z0, z1), Cons(z2, z3)) -> c12(AND(!EQ(z0, z2), prefix(z1, z3)), !EQ'(z0, z2), PREFIX(z1, z3))
   PREFIX(Cons(z0, z1), Nil) -> c13
   PREFIX(Nil, z0) -> c14
   DOMATCH(Cons(z0, z1), Nil, z2) -> c15
   DOMATCH(Nil, Nil, z0) -> c16
   DOMATCH(z0, Cons(z1, z2), z3) -> c17(DOMATCH[ITE](prefix(z0, Cons(z1, z2)), z0, Cons(z1, z2), z3), PREFIX(z0, Cons(z1, z2)))
   EQNATLIST(Cons(z0, z1), Cons(z2, z3)) -> c18(EQNATLIST[ITE](!EQ(z0, z2), z2, z3, z0, z1), !EQ'(z0, z2))
   EQNATLIST(Cons(z0, z1), Nil) -> c19
   EQNATLIST(Nil, Cons(z0, z1)) -> c20
   EQNATLIST(Nil, Nil) -> c21
   NOTEMPTY(Cons(z0, z1)) -> c22
   NOTEMPTY(Nil) -> c23
   STRMATCH(z0, z1) -> c24(DOMATCH(z0, z1, Nil))
K tuples:none
Defined Rule Symbols:   prefix_2, domatch_3, eqNatList_2, notEmpty_1, strmatch_2, and_2, !EQ_2, domatch[Ite]_4, eqNatList[Ite]_5

Defined Pair Symbols:   AND_2, !EQ'_2, DOMATCH[ITE]_4, EQNATLIST[ITE]_5, PREFIX_2, DOMATCH_3, EQNATLIST_2, NOTEMPTY_1, STRMATCH_2

Compound Symbols:   c, c1, c2, c3, c4_1, c5, c6, c7, c8_1, c9_1, c10, c11_1, c12_3, c13, c14, c15, c16, c17_2, c18_2, c19, c20, c21, c22, c23, c24_1


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

(5) CdtLeafRemovalProof (ComplexityIfPolyImplication)
Removed 1 leading nodes:
   STRMATCH(z0, z1) -> c24(DOMATCH(z0, z1, Nil))
Removed 12 trailing nodes:
   !EQ'(0, 0) -> c7
   !EQ'(0, S(z0)) -> c5
   AND(False, True) -> c2
   AND(True, False) -> c1
   PREFIX(Cons(z0, z1), Nil) -> c13
   !EQ'(S(z0), 0) -> c6
   NOTEMPTY(Cons(z0, z1)) -> c22
   AND(True, True) -> c3
   NOTEMPTY(Nil) -> c23
   PREFIX(Nil, z0) -> c14
   EQNATLIST[ITE](False, z0, z1, z2, z3) -> c10
   AND(False, False) -> c

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

(6)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   and(False, False) -> False
   and(True, False) -> False
   and(False, True) -> False
   and(True, True) -> True
   !EQ(S(z0), S(z1)) -> !EQ(z0, z1)
   !EQ(0, S(z0)) -> False
   !EQ(S(z0), 0) -> False
   !EQ(0, 0) -> True
   domatch[Ite](False, z0, Cons(z1, z2), z3) -> domatch(z0, z2, Cons(z3, Cons(Nil, Nil)))
   domatch[Ite](True, z0, Cons(z1, z2), z3) -> Cons(z3, domatch(z0, z2, Cons(z3, Cons(Nil, Nil))))
   eqNatList[Ite](False, z0, z1, z2, z3) -> False
   eqNatList[Ite](True, z0, z1, z2, z3) -> eqNatList(z3, z1)
   prefix(Cons(z0, z1), Cons(z2, z3)) -> and(!EQ(z0, z2), prefix(z1, z3))
   prefix(Cons(z0, z1), Nil) -> False
   prefix(Nil, z0) -> True
   domatch(Cons(z0, z1), Nil, z2) -> Nil
   domatch(Nil, Nil, z0) -> Cons(z0, Nil)
   domatch(z0, Cons(z1, z2), z3) -> domatch[Ite](prefix(z0, Cons(z1, z2)), z0, Cons(z1, z2), z3)
   eqNatList(Cons(z0, z1), Cons(z2, z3)) -> eqNatList[Ite](!EQ(z0, z2), z2, z3, z0, z1)
   eqNatList(Cons(z0, z1), Nil) -> False
   eqNatList(Nil, Cons(z0, z1)) -> False
   eqNatList(Nil, Nil) -> True
   notEmpty(Cons(z0, z1)) -> True
   notEmpty(Nil) -> False
   strmatch(z0, z1) -> domatch(z0, z1, Nil)
Tuples:
   !EQ'(S(z0), S(z1)) -> c4(!EQ'(z0, z1))
   DOMATCH[ITE](False, z0, Cons(z1, z2), z3) -> c8(DOMATCH(z0, z2, Cons(z3, Cons(Nil, Nil))))
   DOMATCH[ITE](True, z0, Cons(z1, z2), z3) -> c9(DOMATCH(z0, z2, Cons(z3, Cons(Nil, Nil))))
   EQNATLIST[ITE](True, z0, z1, z2, z3) -> c11(EQNATLIST(z3, z1))
   PREFIX(Cons(z0, z1), Cons(z2, z3)) -> c12(AND(!EQ(z0, z2), prefix(z1, z3)), !EQ'(z0, z2), PREFIX(z1, z3))
   DOMATCH(Cons(z0, z1), Nil, z2) -> c15
   DOMATCH(Nil, Nil, z0) -> c16
   DOMATCH(z0, Cons(z1, z2), z3) -> c17(DOMATCH[ITE](prefix(z0, Cons(z1, z2)), z0, Cons(z1, z2), z3), PREFIX(z0, Cons(z1, z2)))
   EQNATLIST(Cons(z0, z1), Cons(z2, z3)) -> c18(EQNATLIST[ITE](!EQ(z0, z2), z2, z3, z0, z1), !EQ'(z0, z2))
   EQNATLIST(Cons(z0, z1), Nil) -> c19
   EQNATLIST(Nil, Cons(z0, z1)) -> c20
   EQNATLIST(Nil, Nil) -> c21
S tuples:
   PREFIX(Cons(z0, z1), Cons(z2, z3)) -> c12(AND(!EQ(z0, z2), prefix(z1, z3)), !EQ'(z0, z2), PREFIX(z1, z3))
   DOMATCH(Cons(z0, z1), Nil, z2) -> c15
   DOMATCH(Nil, Nil, z0) -> c16
   DOMATCH(z0, Cons(z1, z2), z3) -> c17(DOMATCH[ITE](prefix(z0, Cons(z1, z2)), z0, Cons(z1, z2), z3), PREFIX(z0, Cons(z1, z2)))
   EQNATLIST(Cons(z0, z1), Cons(z2, z3)) -> c18(EQNATLIST[ITE](!EQ(z0, z2), z2, z3, z0, z1), !EQ'(z0, z2))
   EQNATLIST(Cons(z0, z1), Nil) -> c19
   EQNATLIST(Nil, Cons(z0, z1)) -> c20
   EQNATLIST(Nil, Nil) -> c21
K tuples:none
Defined Rule Symbols:   prefix_2, domatch_3, eqNatList_2, notEmpty_1, strmatch_2, and_2, !EQ_2, domatch[Ite]_4, eqNatList[Ite]_5

Defined Pair Symbols:   !EQ'_2, DOMATCH[ITE]_4, EQNATLIST[ITE]_5, PREFIX_2, DOMATCH_3, EQNATLIST_2

Compound Symbols:   c4_1, c8_1, c9_1, c11_1, c12_3, c15, c16, c17_2, c18_2, c19, c20, c21


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

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

(8)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   and(False, False) -> False
   and(True, False) -> False
   and(False, True) -> False
   and(True, True) -> True
   !EQ(S(z0), S(z1)) -> !EQ(z0, z1)
   !EQ(0, S(z0)) -> False
   !EQ(S(z0), 0) -> False
   !EQ(0, 0) -> True
   domatch[Ite](False, z0, Cons(z1, z2), z3) -> domatch(z0, z2, Cons(z3, Cons(Nil, Nil)))
   domatch[Ite](True, z0, Cons(z1, z2), z3) -> Cons(z3, domatch(z0, z2, Cons(z3, Cons(Nil, Nil))))
   eqNatList[Ite](False, z0, z1, z2, z3) -> False
   eqNatList[Ite](True, z0, z1, z2, z3) -> eqNatList(z3, z1)
   prefix(Cons(z0, z1), Cons(z2, z3)) -> and(!EQ(z0, z2), prefix(z1, z3))
   prefix(Cons(z0, z1), Nil) -> False
   prefix(Nil, z0) -> True
   domatch(Cons(z0, z1), Nil, z2) -> Nil
   domatch(Nil, Nil, z0) -> Cons(z0, Nil)
   domatch(z0, Cons(z1, z2), z3) -> domatch[Ite](prefix(z0, Cons(z1, z2)), z0, Cons(z1, z2), z3)
   eqNatList(Cons(z0, z1), Cons(z2, z3)) -> eqNatList[Ite](!EQ(z0, z2), z2, z3, z0, z1)
   eqNatList(Cons(z0, z1), Nil) -> False
   eqNatList(Nil, Cons(z0, z1)) -> False
   eqNatList(Nil, Nil) -> True
   notEmpty(Cons(z0, z1)) -> True
   notEmpty(Nil) -> False
   strmatch(z0, z1) -> domatch(z0, z1, Nil)
Tuples:
   !EQ'(S(z0), S(z1)) -> c4(!EQ'(z0, z1))
   DOMATCH[ITE](False, z0, Cons(z1, z2), z3) -> c8(DOMATCH(z0, z2, Cons(z3, Cons(Nil, Nil))))
   DOMATCH[ITE](True, z0, Cons(z1, z2), z3) -> c9(DOMATCH(z0, z2, Cons(z3, Cons(Nil, Nil))))
   EQNATLIST[ITE](True, z0, z1, z2, z3) -> c11(EQNATLIST(z3, z1))
   DOMATCH(Cons(z0, z1), Nil, z2) -> c15
   DOMATCH(Nil, Nil, z0) -> c16
   DOMATCH(z0, Cons(z1, z2), z3) -> c17(DOMATCH[ITE](prefix(z0, Cons(z1, z2)), z0, Cons(z1, z2), z3), PREFIX(z0, Cons(z1, z2)))
   EQNATLIST(Cons(z0, z1), Cons(z2, z3)) -> c18(EQNATLIST[ITE](!EQ(z0, z2), z2, z3, z0, z1), !EQ'(z0, z2))
   EQNATLIST(Cons(z0, z1), Nil) -> c19
   EQNATLIST(Nil, Cons(z0, z1)) -> c20
   EQNATLIST(Nil, Nil) -> c21
   PREFIX(Cons(z0, z1), Cons(z2, z3)) -> c12(!EQ'(z0, z2), PREFIX(z1, z3))
S tuples:
   DOMATCH(Cons(z0, z1), Nil, z2) -> c15
   DOMATCH(Nil, Nil, z0) -> c16
   DOMATCH(z0, Cons(z1, z2), z3) -> c17(DOMATCH[ITE](prefix(z0, Cons(z1, z2)), z0, Cons(z1, z2), z3), PREFIX(z0, Cons(z1, z2)))
   EQNATLIST(Cons(z0, z1), Cons(z2, z3)) -> c18(EQNATLIST[ITE](!EQ(z0, z2), z2, z3, z0, z1), !EQ'(z0, z2))
   EQNATLIST(Cons(z0, z1), Nil) -> c19
   EQNATLIST(Nil, Cons(z0, z1)) -> c20
   EQNATLIST(Nil, Nil) -> c21
   PREFIX(Cons(z0, z1), Cons(z2, z3)) -> c12(!EQ'(z0, z2), PREFIX(z1, z3))
K tuples:none
Defined Rule Symbols:   prefix_2, domatch_3, eqNatList_2, notEmpty_1, strmatch_2, and_2, !EQ_2, domatch[Ite]_4, eqNatList[Ite]_5

Defined Pair Symbols:   !EQ'_2, DOMATCH[ITE]_4, EQNATLIST[ITE]_5, DOMATCH_3, EQNATLIST_2, PREFIX_2

Compound Symbols:   c4_1, c8_1, c9_1, c11_1, c15, c16, c17_2, c18_2, c19, c20, c21, c12_2


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

(9) CdtUsableRulesProof (BOTH BOUNDS(ID, ID))
The following rules are not usable and were removed:
   domatch[Ite](False, z0, Cons(z1, z2), z3) -> domatch(z0, z2, Cons(z3, Cons(Nil, Nil)))
   domatch[Ite](True, z0, Cons(z1, z2), z3) -> Cons(z3, domatch(z0, z2, Cons(z3, Cons(Nil, Nil))))
   eqNatList[Ite](False, z0, z1, z2, z3) -> False
   eqNatList[Ite](True, z0, z1, z2, z3) -> eqNatList(z3, z1)
   domatch(Cons(z0, z1), Nil, z2) -> Nil
   domatch(Nil, Nil, z0) -> Cons(z0, Nil)
   domatch(z0, Cons(z1, z2), z3) -> domatch[Ite](prefix(z0, Cons(z1, z2)), z0, Cons(z1, z2), z3)
   eqNatList(Cons(z0, z1), Cons(z2, z3)) -> eqNatList[Ite](!EQ(z0, z2), z2, z3, z0, z1)
   eqNatList(Cons(z0, z1), Nil) -> False
   eqNatList(Nil, Cons(z0, z1)) -> False
   eqNatList(Nil, Nil) -> True
   notEmpty(Cons(z0, z1)) -> True
   notEmpty(Nil) -> False
   strmatch(z0, z1) -> domatch(z0, z1, Nil)

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

(10)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   prefix(Cons(z0, z1), Cons(z2, z3)) -> and(!EQ(z0, z2), prefix(z1, z3))
   prefix(Nil, z0) -> True
   prefix(Cons(z0, z1), Nil) -> False
   and(False, False) -> False
   and(True, False) -> False
   and(False, True) -> False
   and(True, True) -> True
   !EQ(S(z0), S(z1)) -> !EQ(z0, z1)
   !EQ(0, S(z0)) -> False
   !EQ(S(z0), 0) -> False
   !EQ(0, 0) -> True
Tuples:
   !EQ'(S(z0), S(z1)) -> c4(!EQ'(z0, z1))
   DOMATCH[ITE](False, z0, Cons(z1, z2), z3) -> c8(DOMATCH(z0, z2, Cons(z3, Cons(Nil, Nil))))
   DOMATCH[ITE](True, z0, Cons(z1, z2), z3) -> c9(DOMATCH(z0, z2, Cons(z3, Cons(Nil, Nil))))
   EQNATLIST[ITE](True, z0, z1, z2, z3) -> c11(EQNATLIST(z3, z1))
   DOMATCH(Cons(z0, z1), Nil, z2) -> c15
   DOMATCH(Nil, Nil, z0) -> c16
   DOMATCH(z0, Cons(z1, z2), z3) -> c17(DOMATCH[ITE](prefix(z0, Cons(z1, z2)), z0, Cons(z1, z2), z3), PREFIX(z0, Cons(z1, z2)))
   EQNATLIST(Cons(z0, z1), Cons(z2, z3)) -> c18(EQNATLIST[ITE](!EQ(z0, z2), z2, z3, z0, z1), !EQ'(z0, z2))
   EQNATLIST(Cons(z0, z1), Nil) -> c19
   EQNATLIST(Nil, Cons(z0, z1)) -> c20
   EQNATLIST(Nil, Nil) -> c21
   PREFIX(Cons(z0, z1), Cons(z2, z3)) -> c12(!EQ'(z0, z2), PREFIX(z1, z3))
S tuples:
   DOMATCH(Cons(z0, z1), Nil, z2) -> c15
   DOMATCH(Nil, Nil, z0) -> c16
   DOMATCH(z0, Cons(z1, z2), z3) -> c17(DOMATCH[ITE](prefix(z0, Cons(z1, z2)), z0, Cons(z1, z2), z3), PREFIX(z0, Cons(z1, z2)))
   EQNATLIST(Cons(z0, z1), Cons(z2, z3)) -> c18(EQNATLIST[ITE](!EQ(z0, z2), z2, z3, z0, z1), !EQ'(z0, z2))
   EQNATLIST(Cons(z0, z1), Nil) -> c19
   EQNATLIST(Nil, Cons(z0, z1)) -> c20
   EQNATLIST(Nil, Nil) -> c21
   PREFIX(Cons(z0, z1), Cons(z2, z3)) -> c12(!EQ'(z0, z2), PREFIX(z1, z3))
K tuples:none
Defined Rule Symbols:   prefix_2, and_2, !EQ_2

Defined Pair Symbols:   !EQ'_2, DOMATCH[ITE]_4, EQNATLIST[ITE]_5, DOMATCH_3, EQNATLIST_2, PREFIX_2

Compound Symbols:   c4_1, c8_1, c9_1, c11_1, c15, c16, c17_2, c18_2, c19, c20, c21, c12_2


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

(11) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)))
Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.
   EQNATLIST(Cons(z0, z1), Nil) -> c19
   EQNATLIST(Nil, Cons(z0, z1)) -> c20
   EQNATLIST(Nil, Nil) -> c21
We considered the (Usable) Rules:none
And the Tuples:
   !EQ'(S(z0), S(z1)) -> c4(!EQ'(z0, z1))
   DOMATCH[ITE](False, z0, Cons(z1, z2), z3) -> c8(DOMATCH(z0, z2, Cons(z3, Cons(Nil, Nil))))
   DOMATCH[ITE](True, z0, Cons(z1, z2), z3) -> c9(DOMATCH(z0, z2, Cons(z3, Cons(Nil, Nil))))
   EQNATLIST[ITE](True, z0, z1, z2, z3) -> c11(EQNATLIST(z3, z1))
   DOMATCH(Cons(z0, z1), Nil, z2) -> c15
   DOMATCH(Nil, Nil, z0) -> c16
   DOMATCH(z0, Cons(z1, z2), z3) -> c17(DOMATCH[ITE](prefix(z0, Cons(z1, z2)), z0, Cons(z1, z2), z3), PREFIX(z0, Cons(z1, z2)))
   EQNATLIST(Cons(z0, z1), Cons(z2, z3)) -> c18(EQNATLIST[ITE](!EQ(z0, z2), z2, z3, z0, z1), !EQ'(z0, z2))
   EQNATLIST(Cons(z0, z1), Nil) -> c19
   EQNATLIST(Nil, Cons(z0, z1)) -> c20
   EQNATLIST(Nil, Nil) -> c21
   PREFIX(Cons(z0, z1), Cons(z2, z3)) -> c12(!EQ'(z0, z2), PREFIX(z1, z3))
The order we found is given by the following interpretation:

Polynomial interpretation :

   POL(!EQ(x_1, x_2)) = [1] + x_2
   POL(!EQ'(x_1, x_2)) = 0
   POL(0) = [1]
   POL(Cons(x_1, x_2)) = 0
   POL(DOMATCH(x_1, x_2, x_3)) = x_1 + x_3
   POL(DOMATCH[ITE](x_1, x_2, x_3, x_4)) = x_2 + x_3 + x_4
   POL(EQNATLIST(x_1, x_2)) = [1]
   POL(EQNATLIST[ITE](x_1, x_2, x_3, x_4, x_5)) = [1]
   POL(False) = [1]
   POL(Nil) = 0
   POL(PREFIX(x_1, x_2)) = 0
   POL(S(x_1)) = [1] + x_1
   POL(True) = [1]
   POL(and(x_1, x_2)) = [1] + x_1
   POL(c11(x_1)) = x_1
   POL(c12(x_1, x_2)) = x_1 + x_2
   POL(c15) = 0
   POL(c16) = 0
   POL(c17(x_1, x_2)) = x_1 + x_2
   POL(c18(x_1, x_2)) = x_1 + x_2
   POL(c19) = 0
   POL(c20) = 0
   POL(c21) = 0
   POL(c4(x_1)) = x_1
   POL(c8(x_1)) = x_1
   POL(c9(x_1)) = x_1
   POL(prefix(x_1, x_2)) = [1] + x_1 + x_2

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

(12)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   prefix(Cons(z0, z1), Cons(z2, z3)) -> and(!EQ(z0, z2), prefix(z1, z3))
   prefix(Nil, z0) -> True
   prefix(Cons(z0, z1), Nil) -> False
   and(False, False) -> False
   and(True, False) -> False
   and(False, True) -> False
   and(True, True) -> True
   !EQ(S(z0), S(z1)) -> !EQ(z0, z1)
   !EQ(0, S(z0)) -> False
   !EQ(S(z0), 0) -> False
   !EQ(0, 0) -> True
Tuples:
   !EQ'(S(z0), S(z1)) -> c4(!EQ'(z0, z1))
   DOMATCH[ITE](False, z0, Cons(z1, z2), z3) -> c8(DOMATCH(z0, z2, Cons(z3, Cons(Nil, Nil))))
   DOMATCH[ITE](True, z0, Cons(z1, z2), z3) -> c9(DOMATCH(z0, z2, Cons(z3, Cons(Nil, Nil))))
   EQNATLIST[ITE](True, z0, z1, z2, z3) -> c11(EQNATLIST(z3, z1))
   DOMATCH(Cons(z0, z1), Nil, z2) -> c15
   DOMATCH(Nil, Nil, z0) -> c16
   DOMATCH(z0, Cons(z1, z2), z3) -> c17(DOMATCH[ITE](prefix(z0, Cons(z1, z2)), z0, Cons(z1, z2), z3), PREFIX(z0, Cons(z1, z2)))
   EQNATLIST(Cons(z0, z1), Cons(z2, z3)) -> c18(EQNATLIST[ITE](!EQ(z0, z2), z2, z3, z0, z1), !EQ'(z0, z2))
   EQNATLIST(Cons(z0, z1), Nil) -> c19
   EQNATLIST(Nil, Cons(z0, z1)) -> c20
   EQNATLIST(Nil, Nil) -> c21
   PREFIX(Cons(z0, z1), Cons(z2, z3)) -> c12(!EQ'(z0, z2), PREFIX(z1, z3))
S tuples:
   DOMATCH(Cons(z0, z1), Nil, z2) -> c15
   DOMATCH(Nil, Nil, z0) -> c16
   DOMATCH(z0, Cons(z1, z2), z3) -> c17(DOMATCH[ITE](prefix(z0, Cons(z1, z2)), z0, Cons(z1, z2), z3), PREFIX(z0, Cons(z1, z2)))
   EQNATLIST(Cons(z0, z1), Cons(z2, z3)) -> c18(EQNATLIST[ITE](!EQ(z0, z2), z2, z3, z0, z1), !EQ'(z0, z2))
   PREFIX(Cons(z0, z1), Cons(z2, z3)) -> c12(!EQ'(z0, z2), PREFIX(z1, z3))
K tuples:
   EQNATLIST(Cons(z0, z1), Nil) -> c19
   EQNATLIST(Nil, Cons(z0, z1)) -> c20
   EQNATLIST(Nil, Nil) -> c21
Defined Rule Symbols:   prefix_2, and_2, !EQ_2

Defined Pair Symbols:   !EQ'_2, DOMATCH[ITE]_4, EQNATLIST[ITE]_5, DOMATCH_3, EQNATLIST_2, PREFIX_2

Compound Symbols:   c4_1, c8_1, c9_1, c11_1, c15, c16, c17_2, c18_2, c19, c20, c21, c12_2


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

(13) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)))
Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.
   DOMATCH(Cons(z0, z1), Nil, z2) -> c15
We considered the (Usable) Rules:none
And the Tuples:
   !EQ'(S(z0), S(z1)) -> c4(!EQ'(z0, z1))
   DOMATCH[ITE](False, z0, Cons(z1, z2), z3) -> c8(DOMATCH(z0, z2, Cons(z3, Cons(Nil, Nil))))
   DOMATCH[ITE](True, z0, Cons(z1, z2), z3) -> c9(DOMATCH(z0, z2, Cons(z3, Cons(Nil, Nil))))
   EQNATLIST[ITE](True, z0, z1, z2, z3) -> c11(EQNATLIST(z3, z1))
   DOMATCH(Cons(z0, z1), Nil, z2) -> c15
   DOMATCH(Nil, Nil, z0) -> c16
   DOMATCH(z0, Cons(z1, z2), z3) -> c17(DOMATCH[ITE](prefix(z0, Cons(z1, z2)), z0, Cons(z1, z2), z3), PREFIX(z0, Cons(z1, z2)))
   EQNATLIST(Cons(z0, z1), Cons(z2, z3)) -> c18(EQNATLIST[ITE](!EQ(z0, z2), z2, z3, z0, z1), !EQ'(z0, z2))
   EQNATLIST(Cons(z0, z1), Nil) -> c19
   EQNATLIST(Nil, Cons(z0, z1)) -> c20
   EQNATLIST(Nil, Nil) -> c21
   PREFIX(Cons(z0, z1), Cons(z2, z3)) -> c12(!EQ'(z0, z2), PREFIX(z1, z3))
The order we found is given by the following interpretation:

Polynomial interpretation :

   POL(!EQ(x_1, x_2)) = [1]
   POL(!EQ'(x_1, x_2)) = 0
   POL(0) = [1]
   POL(Cons(x_1, x_2)) = [1]
   POL(DOMATCH(x_1, x_2, x_3)) = x_1
   POL(DOMATCH[ITE](x_1, x_2, x_3, x_4)) = x_2
   POL(EQNATLIST(x_1, x_2)) = 0
   POL(EQNATLIST[ITE](x_1, x_2, x_3, x_4, x_5)) = 0
   POL(False) = [1]
   POL(Nil) = 0
   POL(PREFIX(x_1, x_2)) = 0
   POL(S(x_1)) = [1] + x_1
   POL(True) = 0
   POL(and(x_1, x_2)) = [1] + x_1
   POL(c11(x_1)) = x_1
   POL(c12(x_1, x_2)) = x_1 + x_2
   POL(c15) = 0
   POL(c16) = 0
   POL(c17(x_1, x_2)) = x_1 + x_2
   POL(c18(x_1, x_2)) = x_1 + x_2
   POL(c19) = 0
   POL(c20) = 0
   POL(c21) = 0
   POL(c4(x_1)) = x_1
   POL(c8(x_1)) = x_1
   POL(c9(x_1)) = x_1
   POL(prefix(x_1, x_2)) = [1] + x_1 + x_2

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

(14)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   prefix(Cons(z0, z1), Cons(z2, z3)) -> and(!EQ(z0, z2), prefix(z1, z3))
   prefix(Nil, z0) -> True
   prefix(Cons(z0, z1), Nil) -> False
   and(False, False) -> False
   and(True, False) -> False
   and(False, True) -> False
   and(True, True) -> True
   !EQ(S(z0), S(z1)) -> !EQ(z0, z1)
   !EQ(0, S(z0)) -> False
   !EQ(S(z0), 0) -> False
   !EQ(0, 0) -> True
Tuples:
   !EQ'(S(z0), S(z1)) -> c4(!EQ'(z0, z1))
   DOMATCH[ITE](False, z0, Cons(z1, z2), z3) -> c8(DOMATCH(z0, z2, Cons(z3, Cons(Nil, Nil))))
   DOMATCH[ITE](True, z0, Cons(z1, z2), z3) -> c9(DOMATCH(z0, z2, Cons(z3, Cons(Nil, Nil))))
   EQNATLIST[ITE](True, z0, z1, z2, z3) -> c11(EQNATLIST(z3, z1))
   DOMATCH(Cons(z0, z1), Nil, z2) -> c15
   DOMATCH(Nil, Nil, z0) -> c16
   DOMATCH(z0, Cons(z1, z2), z3) -> c17(DOMATCH[ITE](prefix(z0, Cons(z1, z2)), z0, Cons(z1, z2), z3), PREFIX(z0, Cons(z1, z2)))
   EQNATLIST(Cons(z0, z1), Cons(z2, z3)) -> c18(EQNATLIST[ITE](!EQ(z0, z2), z2, z3, z0, z1), !EQ'(z0, z2))
   EQNATLIST(Cons(z0, z1), Nil) -> c19
   EQNATLIST(Nil, Cons(z0, z1)) -> c20
   EQNATLIST(Nil, Nil) -> c21
   PREFIX(Cons(z0, z1), Cons(z2, z3)) -> c12(!EQ'(z0, z2), PREFIX(z1, z3))
S tuples:
   DOMATCH(Nil, Nil, z0) -> c16
   DOMATCH(z0, Cons(z1, z2), z3) -> c17(DOMATCH[ITE](prefix(z0, Cons(z1, z2)), z0, Cons(z1, z2), z3), PREFIX(z0, Cons(z1, z2)))
   EQNATLIST(Cons(z0, z1), Cons(z2, z3)) -> c18(EQNATLIST[ITE](!EQ(z0, z2), z2, z3, z0, z1), !EQ'(z0, z2))
   PREFIX(Cons(z0, z1), Cons(z2, z3)) -> c12(!EQ'(z0, z2), PREFIX(z1, z3))
K tuples:
   EQNATLIST(Cons(z0, z1), Nil) -> c19
   EQNATLIST(Nil, Cons(z0, z1)) -> c20
   EQNATLIST(Nil, Nil) -> c21
   DOMATCH(Cons(z0, z1), Nil, z2) -> c15
Defined Rule Symbols:   prefix_2, and_2, !EQ_2

Defined Pair Symbols:   !EQ'_2, DOMATCH[ITE]_4, EQNATLIST[ITE]_5, DOMATCH_3, EQNATLIST_2, PREFIX_2

Compound Symbols:   c4_1, c8_1, c9_1, c11_1, c15, c16, c17_2, c18_2, c19, c20, c21, c12_2


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

(15) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)))
Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.
   DOMATCH(Nil, Nil, z0) -> c16
We considered the (Usable) Rules:none
And the Tuples:
   !EQ'(S(z0), S(z1)) -> c4(!EQ'(z0, z1))
   DOMATCH[ITE](False, z0, Cons(z1, z2), z3) -> c8(DOMATCH(z0, z2, Cons(z3, Cons(Nil, Nil))))
   DOMATCH[ITE](True, z0, Cons(z1, z2), z3) -> c9(DOMATCH(z0, z2, Cons(z3, Cons(Nil, Nil))))
   EQNATLIST[ITE](True, z0, z1, z2, z3) -> c11(EQNATLIST(z3, z1))
   DOMATCH(Cons(z0, z1), Nil, z2) -> c15
   DOMATCH(Nil, Nil, z0) -> c16
   DOMATCH(z0, Cons(z1, z2), z3) -> c17(DOMATCH[ITE](prefix(z0, Cons(z1, z2)), z0, Cons(z1, z2), z3), PREFIX(z0, Cons(z1, z2)))
   EQNATLIST(Cons(z0, z1), Cons(z2, z3)) -> c18(EQNATLIST[ITE](!EQ(z0, z2), z2, z3, z0, z1), !EQ'(z0, z2))
   EQNATLIST(Cons(z0, z1), Nil) -> c19
   EQNATLIST(Nil, Cons(z0, z1)) -> c20
   EQNATLIST(Nil, Nil) -> c21
   PREFIX(Cons(z0, z1), Cons(z2, z3)) -> c12(!EQ'(z0, z2), PREFIX(z1, z3))
The order we found is given by the following interpretation:

Polynomial interpretation :

   POL(!EQ(x_1, x_2)) = [1]
   POL(!EQ'(x_1, x_2)) = 0
   POL(0) = [1]
   POL(Cons(x_1, x_2)) = 0
   POL(DOMATCH(x_1, x_2, x_3)) = x_1 + x_3
   POL(DOMATCH[ITE](x_1, x_2, x_3, x_4)) = x_2 + x_3 + x_4
   POL(EQNATLIST(x_1, x_2)) = 0
   POL(EQNATLIST[ITE](x_1, x_2, x_3, x_4, x_5)) = 0
   POL(False) = [1]
   POL(Nil) = [1]
   POL(PREFIX(x_1, x_2)) = 0
   POL(S(x_1)) = [1] + x_1
   POL(True) = 0
   POL(and(x_1, x_2)) = [1] + x_1
   POL(c11(x_1)) = x_1
   POL(c12(x_1, x_2)) = x_1 + x_2
   POL(c15) = 0
   POL(c16) = 0
   POL(c17(x_1, x_2)) = x_1 + x_2
   POL(c18(x_1, x_2)) = x_1 + x_2
   POL(c19) = 0
   POL(c20) = 0
   POL(c21) = 0
   POL(c4(x_1)) = x_1
   POL(c8(x_1)) = x_1
   POL(c9(x_1)) = x_1
   POL(prefix(x_1, x_2)) = [1] + x_1

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

(16)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   prefix(Cons(z0, z1), Cons(z2, z3)) -> and(!EQ(z0, z2), prefix(z1, z3))
   prefix(Nil, z0) -> True
   prefix(Cons(z0, z1), Nil) -> False
   and(False, False) -> False
   and(True, False) -> False
   and(False, True) -> False
   and(True, True) -> True
   !EQ(S(z0), S(z1)) -> !EQ(z0, z1)
   !EQ(0, S(z0)) -> False
   !EQ(S(z0), 0) -> False
   !EQ(0, 0) -> True
Tuples:
   !EQ'(S(z0), S(z1)) -> c4(!EQ'(z0, z1))
   DOMATCH[ITE](False, z0, Cons(z1, z2), z3) -> c8(DOMATCH(z0, z2, Cons(z3, Cons(Nil, Nil))))
   DOMATCH[ITE](True, z0, Cons(z1, z2), z3) -> c9(DOMATCH(z0, z2, Cons(z3, Cons(Nil, Nil))))
   EQNATLIST[ITE](True, z0, z1, z2, z3) -> c11(EQNATLIST(z3, z1))
   DOMATCH(Cons(z0, z1), Nil, z2) -> c15
   DOMATCH(Nil, Nil, z0) -> c16
   DOMATCH(z0, Cons(z1, z2), z3) -> c17(DOMATCH[ITE](prefix(z0, Cons(z1, z2)), z0, Cons(z1, z2), z3), PREFIX(z0, Cons(z1, z2)))
   EQNATLIST(Cons(z0, z1), Cons(z2, z3)) -> c18(EQNATLIST[ITE](!EQ(z0, z2), z2, z3, z0, z1), !EQ'(z0, z2))
   EQNATLIST(Cons(z0, z1), Nil) -> c19
   EQNATLIST(Nil, Cons(z0, z1)) -> c20
   EQNATLIST(Nil, Nil) -> c21
   PREFIX(Cons(z0, z1), Cons(z2, z3)) -> c12(!EQ'(z0, z2), PREFIX(z1, z3))
S tuples:
   DOMATCH(z0, Cons(z1, z2), z3) -> c17(DOMATCH[ITE](prefix(z0, Cons(z1, z2)), z0, Cons(z1, z2), z3), PREFIX(z0, Cons(z1, z2)))
   EQNATLIST(Cons(z0, z1), Cons(z2, z3)) -> c18(EQNATLIST[ITE](!EQ(z0, z2), z2, z3, z0, z1), !EQ'(z0, z2))
   PREFIX(Cons(z0, z1), Cons(z2, z3)) -> c12(!EQ'(z0, z2), PREFIX(z1, z3))
K tuples:
   EQNATLIST(Cons(z0, z1), Nil) -> c19
   EQNATLIST(Nil, Cons(z0, z1)) -> c20
   EQNATLIST(Nil, Nil) -> c21
   DOMATCH(Cons(z0, z1), Nil, z2) -> c15
   DOMATCH(Nil, Nil, z0) -> c16
Defined Rule Symbols:   prefix_2, and_2, !EQ_2

Defined Pair Symbols:   !EQ'_2, DOMATCH[ITE]_4, EQNATLIST[ITE]_5, DOMATCH_3, EQNATLIST_2, PREFIX_2

Compound Symbols:   c4_1, c8_1, c9_1, c11_1, c15, c16, c17_2, c18_2, c19, c20, c21, c12_2


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

(17) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)))
Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.
   EQNATLIST(Cons(z0, z1), Cons(z2, z3)) -> c18(EQNATLIST[ITE](!EQ(z0, z2), z2, z3, z0, z1), !EQ'(z0, z2))
We considered the (Usable) Rules:none
And the Tuples:
   !EQ'(S(z0), S(z1)) -> c4(!EQ'(z0, z1))
   DOMATCH[ITE](False, z0, Cons(z1, z2), z3) -> c8(DOMATCH(z0, z2, Cons(z3, Cons(Nil, Nil))))
   DOMATCH[ITE](True, z0, Cons(z1, z2), z3) -> c9(DOMATCH(z0, z2, Cons(z3, Cons(Nil, Nil))))
   EQNATLIST[ITE](True, z0, z1, z2, z3) -> c11(EQNATLIST(z3, z1))
   DOMATCH(Cons(z0, z1), Nil, z2) -> c15
   DOMATCH(Nil, Nil, z0) -> c16
   DOMATCH(z0, Cons(z1, z2), z3) -> c17(DOMATCH[ITE](prefix(z0, Cons(z1, z2)), z0, Cons(z1, z2), z3), PREFIX(z0, Cons(z1, z2)))
   EQNATLIST(Cons(z0, z1), Cons(z2, z3)) -> c18(EQNATLIST[ITE](!EQ(z0, z2), z2, z3, z0, z1), !EQ'(z0, z2))
   EQNATLIST(Cons(z0, z1), Nil) -> c19
   EQNATLIST(Nil, Cons(z0, z1)) -> c20
   EQNATLIST(Nil, Nil) -> c21
   PREFIX(Cons(z0, z1), Cons(z2, z3)) -> c12(!EQ'(z0, z2), PREFIX(z1, z3))
The order we found is given by the following interpretation:

Polynomial interpretation :

   POL(!EQ(x_1, x_2)) = 0
   POL(!EQ'(x_1, x_2)) = 0
   POL(0) = [3]
   POL(Cons(x_1, x_2)) = [3] + x_2
   POL(DOMATCH(x_1, x_2, x_3)) = 0
   POL(DOMATCH[ITE](x_1, x_2, x_3, x_4)) = 0
   POL(EQNATLIST(x_1, x_2)) = [3]x_1 + x_2
   POL(EQNATLIST[ITE](x_1, x_2, x_3, x_4, x_5)) = x_3 + [3]x_5
   POL(False) = 0
   POL(Nil) = 0
   POL(PREFIX(x_1, x_2)) = 0
   POL(S(x_1)) = [3] + x_1
   POL(True) = 0
   POL(and(x_1, x_2)) = 0
   POL(c11(x_1)) = x_1
   POL(c12(x_1, x_2)) = x_1 + x_2
   POL(c15) = 0
   POL(c16) = 0
   POL(c17(x_1, x_2)) = x_1 + x_2
   POL(c18(x_1, x_2)) = x_1 + x_2
   POL(c19) = 0
   POL(c20) = 0
   POL(c21) = 0
   POL(c4(x_1)) = x_1
   POL(c8(x_1)) = x_1
   POL(c9(x_1)) = x_1
   POL(prefix(x_1, x_2)) = [3]x_1 + [3]x_2

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

(18)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   prefix(Cons(z0, z1), Cons(z2, z3)) -> and(!EQ(z0, z2), prefix(z1, z3))
   prefix(Nil, z0) -> True
   prefix(Cons(z0, z1), Nil) -> False
   and(False, False) -> False
   and(True, False) -> False
   and(False, True) -> False
   and(True, True) -> True
   !EQ(S(z0), S(z1)) -> !EQ(z0, z1)
   !EQ(0, S(z0)) -> False
   !EQ(S(z0), 0) -> False
   !EQ(0, 0) -> True
Tuples:
   !EQ'(S(z0), S(z1)) -> c4(!EQ'(z0, z1))
   DOMATCH[ITE](False, z0, Cons(z1, z2), z3) -> c8(DOMATCH(z0, z2, Cons(z3, Cons(Nil, Nil))))
   DOMATCH[ITE](True, z0, Cons(z1, z2), z3) -> c9(DOMATCH(z0, z2, Cons(z3, Cons(Nil, Nil))))
   EQNATLIST[ITE](True, z0, z1, z2, z3) -> c11(EQNATLIST(z3, z1))
   DOMATCH(Cons(z0, z1), Nil, z2) -> c15
   DOMATCH(Nil, Nil, z0) -> c16
   DOMATCH(z0, Cons(z1, z2), z3) -> c17(DOMATCH[ITE](prefix(z0, Cons(z1, z2)), z0, Cons(z1, z2), z3), PREFIX(z0, Cons(z1, z2)))
   EQNATLIST(Cons(z0, z1), Cons(z2, z3)) -> c18(EQNATLIST[ITE](!EQ(z0, z2), z2, z3, z0, z1), !EQ'(z0, z2))
   EQNATLIST(Cons(z0, z1), Nil) -> c19
   EQNATLIST(Nil, Cons(z0, z1)) -> c20
   EQNATLIST(Nil, Nil) -> c21
   PREFIX(Cons(z0, z1), Cons(z2, z3)) -> c12(!EQ'(z0, z2), PREFIX(z1, z3))
S tuples:
   DOMATCH(z0, Cons(z1, z2), z3) -> c17(DOMATCH[ITE](prefix(z0, Cons(z1, z2)), z0, Cons(z1, z2), z3), PREFIX(z0, Cons(z1, z2)))
   PREFIX(Cons(z0, z1), Cons(z2, z3)) -> c12(!EQ'(z0, z2), PREFIX(z1, z3))
K tuples:
   EQNATLIST(Cons(z0, z1), Nil) -> c19
   EQNATLIST(Nil, Cons(z0, z1)) -> c20
   EQNATLIST(Nil, Nil) -> c21
   DOMATCH(Cons(z0, z1), Nil, z2) -> c15
   DOMATCH(Nil, Nil, z0) -> c16
   EQNATLIST(Cons(z0, z1), Cons(z2, z3)) -> c18(EQNATLIST[ITE](!EQ(z0, z2), z2, z3, z0, z1), !EQ'(z0, z2))
Defined Rule Symbols:   prefix_2, and_2, !EQ_2

Defined Pair Symbols:   !EQ'_2, DOMATCH[ITE]_4, EQNATLIST[ITE]_5, DOMATCH_3, EQNATLIST_2, PREFIX_2

Compound Symbols:   c4_1, c8_1, c9_1, c11_1, c15, c16, c17_2, c18_2, c19, c20, c21, c12_2


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

(19) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)))
Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.
   DOMATCH(z0, Cons(z1, z2), z3) -> c17(DOMATCH[ITE](prefix(z0, Cons(z1, z2)), z0, Cons(z1, z2), z3), PREFIX(z0, Cons(z1, z2)))
We considered the (Usable) Rules:none
And the Tuples:
   !EQ'(S(z0), S(z1)) -> c4(!EQ'(z0, z1))
   DOMATCH[ITE](False, z0, Cons(z1, z2), z3) -> c8(DOMATCH(z0, z2, Cons(z3, Cons(Nil, Nil))))
   DOMATCH[ITE](True, z0, Cons(z1, z2), z3) -> c9(DOMATCH(z0, z2, Cons(z3, Cons(Nil, Nil))))
   EQNATLIST[ITE](True, z0, z1, z2, z3) -> c11(EQNATLIST(z3, z1))
   DOMATCH(Cons(z0, z1), Nil, z2) -> c15
   DOMATCH(Nil, Nil, z0) -> c16
   DOMATCH(z0, Cons(z1, z2), z3) -> c17(DOMATCH[ITE](prefix(z0, Cons(z1, z2)), z0, Cons(z1, z2), z3), PREFIX(z0, Cons(z1, z2)))
   EQNATLIST(Cons(z0, z1), Cons(z2, z3)) -> c18(EQNATLIST[ITE](!EQ(z0, z2), z2, z3, z0, z1), !EQ'(z0, z2))
   EQNATLIST(Cons(z0, z1), Nil) -> c19
   EQNATLIST(Nil, Cons(z0, z1)) -> c20
   EQNATLIST(Nil, Nil) -> c21
   PREFIX(Cons(z0, z1), Cons(z2, z3)) -> c12(!EQ'(z0, z2), PREFIX(z1, z3))
The order we found is given by the following interpretation:

Polynomial interpretation :

   POL(!EQ(x_1, x_2)) = [1]
   POL(!EQ'(x_1, x_2)) = 0
   POL(0) = [1]
   POL(Cons(x_1, x_2)) = [1] + x_2
   POL(DOMATCH(x_1, x_2, x_3)) = [1] + x_1 + x_2
   POL(DOMATCH[ITE](x_1, x_2, x_3, x_4)) = x_2 + x_3
   POL(EQNATLIST(x_1, x_2)) = 0
   POL(EQNATLIST[ITE](x_1, x_2, x_3, x_4, x_5)) = 0
   POL(False) = [1]
   POL(Nil) = 0
   POL(PREFIX(x_1, x_2)) = 0
   POL(S(x_1)) = [1] + x_1
   POL(True) = 0
   POL(and(x_1, x_2)) = [1] + x_1
   POL(c11(x_1)) = x_1
   POL(c12(x_1, x_2)) = x_1 + x_2
   POL(c15) = 0
   POL(c16) = 0
   POL(c17(x_1, x_2)) = x_1 + x_2
   POL(c18(x_1, x_2)) = x_1 + x_2
   POL(c19) = 0
   POL(c20) = 0
   POL(c21) = 0
   POL(c4(x_1)) = x_1
   POL(c8(x_1)) = x_1
   POL(c9(x_1)) = x_1
   POL(prefix(x_1, x_2)) = [1] + x_1 + x_2

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

(20)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   prefix(Cons(z0, z1), Cons(z2, z3)) -> and(!EQ(z0, z2), prefix(z1, z3))
   prefix(Nil, z0) -> True
   prefix(Cons(z0, z1), Nil) -> False
   and(False, False) -> False
   and(True, False) -> False
   and(False, True) -> False
   and(True, True) -> True
   !EQ(S(z0), S(z1)) -> !EQ(z0, z1)
   !EQ(0, S(z0)) -> False
   !EQ(S(z0), 0) -> False
   !EQ(0, 0) -> True
Tuples:
   !EQ'(S(z0), S(z1)) -> c4(!EQ'(z0, z1))
   DOMATCH[ITE](False, z0, Cons(z1, z2), z3) -> c8(DOMATCH(z0, z2, Cons(z3, Cons(Nil, Nil))))
   DOMATCH[ITE](True, z0, Cons(z1, z2), z3) -> c9(DOMATCH(z0, z2, Cons(z3, Cons(Nil, Nil))))
   EQNATLIST[ITE](True, z0, z1, z2, z3) -> c11(EQNATLIST(z3, z1))
   DOMATCH(Cons(z0, z1), Nil, z2) -> c15
   DOMATCH(Nil, Nil, z0) -> c16
   DOMATCH(z0, Cons(z1, z2), z3) -> c17(DOMATCH[ITE](prefix(z0, Cons(z1, z2)), z0, Cons(z1, z2), z3), PREFIX(z0, Cons(z1, z2)))
   EQNATLIST(Cons(z0, z1), Cons(z2, z3)) -> c18(EQNATLIST[ITE](!EQ(z0, z2), z2, z3, z0, z1), !EQ'(z0, z2))
   EQNATLIST(Cons(z0, z1), Nil) -> c19
   EQNATLIST(Nil, Cons(z0, z1)) -> c20
   EQNATLIST(Nil, Nil) -> c21
   PREFIX(Cons(z0, z1), Cons(z2, z3)) -> c12(!EQ'(z0, z2), PREFIX(z1, z3))
S tuples:
   PREFIX(Cons(z0, z1), Cons(z2, z3)) -> c12(!EQ'(z0, z2), PREFIX(z1, z3))
K tuples:
   EQNATLIST(Cons(z0, z1), Nil) -> c19
   EQNATLIST(Nil, Cons(z0, z1)) -> c20
   EQNATLIST(Nil, Nil) -> c21
   DOMATCH(Cons(z0, z1), Nil, z2) -> c15
   DOMATCH(Nil, Nil, z0) -> c16
   EQNATLIST(Cons(z0, z1), Cons(z2, z3)) -> c18(EQNATLIST[ITE](!EQ(z0, z2), z2, z3, z0, z1), !EQ'(z0, z2))
   DOMATCH(z0, Cons(z1, z2), z3) -> c17(DOMATCH[ITE](prefix(z0, Cons(z1, z2)), z0, Cons(z1, z2), z3), PREFIX(z0, Cons(z1, z2)))
Defined Rule Symbols:   prefix_2, and_2, !EQ_2

Defined Pair Symbols:   !EQ'_2, DOMATCH[ITE]_4, EQNATLIST[ITE]_5, DOMATCH_3, EQNATLIST_2, PREFIX_2

Compound Symbols:   c4_1, c8_1, c9_1, c11_1, c15, c16, c17_2, c18_2, c19, c20, c21, c12_2


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

(21) CdtRuleRemovalProof (UPPER BOUND(ADD(n^2)))
Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.
   PREFIX(Cons(z0, z1), Cons(z2, z3)) -> c12(!EQ'(z0, z2), PREFIX(z1, z3))
We considered the (Usable) Rules:none
And the Tuples:
   !EQ'(S(z0), S(z1)) -> c4(!EQ'(z0, z1))
   DOMATCH[ITE](False, z0, Cons(z1, z2), z3) -> c8(DOMATCH(z0, z2, Cons(z3, Cons(Nil, Nil))))
   DOMATCH[ITE](True, z0, Cons(z1, z2), z3) -> c9(DOMATCH(z0, z2, Cons(z3, Cons(Nil, Nil))))
   EQNATLIST[ITE](True, z0, z1, z2, z3) -> c11(EQNATLIST(z3, z1))
   DOMATCH(Cons(z0, z1), Nil, z2) -> c15
   DOMATCH(Nil, Nil, z0) -> c16
   DOMATCH(z0, Cons(z1, z2), z3) -> c17(DOMATCH[ITE](prefix(z0, Cons(z1, z2)), z0, Cons(z1, z2), z3), PREFIX(z0, Cons(z1, z2)))
   EQNATLIST(Cons(z0, z1), Cons(z2, z3)) -> c18(EQNATLIST[ITE](!EQ(z0, z2), z2, z3, z0, z1), !EQ'(z0, z2))
   EQNATLIST(Cons(z0, z1), Nil) -> c19
   EQNATLIST(Nil, Cons(z0, z1)) -> c20
   EQNATLIST(Nil, Nil) -> c21
   PREFIX(Cons(z0, z1), Cons(z2, z3)) -> c12(!EQ'(z0, z2), PREFIX(z1, z3))
The order we found is given by the following interpretation:

Polynomial interpretation :

   POL(!EQ(x_1, x_2)) = 0
   POL(!EQ'(x_1, x_2)) = 0
   POL(0) = 0
   POL(Cons(x_1, x_2)) = [1] + x_2
   POL(DOMATCH(x_1, x_2, x_3)) = x_1 + x_1*x_2
   POL(DOMATCH[ITE](x_1, x_2, x_3, x_4)) = x_2*x_3
   POL(EQNATLIST(x_1, x_2)) = 0
   POL(EQNATLIST[ITE](x_1, x_2, x_3, x_4, x_5)) = 0
   POL(False) = 0
   POL(Nil) = 0
   POL(PREFIX(x_1, x_2)) = x_1
   POL(S(x_1)) = 0
   POL(True) = 0
   POL(and(x_1, x_2)) = [1]
   POL(c11(x_1)) = x_1
   POL(c12(x_1, x_2)) = x_1 + x_2
   POL(c15) = 0
   POL(c16) = 0
   POL(c17(x_1, x_2)) = x_1 + x_2
   POL(c18(x_1, x_2)) = x_1 + x_2
   POL(c19) = 0
   POL(c20) = 0
   POL(c21) = 0
   POL(c4(x_1)) = x_1
   POL(c8(x_1)) = x_1
   POL(c9(x_1)) = x_1
   POL(prefix(x_1, x_2)) = 0

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

(22)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   prefix(Cons(z0, z1), Cons(z2, z3)) -> and(!EQ(z0, z2), prefix(z1, z3))
   prefix(Nil, z0) -> True
   prefix(Cons(z0, z1), Nil) -> False
   and(False, False) -> False
   and(True, False) -> False
   and(False, True) -> False
   and(True, True) -> True
   !EQ(S(z0), S(z1)) -> !EQ(z0, z1)
   !EQ(0, S(z0)) -> False
   !EQ(S(z0), 0) -> False
   !EQ(0, 0) -> True
Tuples:
   !EQ'(S(z0), S(z1)) -> c4(!EQ'(z0, z1))
   DOMATCH[ITE](False, z0, Cons(z1, z2), z3) -> c8(DOMATCH(z0, z2, Cons(z3, Cons(Nil, Nil))))
   DOMATCH[ITE](True, z0, Cons(z1, z2), z3) -> c9(DOMATCH(z0, z2, Cons(z3, Cons(Nil, Nil))))
   EQNATLIST[ITE](True, z0, z1, z2, z3) -> c11(EQNATLIST(z3, z1))
   DOMATCH(Cons(z0, z1), Nil, z2) -> c15
   DOMATCH(Nil, Nil, z0) -> c16
   DOMATCH(z0, Cons(z1, z2), z3) -> c17(DOMATCH[ITE](prefix(z0, Cons(z1, z2)), z0, Cons(z1, z2), z3), PREFIX(z0, Cons(z1, z2)))
   EQNATLIST(Cons(z0, z1), Cons(z2, z3)) -> c18(EQNATLIST[ITE](!EQ(z0, z2), z2, z3, z0, z1), !EQ'(z0, z2))
   EQNATLIST(Cons(z0, z1), Nil) -> c19
   EQNATLIST(Nil, Cons(z0, z1)) -> c20
   EQNATLIST(Nil, Nil) -> c21
   PREFIX(Cons(z0, z1), Cons(z2, z3)) -> c12(!EQ'(z0, z2), PREFIX(z1, z3))
S tuples:none
K tuples:
   EQNATLIST(Cons(z0, z1), Nil) -> c19
   EQNATLIST(Nil, Cons(z0, z1)) -> c20
   EQNATLIST(Nil, Nil) -> c21
   DOMATCH(Cons(z0, z1), Nil, z2) -> c15
   DOMATCH(Nil, Nil, z0) -> c16
   EQNATLIST(Cons(z0, z1), Cons(z2, z3)) -> c18(EQNATLIST[ITE](!EQ(z0, z2), z2, z3, z0, z1), !EQ'(z0, z2))
   DOMATCH(z0, Cons(z1, z2), z3) -> c17(DOMATCH[ITE](prefix(z0, Cons(z1, z2)), z0, Cons(z1, z2), z3), PREFIX(z0, Cons(z1, z2)))
   PREFIX(Cons(z0, z1), Cons(z2, z3)) -> c12(!EQ'(z0, z2), PREFIX(z1, z3))
Defined Rule Symbols:   prefix_2, and_2, !EQ_2

Defined Pair Symbols:   !EQ'_2, DOMATCH[ITE]_4, EQNATLIST[ITE]_5, DOMATCH_3, EQNATLIST_2, PREFIX_2

Compound Symbols:   c4_1, c8_1, c9_1, c11_1, c15, c16, c17_2, c18_2, c19, c20, c21, c12_2


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

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

(24)
BOUNDS(1, 1)

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

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

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


The TRS R consists of the following rules:

   prefix(Cons(x', xs'), Cons(x, xs)) -> and(!EQ(x', x), prefix(xs', xs))
   domatch(Cons(x, xs), Nil, n) -> Nil
   domatch(Nil, Nil, n) -> Cons(n, Nil)
   prefix(Cons(x, xs), Nil) -> False
   prefix(Nil, cs) -> True
   domatch(patcs, Cons(x, xs), n) -> domatch[Ite](prefix(patcs, Cons(x, xs)), patcs, Cons(x, xs), n)
   eqNatList(Cons(x, xs), Cons(y, ys)) -> eqNatList[Ite](!EQ(x, y), y, ys, x, xs)
   eqNatList(Cons(x, xs), Nil) -> False
   eqNatList(Nil, Cons(y, ys)) -> False
   eqNatList(Nil, Nil) -> True
   notEmpty(Cons(x, xs)) -> True
   notEmpty(Nil) -> False
   strmatch(patstr, str) -> domatch(patstr, str, Nil)

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

   and(False, False) -> False
   and(True, False) -> False
   and(False, True) -> False
   and(True, True) -> True
   !EQ(S(x), S(y)) -> !EQ(x, y)
   !EQ(0', S(y)) -> False
   !EQ(S(x), 0') -> False
   !EQ(0', 0') -> True
   domatch[Ite](False, patcs, Cons(x, xs), n) -> domatch(patcs, xs, Cons(n, Cons(Nil, Nil)))
   domatch[Ite](True, patcs, Cons(x, xs), n) -> Cons(n, domatch(patcs, xs, Cons(n, Cons(Nil, Nil))))
   eqNatList[Ite](False, y, ys, x, xs) -> False
   eqNatList[Ite](True, y, ys, x, xs) -> eqNatList(xs, ys)

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

(27) SlicingProof (LOWER BOUND(ID))
Sliced the following arguments:
eqNatList[Ite]/1
eqNatList[Ite]/3

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

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


The TRS R consists of the following rules:

   prefix(Cons(x', xs'), Cons(x, xs)) -> and(!EQ(x', x), prefix(xs', xs))
   domatch(Cons(x, xs), Nil, n) -> Nil
   domatch(Nil, Nil, n) -> Cons(n, Nil)
   prefix(Cons(x, xs), Nil) -> False
   prefix(Nil, cs) -> True
   domatch(patcs, Cons(x, xs), n) -> domatch[Ite](prefix(patcs, Cons(x, xs)), patcs, Cons(x, xs), n)
   eqNatList(Cons(x, xs), Cons(y, ys)) -> eqNatList[Ite](!EQ(x, y), ys, xs)
   eqNatList(Cons(x, xs), Nil) -> False
   eqNatList(Nil, Cons(y, ys)) -> False
   eqNatList(Nil, Nil) -> True
   notEmpty(Cons(x, xs)) -> True
   notEmpty(Nil) -> False
   strmatch(patstr, str) -> domatch(patstr, str, Nil)

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

   and(False, False) -> False
   and(True, False) -> False
   and(False, True) -> False
   and(True, True) -> True
   !EQ(S(x), S(y)) -> !EQ(x, y)
   !EQ(0', S(y)) -> False
   !EQ(S(x), 0') -> False
   !EQ(0', 0') -> True
   domatch[Ite](False, patcs, Cons(x, xs), n) -> domatch(patcs, xs, Cons(n, Cons(Nil, Nil)))
   domatch[Ite](True, patcs, Cons(x, xs), n) -> Cons(n, domatch(patcs, xs, Cons(n, Cons(Nil, Nil))))
   eqNatList[Ite](False, ys, xs) -> False
   eqNatList[Ite](True, ys, xs) -> eqNatList(xs, ys)

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

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

(30)
Obligation:
Innermost TRS:
Rules:
prefix(Cons(x', xs'), Cons(x, xs)) -> and(!EQ(x', x), prefix(xs', xs))
domatch(Cons(x, xs), Nil, n) -> Nil
domatch(Nil, Nil, n) -> Cons(n, Nil)
prefix(Cons(x, xs), Nil) -> False
prefix(Nil, cs) -> True
domatch(patcs, Cons(x, xs), n) -> domatch[Ite](prefix(patcs, Cons(x, xs)), patcs, Cons(x, xs), n)
eqNatList(Cons(x, xs), Cons(y, ys)) -> eqNatList[Ite](!EQ(x, y), ys, xs)
eqNatList(Cons(x, xs), Nil) -> False
eqNatList(Nil, Cons(y, ys)) -> False
eqNatList(Nil, Nil) -> True
notEmpty(Cons(x, xs)) -> True
notEmpty(Nil) -> False
strmatch(patstr, str) -> domatch(patstr, str, Nil)
and(False, False) -> False
and(True, False) -> False
and(False, True) -> False
and(True, True) -> True
!EQ(S(x), S(y)) -> !EQ(x, y)
!EQ(0', S(y)) -> False
!EQ(S(x), 0') -> False
!EQ(0', 0') -> True
domatch[Ite](False, patcs, Cons(x, xs), n) -> domatch(patcs, xs, Cons(n, Cons(Nil, Nil)))
domatch[Ite](True, patcs, Cons(x, xs), n) -> Cons(n, domatch(patcs, xs, Cons(n, Cons(Nil, Nil))))
eqNatList[Ite](False, ys, xs) -> False
eqNatList[Ite](True, ys, xs) -> eqNatList(xs, ys)

Types:
prefix :: Cons:Nil:S:0' -> Cons:Nil:S:0' -> False:True
Cons :: Cons:Nil:S:0' -> Cons:Nil:S:0' -> Cons:Nil:S:0'
and :: False:True -> False:True -> False:True
!EQ :: Cons:Nil:S:0' -> Cons:Nil:S:0' -> False:True
domatch :: Cons:Nil:S:0' -> Cons:Nil:S:0' -> Cons:Nil:S:0' -> Cons:Nil:S:0'
Nil :: Cons:Nil:S:0'
False :: False:True
True :: False:True
domatch[Ite] :: False:True -> Cons:Nil:S:0' -> Cons:Nil:S:0' -> Cons:Nil:S:0' -> Cons:Nil:S:0'
eqNatList :: Cons:Nil:S:0' -> Cons:Nil:S:0' -> False:True
eqNatList[Ite] :: False:True -> Cons:Nil:S:0' -> Cons:Nil:S:0' -> False:True
notEmpty :: Cons:Nil:S:0' -> False:True
strmatch :: Cons:Nil:S:0' -> Cons:Nil:S:0' -> Cons:Nil:S:0'
S :: Cons:Nil:S:0' -> Cons:Nil:S:0'
0' :: Cons:Nil:S:0'
hole_False:True1_0 :: False:True
hole_Cons:Nil:S:0'2_0 :: Cons:Nil:S:0'
gen_Cons:Nil:S:0'3_0 :: Nat -> Cons:Nil:S:0'

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

(31) OrderProof (LOWER BOUND(ID))
Heuristically decided to analyse the following defined symbols:
prefix, !EQ, domatch, eqNatList

They will be analysed ascendingly in the following order:
!EQ < prefix
prefix < domatch
!EQ < eqNatList

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

(32)
Obligation:
Innermost TRS:
Rules:
prefix(Cons(x', xs'), Cons(x, xs)) -> and(!EQ(x', x), prefix(xs', xs))
domatch(Cons(x, xs), Nil, n) -> Nil
domatch(Nil, Nil, n) -> Cons(n, Nil)
prefix(Cons(x, xs), Nil) -> False
prefix(Nil, cs) -> True
domatch(patcs, Cons(x, xs), n) -> domatch[Ite](prefix(patcs, Cons(x, xs)), patcs, Cons(x, xs), n)
eqNatList(Cons(x, xs), Cons(y, ys)) -> eqNatList[Ite](!EQ(x, y), ys, xs)
eqNatList(Cons(x, xs), Nil) -> False
eqNatList(Nil, Cons(y, ys)) -> False
eqNatList(Nil, Nil) -> True
notEmpty(Cons(x, xs)) -> True
notEmpty(Nil) -> False
strmatch(patstr, str) -> domatch(patstr, str, Nil)
and(False, False) -> False
and(True, False) -> False
and(False, True) -> False
and(True, True) -> True
!EQ(S(x), S(y)) -> !EQ(x, y)
!EQ(0', S(y)) -> False
!EQ(S(x), 0') -> False
!EQ(0', 0') -> True
domatch[Ite](False, patcs, Cons(x, xs), n) -> domatch(patcs, xs, Cons(n, Cons(Nil, Nil)))
domatch[Ite](True, patcs, Cons(x, xs), n) -> Cons(n, domatch(patcs, xs, Cons(n, Cons(Nil, Nil))))
eqNatList[Ite](False, ys, xs) -> False
eqNatList[Ite](True, ys, xs) -> eqNatList(xs, ys)

Types:
prefix :: Cons:Nil:S:0' -> Cons:Nil:S:0' -> False:True
Cons :: Cons:Nil:S:0' -> Cons:Nil:S:0' -> Cons:Nil:S:0'
and :: False:True -> False:True -> False:True
!EQ :: Cons:Nil:S:0' -> Cons:Nil:S:0' -> False:True
domatch :: Cons:Nil:S:0' -> Cons:Nil:S:0' -> Cons:Nil:S:0' -> Cons:Nil:S:0'
Nil :: Cons:Nil:S:0'
False :: False:True
True :: False:True
domatch[Ite] :: False:True -> Cons:Nil:S:0' -> Cons:Nil:S:0' -> Cons:Nil:S:0' -> Cons:Nil:S:0'
eqNatList :: Cons:Nil:S:0' -> Cons:Nil:S:0' -> False:True
eqNatList[Ite] :: False:True -> Cons:Nil:S:0' -> Cons:Nil:S:0' -> False:True
notEmpty :: Cons:Nil:S:0' -> False:True
strmatch :: Cons:Nil:S:0' -> Cons:Nil:S:0' -> Cons:Nil:S:0'
S :: Cons:Nil:S:0' -> Cons:Nil:S:0'
0' :: Cons:Nil:S:0'
hole_False:True1_0 :: False:True
hole_Cons:Nil:S:0'2_0 :: Cons:Nil:S:0'
gen_Cons:Nil:S:0'3_0 :: Nat -> Cons:Nil:S:0'


Generator Equations:
gen_Cons:Nil:S:0'3_0(0) <=> Nil
gen_Cons:Nil:S:0'3_0(+(x, 1)) <=> Cons(Nil, gen_Cons:Nil:S:0'3_0(x))


The following defined symbols remain to be analysed:
!EQ, prefix, domatch, eqNatList

They will be analysed ascendingly in the following order:
!EQ < prefix
prefix < domatch
!EQ < eqNatList

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

(33) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
prefix(gen_Cons:Nil:S:0'3_0(+(1, n20_0)), gen_Cons:Nil:S:0'3_0(+(1, n20_0))) -> *4_0, rt in Omega(n20_0)

Induction Base:
prefix(gen_Cons:Nil:S:0'3_0(+(1, 0)), gen_Cons:Nil:S:0'3_0(+(1, 0)))

Induction Step:
prefix(gen_Cons:Nil:S:0'3_0(+(1, +(n20_0, 1))), gen_Cons:Nil:S:0'3_0(+(1, +(n20_0, 1)))) ->_R^Omega(1)
and(!EQ(Nil, Nil), prefix(gen_Cons:Nil:S:0'3_0(+(1, n20_0)), gen_Cons:Nil:S:0'3_0(+(1, n20_0)))) ->_IH
and(!EQ(Nil, Nil), *4_0)

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

(34)
Complex Obligation (BEST)

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

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

Innermost TRS:
Rules:
prefix(Cons(x', xs'), Cons(x, xs)) -> and(!EQ(x', x), prefix(xs', xs))
domatch(Cons(x, xs), Nil, n) -> Nil
domatch(Nil, Nil, n) -> Cons(n, Nil)
prefix(Cons(x, xs), Nil) -> False
prefix(Nil, cs) -> True
domatch(patcs, Cons(x, xs), n) -> domatch[Ite](prefix(patcs, Cons(x, xs)), patcs, Cons(x, xs), n)
eqNatList(Cons(x, xs), Cons(y, ys)) -> eqNatList[Ite](!EQ(x, y), ys, xs)
eqNatList(Cons(x, xs), Nil) -> False
eqNatList(Nil, Cons(y, ys)) -> False
eqNatList(Nil, Nil) -> True
notEmpty(Cons(x, xs)) -> True
notEmpty(Nil) -> False
strmatch(patstr, str) -> domatch(patstr, str, Nil)
and(False, False) -> False
and(True, False) -> False
and(False, True) -> False
and(True, True) -> True
!EQ(S(x), S(y)) -> !EQ(x, y)
!EQ(0', S(y)) -> False
!EQ(S(x), 0') -> False
!EQ(0', 0') -> True
domatch[Ite](False, patcs, Cons(x, xs), n) -> domatch(patcs, xs, Cons(n, Cons(Nil, Nil)))
domatch[Ite](True, patcs, Cons(x, xs), n) -> Cons(n, domatch(patcs, xs, Cons(n, Cons(Nil, Nil))))
eqNatList[Ite](False, ys, xs) -> False
eqNatList[Ite](True, ys, xs) -> eqNatList(xs, ys)

Types:
prefix :: Cons:Nil:S:0' -> Cons:Nil:S:0' -> False:True
Cons :: Cons:Nil:S:0' -> Cons:Nil:S:0' -> Cons:Nil:S:0'
and :: False:True -> False:True -> False:True
!EQ :: Cons:Nil:S:0' -> Cons:Nil:S:0' -> False:True
domatch :: Cons:Nil:S:0' -> Cons:Nil:S:0' -> Cons:Nil:S:0' -> Cons:Nil:S:0'
Nil :: Cons:Nil:S:0'
False :: False:True
True :: False:True
domatch[Ite] :: False:True -> Cons:Nil:S:0' -> Cons:Nil:S:0' -> Cons:Nil:S:0' -> Cons:Nil:S:0'
eqNatList :: Cons:Nil:S:0' -> Cons:Nil:S:0' -> False:True
eqNatList[Ite] :: False:True -> Cons:Nil:S:0' -> Cons:Nil:S:0' -> False:True
notEmpty :: Cons:Nil:S:0' -> False:True
strmatch :: Cons:Nil:S:0' -> Cons:Nil:S:0' -> Cons:Nil:S:0'
S :: Cons:Nil:S:0' -> Cons:Nil:S:0'
0' :: Cons:Nil:S:0'
hole_False:True1_0 :: False:True
hole_Cons:Nil:S:0'2_0 :: Cons:Nil:S:0'
gen_Cons:Nil:S:0'3_0 :: Nat -> Cons:Nil:S:0'


Generator Equations:
gen_Cons:Nil:S:0'3_0(0) <=> Nil
gen_Cons:Nil:S:0'3_0(+(x, 1)) <=> Cons(Nil, gen_Cons:Nil:S:0'3_0(x))


The following defined symbols remain to be analysed:
prefix, domatch, eqNatList

They will be analysed ascendingly in the following order:
prefix < domatch

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

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

(37)
BOUNDS(n^1, INF)

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

(38)
Obligation:
Innermost TRS:
Rules:
prefix(Cons(x', xs'), Cons(x, xs)) -> and(!EQ(x', x), prefix(xs', xs))
domatch(Cons(x, xs), Nil, n) -> Nil
domatch(Nil, Nil, n) -> Cons(n, Nil)
prefix(Cons(x, xs), Nil) -> False
prefix(Nil, cs) -> True
domatch(patcs, Cons(x, xs), n) -> domatch[Ite](prefix(patcs, Cons(x, xs)), patcs, Cons(x, xs), n)
eqNatList(Cons(x, xs), Cons(y, ys)) -> eqNatList[Ite](!EQ(x, y), ys, xs)
eqNatList(Cons(x, xs), Nil) -> False
eqNatList(Nil, Cons(y, ys)) -> False
eqNatList(Nil, Nil) -> True
notEmpty(Cons(x, xs)) -> True
notEmpty(Nil) -> False
strmatch(patstr, str) -> domatch(patstr, str, Nil)
and(False, False) -> False
and(True, False) -> False
and(False, True) -> False
and(True, True) -> True
!EQ(S(x), S(y)) -> !EQ(x, y)
!EQ(0', S(y)) -> False
!EQ(S(x), 0') -> False
!EQ(0', 0') -> True
domatch[Ite](False, patcs, Cons(x, xs), n) -> domatch(patcs, xs, Cons(n, Cons(Nil, Nil)))
domatch[Ite](True, patcs, Cons(x, xs), n) -> Cons(n, domatch(patcs, xs, Cons(n, Cons(Nil, Nil))))
eqNatList[Ite](False, ys, xs) -> False
eqNatList[Ite](True, ys, xs) -> eqNatList(xs, ys)

Types:
prefix :: Cons:Nil:S:0' -> Cons:Nil:S:0' -> False:True
Cons :: Cons:Nil:S:0' -> Cons:Nil:S:0' -> Cons:Nil:S:0'
and :: False:True -> False:True -> False:True
!EQ :: Cons:Nil:S:0' -> Cons:Nil:S:0' -> False:True
domatch :: Cons:Nil:S:0' -> Cons:Nil:S:0' -> Cons:Nil:S:0' -> Cons:Nil:S:0'
Nil :: Cons:Nil:S:0'
False :: False:True
True :: False:True
domatch[Ite] :: False:True -> Cons:Nil:S:0' -> Cons:Nil:S:0' -> Cons:Nil:S:0' -> Cons:Nil:S:0'
eqNatList :: Cons:Nil:S:0' -> Cons:Nil:S:0' -> False:True
eqNatList[Ite] :: False:True -> Cons:Nil:S:0' -> Cons:Nil:S:0' -> False:True
notEmpty :: Cons:Nil:S:0' -> False:True
strmatch :: Cons:Nil:S:0' -> Cons:Nil:S:0' -> Cons:Nil:S:0'
S :: Cons:Nil:S:0' -> Cons:Nil:S:0'
0' :: Cons:Nil:S:0'
hole_False:True1_0 :: False:True
hole_Cons:Nil:S:0'2_0 :: Cons:Nil:S:0'
gen_Cons:Nil:S:0'3_0 :: Nat -> Cons:Nil:S:0'


Lemmas:
prefix(gen_Cons:Nil:S:0'3_0(+(1, n20_0)), gen_Cons:Nil:S:0'3_0(+(1, n20_0))) -> *4_0, rt in Omega(n20_0)


Generator Equations:
gen_Cons:Nil:S:0'3_0(0) <=> Nil
gen_Cons:Nil:S:0'3_0(+(x, 1)) <=> Cons(Nil, gen_Cons:Nil:S:0'3_0(x))


The following defined symbols remain to be analysed:
domatch, eqNatList