foldl(x, Cons(S(0), xs)) → foldl(S(x), xs)
foldl(S(0), Cons(x, xs)) → foldl(S(x), xs)
foldr(a, Cons(x, xs)) → op(x, foldr(a, xs))
foldr(a, Nil) → a
foldl(a, Nil) → a
notEmpty(Cons(x, xs)) → True
notEmpty(Nil) → False
op(x, S(0)) → S(x)
op(S(0), y) → S(y)
fold(a, xs) → Cons(foldl(a, xs), Cons(foldr(a, xs), Nil))
Renamed function symbols to avoid clashes with predefined symbol.
Runtime Complexity TRS:
The TRS R consists of the following rules:
foldl'(x, Cons'(S'(0'), xs)) → foldl'(S'(x), xs)
foldl'(S'(0'), Cons'(x, xs)) → foldl'(S'(x), xs)
foldr'(a, Cons'(x, xs)) → op'(x, foldr'(a, xs))
foldr'(a, Nil') → a
foldl'(a, Nil') → a
notEmpty'(Cons'(x, xs)) → True'
notEmpty'(Nil') → False'
op'(x, S'(0')) → S'(x)
op'(S'(0'), y) → S'(y)
fold'(a, xs) → Cons'(foldl'(a, xs), Cons'(foldr'(a, xs), Nil'))
Infered types.
Rules:
foldl'(x, Cons'(S'(0'), xs)) → foldl'(S'(x), xs)
foldl'(S'(0'), Cons'(x, xs)) → foldl'(S'(x), xs)
foldr'(a, Cons'(x, xs)) → op'(x, foldr'(a, xs))
foldr'(a, Nil') → a
foldl'(a, Nil') → a
notEmpty'(Cons'(x, xs)) → True'
notEmpty'(Nil') → False'
op'(x, S'(0')) → S'(x)
op'(S'(0'), y) → S'(y)
fold'(a, xs) → Cons'(foldl'(a, xs), Cons'(foldr'(a, xs), Nil'))
Types:
foldl' :: 0':S' → Cons':Nil' → 0':S'
Cons' :: 0':S' → Cons':Nil' → Cons':Nil'
S' :: 0':S' → 0':S'
0' :: 0':S'
foldr' :: 0':S' → Cons':Nil' → 0':S'
op' :: 0':S' → 0':S' → 0':S'
Nil' :: Cons':Nil'
notEmpty' :: Cons':Nil' → True':False'
True' :: True':False'
False' :: True':False'
fold' :: 0':S' → Cons':Nil' → Cons':Nil'
_hole_0':S'1 :: 0':S'
_hole_Cons':Nil'2 :: Cons':Nil'
_hole_True':False'3 :: True':False'
_gen_0':S'4 :: Nat → 0':S'
_gen_Cons':Nil'5 :: Nat → Cons':Nil'
Heuristically decided to analyse the following defined symbols:
foldl', foldr'
Rules:
foldl'(x, Cons'(S'(0'), xs)) → foldl'(S'(x), xs)
foldl'(S'(0'), Cons'(x, xs)) → foldl'(S'(x), xs)
foldr'(a, Cons'(x, xs)) → op'(x, foldr'(a, xs))
foldr'(a, Nil') → a
foldl'(a, Nil') → a
notEmpty'(Cons'(x, xs)) → True'
notEmpty'(Nil') → False'
op'(x, S'(0')) → S'(x)
op'(S'(0'), y) → S'(y)
fold'(a, xs) → Cons'(foldl'(a, xs), Cons'(foldr'(a, xs), Nil'))
Types:
foldl' :: 0':S' → Cons':Nil' → 0':S'
Cons' :: 0':S' → Cons':Nil' → Cons':Nil'
S' :: 0':S' → 0':S'
0' :: 0':S'
foldr' :: 0':S' → Cons':Nil' → 0':S'
op' :: 0':S' → 0':S' → 0':S'
Nil' :: Cons':Nil'
notEmpty' :: Cons':Nil' → True':False'
True' :: True':False'
False' :: True':False'
fold' :: 0':S' → Cons':Nil' → Cons':Nil'
_hole_0':S'1 :: 0':S'
_hole_Cons':Nil'2 :: Cons':Nil'
_hole_True':False'3 :: True':False'
_gen_0':S'4 :: Nat → 0':S'
_gen_Cons':Nil'5 :: Nat → Cons':Nil'
Generator Equations:
_gen_0':S'4(0) ⇔ 0'
_gen_0':S'4(+(x, 1)) ⇔ S'(_gen_0':S'4(x))
_gen_Cons':Nil'5(0) ⇔ Nil'
_gen_Cons':Nil'5(+(x, 1)) ⇔ Cons'(0', _gen_Cons':Nil'5(x))
The following defined symbols remain to be analysed:
foldl', foldr'
Could not prove a rewrite lemma for the defined symbol foldl'.
Rules:
foldl'(x, Cons'(S'(0'), xs)) → foldl'(S'(x), xs)
foldl'(S'(0'), Cons'(x, xs)) → foldl'(S'(x), xs)
foldr'(a, Cons'(x, xs)) → op'(x, foldr'(a, xs))
foldr'(a, Nil') → a
foldl'(a, Nil') → a
notEmpty'(Cons'(x, xs)) → True'
notEmpty'(Nil') → False'
op'(x, S'(0')) → S'(x)
op'(S'(0'), y) → S'(y)
fold'(a, xs) → Cons'(foldl'(a, xs), Cons'(foldr'(a, xs), Nil'))
Types:
foldl' :: 0':S' → Cons':Nil' → 0':S'
Cons' :: 0':S' → Cons':Nil' → Cons':Nil'
S' :: 0':S' → 0':S'
0' :: 0':S'
foldr' :: 0':S' → Cons':Nil' → 0':S'
op' :: 0':S' → 0':S' → 0':S'
Nil' :: Cons':Nil'
notEmpty' :: Cons':Nil' → True':False'
True' :: True':False'
False' :: True':False'
fold' :: 0':S' → Cons':Nil' → Cons':Nil'
_hole_0':S'1 :: 0':S'
_hole_Cons':Nil'2 :: Cons':Nil'
_hole_True':False'3 :: True':False'
_gen_0':S'4 :: Nat → 0':S'
_gen_Cons':Nil'5 :: Nat → Cons':Nil'
Generator Equations:
_gen_0':S'4(0) ⇔ 0'
_gen_0':S'4(+(x, 1)) ⇔ S'(_gen_0':S'4(x))
_gen_Cons':Nil'5(0) ⇔ Nil'
_gen_Cons':Nil'5(+(x, 1)) ⇔ Cons'(0', _gen_Cons':Nil'5(x))
The following defined symbols remain to be analysed:
foldr'
Proved the following rewrite lemma:
foldr'(_gen_0':S'4(1), _gen_Cons':Nil'5(_n27)) → _gen_0':S'4(1), rt ∈ Ω(1 + n27)
Induction Base:
foldr'(_gen_0':S'4(1), _gen_Cons':Nil'5(0)) →RΩ(1)
_gen_0':S'4(1)
Induction Step:
foldr'(_gen_0':S'4(1), _gen_Cons':Nil'5(+(_$n28, 1))) →RΩ(1)
op'(0', foldr'(_gen_0':S'4(1), _gen_Cons':Nil'5(_$n28))) →IH
op'(0', _gen_0':S'4(1)) →RΩ(1)
S'(0')
We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).
Rules:
foldl'(x, Cons'(S'(0'), xs)) → foldl'(S'(x), xs)
foldl'(S'(0'), Cons'(x, xs)) → foldl'(S'(x), xs)
foldr'(a, Cons'(x, xs)) → op'(x, foldr'(a, xs))
foldr'(a, Nil') → a
foldl'(a, Nil') → a
notEmpty'(Cons'(x, xs)) → True'
notEmpty'(Nil') → False'
op'(x, S'(0')) → S'(x)
op'(S'(0'), y) → S'(y)
fold'(a, xs) → Cons'(foldl'(a, xs), Cons'(foldr'(a, xs), Nil'))
Types:
foldl' :: 0':S' → Cons':Nil' → 0':S'
Cons' :: 0':S' → Cons':Nil' → Cons':Nil'
S' :: 0':S' → 0':S'
0' :: 0':S'
foldr' :: 0':S' → Cons':Nil' → 0':S'
op' :: 0':S' → 0':S' → 0':S'
Nil' :: Cons':Nil'
notEmpty' :: Cons':Nil' → True':False'
True' :: True':False'
False' :: True':False'
fold' :: 0':S' → Cons':Nil' → Cons':Nil'
_hole_0':S'1 :: 0':S'
_hole_Cons':Nil'2 :: Cons':Nil'
_hole_True':False'3 :: True':False'
_gen_0':S'4 :: Nat → 0':S'
_gen_Cons':Nil'5 :: Nat → Cons':Nil'
Lemmas:
foldr'(_gen_0':S'4(1), _gen_Cons':Nil'5(_n27)) → _gen_0':S'4(1), rt ∈ Ω(1 + n27)
Generator Equations:
_gen_0':S'4(0) ⇔ 0'
_gen_0':S'4(+(x, 1)) ⇔ S'(_gen_0':S'4(x))
_gen_Cons':Nil'5(0) ⇔ Nil'
_gen_Cons':Nil'5(+(x, 1)) ⇔ Cons'(0', _gen_Cons':Nil'5(x))
No more defined symbols left to analyse.
The lowerbound Ω(n) was proven with the following lemma:
foldr'(_gen_0':S'4(1), _gen_Cons':Nil'5(_n27)) → _gen_0':S'4(1), rt ∈ Ω(1 + n27)