* Step 1: Sum WORST_CASE(Omega(n^1),O(n^2))
+ Considered Problem:
- Strict TRS:
choice(cons(x,xs)) -> x
choice(cons(x,xs)) -> choice(xs)
eq(0(x),1(y)) -> false()
eq(1(x),0(y)) -> false()
eq(1(x),1(y)) -> eq(x,y)
eq(O(x),0(y)) -> eq(x,y)
eq(nil(),nil()) -> true()
guess(cons(clause,cnf)) -> cons(choice(clause),guess(cnf))
guess(nil()) -> nil()
if(false(),t,e) -> e
if(true(),t,e) -> t
member(x,cons(y,ys)) -> if(eq(x,y),true(),member(x,ys))
member(x,nil()) -> false()
negate(0(x)) -> 1(x)
negate(1(x)) -> 0(x)
sat(cnf) -> satck(cnf,guess(cnf))
satck(cnf,assign) -> if(verify(assign),assign,unsat())
verify(cons(l,ls)) -> if(member(negate(l),ls),false(),verify(ls))
verify(nil()) -> true()
- Signature:
{choice/1,eq/2,guess/1,if/3,member/2,negate/1,sat/1,satck/2,verify/1} / {0/1,1/1,O/1,cons/2,false/0,nil/0
,true/0,unsat/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {choice,eq,guess,if,member,negate,sat,satck
,verify} and constructors {0,1,O,cons,false,nil,true,unsat}
+ Applied Processor:
Sum {left = someStrategy, right = someStrategy}
+ Details:
()
** Step 1.a:1: DecreasingLoops WORST_CASE(Omega(n^1),?)
+ Considered Problem:
- Strict TRS:
choice(cons(x,xs)) -> x
choice(cons(x,xs)) -> choice(xs)
eq(0(x),1(y)) -> false()
eq(1(x),0(y)) -> false()
eq(1(x),1(y)) -> eq(x,y)
eq(O(x),0(y)) -> eq(x,y)
eq(nil(),nil()) -> true()
guess(cons(clause,cnf)) -> cons(choice(clause),guess(cnf))
guess(nil()) -> nil()
if(false(),t,e) -> e
if(true(),t,e) -> t
member(x,cons(y,ys)) -> if(eq(x,y),true(),member(x,ys))
member(x,nil()) -> false()
negate(0(x)) -> 1(x)
negate(1(x)) -> 0(x)
sat(cnf) -> satck(cnf,guess(cnf))
satck(cnf,assign) -> if(verify(assign),assign,unsat())
verify(cons(l,ls)) -> if(member(negate(l),ls),false(),verify(ls))
verify(nil()) -> true()
- Signature:
{choice/1,eq/2,guess/1,if/3,member/2,negate/1,sat/1,satck/2,verify/1} / {0/1,1/1,O/1,cons/2,false/0,nil/0
,true/0,unsat/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {choice,eq,guess,if,member,negate,sat,satck
,verify} and constructors {0,1,O,cons,false,nil,true,unsat}
+ Applied Processor:
DecreasingLoops {bound = AnyLoop, narrow = 10}
+ Details:
The system has following decreasing Loops:
choice(y){y -> cons(x,y)} =
choice(cons(x,y)) ->^+ choice(y)
= C[choice(y) = choice(y){}]
** Step 1.b:1: WeightGap WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict TRS:
choice(cons(x,xs)) -> x
choice(cons(x,xs)) -> choice(xs)
eq(0(x),1(y)) -> false()
eq(1(x),0(y)) -> false()
eq(1(x),1(y)) -> eq(x,y)
eq(O(x),0(y)) -> eq(x,y)
eq(nil(),nil()) -> true()
guess(cons(clause,cnf)) -> cons(choice(clause),guess(cnf))
guess(nil()) -> nil()
if(false(),t,e) -> e
if(true(),t,e) -> t
member(x,cons(y,ys)) -> if(eq(x,y),true(),member(x,ys))
member(x,nil()) -> false()
negate(0(x)) -> 1(x)
negate(1(x)) -> 0(x)
sat(cnf) -> satck(cnf,guess(cnf))
satck(cnf,assign) -> if(verify(assign),assign,unsat())
verify(cons(l,ls)) -> if(member(negate(l),ls),false(),verify(ls))
verify(nil()) -> true()
- Signature:
{choice/1,eq/2,guess/1,if/3,member/2,negate/1,sat/1,satck/2,verify/1} / {0/1,1/1,O/1,cons/2,false/0,nil/0
,true/0,unsat/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {choice,eq,guess,if,member,negate,sat,satck
,verify} and constructors {0,1,O,cons,false,nil,true,unsat}
+ Applied Processor:
WeightGap {wgDimension = 1, wgDegree = 1, 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(cons) = {1,2},
uargs(if) = {1,3},
uargs(member) = {1},
uargs(satck) = {2}
Following symbols are considered usable:
all
TcT has computed the following interpretation:
p(0) = [0]
p(1) = [0]
p(O) = [0]
p(choice) = [2] x1 + [0]
p(cons) = [1] x1 + [1] x2 + [0]
p(eq) = [3]
p(false) = [1]
p(guess) = [3] x1 + [5]
p(if) = [1] x1 + [1] x2 + [1] x3 + [6]
p(member) = [1] x1 + [2]
p(negate) = [4]
p(nil) = [1]
p(sat) = [7] x1 + [0]
p(satck) = [4] x1 + [1] x2 + [0]
p(true) = [0]
p(unsat) = [0]
p(verify) = [0]
Following rules are strictly oriented:
eq(0(x),1(y)) = [3]
> [1]
= false()
eq(1(x),0(y)) = [3]
> [1]
= false()
eq(nil(),nil()) = [3]
> [0]
= true()
guess(nil()) = [8]
> [1]
= nil()
if(false(),t,e) = [1] e + [1] t + [7]
> [1] e + [0]
= e
if(true(),t,e) = [1] e + [1] t + [6]
> [1] t + [0]
= t
member(x,nil()) = [1] x + [2]
> [1]
= false()
negate(0(x)) = [4]
> [0]
= 1(x)
negate(1(x)) = [4]
> [0]
= 0(x)
Following rules are (at-least) weakly oriented:
choice(cons(x,xs)) = [2] x + [2] xs + [0]
>= [1] x + [0]
= x
choice(cons(x,xs)) = [2] x + [2] xs + [0]
>= [2] xs + [0]
= choice(xs)
eq(1(x),1(y)) = [3]
>= [3]
= eq(x,y)
eq(O(x),0(y)) = [3]
>= [3]
= eq(x,y)
guess(cons(clause,cnf)) = [3] clause + [3] cnf + [5]
>= [2] clause + [3] cnf + [5]
= cons(choice(clause),guess(cnf))
member(x,cons(y,ys)) = [1] x + [2]
>= [1] x + [11]
= if(eq(x,y),true(),member(x,ys))
sat(cnf) = [7] cnf + [0]
>= [7] cnf + [5]
= satck(cnf,guess(cnf))
satck(cnf,assign) = [1] assign + [4] cnf + [0]
>= [1] assign + [6]
= if(verify(assign),assign,unsat())
verify(cons(l,ls)) = [0]
>= [13]
= if(member(negate(l),ls),false(),verify(ls))
verify(nil()) = [0]
>= [0]
= true()
Further, it can be verified that all rules not oriented are covered by the weightgap condition.
** Step 1.b:2: WeightGap WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict TRS:
choice(cons(x,xs)) -> x
choice(cons(x,xs)) -> choice(xs)
eq(1(x),1(y)) -> eq(x,y)
eq(O(x),0(y)) -> eq(x,y)
guess(cons(clause,cnf)) -> cons(choice(clause),guess(cnf))
member(x,cons(y,ys)) -> if(eq(x,y),true(),member(x,ys))
sat(cnf) -> satck(cnf,guess(cnf))
satck(cnf,assign) -> if(verify(assign),assign,unsat())
verify(cons(l,ls)) -> if(member(negate(l),ls),false(),verify(ls))
verify(nil()) -> true()
- Weak TRS:
eq(0(x),1(y)) -> false()
eq(1(x),0(y)) -> false()
eq(nil(),nil()) -> true()
guess(nil()) -> nil()
if(false(),t,e) -> e
if(true(),t,e) -> t
member(x,nil()) -> false()
negate(0(x)) -> 1(x)
negate(1(x)) -> 0(x)
- Signature:
{choice/1,eq/2,guess/1,if/3,member/2,negate/1,sat/1,satck/2,verify/1} / {0/1,1/1,O/1,cons/2,false/0,nil/0
,true/0,unsat/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {choice,eq,guess,if,member,negate,sat,satck
,verify} and constructors {0,1,O,cons,false,nil,true,unsat}
+ Applied Processor:
WeightGap {wgDimension = 1, wgDegree = 1, 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(cons) = {1,2},
uargs(if) = {1,3},
uargs(member) = {1},
uargs(satck) = {2}
Following symbols are considered usable:
all
TcT has computed the following interpretation:
p(0) = [0]
p(1) = [0]
p(O) = [1] x1 + [0]
p(choice) = [4] x1 + [0]
p(cons) = [1] x1 + [1] x2 + [0]
p(eq) = [0]
p(false) = [0]
p(guess) = [4] x1 + [0]
p(if) = [1] x1 + [1] x2 + [1] x3 + [0]
p(member) = [1] x1 + [0]
p(negate) = [0]
p(nil) = [0]
p(sat) = [4] x1 + [0]
p(satck) = [1] x2 + [4]
p(true) = [0]
p(unsat) = [0]
p(verify) = [3]
Following rules are strictly oriented:
satck(cnf,assign) = [1] assign + [4]
> [1] assign + [3]
= if(verify(assign),assign,unsat())
verify(nil()) = [3]
> [0]
= true()
Following rules are (at-least) weakly oriented:
choice(cons(x,xs)) = [4] x + [4] xs + [0]
>= [1] x + [0]
= x
choice(cons(x,xs)) = [4] x + [4] xs + [0]
>= [4] xs + [0]
= choice(xs)
eq(0(x),1(y)) = [0]
>= [0]
= false()
eq(1(x),0(y)) = [0]
>= [0]
= false()
eq(1(x),1(y)) = [0]
>= [0]
= eq(x,y)
eq(O(x),0(y)) = [0]
>= [0]
= eq(x,y)
eq(nil(),nil()) = [0]
>= [0]
= true()
guess(cons(clause,cnf)) = [4] clause + [4] cnf + [0]
>= [4] clause + [4] cnf + [0]
= cons(choice(clause),guess(cnf))
guess(nil()) = [0]
>= [0]
= nil()
if(false(),t,e) = [1] e + [1] t + [0]
>= [1] e + [0]
= e
if(true(),t,e) = [1] e + [1] t + [0]
>= [1] t + [0]
= t
member(x,cons(y,ys)) = [1] x + [0]
>= [1] x + [0]
= if(eq(x,y),true(),member(x,ys))
member(x,nil()) = [1] x + [0]
>= [0]
= false()
negate(0(x)) = [0]
>= [0]
= 1(x)
negate(1(x)) = [0]
>= [0]
= 0(x)
sat(cnf) = [4] cnf + [0]
>= [4] cnf + [4]
= satck(cnf,guess(cnf))
verify(cons(l,ls)) = [3]
>= [3]
= if(member(negate(l),ls),false(),verify(ls))
Further, it can be verified that all rules not oriented are covered by the weightgap condition.
** Step 1.b:3: WeightGap WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict TRS:
choice(cons(x,xs)) -> x
choice(cons(x,xs)) -> choice(xs)
eq(1(x),1(y)) -> eq(x,y)
eq(O(x),0(y)) -> eq(x,y)
guess(cons(clause,cnf)) -> cons(choice(clause),guess(cnf))
member(x,cons(y,ys)) -> if(eq(x,y),true(),member(x,ys))
sat(cnf) -> satck(cnf,guess(cnf))
verify(cons(l,ls)) -> if(member(negate(l),ls),false(),verify(ls))
- Weak TRS:
eq(0(x),1(y)) -> false()
eq(1(x),0(y)) -> false()
eq(nil(),nil()) -> true()
guess(nil()) -> nil()
if(false(),t,e) -> e
if(true(),t,e) -> t
member(x,nil()) -> false()
negate(0(x)) -> 1(x)
negate(1(x)) -> 0(x)
satck(cnf,assign) -> if(verify(assign),assign,unsat())
verify(nil()) -> true()
- Signature:
{choice/1,eq/2,guess/1,if/3,member/2,negate/1,sat/1,satck/2,verify/1} / {0/1,1/1,O/1,cons/2,false/0,nil/0
,true/0,unsat/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {choice,eq,guess,if,member,negate,sat,satck
,verify} and constructors {0,1,O,cons,false,nil,true,unsat}
+ Applied Processor:
WeightGap {wgDimension = 1, wgDegree = 1, 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(cons) = {1,2},
uargs(if) = {1,3},
uargs(member) = {1},
uargs(satck) = {2}
Following symbols are considered usable:
all
TcT has computed the following interpretation:
p(0) = [0]
p(1) = [0]
p(O) = [0]
p(choice) = [1] x1 + [6]
p(cons) = [1] x1 + [1] x2 + [2]
p(eq) = [5]
p(false) = [0]
p(guess) = [1] x1 + [0]
p(if) = [1] x1 + [1] x2 + [1] x3 + [0]
p(member) = [1] x1 + [3]
p(negate) = [0]
p(nil) = [1]
p(sat) = [2] x1 + [1]
p(satck) = [1] x1 + [1] x2 + [6]
p(true) = [5]
p(unsat) = [1]
p(verify) = [5]
Following rules are strictly oriented:
choice(cons(x,xs)) = [1] x + [1] xs + [8]
> [1] x + [0]
= x
choice(cons(x,xs)) = [1] x + [1] xs + [8]
> [1] xs + [6]
= choice(xs)
Following rules are (at-least) weakly oriented:
eq(0(x),1(y)) = [5]
>= [0]
= false()
eq(1(x),0(y)) = [5]
>= [0]
= false()
eq(1(x),1(y)) = [5]
>= [5]
= eq(x,y)
eq(O(x),0(y)) = [5]
>= [5]
= eq(x,y)
eq(nil(),nil()) = [5]
>= [5]
= true()
guess(cons(clause,cnf)) = [1] clause + [1] cnf + [2]
>= [1] clause + [1] cnf + [8]
= cons(choice(clause),guess(cnf))
guess(nil()) = [1]
>= [1]
= nil()
if(false(),t,e) = [1] e + [1] t + [0]
>= [1] e + [0]
= e
if(true(),t,e) = [1] e + [1] t + [5]
>= [1] t + [0]
= t
member(x,cons(y,ys)) = [1] x + [3]
>= [1] x + [13]
= if(eq(x,y),true(),member(x,ys))
member(x,nil()) = [1] x + [3]
>= [0]
= false()
negate(0(x)) = [0]
>= [0]
= 1(x)
negate(1(x)) = [0]
>= [0]
= 0(x)
sat(cnf) = [2] cnf + [1]
>= [2] cnf + [6]
= satck(cnf,guess(cnf))
satck(cnf,assign) = [1] assign + [1] cnf + [6]
>= [1] assign + [6]
= if(verify(assign),assign,unsat())
verify(cons(l,ls)) = [5]
>= [8]
= if(member(negate(l),ls),false(),verify(ls))
verify(nil()) = [5]
>= [5]
= true()
Further, it can be verified that all rules not oriented are covered by the weightgap condition.
** Step 1.b:4: WeightGap WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict TRS:
eq(1(x),1(y)) -> eq(x,y)
eq(O(x),0(y)) -> eq(x,y)
guess(cons(clause,cnf)) -> cons(choice(clause),guess(cnf))
member(x,cons(y,ys)) -> if(eq(x,y),true(),member(x,ys))
sat(cnf) -> satck(cnf,guess(cnf))
verify(cons(l,ls)) -> if(member(negate(l),ls),false(),verify(ls))
- Weak TRS:
choice(cons(x,xs)) -> x
choice(cons(x,xs)) -> choice(xs)
eq(0(x),1(y)) -> false()
eq(1(x),0(y)) -> false()
eq(nil(),nil()) -> true()
guess(nil()) -> nil()
if(false(),t,e) -> e
if(true(),t,e) -> t
member(x,nil()) -> false()
negate(0(x)) -> 1(x)
negate(1(x)) -> 0(x)
satck(cnf,assign) -> if(verify(assign),assign,unsat())
verify(nil()) -> true()
- Signature:
{choice/1,eq/2,guess/1,if/3,member/2,negate/1,sat/1,satck/2,verify/1} / {0/1,1/1,O/1,cons/2,false/0,nil/0
,true/0,unsat/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {choice,eq,guess,if,member,negate,sat,satck
,verify} and constructors {0,1,O,cons,false,nil,true,unsat}
+ Applied Processor:
WeightGap {wgDimension = 1, wgDegree = 1, 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(cons) = {1,2},
uargs(if) = {1,3},
uargs(member) = {1},
uargs(satck) = {2}
Following symbols are considered usable:
all
TcT has computed the following interpretation:
p(0) = [0]
p(1) = [0]
p(O) = [0]
p(choice) = [4] x1 + [1]
p(cons) = [1] x1 + [1] x2 + [2]
p(eq) = [0]
p(false) = [0]
p(guess) = [4] x1 + [3]
p(if) = [1] x1 + [1] x2 + [1] x3 + [1]
p(member) = [1] x1 + [0]
p(negate) = [0]
p(nil) = [2]
p(sat) = [4] x1 + [1]
p(satck) = [1] x2 + [1]
p(true) = [0]
p(unsat) = [0]
p(verify) = [0]
Following rules are strictly oriented:
guess(cons(clause,cnf)) = [4] clause + [4] cnf + [11]
> [4] clause + [4] cnf + [6]
= cons(choice(clause),guess(cnf))
Following rules are (at-least) weakly oriented:
choice(cons(x,xs)) = [4] x + [4] xs + [9]
>= [1] x + [0]
= x
choice(cons(x,xs)) = [4] x + [4] xs + [9]
>= [4] xs + [1]
= choice(xs)
eq(0(x),1(y)) = [0]
>= [0]
= false()
eq(1(x),0(y)) = [0]
>= [0]
= false()
eq(1(x),1(y)) = [0]
>= [0]
= eq(x,y)
eq(O(x),0(y)) = [0]
>= [0]
= eq(x,y)
eq(nil(),nil()) = [0]
>= [0]
= true()
guess(nil()) = [11]
>= [2]
= nil()
if(false(),t,e) = [1] e + [1] t + [1]
>= [1] e + [0]
= e
if(true(),t,e) = [1] e + [1] t + [1]
>= [1] t + [0]
= t
member(x,cons(y,ys)) = [1] x + [0]
>= [1] x + [1]
= if(eq(x,y),true(),member(x,ys))
member(x,nil()) = [1] x + [0]
>= [0]
= false()
negate(0(x)) = [0]
>= [0]
= 1(x)
negate(1(x)) = [0]
>= [0]
= 0(x)
sat(cnf) = [4] cnf + [1]
>= [4] cnf + [4]
= satck(cnf,guess(cnf))
satck(cnf,assign) = [1] assign + [1]
>= [1] assign + [1]
= if(verify(assign),assign,unsat())
verify(cons(l,ls)) = [0]
>= [1]
= if(member(negate(l),ls),false(),verify(ls))
verify(nil()) = [0]
>= [0]
= true()
Further, it can be verified that all rules not oriented are covered by the weightgap condition.
** Step 1.b:5: WeightGap WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict TRS:
eq(1(x),1(y)) -> eq(x,y)
eq(O(x),0(y)) -> eq(x,y)
member(x,cons(y,ys)) -> if(eq(x,y),true(),member(x,ys))
sat(cnf) -> satck(cnf,guess(cnf))
verify(cons(l,ls)) -> if(member(negate(l),ls),false(),verify(ls))
- Weak TRS:
choice(cons(x,xs)) -> x
choice(cons(x,xs)) -> choice(xs)
eq(0(x),1(y)) -> false()
eq(1(x),0(y)) -> false()
eq(nil(),nil()) -> true()
guess(cons(clause,cnf)) -> cons(choice(clause),guess(cnf))
guess(nil()) -> nil()
if(false(),t,e) -> e
if(true(),t,e) -> t
member(x,nil()) -> false()
negate(0(x)) -> 1(x)
negate(1(x)) -> 0(x)
satck(cnf,assign) -> if(verify(assign),assign,unsat())
verify(nil()) -> true()
- Signature:
{choice/1,eq/2,guess/1,if/3,member/2,negate/1,sat/1,satck/2,verify/1} / {0/1,1/1,O/1,cons/2,false/0,nil/0
,true/0,unsat/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {choice,eq,guess,if,member,negate,sat,satck
,verify} and constructors {0,1,O,cons,false,nil,true,unsat}
+ Applied Processor:
WeightGap {wgDimension = 1, wgDegree = 1, 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(cons) = {1,2},
uargs(if) = {1,3},
uargs(member) = {1},
uargs(satck) = {2}
Following symbols are considered usable:
all
TcT has computed the following interpretation:
p(0) = [0]
p(1) = [0]
p(O) = [1] x1 + [0]
p(choice) = [1] x1 + [0]
p(cons) = [1] x1 + [1] x2 + [2]
p(eq) = [0]
p(false) = [0]
p(guess) = [1] x1 + [0]
p(if) = [1] x1 + [1] x2 + [1] x3 + [2]
p(member) = [1] x1 + [0]
p(negate) = [7]
p(nil) = [0]
p(sat) = [2] x1 + [5]
p(satck) = [1] x1 + [1] x2 + [4]
p(true) = [0]
p(unsat) = [0]
p(verify) = [0]
Following rules are strictly oriented:
sat(cnf) = [2] cnf + [5]
> [2] cnf + [4]
= satck(cnf,guess(cnf))
Following rules are (at-least) weakly oriented:
choice(cons(x,xs)) = [1] x + [1] xs + [2]
>= [1] x + [0]
= x
choice(cons(x,xs)) = [1] x + [1] xs + [2]
>= [1] xs + [0]
= choice(xs)
eq(0(x),1(y)) = [0]
>= [0]
= false()
eq(1(x),0(y)) = [0]
>= [0]
= false()
eq(1(x),1(y)) = [0]
>= [0]
= eq(x,y)
eq(O(x),0(y)) = [0]
>= [0]
= eq(x,y)
eq(nil(),nil()) = [0]
>= [0]
= true()
guess(cons(clause,cnf)) = [1] clause + [1] cnf + [2]
>= [1] clause + [1] cnf + [2]
= cons(choice(clause),guess(cnf))
guess(nil()) = [0]
>= [0]
= nil()
if(false(),t,e) = [1] e + [1] t + [2]
>= [1] e + [0]
= e
if(true(),t,e) = [1] e + [1] t + [2]
>= [1] t + [0]
= t
member(x,cons(y,ys)) = [1] x + [0]
>= [1] x + [2]
= if(eq(x,y),true(),member(x,ys))
member(x,nil()) = [1] x + [0]
>= [0]
= false()
negate(0(x)) = [7]
>= [0]
= 1(x)
negate(1(x)) = [7]
>= [0]
= 0(x)
satck(cnf,assign) = [1] assign + [1] cnf + [4]
>= [1] assign + [2]
= if(verify(assign),assign,unsat())
verify(cons(l,ls)) = [0]
>= [9]
= if(member(negate(l),ls),false(),verify(ls))
verify(nil()) = [0]
>= [0]
= true()
Further, it can be verified that all rules not oriented are covered by the weightgap condition.
** Step 1.b:6: MI WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict TRS:
eq(1(x),1(y)) -> eq(x,y)
eq(O(x),0(y)) -> eq(x,y)
member(x,cons(y,ys)) -> if(eq(x,y),true(),member(x,ys))
verify(cons(l,ls)) -> if(member(negate(l),ls),false(),verify(ls))
- Weak TRS:
choice(cons(x,xs)) -> x
choice(cons(x,xs)) -> choice(xs)
eq(0(x),1(y)) -> false()
eq(1(x),0(y)) -> false()
eq(nil(),nil()) -> true()
guess(cons(clause,cnf)) -> cons(choice(clause),guess(cnf))
guess(nil()) -> nil()
if(false(),t,e) -> e
if(true(),t,e) -> t
member(x,nil()) -> false()
negate(0(x)) -> 1(x)
negate(1(x)) -> 0(x)
sat(cnf) -> satck(cnf,guess(cnf))
satck(cnf,assign) -> if(verify(assign),assign,unsat())
verify(nil()) -> true()
- Signature:
{choice/1,eq/2,guess/1,if/3,member/2,negate/1,sat/1,satck/2,verify/1} / {0/1,1/1,O/1,cons/2,false/0,nil/0
,true/0,unsat/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {choice,eq,guess,if,member,negate,sat,satck
,verify} and constructors {0,1,O,cons,false,nil,true,unsat}
+ Applied Processor:
MI {miKind = MaximalMatrix (UpperTriangular (Multiplicity Nothing)), miDimension = 1, miUArgs = UArgs, miURules = URules, miSelector = Just any strict-rules}
+ Details:
We apply a matrix interpretation of kind MaximalMatrix (UpperTriangular (Multiplicity Nothing)):
The following argument positions are considered usable:
uargs(cons) = {1,2},
uargs(if) = {1,3},
uargs(member) = {1},
uargs(satck) = {2}
Following symbols are considered usable:
{choice,eq,guess,if,member,negate,sat,satck,verify}
TcT has computed the following interpretation:
p(0) = [0]
p(1) = [0]
p(O) = [1] x_1 + [4]
p(choice) = [1] x_1 + [1]
p(cons) = [1] x_1 + [1] x_2 + [8]
p(eq) = [0]
p(false) = [0]
p(guess) = [2] x_1 + [0]
p(if) = [2] x_1 + [2] x_2 + [1] x_3 + [0]
p(member) = [1] x_1 + [0]
p(negate) = [1] x_1 + [0]
p(nil) = [0]
p(sat) = [13] x_1 + [0]
p(satck) = [6] x_2 + [0]
p(true) = [0]
p(unsat) = [0]
p(verify) = [2] x_1 + [0]
Following rules are strictly oriented:
verify(cons(l,ls)) = [2] l + [2] ls + [16]
> [2] l + [2] ls + [0]
= if(member(negate(l),ls),false(),verify(ls))
Following rules are (at-least) weakly oriented:
choice(cons(x,xs)) = [1] x + [1] xs + [9]
>= [1] x + [0]
= x
choice(cons(x,xs)) = [1] x + [1] xs + [9]
>= [1] xs + [1]
= choice(xs)
eq(0(x),1(y)) = [0]
>= [0]
= false()
eq(1(x),0(y)) = [0]
>= [0]
= false()
eq(1(x),1(y)) = [0]
>= [0]
= eq(x,y)
eq(O(x),0(y)) = [0]
>= [0]
= eq(x,y)
eq(nil(),nil()) = [0]
>= [0]
= true()
guess(cons(clause,cnf)) = [2] clause + [2] cnf + [16]
>= [1] clause + [2] cnf + [9]
= cons(choice(clause),guess(cnf))
guess(nil()) = [0]
>= [0]
= nil()
if(false(),t,e) = [1] e + [2] t + [0]
>= [1] e + [0]
= e
if(true(),t,e) = [1] e + [2] t + [0]
>= [1] t + [0]
= t
member(x,cons(y,ys)) = [1] x + [0]
>= [1] x + [0]
= if(eq(x,y),true(),member(x,ys))
member(x,nil()) = [1] x + [0]
>= [0]
= false()
negate(0(x)) = [0]
>= [0]
= 1(x)
negate(1(x)) = [0]
>= [0]
= 0(x)
sat(cnf) = [13] cnf + [0]
>= [12] cnf + [0]
= satck(cnf,guess(cnf))
satck(cnf,assign) = [6] assign + [0]
>= [6] assign + [0]
= if(verify(assign),assign,unsat())
verify(nil()) = [0]
>= [0]
= true()
** Step 1.b:7: NaturalPI WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict TRS:
eq(1(x),1(y)) -> eq(x,y)
eq(O(x),0(y)) -> eq(x,y)
member(x,cons(y,ys)) -> if(eq(x,y),true(),member(x,ys))
- Weak TRS:
choice(cons(x,xs)) -> x
choice(cons(x,xs)) -> choice(xs)
eq(0(x),1(y)) -> false()
eq(1(x),0(y)) -> false()
eq(nil(),nil()) -> true()
guess(cons(clause,cnf)) -> cons(choice(clause),guess(cnf))
guess(nil()) -> nil()
if(false(),t,e) -> e
if(true(),t,e) -> t
member(x,nil()) -> false()
negate(0(x)) -> 1(x)
negate(1(x)) -> 0(x)
sat(cnf) -> satck(cnf,guess(cnf))
satck(cnf,assign) -> if(verify(assign),assign,unsat())
verify(cons(l,ls)) -> if(member(negate(l),ls),false(),verify(ls))
verify(nil()) -> true()
- Signature:
{choice/1,eq/2,guess/1,if/3,member/2,negate/1,sat/1,satck/2,verify/1} / {0/1,1/1,O/1,cons/2,false/0,nil/0
,true/0,unsat/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {choice,eq,guess,if,member,negate,sat,satck
,verify} and constructors {0,1,O,cons,false,nil,true,unsat}
+ Applied Processor:
NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just any strict-rules}
+ Details:
We apply a polynomial interpretation of kind constructor-based(mixed(2)):
The following argument positions are considered usable:
uargs(cons) = {1,2},
uargs(if) = {1,3},
uargs(member) = {1},
uargs(satck) = {2}
Following symbols are considered usable:
{choice,eq,guess,if,member,negate,sat,satck,verify}
TcT has computed the following interpretation:
p(0) = 0
p(1) = 0
p(O) = x1
p(choice) = x1
p(cons) = 1 + x1 + x2
p(eq) = 0
p(false) = 0
p(guess) = x1
p(if) = 2*x1 + x2 + x3
p(member) = 1 + 2*x1 + x2
p(negate) = 0
p(nil) = 0
p(sat) = 2 + 3*x1 + 3*x1^2
p(satck) = 1 + 3*x2 + 2*x2^2
p(true) = 0
p(unsat) = 0
p(verify) = x1 + x1^2
Following rules are strictly oriented:
member(x,cons(y,ys)) = 2 + 2*x + y + ys
> 1 + 2*x + ys
= if(eq(x,y),true(),member(x,ys))
Following rules are (at-least) weakly oriented:
choice(cons(x,xs)) = 1 + x + xs
>= x
= x
choice(cons(x,xs)) = 1 + x + xs
>= xs
= choice(xs)
eq(0(x),1(y)) = 0
>= 0
= false()
eq(1(x),0(y)) = 0
>= 0
= false()
eq(1(x),1(y)) = 0
>= 0
= eq(x,y)
eq(O(x),0(y)) = 0
>= 0
= eq(x,y)
eq(nil(),nil()) = 0
>= 0
= true()
guess(cons(clause,cnf)) = 1 + clause + cnf
>= 1 + clause + cnf
= cons(choice(clause),guess(cnf))
guess(nil()) = 0
>= 0
= nil()
if(false(),t,e) = e + t
>= e
= e
if(true(),t,e) = e + t
>= t
= t
member(x,nil()) = 1 + 2*x
>= 0
= false()
negate(0(x)) = 0
>= 0
= 1(x)
negate(1(x)) = 0
>= 0
= 0(x)
sat(cnf) = 2 + 3*cnf + 3*cnf^2
>= 1 + 3*cnf + 2*cnf^2
= satck(cnf,guess(cnf))
satck(cnf,assign) = 1 + 3*assign + 2*assign^2
>= 3*assign + 2*assign^2
= if(verify(assign),assign,unsat())
verify(cons(l,ls)) = 2 + 3*l + 2*l*ls + l^2 + 3*ls + ls^2
>= 2 + 3*ls + ls^2
= if(member(negate(l),ls),false(),verify(ls))
verify(nil()) = 0
>= 0
= true()
** Step 1.b:8: NaturalPI WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict TRS:
eq(1(x),1(y)) -> eq(x,y)
eq(O(x),0(y)) -> eq(x,y)
- Weak TRS:
choice(cons(x,xs)) -> x
choice(cons(x,xs)) -> choice(xs)
eq(0(x),1(y)) -> false()
eq(1(x),0(y)) -> false()
eq(nil(),nil()) -> true()
guess(cons(clause,cnf)) -> cons(choice(clause),guess(cnf))
guess(nil()) -> nil()
if(false(),t,e) -> e
if(true(),t,e) -> t
member(x,cons(y,ys)) -> if(eq(x,y),true(),member(x,ys))
member(x,nil()) -> false()
negate(0(x)) -> 1(x)
negate(1(x)) -> 0(x)
sat(cnf) -> satck(cnf,guess(cnf))
satck(cnf,assign) -> if(verify(assign),assign,unsat())
verify(cons(l,ls)) -> if(member(negate(l),ls),false(),verify(ls))
verify(nil()) -> true()
- Signature:
{choice/1,eq/2,guess/1,if/3,member/2,negate/1,sat/1,satck/2,verify/1} / {0/1,1/1,O/1,cons/2,false/0,nil/0
,true/0,unsat/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {choice,eq,guess,if,member,negate,sat,satck
,verify} and constructors {0,1,O,cons,false,nil,true,unsat}
+ Applied Processor:
NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just any strict-rules}
+ Details:
We apply a polynomial interpretation of kind constructor-based(mixed(2)):
The following argument positions are considered usable:
uargs(cons) = {1,2},
uargs(if) = {1,3},
uargs(member) = {1},
uargs(satck) = {2}
Following symbols are considered usable:
{choice,eq,guess,if,member,negate,sat,satck,verify}
TcT has computed the following interpretation:
p(0) = 1 + x1
p(1) = 1 + x1
p(O) = 0
p(choice) = x1
p(cons) = 1 + x1 + x2
p(eq) = x2
p(false) = 0
p(guess) = x1
p(if) = x1 + x2 + x3
p(member) = x1 + x2
p(negate) = x1^2
p(nil) = 0
p(sat) = 2 + 3*x1 + 3*x1^2
p(satck) = x1*x2 + 3*x2 + x2^2
p(true) = 0
p(unsat) = 0
p(verify) = 2*x1 + x1^2
Following rules are strictly oriented:
eq(1(x),1(y)) = 1 + y
> y
= eq(x,y)
eq(O(x),0(y)) = 1 + y
> y
= eq(x,y)
Following rules are (at-least) weakly oriented:
choice(cons(x,xs)) = 1 + x + xs
>= x
= x
choice(cons(x,xs)) = 1 + x + xs
>= xs
= choice(xs)
eq(0(x),1(y)) = 1 + y
>= 0
= false()
eq(1(x),0(y)) = 1 + y
>= 0
= false()
eq(nil(),nil()) = 0
>= 0
= true()
guess(cons(clause,cnf)) = 1 + clause + cnf
>= 1 + clause + cnf
= cons(choice(clause),guess(cnf))
guess(nil()) = 0
>= 0
= nil()
if(false(),t,e) = e + t
>= e
= e
if(true(),t,e) = e + t
>= t
= t
member(x,cons(y,ys)) = 1 + x + y + ys
>= x + y + ys
= if(eq(x,y),true(),member(x,ys))
member(x,nil()) = x
>= 0
= false()
negate(0(x)) = 1 + 2*x + x^2
>= 1 + x
= 1(x)
negate(1(x)) = 1 + 2*x + x^2
>= 1 + x
= 0(x)
sat(cnf) = 2 + 3*cnf + 3*cnf^2
>= 3*cnf + 2*cnf^2
= satck(cnf,guess(cnf))
satck(cnf,assign) = 3*assign + assign*cnf + assign^2
>= 3*assign + assign^2
= if(verify(assign),assign,unsat())
verify(cons(l,ls)) = 3 + 4*l + 2*l*ls + l^2 + 4*ls + ls^2
>= l^2 + 3*ls + ls^2
= if(member(negate(l),ls),false(),verify(ls))
verify(nil()) = 0
>= 0
= true()
** Step 1.b:9: EmptyProcessor WORST_CASE(?,O(1))
+ Considered Problem:
- Weak TRS:
choice(cons(x,xs)) -> x
choice(cons(x,xs)) -> choice(xs)
eq(0(x),1(y)) -> false()
eq(1(x),0(y)) -> false()
eq(1(x),1(y)) -> eq(x,y)
eq(O(x),0(y)) -> eq(x,y)
eq(nil(),nil()) -> true()
guess(cons(clause,cnf)) -> cons(choice(clause),guess(cnf))
guess(nil()) -> nil()
if(false(),t,e) -> e
if(true(),t,e) -> t
member(x,cons(y,ys)) -> if(eq(x,y),true(),member(x,ys))
member(x,nil()) -> false()
negate(0(x)) -> 1(x)
negate(1(x)) -> 0(x)
sat(cnf) -> satck(cnf,guess(cnf))
satck(cnf,assign) -> if(verify(assign),assign,unsat())
verify(cons(l,ls)) -> if(member(negate(l),ls),false(),verify(ls))
verify(nil()) -> true()
- Signature:
{choice/1,eq/2,guess/1,if/3,member/2,negate/1,sat/1,satck/2,verify/1} / {0/1,1/1,O/1,cons/2,false/0,nil/0
,true/0,unsat/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {choice,eq,guess,if,member,negate,sat,satck
,verify} and constructors {0,1,O,cons,false,nil,true,unsat}
+ Applied Processor:
EmptyProcessor
+ Details:
The problem is already closed. The intended complexity is O(1).
WORST_CASE(Omega(n^1),O(n^2))