from(X) → cons(X, n__from(s(X)))
2ndspos(0, Z) → rnil
2ndspos(s(N), cons(X, Z)) → 2ndspos(s(N), cons2(X, activate(Z)))
2ndspos(s(N), cons2(X, cons(Y, Z))) → rcons(posrecip(Y), 2ndsneg(N, activate(Z)))
2ndsneg(0, Z) → rnil
2ndsneg(s(N), cons(X, Z)) → 2ndsneg(s(N), cons2(X, activate(Z)))
2ndsneg(s(N), cons2(X, cons(Y, Z))) → rcons(negrecip(Y), 2ndspos(N, activate(Z)))
pi(X) → 2ndspos(X, from(0))
plus(0, Y) → Y
plus(s(X), Y) → s(plus(X, Y))
times(0, Y) → 0
times(s(X), Y) → plus(Y, times(X, Y))
square(X) → times(X, X)
from(X) → n__from(X)
activate(n__from(X)) → from(X)
activate(X) → X
Renamed function symbols to avoid clashes with predefined symbol.
Runtime Complexity TRS:
The TRS R consists of the following rules:
from'(X) → cons'(X, n__from'(s'(X)))
2ndspos'(0', Z) → rnil'
2ndspos'(s'(N), cons'(X, Z)) → 2ndspos'(s'(N), cons2'(X, activate'(Z)))
2ndspos'(s'(N), cons2'(X, cons'(Y, Z))) → rcons'(posrecip'(Y), 2ndsneg'(N, activate'(Z)))
2ndsneg'(0', Z) → rnil'
2ndsneg'(s'(N), cons'(X, Z)) → 2ndsneg'(s'(N), cons2'(X, activate'(Z)))
2ndsneg'(s'(N), cons2'(X, cons'(Y, Z))) → rcons'(negrecip'(Y), 2ndspos'(N, activate'(Z)))
pi'(X) → 2ndspos'(X, from'(0'))
plus'(0', Y) → Y
plus'(s'(X), Y) → s'(plus'(X, Y))
times'(0', Y) → 0'
times'(s'(X), Y) → plus'(Y, times'(X, Y))
square'(X) → times'(X, X)
from'(X) → n__from'(X)
activate'(n__from'(X)) → from'(X)
activate'(X) → X
Sliced the following arguments:
from'/0
cons'/0
n__from'/0
cons2'/0
rcons'/0
posrecip'/0
negrecip'/0
Runtime Complexity TRS:
The TRS R consists of the following rules:
from' → cons'(n__from')
2ndspos'(0', Z) → rnil'
2ndspos'(s'(N), cons'(Z)) → 2ndspos'(s'(N), cons2'(activate'(Z)))
2ndspos'(s'(N), cons2'(cons'(Z))) → rcons'(2ndsneg'(N, activate'(Z)))
2ndsneg'(0', Z) → rnil'
2ndsneg'(s'(N), cons'(Z)) → 2ndsneg'(s'(N), cons2'(activate'(Z)))
2ndsneg'(s'(N), cons2'(cons'(Z))) → rcons'(2ndspos'(N, activate'(Z)))
pi'(X) → 2ndspos'(X, from')
plus'(0', Y) → Y
plus'(s'(X), Y) → s'(plus'(X, Y))
times'(0', Y) → 0'
times'(s'(X), Y) → plus'(Y, times'(X, Y))
square'(X) → times'(X, X)
from' → n__from'
activate'(n__from') → from'
activate'(X) → X
Infered types.
Rules:
from' → cons'(n__from')
2ndspos'(0', Z) → rnil'
2ndspos'(s'(N), cons'(Z)) → 2ndspos'(s'(N), cons2'(activate'(Z)))
2ndspos'(s'(N), cons2'(cons'(Z))) → rcons'(2ndsneg'(N, activate'(Z)))
2ndsneg'(0', Z) → rnil'
2ndsneg'(s'(N), cons'(Z)) → 2ndsneg'(s'(N), cons2'(activate'(Z)))
2ndsneg'(s'(N), cons2'(cons'(Z))) → rcons'(2ndspos'(N, activate'(Z)))
pi'(X) → 2ndspos'(X, from')
plus'(0', Y) → Y
plus'(s'(X), Y) → s'(plus'(X, Y))
times'(0', Y) → 0'
times'(s'(X), Y) → plus'(Y, times'(X, Y))
square'(X) → times'(X, X)
from' → n__from'
activate'(n__from') → from'
activate'(X) → X
Types:
from' :: n__from':cons':cons2'
cons' :: n__from':cons':cons2' → n__from':cons':cons2'
n__from' :: n__from':cons':cons2'
2ndspos' :: 0':s' → n__from':cons':cons2' → rnil':rcons'
0' :: 0':s'
rnil' :: rnil':rcons'
s' :: 0':s' → 0':s'
cons2' :: n__from':cons':cons2' → n__from':cons':cons2'
activate' :: n__from':cons':cons2' → n__from':cons':cons2'
rcons' :: rnil':rcons' → rnil':rcons'
2ndsneg' :: 0':s' → n__from':cons':cons2' → rnil':rcons'
pi' :: 0':s' → rnil':rcons'
plus' :: 0':s' → 0':s' → 0':s'
times' :: 0':s' → 0':s' → 0':s'
square' :: 0':s' → 0':s'
_hole_n__from':cons':cons2'1 :: n__from':cons':cons2'
_hole_rnil':rcons'2 :: rnil':rcons'
_hole_0':s'3 :: 0':s'
_gen_n__from':cons':cons2'4 :: Nat → n__from':cons':cons2'
_gen_rnil':rcons'5 :: Nat → rnil':rcons'
_gen_0':s'6 :: Nat → 0':s'
Heuristically decided to analyse the following defined symbols:
2ndspos', 2ndsneg', plus', times'
They will be analysed ascendingly in the following order:
2ndspos' = 2ndsneg'
plus' < times'
Rules:
from' → cons'(n__from')
2ndspos'(0', Z) → rnil'
2ndspos'(s'(N), cons'(Z)) → 2ndspos'(s'(N), cons2'(activate'(Z)))
2ndspos'(s'(N), cons2'(cons'(Z))) → rcons'(2ndsneg'(N, activate'(Z)))
2ndsneg'(0', Z) → rnil'
2ndsneg'(s'(N), cons'(Z)) → 2ndsneg'(s'(N), cons2'(activate'(Z)))
2ndsneg'(s'(N), cons2'(cons'(Z))) → rcons'(2ndspos'(N, activate'(Z)))
pi'(X) → 2ndspos'(X, from')
plus'(0', Y) → Y
plus'(s'(X), Y) → s'(plus'(X, Y))
times'(0', Y) → 0'
times'(s'(X), Y) → plus'(Y, times'(X, Y))
square'(X) → times'(X, X)
from' → n__from'
activate'(n__from') → from'
activate'(X) → X
Types:
from' :: n__from':cons':cons2'
cons' :: n__from':cons':cons2' → n__from':cons':cons2'
n__from' :: n__from':cons':cons2'
2ndspos' :: 0':s' → n__from':cons':cons2' → rnil':rcons'
0' :: 0':s'
rnil' :: rnil':rcons'
s' :: 0':s' → 0':s'
cons2' :: n__from':cons':cons2' → n__from':cons':cons2'
activate' :: n__from':cons':cons2' → n__from':cons':cons2'
rcons' :: rnil':rcons' → rnil':rcons'
2ndsneg' :: 0':s' → n__from':cons':cons2' → rnil':rcons'
pi' :: 0':s' → rnil':rcons'
plus' :: 0':s' → 0':s' → 0':s'
times' :: 0':s' → 0':s' → 0':s'
square' :: 0':s' → 0':s'
_hole_n__from':cons':cons2'1 :: n__from':cons':cons2'
_hole_rnil':rcons'2 :: rnil':rcons'
_hole_0':s'3 :: 0':s'
_gen_n__from':cons':cons2'4 :: Nat → n__from':cons':cons2'
_gen_rnil':rcons'5 :: Nat → rnil':rcons'
_gen_0':s'6 :: Nat → 0':s'
Generator Equations:
_gen_n__from':cons':cons2'4(0) ⇔ n__from'
_gen_n__from':cons':cons2'4(+(x, 1)) ⇔ cons'(_gen_n__from':cons':cons2'4(x))
_gen_rnil':rcons'5(0) ⇔ rnil'
_gen_rnil':rcons'5(+(x, 1)) ⇔ rcons'(_gen_rnil':rcons'5(x))
_gen_0':s'6(0) ⇔ 0'
_gen_0':s'6(+(x, 1)) ⇔ s'(_gen_0':s'6(x))
The following defined symbols remain to be analysed:
plus', 2ndspos', 2ndsneg', times'
They will be analysed ascendingly in the following order:
2ndspos' = 2ndsneg'
plus' < times'
Proved the following rewrite lemma:
plus'(_gen_0':s'6(_n8), _gen_0':s'6(b)) → _gen_0':s'6(+(_n8, b)), rt ∈ Ω(1 + n8)
Induction Base:
plus'(_gen_0':s'6(0), _gen_0':s'6(b)) →RΩ(1)
_gen_0':s'6(b)
Induction Step:
plus'(_gen_0':s'6(+(_$n9, 1)), _gen_0':s'6(_b321)) →RΩ(1)
s'(plus'(_gen_0':s'6(_$n9), _gen_0':s'6(_b321))) →IH
s'(_gen_0':s'6(+(_$n9, _b321)))
We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).
Rules:
from' → cons'(n__from')
2ndspos'(0', Z) → rnil'
2ndspos'(s'(N), cons'(Z)) → 2ndspos'(s'(N), cons2'(activate'(Z)))
2ndspos'(s'(N), cons2'(cons'(Z))) → rcons'(2ndsneg'(N, activate'(Z)))
2ndsneg'(0', Z) → rnil'
2ndsneg'(s'(N), cons'(Z)) → 2ndsneg'(s'(N), cons2'(activate'(Z)))
2ndsneg'(s'(N), cons2'(cons'(Z))) → rcons'(2ndspos'(N, activate'(Z)))
pi'(X) → 2ndspos'(X, from')
plus'(0', Y) → Y
plus'(s'(X), Y) → s'(plus'(X, Y))
times'(0', Y) → 0'
times'(s'(X), Y) → plus'(Y, times'(X, Y))
square'(X) → times'(X, X)
from' → n__from'
activate'(n__from') → from'
activate'(X) → X
Types:
from' :: n__from':cons':cons2'
cons' :: n__from':cons':cons2' → n__from':cons':cons2'
n__from' :: n__from':cons':cons2'
2ndspos' :: 0':s' → n__from':cons':cons2' → rnil':rcons'
0' :: 0':s'
rnil' :: rnil':rcons'
s' :: 0':s' → 0':s'
cons2' :: n__from':cons':cons2' → n__from':cons':cons2'
activate' :: n__from':cons':cons2' → n__from':cons':cons2'
rcons' :: rnil':rcons' → rnil':rcons'
2ndsneg' :: 0':s' → n__from':cons':cons2' → rnil':rcons'
pi' :: 0':s' → rnil':rcons'
plus' :: 0':s' → 0':s' → 0':s'
times' :: 0':s' → 0':s' → 0':s'
square' :: 0':s' → 0':s'
_hole_n__from':cons':cons2'1 :: n__from':cons':cons2'
_hole_rnil':rcons'2 :: rnil':rcons'
_hole_0':s'3 :: 0':s'
_gen_n__from':cons':cons2'4 :: Nat → n__from':cons':cons2'
_gen_rnil':rcons'5 :: Nat → rnil':rcons'
_gen_0':s'6 :: Nat → 0':s'
Lemmas:
plus'(_gen_0':s'6(_n8), _gen_0':s'6(b)) → _gen_0':s'6(+(_n8, b)), rt ∈ Ω(1 + n8)
Generator Equations:
_gen_n__from':cons':cons2'4(0) ⇔ n__from'
_gen_n__from':cons':cons2'4(+(x, 1)) ⇔ cons'(_gen_n__from':cons':cons2'4(x))
_gen_rnil':rcons'5(0) ⇔ rnil'
_gen_rnil':rcons'5(+(x, 1)) ⇔ rcons'(_gen_rnil':rcons'5(x))
_gen_0':s'6(0) ⇔ 0'
_gen_0':s'6(+(x, 1)) ⇔ s'(_gen_0':s'6(x))
The following defined symbols remain to be analysed:
times', 2ndspos', 2ndsneg'
They will be analysed ascendingly in the following order:
2ndspos' = 2ndsneg'
Proved the following rewrite lemma:
times'(_gen_0':s'6(_n1033), _gen_0':s'6(b)) → _gen_0':s'6(*(_n1033, b)), rt ∈ Ω(1 + b1581·n1033 + n1033)
Induction Base:
times'(_gen_0':s'6(0), _gen_0':s'6(b)) →RΩ(1)
0'
Induction Step:
times'(_gen_0':s'6(+(_$n1034, 1)), _gen_0':s'6(_b1581)) →RΩ(1)
plus'(_gen_0':s'6(_b1581), times'(_gen_0':s'6(_$n1034), _gen_0':s'6(_b1581))) →IH
plus'(_gen_0':s'6(_b1581), _gen_0':s'6(*(_$n1034, _b1581))) →LΩ(1 + b1581)
_gen_0':s'6(+(_b1581, *(_$n1034, _b1581)))
We have rt ∈ Ω(n2) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n2).
Rules:
from' → cons'(n__from')
2ndspos'(0', Z) → rnil'
2ndspos'(s'(N), cons'(Z)) → 2ndspos'(s'(N), cons2'(activate'(Z)))
2ndspos'(s'(N), cons2'(cons'(Z))) → rcons'(2ndsneg'(N, activate'(Z)))
2ndsneg'(0', Z) → rnil'
2ndsneg'(s'(N), cons'(Z)) → 2ndsneg'(s'(N), cons2'(activate'(Z)))
2ndsneg'(s'(N), cons2'(cons'(Z))) → rcons'(2ndspos'(N, activate'(Z)))
pi'(X) → 2ndspos'(X, from')
plus'(0', Y) → Y
plus'(s'(X), Y) → s'(plus'(X, Y))
times'(0', Y) → 0'
times'(s'(X), Y) → plus'(Y, times'(X, Y))
square'(X) → times'(X, X)
from' → n__from'
activate'(n__from') → from'
activate'(X) → X
Types:
from' :: n__from':cons':cons2'
cons' :: n__from':cons':cons2' → n__from':cons':cons2'
n__from' :: n__from':cons':cons2'
2ndspos' :: 0':s' → n__from':cons':cons2' → rnil':rcons'
0' :: 0':s'
rnil' :: rnil':rcons'
s' :: 0':s' → 0':s'
cons2' :: n__from':cons':cons2' → n__from':cons':cons2'
activate' :: n__from':cons':cons2' → n__from':cons':cons2'
rcons' :: rnil':rcons' → rnil':rcons'
2ndsneg' :: 0':s' → n__from':cons':cons2' → rnil':rcons'
pi' :: 0':s' → rnil':rcons'
plus' :: 0':s' → 0':s' → 0':s'
times' :: 0':s' → 0':s' → 0':s'
square' :: 0':s' → 0':s'
_hole_n__from':cons':cons2'1 :: n__from':cons':cons2'
_hole_rnil':rcons'2 :: rnil':rcons'
_hole_0':s'3 :: 0':s'
_gen_n__from':cons':cons2'4 :: Nat → n__from':cons':cons2'
_gen_rnil':rcons'5 :: Nat → rnil':rcons'
_gen_0':s'6 :: Nat → 0':s'
Lemmas:
plus'(_gen_0':s'6(_n8), _gen_0':s'6(b)) → _gen_0':s'6(+(_n8, b)), rt ∈ Ω(1 + n8)
times'(_gen_0':s'6(_n1033), _gen_0':s'6(b)) → _gen_0':s'6(*(_n1033, b)), rt ∈ Ω(1 + b1581·n1033 + n1033)
Generator Equations:
_gen_n__from':cons':cons2'4(0) ⇔ n__from'
_gen_n__from':cons':cons2'4(+(x, 1)) ⇔ cons'(_gen_n__from':cons':cons2'4(x))
_gen_rnil':rcons'5(0) ⇔ rnil'
_gen_rnil':rcons'5(+(x, 1)) ⇔ rcons'(_gen_rnil':rcons'5(x))
_gen_0':s'6(0) ⇔ 0'
_gen_0':s'6(+(x, 1)) ⇔ s'(_gen_0':s'6(x))
The following defined symbols remain to be analysed:
2ndsneg', 2ndspos'
They will be analysed ascendingly in the following order:
2ndspos' = 2ndsneg'
Could not prove a rewrite lemma for the defined symbol 2ndsneg'.
The following conjecture could not be proven:
2ndsneg'(_gen_0':s'6(_n2566), _gen_n__from':cons':cons2'4(1)) →? _gen_rnil':rcons'5(_n2566)
Rules:
from' → cons'(n__from')
2ndspos'(0', Z) → rnil'
2ndspos'(s'(N), cons'(Z)) → 2ndspos'(s'(N), cons2'(activate'(Z)))
2ndspos'(s'(N), cons2'(cons'(Z))) → rcons'(2ndsneg'(N, activate'(Z)))
2ndsneg'(0', Z) → rnil'
2ndsneg'(s'(N), cons'(Z)) → 2ndsneg'(s'(N), cons2'(activate'(Z)))
2ndsneg'(s'(N), cons2'(cons'(Z))) → rcons'(2ndspos'(N, activate'(Z)))
pi'(X) → 2ndspos'(X, from')
plus'(0', Y) → Y
plus'(s'(X), Y) → s'(plus'(X, Y))
times'(0', Y) → 0'
times'(s'(X), Y) → plus'(Y, times'(X, Y))
square'(X) → times'(X, X)
from' → n__from'
activate'(n__from') → from'
activate'(X) → X
Types:
from' :: n__from':cons':cons2'
cons' :: n__from':cons':cons2' → n__from':cons':cons2'
n__from' :: n__from':cons':cons2'
2ndspos' :: 0':s' → n__from':cons':cons2' → rnil':rcons'
0' :: 0':s'
rnil' :: rnil':rcons'
s' :: 0':s' → 0':s'
cons2' :: n__from':cons':cons2' → n__from':cons':cons2'
activate' :: n__from':cons':cons2' → n__from':cons':cons2'
rcons' :: rnil':rcons' → rnil':rcons'
2ndsneg' :: 0':s' → n__from':cons':cons2' → rnil':rcons'
pi' :: 0':s' → rnil':rcons'
plus' :: 0':s' → 0':s' → 0':s'
times' :: 0':s' → 0':s' → 0':s'
square' :: 0':s' → 0':s'
_hole_n__from':cons':cons2'1 :: n__from':cons':cons2'
_hole_rnil':rcons'2 :: rnil':rcons'
_hole_0':s'3 :: 0':s'
_gen_n__from':cons':cons2'4 :: Nat → n__from':cons':cons2'
_gen_rnil':rcons'5 :: Nat → rnil':rcons'
_gen_0':s'6 :: Nat → 0':s'
Lemmas:
plus'(_gen_0':s'6(_n8), _gen_0':s'6(b)) → _gen_0':s'6(+(_n8, b)), rt ∈ Ω(1 + n8)
times'(_gen_0':s'6(_n1033), _gen_0':s'6(b)) → _gen_0':s'6(*(_n1033, b)), rt ∈ Ω(1 + b1581·n1033 + n1033)
Generator Equations:
_gen_n__from':cons':cons2'4(0) ⇔ n__from'
_gen_n__from':cons':cons2'4(+(x, 1)) ⇔ cons'(_gen_n__from':cons':cons2'4(x))
_gen_rnil':rcons'5(0) ⇔ rnil'
_gen_rnil':rcons'5(+(x, 1)) ⇔ rcons'(_gen_rnil':rcons'5(x))
_gen_0':s'6(0) ⇔ 0'
_gen_0':s'6(+(x, 1)) ⇔ s'(_gen_0':s'6(x))
The following defined symbols remain to be analysed:
2ndspos'
They will be analysed ascendingly in the following order:
2ndspos' = 2ndsneg'
Could not prove a rewrite lemma for the defined symbol 2ndspos'.
The following conjecture could not be proven:
2ndspos'(_gen_0':s'6(_n10278), _gen_n__from':cons':cons2'4(1)) →? _gen_rnil':rcons'5(_n10278)
Rules:
from' → cons'(n__from')
2ndspos'(0', Z) → rnil'
2ndspos'(s'(N), cons'(Z)) → 2ndspos'(s'(N), cons2'(activate'(Z)))
2ndspos'(s'(N), cons2'(cons'(Z))) → rcons'(2ndsneg'(N, activate'(Z)))
2ndsneg'(0', Z) → rnil'
2ndsneg'(s'(N), cons'(Z)) → 2ndsneg'(s'(N), cons2'(activate'(Z)))
2ndsneg'(s'(N), cons2'(cons'(Z))) → rcons'(2ndspos'(N, activate'(Z)))
pi'(X) → 2ndspos'(X, from')
plus'(0', Y) → Y
plus'(s'(X), Y) → s'(plus'(X, Y))
times'(0', Y) → 0'
times'(s'(X), Y) → plus'(Y, times'(X, Y))
square'(X) → times'(X, X)
from' → n__from'
activate'(n__from') → from'
activate'(X) → X
Types:
from' :: n__from':cons':cons2'
cons' :: n__from':cons':cons2' → n__from':cons':cons2'
n__from' :: n__from':cons':cons2'
2ndspos' :: 0':s' → n__from':cons':cons2' → rnil':rcons'
0' :: 0':s'
rnil' :: rnil':rcons'
s' :: 0':s' → 0':s'
cons2' :: n__from':cons':cons2' → n__from':cons':cons2'
activate' :: n__from':cons':cons2' → n__from':cons':cons2'
rcons' :: rnil':rcons' → rnil':rcons'
2ndsneg' :: 0':s' → n__from':cons':cons2' → rnil':rcons'
pi' :: 0':s' → rnil':rcons'
plus' :: 0':s' → 0':s' → 0':s'
times' :: 0':s' → 0':s' → 0':s'
square' :: 0':s' → 0':s'
_hole_n__from':cons':cons2'1 :: n__from':cons':cons2'
_hole_rnil':rcons'2 :: rnil':rcons'
_hole_0':s'3 :: 0':s'
_gen_n__from':cons':cons2'4 :: Nat → n__from':cons':cons2'
_gen_rnil':rcons'5 :: Nat → rnil':rcons'
_gen_0':s'6 :: Nat → 0':s'
Lemmas:
plus'(_gen_0':s'6(_n8), _gen_0':s'6(b)) → _gen_0':s'6(+(_n8, b)), rt ∈ Ω(1 + n8)
times'(_gen_0':s'6(_n1033), _gen_0':s'6(b)) → _gen_0':s'6(*(_n1033, b)), rt ∈ Ω(1 + b1581·n1033 + n1033)
Generator Equations:
_gen_n__from':cons':cons2'4(0) ⇔ n__from'
_gen_n__from':cons':cons2'4(+(x, 1)) ⇔ cons'(_gen_n__from':cons':cons2'4(x))
_gen_rnil':rcons'5(0) ⇔ rnil'
_gen_rnil':rcons'5(+(x, 1)) ⇔ rcons'(_gen_rnil':rcons'5(x))
_gen_0':s'6(0) ⇔ 0'
_gen_0':s'6(+(x, 1)) ⇔ s'(_gen_0':s'6(x))
No more defined symbols left to analyse.
The lowerbound Ω(n2) was proven with the following lemma:
times'(_gen_0':s'6(_n1033), _gen_0':s'6(b)) → _gen_0':s'6(*(_n1033, b)), rt ∈ Ω(1 + b1581·n1033 + n1033)