KILLED
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(1, INF).

(0) CpxRelTRS


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

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

   LE(0, z0) -> c
   LE(s(z0), 0) -> c1
   LE(s(z0), s(z1)) -> c2(LE(z0, z1))
   EQ(0, 0) -> c3
   EQ(0, s(z0)) -> c4
   EQ(s(z0), 0) -> c5
   EQ(s(z0), s(z1)) -> c6(EQ(z0, z1))
   IF(true, z0, z1) -> c7
   IF(false, z0, z1) -> c8
   MINSORT(nil) -> c9
   MINSORT(cons(z0, z1)) -> c10(MIN(z0, z1))
   MINSORT(cons(z0, z1)) -> c11(MINSORT(del(min(z0, z1), cons(z0, z1))), DEL(min(z0, z1), cons(z0, z1)), MIN(z0, z1))
   MIN(z0, nil) -> c12
   MIN(z0, cons(z1, z2)) -> c13(IF(le(z0, z1), min(z0, z2), min(z1, z2)), LE(z0, z1))
   MIN(z0, cons(z1, z2)) -> c14(IF(le(z0, z1), min(z0, z2), min(z1, z2)), MIN(z0, z2))
   MIN(z0, cons(z1, z2)) -> c15(IF(le(z0, z1), min(z0, z2), min(z1, z2)), MIN(z1, z2))
   DEL(z0, nil) -> c16
   DEL(z0, cons(z1, z2)) -> c17(IF(eq(z0, z1), z2, cons(z1, del(z0, z2))), EQ(z0, z1))
   DEL(z0, cons(z1, z2)) -> c18(IF(eq(z0, z1), z2, cons(z1, del(z0, z2))), DEL(z0, z2))

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

   le(0, z0) -> true
   le(s(z0), 0) -> false
   le(s(z0), s(z1)) -> le(z0, z1)
   eq(0, 0) -> true
   eq(0, s(z0)) -> false
   eq(s(z0), 0) -> false
   eq(s(z0), s(z1)) -> eq(z0, z1)
   if(true, z0, z1) -> z0
   if(false, z0, z1) -> z1
   minsort(nil) -> nil
   minsort(cons(z0, z1)) -> cons(min(z0, z1), minsort(del(min(z0, z1), cons(z0, z1))))
   min(z0, nil) -> z0
   min(z0, cons(z1, z2)) -> if(le(z0, z1), min(z0, z2), min(z1, z2))
   del(z0, nil) -> nil
   del(z0, cons(z1, z2)) -> if(eq(z0, z1), z2, cons(z1, del(z0, z2)))

Rewrite Strategy: INNERMOST