null(nil) → true
null(add(n, x)) → false
tail(add(n, x)) → x
tail(nil) → nil
head(add(n, x)) → n
app(nil, y) → y
app(add(n, x), y) → add(n, app(x, y))
reverse(nil) → nil
reverse(add(n, x)) → app(reverse(x), add(n, nil))
shuffle(x) → shuff(x, nil)
shuff(x, y) → if(null(x), x, y, app(y, add(head(x), nil)))
if(true, x, y, z) → y
if(false, x, y, z) → shuff(reverse(tail(x)), z)
Renamed function symbols to avoid clashes with predefined symbol.
Runtime Complexity TRS:
The TRS R consists of the following rules:
null'(nil') → true'
null'(add'(n, x)) → false'
tail'(add'(n, x)) → x
tail'(nil') → nil'
head'(add'(n, x)) → n
app'(nil', y) → y
app'(add'(n, x), y) → add'(n, app'(x, y))
reverse'(nil') → nil'
reverse'(add'(n, x)) → app'(reverse'(x), add'(n, nil'))
shuffle'(x) → shuff'(x, nil')
shuff'(x, y) → if'(null'(x), x, y, app'(y, add'(head'(x), nil')))
if'(true', x, y, z) → y
if'(false', x, y, z) → shuff'(reverse'(tail'(x)), z)
Infered types.
Rules:
null'(nil') → true'
null'(add'(n, x)) → false'
tail'(add'(n, x)) → x
tail'(nil') → nil'
head'(add'(n, x)) → n
app'(nil', y) → y
app'(add'(n, x), y) → add'(n, app'(x, y))
reverse'(nil') → nil'
reverse'(add'(n, x)) → app'(reverse'(x), add'(n, nil'))
shuffle'(x) → shuff'(x, nil')
shuff'(x, y) → if'(null'(x), x, y, app'(y, add'(head'(x), nil')))
if'(true', x, y, z) → y
if'(false', x, y, z) → shuff'(reverse'(tail'(x)), z)
Types:
null' :: nil':add' → true':false'
nil' :: nil':add'
true' :: true':false'
add' :: head' → nil':add' → nil':add'
false' :: true':false'
tail' :: nil':add' → nil':add'
head' :: nil':add' → head'
app' :: nil':add' → nil':add' → nil':add'
reverse' :: nil':add' → nil':add'
shuffle' :: nil':add' → nil':add'
shuff' :: nil':add' → nil':add' → nil':add'
if' :: true':false' → nil':add' → nil':add' → nil':add' → nil':add'
_hole_true':false'1 :: true':false'
_hole_nil':add'2 :: nil':add'
_hole_head'3 :: head'
_gen_nil':add'4 :: Nat → nil':add'
Heuristically decided to analyse the following defined symbols:
app', reverse', shuff'
They will be analysed ascendingly in the following order:
app' < reverse'
app' < shuff'
reverse' < shuff'
Rules:
null'(nil') → true'
null'(add'(n, x)) → false'
tail'(add'(n, x)) → x
tail'(nil') → nil'
head'(add'(n, x)) → n
app'(nil', y) → y
app'(add'(n, x), y) → add'(n, app'(x, y))
reverse'(nil') → nil'
reverse'(add'(n, x)) → app'(reverse'(x), add'(n, nil'))
shuffle'(x) → shuff'(x, nil')
shuff'(x, y) → if'(null'(x), x, y, app'(y, add'(head'(x), nil')))
if'(true', x, y, z) → y
if'(false', x, y, z) → shuff'(reverse'(tail'(x)), z)
Types:
null' :: nil':add' → true':false'
nil' :: nil':add'
true' :: true':false'
add' :: head' → nil':add' → nil':add'
false' :: true':false'
tail' :: nil':add' → nil':add'
head' :: nil':add' → head'
app' :: nil':add' → nil':add' → nil':add'
reverse' :: nil':add' → nil':add'
shuffle' :: nil':add' → nil':add'
shuff' :: nil':add' → nil':add' → nil':add'
if' :: true':false' → nil':add' → nil':add' → nil':add' → nil':add'
_hole_true':false'1 :: true':false'
_hole_nil':add'2 :: nil':add'
_hole_head'3 :: head'
_gen_nil':add'4 :: Nat → nil':add'
Generator Equations:
_gen_nil':add'4(0) ⇔ nil'
_gen_nil':add'4(+(x, 1)) ⇔ add'(_hole_head'3, _gen_nil':add'4(x))
The following defined symbols remain to be analysed:
app', reverse', shuff'
They will be analysed ascendingly in the following order:
app' < reverse'
app' < shuff'
reverse' < shuff'
Proved the following rewrite lemma:
app'(_gen_nil':add'4(_n6), _gen_nil':add'4(b)) → _gen_nil':add'4(+(_n6, b)), rt ∈ Ω(1 + n6)
Induction Base:
app'(_gen_nil':add'4(0), _gen_nil':add'4(b)) →RΩ(1)
_gen_nil':add'4(b)
Induction Step:
app'(_gen_nil':add'4(+(_$n7, 1)), _gen_nil':add'4(_b147)) →RΩ(1)
add'(_hole_head'3, app'(_gen_nil':add'4(_$n7), _gen_nil':add'4(_b147))) →IH
add'(_hole_head'3, _gen_nil':add'4(+(_$n7, _b147)))
We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).
Rules:
null'(nil') → true'
null'(add'(n, x)) → false'
tail'(add'(n, x)) → x
tail'(nil') → nil'
head'(add'(n, x)) → n
app'(nil', y) → y
app'(add'(n, x), y) → add'(n, app'(x, y))
reverse'(nil') → nil'
reverse'(add'(n, x)) → app'(reverse'(x), add'(n, nil'))
shuffle'(x) → shuff'(x, nil')
shuff'(x, y) → if'(null'(x), x, y, app'(y, add'(head'(x), nil')))
if'(true', x, y, z) → y
if'(false', x, y, z) → shuff'(reverse'(tail'(x)), z)
Types:
null' :: nil':add' → true':false'
nil' :: nil':add'
true' :: true':false'
add' :: head' → nil':add' → nil':add'
false' :: true':false'
tail' :: nil':add' → nil':add'
head' :: nil':add' → head'
app' :: nil':add' → nil':add' → nil':add'
reverse' :: nil':add' → nil':add'
shuffle' :: nil':add' → nil':add'
shuff' :: nil':add' → nil':add' → nil':add'
if' :: true':false' → nil':add' → nil':add' → nil':add' → nil':add'
_hole_true':false'1 :: true':false'
_hole_nil':add'2 :: nil':add'
_hole_head'3 :: head'
_gen_nil':add'4 :: Nat → nil':add'
Lemmas:
app'(_gen_nil':add'4(_n6), _gen_nil':add'4(b)) → _gen_nil':add'4(+(_n6, b)), rt ∈ Ω(1 + n6)
Generator Equations:
_gen_nil':add'4(0) ⇔ nil'
_gen_nil':add'4(+(x, 1)) ⇔ add'(_hole_head'3, _gen_nil':add'4(x))
The following defined symbols remain to be analysed:
reverse', shuff'
They will be analysed ascendingly in the following order:
reverse' < shuff'
Proved the following rewrite lemma:
reverse'(_gen_nil':add'4(_n908)) → _gen_nil':add'4(_n908), rt ∈ Ω(1 + n908 + n9082)
Induction Base:
reverse'(_gen_nil':add'4(0)) →RΩ(1)
nil'
Induction Step:
reverse'(_gen_nil':add'4(+(_$n909, 1))) →RΩ(1)
app'(reverse'(_gen_nil':add'4(_$n909)), add'(_hole_head'3, nil')) →IH
app'(_gen_nil':add'4(_$n909), add'(_hole_head'3, nil')) →LΩ(1 + $n909)
_gen_nil':add'4(+(_$n909, +(0, 1)))
We have rt ∈ Ω(n2) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n2).
Rules:
null'(nil') → true'
null'(add'(n, x)) → false'
tail'(add'(n, x)) → x
tail'(nil') → nil'
head'(add'(n, x)) → n
app'(nil', y) → y
app'(add'(n, x), y) → add'(n, app'(x, y))
reverse'(nil') → nil'
reverse'(add'(n, x)) → app'(reverse'(x), add'(n, nil'))
shuffle'(x) → shuff'(x, nil')
shuff'(x, y) → if'(null'(x), x, y, app'(y, add'(head'(x), nil')))
if'(true', x, y, z) → y
if'(false', x, y, z) → shuff'(reverse'(tail'(x)), z)
Types:
null' :: nil':add' → true':false'
nil' :: nil':add'
true' :: true':false'
add' :: head' → nil':add' → nil':add'
false' :: true':false'
tail' :: nil':add' → nil':add'
head' :: nil':add' → head'
app' :: nil':add' → nil':add' → nil':add'
reverse' :: nil':add' → nil':add'
shuffle' :: nil':add' → nil':add'
shuff' :: nil':add' → nil':add' → nil':add'
if' :: true':false' → nil':add' → nil':add' → nil':add' → nil':add'
_hole_true':false'1 :: true':false'
_hole_nil':add'2 :: nil':add'
_hole_head'3 :: head'
_gen_nil':add'4 :: Nat → nil':add'
Lemmas:
app'(_gen_nil':add'4(_n6), _gen_nil':add'4(b)) → _gen_nil':add'4(+(_n6, b)), rt ∈ Ω(1 + n6)
reverse'(_gen_nil':add'4(_n908)) → _gen_nil':add'4(_n908), rt ∈ Ω(1 + n908 + n9082)
Generator Equations:
_gen_nil':add'4(0) ⇔ nil'
_gen_nil':add'4(+(x, 1)) ⇔ add'(_hole_head'3, _gen_nil':add'4(x))
The following defined symbols remain to be analysed:
shuff'
Could not prove a rewrite lemma for the defined symbol shuff'.
Rules:
null'(nil') → true'
null'(add'(n, x)) → false'
tail'(add'(n, x)) → x
tail'(nil') → nil'
head'(add'(n, x)) → n
app'(nil', y) → y
app'(add'(n, x), y) → add'(n, app'(x, y))
reverse'(nil') → nil'
reverse'(add'(n, x)) → app'(reverse'(x), add'(n, nil'))
shuffle'(x) → shuff'(x, nil')
shuff'(x, y) → if'(null'(x), x, y, app'(y, add'(head'(x), nil')))
if'(true', x, y, z) → y
if'(false', x, y, z) → shuff'(reverse'(tail'(x)), z)
Types:
null' :: nil':add' → true':false'
nil' :: nil':add'
true' :: true':false'
add' :: head' → nil':add' → nil':add'
false' :: true':false'
tail' :: nil':add' → nil':add'
head' :: nil':add' → head'
app' :: nil':add' → nil':add' → nil':add'
reverse' :: nil':add' → nil':add'
shuffle' :: nil':add' → nil':add'
shuff' :: nil':add' → nil':add' → nil':add'
if' :: true':false' → nil':add' → nil':add' → nil':add' → nil':add'
_hole_true':false'1 :: true':false'
_hole_nil':add'2 :: nil':add'
_hole_head'3 :: head'
_gen_nil':add'4 :: Nat → nil':add'
Lemmas:
app'(_gen_nil':add'4(_n6), _gen_nil':add'4(b)) → _gen_nil':add'4(+(_n6, b)), rt ∈ Ω(1 + n6)
reverse'(_gen_nil':add'4(_n908)) → _gen_nil':add'4(_n908), rt ∈ Ω(1 + n908 + n9082)
Generator Equations:
_gen_nil':add'4(0) ⇔ nil'
_gen_nil':add'4(+(x, 1)) ⇔ add'(_hole_head'3, _gen_nil':add'4(x))
No more defined symbols left to analyse.
The lowerbound Ω(n2) was proven with the following lemma:
reverse'(_gen_nil':add'4(_n908)) → _gen_nil':add'4(_n908), rt ∈ Ω(1 + n908 + n9082)