WORST_CASE(NON_POLY,?)
proof of /export/starexec/sandbox/benchmark/theBenchmark.trs
# AProVE Commit ID: c69e44bd14796315568835c1ffa2502984884775 mhark 20210624 unpublished


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

(0) CpxRelTRS
(1) SInnermostTerminationProof [BOTH CONCRETE BOUNDS(ID, ID), 773 ms]
(2) CpxRelTRS
(3) RenamingProof [BOTH BOUNDS(ID, ID), 0 ms]
(4) CpxRelTRS
(5) SlicingProof [LOWER BOUND(ID), 0 ms]
(6) CpxRelTRS
(7) TypeInferenceProof [BOTH BOUNDS(ID, ID), 0 ms]
(8) typed CpxTrs
(9) OrderProof [LOWER BOUND(ID), 0 ms]
(10) typed CpxTrs
(11) RewriteLemmaProof [LOWER BOUND(ID), 233 ms]
(12) typed CpxTrs
(13) RewriteLemmaProof [FINISHED, 851 ms]
(14) BOUNDS(EXP, INF)


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

(0)
Obligation:
The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(EXP, 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
----------------------------------------

(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(EXP, 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
----------------------------------------

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

(4)
Obligation:
The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(EXP, 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
----------------------------------------

(5) SlicingProof (LOWER BOUND(ID))
Sliced the following arguments:
IF/1
rev1/0
rev1/1

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

(6)
Obligation:
The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(EXP, 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), z1), EMPTY(z1))
   IF(true, z1) -> c8
   IF(false, z1) -> c9(LAST(head(z1), tail(z1)), HEAD(z1))
   IF(false, 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, 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
----------------------------------------

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

(8)
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), z1), EMPTY(z1))
IF(true, z1) -> c8
IF(false, z1) -> c9(LAST(head(z1), tail(z1)), HEAD(z1))
IF(false, 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, 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 -> 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
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_c11:c1212_13 :: Nat -> c11:c12

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

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

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

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

(10)
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), z1), EMPTY(z1))
IF(true, z1) -> c8
IF(false, z1) -> c9(LAST(head(z1), tail(z1)), HEAD(z1))
IF(false, 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, 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 -> 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
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_c11:c1212_13 :: Nat -> c11:c12


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


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

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

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

(11) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
last(rev1, gen_nil:cons11_13(n14_13)) -> rev1, rt in Omega(0)

Induction Base:
last(rev1, gen_nil:cons11_13(0)) ->_R^Omega(0)
if(empty(gen_nil:cons11_13(0)), rev1, gen_nil:cons11_13(0)) ->_R^Omega(0)
if(true, rev1, gen_nil:cons11_13(0)) ->_R^Omega(0)
rev1

Induction Step:
last(rev1, gen_nil:cons11_13(+(n14_13, 1))) ->_R^Omega(0)
if(empty(gen_nil:cons11_13(+(n14_13, 1))), rev1, gen_nil:cons11_13(+(n14_13, 1))) ->_R^Omega(0)
if(false, rev1, gen_nil:cons11_13(+(1, n14_13))) ->_R^Omega(0)
last(head(gen_nil:cons11_13(+(1, n14_13))), tail(gen_nil:cons11_13(+(1, n14_13)))) ->_R^Omega(0)
last(rev1, tail(gen_nil:cons11_13(+(1, n14_13)))) ->_R^Omega(0)
last(rev1, gen_nil:cons11_13(n14_13)) ->_IH
rev1

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

(12)
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), z1), EMPTY(z1))
IF(true, z1) -> c8
IF(false, z1) -> c9(LAST(head(z1), tail(z1)), HEAD(z1))
IF(false, 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, 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 -> 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
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_c11:c1212_13 :: Nat -> c11:c12


Lemmas:
last(rev1, gen_nil:cons11_13(n14_13)) -> rev1, rt in Omega(0)


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


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

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

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

(13) RewriteLemmaProof (FINISHED)
Proved the following rewrite lemma:
rev2(rev1, gen_nil:cons11_13(n7604_13)) -> gen_nil:cons11_13(n7604_13), rt in Omega(EXP)

Induction Base:
rev2(rev1, gen_nil:cons11_13(0)) ->_R^Omega(0)
nil

Induction Step:
rev2(rev1, gen_nil:cons11_13(+(n7604_13, 1))) ->_R^Omega(0)
rev(cons(rev1, rev2(rev1, gen_nil:cons11_13(n7604_13)))) ->_IH
rev(cons(rev1, gen_nil:cons11_13(c7605_13))) ->_R^Omega(0)
cons(rev1, rev2(rev1, gen_nil:cons11_13(n7604_13))) ->_IH
cons(rev1, gen_nil:cons11_13(c7605_13))

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

(14)
BOUNDS(EXP, INF)