f(x, nil) → g(nil, x)
f(x, g(y, z)) → g(f(x, y), z)
++(x, nil) → x
++(x, g(y, z)) → g(++(x, y), z)
null(nil) → true
null(g(x, y)) → false
mem(nil, y) → false
mem(g(x, y), z) → or(=(y, z), mem(x, z))
mem(x, max(x)) → not(null(x))
max(g(g(nil, x), y)) → max'(x, y)
max(g(g(g(x, y), z), u)) → max'(max(g(g(x, y), z)), u)
Renamed function symbols to avoid clashes with predefined symbol.
Runtime Complexity TRS:
The TRS R consists of the following rules:
f'(x, nil') → g'(nil', x)
f'(x, g'(y, z)) → g'(f'(x, y), z)
++'(x, nil') → x
++'(x, g'(y, z)) → g'(++'(x, y), z)
null'(nil') → true'
null'(g'(x, y)) → false'
mem'(nil', y) → false'
mem'(g'(x, y), z) → or'(='(y, z), mem'(x, z))
mem'(x, max''(x)) → not'(null'(x))
max''(g'(g'(nil', x), y)) → max'''(x, y)
max''(g'(g'(g'(x, y), z), u')) → max'''(max''(g'(g'(x, y), z)), u')
Sliced the following arguments:
or'/0
='/0
='/1
max'''/1
Runtime Complexity TRS:
The TRS R consists of the following rules:
f'(x, nil') → g'(nil', x)
f'(x, g'(y, z)) → g'(f'(x, y), z)
++'(x, nil') → x
++'(x, g'(y, z)) → g'(++'(x, y), z)
null'(nil') → true'
null'(g'(x, y)) → false'
mem'(nil', y) → false'
mem'(g'(x, y), z) → or'(mem'(x, z))
mem'(x, max''(x)) → not'(null'(x))
max''(g'(g'(nil', x), y)) → max'''(x)
max''(g'(g'(g'(x, y), z), u')) → max'''(max''(g'(g'(x, y), z)))
Infered types.
Rules:
f'(x, nil') → g'(nil', x)
f'(x, g'(y, z)) → g'(f'(x, y), z)
++'(x, nil') → x
++'(x, g'(y, z)) → g'(++'(x, y), z)
null'(nil') → true'
null'(g'(x, y)) → false'
mem'(nil', y) → false'
mem'(g'(x, y), z) → or'(mem'(x, z))
mem'(x, max''(x)) → not'(null'(x))
max''(g'(g'(nil', x), y)) → max'''(x)
max''(g'(g'(g'(x, y), z), u')) → max'''(max''(g'(g'(x, y), z)))
Types:
f' :: max''':u' → nil':g' → nil':g'
nil' :: nil':g'
g' :: nil':g' → max''':u' → nil':g'
++' :: nil':g' → nil':g' → nil':g'
null' :: nil':g' → true':false':or':not'
true' :: true':false':or':not'
false' :: true':false':or':not'
mem' :: nil':g' → max''':u' → true':false':or':not'
or' :: true':false':or':not' → true':false':or':not'
max'' :: nil':g' → max''':u'
not' :: true':false':or':not' → true':false':or':not'
max''' :: max''':u' → max''':u'
u' :: max''':u'
_hole_nil':g'1 :: nil':g'
_hole_max''':u'2 :: max''':u'
_hole_true':false':or':not'3 :: true':false':or':not'
_gen_nil':g'4 :: Nat → nil':g'
_gen_max''':u'5 :: Nat → max''':u'
_gen_true':false':or':not'6 :: Nat → true':false':or':not'
Heuristically decided to analyse the following defined symbols:
f', ++', mem', max''
Rules:
f'(x, nil') → g'(nil', x)
f'(x, g'(y, z)) → g'(f'(x, y), z)
++'(x, nil') → x
++'(x, g'(y, z)) → g'(++'(x, y), z)
null'(nil') → true'
null'(g'(x, y)) → false'
mem'(nil', y) → false'
mem'(g'(x, y), z) → or'(mem'(x, z))
mem'(x, max''(x)) → not'(null'(x))
max''(g'(g'(nil', x), y)) → max'''(x)
max''(g'(g'(g'(x, y), z), u')) → max'''(max''(g'(g'(x, y), z)))
Types:
f' :: max''':u' → nil':g' → nil':g'
nil' :: nil':g'
g' :: nil':g' → max''':u' → nil':g'
++' :: nil':g' → nil':g' → nil':g'
null' :: nil':g' → true':false':or':not'
true' :: true':false':or':not'
false' :: true':false':or':not'
mem' :: nil':g' → max''':u' → true':false':or':not'
or' :: true':false':or':not' → true':false':or':not'
max'' :: nil':g' → max''':u'
not' :: true':false':or':not' → true':false':or':not'
max''' :: max''':u' → max''':u'
u' :: max''':u'
_hole_nil':g'1 :: nil':g'
_hole_max''':u'2 :: max''':u'
_hole_true':false':or':not'3 :: true':false':or':not'
_gen_nil':g'4 :: Nat → nil':g'
_gen_max''':u'5 :: Nat → max''':u'
_gen_true':false':or':not'6 :: Nat → true':false':or':not'
Generator Equations:
_gen_nil':g'4(0) ⇔ nil'
_gen_nil':g'4(+(x, 1)) ⇔ g'(_gen_nil':g'4(x), u')
_gen_max''':u'5(0) ⇔ u'
_gen_max''':u'5(+(x, 1)) ⇔ max'''(_gen_max''':u'5(x))
_gen_true':false':or':not'6(0) ⇔ true'
_gen_true':false':or':not'6(+(x, 1)) ⇔ or'(_gen_true':false':or':not'6(x))
The following defined symbols remain to be analysed:
f', ++', mem', max''
Proved the following rewrite lemma:
f'(_gen_max''':u'5(a), _gen_nil':g'4(+(1, _n8))) → _*7, rt ∈ Ω(n8)
Induction Base:
f'(_gen_max''':u'5(a), _gen_nil':g'4(+(1, 0)))
Induction Step:
f'(_gen_max''':u'5(_a548903), _gen_nil':g'4(+(1, +(_$n9, 1)))) →RΩ(1)
g'(f'(_gen_max''':u'5(_a548903), _gen_nil':g'4(+(1, _$n9))), u') →IH
g'(_*7, u')
We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).
Rules:
f'(x, nil') → g'(nil', x)
f'(x, g'(y, z)) → g'(f'(x, y), z)
++'(x, nil') → x
++'(x, g'(y, z)) → g'(++'(x, y), z)
null'(nil') → true'
null'(g'(x, y)) → false'
mem'(nil', y) → false'
mem'(g'(x, y), z) → or'(mem'(x, z))
mem'(x, max''(x)) → not'(null'(x))
max''(g'(g'(nil', x), y)) → max'''(x)
max''(g'(g'(g'(x, y), z), u')) → max'''(max''(g'(g'(x, y), z)))
Types:
f' :: max''':u' → nil':g' → nil':g'
nil' :: nil':g'
g' :: nil':g' → max''':u' → nil':g'
++' :: nil':g' → nil':g' → nil':g'
null' :: nil':g' → true':false':or':not'
true' :: true':false':or':not'
false' :: true':false':or':not'
mem' :: nil':g' → max''':u' → true':false':or':not'
or' :: true':false':or':not' → true':false':or':not'
max'' :: nil':g' → max''':u'
not' :: true':false':or':not' → true':false':or':not'
max''' :: max''':u' → max''':u'
u' :: max''':u'
_hole_nil':g'1 :: nil':g'
_hole_max''':u'2 :: max''':u'
_hole_true':false':or':not'3 :: true':false':or':not'
_gen_nil':g'4 :: Nat → nil':g'
_gen_max''':u'5 :: Nat → max''':u'
_gen_true':false':or':not'6 :: Nat → true':false':or':not'
Lemmas:
f'(_gen_max''':u'5(a), _gen_nil':g'4(+(1, _n8))) → _*7, rt ∈ Ω(n8)
Generator Equations:
_gen_nil':g'4(0) ⇔ nil'
_gen_nil':g'4(+(x, 1)) ⇔ g'(_gen_nil':g'4(x), u')
_gen_max''':u'5(0) ⇔ u'
_gen_max''':u'5(+(x, 1)) ⇔ max'''(_gen_max''':u'5(x))
_gen_true':false':or':not'6(0) ⇔ true'
_gen_true':false':or':not'6(+(x, 1)) ⇔ or'(_gen_true':false':or':not'6(x))
The following defined symbols remain to be analysed:
++', mem', max''
Proved the following rewrite lemma:
++'(_gen_nil':g'4(a), _gen_nil':g'4(_n549440)) → _gen_nil':g'4(+(_n549440, a)), rt ∈ Ω(1 + n549440)
Induction Base:
++'(_gen_nil':g'4(a), _gen_nil':g'4(0)) →RΩ(1)
_gen_nil':g'4(a)
Induction Step:
++'(_gen_nil':g'4(_a549713), _gen_nil':g'4(+(_$n549441, 1))) →RΩ(1)
g'(++'(_gen_nil':g'4(_a549713), _gen_nil':g'4(_$n549441)), u') →IH
g'(_gen_nil':g'4(+(_$n549441, _a549713)), u')
We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).
Rules:
f'(x, nil') → g'(nil', x)
f'(x, g'(y, z)) → g'(f'(x, y), z)
++'(x, nil') → x
++'(x, g'(y, z)) → g'(++'(x, y), z)
null'(nil') → true'
null'(g'(x, y)) → false'
mem'(nil', y) → false'
mem'(g'(x, y), z) → or'(mem'(x, z))
mem'(x, max''(x)) → not'(null'(x))
max''(g'(g'(nil', x), y)) → max'''(x)
max''(g'(g'(g'(x, y), z), u')) → max'''(max''(g'(g'(x, y), z)))
Types:
f' :: max''':u' → nil':g' → nil':g'
nil' :: nil':g'
g' :: nil':g' → max''':u' → nil':g'
++' :: nil':g' → nil':g' → nil':g'
null' :: nil':g' → true':false':or':not'
true' :: true':false':or':not'
false' :: true':false':or':not'
mem' :: nil':g' → max''':u' → true':false':or':not'
or' :: true':false':or':not' → true':false':or':not'
max'' :: nil':g' → max''':u'
not' :: true':false':or':not' → true':false':or':not'
max''' :: max''':u' → max''':u'
u' :: max''':u'
_hole_nil':g'1 :: nil':g'
_hole_max''':u'2 :: max''':u'
_hole_true':false':or':not'3 :: true':false':or':not'
_gen_nil':g'4 :: Nat → nil':g'
_gen_max''':u'5 :: Nat → max''':u'
_gen_true':false':or':not'6 :: Nat → true':false':or':not'
Lemmas:
f'(_gen_max''':u'5(a), _gen_nil':g'4(+(1, _n8))) → _*7, rt ∈ Ω(n8)
++'(_gen_nil':g'4(a), _gen_nil':g'4(_n549440)) → _gen_nil':g'4(+(_n549440, a)), rt ∈ Ω(1 + n549440)
Generator Equations:
_gen_nil':g'4(0) ⇔ nil'
_gen_nil':g'4(+(x, 1)) ⇔ g'(_gen_nil':g'4(x), u')
_gen_max''':u'5(0) ⇔ u'
_gen_max''':u'5(+(x, 1)) ⇔ max'''(_gen_max''':u'5(x))
_gen_true':false':or':not'6(0) ⇔ true'
_gen_true':false':or':not'6(+(x, 1)) ⇔ or'(_gen_true':false':or':not'6(x))
The following defined symbols remain to be analysed:
mem', max''
Proved the following rewrite lemma:
mem'(_gen_nil':g'4(+(1, _n550446)), _gen_max''':u'5(b)) → _*7, rt ∈ Ω(n550446)
Induction Base:
mem'(_gen_nil':g'4(+(1, 0)), _gen_max''':u'5(b))
Induction Step:
mem'(_gen_nil':g'4(+(1, +(_$n550447, 1))), _gen_max''':u'5(_b554002)) →RΩ(1)
or'(mem'(_gen_nil':g'4(+(1, _$n550447)), _gen_max''':u'5(_b554002))) →IH
or'(_*7)
We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).
Rules:
f'(x, nil') → g'(nil', x)
f'(x, g'(y, z)) → g'(f'(x, y), z)
++'(x, nil') → x
++'(x, g'(y, z)) → g'(++'(x, y), z)
null'(nil') → true'
null'(g'(x, y)) → false'
mem'(nil', y) → false'
mem'(g'(x, y), z) → or'(mem'(x, z))
mem'(x, max''(x)) → not'(null'(x))
max''(g'(g'(nil', x), y)) → max'''(x)
max''(g'(g'(g'(x, y), z), u')) → max'''(max''(g'(g'(x, y), z)))
Types:
f' :: max''':u' → nil':g' → nil':g'
nil' :: nil':g'
g' :: nil':g' → max''':u' → nil':g'
++' :: nil':g' → nil':g' → nil':g'
null' :: nil':g' → true':false':or':not'
true' :: true':false':or':not'
false' :: true':false':or':not'
mem' :: nil':g' → max''':u' → true':false':or':not'
or' :: true':false':or':not' → true':false':or':not'
max'' :: nil':g' → max''':u'
not' :: true':false':or':not' → true':false':or':not'
max''' :: max''':u' → max''':u'
u' :: max''':u'
_hole_nil':g'1 :: nil':g'
_hole_max''':u'2 :: max''':u'
_hole_true':false':or':not'3 :: true':false':or':not'
_gen_nil':g'4 :: Nat → nil':g'
_gen_max''':u'5 :: Nat → max''':u'
_gen_true':false':or':not'6 :: Nat → true':false':or':not'
Lemmas:
f'(_gen_max''':u'5(a), _gen_nil':g'4(+(1, _n8))) → _*7, rt ∈ Ω(n8)
++'(_gen_nil':g'4(a), _gen_nil':g'4(_n549440)) → _gen_nil':g'4(+(_n549440, a)), rt ∈ Ω(1 + n549440)
mem'(_gen_nil':g'4(+(1, _n550446)), _gen_max''':u'5(b)) → _*7, rt ∈ Ω(n550446)
Generator Equations:
_gen_nil':g'4(0) ⇔ nil'
_gen_nil':g'4(+(x, 1)) ⇔ g'(_gen_nil':g'4(x), u')
_gen_max''':u'5(0) ⇔ u'
_gen_max''':u'5(+(x, 1)) ⇔ max'''(_gen_max''':u'5(x))
_gen_true':false':or':not'6(0) ⇔ true'
_gen_true':false':or':not'6(+(x, 1)) ⇔ or'(_gen_true':false':or':not'6(x))
The following defined symbols remain to be analysed:
max''
Proved the following rewrite lemma:
max''(_gen_nil':g'4(+(2, _n554614))) → _gen_max''':u'5(+(1, _n554614)), rt ∈ Ω(1 + n554614)
Induction Base:
max''(_gen_nil':g'4(+(2, 0))) →RΩ(1)
max'''(u')
Induction Step:
max''(_gen_nil':g'4(+(2, +(_$n554615, 1)))) →RΩ(1)
max'''(max''(g'(g'(_gen_nil':g'4(_$n554615), u'), u'))) →IH
max'''(_gen_max''':u'5(+(1, _$n554615)))
We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).
Rules:
f'(x, nil') → g'(nil', x)
f'(x, g'(y, z)) → g'(f'(x, y), z)
++'(x, nil') → x
++'(x, g'(y, z)) → g'(++'(x, y), z)
null'(nil') → true'
null'(g'(x, y)) → false'
mem'(nil', y) → false'
mem'(g'(x, y), z) → or'(mem'(x, z))
mem'(x, max''(x)) → not'(null'(x))
max''(g'(g'(nil', x), y)) → max'''(x)
max''(g'(g'(g'(x, y), z), u')) → max'''(max''(g'(g'(x, y), z)))
Types:
f' :: max''':u' → nil':g' → nil':g'
nil' :: nil':g'
g' :: nil':g' → max''':u' → nil':g'
++' :: nil':g' → nil':g' → nil':g'
null' :: nil':g' → true':false':or':not'
true' :: true':false':or':not'
false' :: true':false':or':not'
mem' :: nil':g' → max''':u' → true':false':or':not'
or' :: true':false':or':not' → true':false':or':not'
max'' :: nil':g' → max''':u'
not' :: true':false':or':not' → true':false':or':not'
max''' :: max''':u' → max''':u'
u' :: max''':u'
_hole_nil':g'1 :: nil':g'
_hole_max''':u'2 :: max''':u'
_hole_true':false':or':not'3 :: true':false':or':not'
_gen_nil':g'4 :: Nat → nil':g'
_gen_max''':u'5 :: Nat → max''':u'
_gen_true':false':or':not'6 :: Nat → true':false':or':not'
Lemmas:
f'(_gen_max''':u'5(a), _gen_nil':g'4(+(1, _n8))) → _*7, rt ∈ Ω(n8)
++'(_gen_nil':g'4(a), _gen_nil':g'4(_n549440)) → _gen_nil':g'4(+(_n549440, a)), rt ∈ Ω(1 + n549440)
mem'(_gen_nil':g'4(+(1, _n550446)), _gen_max''':u'5(b)) → _*7, rt ∈ Ω(n550446)
max''(_gen_nil':g'4(+(2, _n554614))) → _gen_max''':u'5(+(1, _n554614)), rt ∈ Ω(1 + n554614)
Generator Equations:
_gen_nil':g'4(0) ⇔ nil'
_gen_nil':g'4(+(x, 1)) ⇔ g'(_gen_nil':g'4(x), u')
_gen_max''':u'5(0) ⇔ u'
_gen_max''':u'5(+(x, 1)) ⇔ max'''(_gen_max''':u'5(x))
_gen_true':false':or':not'6(0) ⇔ true'
_gen_true':false':or':not'6(+(x, 1)) ⇔ or'(_gen_true':false':or':not'6(x))
No more defined symbols left to analyse.
The lowerbound Ω(n) was proven with the following lemma:
f'(_gen_max''':u'5(a), _gen_nil':g'4(+(1, _n8))) → _*7, rt ∈ Ω(n8)