(0) Obligation:
Runtime Complexity TRS:
The TRS R consists of the following rules:
terms(N) → cons(recip(sqr(N)))
sqr(0) → 0
sqr(s(X)) → s(add(sqr(X), dbl(X)))
dbl(0) → 0
dbl(s(X)) → s(s(dbl(X)))
add(0, X) → X
add(s(X), Y) → s(add(X, Y))
first(0, X) → nil
first(s(X), cons(Y)) → cons(Y)
half(0) → 0
half(s(0)) → 0
half(s(s(X))) → s(half(X))
half(dbl(X)) → X
Rewrite Strategy: INNERMOST
(1) DecreasingLoopProof (EQUIVALENT transformation)
The following loop(s) give(s) rise to the lower bound Ω(n1):
The rewrite sequence
sqr(s(X)) →+ s(add(sqr(X), dbl(X)))
gives rise to a decreasing loop by considering the right hand sides subterm at position [0,0].
The pumping substitution is [X / s(X)].
The result substitution is [ ].
(2) BOUNDS(n^1, INF)
(3) RenamingProof (EQUIVALENT transformation)
Renamed function symbols to avoid clashes with predefined symbol.
(4) Obligation:
Runtime Complexity Relative TRS:
The TRS R consists of the following rules:
terms(N) → cons(recip(sqr(N)))
sqr(0') → 0'
sqr(s(X)) → s(add(sqr(X), dbl(X)))
dbl(0') → 0'
dbl(s(X)) → s(s(dbl(X)))
add(0', X) → X
add(s(X), Y) → s(add(X, Y))
first(0', X) → nil
first(s(X), cons(Y)) → cons(Y)
half(0') → 0'
half(s(0')) → 0'
half(s(s(X))) → s(half(X))
half(dbl(X)) → X
S is empty.
Rewrite Strategy: INNERMOST
(5) TypeInferenceProof (BOTH BOUNDS(ID, ID) transformation)
Infered types.
(6) Obligation:
Innermost TRS:
Rules:
terms(N) → cons(recip(sqr(N)))
sqr(0') → 0'
sqr(s(X)) → s(add(sqr(X), dbl(X)))
dbl(0') → 0'
dbl(s(X)) → s(s(dbl(X)))
add(0', X) → X
add(s(X), Y) → s(add(X, Y))
first(0', X) → nil
first(s(X), cons(Y)) → cons(Y)
half(0') → 0'
half(s(0')) → 0'
half(s(s(X))) → s(half(X))
half(dbl(X)) → X
Types:
terms :: 0':s → cons:nil
cons :: recip → cons:nil
recip :: 0':s → recip
sqr :: 0':s → 0':s
0' :: 0':s
s :: 0':s → 0':s
add :: 0':s → 0':s → 0':s
dbl :: 0':s → 0':s
first :: 0':s → cons:nil → cons:nil
nil :: cons:nil
half :: 0':s → 0':s
hole_cons:nil1_0 :: cons:nil
hole_0':s2_0 :: 0':s
hole_recip3_0 :: recip
gen_0':s4_0 :: Nat → 0':s
(7) OrderProof (LOWER BOUND(ID) transformation)
Heuristically decided to analyse the following defined symbols:
sqr,
add,
dbl,
halfThey will be analysed ascendingly in the following order:
add < sqr
dbl < sqr
(8) Obligation:
Innermost TRS:
Rules:
terms(
N) →
cons(
recip(
sqr(
N)))
sqr(
0') →
0'sqr(
s(
X)) →
s(
add(
sqr(
X),
dbl(
X)))
dbl(
0') →
0'dbl(
s(
X)) →
s(
s(
dbl(
X)))
add(
0',
X) →
Xadd(
s(
X),
Y) →
s(
add(
X,
Y))
first(
0',
X) →
nilfirst(
s(
X),
cons(
Y)) →
cons(
Y)
half(
0') →
0'half(
s(
0')) →
0'half(
s(
s(
X))) →
s(
half(
X))
half(
dbl(
X)) →
XTypes:
terms :: 0':s → cons:nil
cons :: recip → cons:nil
recip :: 0':s → recip
sqr :: 0':s → 0':s
0' :: 0':s
s :: 0':s → 0':s
add :: 0':s → 0':s → 0':s
dbl :: 0':s → 0':s
first :: 0':s → cons:nil → cons:nil
nil :: cons:nil
half :: 0':s → 0':s
hole_cons:nil1_0 :: cons:nil
hole_0':s2_0 :: 0':s
hole_recip3_0 :: recip
gen_0':s4_0 :: Nat → 0':s
Generator Equations:
gen_0':s4_0(0) ⇔ 0'
gen_0':s4_0(+(x, 1)) ⇔ s(gen_0':s4_0(x))
The following defined symbols remain to be analysed:
add, sqr, dbl, half
They will be analysed ascendingly in the following order:
add < sqr
dbl < sqr
(9) RewriteLemmaProof (LOWER BOUND(ID) transformation)
Proved the following rewrite lemma:
add(
gen_0':s4_0(
n6_0),
gen_0':s4_0(
b)) →
gen_0':s4_0(
+(
n6_0,
b)), rt ∈ Ω(1 + n6
0)
Induction Base:
add(gen_0':s4_0(0), gen_0':s4_0(b)) →RΩ(1)
gen_0':s4_0(b)
Induction Step:
add(gen_0':s4_0(+(n6_0, 1)), gen_0':s4_0(b)) →RΩ(1)
s(add(gen_0':s4_0(n6_0), gen_0':s4_0(b))) →IH
s(gen_0':s4_0(+(b, c7_0)))
We have rt ∈ Ω(n1) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).
(10) Complex Obligation (BEST)
(11) Obligation:
Innermost TRS:
Rules:
terms(
N) →
cons(
recip(
sqr(
N)))
sqr(
0') →
0'sqr(
s(
X)) →
s(
add(
sqr(
X),
dbl(
X)))
dbl(
0') →
0'dbl(
s(
X)) →
s(
s(
dbl(
X)))
add(
0',
X) →
Xadd(
s(
X),
Y) →
s(
add(
X,
Y))
first(
0',
X) →
nilfirst(
s(
X),
cons(
Y)) →
cons(
Y)
half(
0') →
0'half(
s(
0')) →
0'half(
s(
s(
X))) →
s(
half(
X))
half(
dbl(
X)) →
XTypes:
terms :: 0':s → cons:nil
cons :: recip → cons:nil
recip :: 0':s → recip
sqr :: 0':s → 0':s
0' :: 0':s
s :: 0':s → 0':s
add :: 0':s → 0':s → 0':s
dbl :: 0':s → 0':s
first :: 0':s → cons:nil → cons:nil
nil :: cons:nil
half :: 0':s → 0':s
hole_cons:nil1_0 :: cons:nil
hole_0':s2_0 :: 0':s
hole_recip3_0 :: recip
gen_0':s4_0 :: Nat → 0':s
Lemmas:
add(gen_0':s4_0(n6_0), gen_0':s4_0(b)) → gen_0':s4_0(+(n6_0, b)), rt ∈ Ω(1 + n60)
Generator Equations:
gen_0':s4_0(0) ⇔ 0'
gen_0':s4_0(+(x, 1)) ⇔ s(gen_0':s4_0(x))
The following defined symbols remain to be analysed:
dbl, sqr, half
They will be analysed ascendingly in the following order:
dbl < sqr
(12) RewriteLemmaProof (LOWER BOUND(ID) transformation)
Proved the following rewrite lemma:
dbl(
gen_0':s4_0(
n667_0)) →
gen_0':s4_0(
*(
2,
n667_0)), rt ∈ Ω(1 + n667
0)
Induction Base:
dbl(gen_0':s4_0(0)) →RΩ(1)
0'
Induction Step:
dbl(gen_0':s4_0(+(n667_0, 1))) →RΩ(1)
s(s(dbl(gen_0':s4_0(n667_0)))) →IH
s(s(gen_0':s4_0(*(2, c668_0))))
We have rt ∈ Ω(n1) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).
(13) Complex Obligation (BEST)
(14) Obligation:
Innermost TRS:
Rules:
terms(
N) →
cons(
recip(
sqr(
N)))
sqr(
0') →
0'sqr(
s(
X)) →
s(
add(
sqr(
X),
dbl(
X)))
dbl(
0') →
0'dbl(
s(
X)) →
s(
s(
dbl(
X)))
add(
0',
X) →
Xadd(
s(
X),
Y) →
s(
add(
X,
Y))
first(
0',
X) →
nilfirst(
s(
X),
cons(
Y)) →
cons(
Y)
half(
0') →
0'half(
s(
0')) →
0'half(
s(
s(
X))) →
s(
half(
X))
half(
dbl(
X)) →
XTypes:
terms :: 0':s → cons:nil
cons :: recip → cons:nil
recip :: 0':s → recip
sqr :: 0':s → 0':s
0' :: 0':s
s :: 0':s → 0':s
add :: 0':s → 0':s → 0':s
dbl :: 0':s → 0':s
first :: 0':s → cons:nil → cons:nil
nil :: cons:nil
half :: 0':s → 0':s
hole_cons:nil1_0 :: cons:nil
hole_0':s2_0 :: 0':s
hole_recip3_0 :: recip
gen_0':s4_0 :: Nat → 0':s
Lemmas:
add(gen_0':s4_0(n6_0), gen_0':s4_0(b)) → gen_0':s4_0(+(n6_0, b)), rt ∈ Ω(1 + n60)
dbl(gen_0':s4_0(n667_0)) → gen_0':s4_0(*(2, n667_0)), rt ∈ Ω(1 + n6670)
Generator Equations:
gen_0':s4_0(0) ⇔ 0'
gen_0':s4_0(+(x, 1)) ⇔ s(gen_0':s4_0(x))
The following defined symbols remain to be analysed:
sqr, half
(15) RewriteLemmaProof (LOWER BOUND(ID) transformation)
Proved the following rewrite lemma:
sqr(
gen_0':s4_0(
n967_0)) →
gen_0':s4_0(
*(
n967_0,
n967_0)), rt ∈ Ω(1 + n967
0 + n967
02 + n967
03)
Induction Base:
sqr(gen_0':s4_0(0)) →RΩ(1)
0'
Induction Step:
sqr(gen_0':s4_0(+(n967_0, 1))) →RΩ(1)
s(add(sqr(gen_0':s4_0(n967_0)), dbl(gen_0':s4_0(n967_0)))) →IH
s(add(gen_0':s4_0(*(c968_0, c968_0)), dbl(gen_0':s4_0(n967_0)))) →LΩ(1 + n9670)
s(add(gen_0':s4_0(*(n967_0, n967_0)), gen_0':s4_0(*(2, n967_0)))) →LΩ(1 + n96702)
s(gen_0':s4_0(+(*(n967_0, n967_0), *(2, n967_0))))
We have rt ∈ Ω(n3) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n3).
(16) Complex Obligation (BEST)
(17) Obligation:
Innermost TRS:
Rules:
terms(
N) →
cons(
recip(
sqr(
N)))
sqr(
0') →
0'sqr(
s(
X)) →
s(
add(
sqr(
X),
dbl(
X)))
dbl(
0') →
0'dbl(
s(
X)) →
s(
s(
dbl(
X)))
add(
0',
X) →
Xadd(
s(
X),
Y) →
s(
add(
X,
Y))
first(
0',
X) →
nilfirst(
s(
X),
cons(
Y)) →
cons(
Y)
half(
0') →
0'half(
s(
0')) →
0'half(
s(
s(
X))) →
s(
half(
X))
half(
dbl(
X)) →
XTypes:
terms :: 0':s → cons:nil
cons :: recip → cons:nil
recip :: 0':s → recip
sqr :: 0':s → 0':s
0' :: 0':s
s :: 0':s → 0':s
add :: 0':s → 0':s → 0':s
dbl :: 0':s → 0':s
first :: 0':s → cons:nil → cons:nil
nil :: cons:nil
half :: 0':s → 0':s
hole_cons:nil1_0 :: cons:nil
hole_0':s2_0 :: 0':s
hole_recip3_0 :: recip
gen_0':s4_0 :: Nat → 0':s
Lemmas:
add(gen_0':s4_0(n6_0), gen_0':s4_0(b)) → gen_0':s4_0(+(n6_0, b)), rt ∈ Ω(1 + n60)
dbl(gen_0':s4_0(n667_0)) → gen_0':s4_0(*(2, n667_0)), rt ∈ Ω(1 + n6670)
sqr(gen_0':s4_0(n967_0)) → gen_0':s4_0(*(n967_0, n967_0)), rt ∈ Ω(1 + n9670 + n96702 + n96703)
Generator Equations:
gen_0':s4_0(0) ⇔ 0'
gen_0':s4_0(+(x, 1)) ⇔ s(gen_0':s4_0(x))
The following defined symbols remain to be analysed:
half
(18) RewriteLemmaProof (LOWER BOUND(ID) transformation)
Proved the following rewrite lemma:
half(
gen_0':s4_0(
*(
2,
n1380_0))) →
gen_0':s4_0(
n1380_0), rt ∈ Ω(1 + n1380
0)
Induction Base:
half(gen_0':s4_0(*(2, 0))) →RΩ(1)
0'
Induction Step:
half(gen_0':s4_0(*(2, +(n1380_0, 1)))) →RΩ(1)
s(half(gen_0':s4_0(*(2, n1380_0)))) →IH
s(gen_0':s4_0(c1381_0))
We have rt ∈ Ω(n1) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).
(19) Complex Obligation (BEST)
(20) Obligation:
Innermost TRS:
Rules:
terms(
N) →
cons(
recip(
sqr(
N)))
sqr(
0') →
0'sqr(
s(
X)) →
s(
add(
sqr(
X),
dbl(
X)))
dbl(
0') →
0'dbl(
s(
X)) →
s(
s(
dbl(
X)))
add(
0',
X) →
Xadd(
s(
X),
Y) →
s(
add(
X,
Y))
first(
0',
X) →
nilfirst(
s(
X),
cons(
Y)) →
cons(
Y)
half(
0') →
0'half(
s(
0')) →
0'half(
s(
s(
X))) →
s(
half(
X))
half(
dbl(
X)) →
XTypes:
terms :: 0':s → cons:nil
cons :: recip → cons:nil
recip :: 0':s → recip
sqr :: 0':s → 0':s
0' :: 0':s
s :: 0':s → 0':s
add :: 0':s → 0':s → 0':s
dbl :: 0':s → 0':s
first :: 0':s → cons:nil → cons:nil
nil :: cons:nil
half :: 0':s → 0':s
hole_cons:nil1_0 :: cons:nil
hole_0':s2_0 :: 0':s
hole_recip3_0 :: recip
gen_0':s4_0 :: Nat → 0':s
Lemmas:
add(gen_0':s4_0(n6_0), gen_0':s4_0(b)) → gen_0':s4_0(+(n6_0, b)), rt ∈ Ω(1 + n60)
dbl(gen_0':s4_0(n667_0)) → gen_0':s4_0(*(2, n667_0)), rt ∈ Ω(1 + n6670)
sqr(gen_0':s4_0(n967_0)) → gen_0':s4_0(*(n967_0, n967_0)), rt ∈ Ω(1 + n9670 + n96702 + n96703)
half(gen_0':s4_0(*(2, n1380_0))) → gen_0':s4_0(n1380_0), rt ∈ Ω(1 + n13800)
Generator Equations:
gen_0':s4_0(0) ⇔ 0'
gen_0':s4_0(+(x, 1)) ⇔ s(gen_0':s4_0(x))
No more defined symbols left to analyse.
(21) LowerBoundsProof (EQUIVALENT transformation)
The lowerbound Ω(n3) was proven with the following lemma:
sqr(gen_0':s4_0(n967_0)) → gen_0':s4_0(*(n967_0, n967_0)), rt ∈ Ω(1 + n9670 + n96702 + n96703)
(22) BOUNDS(n^3, INF)
(23) Obligation:
Innermost TRS:
Rules:
terms(
N) →
cons(
recip(
sqr(
N)))
sqr(
0') →
0'sqr(
s(
X)) →
s(
add(
sqr(
X),
dbl(
X)))
dbl(
0') →
0'dbl(
s(
X)) →
s(
s(
dbl(
X)))
add(
0',
X) →
Xadd(
s(
X),
Y) →
s(
add(
X,
Y))
first(
0',
X) →
nilfirst(
s(
X),
cons(
Y)) →
cons(
Y)
half(
0') →
0'half(
s(
0')) →
0'half(
s(
s(
X))) →
s(
half(
X))
half(
dbl(
X)) →
XTypes:
terms :: 0':s → cons:nil
cons :: recip → cons:nil
recip :: 0':s → recip
sqr :: 0':s → 0':s
0' :: 0':s
s :: 0':s → 0':s
add :: 0':s → 0':s → 0':s
dbl :: 0':s → 0':s
first :: 0':s → cons:nil → cons:nil
nil :: cons:nil
half :: 0':s → 0':s
hole_cons:nil1_0 :: cons:nil
hole_0':s2_0 :: 0':s
hole_recip3_0 :: recip
gen_0':s4_0 :: Nat → 0':s
Lemmas:
add(gen_0':s4_0(n6_0), gen_0':s4_0(b)) → gen_0':s4_0(+(n6_0, b)), rt ∈ Ω(1 + n60)
dbl(gen_0':s4_0(n667_0)) → gen_0':s4_0(*(2, n667_0)), rt ∈ Ω(1 + n6670)
sqr(gen_0':s4_0(n967_0)) → gen_0':s4_0(*(n967_0, n967_0)), rt ∈ Ω(1 + n9670 + n96702 + n96703)
half(gen_0':s4_0(*(2, n1380_0))) → gen_0':s4_0(n1380_0), rt ∈ Ω(1 + n13800)
Generator Equations:
gen_0':s4_0(0) ⇔ 0'
gen_0':s4_0(+(x, 1)) ⇔ s(gen_0':s4_0(x))
No more defined symbols left to analyse.
(24) LowerBoundsProof (EQUIVALENT transformation)
The lowerbound Ω(n3) was proven with the following lemma:
sqr(gen_0':s4_0(n967_0)) → gen_0':s4_0(*(n967_0, n967_0)), rt ∈ Ω(1 + n9670 + n96702 + n96703)
(25) BOUNDS(n^3, INF)
(26) Obligation:
Innermost TRS:
Rules:
terms(
N) →
cons(
recip(
sqr(
N)))
sqr(
0') →
0'sqr(
s(
X)) →
s(
add(
sqr(
X),
dbl(
X)))
dbl(
0') →
0'dbl(
s(
X)) →
s(
s(
dbl(
X)))
add(
0',
X) →
Xadd(
s(
X),
Y) →
s(
add(
X,
Y))
first(
0',
X) →
nilfirst(
s(
X),
cons(
Y)) →
cons(
Y)
half(
0') →
0'half(
s(
0')) →
0'half(
s(
s(
X))) →
s(
half(
X))
half(
dbl(
X)) →
XTypes:
terms :: 0':s → cons:nil
cons :: recip → cons:nil
recip :: 0':s → recip
sqr :: 0':s → 0':s
0' :: 0':s
s :: 0':s → 0':s
add :: 0':s → 0':s → 0':s
dbl :: 0':s → 0':s
first :: 0':s → cons:nil → cons:nil
nil :: cons:nil
half :: 0':s → 0':s
hole_cons:nil1_0 :: cons:nil
hole_0':s2_0 :: 0':s
hole_recip3_0 :: recip
gen_0':s4_0 :: Nat → 0':s
Lemmas:
add(gen_0':s4_0(n6_0), gen_0':s4_0(b)) → gen_0':s4_0(+(n6_0, b)), rt ∈ Ω(1 + n60)
dbl(gen_0':s4_0(n667_0)) → gen_0':s4_0(*(2, n667_0)), rt ∈ Ω(1 + n6670)
sqr(gen_0':s4_0(n967_0)) → gen_0':s4_0(*(n967_0, n967_0)), rt ∈ Ω(1 + n9670 + n96702 + n96703)
Generator Equations:
gen_0':s4_0(0) ⇔ 0'
gen_0':s4_0(+(x, 1)) ⇔ s(gen_0':s4_0(x))
No more defined symbols left to analyse.
(27) LowerBoundsProof (EQUIVALENT transformation)
The lowerbound Ω(n3) was proven with the following lemma:
sqr(gen_0':s4_0(n967_0)) → gen_0':s4_0(*(n967_0, n967_0)), rt ∈ Ω(1 + n9670 + n96702 + n96703)
(28) BOUNDS(n^3, INF)
(29) Obligation:
Innermost TRS:
Rules:
terms(
N) →
cons(
recip(
sqr(
N)))
sqr(
0') →
0'sqr(
s(
X)) →
s(
add(
sqr(
X),
dbl(
X)))
dbl(
0') →
0'dbl(
s(
X)) →
s(
s(
dbl(
X)))
add(
0',
X) →
Xadd(
s(
X),
Y) →
s(
add(
X,
Y))
first(
0',
X) →
nilfirst(
s(
X),
cons(
Y)) →
cons(
Y)
half(
0') →
0'half(
s(
0')) →
0'half(
s(
s(
X))) →
s(
half(
X))
half(
dbl(
X)) →
XTypes:
terms :: 0':s → cons:nil
cons :: recip → cons:nil
recip :: 0':s → recip
sqr :: 0':s → 0':s
0' :: 0':s
s :: 0':s → 0':s
add :: 0':s → 0':s → 0':s
dbl :: 0':s → 0':s
first :: 0':s → cons:nil → cons:nil
nil :: cons:nil
half :: 0':s → 0':s
hole_cons:nil1_0 :: cons:nil
hole_0':s2_0 :: 0':s
hole_recip3_0 :: recip
gen_0':s4_0 :: Nat → 0':s
Lemmas:
add(gen_0':s4_0(n6_0), gen_0':s4_0(b)) → gen_0':s4_0(+(n6_0, b)), rt ∈ Ω(1 + n60)
dbl(gen_0':s4_0(n667_0)) → gen_0':s4_0(*(2, n667_0)), rt ∈ Ω(1 + n6670)
Generator Equations:
gen_0':s4_0(0) ⇔ 0'
gen_0':s4_0(+(x, 1)) ⇔ s(gen_0':s4_0(x))
No more defined symbols left to analyse.
(30) LowerBoundsProof (EQUIVALENT transformation)
The lowerbound Ω(n1) was proven with the following lemma:
add(gen_0':s4_0(n6_0), gen_0':s4_0(b)) → gen_0':s4_0(+(n6_0, b)), rt ∈ Ω(1 + n60)
(31) BOUNDS(n^1, INF)
(32) Obligation:
Innermost TRS:
Rules:
terms(
N) →
cons(
recip(
sqr(
N)))
sqr(
0') →
0'sqr(
s(
X)) →
s(
add(
sqr(
X),
dbl(
X)))
dbl(
0') →
0'dbl(
s(
X)) →
s(
s(
dbl(
X)))
add(
0',
X) →
Xadd(
s(
X),
Y) →
s(
add(
X,
Y))
first(
0',
X) →
nilfirst(
s(
X),
cons(
Y)) →
cons(
Y)
half(
0') →
0'half(
s(
0')) →
0'half(
s(
s(
X))) →
s(
half(
X))
half(
dbl(
X)) →
XTypes:
terms :: 0':s → cons:nil
cons :: recip → cons:nil
recip :: 0':s → recip
sqr :: 0':s → 0':s
0' :: 0':s
s :: 0':s → 0':s
add :: 0':s → 0':s → 0':s
dbl :: 0':s → 0':s
first :: 0':s → cons:nil → cons:nil
nil :: cons:nil
half :: 0':s → 0':s
hole_cons:nil1_0 :: cons:nil
hole_0':s2_0 :: 0':s
hole_recip3_0 :: recip
gen_0':s4_0 :: Nat → 0':s
Lemmas:
add(gen_0':s4_0(n6_0), gen_0':s4_0(b)) → gen_0':s4_0(+(n6_0, b)), rt ∈ Ω(1 + n60)
Generator Equations:
gen_0':s4_0(0) ⇔ 0'
gen_0':s4_0(+(x, 1)) ⇔ s(gen_0':s4_0(x))
No more defined symbols left to analyse.
(33) LowerBoundsProof (EQUIVALENT transformation)
The lowerbound Ω(n1) was proven with the following lemma:
add(gen_0':s4_0(n6_0), gen_0':s4_0(b)) → gen_0':s4_0(+(n6_0, b)), rt ∈ Ω(1 + n60)
(34) BOUNDS(n^1, INF)