*** 1 Progress [(O(1),O(n^3))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
ifMinus(false(),s(X),Y) -> s(minus(X,Y))
ifMinus(true(),s(X),Y) -> 0()
le(0(),Y) -> true()
le(s(X),0()) -> false()
le(s(X),s(Y)) -> le(X,Y)
minus(0(),Y) -> 0()
minus(s(X),Y) -> ifMinus(le(s(X),Y),s(X),Y)
quot(0(),s(Y)) -> 0()
quot(s(X),s(Y)) -> s(quot(minus(X,Y),s(Y)))
Weak DP Rules:
Weak TRS Rules:
Signature:
{ifMinus/3,le/2,minus/2,quot/2} / {0/0,false/0,s/1,true/0}
Obligation:
Innermost
basic terms: {ifMinus,le,minus,quot}/{0,false,s,true}
Applied Processor:
WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny}
Proof:
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(ifMinus) = {1},
uargs(quot) = {1},
uargs(s) = {1}
Following symbols are considered usable:
{}
TcT has computed the following interpretation:
p(0) = [7]
p(false) = [9]
p(ifMinus) = [1] x1 + [0]
p(le) = [0]
p(minus) = [5]
p(quot) = [1] x1 + [3] x2 + [0]
p(s) = [1] x1 + [3]
p(true) = [0]
Following rules are strictly oriented:
ifMinus(false(),s(X),Y) = [9]
> [8]
= s(minus(X,Y))
minus(s(X),Y) = [5]
> [0]
= ifMinus(le(s(X),Y),s(X),Y)
quot(0(),s(Y)) = [3] Y + [16]
> [7]
= 0()
Following rules are (at-least) weakly oriented:
ifMinus(true(),s(X),Y) = [0]
>= [7]
= 0()
le(0(),Y) = [0]
>= [0]
= true()
le(s(X),0()) = [0]
>= [9]
= false()
le(s(X),s(Y)) = [0]
>= [0]
= le(X,Y)
minus(0(),Y) = [5]
>= [7]
= 0()
quot(s(X),s(Y)) = [1] X + [3] Y + [12]
>= [3] Y + [17]
= s(quot(minus(X,Y),s(Y)))
Further, it can be verified that all rules not oriented are covered by the weightgap condition.
*** 1.1 Progress [(O(1),O(n^3))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
ifMinus(true(),s(X),Y) -> 0()
le(0(),Y) -> true()
le(s(X),0()) -> false()
le(s(X),s(Y)) -> le(X,Y)
minus(0(),Y) -> 0()
quot(s(X),s(Y)) -> s(quot(minus(X,Y),s(Y)))
Weak DP Rules:
Weak TRS Rules:
ifMinus(false(),s(X),Y) -> s(minus(X,Y))
minus(s(X),Y) -> ifMinus(le(s(X),Y),s(X),Y)
quot(0(),s(Y)) -> 0()
Signature:
{ifMinus/3,le/2,minus/2,quot/2} / {0/0,false/0,s/1,true/0}
Obligation:
Innermost
basic terms: {ifMinus,le,minus,quot}/{0,false,s,true}
Applied Processor:
WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny}
Proof:
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(ifMinus) = {1},
uargs(quot) = {1},
uargs(s) = {1}
Following symbols are considered usable:
{}
TcT has computed the following interpretation:
p(0) = [0]
p(false) = [4]
p(ifMinus) = [1] x1 + [1]
p(le) = [2]
p(minus) = [4]
p(quot) = [1] x1 + [0]
p(s) = [1] x1 + [0]
p(true) = [5]
Following rules are strictly oriented:
ifMinus(true(),s(X),Y) = [6]
> [0]
= 0()
minus(0(),Y) = [4]
> [0]
= 0()
Following rules are (at-least) weakly oriented:
ifMinus(false(),s(X),Y) = [5]
>= [4]
= s(minus(X,Y))
le(0(),Y) = [2]
>= [5]
= true()
le(s(X),0()) = [2]
>= [4]
= false()
le(s(X),s(Y)) = [2]
>= [2]
= le(X,Y)
minus(s(X),Y) = [4]
>= [3]
= ifMinus(le(s(X),Y),s(X),Y)
quot(0(),s(Y)) = [0]
>= [0]
= 0()
quot(s(X),s(Y)) = [1] X + [0]
>= [4]
= s(quot(minus(X,Y),s(Y)))
Further, it can be verified that all rules not oriented are covered by the weightgap condition.
*** 1.1.1 Progress [(O(1),O(n^3))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
le(0(),Y) -> true()
le(s(X),0()) -> false()
le(s(X),s(Y)) -> le(X,Y)
quot(s(X),s(Y)) -> s(quot(minus(X,Y),s(Y)))
Weak DP Rules:
Weak TRS Rules:
ifMinus(false(),s(X),Y) -> s(minus(X,Y))
ifMinus(true(),s(X),Y) -> 0()
minus(0(),Y) -> 0()
minus(s(X),Y) -> ifMinus(le(s(X),Y),s(X),Y)
quot(0(),s(Y)) -> 0()
Signature:
{ifMinus/3,le/2,minus/2,quot/2} / {0/0,false/0,s/1,true/0}
Obligation:
Innermost
basic terms: {ifMinus,le,minus,quot}/{0,false,s,true}
Applied Processor:
WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny}
Proof:
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(ifMinus) = {1},
uargs(quot) = {1},
uargs(s) = {1}
Following symbols are considered usable:
{}
TcT has computed the following interpretation:
p(0) = [0]
p(false) = [15]
p(ifMinus) = [1] x1 + [0]
p(le) = [14]
p(minus) = [15]
p(quot) = [1] x1 + [0]
p(s) = [1] x1 + [0]
p(true) = [0]
Following rules are strictly oriented:
le(0(),Y) = [14]
> [0]
= true()
Following rules are (at-least) weakly oriented:
ifMinus(false(),s(X),Y) = [15]
>= [15]
= s(minus(X,Y))
ifMinus(true(),s(X),Y) = [0]
>= [0]
= 0()
le(s(X),0()) = [14]
>= [15]
= false()
le(s(X),s(Y)) = [14]
>= [14]
= le(X,Y)
minus(0(),Y) = [15]
>= [0]
= 0()
minus(s(X),Y) = [15]
>= [14]
= ifMinus(le(s(X),Y),s(X),Y)
quot(0(),s(Y)) = [0]
>= [0]
= 0()
quot(s(X),s(Y)) = [1] X + [0]
>= [15]
= s(quot(minus(X,Y),s(Y)))
Further, it can be verified that all rules not oriented are covered by the weightgap condition.
*** 1.1.1.1 Progress [(O(1),O(n^3))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
le(s(X),0()) -> false()
le(s(X),s(Y)) -> le(X,Y)
quot(s(X),s(Y)) -> s(quot(minus(X,Y),s(Y)))
Weak DP Rules:
Weak TRS Rules:
ifMinus(false(),s(X),Y) -> s(minus(X,Y))
ifMinus(true(),s(X),Y) -> 0()
le(0(),Y) -> true()
minus(0(),Y) -> 0()
minus(s(X),Y) -> ifMinus(le(s(X),Y),s(X),Y)
quot(0(),s(Y)) -> 0()
Signature:
{ifMinus/3,le/2,minus/2,quot/2} / {0/0,false/0,s/1,true/0}
Obligation:
Innermost
basic terms: {ifMinus,le,minus,quot}/{0,false,s,true}
Applied Processor:
NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any strict-rules, greedy = NoGreedy}
Proof:
We apply a matrix interpretation of kind constructor based matrix interpretation:
The following argument positions are considered usable:
uargs(ifMinus) = {1},
uargs(quot) = {1},
uargs(s) = {1}
Following symbols are considered usable:
{ifMinus,le,minus,quot}
TcT has computed the following interpretation:
p(0) = [0]
p(false) = [0]
p(ifMinus) = [8] x1 + [1] x2 + [0]
p(le) = [0]
p(minus) = [1] x1 + [0]
p(quot) = [2] x1 + [8] x2 + [0]
p(s) = [1] x1 + [1]
p(true) = [0]
Following rules are strictly oriented:
quot(s(X),s(Y)) = [2] X + [8] Y + [10]
> [2] X + [8] Y + [9]
= s(quot(minus(X,Y),s(Y)))
Following rules are (at-least) weakly oriented:
ifMinus(false(),s(X),Y) = [1] X + [1]
>= [1] X + [1]
= s(minus(X,Y))
ifMinus(true(),s(X),Y) = [1] X + [1]
>= [0]
= 0()
le(0(),Y) = [0]
>= [0]
= true()
le(s(X),0()) = [0]
>= [0]
= false()
le(s(X),s(Y)) = [0]
>= [0]
= le(X,Y)
minus(0(),Y) = [0]
>= [0]
= 0()
minus(s(X),Y) = [1] X + [1]
>= [1] X + [1]
= ifMinus(le(s(X),Y),s(X),Y)
quot(0(),s(Y)) = [8] Y + [8]
>= [0]
= 0()
*** 1.1.1.1.1 Progress [(O(1),O(n^3))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
le(s(X),0()) -> false()
le(s(X),s(Y)) -> le(X,Y)
Weak DP Rules:
Weak TRS Rules:
ifMinus(false(),s(X),Y) -> s(minus(X,Y))
ifMinus(true(),s(X),Y) -> 0()
le(0(),Y) -> true()
minus(0(),Y) -> 0()
minus(s(X),Y) -> ifMinus(le(s(X),Y),s(X),Y)
quot(0(),s(Y)) -> 0()
quot(s(X),s(Y)) -> s(quot(minus(X,Y),s(Y)))
Signature:
{ifMinus/3,le/2,minus/2,quot/2} / {0/0,false/0,s/1,true/0}
Obligation:
Innermost
basic terms: {ifMinus,le,minus,quot}/{0,false,s,true}
Applied Processor:
NaturalMI {miDimension = 2, miDegree = 2, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any strict-rules, greedy = NoGreedy}
Proof:
We apply a matrix interpretation of kind constructor based matrix interpretation:
The following argument positions are considered usable:
uargs(ifMinus) = {1},
uargs(quot) = {1},
uargs(s) = {1}
Following symbols are considered usable:
{ifMinus,le,minus,quot}
TcT has computed the following interpretation:
p(0) = [2]
[0]
p(false) = [0]
[0]
p(ifMinus) = [2 0] x1 + [1 2] x2 + [0]
[0 0] [0 1] [0]
p(le) = [2]
[0]
p(minus) = [1 2] x1 + [4]
[0 1] [0]
p(quot) = [2 2] x1 + [0]
[0 1] [0]
p(s) = [1 4] x1 + [1]
[0 1] [4]
p(true) = [1]
[0]
Following rules are strictly oriented:
le(s(X),0()) = [2]
[0]
> [0]
[0]
= false()
Following rules are (at-least) weakly oriented:
ifMinus(false(),s(X),Y) = [1 6] X + [9]
[0 1] [4]
>= [1 6] X + [5]
[0 1] [4]
= s(minus(X,Y))
ifMinus(true(),s(X),Y) = [1 6] X + [11]
[0 1] [4]
>= [2]
[0]
= 0()
le(0(),Y) = [2]
[0]
>= [1]
[0]
= true()
le(s(X),s(Y)) = [2]
[0]
>= [2]
[0]
= le(X,Y)
minus(0(),Y) = [6]
[0]
>= [2]
[0]
= 0()
minus(s(X),Y) = [1 6] X + [13]
[0 1] [4]
>= [1 6] X + [13]
[0 1] [4]
= ifMinus(le(s(X),Y),s(X),Y)
quot(0(),s(Y)) = [4]
[0]
>= [2]
[0]
= 0()
quot(s(X),s(Y)) = [2 10] X + [10]
[0 1] [4]
>= [2 10] X + [9]
[0 1] [4]
= s(quot(minus(X,Y),s(Y)))
*** 1.1.1.1.1.1 Progress [(O(1),O(n^3))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
le(s(X),s(Y)) -> le(X,Y)
Weak DP Rules:
Weak TRS Rules:
ifMinus(false(),s(X),Y) -> s(minus(X,Y))
ifMinus(true(),s(X),Y) -> 0()
le(0(),Y) -> true()
le(s(X),0()) -> false()
minus(0(),Y) -> 0()
minus(s(X),Y) -> ifMinus(le(s(X),Y),s(X),Y)
quot(0(),s(Y)) -> 0()
quot(s(X),s(Y)) -> s(quot(minus(X,Y),s(Y)))
Signature:
{ifMinus/3,le/2,minus/2,quot/2} / {0/0,false/0,s/1,true/0}
Obligation:
Innermost
basic terms: {ifMinus,le,minus,quot}/{0,false,s,true}
Applied Processor:
NaturalMI {miDimension = 3, miDegree = 3, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any strict-rules, greedy = NoGreedy}
Proof:
We apply a matrix interpretation of kind constructor based matrix interpretation:
The following argument positions are considered usable:
uargs(ifMinus) = {1},
uargs(quot) = {1},
uargs(s) = {1}
Following symbols are considered usable:
{ifMinus,le,minus,quot}
TcT has computed the following interpretation:
p(0) = [1]
[0]
[1]
p(false) = [2]
[0]
[0]
p(ifMinus) = [1 0 0] [1 1 0] [0]
[0 0 0] x1 + [0 1 0] x2 + [0]
[0 0 0] [0 0 1] [0]
p(le) = [0 0 2] [0]
[0 2 0] x1 + [0]
[0 0 0] [0]
p(minus) = [1 1 2] [0]
[0 1 0] x1 + [0]
[0 0 1] [0]
p(quot) = [2 2 0] [0 1 1] [0]
[0 1 0] x1 + [0 0 0] x2 + [0]
[0 0 1] [0 0 0] [0]
p(s) = [1 2 0] [0]
[0 1 2] x1 + [0]
[0 0 1] [1]
p(true) = [1]
[0]
[0]
Following rules are strictly oriented:
le(s(X),s(Y)) = [0 0 2] [2]
[0 2 4] X + [0]
[0 0 0] [0]
> [0 0 2] [0]
[0 2 0] X + [0]
[0 0 0] [0]
= le(X,Y)
Following rules are (at-least) weakly oriented:
ifMinus(false(),s(X),Y) = [1 3 2] [2]
[0 1 2] X + [0]
[0 0 1] [1]
>= [1 3 2] [0]
[0 1 2] X + [0]
[0 0 1] [1]
= s(minus(X,Y))
ifMinus(true(),s(X),Y) = [1 3 2] [1]
[0 1 2] X + [0]
[0 0 1] [1]
>= [1]
[0]
[1]
= 0()
le(0(),Y) = [2]
[0]
[0]
>= [1]
[0]
[0]
= true()
le(s(X),0()) = [0 0 2] [2]
[0 2 4] X + [0]
[0 0 0] [0]
>= [2]
[0]
[0]
= false()
minus(0(),Y) = [3]
[0]
[1]
>= [1]
[0]
[1]
= 0()
minus(s(X),Y) = [1 3 4] [2]
[0 1 2] X + [0]
[0 0 1] [1]
>= [1 3 4] [2]
[0 1 2] X + [0]
[0 0 1] [1]
= ifMinus(le(s(X),Y),s(X),Y)
quot(0(),s(Y)) = [0 1 3] [3]
[0 0 0] Y + [0]
[0 0 0] [1]
>= [1]
[0]
[1]
= 0()
quot(s(X),s(Y)) = [2 6 4] [0 1 3] [1]
[0 1 2] X + [0 0 0] Y + [0]
[0 0 1] [0 0 0] [1]
>= [2 6 4] [0 1 3] [1]
[0 1 2] X + [0 0 0] Y + [0]
[0 0 1] [0 0 0] [1]
= s(quot(minus(X,Y),s(Y)))
*** 1.1.1.1.1.1.1 Progress [(O(1),O(1))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
Weak DP Rules:
Weak TRS Rules:
ifMinus(false(),s(X),Y) -> s(minus(X,Y))
ifMinus(true(),s(X),Y) -> 0()
le(0(),Y) -> true()
le(s(X),0()) -> false()
le(s(X),s(Y)) -> le(X,Y)
minus(0(),Y) -> 0()
minus(s(X),Y) -> ifMinus(le(s(X),Y),s(X),Y)
quot(0(),s(Y)) -> 0()
quot(s(X),s(Y)) -> s(quot(minus(X,Y),s(Y)))
Signature:
{ifMinus/3,le/2,minus/2,quot/2} / {0/0,false/0,s/1,true/0}
Obligation:
Innermost
basic terms: {ifMinus,le,minus,quot}/{0,false,s,true}
Applied Processor:
EmptyProcessor
Proof:
The problem is already closed. The intended complexity is O(1).