ack_in(0, n) → ack_out(s(n))
ack_in(s(m), 0) → u11(ack_in(m, s(0)))
u11(ack_out(n)) → ack_out(n)
ack_in(s(m), s(n)) → u21(ack_in(s(m), n), m)
u21(ack_out(n), m) → u22(ack_in(m, n))
u22(ack_out(n)) → ack_out(n)
Renamed function symbols to avoid clashes with predefined symbol.
Runtime Complexity TRS:
The TRS R consists of the following rules:
ack_in'(0', n) → ack_out'(s'(n))
ack_in'(s'(m), 0') → u11'(ack_in'(m, s'(0')))
u11'(ack_out'(n)) → ack_out'(n)
ack_in'(s'(m), s'(n)) → u21'(ack_in'(s'(m), n), m)
u21'(ack_out'(n), m) → u22'(ack_in'(m, n))
u22'(ack_out'(n)) → ack_out'(n)
Infered types.
Rules:
ack_in'(0', n) → ack_out'(s'(n))
ack_in'(s'(m), 0') → u11'(ack_in'(m, s'(0')))
u11'(ack_out'(n)) → ack_out'(n)
ack_in'(s'(m), s'(n)) → u21'(ack_in'(s'(m), n), m)
u21'(ack_out'(n), m) → u22'(ack_in'(m, n))
u22'(ack_out'(n)) → ack_out'(n)
Types:
ack_in' :: 0':s' → 0':s' → ack_out'
0' :: 0':s'
ack_out' :: 0':s' → ack_out'
s' :: 0':s' → 0':s'
u11' :: ack_out' → ack_out'
u21' :: ack_out' → 0':s' → ack_out'
u22' :: ack_out' → ack_out'
_hole_ack_out'1 :: ack_out'
_hole_0':s'2 :: 0':s'
_gen_0':s'3 :: Nat → 0':s'
Heuristically decided to analyse the following defined symbols:
ack_in', u21'
They will be analysed ascendingly in the following order:
ack_in' = u21'
Rules:
ack_in'(0', n) → ack_out'(s'(n))
ack_in'(s'(m), 0') → u11'(ack_in'(m, s'(0')))
u11'(ack_out'(n)) → ack_out'(n)
ack_in'(s'(m), s'(n)) → u21'(ack_in'(s'(m), n), m)
u21'(ack_out'(n), m) → u22'(ack_in'(m, n))
u22'(ack_out'(n)) → ack_out'(n)
Types:
ack_in' :: 0':s' → 0':s' → ack_out'
0' :: 0':s'
ack_out' :: 0':s' → ack_out'
s' :: 0':s' → 0':s'
u11' :: ack_out' → ack_out'
u21' :: ack_out' → 0':s' → ack_out'
u22' :: ack_out' → ack_out'
_hole_ack_out'1 :: ack_out'
_hole_0':s'2 :: 0':s'
_gen_0':s'3 :: Nat → 0':s'
Generator Equations:
_gen_0':s'3(0) ⇔ 0'
_gen_0':s'3(+(x, 1)) ⇔ s'(_gen_0':s'3(x))
The following defined symbols remain to be analysed:
u21', ack_in'
They will be analysed ascendingly in the following order:
ack_in' = u21'
Could not prove a rewrite lemma for the defined symbol u21'.
Rules:
ack_in'(0', n) → ack_out'(s'(n))
ack_in'(s'(m), 0') → u11'(ack_in'(m, s'(0')))
u11'(ack_out'(n)) → ack_out'(n)
ack_in'(s'(m), s'(n)) → u21'(ack_in'(s'(m), n), m)
u21'(ack_out'(n), m) → u22'(ack_in'(m, n))
u22'(ack_out'(n)) → ack_out'(n)
Types:
ack_in' :: 0':s' → 0':s' → ack_out'
0' :: 0':s'
ack_out' :: 0':s' → ack_out'
s' :: 0':s' → 0':s'
u11' :: ack_out' → ack_out'
u21' :: ack_out' → 0':s' → ack_out'
u22' :: ack_out' → ack_out'
_hole_ack_out'1 :: ack_out'
_hole_0':s'2 :: 0':s'
_gen_0':s'3 :: Nat → 0':s'
Generator Equations:
_gen_0':s'3(0) ⇔ 0'
_gen_0':s'3(+(x, 1)) ⇔ s'(_gen_0':s'3(x))
The following defined symbols remain to be analysed:
ack_in'
They will be analysed ascendingly in the following order:
ack_in' = u21'
Proved the following rewrite lemma:
ack_in'(_gen_0':s'3(1), _gen_0':s'3(+(1, _n9293))) → _*4, rt ∈ Ω(n9293)
Induction Base:
ack_in'(_gen_0':s'3(1), _gen_0':s'3(+(1, 0)))
Induction Step:
ack_in'(_gen_0':s'3(1), _gen_0':s'3(+(1, +(_$n9294, 1)))) →RΩ(1)
u21'(ack_in'(s'(_gen_0':s'3(0)), _gen_0':s'3(+(1, _$n9294))), _gen_0':s'3(0)) →IH
u21'(_*4, _gen_0':s'3(0))
We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).
Rules:
ack_in'(0', n) → ack_out'(s'(n))
ack_in'(s'(m), 0') → u11'(ack_in'(m, s'(0')))
u11'(ack_out'(n)) → ack_out'(n)
ack_in'(s'(m), s'(n)) → u21'(ack_in'(s'(m), n), m)
u21'(ack_out'(n), m) → u22'(ack_in'(m, n))
u22'(ack_out'(n)) → ack_out'(n)
Types:
ack_in' :: 0':s' → 0':s' → ack_out'
0' :: 0':s'
ack_out' :: 0':s' → ack_out'
s' :: 0':s' → 0':s'
u11' :: ack_out' → ack_out'
u21' :: ack_out' → 0':s' → ack_out'
u22' :: ack_out' → ack_out'
_hole_ack_out'1 :: ack_out'
_hole_0':s'2 :: 0':s'
_gen_0':s'3 :: Nat → 0':s'
Lemmas:
ack_in'(_gen_0':s'3(1), _gen_0':s'3(+(1, _n9293))) → _*4, rt ∈ Ω(n9293)
Generator Equations:
_gen_0':s'3(0) ⇔ 0'
_gen_0':s'3(+(x, 1)) ⇔ s'(_gen_0':s'3(x))
The following defined symbols remain to be analysed:
u21'
They will be analysed ascendingly in the following order:
ack_in' = u21'
Could not prove a rewrite lemma for the defined symbol u21'.
Rules:
ack_in'(0', n) → ack_out'(s'(n))
ack_in'(s'(m), 0') → u11'(ack_in'(m, s'(0')))
u11'(ack_out'(n)) → ack_out'(n)
ack_in'(s'(m), s'(n)) → u21'(ack_in'(s'(m), n), m)
u21'(ack_out'(n), m) → u22'(ack_in'(m, n))
u22'(ack_out'(n)) → ack_out'(n)
Types:
ack_in' :: 0':s' → 0':s' → ack_out'
0' :: 0':s'
ack_out' :: 0':s' → ack_out'
s' :: 0':s' → 0':s'
u11' :: ack_out' → ack_out'
u21' :: ack_out' → 0':s' → ack_out'
u22' :: ack_out' → ack_out'
_hole_ack_out'1 :: ack_out'
_hole_0':s'2 :: 0':s'
_gen_0':s'3 :: Nat → 0':s'
Lemmas:
ack_in'(_gen_0':s'3(1), _gen_0':s'3(+(1, _n9293))) → _*4, rt ∈ Ω(n9293)
Generator Equations:
_gen_0':s'3(0) ⇔ 0'
_gen_0':s'3(+(x, 1)) ⇔ s'(_gen_0':s'3(x))
No more defined symbols left to analyse.
The lowerbound Ω(n) was proven with the following lemma:
ack_in'(_gen_0':s'3(1), _gen_0':s'3(+(1, _n9293))) → _*4, rt ∈ Ω(n9293)