rec(rec(x)) → sent(rec(x))
rec(sent(x)) → sent(rec(x))
rec(no(x)) → sent(rec(x))
rec(bot) → up(sent(bot))
rec(up(x)) → up(rec(x))
sent(up(x)) → up(sent(x))
no(up(x)) → up(no(x))
top(rec(up(x))) → top(check(rec(x)))
top(sent(up(x))) → top(check(rec(x)))
top(no(up(x))) → top(check(rec(x)))
check(up(x)) → up(check(x))
check(sent(x)) → sent(check(x))
check(rec(x)) → rec(check(x))
check(no(x)) → no(check(x))
check(no(x)) → no(x)
Renamed function symbols to avoid clashes with predefined symbol.
Runtime Complexity TRS:
The TRS R consists of the following rules:
rec'(rec'(x)) → sent'(rec'(x))
rec'(sent'(x)) → sent'(rec'(x))
rec'(no'(x)) → sent'(rec'(x))
rec'(bot') → up'(sent'(bot'))
rec'(up'(x)) → up'(rec'(x))
sent'(up'(x)) → up'(sent'(x))
no'(up'(x)) → up'(no'(x))
top'(rec'(up'(x))) → top'(check'(rec'(x)))
top'(sent'(up'(x))) → top'(check'(rec'(x)))
top'(no'(up'(x))) → top'(check'(rec'(x)))
check'(up'(x)) → up'(check'(x))
check'(sent'(x)) → sent'(check'(x))
check'(rec'(x)) → rec'(check'(x))
check'(no'(x)) → no'(check'(x))
check'(no'(x)) → no'(x)
Infered types.
Rules:
rec'(rec'(x)) → sent'(rec'(x))
rec'(sent'(x)) → sent'(rec'(x))
rec'(no'(x)) → sent'(rec'(x))
rec'(bot') → up'(sent'(bot'))
rec'(up'(x)) → up'(rec'(x))
sent'(up'(x)) → up'(sent'(x))
no'(up'(x)) → up'(no'(x))
top'(rec'(up'(x))) → top'(check'(rec'(x)))
top'(sent'(up'(x))) → top'(check'(rec'(x)))
top'(no'(up'(x))) → top'(check'(rec'(x)))
check'(up'(x)) → up'(check'(x))
check'(sent'(x)) → sent'(check'(x))
check'(rec'(x)) → rec'(check'(x))
check'(no'(x)) → no'(check'(x))
check'(no'(x)) → no'(x)
Types:
rec' :: bot':up' → bot':up'
sent' :: bot':up' → bot':up'
no' :: bot':up' → bot':up'
bot' :: bot':up'
up' :: bot':up' → bot':up'
top' :: bot':up' → top'
check' :: bot':up' → bot':up'
_hole_bot':up'1 :: bot':up'
_hole_top'2 :: top'
_gen_bot':up'3 :: Nat → bot':up'
Heuristically decided to analyse the following defined symbols:
rec', sent', no', top', check'
They will be analysed ascendingly in the following order:
sent' < rec'
rec' < top'
rec' < check'
sent' < check'
no' < check'
check' < top'
Rules:
rec'(rec'(x)) → sent'(rec'(x))
rec'(sent'(x)) → sent'(rec'(x))
rec'(no'(x)) → sent'(rec'(x))
rec'(bot') → up'(sent'(bot'))
rec'(up'(x)) → up'(rec'(x))
sent'(up'(x)) → up'(sent'(x))
no'(up'(x)) → up'(no'(x))
top'(rec'(up'(x))) → top'(check'(rec'(x)))
top'(sent'(up'(x))) → top'(check'(rec'(x)))
top'(no'(up'(x))) → top'(check'(rec'(x)))
check'(up'(x)) → up'(check'(x))
check'(sent'(x)) → sent'(check'(x))
check'(rec'(x)) → rec'(check'(x))
check'(no'(x)) → no'(check'(x))
check'(no'(x)) → no'(x)
Types:
rec' :: bot':up' → bot':up'
sent' :: bot':up' → bot':up'
no' :: bot':up' → bot':up'
bot' :: bot':up'
up' :: bot':up' → bot':up'
top' :: bot':up' → top'
check' :: bot':up' → bot':up'
_hole_bot':up'1 :: bot':up'
_hole_top'2 :: top'
_gen_bot':up'3 :: Nat → bot':up'
Generator Equations:
_gen_bot':up'3(0) ⇔ bot'
_gen_bot':up'3(+(x, 1)) ⇔ up'(_gen_bot':up'3(x))
The following defined symbols remain to be analysed:
sent', rec', no', top', check'
They will be analysed ascendingly in the following order:
sent' < rec'
rec' < top'
rec' < check'
sent' < check'
no' < check'
check' < top'
Proved the following rewrite lemma:
sent'(_gen_bot':up'3(+(1, _n5))) → _*4, rt ∈ Ω(n5)
Induction Base:
sent'(_gen_bot':up'3(+(1, 0)))
Induction Step:
sent'(_gen_bot':up'3(+(1, +(_$n6, 1)))) →RΩ(1)
up'(sent'(_gen_bot':up'3(+(1, _$n6)))) →IH
up'(_*4)
We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).
Rules:
rec'(rec'(x)) → sent'(rec'(x))
rec'(sent'(x)) → sent'(rec'(x))
rec'(no'(x)) → sent'(rec'(x))
rec'(bot') → up'(sent'(bot'))
rec'(up'(x)) → up'(rec'(x))
sent'(up'(x)) → up'(sent'(x))
no'(up'(x)) → up'(no'(x))
top'(rec'(up'(x))) → top'(check'(rec'(x)))
top'(sent'(up'(x))) → top'(check'(rec'(x)))
top'(no'(up'(x))) → top'(check'(rec'(x)))
check'(up'(x)) → up'(check'(x))
check'(sent'(x)) → sent'(check'(x))
check'(rec'(x)) → rec'(check'(x))
check'(no'(x)) → no'(check'(x))
check'(no'(x)) → no'(x)
Types:
rec' :: bot':up' → bot':up'
sent' :: bot':up' → bot':up'
no' :: bot':up' → bot':up'
bot' :: bot':up'
up' :: bot':up' → bot':up'
top' :: bot':up' → top'
check' :: bot':up' → bot':up'
_hole_bot':up'1 :: bot':up'
_hole_top'2 :: top'
_gen_bot':up'3 :: Nat → bot':up'
Lemmas:
sent'(_gen_bot':up'3(+(1, _n5))) → _*4, rt ∈ Ω(n5)
Generator Equations:
_gen_bot':up'3(0) ⇔ bot'
_gen_bot':up'3(+(x, 1)) ⇔ up'(_gen_bot':up'3(x))
The following defined symbols remain to be analysed:
rec', no', top', check'
They will be analysed ascendingly in the following order:
rec' < top'
rec' < check'
no' < check'
check' < top'
Proved the following rewrite lemma:
rec'(_gen_bot':up'3(+(1, _n445))) → _*4, rt ∈ Ω(n445)
Induction Base:
rec'(_gen_bot':up'3(+(1, 0)))
Induction Step:
rec'(_gen_bot':up'3(+(1, +(_$n446, 1)))) →RΩ(1)
up'(rec'(_gen_bot':up'3(+(1, _$n446)))) →IH
up'(_*4)
We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).
Rules:
rec'(rec'(x)) → sent'(rec'(x))
rec'(sent'(x)) → sent'(rec'(x))
rec'(no'(x)) → sent'(rec'(x))
rec'(bot') → up'(sent'(bot'))
rec'(up'(x)) → up'(rec'(x))
sent'(up'(x)) → up'(sent'(x))
no'(up'(x)) → up'(no'(x))
top'(rec'(up'(x))) → top'(check'(rec'(x)))
top'(sent'(up'(x))) → top'(check'(rec'(x)))
top'(no'(up'(x))) → top'(check'(rec'(x)))
check'(up'(x)) → up'(check'(x))
check'(sent'(x)) → sent'(check'(x))
check'(rec'(x)) → rec'(check'(x))
check'(no'(x)) → no'(check'(x))
check'(no'(x)) → no'(x)
Types:
rec' :: bot':up' → bot':up'
sent' :: bot':up' → bot':up'
no' :: bot':up' → bot':up'
bot' :: bot':up'
up' :: bot':up' → bot':up'
top' :: bot':up' → top'
check' :: bot':up' → bot':up'
_hole_bot':up'1 :: bot':up'
_hole_top'2 :: top'
_gen_bot':up'3 :: Nat → bot':up'
Lemmas:
sent'(_gen_bot':up'3(+(1, _n5))) → _*4, rt ∈ Ω(n5)
rec'(_gen_bot':up'3(+(1, _n445))) → _*4, rt ∈ Ω(n445)
Generator Equations:
_gen_bot':up'3(0) ⇔ bot'
_gen_bot':up'3(+(x, 1)) ⇔ up'(_gen_bot':up'3(x))
The following defined symbols remain to be analysed:
no', top', check'
They will be analysed ascendingly in the following order:
no' < check'
check' < top'
Proved the following rewrite lemma:
no'(_gen_bot':up'3(+(1, _n9866))) → _*4, rt ∈ Ω(n9866)
Induction Base:
no'(_gen_bot':up'3(+(1, 0)))
Induction Step:
no'(_gen_bot':up'3(+(1, +(_$n9867, 1)))) →RΩ(1)
up'(no'(_gen_bot':up'3(+(1, _$n9867)))) →IH
up'(_*4)
We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).
Rules:
rec'(rec'(x)) → sent'(rec'(x))
rec'(sent'(x)) → sent'(rec'(x))
rec'(no'(x)) → sent'(rec'(x))
rec'(bot') → up'(sent'(bot'))
rec'(up'(x)) → up'(rec'(x))
sent'(up'(x)) → up'(sent'(x))
no'(up'(x)) → up'(no'(x))
top'(rec'(up'(x))) → top'(check'(rec'(x)))
top'(sent'(up'(x))) → top'(check'(rec'(x)))
top'(no'(up'(x))) → top'(check'(rec'(x)))
check'(up'(x)) → up'(check'(x))
check'(sent'(x)) → sent'(check'(x))
check'(rec'(x)) → rec'(check'(x))
check'(no'(x)) → no'(check'(x))
check'(no'(x)) → no'(x)
Types:
rec' :: bot':up' → bot':up'
sent' :: bot':up' → bot':up'
no' :: bot':up' → bot':up'
bot' :: bot':up'
up' :: bot':up' → bot':up'
top' :: bot':up' → top'
check' :: bot':up' → bot':up'
_hole_bot':up'1 :: bot':up'
_hole_top'2 :: top'
_gen_bot':up'3 :: Nat → bot':up'
Lemmas:
sent'(_gen_bot':up'3(+(1, _n5))) → _*4, rt ∈ Ω(n5)
rec'(_gen_bot':up'3(+(1, _n445))) → _*4, rt ∈ Ω(n445)
no'(_gen_bot':up'3(+(1, _n9866))) → _*4, rt ∈ Ω(n9866)
Generator Equations:
_gen_bot':up'3(0) ⇔ bot'
_gen_bot':up'3(+(x, 1)) ⇔ up'(_gen_bot':up'3(x))
The following defined symbols remain to be analysed:
check', top'
They will be analysed ascendingly in the following order:
check' < top'
Proved the following rewrite lemma:
check'(_gen_bot':up'3(+(1, _n10554))) → _*4, rt ∈ Ω(n10554)
Induction Base:
check'(_gen_bot':up'3(+(1, 0)))
Induction Step:
check'(_gen_bot':up'3(+(1, +(_$n10555, 1)))) →RΩ(1)
up'(check'(_gen_bot':up'3(+(1, _$n10555)))) →IH
up'(_*4)
We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).
Rules:
rec'(rec'(x)) → sent'(rec'(x))
rec'(sent'(x)) → sent'(rec'(x))
rec'(no'(x)) → sent'(rec'(x))
rec'(bot') → up'(sent'(bot'))
rec'(up'(x)) → up'(rec'(x))
sent'(up'(x)) → up'(sent'(x))
no'(up'(x)) → up'(no'(x))
top'(rec'(up'(x))) → top'(check'(rec'(x)))
top'(sent'(up'(x))) → top'(check'(rec'(x)))
top'(no'(up'(x))) → top'(check'(rec'(x)))
check'(up'(x)) → up'(check'(x))
check'(sent'(x)) → sent'(check'(x))
check'(rec'(x)) → rec'(check'(x))
check'(no'(x)) → no'(check'(x))
check'(no'(x)) → no'(x)
Types:
rec' :: bot':up' → bot':up'
sent' :: bot':up' → bot':up'
no' :: bot':up' → bot':up'
bot' :: bot':up'
up' :: bot':up' → bot':up'
top' :: bot':up' → top'
check' :: bot':up' → bot':up'
_hole_bot':up'1 :: bot':up'
_hole_top'2 :: top'
_gen_bot':up'3 :: Nat → bot':up'
Lemmas:
sent'(_gen_bot':up'3(+(1, _n5))) → _*4, rt ∈ Ω(n5)
rec'(_gen_bot':up'3(+(1, _n445))) → _*4, rt ∈ Ω(n445)
no'(_gen_bot':up'3(+(1, _n9866))) → _*4, rt ∈ Ω(n9866)
check'(_gen_bot':up'3(+(1, _n10554))) → _*4, rt ∈ Ω(n10554)
Generator Equations:
_gen_bot':up'3(0) ⇔ bot'
_gen_bot':up'3(+(x, 1)) ⇔ up'(_gen_bot':up'3(x))
The following defined symbols remain to be analysed:
top'
Could not prove a rewrite lemma for the defined symbol top'.
Rules:
rec'(rec'(x)) → sent'(rec'(x))
rec'(sent'(x)) → sent'(rec'(x))
rec'(no'(x)) → sent'(rec'(x))
rec'(bot') → up'(sent'(bot'))
rec'(up'(x)) → up'(rec'(x))
sent'(up'(x)) → up'(sent'(x))
no'(up'(x)) → up'(no'(x))
top'(rec'(up'(x))) → top'(check'(rec'(x)))
top'(sent'(up'(x))) → top'(check'(rec'(x)))
top'(no'(up'(x))) → top'(check'(rec'(x)))
check'(up'(x)) → up'(check'(x))
check'(sent'(x)) → sent'(check'(x))
check'(rec'(x)) → rec'(check'(x))
check'(no'(x)) → no'(check'(x))
check'(no'(x)) → no'(x)
Types:
rec' :: bot':up' → bot':up'
sent' :: bot':up' → bot':up'
no' :: bot':up' → bot':up'
bot' :: bot':up'
up' :: bot':up' → bot':up'
top' :: bot':up' → top'
check' :: bot':up' → bot':up'
_hole_bot':up'1 :: bot':up'
_hole_top'2 :: top'
_gen_bot':up'3 :: Nat → bot':up'
Lemmas:
sent'(_gen_bot':up'3(+(1, _n5))) → _*4, rt ∈ Ω(n5)
rec'(_gen_bot':up'3(+(1, _n445))) → _*4, rt ∈ Ω(n445)
no'(_gen_bot':up'3(+(1, _n9866))) → _*4, rt ∈ Ω(n9866)
check'(_gen_bot':up'3(+(1, _n10554))) → _*4, rt ∈ Ω(n10554)
Generator Equations:
_gen_bot':up'3(0) ⇔ bot'
_gen_bot':up'3(+(x, 1)) ⇔ up'(_gen_bot':up'3(x))
No more defined symbols left to analyse.
The lowerbound Ω(n) was proven with the following lemma:
sent'(_gen_bot':up'3(+(1, _n5))) → _*4, rt ∈ Ω(n5)