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))
+(0(x), j(y)) → j(+(x, y))
+(j(x), 0(y)) → j(+(x, y))
+(1(x), 1(y)) → j(+(+(x, y), 1(#)))
+(j(x), j(y)) → 1(+(+(x, y), j(#)))
+(1(x), j(y)) → 0(+(x, y))
+(j(x), 1(y)) → 0(+(x, y))
+(+(x, y), z) → +(x, +(y, z))
opp(#) → #
opp(0(x)) → 0(opp(x))
opp(1(x)) → j(opp(x))
opp(j(x)) → 1(opp(x))
-(x, y) → +(x, opp(y))
*(#, x) → #
*(0(x), y) → 0(*(x, y))
*(1(x), y) → +(0(*(x, y)), y)
*(j(x), y) → -(0(*(x, y)), y)
*(*(x, y), z) → *(x, *(y, z))
*(+(x, y), z) → +(*(x, z), *(y, z))
*(x, +(y, z)) → +(*(x, y), *(x, 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))
+'(0'(x), j'(y)) → j'(+'(x, y))
+'(j'(x), 0'(y)) → j'(+'(x, y))
+'(1'(x), 1'(y)) → j'(+'(+'(x, y), 1'(#')))
+'(j'(x), j'(y)) → 1'(+'(+'(x, y), j'(#')))
+'(1'(x), j'(y)) → 0'(+'(x, y))
+'(j'(x), 1'(y)) → 0'(+'(x, y))
+'(+'(x, y), z) → +'(x, +'(y, z))
opp'(#') → #'
opp'(0'(x)) → 0'(opp'(x))
opp'(1'(x)) → j'(opp'(x))
opp'(j'(x)) → 1'(opp'(x))
-'(x, y) → +'(x, opp'(y))
*'(#', x) → #'
*'(0'(x), y) → 0'(*'(x, y))
*'(1'(x), y) → +'(0'(*'(x, y)), y)
*'(j'(x), y) → -'(0'(*'(x, y)), y)
*'(*'(x, y), z) → *'(x, *'(y, z))
*'(+'(x, y), z) → +'(*'(x, z), *'(y, z))
*'(x, +'(y, z)) → +'(*'(x, y), *'(x, 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))
+'(0'(x), j'(y)) → j'(+'(x, y))
+'(j'(x), 0'(y)) → j'(+'(x, y))
+'(1'(x), 1'(y)) → j'(+'(+'(x, y), 1'(#')))
+'(j'(x), j'(y)) → 1'(+'(+'(x, y), j'(#')))
+'(1'(x), j'(y)) → 0'(+'(x, y))
+'(j'(x), 1'(y)) → 0'(+'(x, y))
+'(+'(x, y), z) → +'(x, +'(y, z))
opp'(#') → #'
opp'(0'(x)) → 0'(opp'(x))
opp'(1'(x)) → j'(opp'(x))
opp'(j'(x)) → 1'(opp'(x))
-'(x, y) → +'(x, opp'(y))
*'(#', x) → #'
*'(0'(x), y) → 0'(*'(x, y))
*'(1'(x), y) → +'(0'(*'(x, y)), y)
*'(j'(x), y) → -'(0'(*'(x, y)), y)
*'(*'(x, y), z) → *'(x, *'(y, z))
*'(+'(x, y), z) → +'(*'(x, z), *'(y, z))
*'(x, +'(y, z)) → +'(*'(x, y), *'(x, z))
Types:
0' :: #':1':j' → #':1':j'
#' :: #':1':j'
+' :: #':1':j' → #':1':j' → #':1':j'
1' :: #':1':j' → #':1':j'
j' :: #':1':j' → #':1':j'
opp' :: #':1':j' → #':1':j'
-' :: #':1':j' → #':1':j' → #':1':j'
*' :: #':1':j' → #':1':j' → #':1':j'
_hole_#':1':j'1 :: #':1':j'
_gen_#':1':j'2 :: Nat → #':1':j'
Heuristically decided to analyse the following defined symbols:
+', opp', *'
They will be analysed ascendingly in the following order:
+' < *'
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))
+'(0'(x), j'(y)) → j'(+'(x, y))
+'(j'(x), 0'(y)) → j'(+'(x, y))
+'(1'(x), 1'(y)) → j'(+'(+'(x, y), 1'(#')))
+'(j'(x), j'(y)) → 1'(+'(+'(x, y), j'(#')))
+'(1'(x), j'(y)) → 0'(+'(x, y))
+'(j'(x), 1'(y)) → 0'(+'(x, y))
+'(+'(x, y), z) → +'(x, +'(y, z))
opp'(#') → #'
opp'(0'(x)) → 0'(opp'(x))
opp'(1'(x)) → j'(opp'(x))
opp'(j'(x)) → 1'(opp'(x))
-'(x, y) → +'(x, opp'(y))
*'(#', x) → #'
*'(0'(x), y) → 0'(*'(x, y))
*'(1'(x), y) → +'(0'(*'(x, y)), y)
*'(j'(x), y) → -'(0'(*'(x, y)), y)
*'(*'(x, y), z) → *'(x, *'(y, z))
*'(+'(x, y), z) → +'(*'(x, z), *'(y, z))
*'(x, +'(y, z)) → +'(*'(x, y), *'(x, z))
Types:
0' :: #':1':j' → #':1':j'
#' :: #':1':j'
+' :: #':1':j' → #':1':j' → #':1':j'
1' :: #':1':j' → #':1':j'
j' :: #':1':j' → #':1':j'
opp' :: #':1':j' → #':1':j'
-' :: #':1':j' → #':1':j' → #':1':j'
*' :: #':1':j' → #':1':j' → #':1':j'
_hole_#':1':j'1 :: #':1':j'
_gen_#':1':j'2 :: Nat → #':1':j'
Generator Equations:
_gen_#':1':j'2(0) ⇔ #'
_gen_#':1':j'2(+(x, 1)) ⇔ 1'(_gen_#':1':j'2(x))
The following defined symbols remain to be analysed:
+', opp', *'
They will be analysed ascendingly in the following order:
+' < *'
Proved the following rewrite lemma:
+'(_gen_#':1':j'2(+(1, _n4)), _gen_#':1':j'2(+(1, _n4))) → _*3, rt ∈ Ω(n4)
Induction Base:
+'(_gen_#':1':j'2(+(1, 0)), _gen_#':1':j'2(+(1, 0)))
Induction Step:
+'(_gen_#':1':j'2(+(1, +(_$n5, 1))), _gen_#':1':j'2(+(1, +(_$n5, 1)))) →RΩ(1)
j'(+'(+'(_gen_#':1':j'2(+(1, _$n5)), _gen_#':1':j'2(+(1, _$n5))), 1'(#'))) →IH
j'(+'(_*3, 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))
+'(0'(x), j'(y)) → j'(+'(x, y))
+'(j'(x), 0'(y)) → j'(+'(x, y))
+'(1'(x), 1'(y)) → j'(+'(+'(x, y), 1'(#')))
+'(j'(x), j'(y)) → 1'(+'(+'(x, y), j'(#')))
+'(1'(x), j'(y)) → 0'(+'(x, y))
+'(j'(x), 1'(y)) → 0'(+'(x, y))
+'(+'(x, y), z) → +'(x, +'(y, z))
opp'(#') → #'
opp'(0'(x)) → 0'(opp'(x))
opp'(1'(x)) → j'(opp'(x))
opp'(j'(x)) → 1'(opp'(x))
-'(x, y) → +'(x, opp'(y))
*'(#', x) → #'
*'(0'(x), y) → 0'(*'(x, y))
*'(1'(x), y) → +'(0'(*'(x, y)), y)
*'(j'(x), y) → -'(0'(*'(x, y)), y)
*'(*'(x, y), z) → *'(x, *'(y, z))
*'(+'(x, y), z) → +'(*'(x, z), *'(y, z))
*'(x, +'(y, z)) → +'(*'(x, y), *'(x, z))
Types:
0' :: #':1':j' → #':1':j'
#' :: #':1':j'
+' :: #':1':j' → #':1':j' → #':1':j'
1' :: #':1':j' → #':1':j'
j' :: #':1':j' → #':1':j'
opp' :: #':1':j' → #':1':j'
-' :: #':1':j' → #':1':j' → #':1':j'
*' :: #':1':j' → #':1':j' → #':1':j'
_hole_#':1':j'1 :: #':1':j'
_gen_#':1':j'2 :: Nat → #':1':j'
Lemmas:
+'(_gen_#':1':j'2(+(1, _n4)), _gen_#':1':j'2(+(1, _n4))) → _*3, rt ∈ Ω(n4)
Generator Equations:
_gen_#':1':j'2(0) ⇔ #'
_gen_#':1':j'2(+(x, 1)) ⇔ 1'(_gen_#':1':j'2(x))
The following defined symbols remain to be analysed:
opp', *'
Proved the following rewrite lemma:
opp'(_gen_#':1':j'2(+(1, _n4134813))) → _*3, rt ∈ Ω(n4134813)
Induction Base:
opp'(_gen_#':1':j'2(+(1, 0)))
Induction Step:
opp'(_gen_#':1':j'2(+(1, +(_$n4134814, 1)))) →RΩ(1)
j'(opp'(_gen_#':1':j'2(+(1, _$n4134814)))) →IH
j'(_*3)
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))
+'(0'(x), j'(y)) → j'(+'(x, y))
+'(j'(x), 0'(y)) → j'(+'(x, y))
+'(1'(x), 1'(y)) → j'(+'(+'(x, y), 1'(#')))
+'(j'(x), j'(y)) → 1'(+'(+'(x, y), j'(#')))
+'(1'(x), j'(y)) → 0'(+'(x, y))
+'(j'(x), 1'(y)) → 0'(+'(x, y))
+'(+'(x, y), z) → +'(x, +'(y, z))
opp'(#') → #'
opp'(0'(x)) → 0'(opp'(x))
opp'(1'(x)) → j'(opp'(x))
opp'(j'(x)) → 1'(opp'(x))
-'(x, y) → +'(x, opp'(y))
*'(#', x) → #'
*'(0'(x), y) → 0'(*'(x, y))
*'(1'(x), y) → +'(0'(*'(x, y)), y)
*'(j'(x), y) → -'(0'(*'(x, y)), y)
*'(*'(x, y), z) → *'(x, *'(y, z))
*'(+'(x, y), z) → +'(*'(x, z), *'(y, z))
*'(x, +'(y, z)) → +'(*'(x, y), *'(x, z))
Types:
0' :: #':1':j' → #':1':j'
#' :: #':1':j'
+' :: #':1':j' → #':1':j' → #':1':j'
1' :: #':1':j' → #':1':j'
j' :: #':1':j' → #':1':j'
opp' :: #':1':j' → #':1':j'
-' :: #':1':j' → #':1':j' → #':1':j'
*' :: #':1':j' → #':1':j' → #':1':j'
_hole_#':1':j'1 :: #':1':j'
_gen_#':1':j'2 :: Nat → #':1':j'
Lemmas:
+'(_gen_#':1':j'2(+(1, _n4)), _gen_#':1':j'2(+(1, _n4))) → _*3, rt ∈ Ω(n4)
opp'(_gen_#':1':j'2(+(1, _n4134813))) → _*3, rt ∈ Ω(n4134813)
Generator Equations:
_gen_#':1':j'2(0) ⇔ #'
_gen_#':1':j'2(+(x, 1)) ⇔ 1'(_gen_#':1':j'2(x))
The following defined symbols remain to be analysed:
*'
Proved the following rewrite lemma:
*'(_gen_#':1':j'2(_n4136638), _gen_#':1':j'2(0)) → _gen_#':1':j'2(0), rt ∈ Ω(1 + n4136638)
Induction Base:
*'(_gen_#':1':j'2(0), _gen_#':1':j'2(0)) →RΩ(1)
#'
Induction Step:
*'(_gen_#':1':j'2(+(_$n4136639, 1)), _gen_#':1':j'2(0)) →RΩ(1)
+'(0'(*'(_gen_#':1':j'2(_$n4136639), _gen_#':1':j'2(0))), _gen_#':1':j'2(0)) →IH
+'(0'(_gen_#':1':j'2(0)), _gen_#':1':j'2(0)) →RΩ(1)
+'(#', _gen_#':1':j'2(0)) →RΩ(1)
_gen_#':1':j'2(0)
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))
+'(0'(x), j'(y)) → j'(+'(x, y))
+'(j'(x), 0'(y)) → j'(+'(x, y))
+'(1'(x), 1'(y)) → j'(+'(+'(x, y), 1'(#')))
+'(j'(x), j'(y)) → 1'(+'(+'(x, y), j'(#')))
+'(1'(x), j'(y)) → 0'(+'(x, y))
+'(j'(x), 1'(y)) → 0'(+'(x, y))
+'(+'(x, y), z) → +'(x, +'(y, z))
opp'(#') → #'
opp'(0'(x)) → 0'(opp'(x))
opp'(1'(x)) → j'(opp'(x))
opp'(j'(x)) → 1'(opp'(x))
-'(x, y) → +'(x, opp'(y))
*'(#', x) → #'
*'(0'(x), y) → 0'(*'(x, y))
*'(1'(x), y) → +'(0'(*'(x, y)), y)
*'(j'(x), y) → -'(0'(*'(x, y)), y)
*'(*'(x, y), z) → *'(x, *'(y, z))
*'(+'(x, y), z) → +'(*'(x, z), *'(y, z))
*'(x, +'(y, z)) → +'(*'(x, y), *'(x, z))
Types:
0' :: #':1':j' → #':1':j'
#' :: #':1':j'
+' :: #':1':j' → #':1':j' → #':1':j'
1' :: #':1':j' → #':1':j'
j' :: #':1':j' → #':1':j'
opp' :: #':1':j' → #':1':j'
-' :: #':1':j' → #':1':j' → #':1':j'
*' :: #':1':j' → #':1':j' → #':1':j'
_hole_#':1':j'1 :: #':1':j'
_gen_#':1':j'2 :: Nat → #':1':j'
Lemmas:
+'(_gen_#':1':j'2(+(1, _n4)), _gen_#':1':j'2(+(1, _n4))) → _*3, rt ∈ Ω(n4)
opp'(_gen_#':1':j'2(+(1, _n4134813))) → _*3, rt ∈ Ω(n4134813)
*'(_gen_#':1':j'2(_n4136638), _gen_#':1':j'2(0)) → _gen_#':1':j'2(0), rt ∈ Ω(1 + n4136638)
Generator Equations:
_gen_#':1':j'2(0) ⇔ #'
_gen_#':1':j'2(+(x, 1)) ⇔ 1'(_gen_#':1':j'2(x))
No more defined symbols left to analyse.
The lowerbound Ω(n) was proven with the following lemma:
+'(_gen_#':1':j'2(+(1, _n4)), _gen_#':1':j'2(+(1, _n4))) → _*3, rt ∈ Ω(n4)