(0) Obligation:
Runtime Complexity Relative TRS:
The TRS R consists of the following rules:
rewrite(Op(Val(n), y)) → Op(rewrite(y), Val(n))
rewrite(Op(Op(x, y), y')) → rewrite[Let](Op(Op(x, y), y'), Op(x, y), rewrite(x))
rewrite(Val(n)) → Val(n)
second(Op(x, y)) → y
isOp(Val(n)) → False
isOp(Op(x, y)) → True
first(Val(n)) → Val(n)
first(Op(x, y)) → x
assrewrite(exp) → rewrite(exp)
The (relative) TRS S consists of the following rules:
rewrite[Let](exp, Op(x, y), a1) → rewrite[Let][Let](exp, Op(x, y), a1, rewrite(y))
rewrite[Let][Let](Op(x, y), opab, a1, b1) → rewrite[Let][Let][Let](Op(x, y), a1, b1, rewrite(y))
rewrite[Let][Let][Let](exp, a1, b1, c1) → rewrite(Op(a1, Op(b1, rewrite(c1))))
Rewrite Strategy: INNERMOST
(1) RenamingProof (EQUIVALENT transformation)
Renamed function symbols to avoid clashes with predefined symbol.
(2) Obligation:
Runtime Complexity Relative TRS:
The TRS R consists of the following rules:
rewrite(Op(Val(n), y)) → Op(rewrite(y), Val(n))
rewrite(Op(Op(x, y), y')) → rewrite[Let](Op(Op(x, y), y'), Op(x, y), rewrite(x))
rewrite(Val(n)) → Val(n)
second(Op(x, y)) → y
isOp(Val(n)) → False
isOp(Op(x, y)) → True
first(Val(n)) → Val(n)
first(Op(x, y)) → x
assrewrite(exp) → rewrite(exp)
The (relative) TRS S consists of the following rules:
rewrite[Let](exp, Op(x, y), a1) → rewrite[Let][Let](exp, Op(x, y), a1, rewrite(y))
rewrite[Let][Let](Op(x, y), opab, a1, b1) → rewrite[Let][Let][Let](Op(x, y), a1, b1, rewrite(y))
rewrite[Let][Let][Let](exp, a1, b1, c1) → rewrite(Op(a1, Op(b1, rewrite(c1))))
Rewrite Strategy: INNERMOST
(3) SlicingProof (LOWER BOUND(ID) transformation)
Sliced the following arguments:
Val/0
rewrite[Let][Let]/1
rewrite[Let][Let][Let]/0
(4) Obligation:
Runtime Complexity Relative TRS:
The TRS R consists of the following rules:
rewrite(Op(Val, y)) → Op(rewrite(y), Val)
rewrite(Op(Op(x, y), y')) → rewrite[Let](Op(Op(x, y), y'), Op(x, y), rewrite(x))
rewrite(Val) → Val
second(Op(x, y)) → y
isOp(Val) → False
isOp(Op(x, y)) → True
first(Val) → Val
first(Op(x, y)) → x
assrewrite(exp) → rewrite(exp)
The (relative) TRS S consists of the following rules:
rewrite[Let](exp, Op(x, y), a1) → rewrite[Let][Let](exp, a1, rewrite(y))
rewrite[Let][Let](Op(x, y), a1, b1) → rewrite[Let][Let][Let](a1, b1, rewrite(y))
rewrite[Let][Let][Let](a1, b1, c1) → rewrite(Op(a1, Op(b1, rewrite(c1))))
Rewrite Strategy: INNERMOST
(5) TypeInferenceProof (BOTH BOUNDS(ID, ID) transformation)
Infered types.
(6) Obligation:
Innermost TRS:
Rules:
rewrite(Op(Val, y)) → Op(rewrite(y), Val)
rewrite(Op(Op(x, y), y')) → rewrite[Let](Op(Op(x, y), y'), Op(x, y), rewrite(x))
rewrite(Val) → Val
second(Op(x, y)) → y
isOp(Val) → False
isOp(Op(x, y)) → True
first(Val) → Val
first(Op(x, y)) → x
assrewrite(exp) → rewrite(exp)
rewrite[Let](exp, Op(x, y), a1) → rewrite[Let][Let](exp, a1, rewrite(y))
rewrite[Let][Let](Op(x, y), a1, b1) → rewrite[Let][Let][Let](a1, b1, rewrite(y))
rewrite[Let][Let][Let](a1, b1, c1) → rewrite(Op(a1, Op(b1, rewrite(c1))))
Types:
rewrite :: Val:Op → Val:Op
Op :: Val:Op → Val:Op → Val:Op
Val :: Val:Op
rewrite[Let] :: Val:Op → Val:Op → Val:Op → Val:Op
second :: Val:Op → Val:Op
isOp :: Val:Op → False:True
False :: False:True
True :: False:True
first :: Val:Op → Val:Op
assrewrite :: Val:Op → Val:Op
rewrite[Let][Let] :: Val:Op → Val:Op → Val:Op → Val:Op
rewrite[Let][Let][Let] :: Val:Op → Val:Op → Val:Op → Val:Op
hole_Val:Op1_0 :: Val:Op
hole_False:True2_0 :: False:True
gen_Val:Op3_0 :: Nat → Val:Op
(7) OrderProof (LOWER BOUND(ID) transformation)
Heuristically decided to analyse the following defined symbols:
rewrite
(8) Obligation:
Innermost TRS:
Rules:
rewrite(
Op(
Val,
y)) →
Op(
rewrite(
y),
Val)
rewrite(
Op(
Op(
x,
y),
y')) →
rewrite[Let](
Op(
Op(
x,
y),
y'),
Op(
x,
y),
rewrite(
x))
rewrite(
Val) →
Valsecond(
Op(
x,
y)) →
yisOp(
Val) →
FalseisOp(
Op(
x,
y)) →
Truefirst(
Val) →
Valfirst(
Op(
x,
y)) →
xassrewrite(
exp) →
rewrite(
exp)
rewrite[Let](
exp,
Op(
x,
y),
a1) →
rewrite[Let][Let](
exp,
a1,
rewrite(
y))
rewrite[Let][Let](
Op(
x,
y),
a1,
b1) →
rewrite[Let][Let][Let](
a1,
b1,
rewrite(
y))
rewrite[Let][Let][Let](
a1,
b1,
c1) →
rewrite(
Op(
a1,
Op(
b1,
rewrite(
c1))))
Types:
rewrite :: Val:Op → Val:Op
Op :: Val:Op → Val:Op → Val:Op
Val :: Val:Op
rewrite[Let] :: Val:Op → Val:Op → Val:Op → Val:Op
second :: Val:Op → Val:Op
isOp :: Val:Op → False:True
False :: False:True
True :: False:True
first :: Val:Op → Val:Op
assrewrite :: Val:Op → Val:Op
rewrite[Let][Let] :: Val:Op → Val:Op → Val:Op → Val:Op
rewrite[Let][Let][Let] :: Val:Op → Val:Op → Val:Op → Val:Op
hole_Val:Op1_0 :: Val:Op
hole_False:True2_0 :: False:True
gen_Val:Op3_0 :: Nat → Val:Op
Generator Equations:
gen_Val:Op3_0(0) ⇔ Val
gen_Val:Op3_0(+(x, 1)) ⇔ Op(Val, gen_Val:Op3_0(x))
The following defined symbols remain to be analysed:
rewrite
(9) RewriteLemmaProof (LOWER BOUND(ID) transformation)
Proved the following rewrite lemma:
rewrite(
gen_Val:Op3_0(
+(
1,
n5_0))) →
*4_0, rt ∈ Ω(n5
0)
Induction Base:
rewrite(gen_Val:Op3_0(+(1, 0)))
Induction Step:
rewrite(gen_Val:Op3_0(+(1, +(n5_0, 1)))) →RΩ(1)
Op(rewrite(gen_Val:Op3_0(+(1, n5_0))), Val) →IH
Op(*4_0, Val)
We have rt ∈ Ω(n1) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).
(10) Complex Obligation (BEST)
(11) Obligation:
Innermost TRS:
Rules:
rewrite(
Op(
Val,
y)) →
Op(
rewrite(
y),
Val)
rewrite(
Op(
Op(
x,
y),
y')) →
rewrite[Let](
Op(
Op(
x,
y),
y'),
Op(
x,
y),
rewrite(
x))
rewrite(
Val) →
Valsecond(
Op(
x,
y)) →
yisOp(
Val) →
FalseisOp(
Op(
x,
y)) →
Truefirst(
Val) →
Valfirst(
Op(
x,
y)) →
xassrewrite(
exp) →
rewrite(
exp)
rewrite[Let](
exp,
Op(
x,
y),
a1) →
rewrite[Let][Let](
exp,
a1,
rewrite(
y))
rewrite[Let][Let](
Op(
x,
y),
a1,
b1) →
rewrite[Let][Let][Let](
a1,
b1,
rewrite(
y))
rewrite[Let][Let][Let](
a1,
b1,
c1) →
rewrite(
Op(
a1,
Op(
b1,
rewrite(
c1))))
Types:
rewrite :: Val:Op → Val:Op
Op :: Val:Op → Val:Op → Val:Op
Val :: Val:Op
rewrite[Let] :: Val:Op → Val:Op → Val:Op → Val:Op
second :: Val:Op → Val:Op
isOp :: Val:Op → False:True
False :: False:True
True :: False:True
first :: Val:Op → Val:Op
assrewrite :: Val:Op → Val:Op
rewrite[Let][Let] :: Val:Op → Val:Op → Val:Op → Val:Op
rewrite[Let][Let][Let] :: Val:Op → Val:Op → Val:Op → Val:Op
hole_Val:Op1_0 :: Val:Op
hole_False:True2_0 :: False:True
gen_Val:Op3_0 :: Nat → Val:Op
Lemmas:
rewrite(gen_Val:Op3_0(+(1, n5_0))) → *4_0, rt ∈ Ω(n50)
Generator Equations:
gen_Val:Op3_0(0) ⇔ Val
gen_Val:Op3_0(+(x, 1)) ⇔ Op(Val, gen_Val:Op3_0(x))
No more defined symbols left to analyse.
(12) LowerBoundsProof (EQUIVALENT transformation)
The lowerbound Ω(n1) was proven with the following lemma:
rewrite(gen_Val:Op3_0(+(1, n5_0))) → *4_0, rt ∈ Ω(n50)
(13) BOUNDS(n^1, INF)
(14) Obligation:
Innermost TRS:
Rules:
rewrite(
Op(
Val,
y)) →
Op(
rewrite(
y),
Val)
rewrite(
Op(
Op(
x,
y),
y')) →
rewrite[Let](
Op(
Op(
x,
y),
y'),
Op(
x,
y),
rewrite(
x))
rewrite(
Val) →
Valsecond(
Op(
x,
y)) →
yisOp(
Val) →
FalseisOp(
Op(
x,
y)) →
Truefirst(
Val) →
Valfirst(
Op(
x,
y)) →
xassrewrite(
exp) →
rewrite(
exp)
rewrite[Let](
exp,
Op(
x,
y),
a1) →
rewrite[Let][Let](
exp,
a1,
rewrite(
y))
rewrite[Let][Let](
Op(
x,
y),
a1,
b1) →
rewrite[Let][Let][Let](
a1,
b1,
rewrite(
y))
rewrite[Let][Let][Let](
a1,
b1,
c1) →
rewrite(
Op(
a1,
Op(
b1,
rewrite(
c1))))
Types:
rewrite :: Val:Op → Val:Op
Op :: Val:Op → Val:Op → Val:Op
Val :: Val:Op
rewrite[Let] :: Val:Op → Val:Op → Val:Op → Val:Op
second :: Val:Op → Val:Op
isOp :: Val:Op → False:True
False :: False:True
True :: False:True
first :: Val:Op → Val:Op
assrewrite :: Val:Op → Val:Op
rewrite[Let][Let] :: Val:Op → Val:Op → Val:Op → Val:Op
rewrite[Let][Let][Let] :: Val:Op → Val:Op → Val:Op → Val:Op
hole_Val:Op1_0 :: Val:Op
hole_False:True2_0 :: False:True
gen_Val:Op3_0 :: Nat → Val:Op
Lemmas:
rewrite(gen_Val:Op3_0(+(1, n5_0))) → *4_0, rt ∈ Ω(n50)
Generator Equations:
gen_Val:Op3_0(0) ⇔ Val
gen_Val:Op3_0(+(x, 1)) ⇔ Op(Val, gen_Val:Op3_0(x))
No more defined symbols left to analyse.
(15) LowerBoundsProof (EQUIVALENT transformation)
The lowerbound Ω(n1) was proven with the following lemma:
rewrite(gen_Val:Op3_0(+(1, n5_0))) → *4_0, rt ∈ Ω(n50)
(16) BOUNDS(n^1, INF)