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(nil) → nil
shuffle(add(n, x)) → add(n, shuffle(reverse(x)))
Renamed function symbols to avoid clashes with predefined symbol.
Runtime Complexity TRS:
The TRS R consists of the following rules:
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'(nil') → nil'
shuffle'(add'(n, x)) → add'(n, shuffle'(reverse'(x)))
Sliced the following arguments:
add'/0
Runtime Complexity TRS:
The TRS R consists of the following rules:
app'(nil', y) → y
app'(add'(x), y) → add'(app'(x, y))
reverse'(nil') → nil'
reverse'(add'(x)) → app'(reverse'(x), add'(nil'))
shuffle'(nil') → nil'
shuffle'(add'(x)) → add'(shuffle'(reverse'(x)))
Infered types.
Rules:
app'(nil', y) → y
app'(add'(x), y) → add'(app'(x, y))
reverse'(nil') → nil'
reverse'(add'(x)) → app'(reverse'(x), add'(nil'))
shuffle'(nil') → nil'
shuffle'(add'(x)) → add'(shuffle'(reverse'(x)))
Types:
app' :: nil':add' → nil':add' → nil':add'
nil' :: nil':add'
add' :: nil':add' → nil':add'
reverse' :: nil':add' → nil':add'
shuffle' :: nil':add' → nil':add'
_hole_nil':add'1 :: nil':add'
_gen_nil':add'2 :: Nat → nil':add'
Heuristically decided to analyse the following defined symbols:
app', reverse', shuffle'
They will be analysed ascendingly in the following order:
app' < reverse'
reverse' < shuffle'
Rules:
app'(nil', y) → y
app'(add'(x), y) → add'(app'(x, y))
reverse'(nil') → nil'
reverse'(add'(x)) → app'(reverse'(x), add'(nil'))
shuffle'(nil') → nil'
shuffle'(add'(x)) → add'(shuffle'(reverse'(x)))
Types:
app' :: nil':add' → nil':add' → nil':add'
nil' :: nil':add'
add' :: nil':add' → nil':add'
reverse' :: nil':add' → nil':add'
shuffle' :: nil':add' → nil':add'
_hole_nil':add'1 :: nil':add'
_gen_nil':add'2 :: Nat → nil':add'
Generator Equations:
_gen_nil':add'2(0) ⇔ nil'
_gen_nil':add'2(+(x, 1)) ⇔ add'(_gen_nil':add'2(x))
The following defined symbols remain to be analysed:
app', reverse', shuffle'
They will be analysed ascendingly in the following order:
app' < reverse'
reverse' < shuffle'
Proved the following rewrite lemma:
app'(_gen_nil':add'2(_n4), _gen_nil':add'2(b)) → _gen_nil':add'2(+(_n4, b)), rt ∈ Ω(1 + n4)
Induction Base:
app'(_gen_nil':add'2(0), _gen_nil':add'2(b)) →RΩ(1)
_gen_nil':add'2(b)
Induction Step:
app'(_gen_nil':add'2(+(_$n5, 1)), _gen_nil':add'2(_b137)) →RΩ(1)
add'(app'(_gen_nil':add'2(_$n5), _gen_nil':add'2(_b137))) →IH
add'(_gen_nil':add'2(+(_$n5, _b137)))
We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).
Rules:
app'(nil', y) → y
app'(add'(x), y) → add'(app'(x, y))
reverse'(nil') → nil'
reverse'(add'(x)) → app'(reverse'(x), add'(nil'))
shuffle'(nil') → nil'
shuffle'(add'(x)) → add'(shuffle'(reverse'(x)))
Types:
app' :: nil':add' → nil':add' → nil':add'
nil' :: nil':add'
add' :: nil':add' → nil':add'
reverse' :: nil':add' → nil':add'
shuffle' :: nil':add' → nil':add'
_hole_nil':add'1 :: nil':add'
_gen_nil':add'2 :: Nat → nil':add'
Lemmas:
app'(_gen_nil':add'2(_n4), _gen_nil':add'2(b)) → _gen_nil':add'2(+(_n4, b)), rt ∈ Ω(1 + n4)
Generator Equations:
_gen_nil':add'2(0) ⇔ nil'
_gen_nil':add'2(+(x, 1)) ⇔ add'(_gen_nil':add'2(x))
The following defined symbols remain to be analysed:
reverse', shuffle'
They will be analysed ascendingly in the following order:
reverse' < shuffle'
Proved the following rewrite lemma:
reverse'(_gen_nil':add'2(_n395)) → _gen_nil':add'2(_n395), rt ∈ Ω(1 + n395 + n3952)
Induction Base:
reverse'(_gen_nil':add'2(0)) →RΩ(1)
nil'
Induction Step:
reverse'(_gen_nil':add'2(+(_$n396, 1))) →RΩ(1)
app'(reverse'(_gen_nil':add'2(_$n396)), add'(nil')) →IH
app'(_gen_nil':add'2(_$n396), add'(nil')) →LΩ(1 + $n396)
_gen_nil':add'2(+(_$n396, +(0, 1)))
We have rt ∈ Ω(n2) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n2).
Rules:
app'(nil', y) → y
app'(add'(x), y) → add'(app'(x, y))
reverse'(nil') → nil'
reverse'(add'(x)) → app'(reverse'(x), add'(nil'))
shuffle'(nil') → nil'
shuffle'(add'(x)) → add'(shuffle'(reverse'(x)))
Types:
app' :: nil':add' → nil':add' → nil':add'
nil' :: nil':add'
add' :: nil':add' → nil':add'
reverse' :: nil':add' → nil':add'
shuffle' :: nil':add' → nil':add'
_hole_nil':add'1 :: nil':add'
_gen_nil':add'2 :: Nat → nil':add'
Lemmas:
app'(_gen_nil':add'2(_n4), _gen_nil':add'2(b)) → _gen_nil':add'2(+(_n4, b)), rt ∈ Ω(1 + n4)
reverse'(_gen_nil':add'2(_n395)) → _gen_nil':add'2(_n395), rt ∈ Ω(1 + n395 + n3952)
Generator Equations:
_gen_nil':add'2(0) ⇔ nil'
_gen_nil':add'2(+(x, 1)) ⇔ add'(_gen_nil':add'2(x))
The following defined symbols remain to be analysed:
shuffle'
Proved the following rewrite lemma:
shuffle'(_gen_nil':add'2(_n738)) → _gen_nil':add'2(_n738), rt ∈ Ω(1 + n738 + n7382 + n7383)
Induction Base:
shuffle'(_gen_nil':add'2(0)) →RΩ(1)
nil'
Induction Step:
shuffle'(_gen_nil':add'2(+(_$n739, 1))) →RΩ(1)
add'(shuffle'(reverse'(_gen_nil':add'2(_$n739)))) →LΩ(1 + $n739 + $n7392)
add'(shuffle'(_gen_nil':add'2(_$n739))) →IH
add'(_gen_nil':add'2(_$n739))
We have rt ∈ Ω(n3) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n3).
Rules:
app'(nil', y) → y
app'(add'(x), y) → add'(app'(x, y))
reverse'(nil') → nil'
reverse'(add'(x)) → app'(reverse'(x), add'(nil'))
shuffle'(nil') → nil'
shuffle'(add'(x)) → add'(shuffle'(reverse'(x)))
Types:
app' :: nil':add' → nil':add' → nil':add'
nil' :: nil':add'
add' :: nil':add' → nil':add'
reverse' :: nil':add' → nil':add'
shuffle' :: nil':add' → nil':add'
_hole_nil':add'1 :: nil':add'
_gen_nil':add'2 :: Nat → nil':add'
Lemmas:
app'(_gen_nil':add'2(_n4), _gen_nil':add'2(b)) → _gen_nil':add'2(+(_n4, b)), rt ∈ Ω(1 + n4)
reverse'(_gen_nil':add'2(_n395)) → _gen_nil':add'2(_n395), rt ∈ Ω(1 + n395 + n3952)
shuffle'(_gen_nil':add'2(_n738)) → _gen_nil':add'2(_n738), rt ∈ Ω(1 + n738 + n7382 + n7383)
Generator Equations:
_gen_nil':add'2(0) ⇔ nil'
_gen_nil':add'2(+(x, 1)) ⇔ add'(_gen_nil':add'2(x))
No more defined symbols left to analyse.
The lowerbound Ω(n3) was proven with the following lemma:
shuffle'(_gen_nil':add'2(_n738)) → _gen_nil':add'2(_n738), rt ∈ Ω(1 + n738 + n7382 + n7383)