0(#) → #
+(x, #) → x
+(#, x) → x
+(0(x), 0(y)) → 0(+(x, y))
+(0(x), 1(y)) → 1(+(x, y))
+(1(x), 0(y)) → 1(+(x, y))
+(1(x), 1(y)) → 0(+(+(x, y), 1(#)))
+(x, +(y, z)) → +(+(x, y), z)
-(x, #) → x
-(#, x) → #
-(0(x), 0(y)) → 0(-(x, y))
-(0(x), 1(y)) → 1(-(-(x, y), 1(#)))
-(1(x), 0(y)) → 1(-(x, y))
-(1(x), 1(y)) → 0(-(x, y))
not(false) → true
not(true) → false
and(x, true) → x
and(x, false) → false
if(true, x, y) → x
if(false, x, y) → y
ge(0(x), 0(y)) → ge(x, y)
ge(0(x), 1(y)) → not(ge(y, x))
ge(1(x), 0(y)) → ge(x, y)
ge(1(x), 1(y)) → ge(x, y)
ge(x, #) → true
ge(#, 1(x)) → false
ge(#, 0(x)) → ge(#, x)
val(l(x)) → x
val(n(x, y, z)) → x
min(l(x)) → x
min(n(x, y, z)) → min(y)
max(l(x)) → x
max(n(x, y, z)) → max(z)
bs(l(x)) → true
bs(n(x, y, z)) → and(and(ge(x, max(y)), ge(min(z), x)), and(bs(y), bs(z)))
size(l(x)) → 1(#)
size(n(x, y, z)) → +(+(size(x), size(y)), 1(#))
wb(l(x)) → true
wb(n(x, y, z)) → and(if(ge(size(y), size(z)), ge(1(#), -(size(y), size(z))), ge(1(#), -(size(z), size(y)))), and(wb(y), wb(z)))
Renamed function symbols to avoid clashes with predefined symbol.
Runtime Complexity TRS:
The TRS R consists of the following rules:
0'(#') → #'
+'(x, #') → x
+'(#', x) → x
+'(0'(x), 0'(y)) → 0'(+'(x, y))
+'(0'(x), 1'(y)) → 1'(+'(x, y))
+'(1'(x), 0'(y)) → 1'(+'(x, y))
+'(1'(x), 1'(y)) → 0'(+'(+'(x, y), 1'(#')))
+'(x, +'(y, z)) → +'(+'(x, y), z)
-'(x, #') → x
-'(#', x) → #'
-'(0'(x), 0'(y)) → 0'(-'(x, y))
-'(0'(x), 1'(y)) → 1'(-'(-'(x, y), 1'(#')))
-'(1'(x), 0'(y)) → 1'(-'(x, y))
-'(1'(x), 1'(y)) → 0'(-'(x, y))
not'(false') → true'
not'(true') → false'
and'(x, true') → x
and'(x, false') → false'
if'(true', x, y) → x
if'(false', x, y) → y
ge'(0'(x), 0'(y)) → ge'(x, y)
ge'(0'(x), 1'(y)) → not'(ge'(y, x))
ge'(1'(x), 0'(y)) → ge'(x, y)
ge'(1'(x), 1'(y)) → ge'(x, y)
ge'(x, #') → true'
ge'(#', 1'(x)) → false'
ge'(#', 0'(x)) → ge'(#', x)
val'(l'(x)) → x
val'(n'(x, y, z)) → x
min'(l'(x)) → x
min'(n'(x, y, z)) → min'(y)
max'(l'(x)) → x
max'(n'(x, y, z)) → max'(z)
bs'(l'(x)) → true'
bs'(n'(x, y, z)) → and'(and'(ge'(x, max'(y)), ge'(min'(z), x)), and'(bs'(y), bs'(z)))
size'(l'(x)) → 1'(#')
size'(n'(x, y, z)) → +'(+'(size'(x), size'(y)), 1'(#'))
wb'(l'(x)) → true'
wb'(n'(x, y, z)) → and'(if'(ge'(size'(y), size'(z)), ge'(1'(#'), -'(size'(y), size'(z))), ge'(1'(#'), -'(size'(z), size'(y)))), and'(wb'(y), wb'(z)))
Infered types.
Rules:
0'(#') → #'
+'(x, #') → x
+'(#', x) → x
+'(0'(x), 0'(y)) → 0'(+'(x, y))
+'(0'(x), 1'(y)) → 1'(+'(x, y))
+'(1'(x), 0'(y)) → 1'(+'(x, y))
+'(1'(x), 1'(y)) → 0'(+'(+'(x, y), 1'(#')))
+'(x, +'(y, z)) → +'(+'(x, y), z)
-'(x, #') → x
-'(#', x) → #'
-'(0'(x), 0'(y)) → 0'(-'(x, y))
-'(0'(x), 1'(y)) → 1'(-'(-'(x, y), 1'(#')))
-'(1'(x), 0'(y)) → 1'(-'(x, y))
-'(1'(x), 1'(y)) → 0'(-'(x, y))
not'(false') → true'
not'(true') → false'
and'(x, true') → x
and'(x, false') → false'
if'(true', x, y) → x
if'(false', x, y) → y
ge'(0'(x), 0'(y)) → ge'(x, y)
ge'(0'(x), 1'(y)) → not'(ge'(y, x))
ge'(1'(x), 0'(y)) → ge'(x, y)
ge'(1'(x), 1'(y)) → ge'(x, y)
ge'(x, #') → true'
ge'(#', 1'(x)) → false'
ge'(#', 0'(x)) → ge'(#', x)
val'(l'(x)) → x
val'(n'(x, y, z)) → x
min'(l'(x)) → x
min'(n'(x, y, z)) → min'(y)
max'(l'(x)) → x
max'(n'(x, y, z)) → max'(z)
bs'(l'(x)) → true'
bs'(n'(x, y, z)) → and'(and'(ge'(x, max'(y)), ge'(min'(z), x)), and'(bs'(y), bs'(z)))
size'(l'(x)) → 1'(#')
size'(n'(x, y, z)) → +'(+'(size'(x), size'(y)), 1'(#'))
wb'(l'(x)) → true'
wb'(n'(x, y, z)) → and'(if'(ge'(size'(y), size'(z)), ge'(1'(#'), -'(size'(y), size'(z))), ge'(1'(#'), -'(size'(z), size'(y)))), and'(wb'(y), wb'(z)))
Types:
0' :: #':1':l':n' → #':1':l':n'
#' :: #':1':l':n'
+' :: #':1':l':n' → #':1':l':n' → #':1':l':n'
1' :: #':1':l':n' → #':1':l':n'
-' :: #':1':l':n' → #':1':l':n' → #':1':l':n'
not' :: false':true' → false':true'
false' :: false':true'
true' :: false':true'
and' :: false':true' → false':true' → false':true'
if' :: false':true' → false':true' → false':true' → false':true'
ge' :: #':1':l':n' → #':1':l':n' → false':true'
val' :: #':1':l':n' → #':1':l':n'
l' :: #':1':l':n' → #':1':l':n'
n' :: #':1':l':n' → #':1':l':n' → #':1':l':n' → #':1':l':n'
min' :: #':1':l':n' → #':1':l':n'
max' :: #':1':l':n' → #':1':l':n'
bs' :: #':1':l':n' → false':true'
size' :: #':1':l':n' → #':1':l':n'
wb' :: #':1':l':n' → false':true'
_hole_#':1':l':n'1 :: #':1':l':n'
_hole_false':true'2 :: false':true'
_gen_#':1':l':n'3 :: Nat → #':1':l':n'
Heuristically decided to analyse the following defined symbols:
+', -', ge', min', max', bs', size', wb'
They will be analysed ascendingly in the following order:
+' < size'
-' < wb'
ge' < bs'
ge' < wb'
min' < bs'
max' < bs'
size' < wb'
Rules:
0'(#') → #'
+'(x, #') → x
+'(#', x) → x
+'(0'(x), 0'(y)) → 0'(+'(x, y))
+'(0'(x), 1'(y)) → 1'(+'(x, y))
+'(1'(x), 0'(y)) → 1'(+'(x, y))
+'(1'(x), 1'(y)) → 0'(+'(+'(x, y), 1'(#')))
+'(x, +'(y, z)) → +'(+'(x, y), z)
-'(x, #') → x
-'(#', x) → #'
-'(0'(x), 0'(y)) → 0'(-'(x, y))
-'(0'(x), 1'(y)) → 1'(-'(-'(x, y), 1'(#')))
-'(1'(x), 0'(y)) → 1'(-'(x, y))
-'(1'(x), 1'(y)) → 0'(-'(x, y))
not'(false') → true'
not'(true') → false'
and'(x, true') → x
and'(x, false') → false'
if'(true', x, y) → x
if'(false', x, y) → y
ge'(0'(x), 0'(y)) → ge'(x, y)
ge'(0'(x), 1'(y)) → not'(ge'(y, x))
ge'(1'(x), 0'(y)) → ge'(x, y)
ge'(1'(x), 1'(y)) → ge'(x, y)
ge'(x, #') → true'
ge'(#', 1'(x)) → false'
ge'(#', 0'(x)) → ge'(#', x)
val'(l'(x)) → x
val'(n'(x, y, z)) → x
min'(l'(x)) → x
min'(n'(x, y, z)) → min'(y)
max'(l'(x)) → x
max'(n'(x, y, z)) → max'(z)
bs'(l'(x)) → true'
bs'(n'(x, y, z)) → and'(and'(ge'(x, max'(y)), ge'(min'(z), x)), and'(bs'(y), bs'(z)))
size'(l'(x)) → 1'(#')
size'(n'(x, y, z)) → +'(+'(size'(x), size'(y)), 1'(#'))
wb'(l'(x)) → true'
wb'(n'(x, y, z)) → and'(if'(ge'(size'(y), size'(z)), ge'(1'(#'), -'(size'(y), size'(z))), ge'(1'(#'), -'(size'(z), size'(y)))), and'(wb'(y), wb'(z)))
Types:
0' :: #':1':l':n' → #':1':l':n'
#' :: #':1':l':n'
+' :: #':1':l':n' → #':1':l':n' → #':1':l':n'
1' :: #':1':l':n' → #':1':l':n'
-' :: #':1':l':n' → #':1':l':n' → #':1':l':n'
not' :: false':true' → false':true'
false' :: false':true'
true' :: false':true'
and' :: false':true' → false':true' → false':true'
if' :: false':true' → false':true' → false':true' → false':true'
ge' :: #':1':l':n' → #':1':l':n' → false':true'
val' :: #':1':l':n' → #':1':l':n'
l' :: #':1':l':n' → #':1':l':n'
n' :: #':1':l':n' → #':1':l':n' → #':1':l':n' → #':1':l':n'
min' :: #':1':l':n' → #':1':l':n'
max' :: #':1':l':n' → #':1':l':n'
bs' :: #':1':l':n' → false':true'
size' :: #':1':l':n' → #':1':l':n'
wb' :: #':1':l':n' → false':true'
_hole_#':1':l':n'1 :: #':1':l':n'
_hole_false':true'2 :: false':true'
_gen_#':1':l':n'3 :: Nat → #':1':l':n'
Generator Equations:
_gen_#':1':l':n'3(0) ⇔ #'
_gen_#':1':l':n'3(+(x, 1)) ⇔ 1'(_gen_#':1':l':n'3(x))
The following defined symbols remain to be analysed:
+', -', ge', min', max', bs', size', wb'
They will be analysed ascendingly in the following order:
+' < size'
-' < wb'
ge' < bs'
ge' < wb'
min' < bs'
max' < bs'
size' < wb'
Proved the following rewrite lemma:
+'(_gen_#':1':l':n'3(+(1, _n5)), _gen_#':1':l':n'3(+(1, _n5))) → _*4, rt ∈ Ω(n5)
Induction Base:
+'(_gen_#':1':l':n'3(+(1, 0)), _gen_#':1':l':n'3(+(1, 0)))
Induction Step:
+'(_gen_#':1':l':n'3(+(1, +(_$n6, 1))), _gen_#':1':l':n'3(+(1, +(_$n6, 1)))) →RΩ(1)
0'(+'(+'(_gen_#':1':l':n'3(+(1, _$n6)), _gen_#':1':l':n'3(+(1, _$n6))), 1'(#'))) →IH
0'(+'(_*4, 1'(#')))
We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).
Rules:
0'(#') → #'
+'(x, #') → x
+'(#', x) → x
+'(0'(x), 0'(y)) → 0'(+'(x, y))
+'(0'(x), 1'(y)) → 1'(+'(x, y))
+'(1'(x), 0'(y)) → 1'(+'(x, y))
+'(1'(x), 1'(y)) → 0'(+'(+'(x, y), 1'(#')))
+'(x, +'(y, z)) → +'(+'(x, y), z)
-'(x, #') → x
-'(#', x) → #'
-'(0'(x), 0'(y)) → 0'(-'(x, y))
-'(0'(x), 1'(y)) → 1'(-'(-'(x, y), 1'(#')))
-'(1'(x), 0'(y)) → 1'(-'(x, y))
-'(1'(x), 1'(y)) → 0'(-'(x, y))
not'(false') → true'
not'(true') → false'
and'(x, true') → x
and'(x, false') → false'
if'(true', x, y) → x
if'(false', x, y) → y
ge'(0'(x), 0'(y)) → ge'(x, y)
ge'(0'(x), 1'(y)) → not'(ge'(y, x))
ge'(1'(x), 0'(y)) → ge'(x, y)
ge'(1'(x), 1'(y)) → ge'(x, y)
ge'(x, #') → true'
ge'(#', 1'(x)) → false'
ge'(#', 0'(x)) → ge'(#', x)
val'(l'(x)) → x
val'(n'(x, y, z)) → x
min'(l'(x)) → x
min'(n'(x, y, z)) → min'(y)
max'(l'(x)) → x
max'(n'(x, y, z)) → max'(z)
bs'(l'(x)) → true'
bs'(n'(x, y, z)) → and'(and'(ge'(x, max'(y)), ge'(min'(z), x)), and'(bs'(y), bs'(z)))
size'(l'(x)) → 1'(#')
size'(n'(x, y, z)) → +'(+'(size'(x), size'(y)), 1'(#'))
wb'(l'(x)) → true'
wb'(n'(x, y, z)) → and'(if'(ge'(size'(y), size'(z)), ge'(1'(#'), -'(size'(y), size'(z))), ge'(1'(#'), -'(size'(z), size'(y)))), and'(wb'(y), wb'(z)))
Types:
0' :: #':1':l':n' → #':1':l':n'
#' :: #':1':l':n'
+' :: #':1':l':n' → #':1':l':n' → #':1':l':n'
1' :: #':1':l':n' → #':1':l':n'
-' :: #':1':l':n' → #':1':l':n' → #':1':l':n'
not' :: false':true' → false':true'
false' :: false':true'
true' :: false':true'
and' :: false':true' → false':true' → false':true'
if' :: false':true' → false':true' → false':true' → false':true'
ge' :: #':1':l':n' → #':1':l':n' → false':true'
val' :: #':1':l':n' → #':1':l':n'
l' :: #':1':l':n' → #':1':l':n'
n' :: #':1':l':n' → #':1':l':n' → #':1':l':n' → #':1':l':n'
min' :: #':1':l':n' → #':1':l':n'
max' :: #':1':l':n' → #':1':l':n'
bs' :: #':1':l':n' → false':true'
size' :: #':1':l':n' → #':1':l':n'
wb' :: #':1':l':n' → false':true'
_hole_#':1':l':n'1 :: #':1':l':n'
_hole_false':true'2 :: false':true'
_gen_#':1':l':n'3 :: Nat → #':1':l':n'
Lemmas:
+'(_gen_#':1':l':n'3(+(1, _n5)), _gen_#':1':l':n'3(+(1, _n5))) → _*4, rt ∈ Ω(n5)
Generator Equations:
_gen_#':1':l':n'3(0) ⇔ #'
_gen_#':1':l':n'3(+(x, 1)) ⇔ 1'(_gen_#':1':l':n'3(x))
The following defined symbols remain to be analysed:
-', ge', min', max', bs', size', wb'
They will be analysed ascendingly in the following order:
-' < wb'
ge' < bs'
ge' < wb'
min' < bs'
max' < bs'
size' < wb'
Proved the following rewrite lemma:
-'(_gen_#':1':l':n'3(_n578937), _gen_#':1':l':n'3(_n578937)) → _gen_#':1':l':n'3(0), rt ∈ Ω(1 + n578937)
Induction Base:
-'(_gen_#':1':l':n'3(0), _gen_#':1':l':n'3(0)) →RΩ(1)
_gen_#':1':l':n'3(0)
Induction Step:
-'(_gen_#':1':l':n'3(+(_$n578938, 1)), _gen_#':1':l':n'3(+(_$n578938, 1))) →RΩ(1)
0'(-'(_gen_#':1':l':n'3(_$n578938), _gen_#':1':l':n'3(_$n578938))) →IH
0'(_gen_#':1':l':n'3(0)) →RΩ(1)
#'
We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).
Rules:
0'(#') → #'
+'(x, #') → x
+'(#', x) → x
+'(0'(x), 0'(y)) → 0'(+'(x, y))
+'(0'(x), 1'(y)) → 1'(+'(x, y))
+'(1'(x), 0'(y)) → 1'(+'(x, y))
+'(1'(x), 1'(y)) → 0'(+'(+'(x, y), 1'(#')))
+'(x, +'(y, z)) → +'(+'(x, y), z)
-'(x, #') → x
-'(#', x) → #'
-'(0'(x), 0'(y)) → 0'(-'(x, y))
-'(0'(x), 1'(y)) → 1'(-'(-'(x, y), 1'(#')))
-'(1'(x), 0'(y)) → 1'(-'(x, y))
-'(1'(x), 1'(y)) → 0'(-'(x, y))
not'(false') → true'
not'(true') → false'
and'(x, true') → x
and'(x, false') → false'
if'(true', x, y) → x
if'(false', x, y) → y
ge'(0'(x), 0'(y)) → ge'(x, y)
ge'(0'(x), 1'(y)) → not'(ge'(y, x))
ge'(1'(x), 0'(y)) → ge'(x, y)
ge'(1'(x), 1'(y)) → ge'(x, y)
ge'(x, #') → true'
ge'(#', 1'(x)) → false'
ge'(#', 0'(x)) → ge'(#', x)
val'(l'(x)) → x
val'(n'(x, y, z)) → x
min'(l'(x)) → x
min'(n'(x, y, z)) → min'(y)
max'(l'(x)) → x
max'(n'(x, y, z)) → max'(z)
bs'(l'(x)) → true'
bs'(n'(x, y, z)) → and'(and'(ge'(x, max'(y)), ge'(min'(z), x)), and'(bs'(y), bs'(z)))
size'(l'(x)) → 1'(#')
size'(n'(x, y, z)) → +'(+'(size'(x), size'(y)), 1'(#'))
wb'(l'(x)) → true'
wb'(n'(x, y, z)) → and'(if'(ge'(size'(y), size'(z)), ge'(1'(#'), -'(size'(y), size'(z))), ge'(1'(#'), -'(size'(z), size'(y)))), and'(wb'(y), wb'(z)))
Types:
0' :: #':1':l':n' → #':1':l':n'
#' :: #':1':l':n'
+' :: #':1':l':n' → #':1':l':n' → #':1':l':n'
1' :: #':1':l':n' → #':1':l':n'
-' :: #':1':l':n' → #':1':l':n' → #':1':l':n'
not' :: false':true' → false':true'
false' :: false':true'
true' :: false':true'
and' :: false':true' → false':true' → false':true'
if' :: false':true' → false':true' → false':true' → false':true'
ge' :: #':1':l':n' → #':1':l':n' → false':true'
val' :: #':1':l':n' → #':1':l':n'
l' :: #':1':l':n' → #':1':l':n'
n' :: #':1':l':n' → #':1':l':n' → #':1':l':n' → #':1':l':n'
min' :: #':1':l':n' → #':1':l':n'
max' :: #':1':l':n' → #':1':l':n'
bs' :: #':1':l':n' → false':true'
size' :: #':1':l':n' → #':1':l':n'
wb' :: #':1':l':n' → false':true'
_hole_#':1':l':n'1 :: #':1':l':n'
_hole_false':true'2 :: false':true'
_gen_#':1':l':n'3 :: Nat → #':1':l':n'
Lemmas:
+'(_gen_#':1':l':n'3(+(1, _n5)), _gen_#':1':l':n'3(+(1, _n5))) → _*4, rt ∈ Ω(n5)
-'(_gen_#':1':l':n'3(_n578937), _gen_#':1':l':n'3(_n578937)) → _gen_#':1':l':n'3(0), rt ∈ Ω(1 + n578937)
Generator Equations:
_gen_#':1':l':n'3(0) ⇔ #'
_gen_#':1':l':n'3(+(x, 1)) ⇔ 1'(_gen_#':1':l':n'3(x))
The following defined symbols remain to be analysed:
ge', min', max', bs', size', wb'
They will be analysed ascendingly in the following order:
ge' < bs'
ge' < wb'
min' < bs'
max' < bs'
size' < wb'
Proved the following rewrite lemma:
ge'(_gen_#':1':l':n'3(_n582554), _gen_#':1':l':n'3(_n582554)) → true', rt ∈ Ω(1 + n582554)
Induction Base:
ge'(_gen_#':1':l':n'3(0), _gen_#':1':l':n'3(0)) →RΩ(1)
true'
Induction Step:
ge'(_gen_#':1':l':n'3(+(_$n582555, 1)), _gen_#':1':l':n'3(+(_$n582555, 1))) →RΩ(1)
ge'(_gen_#':1':l':n'3(_$n582555), _gen_#':1':l':n'3(_$n582555)) →IH
true'
We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).
Rules:
0'(#') → #'
+'(x, #') → x
+'(#', x) → x
+'(0'(x), 0'(y)) → 0'(+'(x, y))
+'(0'(x), 1'(y)) → 1'(+'(x, y))
+'(1'(x), 0'(y)) → 1'(+'(x, y))
+'(1'(x), 1'(y)) → 0'(+'(+'(x, y), 1'(#')))
+'(x, +'(y, z)) → +'(+'(x, y), z)
-'(x, #') → x
-'(#', x) → #'
-'(0'(x), 0'(y)) → 0'(-'(x, y))
-'(0'(x), 1'(y)) → 1'(-'(-'(x, y), 1'(#')))
-'(1'(x), 0'(y)) → 1'(-'(x, y))
-'(1'(x), 1'(y)) → 0'(-'(x, y))
not'(false') → true'
not'(true') → false'
and'(x, true') → x
and'(x, false') → false'
if'(true', x, y) → x
if'(false', x, y) → y
ge'(0'(x), 0'(y)) → ge'(x, y)
ge'(0'(x), 1'(y)) → not'(ge'(y, x))
ge'(1'(x), 0'(y)) → ge'(x, y)
ge'(1'(x), 1'(y)) → ge'(x, y)
ge'(x, #') → true'
ge'(#', 1'(x)) → false'
ge'(#', 0'(x)) → ge'(#', x)
val'(l'(x)) → x
val'(n'(x, y, z)) → x
min'(l'(x)) → x
min'(n'(x, y, z)) → min'(y)
max'(l'(x)) → x
max'(n'(x, y, z)) → max'(z)
bs'(l'(x)) → true'
bs'(n'(x, y, z)) → and'(and'(ge'(x, max'(y)), ge'(min'(z), x)), and'(bs'(y), bs'(z)))
size'(l'(x)) → 1'(#')
size'(n'(x, y, z)) → +'(+'(size'(x), size'(y)), 1'(#'))
wb'(l'(x)) → true'
wb'(n'(x, y, z)) → and'(if'(ge'(size'(y), size'(z)), ge'(1'(#'), -'(size'(y), size'(z))), ge'(1'(#'), -'(size'(z), size'(y)))), and'(wb'(y), wb'(z)))
Types:
0' :: #':1':l':n' → #':1':l':n'
#' :: #':1':l':n'
+' :: #':1':l':n' → #':1':l':n' → #':1':l':n'
1' :: #':1':l':n' → #':1':l':n'
-' :: #':1':l':n' → #':1':l':n' → #':1':l':n'
not' :: false':true' → false':true'
false' :: false':true'
true' :: false':true'
and' :: false':true' → false':true' → false':true'
if' :: false':true' → false':true' → false':true' → false':true'
ge' :: #':1':l':n' → #':1':l':n' → false':true'
val' :: #':1':l':n' → #':1':l':n'
l' :: #':1':l':n' → #':1':l':n'
n' :: #':1':l':n' → #':1':l':n' → #':1':l':n' → #':1':l':n'
min' :: #':1':l':n' → #':1':l':n'
max' :: #':1':l':n' → #':1':l':n'
bs' :: #':1':l':n' → false':true'
size' :: #':1':l':n' → #':1':l':n'
wb' :: #':1':l':n' → false':true'
_hole_#':1':l':n'1 :: #':1':l':n'
_hole_false':true'2 :: false':true'
_gen_#':1':l':n'3 :: Nat → #':1':l':n'
Lemmas:
+'(_gen_#':1':l':n'3(+(1, _n5)), _gen_#':1':l':n'3(+(1, _n5))) → _*4, rt ∈ Ω(n5)
-'(_gen_#':1':l':n'3(_n578937), _gen_#':1':l':n'3(_n578937)) → _gen_#':1':l':n'3(0), rt ∈ Ω(1 + n578937)
ge'(_gen_#':1':l':n'3(_n582554), _gen_#':1':l':n'3(_n582554)) → true', rt ∈ Ω(1 + n582554)
Generator Equations:
_gen_#':1':l':n'3(0) ⇔ #'
_gen_#':1':l':n'3(+(x, 1)) ⇔ 1'(_gen_#':1':l':n'3(x))
The following defined symbols remain to be analysed:
min', max', bs', size', wb'
They will be analysed ascendingly in the following order:
min' < bs'
max' < bs'
size' < wb'
Could not prove a rewrite lemma for the defined symbol min'.
Rules:
0'(#') → #'
+'(x, #') → x
+'(#', x) → x
+'(0'(x), 0'(y)) → 0'(+'(x, y))
+'(0'(x), 1'(y)) → 1'(+'(x, y))
+'(1'(x), 0'(y)) → 1'(+'(x, y))
+'(1'(x), 1'(y)) → 0'(+'(+'(x, y), 1'(#')))
+'(x, +'(y, z)) → +'(+'(x, y), z)
-'(x, #') → x
-'(#', x) → #'
-'(0'(x), 0'(y)) → 0'(-'(x, y))
-'(0'(x), 1'(y)) → 1'(-'(-'(x, y), 1'(#')))
-'(1'(x), 0'(y)) → 1'(-'(x, y))
-'(1'(x), 1'(y)) → 0'(-'(x, y))
not'(false') → true'
not'(true') → false'
and'(x, true') → x
and'(x, false') → false'
if'(true', x, y) → x
if'(false', x, y) → y
ge'(0'(x), 0'(y)) → ge'(x, y)
ge'(0'(x), 1'(y)) → not'(ge'(y, x))
ge'(1'(x), 0'(y)) → ge'(x, y)
ge'(1'(x), 1'(y)) → ge'(x, y)
ge'(x, #') → true'
ge'(#', 1'(x)) → false'
ge'(#', 0'(x)) → ge'(#', x)
val'(l'(x)) → x
val'(n'(x, y, z)) → x
min'(l'(x)) → x
min'(n'(x, y, z)) → min'(y)
max'(l'(x)) → x
max'(n'(x, y, z)) → max'(z)
bs'(l'(x)) → true'
bs'(n'(x, y, z)) → and'(and'(ge'(x, max'(y)), ge'(min'(z), x)), and'(bs'(y), bs'(z)))
size'(l'(x)) → 1'(#')
size'(n'(x, y, z)) → +'(+'(size'(x), size'(y)), 1'(#'))
wb'(l'(x)) → true'
wb'(n'(x, y, z)) → and'(if'(ge'(size'(y), size'(z)), ge'(1'(#'), -'(size'(y), size'(z))), ge'(1'(#'), -'(size'(z), size'(y)))), and'(wb'(y), wb'(z)))
Types:
0' :: #':1':l':n' → #':1':l':n'
#' :: #':1':l':n'
+' :: #':1':l':n' → #':1':l':n' → #':1':l':n'
1' :: #':1':l':n' → #':1':l':n'
-' :: #':1':l':n' → #':1':l':n' → #':1':l':n'
not' :: false':true' → false':true'
false' :: false':true'
true' :: false':true'
and' :: false':true' → false':true' → false':true'
if' :: false':true' → false':true' → false':true' → false':true'
ge' :: #':1':l':n' → #':1':l':n' → false':true'
val' :: #':1':l':n' → #':1':l':n'
l' :: #':1':l':n' → #':1':l':n'
n' :: #':1':l':n' → #':1':l':n' → #':1':l':n' → #':1':l':n'
min' :: #':1':l':n' → #':1':l':n'
max' :: #':1':l':n' → #':1':l':n'
bs' :: #':1':l':n' → false':true'
size' :: #':1':l':n' → #':1':l':n'
wb' :: #':1':l':n' → false':true'
_hole_#':1':l':n'1 :: #':1':l':n'
_hole_false':true'2 :: false':true'
_gen_#':1':l':n'3 :: Nat → #':1':l':n'
Lemmas:
+'(_gen_#':1':l':n'3(+(1, _n5)), _gen_#':1':l':n'3(+(1, _n5))) → _*4, rt ∈ Ω(n5)
-'(_gen_#':1':l':n'3(_n578937), _gen_#':1':l':n'3(_n578937)) → _gen_#':1':l':n'3(0), rt ∈ Ω(1 + n578937)
ge'(_gen_#':1':l':n'3(_n582554), _gen_#':1':l':n'3(_n582554)) → true', rt ∈ Ω(1 + n582554)
Generator Equations:
_gen_#':1':l':n'3(0) ⇔ #'
_gen_#':1':l':n'3(+(x, 1)) ⇔ 1'(_gen_#':1':l':n'3(x))
The following defined symbols remain to be analysed:
max', bs', size', wb'
They will be analysed ascendingly in the following order:
max' < bs'
size' < wb'
Could not prove a rewrite lemma for the defined symbol max'.
Rules:
0'(#') → #'
+'(x, #') → x
+'(#', x) → x
+'(0'(x), 0'(y)) → 0'(+'(x, y))
+'(0'(x), 1'(y)) → 1'(+'(x, y))
+'(1'(x), 0'(y)) → 1'(+'(x, y))
+'(1'(x), 1'(y)) → 0'(+'(+'(x, y), 1'(#')))
+'(x, +'(y, z)) → +'(+'(x, y), z)
-'(x, #') → x
-'(#', x) → #'
-'(0'(x), 0'(y)) → 0'(-'(x, y))
-'(0'(x), 1'(y)) → 1'(-'(-'(x, y), 1'(#')))
-'(1'(x), 0'(y)) → 1'(-'(x, y))
-'(1'(x), 1'(y)) → 0'(-'(x, y))
not'(false') → true'
not'(true') → false'
and'(x, true') → x
and'(x, false') → false'
if'(true', x, y) → x
if'(false', x, y) → y
ge'(0'(x), 0'(y)) → ge'(x, y)
ge'(0'(x), 1'(y)) → not'(ge'(y, x))
ge'(1'(x), 0'(y)) → ge'(x, y)
ge'(1'(x), 1'(y)) → ge'(x, y)
ge'(x, #') → true'
ge'(#', 1'(x)) → false'
ge'(#', 0'(x)) → ge'(#', x)
val'(l'(x)) → x
val'(n'(x, y, z)) → x
min'(l'(x)) → x
min'(n'(x, y, z)) → min'(y)
max'(l'(x)) → x
max'(n'(x, y, z)) → max'(z)
bs'(l'(x)) → true'
bs'(n'(x, y, z)) → and'(and'(ge'(x, max'(y)), ge'(min'(z), x)), and'(bs'(y), bs'(z)))
size'(l'(x)) → 1'(#')
size'(n'(x, y, z)) → +'(+'(size'(x), size'(y)), 1'(#'))
wb'(l'(x)) → true'
wb'(n'(x, y, z)) → and'(if'(ge'(size'(y), size'(z)), ge'(1'(#'), -'(size'(y), size'(z))), ge'(1'(#'), -'(size'(z), size'(y)))), and'(wb'(y), wb'(z)))
Types:
0' :: #':1':l':n' → #':1':l':n'
#' :: #':1':l':n'
+' :: #':1':l':n' → #':1':l':n' → #':1':l':n'
1' :: #':1':l':n' → #':1':l':n'
-' :: #':1':l':n' → #':1':l':n' → #':1':l':n'
not' :: false':true' → false':true'
false' :: false':true'
true' :: false':true'
and' :: false':true' → false':true' → false':true'
if' :: false':true' → false':true' → false':true' → false':true'
ge' :: #':1':l':n' → #':1':l':n' → false':true'
val' :: #':1':l':n' → #':1':l':n'
l' :: #':1':l':n' → #':1':l':n'
n' :: #':1':l':n' → #':1':l':n' → #':1':l':n' → #':1':l':n'
min' :: #':1':l':n' → #':1':l':n'
max' :: #':1':l':n' → #':1':l':n'
bs' :: #':1':l':n' → false':true'
size' :: #':1':l':n' → #':1':l':n'
wb' :: #':1':l':n' → false':true'
_hole_#':1':l':n'1 :: #':1':l':n'
_hole_false':true'2 :: false':true'
_gen_#':1':l':n'3 :: Nat → #':1':l':n'
Lemmas:
+'(_gen_#':1':l':n'3(+(1, _n5)), _gen_#':1':l':n'3(+(1, _n5))) → _*4, rt ∈ Ω(n5)
-'(_gen_#':1':l':n'3(_n578937), _gen_#':1':l':n'3(_n578937)) → _gen_#':1':l':n'3(0), rt ∈ Ω(1 + n578937)
ge'(_gen_#':1':l':n'3(_n582554), _gen_#':1':l':n'3(_n582554)) → true', rt ∈ Ω(1 + n582554)
Generator Equations:
_gen_#':1':l':n'3(0) ⇔ #'
_gen_#':1':l':n'3(+(x, 1)) ⇔ 1'(_gen_#':1':l':n'3(x))
The following defined symbols remain to be analysed:
bs', size', wb'
They will be analysed ascendingly in the following order:
size' < wb'
Could not prove a rewrite lemma for the defined symbol bs'.
Rules:
0'(#') → #'
+'(x, #') → x
+'(#', x) → x
+'(0'(x), 0'(y)) → 0'(+'(x, y))
+'(0'(x), 1'(y)) → 1'(+'(x, y))
+'(1'(x), 0'(y)) → 1'(+'(x, y))
+'(1'(x), 1'(y)) → 0'(+'(+'(x, y), 1'(#')))
+'(x, +'(y, z)) → +'(+'(x, y), z)
-'(x, #') → x
-'(#', x) → #'
-'(0'(x), 0'(y)) → 0'(-'(x, y))
-'(0'(x), 1'(y)) → 1'(-'(-'(x, y), 1'(#')))
-'(1'(x), 0'(y)) → 1'(-'(x, y))
-'(1'(x), 1'(y)) → 0'(-'(x, y))
not'(false') → true'
not'(true') → false'
and'(x, true') → x
and'(x, false') → false'
if'(true', x, y) → x
if'(false', x, y) → y
ge'(0'(x), 0'(y)) → ge'(x, y)
ge'(0'(x), 1'(y)) → not'(ge'(y, x))
ge'(1'(x), 0'(y)) → ge'(x, y)
ge'(1'(x), 1'(y)) → ge'(x, y)
ge'(x, #') → true'
ge'(#', 1'(x)) → false'
ge'(#', 0'(x)) → ge'(#', x)
val'(l'(x)) → x
val'(n'(x, y, z)) → x
min'(l'(x)) → x
min'(n'(x, y, z)) → min'(y)
max'(l'(x)) → x
max'(n'(x, y, z)) → max'(z)
bs'(l'(x)) → true'
bs'(n'(x, y, z)) → and'(and'(ge'(x, max'(y)), ge'(min'(z), x)), and'(bs'(y), bs'(z)))
size'(l'(x)) → 1'(#')
size'(n'(x, y, z)) → +'(+'(size'(x), size'(y)), 1'(#'))
wb'(l'(x)) → true'
wb'(n'(x, y, z)) → and'(if'(ge'(size'(y), size'(z)), ge'(1'(#'), -'(size'(y), size'(z))), ge'(1'(#'), -'(size'(z), size'(y)))), and'(wb'(y), wb'(z)))
Types:
0' :: #':1':l':n' → #':1':l':n'
#' :: #':1':l':n'
+' :: #':1':l':n' → #':1':l':n' → #':1':l':n'
1' :: #':1':l':n' → #':1':l':n'
-' :: #':1':l':n' → #':1':l':n' → #':1':l':n'
not' :: false':true' → false':true'
false' :: false':true'
true' :: false':true'
and' :: false':true' → false':true' → false':true'
if' :: false':true' → false':true' → false':true' → false':true'
ge' :: #':1':l':n' → #':1':l':n' → false':true'
val' :: #':1':l':n' → #':1':l':n'
l' :: #':1':l':n' → #':1':l':n'
n' :: #':1':l':n' → #':1':l':n' → #':1':l':n' → #':1':l':n'
min' :: #':1':l':n' → #':1':l':n'
max' :: #':1':l':n' → #':1':l':n'
bs' :: #':1':l':n' → false':true'
size' :: #':1':l':n' → #':1':l':n'
wb' :: #':1':l':n' → false':true'
_hole_#':1':l':n'1 :: #':1':l':n'
_hole_false':true'2 :: false':true'
_gen_#':1':l':n'3 :: Nat → #':1':l':n'
Lemmas:
+'(_gen_#':1':l':n'3(+(1, _n5)), _gen_#':1':l':n'3(+(1, _n5))) → _*4, rt ∈ Ω(n5)
-'(_gen_#':1':l':n'3(_n578937), _gen_#':1':l':n'3(_n578937)) → _gen_#':1':l':n'3(0), rt ∈ Ω(1 + n578937)
ge'(_gen_#':1':l':n'3(_n582554), _gen_#':1':l':n'3(_n582554)) → true', rt ∈ Ω(1 + n582554)
Generator Equations:
_gen_#':1':l':n'3(0) ⇔ #'
_gen_#':1':l':n'3(+(x, 1)) ⇔ 1'(_gen_#':1':l':n'3(x))
The following defined symbols remain to be analysed:
size', wb'
They will be analysed ascendingly in the following order:
size' < wb'
Could not prove a rewrite lemma for the defined symbol size'.
Rules:
0'(#') → #'
+'(x, #') → x
+'(#', x) → x
+'(0'(x), 0'(y)) → 0'(+'(x, y))
+'(0'(x), 1'(y)) → 1'(+'(x, y))
+'(1'(x), 0'(y)) → 1'(+'(x, y))
+'(1'(x), 1'(y)) → 0'(+'(+'(x, y), 1'(#')))
+'(x, +'(y, z)) → +'(+'(x, y), z)
-'(x, #') → x
-'(#', x) → #'
-'(0'(x), 0'(y)) → 0'(-'(x, y))
-'(0'(x), 1'(y)) → 1'(-'(-'(x, y), 1'(#')))
-'(1'(x), 0'(y)) → 1'(-'(x, y))
-'(1'(x), 1'(y)) → 0'(-'(x, y))
not'(false') → true'
not'(true') → false'
and'(x, true') → x
and'(x, false') → false'
if'(true', x, y) → x
if'(false', x, y) → y
ge'(0'(x), 0'(y)) → ge'(x, y)
ge'(0'(x), 1'(y)) → not'(ge'(y, x))
ge'(1'(x), 0'(y)) → ge'(x, y)
ge'(1'(x), 1'(y)) → ge'(x, y)
ge'(x, #') → true'
ge'(#', 1'(x)) → false'
ge'(#', 0'(x)) → ge'(#', x)
val'(l'(x)) → x
val'(n'(x, y, z)) → x
min'(l'(x)) → x
min'(n'(x, y, z)) → min'(y)
max'(l'(x)) → x
max'(n'(x, y, z)) → max'(z)
bs'(l'(x)) → true'
bs'(n'(x, y, z)) → and'(and'(ge'(x, max'(y)), ge'(min'(z), x)), and'(bs'(y), bs'(z)))
size'(l'(x)) → 1'(#')
size'(n'(x, y, z)) → +'(+'(size'(x), size'(y)), 1'(#'))
wb'(l'(x)) → true'
wb'(n'(x, y, z)) → and'(if'(ge'(size'(y), size'(z)), ge'(1'(#'), -'(size'(y), size'(z))), ge'(1'(#'), -'(size'(z), size'(y)))), and'(wb'(y), wb'(z)))
Types:
0' :: #':1':l':n' → #':1':l':n'
#' :: #':1':l':n'
+' :: #':1':l':n' → #':1':l':n' → #':1':l':n'
1' :: #':1':l':n' → #':1':l':n'
-' :: #':1':l':n' → #':1':l':n' → #':1':l':n'
not' :: false':true' → false':true'
false' :: false':true'
true' :: false':true'
and' :: false':true' → false':true' → false':true'
if' :: false':true' → false':true' → false':true' → false':true'
ge' :: #':1':l':n' → #':1':l':n' → false':true'
val' :: #':1':l':n' → #':1':l':n'
l' :: #':1':l':n' → #':1':l':n'
n' :: #':1':l':n' → #':1':l':n' → #':1':l':n' → #':1':l':n'
min' :: #':1':l':n' → #':1':l':n'
max' :: #':1':l':n' → #':1':l':n'
bs' :: #':1':l':n' → false':true'
size' :: #':1':l':n' → #':1':l':n'
wb' :: #':1':l':n' → false':true'
_hole_#':1':l':n'1 :: #':1':l':n'
_hole_false':true'2 :: false':true'
_gen_#':1':l':n'3 :: Nat → #':1':l':n'
Lemmas:
+'(_gen_#':1':l':n'3(+(1, _n5)), _gen_#':1':l':n'3(+(1, _n5))) → _*4, rt ∈ Ω(n5)
-'(_gen_#':1':l':n'3(_n578937), _gen_#':1':l':n'3(_n578937)) → _gen_#':1':l':n'3(0), rt ∈ Ω(1 + n578937)
ge'(_gen_#':1':l':n'3(_n582554), _gen_#':1':l':n'3(_n582554)) → true', rt ∈ Ω(1 + n582554)
Generator Equations:
_gen_#':1':l':n'3(0) ⇔ #'
_gen_#':1':l':n'3(+(x, 1)) ⇔ 1'(_gen_#':1':l':n'3(x))
The following defined symbols remain to be analysed:
wb'
Could not prove a rewrite lemma for the defined symbol wb'.
Rules:
0'(#') → #'
+'(x, #') → x
+'(#', x) → x
+'(0'(x), 0'(y)) → 0'(+'(x, y))
+'(0'(x), 1'(y)) → 1'(+'(x, y))
+'(1'(x), 0'(y)) → 1'(+'(x, y))
+'(1'(x), 1'(y)) → 0'(+'(+'(x, y), 1'(#')))
+'(x, +'(y, z)) → +'(+'(x, y), z)
-'(x, #') → x
-'(#', x) → #'
-'(0'(x), 0'(y)) → 0'(-'(x, y))
-'(0'(x), 1'(y)) → 1'(-'(-'(x, y), 1'(#')))
-'(1'(x), 0'(y)) → 1'(-'(x, y))
-'(1'(x), 1'(y)) → 0'(-'(x, y))
not'(false') → true'
not'(true') → false'
and'(x, true') → x
and'(x, false') → false'
if'(true', x, y) → x
if'(false', x, y) → y
ge'(0'(x), 0'(y)) → ge'(x, y)
ge'(0'(x), 1'(y)) → not'(ge'(y, x))
ge'(1'(x), 0'(y)) → ge'(x, y)
ge'(1'(x), 1'(y)) → ge'(x, y)
ge'(x, #') → true'
ge'(#', 1'(x)) → false'
ge'(#', 0'(x)) → ge'(#', x)
val'(l'(x)) → x
val'(n'(x, y, z)) → x
min'(l'(x)) → x
min'(n'(x, y, z)) → min'(y)
max'(l'(x)) → x
max'(n'(x, y, z)) → max'(z)
bs'(l'(x)) → true'
bs'(n'(x, y, z)) → and'(and'(ge'(x, max'(y)), ge'(min'(z), x)), and'(bs'(y), bs'(z)))
size'(l'(x)) → 1'(#')
size'(n'(x, y, z)) → +'(+'(size'(x), size'(y)), 1'(#'))
wb'(l'(x)) → true'
wb'(n'(x, y, z)) → and'(if'(ge'(size'(y), size'(z)), ge'(1'(#'), -'(size'(y), size'(z))), ge'(1'(#'), -'(size'(z), size'(y)))), and'(wb'(y), wb'(z)))
Types:
0' :: #':1':l':n' → #':1':l':n'
#' :: #':1':l':n'
+' :: #':1':l':n' → #':1':l':n' → #':1':l':n'
1' :: #':1':l':n' → #':1':l':n'
-' :: #':1':l':n' → #':1':l':n' → #':1':l':n'
not' :: false':true' → false':true'
false' :: false':true'
true' :: false':true'
and' :: false':true' → false':true' → false':true'
if' :: false':true' → false':true' → false':true' → false':true'
ge' :: #':1':l':n' → #':1':l':n' → false':true'
val' :: #':1':l':n' → #':1':l':n'
l' :: #':1':l':n' → #':1':l':n'
n' :: #':1':l':n' → #':1':l':n' → #':1':l':n' → #':1':l':n'
min' :: #':1':l':n' → #':1':l':n'
max' :: #':1':l':n' → #':1':l':n'
bs' :: #':1':l':n' → false':true'
size' :: #':1':l':n' → #':1':l':n'
wb' :: #':1':l':n' → false':true'
_hole_#':1':l':n'1 :: #':1':l':n'
_hole_false':true'2 :: false':true'
_gen_#':1':l':n'3 :: Nat → #':1':l':n'
Lemmas:
+'(_gen_#':1':l':n'3(+(1, _n5)), _gen_#':1':l':n'3(+(1, _n5))) → _*4, rt ∈ Ω(n5)
-'(_gen_#':1':l':n'3(_n578937), _gen_#':1':l':n'3(_n578937)) → _gen_#':1':l':n'3(0), rt ∈ Ω(1 + n578937)
ge'(_gen_#':1':l':n'3(_n582554), _gen_#':1':l':n'3(_n582554)) → true', rt ∈ Ω(1 + n582554)
Generator Equations:
_gen_#':1':l':n'3(0) ⇔ #'
_gen_#':1':l':n'3(+(x, 1)) ⇔ 1'(_gen_#':1':l':n'3(x))
No more defined symbols left to analyse.
The lowerbound Ω(n) was proven with the following lemma:
+'(_gen_#':1':l':n'3(+(1, _n5)), _gen_#':1':l':n'3(+(1, _n5))) → _*4, rt ∈ Ω(n5)