cd /tools/ && ls
ceta minismt pwhile tct-its tct-trs z3-z3-4.8.4 gubs paicc share tct-jbc yices-2.6.1
Central to automating the analysis is a simple yet powerful framework for complexity.
In the following let $P_i$ denote a complexity problem and $f_i$ denote a bounding function. The precise notion of $P$ and $f$ depends on the analysis and is kept abstract within the framework. The complexity judgement $\;\vdash P \colon f$ indicates that problem $P$ is bounded by function $f$.
Example: Consider the judgement $\vdash \langle \mathtt{insertionSort}(es), \#\text{comparison wrt. } n = len(es) \rangle \colon \mathcal{O}(n^2)$. Here, the complexity problem $P$ is a sorting program associated with the resource of interest and the bounding function $f$ is expressed in big-$\mathcal{O}$ notation.
The heart of the complexity framework is the inference rule
$$\frac{Pre(P) \quad \vdash P_1 \colon f_1 \cdots \vdash P_n \colon f_n}{\vdash P \colon f}\;,$$which is sound if under precondition $Pre(P)$ the validity of judgements is preserved, that is,
$$Pre(P) \wedge \vdash P_1 \colon f_1 \wedge \cdots \wedge P_n \colon f_n \Rightarrow P \colon f\;.$$Using this inference rule we can express and combine a variety of problem transformations that origin from compiler design, program analysis, termination and resource analysis, etc. For instance,
The inference rules provides us a formal notion of complexity proofs. To facilitate the proof search we provide a strategy combinator language. Most prominent are the following combinators:
s1 >>> s2 (sequential composition)
s1 <|> s2 (alternative)
try s (trackbacking)
Example: An illustrating pattern for a strategy is:
inferInvariants >>> simplify >>> try decompose >>> (linearBound <|> quadraticBound <|> cubicBound)
Morally, at first we infer additional informations that support the rest of the analysis. Then, we apply simplifications to reduce the complexity of subsequent problem transformations. Afterwards, we try to decompose the problem into smaller subproblems. Finally, we apply dedicated techniques for the inference of linear, qudratic and cubic bounding functions.
ls /tools/tct-trs
CHANGELOG ISSUES.md README.md src stack.yaml.lock tct-trs.cabal examples LICENSE Setup.hs stack.yaml tct-trs
Term Rewriting is a declarative computation module. A Term rewrite System $\mathcal{R}$ is a set of directed equations.
cat /tools/share/bfs.trs
(VAR x xs y ys t t1 t2 ts)
(RULES
appendreverse(::(x,xs), ys) -> appendreverse(xs,::(x,ys))
appendreverse(nil, ys) -> ys
reverse(xs) -> appendreverse(xs, nil)
eq(s(x), s(y)) ->= eq(x, y)
eq(0, 0) ->= #true
eq(x,y) ->= #false
bfs(xs, ys, x) -> bfs#1(xs,ys,x)
bfs#1(nil, ys, x) -> bfs#2(ys, x)
bfs#1(::(t,ts), ys, x) -> bfs#3(t, ys, ts, x)
bfs#2(::(t,ts), x) -> bfs(reverse(::(t, ts)), nil, x)
bfs#2(nil , x) -> leaf
bfs#3(leaf, ys, ts, x) -> bfs(ts, ys, x)
bfs#3(node(y,t1,t2), ys, ts, x) -> bfs#4(eq(x,y), ys, t1, t2, ts, x, y)
bfs#4(#true, ys, t1, t2, ts, x, y) -> node(y, t1, t2)
bfs#4(#false, ys, t1, t2, ts, x, y) -> bfs(ts, ::(t2,::(t1,ys)),x)
dobfs(t, x) -> bfs(::(t,nil), nil, x)
main(t,x) -> dobfs(t, x)
)
(COMMENT
main(t, x) = dobfs(t, x)
dobfs(t, x) = bfs([t],[],x)
bfs(xs, ys, x) = match xs with
| [] -> match ys with
| [] -> leaf
| (t::ts) -> bfs(reverse(t::ts), [], x)
| (t::ts) -> match t with
| leaf -> bfs(ts, ys, x)
| node(y, t1, t2) -> if x == y then node (y, t1, t2) else bfs(ts, t2 :: t1 :: ys, x)
)
tct-trs --complexity rci --strategy "dependencyPairs :kind WIDP >>> try dpsimps >>> matrices :from 0 :to 2" /tools/share/bfs.trs
WORST_CASE(?,O(n^2))
* Step 1: DependencyPairs WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict TRS:
appendreverse(::(x,xs),ys) -> appendreverse(xs,::(x,ys))
appendreverse(nil(),ys) -> ys
bfs(xs,ys,x) -> bfs#1(xs,ys,x)
bfs#1(::(t,ts),ys,x) -> bfs#3(t,ys,ts,x)
bfs#1(nil(),ys,x) -> bfs#2(ys,x)
bfs#2(::(t,ts),x) -> bfs(reverse(::(t,ts)),nil(),x)
bfs#2(nil(),x) -> leaf()
bfs#3(leaf(),ys,ts,x) -> bfs(ts,ys,x)
bfs#3(node(y,t1,t2),ys,ts,x) -> bfs#4(eq(x,y),ys,t1,t2,ts,x,y)
bfs#4(#false(),ys,t1,t2,ts,x,y) -> bfs(ts,::(t2,::(t1,ys)),x)
bfs#4(#true(),ys,t1,t2,ts,x,y) -> node(y,t1,t2)
dobfs(t,x) -> bfs(::(t,nil()),nil(),x)
main(t,x) -> dobfs(t,x)
reverse(xs) -> appendreverse(xs,nil())
- Weak TRS:
eq(x,y) -> #false()
eq(0(),0()) -> #true()
eq(s(x),s(y)) -> eq(x,y)
- Signature:
{appendreverse/2,bfs/3,bfs#1/3,bfs#2/2,bfs#3/4,bfs#4/7,dobfs/2,eq/2,main/2,reverse/1} / {#false/0,#true/0
,0/0,::/2,leaf/0,nil/0,node/3,s/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {appendreverse,bfs,bfs#1,bfs#2,bfs#3,bfs#4,dobfs,eq,main
,reverse} and constructors {#false,#true,0,::,leaf,nil,node,s}
+ Applied Processor:
DependencyPairs {dpKind_ = WIDP}
+ Details:
We add the following weak innermost dependency pairs:
Strict DPs
appendreverse#(::(x,xs),ys) -> c_1(appendreverse#(xs,::(x,ys)))
appendreverse#(nil(),ys) -> c_2()
bfs#(xs,ys,x) -> c_3(bfs#1#(xs,ys,x))
bfs#1#(::(t,ts),ys,x) -> c_4(bfs#3#(t,ys,ts,x))
bfs#1#(nil(),ys,x) -> c_5(bfs#2#(ys,x))
bfs#2#(::(t,ts),x) -> c_6(bfs#(reverse(::(t,ts)),nil(),x))
bfs#2#(nil(),x) -> c_7()
bfs#3#(leaf(),ys,ts,x) -> c_8(bfs#(ts,ys,x))
bfs#3#(node(y,t1,t2),ys,ts,x) -> c_9(bfs#4#(eq(x,y),ys,t1,t2,ts,x,y))
bfs#4#(#false(),ys,t1,t2,ts,x,y) -> c_10(bfs#(ts,::(t2,::(t1,ys)),x))
bfs#4#(#true(),ys,t1,t2,ts,x,y) -> c_11()
dobfs#(t,x) -> c_12(bfs#(::(t,nil()),nil(),x))
main#(t,x) -> c_13(dobfs#(t,x))
reverse#(xs) -> c_14(appendreverse#(xs,nil()))
Weak DPs
eq#(x,y) -> c_15()
eq#(0(),0()) -> c_16()
eq#(s(x),s(y)) -> c_17(eq#(x,y))
and mark the set of starting terms.
* Step 2: PredecessorEstimation WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict DPs:
appendreverse#(::(x,xs),ys) -> c_1(appendreverse#(xs,::(x,ys)))
appendreverse#(nil(),ys) -> c_2()
bfs#(xs,ys,x) -> c_3(bfs#1#(xs,ys,x))
bfs#1#(::(t,ts),ys,x) -> c_4(bfs#3#(t,ys,ts,x))
bfs#1#(nil(),ys,x) -> c_5(bfs#2#(ys,x))
bfs#2#(::(t,ts),x) -> c_6(bfs#(reverse(::(t,ts)),nil(),x))
bfs#2#(nil(),x) -> c_7()
bfs#3#(leaf(),ys,ts,x) -> c_8(bfs#(ts,ys,x))
bfs#3#(node(y,t1,t2),ys,ts,x) -> c_9(bfs#4#(eq(x,y),ys,t1,t2,ts,x,y))
bfs#4#(#false(),ys,t1,t2,ts,x,y) -> c_10(bfs#(ts,::(t2,::(t1,ys)),x))
bfs#4#(#true(),ys,t1,t2,ts,x,y) -> c_11()
dobfs#(t,x) -> c_12(bfs#(::(t,nil()),nil(),x))
main#(t,x) -> c_13(dobfs#(t,x))
reverse#(xs) -> c_14(appendreverse#(xs,nil()))
- Strict TRS:
appendreverse(::(x,xs),ys) -> appendreverse(xs,::(x,ys))
appendreverse(nil(),ys) -> ys
bfs(xs,ys,x) -> bfs#1(xs,ys,x)
bfs#1(::(t,ts),ys,x) -> bfs#3(t,ys,ts,x)
bfs#1(nil(),ys,x) -> bfs#2(ys,x)
bfs#2(::(t,ts),x) -> bfs(reverse(::(t,ts)),nil(),x)
bfs#2(nil(),x) -> leaf()
bfs#3(leaf(),ys,ts,x) -> bfs(ts,ys,x)
bfs#3(node(y,t1,t2),ys,ts,x) -> bfs#4(eq(x,y),ys,t1,t2,ts,x,y)
bfs#4(#false(),ys,t1,t2,ts,x,y) -> bfs(ts,::(t2,::(t1,ys)),x)
bfs#4(#true(),ys,t1,t2,ts,x,y) -> node(y,t1,t2)
dobfs(t,x) -> bfs(::(t,nil()),nil(),x)
main(t,x) -> dobfs(t,x)
reverse(xs) -> appendreverse(xs,nil())
- Weak DPs:
eq#(x,y) -> c_15()
eq#(0(),0()) -> c_16()
eq#(s(x),s(y)) -> c_17(eq#(x,y))
- Weak TRS:
eq(x,y) -> #false()
eq(0(),0()) -> #true()
eq(s(x),s(y)) -> eq(x,y)
- Signature:
{appendreverse/2,bfs/3,bfs#1/3,bfs#2/2,bfs#3/4,bfs#4/7,dobfs/2,eq/2,main/2,reverse/1,appendreverse#/2,bfs#/3
,bfs#1#/3,bfs#2#/2,bfs#3#/4,bfs#4#/7,dobfs#/2,eq#/2,main#/2,reverse#/1} / {#false/0,#true/0,0/0,::/2,leaf/0
,nil/0,node/3,s/1,c_1/1,c_2/0,c_3/1,c_4/1,c_5/1,c_6/1,c_7/0,c_8/1,c_9/1,c_10/1,c_11/0,c_12/1,c_13/1,c_14/1
,c_15/0,c_16/0,c_17/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {appendreverse#,bfs#,bfs#1#,bfs#2#,bfs#3#,bfs#4#,dobfs#
,eq#,main#,reverse#} and constructors {#false,#true,0,::,leaf,nil,node,s}
+ Applied Processor:
PredecessorEstimation {onSelection = all simple predecessor estimation selector}
+ Details:
We estimate the number of application of
{2,7,11}
by application of
Pre({2,7,11}) = {1,5,9,14}.
Here rules are labelled as follows:
1: appendreverse#(::(x,xs),ys) -> c_1(appendreverse#(xs,::(x,ys)))
2: appendreverse#(nil(),ys) -> c_2()
3: bfs#(xs,ys,x) -> c_3(bfs#1#(xs,ys,x))
4: bfs#1#(::(t,ts),ys,x) -> c_4(bfs#3#(t,ys,ts,x))
5: bfs#1#(nil(),ys,x) -> c_5(bfs#2#(ys,x))
6: bfs#2#(::(t,ts),x) -> c_6(bfs#(reverse(::(t,ts)),nil(),x))
7: bfs#2#(nil(),x) -> c_7()
8: bfs#3#(leaf(),ys,ts,x) -> c_8(bfs#(ts,ys,x))
9: bfs#3#(node(y,t1,t2),ys,ts,x) -> c_9(bfs#4#(eq(x,y),ys,t1,t2,ts,x,y))
10: bfs#4#(#false(),ys,t1,t2,ts,x,y) -> c_10(bfs#(ts,::(t2,::(t1,ys)),x))
11: bfs#4#(#true(),ys,t1,t2,ts,x,y) -> c_11()
12: dobfs#(t,x) -> c_12(bfs#(::(t,nil()),nil(),x))
13: main#(t,x) -> c_13(dobfs#(t,x))
14: reverse#(xs) -> c_14(appendreverse#(xs,nil()))
15: eq#(x,y) -> c_15()
16: eq#(0(),0()) -> c_16()
17: eq#(s(x),s(y)) -> c_17(eq#(x,y))
* Step 3: UsableRules WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict DPs:
appendreverse#(::(x,xs),ys) -> c_1(appendreverse#(xs,::(x,ys)))
bfs#(xs,ys,x) -> c_3(bfs#1#(xs,ys,x))
bfs#1#(::(t,ts),ys,x) -> c_4(bfs#3#(t,ys,ts,x))
bfs#1#(nil(),ys,x) -> c_5(bfs#2#(ys,x))
bfs#2#(::(t,ts),x) -> c_6(bfs#(reverse(::(t,ts)),nil(),x))
bfs#3#(leaf(),ys,ts,x) -> c_8(bfs#(ts,ys,x))
bfs#3#(node(y,t1,t2),ys,ts,x) -> c_9(bfs#4#(eq(x,y),ys,t1,t2,ts,x,y))
bfs#4#(#false(),ys,t1,t2,ts,x,y) -> c_10(bfs#(ts,::(t2,::(t1,ys)),x))
dobfs#(t,x) -> c_12(bfs#(::(t,nil()),nil(),x))
main#(t,x) -> c_13(dobfs#(t,x))
reverse#(xs) -> c_14(appendreverse#(xs,nil()))
- Strict TRS:
appendreverse(::(x,xs),ys) -> appendreverse(xs,::(x,ys))
appendreverse(nil(),ys) -> ys
bfs(xs,ys,x) -> bfs#1(xs,ys,x)
bfs#1(::(t,ts),ys,x) -> bfs#3(t,ys,ts,x)
bfs#1(nil(),ys,x) -> bfs#2(ys,x)
bfs#2(::(t,ts),x) -> bfs(reverse(::(t,ts)),nil(),x)
bfs#2(nil(),x) -> leaf()
bfs#3(leaf(),ys,ts,x) -> bfs(ts,ys,x)
bfs#3(node(y,t1,t2),ys,ts,x) -> bfs#4(eq(x,y),ys,t1,t2,ts,x,y)
bfs#4(#false(),ys,t1,t2,ts,x,y) -> bfs(ts,::(t2,::(t1,ys)),x)
bfs#4(#true(),ys,t1,t2,ts,x,y) -> node(y,t1,t2)
dobfs(t,x) -> bfs(::(t,nil()),nil(),x)
main(t,x) -> dobfs(t,x)
reverse(xs) -> appendreverse(xs,nil())
- Weak DPs:
appendreverse#(nil(),ys) -> c_2()
bfs#2#(nil(),x) -> c_7()
bfs#4#(#true(),ys,t1,t2,ts,x,y) -> c_11()
eq#(x,y) -> c_15()
eq#(0(),0()) -> c_16()
eq#(s(x),s(y)) -> c_17(eq#(x,y))
- Weak TRS:
eq(x,y) -> #false()
eq(0(),0()) -> #true()
eq(s(x),s(y)) -> eq(x,y)
- Signature:
{appendreverse/2,bfs/3,bfs#1/3,bfs#2/2,bfs#3/4,bfs#4/7,dobfs/2,eq/2,main/2,reverse/1,appendreverse#/2,bfs#/3
,bfs#1#/3,bfs#2#/2,bfs#3#/4,bfs#4#/7,dobfs#/2,eq#/2,main#/2,reverse#/1} / {#false/0,#true/0,0/0,::/2,leaf/0
,nil/0,node/3,s/1,c_1/1,c_2/0,c_3/1,c_4/1,c_5/1,c_6/1,c_7/0,c_8/1,c_9/1,c_10/1,c_11/0,c_12/1,c_13/1,c_14/1
,c_15/0,c_16/0,c_17/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {appendreverse#,bfs#,bfs#1#,bfs#2#,bfs#3#,bfs#4#,dobfs#
,eq#,main#,reverse#} and constructors {#false,#true,0,::,leaf,nil,node,s}
+ Applied Processor:
UsableRules
+ Details:
We replace rewrite rules by usable rules:
appendreverse(::(x,xs),ys) -> appendreverse(xs,::(x,ys))
appendreverse(nil(),ys) -> ys
eq(x,y) -> #false()
eq(0(),0()) -> #true()
eq(s(x),s(y)) -> eq(x,y)
reverse(xs) -> appendreverse(xs,nil())
appendreverse#(::(x,xs),ys) -> c_1(appendreverse#(xs,::(x,ys)))
appendreverse#(nil(),ys) -> c_2()
bfs#(xs,ys,x) -> c_3(bfs#1#(xs,ys,x))
bfs#1#(::(t,ts),ys,x) -> c_4(bfs#3#(t,ys,ts,x))
bfs#1#(nil(),ys,x) -> c_5(bfs#2#(ys,x))
bfs#2#(::(t,ts),x) -> c_6(bfs#(reverse(::(t,ts)),nil(),x))
bfs#2#(nil(),x) -> c_7()
bfs#3#(leaf(),ys,ts,x) -> c_8(bfs#(ts,ys,x))
bfs#3#(node(y,t1,t2),ys,ts,x) -> c_9(bfs#4#(eq(x,y),ys,t1,t2,ts,x,y))
bfs#4#(#false(),ys,t1,t2,ts,x,y) -> c_10(bfs#(ts,::(t2,::(t1,ys)),x))
bfs#4#(#true(),ys,t1,t2,ts,x,y) -> c_11()
dobfs#(t,x) -> c_12(bfs#(::(t,nil()),nil(),x))
eq#(x,y) -> c_15()
eq#(0(),0()) -> c_16()
eq#(s(x),s(y)) -> c_17(eq#(x,y))
main#(t,x) -> c_13(dobfs#(t,x))
reverse#(xs) -> c_14(appendreverse#(xs,nil()))
* Step 4: WeightGap WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict DPs:
appendreverse#(::(x,xs),ys) -> c_1(appendreverse#(xs,::(x,ys)))
bfs#(xs,ys,x) -> c_3(bfs#1#(xs,ys,x))
bfs#1#(::(t,ts),ys,x) -> c_4(bfs#3#(t,ys,ts,x))
bfs#1#(nil(),ys,x) -> c_5(bfs#2#(ys,x))
bfs#2#(::(t,ts),x) -> c_6(bfs#(reverse(::(t,ts)),nil(),x))
bfs#3#(leaf(),ys,ts,x) -> c_8(bfs#(ts,ys,x))
bfs#3#(node(y,t1,t2),ys,ts,x) -> c_9(bfs#4#(eq(x,y),ys,t1,t2,ts,x,y))
bfs#4#(#false(),ys,t1,t2,ts,x,y) -> c_10(bfs#(ts,::(t2,::(t1,ys)),x))
dobfs#(t,x) -> c_12(bfs#(::(t,nil()),nil(),x))
main#(t,x) -> c_13(dobfs#(t,x))
reverse#(xs) -> c_14(appendreverse#(xs,nil()))
- Strict TRS:
appendreverse(::(x,xs),ys) -> appendreverse(xs,::(x,ys))
appendreverse(nil(),ys) -> ys
reverse(xs) -> appendreverse(xs,nil())
- Weak DPs:
appendreverse#(nil(),ys) -> c_2()
bfs#2#(nil(),x) -> c_7()
bfs#4#(#true(),ys,t1,t2,ts,x,y) -> c_11()
eq#(x,y) -> c_15()
eq#(0(),0()) -> c_16()
eq#(s(x),s(y)) -> c_17(eq#(x,y))
- Weak TRS:
eq(x,y) -> #false()
eq(0(),0()) -> #true()
eq(s(x),s(y)) -> eq(x,y)
- Signature:
{appendreverse/2,bfs/3,bfs#1/3,bfs#2/2,bfs#3/4,bfs#4/7,dobfs/2,eq/2,main/2,reverse/1,appendreverse#/2,bfs#/3
,bfs#1#/3,bfs#2#/2,bfs#3#/4,bfs#4#/7,dobfs#/2,eq#/2,main#/2,reverse#/1} / {#false/0,#true/0,0/0,::/2,leaf/0
,nil/0,node/3,s/1,c_1/1,c_2/0,c_3/1,c_4/1,c_5/1,c_6/1,c_7/0,c_8/1,c_9/1,c_10/1,c_11/0,c_12/1,c_13/1,c_14/1
,c_15/0,c_16/0,c_17/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {appendreverse#,bfs#,bfs#1#,bfs#2#,bfs#3#,bfs#4#,dobfs#
,eq#,main#,reverse#} and constructors {#false,#true,0,::,leaf,nil,node,s}
+ Applied Processor:
WeightGap {wgDimension = 1, wgDegree = 0, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny}
+ Details:
The weightgap principle applies using the following nonconstant growth matrix-interpretation:
We apply a matrix interpretation of kind constructor based matrix interpretation:
The following argument positions are considered usable:
uargs(bfs#) = {1},
uargs(bfs#4#) = {1},
uargs(c_1) = {1},
uargs(c_3) = {1},
uargs(c_4) = {1},
uargs(c_5) = {1},
uargs(c_6) = {1},
uargs(c_8) = {1},
uargs(c_9) = {1},
uargs(c_10) = {1},
uargs(c_12) = {1},
uargs(c_13) = {1},
uargs(c_14) = {1},
uargs(c_17) = {1}
Following symbols are considered usable:
all
TcT has computed the following interpretation:
p(#false) = [0]
p(#true) = [0]
p(0) = [2]
p(::) = [1] x2 + [5]
p(appendreverse) = [2] x2 + [0]
p(bfs) = [0]
p(bfs#1) = [0]
p(bfs#2) = [0]
p(bfs#3) = [0]
p(bfs#4) = [0]
p(dobfs) = [0]
p(eq) = [4]
p(leaf) = [0]
p(main) = [0]
p(nil) = [0]
p(node) = [1] x1 + [0]
p(reverse) = [3]
p(s) = [1] x1 + [0]
p(appendreverse#) = [2] x1 + [1] x2 + [5]
p(bfs#) = [1] x1 + [5]
p(bfs#1#) = [1] x1 + [0]
p(bfs#2#) = [0]
p(bfs#3#) = [1] x3 + [0]
p(bfs#4#) = [1] x1 + [1] x5 + [0]
p(dobfs#) = [0]
p(eq#) = [1] x1 + [2] x2 + [4]
p(main#) = [0]
p(reverse#) = [2] x1 + [2]
p(c_1) = [1] x1 + [2]
p(c_2) = [5]
p(c_3) = [1] x1 + [0]
p(c_4) = [1] x1 + [0]
p(c_5) = [1] x1 + [0]
p(c_6) = [1] x1 + [0]
p(c_7) = [0]
p(c_8) = [1] x1 + [0]
p(c_9) = [1] x1 + [0]
p(c_10) = [1] x1 + [0]
p(c_11) = [0]
p(c_12) = [1] x1 + [3]
p(c_13) = [1] x1 + [0]
p(c_14) = [1] x1 + [0]
p(c_15) = [4]
p(c_16) = [1]
p(c_17) = [1] x1 + [0]
Following rules are strictly oriented:
appendreverse#(::(x,xs),ys) = [2] xs + [1] ys + [15]
> [2] xs + [1] ys + [12]
= c_1(appendreverse#(xs,::(x,ys)))
bfs#(xs,ys,x) = [1] xs + [5]
> [1] xs + [0]
= c_3(bfs#1#(xs,ys,x))
bfs#1#(::(t,ts),ys,x) = [1] ts + [5]
> [1] ts + [0]
= c_4(bfs#3#(t,ys,ts,x))
reverse(xs) = [3]
> [0]
= appendreverse(xs,nil())
Following rules are (at-least) weakly oriented:
appendreverse#(nil(),ys) = [1] ys + [5]
>= [5]
= c_2()
bfs#1#(nil(),ys,x) = [0]
>= [0]
= c_5(bfs#2#(ys,x))
bfs#2#(::(t,ts),x) = [0]
>= [8]
= c_6(bfs#(reverse(::(t,ts)),nil(),x))
bfs#2#(nil(),x) = [0]
>= [0]
= c_7()
bfs#3#(leaf(),ys,ts,x) = [1] ts + [0]
>= [1] ts + [5]
= c_8(bfs#(ts,ys,x))
bfs#3#(node(y,t1,t2),ys,ts,x) = [1] ts + [0]
>= [1] ts + [4]
= c_9(bfs#4#(eq(x,y),ys,t1,t2,ts,x,y))
bfs#4#(#false(),ys,t1,t2,ts,x,y) = [1] ts + [0]
>= [1] ts + [5]
= c_10(bfs#(ts,::(t2,::(t1,ys)),x))
bfs#4#(#true(),ys,t1,t2,ts,x,y) = [1] ts + [0]
>= [0]
= c_11()
dobfs#(t,x) = [0]
>= [13]
= c_12(bfs#(::(t,nil()),nil(),x))
eq#(x,y) = [1] x + [2] y + [4]
>= [4]
= c_15()
eq#(0(),0()) = [10]
>= [1]
= c_16()
eq#(s(x),s(y)) = [1] x + [2] y + [4]
>= [1] x + [2] y + [4]
= c_17(eq#(x,y))
main#(t,x) = [0]
>= [0]
= c_13(dobfs#(t,x))
reverse#(xs) = [2] xs + [2]
>= [2] xs + [5]
= c_14(appendreverse#(xs,nil()))
appendreverse(::(x,xs),ys) = [2] ys + [0]
>= [2] ys + [10]
= appendreverse(xs,::(x,ys))
appendreverse(nil(),ys) = [2] ys + [0]
>= [1] ys + [0]
= ys
eq(x,y) = [4]
>= [0]
= #false()
eq(0(),0()) = [4]
>= [0]
= #true()
eq(s(x),s(y)) = [4]
>= [4]
= eq(x,y)
Further, it can be verified that all rules not oriented are covered by the weightgap condition.
* Step 5: WeightGap WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict DPs:
bfs#1#(nil(),ys,x) -> c_5(bfs#2#(ys,x))
bfs#2#(::(t,ts),x) -> c_6(bfs#(reverse(::(t,ts)),nil(),x))
bfs#3#(leaf(),ys,ts,x) -> c_8(bfs#(ts,ys,x))
bfs#3#(node(y,t1,t2),ys,ts,x) -> c_9(bfs#4#(eq(x,y),ys,t1,t2,ts,x,y))
bfs#4#(#false(),ys,t1,t2,ts,x,y) -> c_10(bfs#(ts,::(t2,::(t1,ys)),x))
dobfs#(t,x) -> c_12(bfs#(::(t,nil()),nil(),x))
main#(t,x) -> c_13(dobfs#(t,x))
reverse#(xs) -> c_14(appendreverse#(xs,nil()))
- Strict TRS:
appendreverse(::(x,xs),ys) -> appendreverse(xs,::(x,ys))
appendreverse(nil(),ys) -> ys
- Weak DPs:
appendreverse#(::(x,xs),ys) -> c_1(appendreverse#(xs,::(x,ys)))
appendreverse#(nil(),ys) -> c_2()
bfs#(xs,ys,x) -> c_3(bfs#1#(xs,ys,x))
bfs#1#(::(t,ts),ys,x) -> c_4(bfs#3#(t,ys,ts,x))
bfs#2#(nil(),x) -> c_7()
bfs#4#(#true(),ys,t1,t2,ts,x,y) -> c_11()
eq#(x,y) -> c_15()
eq#(0(),0()) -> c_16()
eq#(s(x),s(y)) -> c_17(eq#(x,y))
- Weak TRS:
eq(x,y) -> #false()
eq(0(),0()) -> #true()
eq(s(x),s(y)) -> eq(x,y)
reverse(xs) -> appendreverse(xs,nil())
- Signature:
{appendreverse/2,bfs/3,bfs#1/3,bfs#2/2,bfs#3/4,bfs#4/7,dobfs/2,eq/2,main/2,reverse/1,appendreverse#/2,bfs#/3
,bfs#1#/3,bfs#2#/2,bfs#3#/4,bfs#4#/7,dobfs#/2,eq#/2,main#/2,reverse#/1} / {#false/0,#true/0,0/0,::/2,leaf/0
,nil/0,node/3,s/1,c_1/1,c_2/0,c_3/1,c_4/1,c_5/1,c_6/1,c_7/0,c_8/1,c_9/1,c_10/1,c_11/0,c_12/1,c_13/1,c_14/1
,c_15/0,c_16/0,c_17/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {appendreverse#,bfs#,bfs#1#,bfs#2#,bfs#3#,bfs#4#,dobfs#
,eq#,main#,reverse#} and constructors {#false,#true,0,::,leaf,nil,node,s}
+ Applied Processor:
WeightGap {wgDimension = 1, wgDegree = 0, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny}
+ Details:
The weightgap principle applies using the following nonconstant growth matrix-interpretation:
We apply a matrix interpretation of kind constructor based matrix interpretation:
The following argument positions are considered usable:
uargs(bfs#) = {1},
uargs(bfs#4#) = {1},
uargs(c_1) = {1},
uargs(c_3) = {1},
uargs(c_4) = {1},
uargs(c_5) = {1},
uargs(c_6) = {1},
uargs(c_8) = {1},
uargs(c_9) = {1},
uargs(c_10) = {1},
uargs(c_12) = {1},
uargs(c_13) = {1},
uargs(c_14) = {1},
uargs(c_17) = {1}
Following symbols are considered usable:
all
TcT has computed the following interpretation:
p(#false) = [0]
p(#true) = [0]
p(0) = [2]
p(::) = [1] x2 + [0]
p(appendreverse) = [4] x2 + [0]
p(bfs) = [0]
p(bfs#1) = [0]
p(bfs#2) = [0]
p(bfs#3) = [0]
p(bfs#4) = [0]
p(dobfs) = [0]
p(eq) = [0]
p(leaf) = [0]
p(main) = [0]
p(nil) = [0]
p(node) = [1] x3 + [0]
p(reverse) = [0]
p(s) = [1] x1 + [0]
p(appendreverse#) = [1] x2 + [3]
p(bfs#) = [1] x1 + [0]
p(bfs#1#) = [1] x1 + [0]
p(bfs#2#) = [3]
p(bfs#3#) = [1] x3 + [0]
p(bfs#4#) = [1] x1 + [1] x5 + [5]
p(dobfs#) = [1] x1 + [4] x2 + [0]
p(eq#) = [4] x1 + [1] x2 + [4]
p(main#) = [1] x1 + [4] x2 + [4]
p(reverse#) = [2]
p(c_1) = [1] x1 + [0]
p(c_2) = [3]
p(c_3) = [1] x1 + [0]
p(c_4) = [1] x1 + [0]
p(c_5) = [1] x1 + [1]
p(c_6) = [1] x1 + [0]
p(c_7) = [2]
p(c_8) = [1] x1 + [3]
p(c_9) = [1] x1 + [0]
p(c_10) = [1] x1 + [0]
p(c_11) = [5]
p(c_12) = [1] x1 + [0]
p(c_13) = [1] x1 + [0]
p(c_14) = [1] x1 + [0]
p(c_15) = [0]
p(c_16) = [0]
p(c_17) = [1] x1 + [0]
Following rules are strictly oriented:
bfs#2#(::(t,ts),x) = [3]
> [0]
= c_6(bfs#(reverse(::(t,ts)),nil(),x))
bfs#4#(#false(),ys,t1,t2,ts,x,y) = [1] ts + [5]
> [1] ts + [0]
= c_10(bfs#(ts,::(t2,::(t1,ys)),x))
main#(t,x) = [1] t + [4] x + [4]
> [1] t + [4] x + [0]
= c_13(dobfs#(t,x))
Following rules are (at-least) weakly oriented:
appendreverse#(::(x,xs),ys) = [1] ys + [3]
>= [1] ys + [3]
= c_1(appendreverse#(xs,::(x,ys)))
appendreverse#(nil(),ys) = [1] ys + [3]
>= [3]
= c_2()
bfs#(xs,ys,x) = [1] xs + [0]
>= [1] xs + [0]
= c_3(bfs#1#(xs,ys,x))
bfs#1#(::(t,ts),ys,x) = [1] ts + [0]
>= [1] ts + [0]
= c_4(bfs#3#(t,ys,ts,x))
bfs#1#(nil(),ys,x) = [0]
>= [4]
= c_5(bfs#2#(ys,x))
bfs#2#(nil(),x) = [3]
>= [2]
= c_7()
bfs#3#(leaf(),ys,ts,x) = [1] ts + [0]
>= [1] ts + [3]
= c_8(bfs#(ts,ys,x))
bfs#3#(node(y,t1,t2),ys,ts,x) = [1] ts + [0]
>= [1] ts + [5]
= c_9(bfs#4#(eq(x,y),ys,t1,t2,ts,x,y))
bfs#4#(#true(),ys,t1,t2,ts,x,y) = [1] ts + [5]
>= [5]
= c_11()
dobfs#(t,x) = [1] t + [4] x + [0]
>= [0]
= c_12(bfs#(::(t,nil()),nil(),x))
eq#(x,y) = [4] x + [1] y + [4]
>= [0]
= c_15()
eq#(0(),0()) = [14]
>= [0]
= c_16()
eq#(s(x),s(y)) = [4] x + [1] y + [4]
>= [4] x + [1] y + [4]
= c_17(eq#(x,y))
reverse#(xs) = [2]
>= [3]
= c_14(appendreverse#(xs,nil()))
appendreverse(::(x,xs),ys) = [4] ys + [0]
>= [4] ys + [0]
= appendreverse(xs,::(x,ys))
appendreverse(nil(),ys) = [4] ys + [0]
>= [1] ys + [0]
= ys
eq(x,y) = [0]
>= [0]
= #false()
eq(0(),0()) = [0]
>= [0]
= #true()
eq(s(x),s(y)) = [0]
>= [0]
= eq(x,y)
reverse(xs) = [0]
>= [0]
= appendreverse(xs,nil())
Further, it can be verified that all rules not oriented are covered by the weightgap condition.
* Step 6: WeightGap WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict DPs:
bfs#1#(nil(),ys,x) -> c_5(bfs#2#(ys,x))
bfs#3#(leaf(),ys,ts,x) -> c_8(bfs#(ts,ys,x))
bfs#3#(node(y,t1,t2),ys,ts,x) -> c_9(bfs#4#(eq(x,y),ys,t1,t2,ts,x,y))
dobfs#(t,x) -> c_12(bfs#(::(t,nil()),nil(),x))
reverse#(xs) -> c_14(appendreverse#(xs,nil()))
- Strict TRS:
appendreverse(::(x,xs),ys) -> appendreverse(xs,::(x,ys))
appendreverse(nil(),ys) -> ys
- Weak DPs:
appendreverse#(::(x,xs),ys) -> c_1(appendreverse#(xs,::(x,ys)))
appendreverse#(nil(),ys) -> c_2()
bfs#(xs,ys,x) -> c_3(bfs#1#(xs,ys,x))
bfs#1#(::(t,ts),ys,x) -> c_4(bfs#3#(t,ys,ts,x))
bfs#2#(::(t,ts),x) -> c_6(bfs#(reverse(::(t,ts)),nil(),x))
bfs#2#(nil(),x) -> c_7()
bfs#4#(#false(),ys,t1,t2,ts,x,y) -> c_10(bfs#(ts,::(t2,::(t1,ys)),x))
bfs#4#(#true(),ys,t1,t2,ts,x,y) -> c_11()
eq#(x,y) -> c_15()
eq#(0(),0()) -> c_16()
eq#(s(x),s(y)) -> c_17(eq#(x,y))
main#(t,x) -> c_13(dobfs#(t,x))
- Weak TRS:
eq(x,y) -> #false()
eq(0(),0()) -> #true()
eq(s(x),s(y)) -> eq(x,y)
reverse(xs) -> appendreverse(xs,nil())
- Signature:
{appendreverse/2,bfs/3,bfs#1/3,bfs#2/2,bfs#3/4,bfs#4/7,dobfs/2,eq/2,main/2,reverse/1,appendreverse#/2,bfs#/3
,bfs#1#/3,bfs#2#/2,bfs#3#/4,bfs#4#/7,dobfs#/2,eq#/2,main#/2,reverse#/1} / {#false/0,#true/0,0/0,::/2,leaf/0
,nil/0,node/3,s/1,c_1/1,c_2/0,c_3/1,c_4/1,c_5/1,c_6/1,c_7/0,c_8/1,c_9/1,c_10/1,c_11/0,c_12/1,c_13/1,c_14/1
,c_15/0,c_16/0,c_17/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {appendreverse#,bfs#,bfs#1#,bfs#2#,bfs#3#,bfs#4#,dobfs#
,eq#,main#,reverse#} and constructors {#false,#true,0,::,leaf,nil,node,s}
+ Applied Processor:
WeightGap {wgDimension = 1, wgDegree = 0, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny}
+ Details:
The weightgap principle applies using the following nonconstant growth matrix-interpretation:
We apply a matrix interpretation of kind constructor based matrix interpretation:
The following argument positions are considered usable:
uargs(bfs#) = {1},
uargs(bfs#4#) = {1},
uargs(c_1) = {1},
uargs(c_3) = {1},
uargs(c_4) = {1},
uargs(c_5) = {1},
uargs(c_6) = {1},
uargs(c_8) = {1},
uargs(c_9) = {1},
uargs(c_10) = {1},
uargs(c_12) = {1},
uargs(c_13) = {1},
uargs(c_14) = {1},
uargs(c_17) = {1}
Following symbols are considered usable:
all
TcT has computed the following interpretation:
p(#false) = [4]
p(#true) = [0]
p(0) = [5]
p(::) = [1] x2 + [1]
p(appendreverse) = [4] x2 + [0]
p(bfs) = [0]
p(bfs#1) = [2] x1 + [1] x2 + [1] x3 + [0]
p(bfs#2) = [0]
p(bfs#3) = [1] x3 + [0]
p(bfs#4) = [1] x1 + [1] x2 + [2] x4 + [2] x5 + [2] x6 + [1] x7 + [0]
p(dobfs) = [0]
p(eq) = [5]
p(leaf) = [2]
p(main) = [0]
p(nil) = [0]
p(node) = [1] x1 + [1] x3 + [1]
p(reverse) = [0]
p(s) = [1] x1 + [0]
p(appendreverse#) = [6] x1 + [1]
p(bfs#) = [1] x1 + [1] x2 + [3]
p(bfs#1#) = [1] x1 + [1] x2 + [1]
p(bfs#2#) = [6]
p(bfs#3#) = [1] x2 + [1] x3 + [1]
p(bfs#4#) = [1] x1 + [1] x2 + [1] x5 + [5]
p(dobfs#) = [2] x2 + [0]
p(eq#) = [2] x2 + [0]
p(main#) = [4] x2 + [2]
p(reverse#) = [6] x1 + [6]
p(c_1) = [1] x1 + [1]
p(c_2) = [1]
p(c_3) = [1] x1 + [1]
p(c_4) = [1] x1 + [1]
p(c_5) = [1] x1 + [1]
p(c_6) = [1] x1 + [3]
p(c_7) = [0]
p(c_8) = [1] x1 + [0]
p(c_9) = [1] x1 + [0]
p(c_10) = [1] x1 + [4]
p(c_11) = [5]
p(c_12) = [1] x1 + [0]
p(c_13) = [1] x1 + [0]
p(c_14) = [1] x1 + [4]
p(c_15) = [0]
p(c_16) = [4]
p(c_17) = [1] x1 + [0]
Following rules are strictly oriented:
reverse#(xs) = [6] xs + [6]
> [6] xs + [5]
= c_14(appendreverse#(xs,nil()))
Following rules are (at-least) weakly oriented:
appendreverse#(::(x,xs),ys) = [6] xs + [7]
>= [6] xs + [2]
= c_1(appendreverse#(xs,::(x,ys)))
appendreverse#(nil(),ys) = [1]
>= [1]
= c_2()
bfs#(xs,ys,x) = [1] xs + [1] ys + [3]
>= [1] xs + [1] ys + [2]
= c_3(bfs#1#(xs,ys,x))
bfs#1#(::(t,ts),ys,x) = [1] ts + [1] ys + [2]
>= [1] ts + [1] ys + [2]
= c_4(bfs#3#(t,ys,ts,x))
bfs#1#(nil(),ys,x) = [1] ys + [1]
>= [7]
= c_5(bfs#2#(ys,x))
bfs#2#(::(t,ts),x) = [6]
>= [6]
= c_6(bfs#(reverse(::(t,ts)),nil(),x))
bfs#2#(nil(),x) = [6]
>= [0]
= c_7()
bfs#3#(leaf(),ys,ts,x) = [1] ts + [1] ys + [1]
>= [1] ts + [1] ys + [3]
= c_8(bfs#(ts,ys,x))
bfs#3#(node(y,t1,t2),ys,ts,x) = [1] ts + [1] ys + [1]
>= [1] ts + [1] ys + [10]
= c_9(bfs#4#(eq(x,y),ys,t1,t2,ts,x,y))
bfs#4#(#false(),ys,t1,t2,ts,x,y) = [1] ts + [1] ys + [9]
>= [1] ts + [1] ys + [9]
= c_10(bfs#(ts,::(t2,::(t1,ys)),x))
bfs#4#(#true(),ys,t1,t2,ts,x,y) = [1] ts + [1] ys + [5]
>= [5]
= c_11()
dobfs#(t,x) = [2] x + [0]
>= [4]
= c_12(bfs#(::(t,nil()),nil(),x))
eq#(x,y) = [2] y + [0]
>= [0]
= c_15()
eq#(0(),0()) = [10]
>= [4]
= c_16()
eq#(s(x),s(y)) = [2] y + [0]
>= [2] y + [0]
= c_17(eq#(x,y))
main#(t,x) = [4] x + [2]
>= [2] x + [0]
= c_13(dobfs#(t,x))
appendreverse(::(x,xs),ys) = [4] ys + [0]
>= [4] ys + [4]
= appendreverse(xs,::(x,ys))
appendreverse(nil(),ys) = [4] ys + [0]
>= [1] ys + [0]
= ys
eq(x,y) = [5]
>= [4]
= #false()
eq(0(),0()) = [5]
>= [0]
= #true()
eq(s(x),s(y)) = [5]
>= [5]
= eq(x,y)
reverse(xs) = [0]
>= [0]
= appendreverse(xs,nil())
Further, it can be verified that all rules not oriented are covered by the weightgap condition.
* Step 7: WeightGap WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict DPs:
bfs#1#(nil(),ys,x) -> c_5(bfs#2#(ys,x))
bfs#3#(leaf(),ys,ts,x) -> c_8(bfs#(ts,ys,x))
bfs#3#(node(y,t1,t2),ys,ts,x) -> c_9(bfs#4#(eq(x,y),ys,t1,t2,ts,x,y))
dobfs#(t,x) -> c_12(bfs#(::(t,nil()),nil(),x))
- Strict TRS:
appendreverse(::(x,xs),ys) -> appendreverse(xs,::(x,ys))
appendreverse(nil(),ys) -> ys
- Weak DPs:
appendreverse#(::(x,xs),ys) -> c_1(appendreverse#(xs,::(x,ys)))
appendreverse#(nil(),ys) -> c_2()
bfs#(xs,ys,x) -> c_3(bfs#1#(xs,ys,x))
bfs#1#(::(t,ts),ys,x) -> c_4(bfs#3#(t,ys,ts,x))
bfs#2#(::(t,ts),x) -> c_6(bfs#(reverse(::(t,ts)),nil(),x))
bfs#2#(nil(),x) -> c_7()
bfs#4#(#false(),ys,t1,t2,ts,x,y) -> c_10(bfs#(ts,::(t2,::(t1,ys)),x))
bfs#4#(#true(),ys,t1,t2,ts,x,y) -> c_11()
eq#(x,y) -> c_15()
eq#(0(),0()) -> c_16()
eq#(s(x),s(y)) -> c_17(eq#(x,y))
main#(t,x) -> c_13(dobfs#(t,x))
reverse#(xs) -> c_14(appendreverse#(xs,nil()))
- Weak TRS:
eq(x,y) -> #false()
eq(0(),0()) -> #true()
eq(s(x),s(y)) -> eq(x,y)
reverse(xs) -> appendreverse(xs,nil())
- Signature:
{appendreverse/2,bfs/3,bfs#1/3,bfs#2/2,bfs#3/4,bfs#4/7,dobfs/2,eq/2,main/2,reverse/1,appendreverse#/2,bfs#/3
,bfs#1#/3,bfs#2#/2,bfs#3#/4,bfs#4#/7,dobfs#/2,eq#/2,main#/2,reverse#/1} / {#false/0,#true/0,0/0,::/2,leaf/0
,nil/0,node/3,s/1,c_1/1,c_2/0,c_3/1,c_4/1,c_5/1,c_6/1,c_7/0,c_8/1,c_9/1,c_10/1,c_11/0,c_12/1,c_13/1,c_14/1
,c_15/0,c_16/0,c_17/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {appendreverse#,bfs#,bfs#1#,bfs#2#,bfs#3#,bfs#4#,dobfs#
,eq#,main#,reverse#} and constructors {#false,#true,0,::,leaf,nil,node,s}
+ Applied Processor:
WeightGap {wgDimension = 1, wgDegree = 0, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny}
+ Details:
The weightgap principle applies using the following nonconstant growth matrix-interpretation:
We apply a matrix interpretation of kind constructor based matrix interpretation:
The following argument positions are considered usable:
uargs(bfs#) = {1},
uargs(bfs#4#) = {1},
uargs(c_1) = {1},
uargs(c_3) = {1},
uargs(c_4) = {1},
uargs(c_5) = {1},
uargs(c_6) = {1},
uargs(c_8) = {1},
uargs(c_9) = {1},
uargs(c_10) = {1},
uargs(c_12) = {1},
uargs(c_13) = {1},
uargs(c_14) = {1},
uargs(c_17) = {1}
Following symbols are considered usable:
all
TcT has computed the following interpretation:
p(#false) = [0]
p(#true) = [0]
p(0) = [0]
p(::) = [1] x2 + [1]
p(appendreverse) = [4] x2 + [3]
p(bfs) = [0]
p(bfs#1) = [0]
p(bfs#2) = [0]
p(bfs#3) = [0]
p(bfs#4) = [1] x5 + [0]
p(dobfs) = [1] x1 + [0]
p(eq) = [5]
p(leaf) = [1]
p(main) = [4] x1 + [2] x2 + [0]
p(nil) = [0]
p(node) = [0]
p(reverse) = [4]
p(s) = [1] x1 + [5]
p(appendreverse#) = [3]
p(bfs#) = [1] x1 + [0]
p(bfs#1#) = [1] x1 + [0]
p(bfs#2#) = [4]
p(bfs#3#) = [1] x3 + [1]
p(bfs#4#) = [1] x1 + [1] x5 + [4]
p(dobfs#) = [1] x1 + [4] x2 + [0]
p(eq#) = [1] x2 + [3]
p(main#) = [2] x1 + [5] x2 + [5]
p(reverse#) = [5] x1 + [7]
p(c_1) = [1] x1 + [0]
p(c_2) = [1]
p(c_3) = [1] x1 + [0]
p(c_4) = [1] x1 + [0]
p(c_5) = [1] x1 + [4]
p(c_6) = [1] x1 + [0]
p(c_7) = [4]
p(c_8) = [1] x1 + [1]
p(c_9) = [1] x1 + [0]
p(c_10) = [1] x1 + [3]
p(c_11) = [0]
p(c_12) = [1] x1 + [0]
p(c_13) = [1] x1 + [5]
p(c_14) = [1] x1 + [4]
p(c_15) = [0]
p(c_16) = [3]
p(c_17) = [1] x1 + [0]
Following rules are strictly oriented:
appendreverse(nil(),ys) = [4] ys + [3]
> [1] ys + [0]
= ys
Following rules are (at-least) weakly oriented:
appendreverse#(::(x,xs),ys) = [3]
>= [3]
= c_1(appendreverse#(xs,::(x,ys)))
appendreverse#(nil(),ys) = [3]
>= [1]
= c_2()
bfs#(xs,ys,x) = [1] xs + [0]
>= [1] xs + [0]
= c_3(bfs#1#(xs,ys,x))
bfs#1#(::(t,ts),ys,x) = [1] ts + [1]
>= [1] ts + [1]
= c_4(bfs#3#(t,ys,ts,x))
bfs#1#(nil(),ys,x) = [0]
>= [8]
= c_5(bfs#2#(ys,x))
bfs#2#(::(t,ts),x) = [4]
>= [4]
= c_6(bfs#(reverse(::(t,ts)),nil(),x))
bfs#2#(nil(),x) = [4]
>= [4]
= c_7()
bfs#3#(leaf(),ys,ts,x) = [1] ts + [1]
>= [1] ts + [1]
= c_8(bfs#(ts,ys,x))
bfs#3#(node(y,t1,t2),ys,ts,x) = [1] ts + [1]
>= [1] ts + [9]
= c_9(bfs#4#(eq(x,y),ys,t1,t2,ts,x,y))
bfs#4#(#false(),ys,t1,t2,ts,x,y) = [1] ts + [4]
>= [1] ts + [3]
= c_10(bfs#(ts,::(t2,::(t1,ys)),x))
bfs#4#(#true(),ys,t1,t2,ts,x,y) = [1] ts + [4]
>= [0]
= c_11()
dobfs#(t,x) = [1] t + [4] x + [0]
>= [1]
= c_12(bfs#(::(t,nil()),nil(),x))
eq#(x,y) = [1] y + [3]
>= [0]
= c_15()
eq#(0(),0()) = [3]
>= [3]
= c_16()
eq#(s(x),s(y)) = [1] y + [8]
>= [1] y + [3]
= c_17(eq#(x,y))
main#(t,x) = [2] t + [5] x + [5]
>= [1] t + [4] x + [5]
= c_13(dobfs#(t,x))
reverse#(xs) = [5] xs + [7]
>= [7]
= c_14(appendreverse#(xs,nil()))
appendreverse(::(x,xs),ys) = [4] ys + [3]
>= [4] ys + [7]
= appendreverse(xs,::(x,ys))
eq(x,y) = [5]
>= [0]
= #false()
eq(0(),0()) = [5]
>= [0]
= #true()
eq(s(x),s(y)) = [5]
>= [5]
= eq(x,y)
reverse(xs) = [4]
>= [3]
= appendreverse(xs,nil())
Further, it can be verified that all rules not oriented are covered by the weightgap condition.
* Step 8: WeightGap WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict DPs:
bfs#1#(nil(),ys,x) -> c_5(bfs#2#(ys,x))
bfs#3#(leaf(),ys,ts,x) -> c_8(bfs#(ts,ys,x))
bfs#3#(node(y,t1,t2),ys,ts,x) -> c_9(bfs#4#(eq(x,y),ys,t1,t2,ts,x,y))
dobfs#(t,x) -> c_12(bfs#(::(t,nil()),nil(),x))
- Strict TRS:
appendreverse(::(x,xs),ys) -> appendreverse(xs,::(x,ys))
- Weak DPs:
appendreverse#(::(x,xs),ys) -> c_1(appendreverse#(xs,::(x,ys)))
appendreverse#(nil(),ys) -> c_2()
bfs#(xs,ys,x) -> c_3(bfs#1#(xs,ys,x))
bfs#1#(::(t,ts),ys,x) -> c_4(bfs#3#(t,ys,ts,x))
bfs#2#(::(t,ts),x) -> c_6(bfs#(reverse(::(t,ts)),nil(),x))
bfs#2#(nil(),x) -> c_7()
bfs#4#(#false(),ys,t1,t2,ts,x,y) -> c_10(bfs#(ts,::(t2,::(t1,ys)),x))
bfs#4#(#true(),ys,t1,t2,ts,x,y) -> c_11()
eq#(x,y) -> c_15()
eq#(0(),0()) -> c_16()
eq#(s(x),s(y)) -> c_17(eq#(x,y))
main#(t,x) -> c_13(dobfs#(t,x))
reverse#(xs) -> c_14(appendreverse#(xs,nil()))
- Weak TRS:
appendreverse(nil(),ys) -> ys
eq(x,y) -> #false()
eq(0(),0()) -> #true()
eq(s(x),s(y)) -> eq(x,y)
reverse(xs) -> appendreverse(xs,nil())
- Signature:
{appendreverse/2,bfs/3,bfs#1/3,bfs#2/2,bfs#3/4,bfs#4/7,dobfs/2,eq/2,main/2,reverse/1,appendreverse#/2,bfs#/3
,bfs#1#/3,bfs#2#/2,bfs#3#/4,bfs#4#/7,dobfs#/2,eq#/2,main#/2,reverse#/1} / {#false/0,#true/0,0/0,::/2,leaf/0
,nil/0,node/3,s/1,c_1/1,c_2/0,c_3/1,c_4/1,c_5/1,c_6/1,c_7/0,c_8/1,c_9/1,c_10/1,c_11/0,c_12/1,c_13/1,c_14/1
,c_15/0,c_16/0,c_17/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {appendreverse#,bfs#,bfs#1#,bfs#2#,bfs#3#,bfs#4#,dobfs#
,eq#,main#,reverse#} and constructors {#false,#true,0,::,leaf,nil,node,s}
+ Applied Processor:
WeightGap {wgDimension = 1, wgDegree = 0, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny}
+ Details:
The weightgap principle applies using the following nonconstant growth matrix-interpretation:
We apply a matrix interpretation of kind constructor based matrix interpretation:
The following argument positions are considered usable:
uargs(bfs#) = {1},
uargs(bfs#4#) = {1},
uargs(c_1) = {1},
uargs(c_3) = {1},
uargs(c_4) = {1},
uargs(c_5) = {1},
uargs(c_6) = {1},
uargs(c_8) = {1},
uargs(c_9) = {1},
uargs(c_10) = {1},
uargs(c_12) = {1},
uargs(c_13) = {1},
uargs(c_14) = {1},
uargs(c_17) = {1}
Following symbols are considered usable:
all
TcT has computed the following interpretation:
p(#false) = [2]
p(#true) = [1]
p(0) = [0]
p(::) = [1] x2 + [0]
p(appendreverse) = [1] x2 + [0]
p(bfs) = [0]
p(bfs#1) = [0]
p(bfs#2) = [0]
p(bfs#3) = [0]
p(bfs#4) = [0]
p(dobfs) = [0]
p(eq) = [3]
p(leaf) = [4]
p(main) = [1] x1 + [0]
p(nil) = [0]
p(node) = [1] x1 + [1] x3 + [2]
p(reverse) = [0]
p(s) = [1] x1 + [1]
p(appendreverse#) = [1]
p(bfs#) = [1] x1 + [2] x3 + [2]
p(bfs#1#) = [1] x1 + [2] x3 + [2]
p(bfs#2#) = [2] x2 + [3]
p(bfs#3#) = [1] x3 + [2] x4 + [0]
p(bfs#4#) = [1] x1 + [1] x5 + [2] x6 + [2]
p(dobfs#) = [2] x1 + [4] x2 + [5]
p(eq#) = [1] x2 + [0]
p(main#) = [2] x1 + [7] x2 + [7]
p(reverse#) = [1]
p(c_1) = [1] x1 + [0]
p(c_2) = [1]
p(c_3) = [1] x1 + [0]
p(c_4) = [1] x1 + [2]
p(c_5) = [1] x1 + [0]
p(c_6) = [1] x1 + [1]
p(c_7) = [0]
p(c_8) = [1] x1 + [6]
p(c_9) = [1] x1 + [7]
p(c_10) = [1] x1 + [2]
p(c_11) = [0]
p(c_12) = [1] x1 + [2]
p(c_13) = [1] x1 + [2]
p(c_14) = [1] x1 + [0]
p(c_15) = [0]
p(c_16) = [0]
p(c_17) = [1] x1 + [0]
Following rules are strictly oriented:
dobfs#(t,x) = [2] t + [4] x + [5]
> [2] x + [4]
= c_12(bfs#(::(t,nil()),nil(),x))
Following rules are (at-least) weakly oriented:
appendreverse#(::(x,xs),ys) = [1]
>= [1]
= c_1(appendreverse#(xs,::(x,ys)))
appendreverse#(nil(),ys) = [1]
>= [1]
= c_2()
bfs#(xs,ys,x) = [2] x + [1] xs + [2]
>= [2] x + [1] xs + [2]
= c_3(bfs#1#(xs,ys,x))
bfs#1#(::(t,ts),ys,x) = [1] ts + [2] x + [2]
>= [1] ts + [2] x + [2]
= c_4(bfs#3#(t,ys,ts,x))
bfs#1#(nil(),ys,x) = [2] x + [2]
>= [2] x + [3]
= c_5(bfs#2#(ys,x))
bfs#2#(::(t,ts),x) = [2] x + [3]
>= [2] x + [3]
= c_6(bfs#(reverse(::(t,ts)),nil(),x))
bfs#2#(nil(),x) = [2] x + [3]
>= [0]
= c_7()
bfs#3#(leaf(),ys,ts,x) = [1] ts + [2] x + [0]
>= [1] ts + [2] x + [8]
= c_8(bfs#(ts,ys,x))
bfs#3#(node(y,t1,t2),ys,ts,x) = [1] ts + [2] x + [0]
>= [1] ts + [2] x + [12]
= c_9(bfs#4#(eq(x,y),ys,t1,t2,ts,x,y))
bfs#4#(#false(),ys,t1,t2,ts,x,y) = [1] ts + [2] x + [4]
>= [1] ts + [2] x + [4]
= c_10(bfs#(ts,::(t2,::(t1,ys)),x))
bfs#4#(#true(),ys,t1,t2,ts,x,y) = [1] ts + [2] x + [3]
>= [0]
= c_11()
eq#(x,y) = [1] y + [0]
>= [0]
= c_15()
eq#(0(),0()) = [0]
>= [0]
= c_16()
eq#(s(x),s(y)) = [1] y + [1]
>= [1] y + [0]
= c_17(eq#(x,y))
main#(t,x) = [2] t + [7] x + [7]
>= [2] t + [4] x + [7]
= c_13(dobfs#(t,x))
reverse#(xs) = [1]
>= [1]
= c_14(appendreverse#(xs,nil()))
appendreverse(::(x,xs),ys) = [1] ys + [0]
>= [1] ys + [0]
= appendreverse(xs,::(x,ys))
appendreverse(nil(),ys) = [1] ys + [0]
>= [1] ys + [0]
= ys
eq(x,y) = [3]
>= [2]
= #false()
eq(0(),0()) = [3]
>= [1]
= #true()
eq(s(x),s(y)) = [3]
>= [3]
= eq(x,y)
reverse(xs) = [0]
>= [0]
= appendreverse(xs,nil())
Further, it can be verified that all rules not oriented are covered by the weightgap condition.
* Step 9: WeightGap WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict DPs:
bfs#1#(nil(),ys,x) -> c_5(bfs#2#(ys,x))
bfs#3#(leaf(),ys,ts,x) -> c_8(bfs#(ts,ys,x))
bfs#3#(node(y,t1,t2),ys,ts,x) -> c_9(bfs#4#(eq(x,y),ys,t1,t2,ts,x,y))
- Strict TRS:
appendreverse(::(x,xs),ys) -> appendreverse(xs,::(x,ys))
- Weak DPs:
appendreverse#(::(x,xs),ys) -> c_1(appendreverse#(xs,::(x,ys)))
appendreverse#(nil(),ys) -> c_2()
bfs#(xs,ys,x) -> c_3(bfs#1#(xs,ys,x))
bfs#1#(::(t,ts),ys,x) -> c_4(bfs#3#(t,ys,ts,x))
bfs#2#(::(t,ts),x) -> c_6(bfs#(reverse(::(t,ts)),nil(),x))
bfs#2#(nil(),x) -> c_7()
bfs#4#(#false(),ys,t1,t2,ts,x,y) -> c_10(bfs#(ts,::(t2,::(t1,ys)),x))
bfs#4#(#true(),ys,t1,t2,ts,x,y) -> c_11()
dobfs#(t,x) -> c_12(bfs#(::(t,nil()),nil(),x))
eq#(x,y) -> c_15()
eq#(0(),0()) -> c_16()
eq#(s(x),s(y)) -> c_17(eq#(x,y))
main#(t,x) -> c_13(dobfs#(t,x))
reverse#(xs) -> c_14(appendreverse#(xs,nil()))
- Weak TRS:
appendreverse(nil(),ys) -> ys
eq(x,y) -> #false()
eq(0(),0()) -> #true()
eq(s(x),s(y)) -> eq(x,y)
reverse(xs) -> appendreverse(xs,nil())
- Signature:
{appendreverse/2,bfs/3,bfs#1/3,bfs#2/2,bfs#3/4,bfs#4/7,dobfs/2,eq/2,main/2,reverse/1,appendreverse#/2,bfs#/3
,bfs#1#/3,bfs#2#/2,bfs#3#/4,bfs#4#/7,dobfs#/2,eq#/2,main#/2,reverse#/1} / {#false/0,#true/0,0/0,::/2,leaf/0
,nil/0,node/3,s/1,c_1/1,c_2/0,c_3/1,c_4/1,c_5/1,c_6/1,c_7/0,c_8/1,c_9/1,c_10/1,c_11/0,c_12/1,c_13/1,c_14/1
,c_15/0,c_16/0,c_17/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {appendreverse#,bfs#,bfs#1#,bfs#2#,bfs#3#,bfs#4#,dobfs#
,eq#,main#,reverse#} and constructors {#false,#true,0,::,leaf,nil,node,s}
+ Applied Processor:
WeightGap {wgDimension = 1, wgDegree = 0, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny}
+ Details:
The weightgap principle applies using the following nonconstant growth matrix-interpretation:
We apply a matrix interpretation of kind constructor based matrix interpretation:
The following argument positions are considered usable:
uargs(bfs#) = {1},
uargs(bfs#4#) = {1},
uargs(c_1) = {1},
uargs(c_3) = {1},
uargs(c_4) = {1},
uargs(c_5) = {1},
uargs(c_6) = {1},
uargs(c_8) = {1},
uargs(c_9) = {1},
uargs(c_10) = {1},
uargs(c_12) = {1},
uargs(c_13) = {1},
uargs(c_14) = {1},
uargs(c_17) = {1}
Following symbols are considered usable:
all
TcT has computed the following interpretation:
p(#false) = [4]
p(#true) = [3]
p(0) = [5]
p(::) = [1] x2 + [1]
p(appendreverse) = [2] x2 + [0]
p(bfs) = [1] x1 + [1] x2 + [1]
p(bfs#1) = [1] x2 + [1] x3 + [1]
p(bfs#2) = [0]
p(bfs#3) = [4] x2 + [2] x4 + [1]
p(bfs#4) = [1] x2 + [2] x3 + [1] x5 + [2]
p(dobfs) = [4] x1 + [1] x2 + [2]
p(eq) = [7]
p(leaf) = [1]
p(main) = [1] x2 + [2]
p(nil) = [0]
p(node) = [1] x1 + [1] x2 + [1] x3 + [0]
p(reverse) = [0]
p(s) = [1] x1 + [1]
p(appendreverse#) = [1] x1 + [4]
p(bfs#) = [1] x1 + [2] x2 + [0]
p(bfs#1#) = [1] x1 + [2] x2 + [0]
p(bfs#2#) = [1] x1 + [3]
p(bfs#3#) = [2] x2 + [1] x3 + [1]
p(bfs#4#) = [1] x1 + [2] x2 + [1] x5 + [2]
p(dobfs#) = [2]
p(eq#) = [1] x1 + [5]
p(main#) = [2] x1 + [2]
p(reverse#) = [1] x1 + [4]
p(c_1) = [1] x1 + [0]
p(c_2) = [4]
p(c_3) = [1] x1 + [0]
p(c_4) = [1] x1 + [0]
p(c_5) = [1] x1 + [4]
p(c_6) = [1] x1 + [4]
p(c_7) = [0]
p(c_8) = [1] x1 + [0]
p(c_9) = [1] x1 + [4]
p(c_10) = [1] x1 + [2]
p(c_11) = [0]
p(c_12) = [1] x1 + [0]
p(c_13) = [1] x1 + [0]
p(c_14) = [1] x1 + [0]
p(c_15) = [0]
p(c_16) = [1]
p(c_17) = [1] x1 + [1]
Following rules are strictly oriented:
bfs#3#(leaf(),ys,ts,x) = [1] ts + [2] ys + [1]
> [1] ts + [2] ys + [0]
= c_8(bfs#(ts,ys,x))
Following rules are (at-least) weakly oriented:
appendreverse#(::(x,xs),ys) = [1] xs + [5]
>= [1] xs + [4]
= c_1(appendreverse#(xs,::(x,ys)))
appendreverse#(nil(),ys) = [4]
>= [4]
= c_2()
bfs#(xs,ys,x) = [1] xs + [2] ys + [0]
>= [1] xs + [2] ys + [0]
= c_3(bfs#1#(xs,ys,x))
bfs#1#(::(t,ts),ys,x) = [1] ts + [2] ys + [1]
>= [1] ts + [2] ys + [1]
= c_4(bfs#3#(t,ys,ts,x))
bfs#1#(nil(),ys,x) = [2] ys + [0]
>= [1] ys + [7]
= c_5(bfs#2#(ys,x))
bfs#2#(::(t,ts),x) = [1] ts + [4]
>= [4]
= c_6(bfs#(reverse(::(t,ts)),nil(),x))
bfs#2#(nil(),x) = [3]
>= [0]
= c_7()
bfs#3#(node(y,t1,t2),ys,ts,x) = [1] ts + [2] ys + [1]
>= [1] ts + [2] ys + [13]
= c_9(bfs#4#(eq(x,y),ys,t1,t2,ts,x,y))
bfs#4#(#false(),ys,t1,t2,ts,x,y) = [1] ts + [2] ys + [6]
>= [1] ts + [2] ys + [6]
= c_10(bfs#(ts,::(t2,::(t1,ys)),x))
bfs#4#(#true(),ys,t1,t2,ts,x,y) = [1] ts + [2] ys + [5]
>= [0]
= c_11()
dobfs#(t,x) = [2]
>= [1]
= c_12(bfs#(::(t,nil()),nil(),x))
eq#(x,y) = [1] x + [5]
>= [0]
= c_15()
eq#(0(),0()) = [10]
>= [1]
= c_16()
eq#(s(x),s(y)) = [1] x + [6]
>= [1] x + [6]
= c_17(eq#(x,y))
main#(t,x) = [2] t + [2]
>= [2]
= c_13(dobfs#(t,x))
reverse#(xs) = [1] xs + [4]
>= [1] xs + [4]
= c_14(appendreverse#(xs,nil()))
appendreverse(::(x,xs),ys) = [2] ys + [0]
>= [2] ys + [2]
= appendreverse(xs,::(x,ys))
appendreverse(nil(),ys) = [2] ys + [0]
>= [1] ys + [0]
= ys
eq(x,y) = [7]
>= [4]
= #false()
eq(0(),0()) = [7]
>= [3]
= #true()
eq(s(x),s(y)) = [7]
>= [7]
= eq(x,y)
reverse(xs) = [0]
>= [0]
= appendreverse(xs,nil())
Further, it can be verified that all rules not oriented are covered by the weightgap condition.
* Step 10: WeightGap WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict DPs:
bfs#1#(nil(),ys,x) -> c_5(bfs#2#(ys,x))
bfs#3#(node(y,t1,t2),ys,ts,x) -> c_9(bfs#4#(eq(x,y),ys,t1,t2,ts,x,y))
- Strict TRS:
appendreverse(::(x,xs),ys) -> appendreverse(xs,::(x,ys))
- Weak DPs:
appendreverse#(::(x,xs),ys) -> c_1(appendreverse#(xs,::(x,ys)))
appendreverse#(nil(),ys) -> c_2()
bfs#(xs,ys,x) -> c_3(bfs#1#(xs,ys,x))
bfs#1#(::(t,ts),ys,x) -> c_4(bfs#3#(t,ys,ts,x))
bfs#2#(::(t,ts),x) -> c_6(bfs#(reverse(::(t,ts)),nil(),x))
bfs#2#(nil(),x) -> c_7()
bfs#3#(leaf(),ys,ts,x) -> c_8(bfs#(ts,ys,x))
bfs#4#(#false(),ys,t1,t2,ts,x,y) -> c_10(bfs#(ts,::(t2,::(t1,ys)),x))
bfs#4#(#true(),ys,t1,t2,ts,x,y) -> c_11()
dobfs#(t,x) -> c_12(bfs#(::(t,nil()),nil(),x))
eq#(x,y) -> c_15()
eq#(0(),0()) -> c_16()
eq#(s(x),s(y)) -> c_17(eq#(x,y))
main#(t,x) -> c_13(dobfs#(t,x))
reverse#(xs) -> c_14(appendreverse#(xs,nil()))
- Weak TRS:
appendreverse(nil(),ys) -> ys
eq(x,y) -> #false()
eq(0(),0()) -> #true()
eq(s(x),s(y)) -> eq(x,y)
reverse(xs) -> appendreverse(xs,nil())
- Signature:
{appendreverse/2,bfs/3,bfs#1/3,bfs#2/2,bfs#3/4,bfs#4/7,dobfs/2,eq/2,main/2,reverse/1,appendreverse#/2,bfs#/3
,bfs#1#/3,bfs#2#/2,bfs#3#/4,bfs#4#/7,dobfs#/2,eq#/2,main#/2,reverse#/1} / {#false/0,#true/0,0/0,::/2,leaf/0
,nil/0,node/3,s/1,c_1/1,c_2/0,c_3/1,c_4/1,c_5/1,c_6/1,c_7/0,c_8/1,c_9/1,c_10/1,c_11/0,c_12/1,c_13/1,c_14/1
,c_15/0,c_16/0,c_17/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {appendreverse#,bfs#,bfs#1#,bfs#2#,bfs#3#,bfs#4#,dobfs#
,eq#,main#,reverse#} and constructors {#false,#true,0,::,leaf,nil,node,s}
+ Applied Processor:
WeightGap {wgDimension = 1, wgDegree = 0, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny}
+ Details:
The weightgap principle applies using the following nonconstant growth matrix-interpretation:
We apply a matrix interpretation of kind constructor based matrix interpretation:
The following argument positions are considered usable:
uargs(bfs#) = {1},
uargs(bfs#4#) = {1},
uargs(c_1) = {1},
uargs(c_3) = {1},
uargs(c_4) = {1},
uargs(c_5) = {1},
uargs(c_6) = {1},
uargs(c_8) = {1},
uargs(c_9) = {1},
uargs(c_10) = {1},
uargs(c_12) = {1},
uargs(c_13) = {1},
uargs(c_14) = {1},
uargs(c_17) = {1}
Following symbols are considered usable:
all
TcT has computed the following interpretation:
p(#false) = [0]
p(#true) = [0]
p(0) = [0]
p(::) = [1] x2 + [1]
p(appendreverse) = [4] x2 + [2]
p(bfs) = [0]
p(bfs#1) = [0]
p(bfs#2) = [0]
p(bfs#3) = [0]
p(bfs#4) = [1] x7 + [0]
p(dobfs) = [0]
p(eq) = [0]
p(leaf) = [0]
p(main) = [1] x1 + [1] x2 + [1]
p(nil) = [0]
p(node) = [1] x2 + [1] x3 + [1]
p(reverse) = [3]
p(s) = [0]
p(appendreverse#) = [3] x1 + [1]
p(bfs#) = [1] x1 + [0]
p(bfs#1#) = [1] x1 + [0]
p(bfs#2#) = [3]
p(bfs#3#) = [1] x3 + [1]
p(bfs#4#) = [1] x1 + [1] x5 + [0]
p(dobfs#) = [1] x1 + [4]
p(eq#) = [1]
p(main#) = [3] x1 + [4]
p(reverse#) = [4] x1 + [2]
p(c_1) = [1] x1 + [0]
p(c_2) = [1]
p(c_3) = [1] x1 + [0]
p(c_4) = [1] x1 + [0]
p(c_5) = [1] x1 + [2]
p(c_6) = [1] x1 + [0]
p(c_7) = [1]
p(c_8) = [1] x1 + [1]
p(c_9) = [1] x1 + [0]
p(c_10) = [1] x1 + [0]
p(c_11) = [0]
p(c_12) = [1] x1 + [3]
p(c_13) = [1] x1 + [0]
p(c_14) = [1] x1 + [1]
p(c_15) = [0]
p(c_16) = [1]
p(c_17) = [1] x1 + [0]
Following rules are strictly oriented:
bfs#3#(node(y,t1,t2),ys,ts,x) = [1] ts + [1]
> [1] ts + [0]
= c_9(bfs#4#(eq(x,y),ys,t1,t2,ts,x,y))
Following rules are (at-least) weakly oriented:
appendreverse#(::(x,xs),ys) = [3] xs + [4]
>= [3] xs + [1]
= c_1(appendreverse#(xs,::(x,ys)))
appendreverse#(nil(),ys) = [1]
>= [1]
= c_2()
bfs#(xs,ys,x) = [1] xs + [0]
>= [1] xs + [0]
= c_3(bfs#1#(xs,ys,x))
bfs#1#(::(t,ts),ys,x) = [1] ts + [1]
>= [1] ts + [1]
= c_4(bfs#3#(t,ys,ts,x))
bfs#1#(nil(),ys,x) = [0]
>= [5]
= c_5(bfs#2#(ys,x))
bfs#2#(::(t,ts),x) = [3]
>= [3]
= c_6(bfs#(reverse(::(t,ts)),nil(),x))
bfs#2#(nil(),x) = [3]
>= [1]
= c_7()
bfs#3#(leaf(),ys,ts,x) = [1] ts + [1]
>= [1] ts + [1]
= c_8(bfs#(ts,ys,x))
bfs#4#(#false(),ys,t1,t2,ts,x,y) = [1] ts + [0]
>= [1] ts + [0]
= c_10(bfs#(ts,::(t2,::(t1,ys)),x))
bfs#4#(#true(),ys,t1,t2,ts,x,y) = [1] ts + [0]
>= [0]
= c_11()
dobfs#(t,x) = [1] t + [4]
>= [4]
= c_12(bfs#(::(t,nil()),nil(),x))
eq#(x,y) = [1]
>= [0]
= c_15()
eq#(0(),0()) = [1]
>= [1]
= c_16()
eq#(s(x),s(y)) = [1]
>= [1]
= c_17(eq#(x,y))
main#(t,x) = [3] t + [4]
>= [1] t + [4]
= c_13(dobfs#(t,x))
reverse#(xs) = [4] xs + [2]
>= [3] xs + [2]
= c_14(appendreverse#(xs,nil()))
appendreverse(::(x,xs),ys) = [4] ys + [2]
>= [4] ys + [6]
= appendreverse(xs,::(x,ys))
appendreverse(nil(),ys) = [4] ys + [2]
>= [1] ys + [0]
= ys
eq(x,y) = [0]
>= [0]
= #false()
eq(0(),0()) = [0]
>= [0]
= #true()
eq(s(x),s(y)) = [0]
>= [0]
= eq(x,y)
reverse(xs) = [3]
>= [2]
= appendreverse(xs,nil())
Further, it can be verified that all rules not oriented are covered by the weightgap condition.
* Step 11: NaturalMI WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict DPs:
bfs#1#(nil(),ys,x) -> c_5(bfs#2#(ys,x))
- Strict TRS:
appendreverse(::(x,xs),ys) -> appendreverse(xs,::(x,ys))
- Weak DPs:
appendreverse#(::(x,xs),ys) -> c_1(appendreverse#(xs,::(x,ys)))
appendreverse#(nil(),ys) -> c_2()
bfs#(xs,ys,x) -> c_3(bfs#1#(xs,ys,x))
bfs#1#(::(t,ts),ys,x) -> c_4(bfs#3#(t,ys,ts,x))
bfs#2#(::(t,ts),x) -> c_6(bfs#(reverse(::(t,ts)),nil(),x))
bfs#2#(nil(),x) -> c_7()
bfs#3#(leaf(),ys,ts,x) -> c_8(bfs#(ts,ys,x))
bfs#3#(node(y,t1,t2),ys,ts,x) -> c_9(bfs#4#(eq(x,y),ys,t1,t2,ts,x,y))
bfs#4#(#false(),ys,t1,t2,ts,x,y) -> c_10(bfs#(ts,::(t2,::(t1,ys)),x))
bfs#4#(#true(),ys,t1,t2,ts,x,y) -> c_11()
dobfs#(t,x) -> c_12(bfs#(::(t,nil()),nil(),x))
eq#(x,y) -> c_15()
eq#(0(),0()) -> c_16()
eq#(s(x),s(y)) -> c_17(eq#(x,y))
main#(t,x) -> c_13(dobfs#(t,x))
reverse#(xs) -> c_14(appendreverse#(xs,nil()))
- Weak TRS:
appendreverse(nil(),ys) -> ys
eq(x,y) -> #false()
eq(0(),0()) -> #true()
eq(s(x),s(y)) -> eq(x,y)
reverse(xs) -> appendreverse(xs,nil())
- Signature:
{appendreverse/2,bfs/3,bfs#1/3,bfs#2/2,bfs#3/4,bfs#4/7,dobfs/2,eq/2,main/2,reverse/1,appendreverse#/2,bfs#/3
,bfs#1#/3,bfs#2#/2,bfs#3#/4,bfs#4#/7,dobfs#/2,eq#/2,main#/2,reverse#/1} / {#false/0,#true/0,0/0,::/2,leaf/0
,nil/0,node/3,s/1,c_1/1,c_2/0,c_3/1,c_4/1,c_5/1,c_6/1,c_7/0,c_8/1,c_9/1,c_10/1,c_11/0,c_12/1,c_13/1,c_14/1
,c_15/0,c_16/0,c_17/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {appendreverse#,bfs#,bfs#1#,bfs#2#,bfs#3#,bfs#4#,dobfs#
,eq#,main#,reverse#} and constructors {#false,#true,0,::,leaf,nil,node,s}
+ Applied Processor:
NaturalMI {miDimension = 2, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any strict-rules}
+ Details:
We apply a matrix interpretation of kind constructor based matrix interpretation (containing no more than 1 non-zero interpretation-entries in the diagonal of the component-wise maxima):
The following argument positions are considered usable:
uargs(bfs#) = {1},
uargs(bfs#4#) = {1},
uargs(c_1) = {1},
uargs(c_3) = {1},
uargs(c_4) = {1},
uargs(c_5) = {1},
uargs(c_6) = {1},
uargs(c_8) = {1},
uargs(c_9) = {1},
uargs(c_10) = {1},
uargs(c_12) = {1},
uargs(c_13) = {1},
uargs(c_14) = {1},
uargs(c_17) = {1}
Following symbols are considered usable:
{appendreverse,eq,reverse,appendreverse#,bfs#,bfs#1#,bfs#2#,bfs#3#,bfs#4#,dobfs#,eq#,main#,reverse#}
TcT has computed the following interpretation:
p(#false) = [0]
[2]
p(#true) = [0]
[2]
p(0) = [2]
[2]
p(::) = [1 1] x1 + [1 1] x2 + [0]
[0 0] [0 0] [1]
p(appendreverse) = [1 1] x1 + [1 1] x2 + [0]
[2 1] [0 1] [0]
p(bfs) = [2]
[0]
p(bfs#1) = [0]
[0]
p(bfs#2) = [2]
[0]
p(bfs#3) = [0 0] x3 + [0 0] x4 + [1]
[0 1] [0 2] [1]
p(bfs#4) = [2 0] x1 + [0 0] x5 + [1]
[1 1] [0 1] [1]
p(dobfs) = [2]
[0]
p(eq) = [0]
[2]
p(leaf) = [0]
[2]
p(main) = [0]
[0]
p(nil) = [0]
[0]
p(node) = [1 2] x1 + [1 1] x2 + [1 1] x3 + [0]
[0 0] [0 0] [0 0] [3]
p(reverse) = [1 1] x1 + [0]
[2 2] [0]
p(s) = [0]
[0]
p(appendreverse#) = [0 0] x1 + [0 0] x2 + [1]
[2 2] [2 0] [3]
p(bfs#) = [2 0] x1 + [2 3] x2 + [1]
[0 2] [0 0] [2]
p(bfs#1#) = [2 0] x1 + [2 3] x2 + [0 0] x3 + [1]
[2 0] [2 0] [0 1] [0]
p(bfs#2#) = [2 3] x1 + [0]
[2 2] [1]
p(bfs#3#) = [2 2] x1 + [2 3] x2 + [2 2] x3 + [0 0] x4 + [1]
[0 0] [2 0] [0 2] [2 3] [2]
p(bfs#4#) = [2 3] x1 + [2 2] x2 + [2 2] x3 + [2 2] x4 + [2 0] x5 + [1 1] x7 + [1]
[0 2] [0 0] [0 2] [0 0] [2 2] [0 2] [3]
p(dobfs#) = [3 2] x1 + [2 0] x2 + [1]
[1 1] [0 0] [1]
p(eq#) = [0 0] x2 + [0]
[2 0] [0]
p(main#) = [3 3] x1 + [2 2] x2 + [3]
[3 2] [2 0] [1]
p(reverse#) = [0 0] x1 + [2]
[2 1] [2]
p(c_1) = [1 0] x1 + [0]
[2 0] [3]
p(c_2) = [1]
[3]
p(c_3) = [1 0] x1 + [0]
[0 0] [2]
p(c_4) = [1 0] x1 + [0]
[0 0] [0]
p(c_5) = [1 0] x1 + [0]
[0 0] [0]
p(c_6) = [1 0] x1 + [0]
[0 0] [0]
p(c_7) = [0]
[0]
p(c_8) = [1 1] x1 + [1]
[0 1] [0]
p(c_9) = [1 0] x1 + [0]
[0 0] [2]
p(c_10) = [1 0] x1 + [1]
[0 1] [0]
p(c_11) = [2]
[2]
p(c_12) = [1 0] x1 + [0]
[0 0] [0]
p(c_13) = [1 0] x1 + [2]
[1 0] [0]
p(c_14) = [2 0] x1 + [0]
[2 0] [0]
p(c_15) = [0]
[0]
p(c_16) = [0]
[0]
p(c_17) = [2 0] x1 + [0]
[0 0] [0]
Following rules are strictly oriented:
bfs#1#(nil(),ys,x) = [0 0] x + [2 3] ys + [1]
[0 1] [2 0] [0]
> [2 3] ys + [0]
[0 0] [0]
= c_5(bfs#2#(ys,x))
Following rules are (at-least) weakly oriented:
appendreverse#(::(x,xs),ys) = [0 0] x + [0 0] xs + [0 0] ys + [1]
[2 2] [2 2] [2 0] [5]
>= [1]
[5]
= c_1(appendreverse#(xs,::(x,ys)))
appendreverse#(nil(),ys) = [0 0] ys + [1]
[2 0] [3]
>= [1]
[3]
= c_2()
bfs#(xs,ys,x) = [2 0] xs + [2 3] ys + [1]
[0 2] [0 0] [2]
>= [2 0] xs + [2 3] ys + [1]
[0 0] [0 0] [2]
= c_3(bfs#1#(xs,ys,x))
bfs#1#(::(t,ts),ys,x) = [2 2] t + [2 2] ts + [0 0] x + [2 3] ys + [1]
[2 2] [2 2] [0 1] [2 0] [0]
>= [2 2] t + [2 2] ts + [2 3] ys + [1]
[0 0] [0 0] [0 0] [0]
= c_4(bfs#3#(t,ys,ts,x))
bfs#2#(::(t,ts),x) = [2 2] t + [2 2] ts + [3]
[2 2] [2 2] [3]
>= [2 2] t + [2 2] ts + [3]
[0 0] [0 0] [0]
= c_6(bfs#(reverse(::(t,ts)),nil(),x))
bfs#2#(nil(),x) = [0]
[1]
>= [0]
[0]
= c_7()
bfs#3#(leaf(),ys,ts,x) = [2 2] ts + [0 0] x + [2 3] ys + [5]
[0 2] [2 3] [2 0] [2]
>= [2 2] ts + [2 3] ys + [4]
[0 2] [0 0] [2]
= c_8(bfs#(ts,ys,x))
bfs#3#(node(y,t1,t2),ys,ts,x) = [2 2] t1 + [2 2] t2 + [2 2] ts + [0 0] x + [2 4] y + [2 3] ys + [7]
[0 0] [0 0] [0 2] [2 3] [0 0] [2 0] [2]
>= [2 2] t1 + [2 2] t2 + [2 0] ts + [1 1] y + [2 2] ys + [7]
[0 0] [0 0] [0 0] [0 0] [0 0] [2]
= c_9(bfs#4#(eq(x,y),ys,t1,t2,ts,x,y))
bfs#4#(#false(),ys,t1,t2,ts,x,y) = [2 2] t1 + [2 2] t2 + [2 0] ts + [1 1] y + [2 2] ys + [7]
[0 2] [0 0] [2 2] [0 2] [0 0] [7]
>= [2 2] t1 + [2 2] t2 + [2 0] ts + [2 2] ys + [7]
[0 0] [0 0] [0 2] [0 0] [2]
= c_10(bfs#(ts,::(t2,::(t1,ys)),x))
bfs#4#(#true(),ys,t1,t2,ts,x,y) = [2 2] t1 + [2 2] t2 + [2 0] ts + [1 1] y + [2 2] ys + [7]
[0 2] [0 0] [2 2] [0 2] [0 0] [7]
>= [2]
[2]
= c_11()
dobfs#(t,x) = [3 2] t + [2 0] x + [1]
[1 1] [0 0] [1]
>= [2 2] t + [1]
[0 0] [0]
= c_12(bfs#(::(t,nil()),nil(),x))
eq#(x,y) = [0 0] y + [0]
[2 0] [0]
>= [0]
[0]
= c_15()
eq#(0(),0()) = [0]
[4]
>= [0]
[0]
= c_16()
eq#(s(x),s(y)) = [0]
[0]
>= [0]
[0]
= c_17(eq#(x,y))
main#(t,x) = [3 3] t + [2 2] x + [3]
[3 2] [2 0] [1]
>= [3 2] t + [2 0] x + [3]
[3 2] [2 0] [1]
= c_13(dobfs#(t,x))
reverse#(xs) = [0 0] xs + [2]
[2 1] [2]
>= [2]
[2]
= c_14(appendreverse#(xs,nil()))
appendreverse(::(x,xs),ys) = [1 1] x + [1 1] xs + [1 1] ys + [1]
[2 2] [2 2] [0 1] [1]
>= [1 1] x + [1 1] xs + [1 1] ys + [1]
[0 0] [2 1] [0 0] [1]
= appendreverse(xs,::(x,ys))
appendreverse(nil(),ys) = [1 1] ys + [0]
[0 1] [0]
>= [1 0] ys + [0]
[0 1] [0]
= ys
eq(x,y) = [0]
[2]
>= [0]
[2]
= #false()
eq(0(),0()) = [0]
[2]
>= [0]
[2]
= #true()
eq(s(x),s(y)) = [0]
[2]
>= [0]
[2]
= eq(x,y)
reverse(xs) = [1 1] xs + [0]
[2 2] [0]
>= [1 1] xs + [0]
[2 1] [0]
= appendreverse(xs,nil())
* Step 12: NaturalMI WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict TRS:
appendreverse(::(x,xs),ys) -> appendreverse(xs,::(x,ys))
- Weak DPs:
appendreverse#(::(x,xs),ys) -> c_1(appendreverse#(xs,::(x,ys)))
appendreverse#(nil(),ys) -> c_2()
bfs#(xs,ys,x) -> c_3(bfs#1#(xs,ys,x))
bfs#1#(::(t,ts),ys,x) -> c_4(bfs#3#(t,ys,ts,x))
bfs#1#(nil(),ys,x) -> c_5(bfs#2#(ys,x))
bfs#2#(::(t,ts),x) -> c_6(bfs#(reverse(::(t,ts)),nil(),x))
bfs#2#(nil(),x) -> c_7()
bfs#3#(leaf(),ys,ts,x) -> c_8(bfs#(ts,ys,x))
bfs#3#(node(y,t1,t2),ys,ts,x) -> c_9(bfs#4#(eq(x,y),ys,t1,t2,ts,x,y))
bfs#4#(#false(),ys,t1,t2,ts,x,y) -> c_10(bfs#(ts,::(t2,::(t1,ys)),x))
bfs#4#(#true(),ys,t1,t2,ts,x,y) -> c_11()
dobfs#(t,x) -> c_12(bfs#(::(t,nil()),nil(),x))
eq#(x,y) -> c_15()
eq#(0(),0()) -> c_16()
eq#(s(x),s(y)) -> c_17(eq#(x,y))
main#(t,x) -> c_13(dobfs#(t,x))
reverse#(xs) -> c_14(appendreverse#(xs,nil()))
- Weak TRS:
appendreverse(nil(),ys) -> ys
eq(x,y) -> #false()
eq(0(),0()) -> #true()
eq(s(x),s(y)) -> eq(x,y)
reverse(xs) -> appendreverse(xs,nil())
- Signature:
{appendreverse/2,bfs/3,bfs#1/3,bfs#2/2,bfs#3/4,bfs#4/7,dobfs/2,eq/2,main/2,reverse/1,appendreverse#/2,bfs#/3
,bfs#1#/3,bfs#2#/2,bfs#3#/4,bfs#4#/7,dobfs#/2,eq#/2,main#/2,reverse#/1} / {#false/0,#true/0,0/0,::/2,leaf/0
,nil/0,node/3,s/1,c_1/1,c_2/0,c_3/1,c_4/1,c_5/1,c_6/1,c_7/0,c_8/1,c_9/1,c_10/1,c_11/0,c_12/1,c_13/1,c_14/1
,c_15/0,c_16/0,c_17/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {appendreverse#,bfs#,bfs#1#,bfs#2#,bfs#3#,bfs#4#,dobfs#
,eq#,main#,reverse#} and constructors {#false,#true,0,::,leaf,nil,node,s}
+ Applied Processor:
NaturalMI {miDimension = 3, miDegree = 2, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any strict-rules}
+ Details:
We apply a matrix interpretation of kind constructor based matrix interpretation (containing no more than 2 non-zero interpretation-entries in the diagonal of the component-wise maxima):
The following argument positions are considered usable:
uargs(bfs#) = {1},
uargs(bfs#4#) = {1},
uargs(c_1) = {1},
uargs(c_3) = {1},
uargs(c_4) = {1},
uargs(c_5) = {1},
uargs(c_6) = {1},
uargs(c_8) = {1},
uargs(c_9) = {1},
uargs(c_10) = {1},
uargs(c_12) = {1},
uargs(c_13) = {1},
uargs(c_14) = {1},
uargs(c_17) = {1}
Following symbols are considered usable:
{appendreverse,eq,reverse,appendreverse#,bfs#,bfs#1#,bfs#2#,bfs#3#,bfs#4#,dobfs#,eq#,main#,reverse#}
TcT has computed the following interpretation:
p(#false) = [1]
[0]
[0]
p(#true) = [0]
[0]
[0]
p(0) = [1]
[0]
[1]
p(::) = [0 1 1] [1 0 0] [0]
[0 1 1] x1 + [0 1 0] x2 + [1]
[0 0 0] [0 0 0] [0]
p(appendreverse) = [0 1 0] [1 0 0] [0]
[1 1 0] x1 + [1 1 0] x2 + [0]
[0 0 0] [0 0 1] [0]
p(bfs) = [0]
[0]
[0]
p(bfs#1) = [0]
[0]
[0]
p(bfs#2) = [0]
[0]
[0]
p(bfs#3) = [0]
[0]
[0]
p(bfs#4) = [0]
[0]
[0]
p(dobfs) = [0]
[0]
[0]
p(eq) = [0 0 0] [1]
[1 0 0] x1 + [0]
[0 0 0] [0]
p(leaf) = [0]
[0]
[1]
p(main) = [0]
[0]
[0]
p(nil) = [0]
[0]
[1]
p(node) = [0 1 0] [1 0 1] [0 1 0] [1]
[0 1 1] x1 + [0 1 1] x2 + [0 1 1] x3 + [1]
[0 0 0] [0 0 0] [0 0 0] [1]
p(reverse) = [0 1 0] [0]
[1 1 0] x1 + [0]
[1 0 0] [1]
p(s) = [1 0 1] [1]
[0 1 1] x1 + [1]
[0 0 0] [1]
p(appendreverse#) = [0 0 0] [0]
[1 1 0] x1 + [1]
[0 0 0] [1]
p(bfs#) = [1 0 0] [0 1 0] [0 1 0] [0]
[0 0 0] x1 + [0 0 1] x2 + [0 0 0] x3 + [0]
[0 0 0] [0 0 1] [1 0 0] [0]
p(bfs#1#) = [1 0 0] [0 1 0] [0 1 0] [0]
[0 0 0] x1 + [0 1 1] x2 + [0 0 1] x3 + [0]
[0 0 1] [0 1 1] [1 1 1] [1]
p(bfs#2#) = [0 1 0] [0 1 0] [0]
[0 1 0] x1 + [0 1 0] x2 + [1]
[0 1 1] [1 1 0] [1]
p(bfs#3#) = [0 1 1] [0 1 0] [1 0 0] [0 1 0] [0]
[1 1 1] x1 + [1 1 0] x2 + [1 1 1] x3 + [0 1 1] x4 + [0]
[1 0 0] [0 1 1] [1 1 0] [0 1 0] [1]
p(bfs#4#) = [1 0 0] [0 1 0] [0 1 1] [0 1 1] [1 0 0] [0 1 0] [0 1 1] [1]
[1 0 0] x1 + [0 0 0] x2 + [0 1 0] x3 + [0 1 1] x4 + [1 0 0] x5 + [0 1 0] x6 + [0 0 0] x7 + [1]
[0 0 0] [0 0 0] [0 0 0] [0 1 0] [0 0 0] [0 0 1] [0 0 0] [0]
p(dobfs#) = [0 1 1] [1 1 1] [1]
[1 1 1] x1 + [0 1 0] x2 + [1]
[1 0 0] [0 0 0] [0]
p(eq#) = [0 1 0] [0 1 0] [1]
[0 0 0] x1 + [0 0 1] x2 + [1]
[1 1 1] [0 0 0] [0]
p(main#) = [1 1 1] [1 1 1] [1]
[0 0 0] x1 + [0 1 0] x2 + [0]
[0 1 0] [0 0 1] [0]
p(reverse#) = [1 1 1] [1]
[1 0 0] x1 + [0]
[1 1 1] [1]
p(c_1) = [1 0 0] [0]
[0 1 0] x1 + [1]
[0 0 0] [0]
p(c_2) = [0]
[0]
[0]
p(c_3) = [1 0 0] [0]
[0 0 0] x1 + [0]
[0 0 0] [0]
p(c_4) = [1 0 0] [0]
[0 0 0] x1 + [0]
[0 0 0] [1]
p(c_5) = [1 0 0] [0]
[0 0 0] x1 + [0]
[1 0 0] [0]
p(c_6) = [1 0 0] [0]
[1 0 0] x1 + [1]
[0 0 1] [1]
p(c_7) = [0]
[0]
[0]
p(c_8) = [1 0 0] [1]
[1 0 0] x1 + [1]
[1 0 0] [0]
p(c_9) = [1 0 0] [0]
[0 1 0] x1 + [0]
[0 0 0] [0]
p(c_10) = [1 0 0] [0]
[0 0 0] x1 + [1]
[0 0 0] [0]
p(c_11) = [1]
[1]
[0]
p(c_12) = [1 0 1] [0]
[1 0 0] x1 + [0]
[0 0 0] [0]
p(c_13) = [1 0 1] [0]
[0 0 0] x1 + [0]
[0 0 0] [0]
p(c_14) = [1 0 0] [1]
[0 0 0] x1 + [0]
[0 1 0] [0]
p(c_15) = [0]
[0]
[0]
p(c_16) = [0]
[0]
[0]
p(c_17) = [1 1 0] [0]
[0 0 0] x1 + [0]
[0 0 1] [0]
Following rules are strictly oriented:
appendreverse(::(x,xs),ys) = [0 1 1] [0 1 0] [1 0 0] [1]
[0 2 2] x + [1 1 0] xs + [1 1 0] ys + [1]
[0 0 0] [0 0 0] [0 0 1] [0]
> [0 1 1] [0 1 0] [1 0 0] [0]
[0 2 2] x + [1 1 0] xs + [1 1 0] ys + [1]
[0 0 0] [0 0 0] [0 0 0] [0]
= appendreverse(xs,::(x,ys))
Following rules are (at-least) weakly oriented:
appendreverse#(::(x,xs),ys) = [0 0 0] [0 0 0] [0]
[0 2 2] x + [1 1 0] xs + [2]
[0 0 0] [0 0 0] [1]
>= [0 0 0] [0]
[1 1 0] xs + [2]
[0 0 0] [0]
= c_1(appendreverse#(xs,::(x,ys)))
appendreverse#(nil(),ys) = [0]
[1]
[1]
>= [0]
[0]
[0]
= c_2()
bfs#(xs,ys,x) = [0 1 0] [1 0 0] [0 1 0] [0]
[0 0 0] x + [0 0 0] xs + [0 0 1] ys + [0]
[1 0 0] [0 0 0] [0 0 1] [0]
>= [0 1 0] [1 0 0] [0 1 0] [0]
[0 0 0] x + [0 0 0] xs + [0 0 0] ys + [0]
[0 0 0] [0 0 0] [0 0 0] [0]
= c_3(bfs#1#(xs,ys,x))
bfs#1#(::(t,ts),ys,x) = [0 1 1] [1 0 0] [0 1 0] [0 1 0] [0]
[0 0 0] t + [0 0 0] ts + [0 0 1] x + [0 1 1] ys + [0]
[0 0 0] [0 0 0] [1 1 1] [0 1 1] [1]
>= [0 1 1] [1 0 0] [0 1 0] [0 1 0] [0]
[0 0 0] t + [0 0 0] ts + [0 0 0] x + [0 0 0] ys + [0]
[0 0 0] [0 0 0] [0 0 0] [0 0 0] [1]
= c_4(bfs#3#(t,ys,ts,x))
bfs#1#(nil(),ys,x) = [0 1 0] [0 1 0] [0]
[0 0 1] x + [0 1 1] ys + [0]
[1 1 1] [0 1 1] [2]
>= [0 1 0] [0 1 0] [0]
[0 0 0] x + [0 0 0] ys + [0]
[0 1 0] [0 1 0] [0]
= c_5(bfs#2#(ys,x))
bfs#2#(::(t,ts),x) = [0 1 1] [0 1 0] [0 1 0] [1]
[0 1 1] t + [0 1 0] ts + [0 1 0] x + [2]
[0 1 1] [0 1 0] [1 1 0] [2]
>= [0 1 1] [0 1 0] [0 1 0] [1]
[0 1 1] t + [0 1 0] ts + [0 1 0] x + [2]
[0 0 0] [0 0 0] [1 0 0] [2]
= c_6(bfs#(reverse(::(t,ts)),nil(),x))
bfs#2#(nil(),x) = [0 1 0] [0]
[0 1 0] x + [1]
[1 1 0] [2]
>= [0]
[0]
[0]
= c_7()
bfs#3#(leaf(),ys,ts,x) = [1 0 0] [0 1 0] [0 1 0] [1]
[1 1 1] ts + [0 1 1] x + [1 1 0] ys + [1]
[1 1 0] [0 1 0] [0 1 1] [1]
>= [1 0 0] [0 1 0] [0 1 0] [1]
[1 0 0] ts + [0 1 0] x + [0 1 0] ys + [1]
[1 0 0] [0 1 0] [0 1 0] [0]
= c_8(bfs#(ts,ys,x))
bfs#3#(node(y,t1,t2),ys,ts,x) = [0 1 1] [0 1 1] [1 0 0] [0 1 0] [0 1 1] [0 1 0] [2]
[1 1 2] t1 + [0 2 1] t2 + [1 1 1] ts + [0 1 1] x + [0 2 1] y + [1 1 0] ys + [3]
[1 0 1] [0 1 0] [1 1 0] [0 1 0] [0 1 0] [0 1 1] [2]
>= [0 1 1] [0 1 1] [1 0 0] [0 1 0] [0 1 1] [0 1 0] [2]
[0 1 0] t1 + [0 1 1] t2 + [1 0 0] ts + [0 1 0] x + [0 0 0] y + [0 0 0] ys + [2]
[0 0 0] [0 0 0] [0 0 0] [0 0 0] [0 0 0] [0 0 0] [0]
= c_9(bfs#4#(eq(x,y),ys,t1,t2,ts,x,y))
bfs#4#(#false(),ys,t1,t2,ts,x,y) = [0 1 1] [0 1 1] [1 0 0] [0 1 0] [0 1 1] [0 1 0] [2]
[0 1 0] t1 + [0 1 1] t2 + [1 0 0] ts + [0 1 0] x + [0 0 0] y + [0 0 0] ys + [2]
[0 0 0] [0 1 0] [0 0 0] [0 0 1] [0 0 0] [0 0 0] [0]
>= [0 1 1] [0 1 1] [1 0 0] [0 1 0] [0 1 0] [2]
[0 0 0] t1 + [0 0 0] t2 + [0 0 0] ts + [0 0 0] x + [0 0 0] ys + [1]
[0 0 0] [0 0 0] [0 0 0] [0 0 0] [0 0 0] [0]
= c_10(bfs#(ts,::(t2,::(t1,ys)),x))
bfs#4#(#true(),ys,t1,t2,ts,x,y) = [0 1 1] [0 1 1] [1 0 0] [0 1 0] [0 1 1] [0 1 0] [1]
[0 1 0] t1 + [0 1 1] t2 + [1 0 0] ts + [0 1 0] x + [0 0 0] y + [0 0 0] ys + [1]
[0 0 0] [0 1 0] [0 0 0] [0 0 1] [0 0 0] [0 0 0] [0]
>= [1]
[1]
[0]
= c_11()
dobfs#(t,x) = [0 1 1] [1 1 1] [1]
[1 1 1] t + [0 1 0] x + [1]
[1 0 0] [0 0 0] [0]
>= [0 1 1] [1 1 0] [1]
[0 1 1] t + [0 1 0] x + [0]
[0 0 0] [0 0 0] [0]
= c_12(bfs#(::(t,nil()),nil(),x))
eq#(x,y) = [0 1 0] [0 1 0] [1]
[0 0 0] x + [0 0 1] y + [1]
[1 1 1] [0 0 0] [0]
>= [0]
[0]
[0]
= c_15()
eq#(0(),0()) = [1]
[2]
[2]
>= [0]
[0]
[0]
= c_16()
eq#(s(x),s(y)) = [0 1 1] [0 1 1] [3]
[0 0 0] x + [0 0 0] y + [2]
[1 1 2] [0 0 0] [3]
>= [0 1 0] [0 1 1] [2]
[0 0 0] x + [0 0 0] y + [0]
[1 1 1] [0 0 0] [0]
= c_17(eq#(x,y))
main#(t,x) = [1 1 1] [1 1 1] [1]
[0 0 0] t + [0 1 0] x + [0]
[0 1 0] [0 0 1] [0]
>= [1 1 1] [1 1 1] [1]
[0 0 0] t + [0 0 0] x + [0]
[0 0 0] [0 0 0] [0]
= c_13(dobfs#(t,x))
reverse#(xs) = [1 1 1] [1]
[1 0 0] xs + [0]
[1 1 1] [1]
>= [0 0 0] [1]
[0 0 0] xs + [0]
[1 1 0] [1]
= c_14(appendreverse#(xs,nil()))
appendreverse(nil(),ys) = [1 0 0] [0]
[1 1 0] ys + [0]
[0 0 1] [0]
>= [1 0 0] [0]
[0 1 0] ys + [0]
[0 0 1] [0]
= ys
eq(x,y) = [0 0 0] [1]
[1 0 0] x + [0]
[0 0 0] [0]
>= [1]
[0]
[0]
= #false()
eq(0(),0()) = [1]
[1]
[0]
>= [0]
[0]
[0]
= #true()
eq(s(x),s(y)) = [0 0 0] [1]
[1 0 1] x + [1]
[0 0 0] [0]
>= [0 0 0] [1]
[1 0 0] x + [0]
[0 0 0] [0]
= eq(x,y)
reverse(xs) = [0 1 0] [0]
[1 1 0] xs + [0]
[1 0 0] [1]
>= [0 1 0] [0]
[1 1 0] xs + [0]
[0 0 0] [1]
= appendreverse(xs,nil())
* Step 13: EmptyProcessor WORST_CASE(?,O(1))
+ Considered Problem:
- Weak DPs:
appendreverse#(::(x,xs),ys) -> c_1(appendreverse#(xs,::(x,ys)))
appendreverse#(nil(),ys) -> c_2()
bfs#(xs,ys,x) -> c_3(bfs#1#(xs,ys,x))
bfs#1#(::(t,ts),ys,x) -> c_4(bfs#3#(t,ys,ts,x))
bfs#1#(nil(),ys,x) -> c_5(bfs#2#(ys,x))
bfs#2#(::(t,ts),x) -> c_6(bfs#(reverse(::(t,ts)),nil(),x))
bfs#2#(nil(),x) -> c_7()
bfs#3#(leaf(),ys,ts,x) -> c_8(bfs#(ts,ys,x))
bfs#3#(node(y,t1,t2),ys,ts,x) -> c_9(bfs#4#(eq(x,y),ys,t1,t2,ts,x,y))
bfs#4#(#false(),ys,t1,t2,ts,x,y) -> c_10(bfs#(ts,::(t2,::(t1,ys)),x))
bfs#4#(#true(),ys,t1,t2,ts,x,y) -> c_11()
dobfs#(t,x) -> c_12(bfs#(::(t,nil()),nil(),x))
eq#(x,y) -> c_15()
eq#(0(),0()) -> c_16()
eq#(s(x),s(y)) -> c_17(eq#(x,y))
main#(t,x) -> c_13(dobfs#(t,x))
reverse#(xs) -> c_14(appendreverse#(xs,nil()))
- Weak TRS:
appendreverse(::(x,xs),ys) -> appendreverse(xs,::(x,ys))
appendreverse(nil(),ys) -> ys
eq(x,y) -> #false()
eq(0(),0()) -> #true()
eq(s(x),s(y)) -> eq(x,y)
reverse(xs) -> appendreverse(xs,nil())
- Signature:
{appendreverse/2,bfs/3,bfs#1/3,bfs#2/2,bfs#3/4,bfs#4/7,dobfs/2,eq/2,main/2,reverse/1,appendreverse#/2,bfs#/3
,bfs#1#/3,bfs#2#/2,bfs#3#/4,bfs#4#/7,dobfs#/2,eq#/2,main#/2,reverse#/1} / {#false/0,#true/0,0/0,::/2,leaf/0
,nil/0,node/3,s/1,c_1/1,c_2/0,c_3/1,c_4/1,c_5/1,c_6/1,c_7/0,c_8/1,c_9/1,c_10/1,c_11/0,c_12/1,c_13/1,c_14/1
,c_15/0,c_16/0,c_17/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {appendreverse#,bfs#,bfs#1#,bfs#2#,bfs#3#,bfs#4#,dobfs#
,eq#,main#,reverse#} and constructors {#false,#true,0,::,leaf,nil,node,s}
+ Applied Processor:
EmptyProcessor
+ Details:
The problem is already closed. The intended complexity is O(1).
WORST_CASE(?,O(n^2))