top1(free(x), y) → top2(check(new(x)), y)
top1(free(x), y) → top2(new(x), check(y))
top1(free(x), y) → top2(check(x), new(y))
top1(free(x), y) → top2(x, check(new(y)))
top2(x, free(y)) → top1(check(new(x)), y)
top2(x, free(y)) → top1(new(x), check(y))
top2(x, free(y)) → top1(check(x), new(y))
top2(x, free(y)) → top1(x, check(new(y)))
new(free(x)) → free(new(x))
old(free(x)) → free(old(x))
new(serve) → free(serve)
old(serve) → free(serve)
check(free(x)) → free(check(x))
check(new(x)) → new(check(x))
check(old(x)) → old(check(x))
check(old(x)) → old(x)
Renamed function symbols to avoid clashes with predefined symbol.
Runtime Complexity TRS:
The TRS R consists of the following rules:
top1'(free'(x), y) → top2'(check'(new'(x)), y)
top1'(free'(x), y) → top2'(new'(x), check'(y))
top1'(free'(x), y) → top2'(check'(x), new'(y))
top1'(free'(x), y) → top2'(x, check'(new'(y)))
top2'(x, free'(y)) → top1'(check'(new'(x)), y)
top2'(x, free'(y)) → top1'(new'(x), check'(y))
top2'(x, free'(y)) → top1'(check'(x), new'(y))
top2'(x, free'(y)) → top1'(x, check'(new'(y)))
new'(free'(x)) → free'(new'(x))
old'(free'(x)) → free'(old'(x))
new'(serve') → free'(serve')
old'(serve') → free'(serve')
check'(free'(x)) → free'(check'(x))
check'(new'(x)) → new'(check'(x))
check'(old'(x)) → old'(check'(x))
check'(old'(x)) → old'(x)
Infered types.
Rules:
top1'(free'(x), y) → top2'(check'(new'(x)), y)
top1'(free'(x), y) → top2'(new'(x), check'(y))
top1'(free'(x), y) → top2'(check'(x), new'(y))
top1'(free'(x), y) → top2'(x, check'(new'(y)))
top2'(x, free'(y)) → top1'(check'(new'(x)), y)
top2'(x, free'(y)) → top1'(new'(x), check'(y))
top2'(x, free'(y)) → top1'(check'(x), new'(y))
top2'(x, free'(y)) → top1'(x, check'(new'(y)))
new'(free'(x)) → free'(new'(x))
old'(free'(x)) → free'(old'(x))
new'(serve') → free'(serve')
old'(serve') → free'(serve')
check'(free'(x)) → free'(check'(x))
check'(new'(x)) → new'(check'(x))
check'(old'(x)) → old'(check'(x))
check'(old'(x)) → old'(x)
Types:
top1' :: free':serve' → free':serve' → top1':top2'
free' :: free':serve' → free':serve'
top2' :: free':serve' → free':serve' → top1':top2'
check' :: free':serve' → free':serve'
new' :: free':serve' → free':serve'
old' :: free':serve' → free':serve'
serve' :: free':serve'
_hole_top1':top2'1 :: top1':top2'
_hole_free':serve'2 :: free':serve'
_gen_free':serve'3 :: Nat → free':serve'
Heuristically decided to analyse the following defined symbols:
top1', top2', check', new', old'
They will be analysed ascendingly in the following order:
top1' = top2'
check' < top1'
new' < top1'
check' < top2'
new' < top2'
new' < check'
old' < check'
Rules:
top1'(free'(x), y) → top2'(check'(new'(x)), y)
top1'(free'(x), y) → top2'(new'(x), check'(y))
top1'(free'(x), y) → top2'(check'(x), new'(y))
top1'(free'(x), y) → top2'(x, check'(new'(y)))
top2'(x, free'(y)) → top1'(check'(new'(x)), y)
top2'(x, free'(y)) → top1'(new'(x), check'(y))
top2'(x, free'(y)) → top1'(check'(x), new'(y))
top2'(x, free'(y)) → top1'(x, check'(new'(y)))
new'(free'(x)) → free'(new'(x))
old'(free'(x)) → free'(old'(x))
new'(serve') → free'(serve')
old'(serve') → free'(serve')
check'(free'(x)) → free'(check'(x))
check'(new'(x)) → new'(check'(x))
check'(old'(x)) → old'(check'(x))
check'(old'(x)) → old'(x)
Types:
top1' :: free':serve' → free':serve' → top1':top2'
free' :: free':serve' → free':serve'
top2' :: free':serve' → free':serve' → top1':top2'
check' :: free':serve' → free':serve'
new' :: free':serve' → free':serve'
old' :: free':serve' → free':serve'
serve' :: free':serve'
_hole_top1':top2'1 :: top1':top2'
_hole_free':serve'2 :: free':serve'
_gen_free':serve'3 :: Nat → free':serve'
Generator Equations:
_gen_free':serve'3(0) ⇔ serve'
_gen_free':serve'3(+(x, 1)) ⇔ free'(_gen_free':serve'3(x))
The following defined symbols remain to be analysed:
new', top1', top2', check', old'
They will be analysed ascendingly in the following order:
top1' = top2'
check' < top1'
new' < top1'
check' < top2'
new' < top2'
new' < check'
old' < check'
Proved the following rewrite lemma:
new'(_gen_free':serve'3(_n5)) → _gen_free':serve'3(+(1, _n5)), rt ∈ Ω(1 + n5)
Induction Base:
new'(_gen_free':serve'3(0)) →RΩ(1)
free'(serve')
Induction Step:
new'(_gen_free':serve'3(+(_$n6, 1))) →RΩ(1)
free'(new'(_gen_free':serve'3(_$n6))) →IH
free'(_gen_free':serve'3(+(1, _$n6)))
We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).
Rules:
top1'(free'(x), y) → top2'(check'(new'(x)), y)
top1'(free'(x), y) → top2'(new'(x), check'(y))
top1'(free'(x), y) → top2'(check'(x), new'(y))
top1'(free'(x), y) → top2'(x, check'(new'(y)))
top2'(x, free'(y)) → top1'(check'(new'(x)), y)
top2'(x, free'(y)) → top1'(new'(x), check'(y))
top2'(x, free'(y)) → top1'(check'(x), new'(y))
top2'(x, free'(y)) → top1'(x, check'(new'(y)))
new'(free'(x)) → free'(new'(x))
old'(free'(x)) → free'(old'(x))
new'(serve') → free'(serve')
old'(serve') → free'(serve')
check'(free'(x)) → free'(check'(x))
check'(new'(x)) → new'(check'(x))
check'(old'(x)) → old'(check'(x))
check'(old'(x)) → old'(x)
Types:
top1' :: free':serve' → free':serve' → top1':top2'
free' :: free':serve' → free':serve'
top2' :: free':serve' → free':serve' → top1':top2'
check' :: free':serve' → free':serve'
new' :: free':serve' → free':serve'
old' :: free':serve' → free':serve'
serve' :: free':serve'
_hole_top1':top2'1 :: top1':top2'
_hole_free':serve'2 :: free':serve'
_gen_free':serve'3 :: Nat → free':serve'
Lemmas:
new'(_gen_free':serve'3(_n5)) → _gen_free':serve'3(+(1, _n5)), rt ∈ Ω(1 + n5)
Generator Equations:
_gen_free':serve'3(0) ⇔ serve'
_gen_free':serve'3(+(x, 1)) ⇔ free'(_gen_free':serve'3(x))
The following defined symbols remain to be analysed:
old', top1', top2', check'
They will be analysed ascendingly in the following order:
top1' = top2'
check' < top1'
check' < top2'
old' < check'
Proved the following rewrite lemma:
old'(_gen_free':serve'3(_n585)) → _gen_free':serve'3(+(1, _n585)), rt ∈ Ω(1 + n585)
Induction Base:
old'(_gen_free':serve'3(0)) →RΩ(1)
free'(serve')
Induction Step:
old'(_gen_free':serve'3(+(_$n586, 1))) →RΩ(1)
free'(old'(_gen_free':serve'3(_$n586))) →IH
free'(_gen_free':serve'3(+(1, _$n586)))
We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).
Rules:
top1'(free'(x), y) → top2'(check'(new'(x)), y)
top1'(free'(x), y) → top2'(new'(x), check'(y))
top1'(free'(x), y) → top2'(check'(x), new'(y))
top1'(free'(x), y) → top2'(x, check'(new'(y)))
top2'(x, free'(y)) → top1'(check'(new'(x)), y)
top2'(x, free'(y)) → top1'(new'(x), check'(y))
top2'(x, free'(y)) → top1'(check'(x), new'(y))
top2'(x, free'(y)) → top1'(x, check'(new'(y)))
new'(free'(x)) → free'(new'(x))
old'(free'(x)) → free'(old'(x))
new'(serve') → free'(serve')
old'(serve') → free'(serve')
check'(free'(x)) → free'(check'(x))
check'(new'(x)) → new'(check'(x))
check'(old'(x)) → old'(check'(x))
check'(old'(x)) → old'(x)
Types:
top1' :: free':serve' → free':serve' → top1':top2'
free' :: free':serve' → free':serve'
top2' :: free':serve' → free':serve' → top1':top2'
check' :: free':serve' → free':serve'
new' :: free':serve' → free':serve'
old' :: free':serve' → free':serve'
serve' :: free':serve'
_hole_top1':top2'1 :: top1':top2'
_hole_free':serve'2 :: free':serve'
_gen_free':serve'3 :: Nat → free':serve'
Lemmas:
new'(_gen_free':serve'3(_n5)) → _gen_free':serve'3(+(1, _n5)), rt ∈ Ω(1 + n5)
old'(_gen_free':serve'3(_n585)) → _gen_free':serve'3(+(1, _n585)), rt ∈ Ω(1 + n585)
Generator Equations:
_gen_free':serve'3(0) ⇔ serve'
_gen_free':serve'3(+(x, 1)) ⇔ free'(_gen_free':serve'3(x))
The following defined symbols remain to be analysed:
check', top1', top2'
They will be analysed ascendingly in the following order:
top1' = top2'
check' < top1'
check' < top2'
Proved the following rewrite lemma:
check'(_gen_free':serve'3(+(1, _n1187))) → _*4, rt ∈ Ω(n1187)
Induction Base:
check'(_gen_free':serve'3(+(1, 0)))
Induction Step:
check'(_gen_free':serve'3(+(1, +(_$n1188, 1)))) →RΩ(1)
free'(check'(_gen_free':serve'3(+(1, _$n1188)))) →IH
free'(_*4)
We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).
Rules:
top1'(free'(x), y) → top2'(check'(new'(x)), y)
top1'(free'(x), y) → top2'(new'(x), check'(y))
top1'(free'(x), y) → top2'(check'(x), new'(y))
top1'(free'(x), y) → top2'(x, check'(new'(y)))
top2'(x, free'(y)) → top1'(check'(new'(x)), y)
top2'(x, free'(y)) → top1'(new'(x), check'(y))
top2'(x, free'(y)) → top1'(check'(x), new'(y))
top2'(x, free'(y)) → top1'(x, check'(new'(y)))
new'(free'(x)) → free'(new'(x))
old'(free'(x)) → free'(old'(x))
new'(serve') → free'(serve')
old'(serve') → free'(serve')
check'(free'(x)) → free'(check'(x))
check'(new'(x)) → new'(check'(x))
check'(old'(x)) → old'(check'(x))
check'(old'(x)) → old'(x)
Types:
top1' :: free':serve' → free':serve' → top1':top2'
free' :: free':serve' → free':serve'
top2' :: free':serve' → free':serve' → top1':top2'
check' :: free':serve' → free':serve'
new' :: free':serve' → free':serve'
old' :: free':serve' → free':serve'
serve' :: free':serve'
_hole_top1':top2'1 :: top1':top2'
_hole_free':serve'2 :: free':serve'
_gen_free':serve'3 :: Nat → free':serve'
Lemmas:
new'(_gen_free':serve'3(_n5)) → _gen_free':serve'3(+(1, _n5)), rt ∈ Ω(1 + n5)
old'(_gen_free':serve'3(_n585)) → _gen_free':serve'3(+(1, _n585)), rt ∈ Ω(1 + n585)
check'(_gen_free':serve'3(+(1, _n1187))) → _*4, rt ∈ Ω(n1187)
Generator Equations:
_gen_free':serve'3(0) ⇔ serve'
_gen_free':serve'3(+(x, 1)) ⇔ free'(_gen_free':serve'3(x))
The following defined symbols remain to be analysed:
top2', top1'
They will be analysed ascendingly in the following order:
top1' = top2'
Could not prove a rewrite lemma for the defined symbol top2'.
Rules:
top1'(free'(x), y) → top2'(check'(new'(x)), y)
top1'(free'(x), y) → top2'(new'(x), check'(y))
top1'(free'(x), y) → top2'(check'(x), new'(y))
top1'(free'(x), y) → top2'(x, check'(new'(y)))
top2'(x, free'(y)) → top1'(check'(new'(x)), y)
top2'(x, free'(y)) → top1'(new'(x), check'(y))
top2'(x, free'(y)) → top1'(check'(x), new'(y))
top2'(x, free'(y)) → top1'(x, check'(new'(y)))
new'(free'(x)) → free'(new'(x))
old'(free'(x)) → free'(old'(x))
new'(serve') → free'(serve')
old'(serve') → free'(serve')
check'(free'(x)) → free'(check'(x))
check'(new'(x)) → new'(check'(x))
check'(old'(x)) → old'(check'(x))
check'(old'(x)) → old'(x)
Types:
top1' :: free':serve' → free':serve' → top1':top2'
free' :: free':serve' → free':serve'
top2' :: free':serve' → free':serve' → top1':top2'
check' :: free':serve' → free':serve'
new' :: free':serve' → free':serve'
old' :: free':serve' → free':serve'
serve' :: free':serve'
_hole_top1':top2'1 :: top1':top2'
_hole_free':serve'2 :: free':serve'
_gen_free':serve'3 :: Nat → free':serve'
Lemmas:
new'(_gen_free':serve'3(_n5)) → _gen_free':serve'3(+(1, _n5)), rt ∈ Ω(1 + n5)
old'(_gen_free':serve'3(_n585)) → _gen_free':serve'3(+(1, _n585)), rt ∈ Ω(1 + n585)
check'(_gen_free':serve'3(+(1, _n1187))) → _*4, rt ∈ Ω(n1187)
Generator Equations:
_gen_free':serve'3(0) ⇔ serve'
_gen_free':serve'3(+(x, 1)) ⇔ free'(_gen_free':serve'3(x))
The following defined symbols remain to be analysed:
top1'
They will be analysed ascendingly in the following order:
top1' = top2'
Could not prove a rewrite lemma for the defined symbol top1'.
Rules:
top1'(free'(x), y) → top2'(check'(new'(x)), y)
top1'(free'(x), y) → top2'(new'(x), check'(y))
top1'(free'(x), y) → top2'(check'(x), new'(y))
top1'(free'(x), y) → top2'(x, check'(new'(y)))
top2'(x, free'(y)) → top1'(check'(new'(x)), y)
top2'(x, free'(y)) → top1'(new'(x), check'(y))
top2'(x, free'(y)) → top1'(check'(x), new'(y))
top2'(x, free'(y)) → top1'(x, check'(new'(y)))
new'(free'(x)) → free'(new'(x))
old'(free'(x)) → free'(old'(x))
new'(serve') → free'(serve')
old'(serve') → free'(serve')
check'(free'(x)) → free'(check'(x))
check'(new'(x)) → new'(check'(x))
check'(old'(x)) → old'(check'(x))
check'(old'(x)) → old'(x)
Types:
top1' :: free':serve' → free':serve' → top1':top2'
free' :: free':serve' → free':serve'
top2' :: free':serve' → free':serve' → top1':top2'
check' :: free':serve' → free':serve'
new' :: free':serve' → free':serve'
old' :: free':serve' → free':serve'
serve' :: free':serve'
_hole_top1':top2'1 :: top1':top2'
_hole_free':serve'2 :: free':serve'
_gen_free':serve'3 :: Nat → free':serve'
Lemmas:
new'(_gen_free':serve'3(_n5)) → _gen_free':serve'3(+(1, _n5)), rt ∈ Ω(1 + n5)
old'(_gen_free':serve'3(_n585)) → _gen_free':serve'3(+(1, _n585)), rt ∈ Ω(1 + n585)
check'(_gen_free':serve'3(+(1, _n1187))) → _*4, rt ∈ Ω(n1187)
Generator Equations:
_gen_free':serve'3(0) ⇔ serve'
_gen_free':serve'3(+(x, 1)) ⇔ free'(_gen_free':serve'3(x))
No more defined symbols left to analyse.
The lowerbound Ω(n) was proven with the following lemma:
new'(_gen_free':serve'3(_n5)) → _gen_free':serve'3(+(1, _n5)), rt ∈ Ω(1 + n5)