WORST_CASE(?,O(n^1))
* Step 1: WeightGap WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict TRS:
f(0(),y,0(),u) -> true()
f(0(),y,s(z),u) -> false()
f(s(x),0(),z,u) -> f(x,u,minus(z,s(x)),u)
f(s(x),s(y),z,u) -> if(le(x,y),f(s(x),minus(y,x),z,u),f(x,u,z,u))
perfectp(0()) -> false()
perfectp(s(x)) -> f(x,s(0()),s(x),s(x))
- Signature:
{f/4,perfectp/1} / {0/0,false/0,if/3,le/2,minus/2,s/1,true/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {f,perfectp} and constructors {0,false,if,le,minus,s,true}
+ 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(if) = {3}
Following symbols are considered usable:
all
TcT has computed the following interpretation:
p(0) = [1]
p(f) = [12] x3 + [0]
p(false) = [0]
p(if) = [1] x3 + [0]
p(le) = [1] x1 + [1] x2 + [0]
p(minus) = [1] x1 + [1] x2 + [0]
p(perfectp) = [3]
p(s) = [0]
p(true) = [0]
Following rules are strictly oriented:
f(0(),y,0(),u) = [12]
> [0]
= true()
perfectp(0()) = [3]
> [0]
= false()
perfectp(s(x)) = [3]
> [0]
= f(x,s(0()),s(x),s(x))
Following rules are (at-least) weakly oriented:
f(0(),y,s(z),u) = [0]
>= [0]
= false()
f(s(x),0(),z,u) = [12] z + [0]
>= [12] z + [0]
= f(x,u,minus(z,s(x)),u)
f(s(x),s(y),z,u) = [12] z + [0]
>= [12] z + [0]
= if(le(x,y),f(s(x),minus(y,x),z,u),f(x,u,z,u))
Further, it can be verified that all rules not oriented are covered by the weightgap condition.
* Step 2: NaturalMI WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict TRS:
f(0(),y,s(z),u) -> false()
f(s(x),0(),z,u) -> f(x,u,minus(z,s(x)),u)
f(s(x),s(y),z,u) -> if(le(x,y),f(s(x),minus(y,x),z,u),f(x,u,z,u))
- Weak TRS:
f(0(),y,0(),u) -> true()
perfectp(0()) -> false()
perfectp(s(x)) -> f(x,s(0()),s(x),s(x))
- Signature:
{f/4,perfectp/1} / {0/0,false/0,if/3,le/2,minus/2,s/1,true/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {f,perfectp} and constructors {0,false,if,le,minus,s,true}
+ Applied Processor:
NaturalMI {miDimension = 1, 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:
The following argument positions are considered usable:
uargs(if) = {3}
Following symbols are considered usable:
{f,perfectp}
TcT has computed the following interpretation:
p(0) = [0]
p(f) = [5]
p(false) = [4]
p(if) = [1] x3 + [0]
p(le) = [0]
p(minus) = [10]
p(perfectp) = [8]
p(s) = [14]
p(true) = [5]
Following rules are strictly oriented:
f(0(),y,s(z),u) = [5]
> [4]
= false()
Following rules are (at-least) weakly oriented:
f(0(),y,0(),u) = [5]
>= [5]
= true()
f(s(x),0(),z,u) = [5]
>= [5]
= f(x,u,minus(z,s(x)),u)
f(s(x),s(y),z,u) = [5]
>= [5]
= if(le(x,y),f(s(x),minus(y,x),z,u),f(x,u,z,u))
perfectp(0()) = [8]
>= [4]
= false()
perfectp(s(x)) = [8]
>= [5]
= f(x,s(0()),s(x),s(x))
* Step 3: NaturalMI WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict TRS:
f(s(x),0(),z,u) -> f(x,u,minus(z,s(x)),u)
f(s(x),s(y),z,u) -> if(le(x,y),f(s(x),minus(y,x),z,u),f(x,u,z,u))
- Weak TRS:
f(0(),y,0(),u) -> true()
f(0(),y,s(z),u) -> false()
perfectp(0()) -> false()
perfectp(s(x)) -> f(x,s(0()),s(x),s(x))
- Signature:
{f/4,perfectp/1} / {0/0,false/0,if/3,le/2,minus/2,s/1,true/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {f,perfectp} and constructors {0,false,if,le,minus,s,true}
+ Applied Processor:
NaturalMI {miDimension = 1, 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:
The following argument positions are considered usable:
uargs(if) = {3}
Following symbols are considered usable:
{f,perfectp}
TcT has computed the following interpretation:
p(0) = [2]
p(f) = [7] x1 + [0]
p(false) = [14]
p(if) = [1] x1 + [1] x3 + [12]
p(le) = [0]
p(minus) = [0]
p(perfectp) = [8] x1 + [1]
p(s) = [1] x1 + [3]
p(true) = [0]
Following rules are strictly oriented:
f(s(x),0(),z,u) = [7] x + [21]
> [7] x + [0]
= f(x,u,minus(z,s(x)),u)
f(s(x),s(y),z,u) = [7] x + [21]
> [7] x + [12]
= if(le(x,y),f(s(x),minus(y,x),z,u),f(x,u,z,u))
Following rules are (at-least) weakly oriented:
f(0(),y,0(),u) = [14]
>= [0]
= true()
f(0(),y,s(z),u) = [14]
>= [14]
= false()
perfectp(0()) = [17]
>= [14]
= false()
perfectp(s(x)) = [8] x + [25]
>= [7] x + [0]
= f(x,s(0()),s(x),s(x))
* Step 4: EmptyProcessor WORST_CASE(?,O(1))
+ Considered Problem:
- Weak TRS:
f(0(),y,0(),u) -> true()
f(0(),y,s(z),u) -> false()
f(s(x),0(),z,u) -> f(x,u,minus(z,s(x)),u)
f(s(x),s(y),z,u) -> if(le(x,y),f(s(x),minus(y,x),z,u),f(x,u,z,u))
perfectp(0()) -> false()
perfectp(s(x)) -> f(x,s(0()),s(x),s(x))
- Signature:
{f/4,perfectp/1} / {0/0,false/0,if/3,le/2,minus/2,s/1,true/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {f,perfectp} and constructors {0,false,if,le,minus,s,true}
+ Applied Processor:
EmptyProcessor
+ Details:
The problem is already closed. The intended complexity is O(1).
WORST_CASE(?,O(n^1))