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(true) → false
not(false) → true
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(#, 0(x)) → ge(#, x)
ge(#, 1(x)) → false
log(x) → -(log'(x), 1(#))
log'(#) → #
log'(1(x)) → +(log'(x), 1(#))
log'(0(x)) → if(ge(x, 1(#)), +(log'(x), 1(#)), #)
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'(true') → false'
not'(false') → true'
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'(#', 0'(x)) → ge'(#', x)
ge'(#', 1'(x)) → false'
log''(x) → -'(log'''(x), 1'(#'))
log'''(#') → #'
log'''(1'(x)) → +'(log'''(x), 1'(#'))
log'''(0'(x)) → if'(ge'(x, 1'(#')), +'(log'''(x), 1'(#')), #')
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'(true') → false'
not'(false') → true'
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'(#', 0'(x)) → ge'(#', x)
ge'(#', 1'(x)) → false'
log''(x) → -'(log'''(x), 1'(#'))
log'''(#') → #'
log'''(1'(x)) → +'(log'''(x), 1'(#'))
log'''(0'(x)) → if'(ge'(x, 1'(#')), +'(log'''(x), 1'(#')), #')
Types:
0' :: #':1' → #':1'
#' :: #':1'
+' :: #':1' → #':1' → #':1'
1' :: #':1' → #':1'
-' :: #':1' → #':1' → #':1'
not' :: true':false' → true':false'
true' :: true':false'
false' :: true':false'
if' :: true':false' → #':1' → #':1' → #':1'
ge' :: #':1' → #':1' → true':false'
log'' :: #':1' → #':1'
log''' :: #':1' → #':1'
_hole_#':1'1 :: #':1'
_hole_true':false'2 :: true':false'
_gen_#':1'3 :: Nat → #':1'
Heuristically decided to analyse the following defined symbols:
+', -', ge', log'''
They will be analysed ascendingly in the following order:
+' < log'''
ge' < log'''
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'(true') → false'
not'(false') → true'
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'(#', 0'(x)) → ge'(#', x)
ge'(#', 1'(x)) → false'
log''(x) → -'(log'''(x), 1'(#'))
log'''(#') → #'
log'''(1'(x)) → +'(log'''(x), 1'(#'))
log'''(0'(x)) → if'(ge'(x, 1'(#')), +'(log'''(x), 1'(#')), #')
Types:
0' :: #':1' → #':1'
#' :: #':1'
+' :: #':1' → #':1' → #':1'
1' :: #':1' → #':1'
-' :: #':1' → #':1' → #':1'
not' :: true':false' → true':false'
true' :: true':false'
false' :: true':false'
if' :: true':false' → #':1' → #':1' → #':1'
ge' :: #':1' → #':1' → true':false'
log'' :: #':1' → #':1'
log''' :: #':1' → #':1'
_hole_#':1'1 :: #':1'
_hole_true':false'2 :: true':false'
_gen_#':1'3 :: Nat → #':1'
Generator Equations:
_gen_#':1'3(0) ⇔ #'
_gen_#':1'3(+(x, 1)) ⇔ 1'(_gen_#':1'3(x))
The following defined symbols remain to be analysed:
+', -', ge', log'''
They will be analysed ascendingly in the following order:
+' < log'''
ge' < log'''
Proved the following rewrite lemma:
+'(_gen_#':1'3(_n5), _gen_#':1'3(_n5)) → _*4, rt ∈ Ω(n5)
Induction Base:
+'(_gen_#':1'3(0), _gen_#':1'3(0))
Induction Step:
+'(_gen_#':1'3(+(_$n6, 1)), _gen_#':1'3(+(_$n6, 1))) →RΩ(1)
0'(+'(+'(_gen_#':1'3(_$n6), _gen_#':1'3(_$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'(true') → false'
not'(false') → true'
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'(#', 0'(x)) → ge'(#', x)
ge'(#', 1'(x)) → false'
log''(x) → -'(log'''(x), 1'(#'))
log'''(#') → #'
log'''(1'(x)) → +'(log'''(x), 1'(#'))
log'''(0'(x)) → if'(ge'(x, 1'(#')), +'(log'''(x), 1'(#')), #')
Types:
0' :: #':1' → #':1'
#' :: #':1'
+' :: #':1' → #':1' → #':1'
1' :: #':1' → #':1'
-' :: #':1' → #':1' → #':1'
not' :: true':false' → true':false'
true' :: true':false'
false' :: true':false'
if' :: true':false' → #':1' → #':1' → #':1'
ge' :: #':1' → #':1' → true':false'
log'' :: #':1' → #':1'
log''' :: #':1' → #':1'
_hole_#':1'1 :: #':1'
_hole_true':false'2 :: true':false'
_gen_#':1'3 :: Nat → #':1'
Lemmas:
+'(_gen_#':1'3(_n5), _gen_#':1'3(_n5)) → _*4, rt ∈ Ω(n5)
Generator Equations:
_gen_#':1'3(0) ⇔ #'
_gen_#':1'3(+(x, 1)) ⇔ 1'(_gen_#':1'3(x))
The following defined symbols remain to be analysed:
-', ge', log'''
They will be analysed ascendingly in the following order:
ge' < log'''
Proved the following rewrite lemma:
-'(_gen_#':1'3(_n41737), _gen_#':1'3(_n41737)) → _gen_#':1'3(0), rt ∈ Ω(1 + n41737)
Induction Base:
-'(_gen_#':1'3(0), _gen_#':1'3(0)) →RΩ(1)
#'
Induction Step:
-'(_gen_#':1'3(+(_$n41738, 1)), _gen_#':1'3(+(_$n41738, 1))) →RΩ(1)
0'(-'(_gen_#':1'3(_$n41738), _gen_#':1'3(_$n41738))) →IH
0'(_gen_#':1'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'(true') → false'
not'(false') → true'
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'(#', 0'(x)) → ge'(#', x)
ge'(#', 1'(x)) → false'
log''(x) → -'(log'''(x), 1'(#'))
log'''(#') → #'
log'''(1'(x)) → +'(log'''(x), 1'(#'))
log'''(0'(x)) → if'(ge'(x, 1'(#')), +'(log'''(x), 1'(#')), #')
Types:
0' :: #':1' → #':1'
#' :: #':1'
+' :: #':1' → #':1' → #':1'
1' :: #':1' → #':1'
-' :: #':1' → #':1' → #':1'
not' :: true':false' → true':false'
true' :: true':false'
false' :: true':false'
if' :: true':false' → #':1' → #':1' → #':1'
ge' :: #':1' → #':1' → true':false'
log'' :: #':1' → #':1'
log''' :: #':1' → #':1'
_hole_#':1'1 :: #':1'
_hole_true':false'2 :: true':false'
_gen_#':1'3 :: Nat → #':1'
Lemmas:
+'(_gen_#':1'3(_n5), _gen_#':1'3(_n5)) → _*4, rt ∈ Ω(n5)
-'(_gen_#':1'3(_n41737), _gen_#':1'3(_n41737)) → _gen_#':1'3(0), rt ∈ Ω(1 + n41737)
Generator Equations:
_gen_#':1'3(0) ⇔ #'
_gen_#':1'3(+(x, 1)) ⇔ 1'(_gen_#':1'3(x))
The following defined symbols remain to be analysed:
ge', log'''
They will be analysed ascendingly in the following order:
ge' < log'''
Proved the following rewrite lemma:
ge'(_gen_#':1'3(_n44649), _gen_#':1'3(_n44649)) → true', rt ∈ Ω(1 + n44649)
Induction Base:
ge'(_gen_#':1'3(0), _gen_#':1'3(0)) →RΩ(1)
true'
Induction Step:
ge'(_gen_#':1'3(+(_$n44650, 1)), _gen_#':1'3(+(_$n44650, 1))) →RΩ(1)
ge'(_gen_#':1'3(_$n44650), _gen_#':1'3(_$n44650)) →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'(true') → false'
not'(false') → true'
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'(#', 0'(x)) → ge'(#', x)
ge'(#', 1'(x)) → false'
log''(x) → -'(log'''(x), 1'(#'))
log'''(#') → #'
log'''(1'(x)) → +'(log'''(x), 1'(#'))
log'''(0'(x)) → if'(ge'(x, 1'(#')), +'(log'''(x), 1'(#')), #')
Types:
0' :: #':1' → #':1'
#' :: #':1'
+' :: #':1' → #':1' → #':1'
1' :: #':1' → #':1'
-' :: #':1' → #':1' → #':1'
not' :: true':false' → true':false'
true' :: true':false'
false' :: true':false'
if' :: true':false' → #':1' → #':1' → #':1'
ge' :: #':1' → #':1' → true':false'
log'' :: #':1' → #':1'
log''' :: #':1' → #':1'
_hole_#':1'1 :: #':1'
_hole_true':false'2 :: true':false'
_gen_#':1'3 :: Nat → #':1'
Lemmas:
+'(_gen_#':1'3(_n5), _gen_#':1'3(_n5)) → _*4, rt ∈ Ω(n5)
-'(_gen_#':1'3(_n41737), _gen_#':1'3(_n41737)) → _gen_#':1'3(0), rt ∈ Ω(1 + n41737)
ge'(_gen_#':1'3(_n44649), _gen_#':1'3(_n44649)) → true', rt ∈ Ω(1 + n44649)
Generator Equations:
_gen_#':1'3(0) ⇔ #'
_gen_#':1'3(+(x, 1)) ⇔ 1'(_gen_#':1'3(x))
The following defined symbols remain to be analysed:
log'''
Proved the following rewrite lemma:
log'''(_gen_#':1'3(+(1, _n47789))) → _*4, rt ∈ Ω(n47789)
Induction Base:
log'''(_gen_#':1'3(+(1, 0)))
Induction Step:
log'''(_gen_#':1'3(+(1, +(_$n47790, 1)))) →RΩ(1)
+'(log'''(_gen_#':1'3(+(1, _$n47790))), 1'(#')) →IH
+'(_*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'(true') → false'
not'(false') → true'
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'(#', 0'(x)) → ge'(#', x)
ge'(#', 1'(x)) → false'
log''(x) → -'(log'''(x), 1'(#'))
log'''(#') → #'
log'''(1'(x)) → +'(log'''(x), 1'(#'))
log'''(0'(x)) → if'(ge'(x, 1'(#')), +'(log'''(x), 1'(#')), #')
Types:
0' :: #':1' → #':1'
#' :: #':1'
+' :: #':1' → #':1' → #':1'
1' :: #':1' → #':1'
-' :: #':1' → #':1' → #':1'
not' :: true':false' → true':false'
true' :: true':false'
false' :: true':false'
if' :: true':false' → #':1' → #':1' → #':1'
ge' :: #':1' → #':1' → true':false'
log'' :: #':1' → #':1'
log''' :: #':1' → #':1'
_hole_#':1'1 :: #':1'
_hole_true':false'2 :: true':false'
_gen_#':1'3 :: Nat → #':1'
Lemmas:
+'(_gen_#':1'3(_n5), _gen_#':1'3(_n5)) → _*4, rt ∈ Ω(n5)
-'(_gen_#':1'3(_n41737), _gen_#':1'3(_n41737)) → _gen_#':1'3(0), rt ∈ Ω(1 + n41737)
ge'(_gen_#':1'3(_n44649), _gen_#':1'3(_n44649)) → true', rt ∈ Ω(1 + n44649)
log'''(_gen_#':1'3(+(1, _n47789))) → _*4, rt ∈ Ω(n47789)
Generator Equations:
_gen_#':1'3(0) ⇔ #'
_gen_#':1'3(+(x, 1)) ⇔ 1'(_gen_#':1'3(x))
No more defined symbols left to analyse.
The lowerbound Ω(n) was proven with the following lemma:
+'(_gen_#':1'3(_n5), _gen_#':1'3(_n5)) → _*4, rt ∈ Ω(n5)