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