WORST_CASE(Omega(n^1),?)
proof of input_OMqDOzMaHU.trs
# AProVE Commit ID: aff8ecad908e01718a4c36e68d2e55d5e0f16e15 fuhs 20220216 unpublished


The Runtime Complexity (parallel-innermost) of the given CpxTRS could be proven to be BOUNDS(n^1, INF).

(0) CpxTRS
(1) CpxTrsToCdtProof [BOTH BOUNDS(ID, ID), 0 ms]
(2) CdtProblem
(3) CdtToCpxRelTrsProof [BOTH BOUNDS(ID, ID), 0 ms]
(4) CpxRelTRS
(5) RenamingProof [BOTH BOUNDS(ID, ID), 0 ms]
(6) CpxRelTRS
(7) TypeInferenceProof [BOTH BOUNDS(ID, ID), 0 ms]
(8) typed CpxTrs
(9) OrderProof [LOWER BOUND(ID), 15 ms]
(10) typed CpxTrs
(11) RewriteLemmaProof [LOWER BOUND(ID), 322 ms]
(12) typed CpxTrs
(13) RewriteLemmaProof [LOWER BOUND(ID), 165 ms]
(14) BEST
    (15) proven lower bound
        (16) LowerBoundPropagationProof [FINISHED, 0 ms]
        (17) BOUNDS(n^1, INF)
    (18) typed CpxTrs
        (19) RewriteLemmaProof [LOWER BOUND(ID), 68 ms]
        (20) typed CpxTrs
        (21) RewriteLemmaProof [LOWER BOUND(ID), 34 ms]
        (22) typed CpxTrs


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

(0)
Obligation:
The Runtime Complexity (parallel-innermost) of the given CpxTRS could be proven to be BOUNDS(n^1, INF).


The TRS R consists of the following rules:

   div(x, s(y)) -> d(x, s(y), 0)
   d(x, s(y), z) -> cond(ge(x, z), x, y, z)
   cond(true, x, y, z) -> s(d(x, s(y), plus(s(y), z)))
   cond(false, x, y, z) -> 0
   ge(u, 0) -> true
   ge(0, s(v)) -> false
   ge(s(u), s(v)) -> ge(u, v)
   plus(n, 0) -> n
   plus(n, s(m)) -> s(plus(n, m))

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

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

(2)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   div(z0, s(z1)) -> d(z0, s(z1), 0)
   d(z0, s(z1), z2) -> cond(ge(z0, z2), z0, z1, z2)
   cond(true, z0, z1, z2) -> s(d(z0, s(z1), plus(s(z1), z2)))
   cond(false, z0, z1, z2) -> 0
   ge(z0, 0) -> true
   ge(0, s(z0)) -> false
   ge(s(z0), s(z1)) -> ge(z0, z1)
   plus(z0, 0) -> z0
   plus(z0, s(z1)) -> s(plus(z0, z1))
Tuples:
   DIV(z0, s(z1)) -> c(D(z0, s(z1), 0))
   D(z0, s(z1), z2) -> c1(COND(ge(z0, z2), z0, z1, z2), GE(z0, z2))
   COND(true, z0, z1, z2) -> c2(D(z0, s(z1), plus(s(z1), z2)), PLUS(s(z1), z2))
   COND(false, z0, z1, z2) -> c3
   GE(z0, 0) -> c4
   GE(0, s(z0)) -> c5
   GE(s(z0), s(z1)) -> c6(GE(z0, z1))
   PLUS(z0, 0) -> c7
   PLUS(z0, s(z1)) -> c8(PLUS(z0, z1))
S tuples:
   DIV(z0, s(z1)) -> c(D(z0, s(z1), 0))
   D(z0, s(z1), z2) -> c1(COND(ge(z0, z2), z0, z1, z2), GE(z0, z2))
   COND(true, z0, z1, z2) -> c2(D(z0, s(z1), plus(s(z1), z2)), PLUS(s(z1), z2))
   COND(false, z0, z1, z2) -> c3
   GE(z0, 0) -> c4
   GE(0, s(z0)) -> c5
   GE(s(z0), s(z1)) -> c6(GE(z0, z1))
   PLUS(z0, 0) -> c7
   PLUS(z0, s(z1)) -> c8(PLUS(z0, z1))
K tuples:none
Defined Rule Symbols:   div_2, d_3, cond_4, ge_2, plus_2

Defined Pair Symbols:   DIV_2, D_3, COND_4, GE_2, PLUS_2

Compound Symbols:   c_1, c1_2, c2_2, c3, c4, c5, c6_1, c7, c8_1


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

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

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

   DIV(z0, s(z1)) -> c(D(z0, s(z1), 0))
   D(z0, s(z1), z2) -> c1(COND(ge(z0, z2), z0, z1, z2), GE(z0, z2))
   COND(true, z0, z1, z2) -> c2(D(z0, s(z1), plus(s(z1), z2)), PLUS(s(z1), z2))
   COND(false, z0, z1, z2) -> c3
   GE(z0, 0) -> c4
   GE(0, s(z0)) -> c5
   GE(s(z0), s(z1)) -> c6(GE(z0, z1))
   PLUS(z0, 0) -> c7
   PLUS(z0, s(z1)) -> c8(PLUS(z0, z1))

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

   div(z0, s(z1)) -> d(z0, s(z1), 0)
   d(z0, s(z1), z2) -> cond(ge(z0, z2), z0, z1, z2)
   cond(true, z0, z1, z2) -> s(d(z0, s(z1), plus(s(z1), z2)))
   cond(false, z0, z1, z2) -> 0
   ge(z0, 0) -> true
   ge(0, s(z0)) -> false
   ge(s(z0), s(z1)) -> ge(z0, z1)
   plus(z0, 0) -> z0
   plus(z0, s(z1)) -> s(plus(z0, z1))

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

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

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

   DIV(z0, s(z1)) -> c(D(z0, s(z1), 0'))
   D(z0, s(z1), z2) -> c1(COND(ge(z0, z2), z0, z1, z2), GE(z0, z2))
   COND(true, z0, z1, z2) -> c2(D(z0, s(z1), plus(s(z1), z2)), PLUS(s(z1), z2))
   COND(false, z0, z1, z2) -> c3
   GE(z0, 0') -> c4
   GE(0', s(z0)) -> c5
   GE(s(z0), s(z1)) -> c6(GE(z0, z1))
   PLUS(z0, 0') -> c7
   PLUS(z0, s(z1)) -> c8(PLUS(z0, z1))

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

   div(z0, s(z1)) -> d(z0, s(z1), 0')
   d(z0, s(z1), z2) -> cond(ge(z0, z2), z0, z1, z2)
   cond(true, z0, z1, z2) -> s(d(z0, s(z1), plus(s(z1), z2)))
   cond(false, z0, z1, z2) -> 0'
   ge(z0, 0') -> true
   ge(0', s(z0)) -> false
   ge(s(z0), s(z1)) -> ge(z0, z1)
   plus(z0, 0') -> z0
   plus(z0, s(z1)) -> s(plus(z0, z1))

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

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

(8)
Obligation:
Innermost TRS:
Rules:
DIV(z0, s(z1)) -> c(D(z0, s(z1), 0'))
D(z0, s(z1), z2) -> c1(COND(ge(z0, z2), z0, z1, z2), GE(z0, z2))
COND(true, z0, z1, z2) -> c2(D(z0, s(z1), plus(s(z1), z2)), PLUS(s(z1), z2))
COND(false, z0, z1, z2) -> c3
GE(z0, 0') -> c4
GE(0', s(z0)) -> c5
GE(s(z0), s(z1)) -> c6(GE(z0, z1))
PLUS(z0, 0') -> c7
PLUS(z0, s(z1)) -> c8(PLUS(z0, z1))
div(z0, s(z1)) -> d(z0, s(z1), 0')
d(z0, s(z1), z2) -> cond(ge(z0, z2), z0, z1, z2)
cond(true, z0, z1, z2) -> s(d(z0, s(z1), plus(s(z1), z2)))
cond(false, z0, z1, z2) -> 0'
ge(z0, 0') -> true
ge(0', s(z0)) -> false
ge(s(z0), s(z1)) -> ge(z0, z1)
plus(z0, 0') -> z0
plus(z0, s(z1)) -> s(plus(z0, z1))

Types:
DIV :: s:0' -> s:0' -> c
s :: s:0' -> s:0'
c :: c1 -> c
D :: s:0' -> s:0' -> s:0' -> c1
0' :: s:0'
c1 :: c2:c3 -> c4:c5:c6 -> c1
COND :: true:false -> s:0' -> s:0' -> s:0' -> c2:c3
ge :: s:0' -> s:0' -> true:false
GE :: s:0' -> s:0' -> c4:c5:c6
true :: true:false
c2 :: c1 -> c7:c8 -> c2:c3
plus :: s:0' -> s:0' -> s:0'
PLUS :: s:0' -> s:0' -> c7:c8
false :: true:false
c3 :: c2:c3
c4 :: c4:c5:c6
c5 :: c4:c5:c6
c6 :: c4:c5:c6 -> c4:c5:c6
c7 :: c7:c8
c8 :: c7:c8 -> c7:c8
div :: s:0' -> s:0' -> s:0'
d :: s:0' -> s:0' -> s:0' -> s:0'
cond :: true:false -> s:0' -> s:0' -> s:0' -> s:0'
hole_c1_9 :: c
hole_s:0'2_9 :: s:0'
hole_c13_9 :: c1
hole_c2:c34_9 :: c2:c3
hole_c4:c5:c65_9 :: c4:c5:c6
hole_true:false6_9 :: true:false
hole_c7:c87_9 :: c7:c8
gen_s:0'8_9 :: Nat -> s:0'
gen_c4:c5:c69_9 :: Nat -> c4:c5:c6
gen_c7:c810_9 :: Nat -> c7:c8

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

(9) OrderProof (LOWER BOUND(ID))
Heuristically decided to analyse the following defined symbols:
D, ge, GE, plus, PLUS, d

They will be analysed ascendingly in the following order:
ge < D
GE < D
plus < D
PLUS < D
ge < d
plus < d

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

(10)
Obligation:
Innermost TRS:
Rules:
DIV(z0, s(z1)) -> c(D(z0, s(z1), 0'))
D(z0, s(z1), z2) -> c1(COND(ge(z0, z2), z0, z1, z2), GE(z0, z2))
COND(true, z0, z1, z2) -> c2(D(z0, s(z1), plus(s(z1), z2)), PLUS(s(z1), z2))
COND(false, z0, z1, z2) -> c3
GE(z0, 0') -> c4
GE(0', s(z0)) -> c5
GE(s(z0), s(z1)) -> c6(GE(z0, z1))
PLUS(z0, 0') -> c7
PLUS(z0, s(z1)) -> c8(PLUS(z0, z1))
div(z0, s(z1)) -> d(z0, s(z1), 0')
d(z0, s(z1), z2) -> cond(ge(z0, z2), z0, z1, z2)
cond(true, z0, z1, z2) -> s(d(z0, s(z1), plus(s(z1), z2)))
cond(false, z0, z1, z2) -> 0'
ge(z0, 0') -> true
ge(0', s(z0)) -> false
ge(s(z0), s(z1)) -> ge(z0, z1)
plus(z0, 0') -> z0
plus(z0, s(z1)) -> s(plus(z0, z1))

Types:
DIV :: s:0' -> s:0' -> c
s :: s:0' -> s:0'
c :: c1 -> c
D :: s:0' -> s:0' -> s:0' -> c1
0' :: s:0'
c1 :: c2:c3 -> c4:c5:c6 -> c1
COND :: true:false -> s:0' -> s:0' -> s:0' -> c2:c3
ge :: s:0' -> s:0' -> true:false
GE :: s:0' -> s:0' -> c4:c5:c6
true :: true:false
c2 :: c1 -> c7:c8 -> c2:c3
plus :: s:0' -> s:0' -> s:0'
PLUS :: s:0' -> s:0' -> c7:c8
false :: true:false
c3 :: c2:c3
c4 :: c4:c5:c6
c5 :: c4:c5:c6
c6 :: c4:c5:c6 -> c4:c5:c6
c7 :: c7:c8
c8 :: c7:c8 -> c7:c8
div :: s:0' -> s:0' -> s:0'
d :: s:0' -> s:0' -> s:0' -> s:0'
cond :: true:false -> s:0' -> s:0' -> s:0' -> s:0'
hole_c1_9 :: c
hole_s:0'2_9 :: s:0'
hole_c13_9 :: c1
hole_c2:c34_9 :: c2:c3
hole_c4:c5:c65_9 :: c4:c5:c6
hole_true:false6_9 :: true:false
hole_c7:c87_9 :: c7:c8
gen_s:0'8_9 :: Nat -> s:0'
gen_c4:c5:c69_9 :: Nat -> c4:c5:c6
gen_c7:c810_9 :: Nat -> c7:c8


Generator Equations:
gen_s:0'8_9(0) <=> 0'
gen_s:0'8_9(+(x, 1)) <=> s(gen_s:0'8_9(x))
gen_c4:c5:c69_9(0) <=> c4
gen_c4:c5:c69_9(+(x, 1)) <=> c6(gen_c4:c5:c69_9(x))
gen_c7:c810_9(0) <=> c7
gen_c7:c810_9(+(x, 1)) <=> c8(gen_c7:c810_9(x))


The following defined symbols remain to be analysed:
ge, D, GE, plus, PLUS, d

They will be analysed ascendingly in the following order:
ge < D
GE < D
plus < D
PLUS < D
ge < d
plus < d

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

(11) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
ge(gen_s:0'8_9(n12_9), gen_s:0'8_9(n12_9)) -> true, rt in Omega(0)

Induction Base:
ge(gen_s:0'8_9(0), gen_s:0'8_9(0)) ->_R^Omega(0)
true

Induction Step:
ge(gen_s:0'8_9(+(n12_9, 1)), gen_s:0'8_9(+(n12_9, 1))) ->_R^Omega(0)
ge(gen_s:0'8_9(n12_9), gen_s:0'8_9(n12_9)) ->_IH
true

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:
DIV(z0, s(z1)) -> c(D(z0, s(z1), 0'))
D(z0, s(z1), z2) -> c1(COND(ge(z0, z2), z0, z1, z2), GE(z0, z2))
COND(true, z0, z1, z2) -> c2(D(z0, s(z1), plus(s(z1), z2)), PLUS(s(z1), z2))
COND(false, z0, z1, z2) -> c3
GE(z0, 0') -> c4
GE(0', s(z0)) -> c5
GE(s(z0), s(z1)) -> c6(GE(z0, z1))
PLUS(z0, 0') -> c7
PLUS(z0, s(z1)) -> c8(PLUS(z0, z1))
div(z0, s(z1)) -> d(z0, s(z1), 0')
d(z0, s(z1), z2) -> cond(ge(z0, z2), z0, z1, z2)
cond(true, z0, z1, z2) -> s(d(z0, s(z1), plus(s(z1), z2)))
cond(false, z0, z1, z2) -> 0'
ge(z0, 0') -> true
ge(0', s(z0)) -> false
ge(s(z0), s(z1)) -> ge(z0, z1)
plus(z0, 0') -> z0
plus(z0, s(z1)) -> s(plus(z0, z1))

Types:
DIV :: s:0' -> s:0' -> c
s :: s:0' -> s:0'
c :: c1 -> c
D :: s:0' -> s:0' -> s:0' -> c1
0' :: s:0'
c1 :: c2:c3 -> c4:c5:c6 -> c1
COND :: true:false -> s:0' -> s:0' -> s:0' -> c2:c3
ge :: s:0' -> s:0' -> true:false
GE :: s:0' -> s:0' -> c4:c5:c6
true :: true:false
c2 :: c1 -> c7:c8 -> c2:c3
plus :: s:0' -> s:0' -> s:0'
PLUS :: s:0' -> s:0' -> c7:c8
false :: true:false
c3 :: c2:c3
c4 :: c4:c5:c6
c5 :: c4:c5:c6
c6 :: c4:c5:c6 -> c4:c5:c6
c7 :: c7:c8
c8 :: c7:c8 -> c7:c8
div :: s:0' -> s:0' -> s:0'
d :: s:0' -> s:0' -> s:0' -> s:0'
cond :: true:false -> s:0' -> s:0' -> s:0' -> s:0'
hole_c1_9 :: c
hole_s:0'2_9 :: s:0'
hole_c13_9 :: c1
hole_c2:c34_9 :: c2:c3
hole_c4:c5:c65_9 :: c4:c5:c6
hole_true:false6_9 :: true:false
hole_c7:c87_9 :: c7:c8
gen_s:0'8_9 :: Nat -> s:0'
gen_c4:c5:c69_9 :: Nat -> c4:c5:c6
gen_c7:c810_9 :: Nat -> c7:c8


Lemmas:
ge(gen_s:0'8_9(n12_9), gen_s:0'8_9(n12_9)) -> true, rt in Omega(0)


Generator Equations:
gen_s:0'8_9(0) <=> 0'
gen_s:0'8_9(+(x, 1)) <=> s(gen_s:0'8_9(x))
gen_c4:c5:c69_9(0) <=> c4
gen_c4:c5:c69_9(+(x, 1)) <=> c6(gen_c4:c5:c69_9(x))
gen_c7:c810_9(0) <=> c7
gen_c7:c810_9(+(x, 1)) <=> c8(gen_c7:c810_9(x))


The following defined symbols remain to be analysed:
GE, D, plus, PLUS, d

They will be analysed ascendingly in the following order:
GE < D
plus < D
PLUS < D
plus < d

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

(13) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
GE(gen_s:0'8_9(n350_9), gen_s:0'8_9(n350_9)) -> gen_c4:c5:c69_9(n350_9), rt in Omega(1 + n350_9)

Induction Base:
GE(gen_s:0'8_9(0), gen_s:0'8_9(0)) ->_R^Omega(1)
c4

Induction Step:
GE(gen_s:0'8_9(+(n350_9, 1)), gen_s:0'8_9(+(n350_9, 1))) ->_R^Omega(1)
c6(GE(gen_s:0'8_9(n350_9), gen_s:0'8_9(n350_9))) ->_IH
c6(gen_c4:c5:c69_9(c351_9))

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

(14)
Complex Obligation (BEST)

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

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

Innermost TRS:
Rules:
DIV(z0, s(z1)) -> c(D(z0, s(z1), 0'))
D(z0, s(z1), z2) -> c1(COND(ge(z0, z2), z0, z1, z2), GE(z0, z2))
COND(true, z0, z1, z2) -> c2(D(z0, s(z1), plus(s(z1), z2)), PLUS(s(z1), z2))
COND(false, z0, z1, z2) -> c3
GE(z0, 0') -> c4
GE(0', s(z0)) -> c5
GE(s(z0), s(z1)) -> c6(GE(z0, z1))
PLUS(z0, 0') -> c7
PLUS(z0, s(z1)) -> c8(PLUS(z0, z1))
div(z0, s(z1)) -> d(z0, s(z1), 0')
d(z0, s(z1), z2) -> cond(ge(z0, z2), z0, z1, z2)
cond(true, z0, z1, z2) -> s(d(z0, s(z1), plus(s(z1), z2)))
cond(false, z0, z1, z2) -> 0'
ge(z0, 0') -> true
ge(0', s(z0)) -> false
ge(s(z0), s(z1)) -> ge(z0, z1)
plus(z0, 0') -> z0
plus(z0, s(z1)) -> s(plus(z0, z1))

Types:
DIV :: s:0' -> s:0' -> c
s :: s:0' -> s:0'
c :: c1 -> c
D :: s:0' -> s:0' -> s:0' -> c1
0' :: s:0'
c1 :: c2:c3 -> c4:c5:c6 -> c1
COND :: true:false -> s:0' -> s:0' -> s:0' -> c2:c3
ge :: s:0' -> s:0' -> true:false
GE :: s:0' -> s:0' -> c4:c5:c6
true :: true:false
c2 :: c1 -> c7:c8 -> c2:c3
plus :: s:0' -> s:0' -> s:0'
PLUS :: s:0' -> s:0' -> c7:c8
false :: true:false
c3 :: c2:c3
c4 :: c4:c5:c6
c5 :: c4:c5:c6
c6 :: c4:c5:c6 -> c4:c5:c6
c7 :: c7:c8
c8 :: c7:c8 -> c7:c8
div :: s:0' -> s:0' -> s:0'
d :: s:0' -> s:0' -> s:0' -> s:0'
cond :: true:false -> s:0' -> s:0' -> s:0' -> s:0'
hole_c1_9 :: c
hole_s:0'2_9 :: s:0'
hole_c13_9 :: c1
hole_c2:c34_9 :: c2:c3
hole_c4:c5:c65_9 :: c4:c5:c6
hole_true:false6_9 :: true:false
hole_c7:c87_9 :: c7:c8
gen_s:0'8_9 :: Nat -> s:0'
gen_c4:c5:c69_9 :: Nat -> c4:c5:c6
gen_c7:c810_9 :: Nat -> c7:c8


Lemmas:
ge(gen_s:0'8_9(n12_9), gen_s:0'8_9(n12_9)) -> true, rt in Omega(0)


Generator Equations:
gen_s:0'8_9(0) <=> 0'
gen_s:0'8_9(+(x, 1)) <=> s(gen_s:0'8_9(x))
gen_c4:c5:c69_9(0) <=> c4
gen_c4:c5:c69_9(+(x, 1)) <=> c6(gen_c4:c5:c69_9(x))
gen_c7:c810_9(0) <=> c7
gen_c7:c810_9(+(x, 1)) <=> c8(gen_c7:c810_9(x))


The following defined symbols remain to be analysed:
GE, D, plus, PLUS, d

They will be analysed ascendingly in the following order:
GE < D
plus < D
PLUS < D
plus < d

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

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

(17)
BOUNDS(n^1, INF)

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

(18)
Obligation:
Innermost TRS:
Rules:
DIV(z0, s(z1)) -> c(D(z0, s(z1), 0'))
D(z0, s(z1), z2) -> c1(COND(ge(z0, z2), z0, z1, z2), GE(z0, z2))
COND(true, z0, z1, z2) -> c2(D(z0, s(z1), plus(s(z1), z2)), PLUS(s(z1), z2))
COND(false, z0, z1, z2) -> c3
GE(z0, 0') -> c4
GE(0', s(z0)) -> c5
GE(s(z0), s(z1)) -> c6(GE(z0, z1))
PLUS(z0, 0') -> c7
PLUS(z0, s(z1)) -> c8(PLUS(z0, z1))
div(z0, s(z1)) -> d(z0, s(z1), 0')
d(z0, s(z1), z2) -> cond(ge(z0, z2), z0, z1, z2)
cond(true, z0, z1, z2) -> s(d(z0, s(z1), plus(s(z1), z2)))
cond(false, z0, z1, z2) -> 0'
ge(z0, 0') -> true
ge(0', s(z0)) -> false
ge(s(z0), s(z1)) -> ge(z0, z1)
plus(z0, 0') -> z0
plus(z0, s(z1)) -> s(plus(z0, z1))

Types:
DIV :: s:0' -> s:0' -> c
s :: s:0' -> s:0'
c :: c1 -> c
D :: s:0' -> s:0' -> s:0' -> c1
0' :: s:0'
c1 :: c2:c3 -> c4:c5:c6 -> c1
COND :: true:false -> s:0' -> s:0' -> s:0' -> c2:c3
ge :: s:0' -> s:0' -> true:false
GE :: s:0' -> s:0' -> c4:c5:c6
true :: true:false
c2 :: c1 -> c7:c8 -> c2:c3
plus :: s:0' -> s:0' -> s:0'
PLUS :: s:0' -> s:0' -> c7:c8
false :: true:false
c3 :: c2:c3
c4 :: c4:c5:c6
c5 :: c4:c5:c6
c6 :: c4:c5:c6 -> c4:c5:c6
c7 :: c7:c8
c8 :: c7:c8 -> c7:c8
div :: s:0' -> s:0' -> s:0'
d :: s:0' -> s:0' -> s:0' -> s:0'
cond :: true:false -> s:0' -> s:0' -> s:0' -> s:0'
hole_c1_9 :: c
hole_s:0'2_9 :: s:0'
hole_c13_9 :: c1
hole_c2:c34_9 :: c2:c3
hole_c4:c5:c65_9 :: c4:c5:c6
hole_true:false6_9 :: true:false
hole_c7:c87_9 :: c7:c8
gen_s:0'8_9 :: Nat -> s:0'
gen_c4:c5:c69_9 :: Nat -> c4:c5:c6
gen_c7:c810_9 :: Nat -> c7:c8


Lemmas:
ge(gen_s:0'8_9(n12_9), gen_s:0'8_9(n12_9)) -> true, rt in Omega(0)
GE(gen_s:0'8_9(n350_9), gen_s:0'8_9(n350_9)) -> gen_c4:c5:c69_9(n350_9), rt in Omega(1 + n350_9)


Generator Equations:
gen_s:0'8_9(0) <=> 0'
gen_s:0'8_9(+(x, 1)) <=> s(gen_s:0'8_9(x))
gen_c4:c5:c69_9(0) <=> c4
gen_c4:c5:c69_9(+(x, 1)) <=> c6(gen_c4:c5:c69_9(x))
gen_c7:c810_9(0) <=> c7
gen_c7:c810_9(+(x, 1)) <=> c8(gen_c7:c810_9(x))


The following defined symbols remain to be analysed:
plus, D, PLUS, d

They will be analysed ascendingly in the following order:
plus < D
PLUS < D
plus < d

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

(19) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
plus(gen_s:0'8_9(a), gen_s:0'8_9(n948_9)) -> gen_s:0'8_9(+(n948_9, a)), rt in Omega(0)

Induction Base:
plus(gen_s:0'8_9(a), gen_s:0'8_9(0)) ->_R^Omega(0)
gen_s:0'8_9(a)

Induction Step:
plus(gen_s:0'8_9(a), gen_s:0'8_9(+(n948_9, 1))) ->_R^Omega(0)
s(plus(gen_s:0'8_9(a), gen_s:0'8_9(n948_9))) ->_IH
s(gen_s:0'8_9(+(a, c949_9)))

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

(20)
Obligation:
Innermost TRS:
Rules:
DIV(z0, s(z1)) -> c(D(z0, s(z1), 0'))
D(z0, s(z1), z2) -> c1(COND(ge(z0, z2), z0, z1, z2), GE(z0, z2))
COND(true, z0, z1, z2) -> c2(D(z0, s(z1), plus(s(z1), z2)), PLUS(s(z1), z2))
COND(false, z0, z1, z2) -> c3
GE(z0, 0') -> c4
GE(0', s(z0)) -> c5
GE(s(z0), s(z1)) -> c6(GE(z0, z1))
PLUS(z0, 0') -> c7
PLUS(z0, s(z1)) -> c8(PLUS(z0, z1))
div(z0, s(z1)) -> d(z0, s(z1), 0')
d(z0, s(z1), z2) -> cond(ge(z0, z2), z0, z1, z2)
cond(true, z0, z1, z2) -> s(d(z0, s(z1), plus(s(z1), z2)))
cond(false, z0, z1, z2) -> 0'
ge(z0, 0') -> true
ge(0', s(z0)) -> false
ge(s(z0), s(z1)) -> ge(z0, z1)
plus(z0, 0') -> z0
plus(z0, s(z1)) -> s(plus(z0, z1))

Types:
DIV :: s:0' -> s:0' -> c
s :: s:0' -> s:0'
c :: c1 -> c
D :: s:0' -> s:0' -> s:0' -> c1
0' :: s:0'
c1 :: c2:c3 -> c4:c5:c6 -> c1
COND :: true:false -> s:0' -> s:0' -> s:0' -> c2:c3
ge :: s:0' -> s:0' -> true:false
GE :: s:0' -> s:0' -> c4:c5:c6
true :: true:false
c2 :: c1 -> c7:c8 -> c2:c3
plus :: s:0' -> s:0' -> s:0'
PLUS :: s:0' -> s:0' -> c7:c8
false :: true:false
c3 :: c2:c3
c4 :: c4:c5:c6
c5 :: c4:c5:c6
c6 :: c4:c5:c6 -> c4:c5:c6
c7 :: c7:c8
c8 :: c7:c8 -> c7:c8
div :: s:0' -> s:0' -> s:0'
d :: s:0' -> s:0' -> s:0' -> s:0'
cond :: true:false -> s:0' -> s:0' -> s:0' -> s:0'
hole_c1_9 :: c
hole_s:0'2_9 :: s:0'
hole_c13_9 :: c1
hole_c2:c34_9 :: c2:c3
hole_c4:c5:c65_9 :: c4:c5:c6
hole_true:false6_9 :: true:false
hole_c7:c87_9 :: c7:c8
gen_s:0'8_9 :: Nat -> s:0'
gen_c4:c5:c69_9 :: Nat -> c4:c5:c6
gen_c7:c810_9 :: Nat -> c7:c8


Lemmas:
ge(gen_s:0'8_9(n12_9), gen_s:0'8_9(n12_9)) -> true, rt in Omega(0)
GE(gen_s:0'8_9(n350_9), gen_s:0'8_9(n350_9)) -> gen_c4:c5:c69_9(n350_9), rt in Omega(1 + n350_9)
plus(gen_s:0'8_9(a), gen_s:0'8_9(n948_9)) -> gen_s:0'8_9(+(n948_9, a)), rt in Omega(0)


Generator Equations:
gen_s:0'8_9(0) <=> 0'
gen_s:0'8_9(+(x, 1)) <=> s(gen_s:0'8_9(x))
gen_c4:c5:c69_9(0) <=> c4
gen_c4:c5:c69_9(+(x, 1)) <=> c6(gen_c4:c5:c69_9(x))
gen_c7:c810_9(0) <=> c7
gen_c7:c810_9(+(x, 1)) <=> c8(gen_c7:c810_9(x))


The following defined symbols remain to be analysed:
PLUS, D, d

They will be analysed ascendingly in the following order:
PLUS < D

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

(21) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
PLUS(gen_s:0'8_9(a), gen_s:0'8_9(n1887_9)) -> gen_c7:c810_9(n1887_9), rt in Omega(1 + n1887_9)

Induction Base:
PLUS(gen_s:0'8_9(a), gen_s:0'8_9(0)) ->_R^Omega(1)
c7

Induction Step:
PLUS(gen_s:0'8_9(a), gen_s:0'8_9(+(n1887_9, 1))) ->_R^Omega(1)
c8(PLUS(gen_s:0'8_9(a), gen_s:0'8_9(n1887_9))) ->_IH
c8(gen_c7:c810_9(c1888_9))

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

(22)
Obligation:
Innermost TRS:
Rules:
DIV(z0, s(z1)) -> c(D(z0, s(z1), 0'))
D(z0, s(z1), z2) -> c1(COND(ge(z0, z2), z0, z1, z2), GE(z0, z2))
COND(true, z0, z1, z2) -> c2(D(z0, s(z1), plus(s(z1), z2)), PLUS(s(z1), z2))
COND(false, z0, z1, z2) -> c3
GE(z0, 0') -> c4
GE(0', s(z0)) -> c5
GE(s(z0), s(z1)) -> c6(GE(z0, z1))
PLUS(z0, 0') -> c7
PLUS(z0, s(z1)) -> c8(PLUS(z0, z1))
div(z0, s(z1)) -> d(z0, s(z1), 0')
d(z0, s(z1), z2) -> cond(ge(z0, z2), z0, z1, z2)
cond(true, z0, z1, z2) -> s(d(z0, s(z1), plus(s(z1), z2)))
cond(false, z0, z1, z2) -> 0'
ge(z0, 0') -> true
ge(0', s(z0)) -> false
ge(s(z0), s(z1)) -> ge(z0, z1)
plus(z0, 0') -> z0
plus(z0, s(z1)) -> s(plus(z0, z1))

Types:
DIV :: s:0' -> s:0' -> c
s :: s:0' -> s:0'
c :: c1 -> c
D :: s:0' -> s:0' -> s:0' -> c1
0' :: s:0'
c1 :: c2:c3 -> c4:c5:c6 -> c1
COND :: true:false -> s:0' -> s:0' -> s:0' -> c2:c3
ge :: s:0' -> s:0' -> true:false
GE :: s:0' -> s:0' -> c4:c5:c6
true :: true:false
c2 :: c1 -> c7:c8 -> c2:c3
plus :: s:0' -> s:0' -> s:0'
PLUS :: s:0' -> s:0' -> c7:c8
false :: true:false
c3 :: c2:c3
c4 :: c4:c5:c6
c5 :: c4:c5:c6
c6 :: c4:c5:c6 -> c4:c5:c6
c7 :: c7:c8
c8 :: c7:c8 -> c7:c8
div :: s:0' -> s:0' -> s:0'
d :: s:0' -> s:0' -> s:0' -> s:0'
cond :: true:false -> s:0' -> s:0' -> s:0' -> s:0'
hole_c1_9 :: c
hole_s:0'2_9 :: s:0'
hole_c13_9 :: c1
hole_c2:c34_9 :: c2:c3
hole_c4:c5:c65_9 :: c4:c5:c6
hole_true:false6_9 :: true:false
hole_c7:c87_9 :: c7:c8
gen_s:0'8_9 :: Nat -> s:0'
gen_c4:c5:c69_9 :: Nat -> c4:c5:c6
gen_c7:c810_9 :: Nat -> c7:c8


Lemmas:
ge(gen_s:0'8_9(n12_9), gen_s:0'8_9(n12_9)) -> true, rt in Omega(0)
GE(gen_s:0'8_9(n350_9), gen_s:0'8_9(n350_9)) -> gen_c4:c5:c69_9(n350_9), rt in Omega(1 + n350_9)
plus(gen_s:0'8_9(a), gen_s:0'8_9(n948_9)) -> gen_s:0'8_9(+(n948_9, a)), rt in Omega(0)
PLUS(gen_s:0'8_9(a), gen_s:0'8_9(n1887_9)) -> gen_c7:c810_9(n1887_9), rt in Omega(1 + n1887_9)


Generator Equations:
gen_s:0'8_9(0) <=> 0'
gen_s:0'8_9(+(x, 1)) <=> s(gen_s:0'8_9(x))
gen_c4:c5:c69_9(0) <=> c4
gen_c4:c5:c69_9(+(x, 1)) <=> c6(gen_c4:c5:c69_9(x))
gen_c7:c810_9(0) <=> c7
gen_c7:c810_9(+(x, 1)) <=> c8(gen_c7:c810_9(x))


The following defined symbols remain to be analysed:
D, d