D(t) → s(h)
D(constant) → h
D(b(x, y)) → b(D(x), D(y))
D(c(x, y)) → b(c(y, D(x)), c(x, D(y)))
D(m(x, y)) → m(D(x), D(y))
D(opp(x)) → opp(D(x))
D(div(x, y)) → m(div(D(x), y), div(c(x, D(y)), pow(y, 2)))
D(ln(x)) → div(D(x), x)
D(pow(x, y)) → b(c(c(y, pow(x, m(y, 1))), D(x)), c(c(pow(x, y), ln(x)), D(y)))
b(h, x) → x
b(x, h) → x
b(s(x), s(y)) → s(s(b(x, y)))
b(b(x, y), z) → b(x, b(y, z))
Renamed function symbols to avoid clashes with predefined symbol.
Runtime Complexity TRS:
The TRS R consists of the following rules:
D'(t') → s'(h')
D'(constant') → h'
D'(b'(x, y)) → b'(D'(x), D'(y))
D'(c'(x, y)) → b'(c'(y, D'(x)), c'(x, D'(y)))
D'(m'(x, y)) → m'(D'(x), D'(y))
D'(opp'(x)) → opp'(D'(x))
D'(div'(x, y)) → m'(div'(D'(x), y), div'(c'(x, D'(y)), pow'(y, 2')))
D'(ln'(x)) → div'(D'(x), x)
D'(pow'(x, y)) → b'(c'(c'(y, pow'(x, m'(y, 1'))), D'(x)), c'(c'(pow'(x, y), ln'(x)), D'(y)))
b'(h', x) → x
b'(x, h') → x
b'(s'(x), s'(y)) → s'(s'(b'(x, y)))
b'(b'(x, y), z) → b'(x, b'(y, z))
Infered types.
Rules:
D'(t') → s'(h')
D'(constant') → h'
D'(b'(x, y)) → b'(D'(x), D'(y))
D'(c'(x, y)) → b'(c'(y, D'(x)), c'(x, D'(y)))
D'(m'(x, y)) → m'(D'(x), D'(y))
D'(opp'(x)) → opp'(D'(x))
D'(div'(x, y)) → m'(div'(D'(x), y), div'(c'(x, D'(y)), pow'(y, 2')))
D'(ln'(x)) → div'(D'(x), x)
D'(pow'(x, y)) → b'(c'(c'(y, pow'(x, m'(y, 1'))), D'(x)), c'(c'(pow'(x, y), ln'(x)), D'(y)))
b'(h', x) → x
b'(x, h') → x
b'(s'(x), s'(y)) → s'(s'(b'(x, y)))
b'(b'(x, y), z) → b'(x, b'(y, z))
Types:
D' :: t':h':s':constant':c':m':opp':div':2':pow':ln':1' → t':h':s':constant':c':m':opp':div':2':pow':ln':1'
t' :: t':h':s':constant':c':m':opp':div':2':pow':ln':1'
s' :: t':h':s':constant':c':m':opp':div':2':pow':ln':1' → t':h':s':constant':c':m':opp':div':2':pow':ln':1'
h' :: t':h':s':constant':c':m':opp':div':2':pow':ln':1'
constant' :: t':h':s':constant':c':m':opp':div':2':pow':ln':1'
b' :: t':h':s':constant':c':m':opp':div':2':pow':ln':1' → t':h':s':constant':c':m':opp':div':2':pow':ln':1' → t':h':s':constant':c':m':opp':div':2':pow':ln':1'
c' :: t':h':s':constant':c':m':opp':div':2':pow':ln':1' → t':h':s':constant':c':m':opp':div':2':pow':ln':1' → t':h':s':constant':c':m':opp':div':2':pow':ln':1'
m' :: t':h':s':constant':c':m':opp':div':2':pow':ln':1' → t':h':s':constant':c':m':opp':div':2':pow':ln':1' → t':h':s':constant':c':m':opp':div':2':pow':ln':1'
opp' :: t':h':s':constant':c':m':opp':div':2':pow':ln':1' → t':h':s':constant':c':m':opp':div':2':pow':ln':1'
div' :: t':h':s':constant':c':m':opp':div':2':pow':ln':1' → t':h':s':constant':c':m':opp':div':2':pow':ln':1' → t':h':s':constant':c':m':opp':div':2':pow':ln':1'
pow' :: t':h':s':constant':c':m':opp':div':2':pow':ln':1' → t':h':s':constant':c':m':opp':div':2':pow':ln':1' → t':h':s':constant':c':m':opp':div':2':pow':ln':1'
2' :: t':h':s':constant':c':m':opp':div':2':pow':ln':1'
ln' :: t':h':s':constant':c':m':opp':div':2':pow':ln':1' → t':h':s':constant':c':m':opp':div':2':pow':ln':1'
1' :: t':h':s':constant':c':m':opp':div':2':pow':ln':1'
_hole_t':h':s':constant':c':m':opp':div':2':pow':ln':1'1 :: t':h':s':constant':c':m':opp':div':2':pow':ln':1'
_gen_t':h':s':constant':c':m':opp':div':2':pow':ln':1'2 :: Nat → t':h':s':constant':c':m':opp':div':2':pow':ln':1'
Heuristically decided to analyse the following defined symbols:
D', b'
They will be analysed ascendingly in the following order:
b' < D'
Rules:
D'(t') → s'(h')
D'(constant') → h'
D'(b'(x, y)) → b'(D'(x), D'(y))
D'(c'(x, y)) → b'(c'(y, D'(x)), c'(x, D'(y)))
D'(m'(x, y)) → m'(D'(x), D'(y))
D'(opp'(x)) → opp'(D'(x))
D'(div'(x, y)) → m'(div'(D'(x), y), div'(c'(x, D'(y)), pow'(y, 2')))
D'(ln'(x)) → div'(D'(x), x)
D'(pow'(x, y)) → b'(c'(c'(y, pow'(x, m'(y, 1'))), D'(x)), c'(c'(pow'(x, y), ln'(x)), D'(y)))
b'(h', x) → x
b'(x, h') → x
b'(s'(x), s'(y)) → s'(s'(b'(x, y)))
b'(b'(x, y), z) → b'(x, b'(y, z))
Types:
D' :: t':h':s':constant':c':m':opp':div':2':pow':ln':1' → t':h':s':constant':c':m':opp':div':2':pow':ln':1'
t' :: t':h':s':constant':c':m':opp':div':2':pow':ln':1'
s' :: t':h':s':constant':c':m':opp':div':2':pow':ln':1' → t':h':s':constant':c':m':opp':div':2':pow':ln':1'
h' :: t':h':s':constant':c':m':opp':div':2':pow':ln':1'
constant' :: t':h':s':constant':c':m':opp':div':2':pow':ln':1'
b' :: t':h':s':constant':c':m':opp':div':2':pow':ln':1' → t':h':s':constant':c':m':opp':div':2':pow':ln':1' → t':h':s':constant':c':m':opp':div':2':pow':ln':1'
c' :: t':h':s':constant':c':m':opp':div':2':pow':ln':1' → t':h':s':constant':c':m':opp':div':2':pow':ln':1' → t':h':s':constant':c':m':opp':div':2':pow':ln':1'
m' :: t':h':s':constant':c':m':opp':div':2':pow':ln':1' → t':h':s':constant':c':m':opp':div':2':pow':ln':1' → t':h':s':constant':c':m':opp':div':2':pow':ln':1'
opp' :: t':h':s':constant':c':m':opp':div':2':pow':ln':1' → t':h':s':constant':c':m':opp':div':2':pow':ln':1'
div' :: t':h':s':constant':c':m':opp':div':2':pow':ln':1' → t':h':s':constant':c':m':opp':div':2':pow':ln':1' → t':h':s':constant':c':m':opp':div':2':pow':ln':1'
pow' :: t':h':s':constant':c':m':opp':div':2':pow':ln':1' → t':h':s':constant':c':m':opp':div':2':pow':ln':1' → t':h':s':constant':c':m':opp':div':2':pow':ln':1'
2' :: t':h':s':constant':c':m':opp':div':2':pow':ln':1'
ln' :: t':h':s':constant':c':m':opp':div':2':pow':ln':1' → t':h':s':constant':c':m':opp':div':2':pow':ln':1'
1' :: t':h':s':constant':c':m':opp':div':2':pow':ln':1'
_hole_t':h':s':constant':c':m':opp':div':2':pow':ln':1'1 :: t':h':s':constant':c':m':opp':div':2':pow':ln':1'
_gen_t':h':s':constant':c':m':opp':div':2':pow':ln':1'2 :: Nat → t':h':s':constant':c':m':opp':div':2':pow':ln':1'
Generator Equations:
_gen_t':h':s':constant':c':m':opp':div':2':pow':ln':1'2(0) ⇔ t'
_gen_t':h':s':constant':c':m':opp':div':2':pow':ln':1'2(+(x, 1)) ⇔ s'(_gen_t':h':s':constant':c':m':opp':div':2':pow':ln':1'2(x))
The following defined symbols remain to be analysed:
b', D'
They will be analysed ascendingly in the following order:
b' < D'
Proved the following rewrite lemma:
b'(_gen_t':h':s':constant':c':m':opp':div':2':pow':ln':1'2(+(1, _n4)), _gen_t':h':s':constant':c':m':opp':div':2':pow':ln':1'2(+(1, _n4))) → _*3, rt ∈ Ω(n4)
Induction Base:
b'(_gen_t':h':s':constant':c':m':opp':div':2':pow':ln':1'2(+(1, 0)), _gen_t':h':s':constant':c':m':opp':div':2':pow':ln':1'2(+(1, 0)))
Induction Step:
b'(_gen_t':h':s':constant':c':m':opp':div':2':pow':ln':1'2(+(1, +(_$n5, 1))), _gen_t':h':s':constant':c':m':opp':div':2':pow':ln':1'2(+(1, +(_$n5, 1)))) →RΩ(1)
s'(s'(b'(_gen_t':h':s':constant':c':m':opp':div':2':pow':ln':1'2(+(1, _$n5)), _gen_t':h':s':constant':c':m':opp':div':2':pow':ln':1'2(+(1, _$n5))))) →IH
s'(s'(_*3))
We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).
Rules:
D'(t') → s'(h')
D'(constant') → h'
D'(b'(x, y)) → b'(D'(x), D'(y))
D'(c'(x, y)) → b'(c'(y, D'(x)), c'(x, D'(y)))
D'(m'(x, y)) → m'(D'(x), D'(y))
D'(opp'(x)) → opp'(D'(x))
D'(div'(x, y)) → m'(div'(D'(x), y), div'(c'(x, D'(y)), pow'(y, 2')))
D'(ln'(x)) → div'(D'(x), x)
D'(pow'(x, y)) → b'(c'(c'(y, pow'(x, m'(y, 1'))), D'(x)), c'(c'(pow'(x, y), ln'(x)), D'(y)))
b'(h', x) → x
b'(x, h') → x
b'(s'(x), s'(y)) → s'(s'(b'(x, y)))
b'(b'(x, y), z) → b'(x, b'(y, z))
Types:
D' :: t':h':s':constant':c':m':opp':div':2':pow':ln':1' → t':h':s':constant':c':m':opp':div':2':pow':ln':1'
t' :: t':h':s':constant':c':m':opp':div':2':pow':ln':1'
s' :: t':h':s':constant':c':m':opp':div':2':pow':ln':1' → t':h':s':constant':c':m':opp':div':2':pow':ln':1'
h' :: t':h':s':constant':c':m':opp':div':2':pow':ln':1'
constant' :: t':h':s':constant':c':m':opp':div':2':pow':ln':1'
b' :: t':h':s':constant':c':m':opp':div':2':pow':ln':1' → t':h':s':constant':c':m':opp':div':2':pow':ln':1' → t':h':s':constant':c':m':opp':div':2':pow':ln':1'
c' :: t':h':s':constant':c':m':opp':div':2':pow':ln':1' → t':h':s':constant':c':m':opp':div':2':pow':ln':1' → t':h':s':constant':c':m':opp':div':2':pow':ln':1'
m' :: t':h':s':constant':c':m':opp':div':2':pow':ln':1' → t':h':s':constant':c':m':opp':div':2':pow':ln':1' → t':h':s':constant':c':m':opp':div':2':pow':ln':1'
opp' :: t':h':s':constant':c':m':opp':div':2':pow':ln':1' → t':h':s':constant':c':m':opp':div':2':pow':ln':1'
div' :: t':h':s':constant':c':m':opp':div':2':pow':ln':1' → t':h':s':constant':c':m':opp':div':2':pow':ln':1' → t':h':s':constant':c':m':opp':div':2':pow':ln':1'
pow' :: t':h':s':constant':c':m':opp':div':2':pow':ln':1' → t':h':s':constant':c':m':opp':div':2':pow':ln':1' → t':h':s':constant':c':m':opp':div':2':pow':ln':1'
2' :: t':h':s':constant':c':m':opp':div':2':pow':ln':1'
ln' :: t':h':s':constant':c':m':opp':div':2':pow':ln':1' → t':h':s':constant':c':m':opp':div':2':pow':ln':1'
1' :: t':h':s':constant':c':m':opp':div':2':pow':ln':1'
_hole_t':h':s':constant':c':m':opp':div':2':pow':ln':1'1 :: t':h':s':constant':c':m':opp':div':2':pow':ln':1'
_gen_t':h':s':constant':c':m':opp':div':2':pow':ln':1'2 :: Nat → t':h':s':constant':c':m':opp':div':2':pow':ln':1'
Lemmas:
b'(_gen_t':h':s':constant':c':m':opp':div':2':pow':ln':1'2(+(1, _n4)), _gen_t':h':s':constant':c':m':opp':div':2':pow':ln':1'2(+(1, _n4))) → _*3, rt ∈ Ω(n4)
Generator Equations:
_gen_t':h':s':constant':c':m':opp':div':2':pow':ln':1'2(0) ⇔ t'
_gen_t':h':s':constant':c':m':opp':div':2':pow':ln':1'2(+(x, 1)) ⇔ s'(_gen_t':h':s':constant':c':m':opp':div':2':pow':ln':1'2(x))
The following defined symbols remain to be analysed:
D'
Could not prove a rewrite lemma for the defined symbol D'.
Rules:
D'(t') → s'(h')
D'(constant') → h'
D'(b'(x, y)) → b'(D'(x), D'(y))
D'(c'(x, y)) → b'(c'(y, D'(x)), c'(x, D'(y)))
D'(m'(x, y)) → m'(D'(x), D'(y))
D'(opp'(x)) → opp'(D'(x))
D'(div'(x, y)) → m'(div'(D'(x), y), div'(c'(x, D'(y)), pow'(y, 2')))
D'(ln'(x)) → div'(D'(x), x)
D'(pow'(x, y)) → b'(c'(c'(y, pow'(x, m'(y, 1'))), D'(x)), c'(c'(pow'(x, y), ln'(x)), D'(y)))
b'(h', x) → x
b'(x, h') → x
b'(s'(x), s'(y)) → s'(s'(b'(x, y)))
b'(b'(x, y), z) → b'(x, b'(y, z))
Types:
D' :: t':h':s':constant':c':m':opp':div':2':pow':ln':1' → t':h':s':constant':c':m':opp':div':2':pow':ln':1'
t' :: t':h':s':constant':c':m':opp':div':2':pow':ln':1'
s' :: t':h':s':constant':c':m':opp':div':2':pow':ln':1' → t':h':s':constant':c':m':opp':div':2':pow':ln':1'
h' :: t':h':s':constant':c':m':opp':div':2':pow':ln':1'
constant' :: t':h':s':constant':c':m':opp':div':2':pow':ln':1'
b' :: t':h':s':constant':c':m':opp':div':2':pow':ln':1' → t':h':s':constant':c':m':opp':div':2':pow':ln':1' → t':h':s':constant':c':m':opp':div':2':pow':ln':1'
c' :: t':h':s':constant':c':m':opp':div':2':pow':ln':1' → t':h':s':constant':c':m':opp':div':2':pow':ln':1' → t':h':s':constant':c':m':opp':div':2':pow':ln':1'
m' :: t':h':s':constant':c':m':opp':div':2':pow':ln':1' → t':h':s':constant':c':m':opp':div':2':pow':ln':1' → t':h':s':constant':c':m':opp':div':2':pow':ln':1'
opp' :: t':h':s':constant':c':m':opp':div':2':pow':ln':1' → t':h':s':constant':c':m':opp':div':2':pow':ln':1'
div' :: t':h':s':constant':c':m':opp':div':2':pow':ln':1' → t':h':s':constant':c':m':opp':div':2':pow':ln':1' → t':h':s':constant':c':m':opp':div':2':pow':ln':1'
pow' :: t':h':s':constant':c':m':opp':div':2':pow':ln':1' → t':h':s':constant':c':m':opp':div':2':pow':ln':1' → t':h':s':constant':c':m':opp':div':2':pow':ln':1'
2' :: t':h':s':constant':c':m':opp':div':2':pow':ln':1'
ln' :: t':h':s':constant':c':m':opp':div':2':pow':ln':1' → t':h':s':constant':c':m':opp':div':2':pow':ln':1'
1' :: t':h':s':constant':c':m':opp':div':2':pow':ln':1'
_hole_t':h':s':constant':c':m':opp':div':2':pow':ln':1'1 :: t':h':s':constant':c':m':opp':div':2':pow':ln':1'
_gen_t':h':s':constant':c':m':opp':div':2':pow':ln':1'2 :: Nat → t':h':s':constant':c':m':opp':div':2':pow':ln':1'
Lemmas:
b'(_gen_t':h':s':constant':c':m':opp':div':2':pow':ln':1'2(+(1, _n4)), _gen_t':h':s':constant':c':m':opp':div':2':pow':ln':1'2(+(1, _n4))) → _*3, rt ∈ Ω(n4)
Generator Equations:
_gen_t':h':s':constant':c':m':opp':div':2':pow':ln':1'2(0) ⇔ t'
_gen_t':h':s':constant':c':m':opp':div':2':pow':ln':1'2(+(x, 1)) ⇔ s'(_gen_t':h':s':constant':c':m':opp':div':2':pow':ln':1'2(x))
No more defined symbols left to analyse.
The lowerbound Ω(n) was proven with the following lemma:
b'(_gen_t':h':s':constant':c':m':opp':div':2':pow':ln':1'2(+(1, _n4)), _gen_t':h':s':constant':c':m':opp':div':2':pow':ln':1'2(+(1, _n4))) → _*3, rt ∈ Ω(n4)