*** 1 Progress [(O(1),O(n^1))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
mem(x,nil()) -> false()
mem(x,set(y)) -> =(x,y)
mem(x,union(y,z)) -> or(mem(x,y),mem(x,z))
or(x,true()) -> true()
or(false(),false()) -> false()
or(true(),y) -> true()
Weak DP Rules:
Weak TRS Rules:
Signature:
{mem/2,or/2} / {=/2,false/0,nil/0,set/1,true/0,union/2}
Obligation:
Full
basic terms: {mem,or}/{=,false,nil,set,true,union}
Applied Processor:
DependencyPairs {dpKind_ = DT}
Proof:
We add the following weak dependency pairs:
Strict DPs
mem#(x,nil()) -> c_1()
mem#(x,set(y)) -> c_2(x,y)
mem#(x,union(y,z)) -> c_3(or#(mem(x,y),mem(x,z)))
or#(x,true()) -> c_4()
or#(false(),false()) -> c_5()
or#(true(),y) -> c_6()
Weak DPs
and mark the set of starting terms.
*** 1.1 Progress [(O(1),O(n^1))] ***
Considered Problem:
Strict DP Rules:
mem#(x,nil()) -> c_1()
mem#(x,set(y)) -> c_2(x,y)
mem#(x,union(y,z)) -> c_3(or#(mem(x,y),mem(x,z)))
or#(x,true()) -> c_4()
or#(false(),false()) -> c_5()
or#(true(),y) -> c_6()
Strict TRS Rules:
mem(x,nil()) -> false()
mem(x,set(y)) -> =(x,y)
mem(x,union(y,z)) -> or(mem(x,y),mem(x,z))
or(x,true()) -> true()
or(false(),false()) -> false()
or(true(),y) -> true()
Weak DP Rules:
Weak TRS Rules:
Signature:
{mem/2,or/2,mem#/2,or#/2} / {=/2,false/0,nil/0,set/1,true/0,union/2,c_1/0,c_2/2,c_3/1,c_4/0,c_5/0,c_6/0}
Obligation:
Full
basic terms: {mem#,or#}/{=,false,nil,set,true,union}
Applied Processor:
PredecessorEstimation {onSelection = all simple predecessor estimation selector}
Proof:
We estimate the number of application of
{1,4,5,6}
by application of
Pre({1,4,5,6}) = {2,3}.
Here rules are labelled as follows:
1: mem#(x,nil()) -> c_1()
2: mem#(x,set(y)) -> c_2(x,y)
3: mem#(x,union(y,z)) ->
c_3(or#(mem(x,y),mem(x,z)))
4: or#(x,true()) -> c_4()
5: or#(false(),false()) -> c_5()
6: or#(true(),y) -> c_6()
*** 1.1.1 Progress [(O(1),O(n^1))] ***
Considered Problem:
Strict DP Rules:
mem#(x,set(y)) -> c_2(x,y)
mem#(x,union(y,z)) -> c_3(or#(mem(x,y),mem(x,z)))
Strict TRS Rules:
mem(x,nil()) -> false()
mem(x,set(y)) -> =(x,y)
mem(x,union(y,z)) -> or(mem(x,y),mem(x,z))
or(x,true()) -> true()
or(false(),false()) -> false()
or(true(),y) -> true()
Weak DP Rules:
mem#(x,nil()) -> c_1()
or#(x,true()) -> c_4()
or#(false(),false()) -> c_5()
or#(true(),y) -> c_6()
Weak TRS Rules:
Signature:
{mem/2,or/2,mem#/2,or#/2} / {=/2,false/0,nil/0,set/1,true/0,union/2,c_1/0,c_2/2,c_3/1,c_4/0,c_5/0,c_6/0}
Obligation:
Full
basic terms: {mem#,or#}/{=,false,nil,set,true,union}
Applied Processor:
PredecessorEstimation {onSelection = all simple predecessor estimation selector}
Proof:
We estimate the number of application of
{2}
by application of
Pre({2}) = {1}.
Here rules are labelled as follows:
1: mem#(x,set(y)) -> c_2(x,y)
2: mem#(x,union(y,z)) ->
c_3(or#(mem(x,y),mem(x,z)))
3: mem#(x,nil()) -> c_1()
4: or#(x,true()) -> c_4()
5: or#(false(),false()) -> c_5()
6: or#(true(),y) -> c_6()
*** 1.1.1.1 Progress [(O(1),O(n^1))] ***
Considered Problem:
Strict DP Rules:
mem#(x,set(y)) -> c_2(x,y)
Strict TRS Rules:
mem(x,nil()) -> false()
mem(x,set(y)) -> =(x,y)
mem(x,union(y,z)) -> or(mem(x,y),mem(x,z))
or(x,true()) -> true()
or(false(),false()) -> false()
or(true(),y) -> true()
Weak DP Rules:
mem#(x,nil()) -> c_1()
mem#(x,union(y,z)) -> c_3(or#(mem(x,y),mem(x,z)))
or#(x,true()) -> c_4()
or#(false(),false()) -> c_5()
or#(true(),y) -> c_6()
Weak TRS Rules:
Signature:
{mem/2,or/2,mem#/2,or#/2} / {=/2,false/0,nil/0,set/1,true/0,union/2,c_1/0,c_2/2,c_3/1,c_4/0,c_5/0,c_6/0}
Obligation:
Full
basic terms: {mem#,or#}/{=,false,nil,set,true,union}
Applied Processor:
WeightGap {wgDimension = 1, wgDegree = 0, 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(or) = {1,2},
uargs(or#) = {1,2},
uargs(c_3) = {1}
Following symbols are considered usable:
{}
TcT has computed the following interpretation:
p(=) = [1] x2 + [0]
p(false) = [0]
p(mem) = [1] x2 + [0]
p(nil) = [0]
p(or) = [1] x1 + [1] x2 + [0]
p(set) = [1] x1 + [1]
p(true) = [0]
p(union) = [1] x1 + [1] x2 + [0]
p(mem#) = [1] x2 + [0]
p(or#) = [1] x1 + [1] x2 + [0]
p(c_1) = [0]
p(c_2) = [1] x2 + [0]
p(c_3) = [1] x1 + [0]
p(c_4) = [0]
p(c_5) = [0]
p(c_6) = [0]
Following rules are strictly oriented:
mem#(x,set(y)) = [1] y + [1]
> [1] y + [0]
= c_2(x,y)
mem(x,set(y)) = [1] y + [1]
> [1] y + [0]
= =(x,y)
Following rules are (at-least) weakly oriented:
mem#(x,nil()) = [0]
>= [0]
= c_1()
mem#(x,union(y,z)) = [1] y + [1] z + [0]
>= [1] y + [1] z + [0]
= c_3(or#(mem(x,y),mem(x,z)))
or#(x,true()) = [1] x + [0]
>= [0]
= c_4()
or#(false(),false()) = [0]
>= [0]
= c_5()
or#(true(),y) = [1] y + [0]
>= [0]
= c_6()
mem(x,nil()) = [0]
>= [0]
= false()
mem(x,union(y,z)) = [1] y + [1] z + [0]
>= [1] y + [1] z + [0]
= or(mem(x,y),mem(x,z))
or(x,true()) = [1] x + [0]
>= [0]
= true()
or(false(),false()) = [0]
>= [0]
= false()
or(true(),y) = [1] y + [0]
>= [0]
= true()
Further, it can be verified that all rules not oriented are covered by the weightgap condition.
*** 1.1.1.1.1 Progress [(O(1),O(n^1))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
mem(x,nil()) -> false()
mem(x,union(y,z)) -> or(mem(x,y),mem(x,z))
or(x,true()) -> true()
or(false(),false()) -> false()
or(true(),y) -> true()
Weak DP Rules:
mem#(x,nil()) -> c_1()
mem#(x,set(y)) -> c_2(x,y)
mem#(x,union(y,z)) -> c_3(or#(mem(x,y),mem(x,z)))
or#(x,true()) -> c_4()
or#(false(),false()) -> c_5()
or#(true(),y) -> c_6()
Weak TRS Rules:
mem(x,set(y)) -> =(x,y)
Signature:
{mem/2,or/2,mem#/2,or#/2} / {=/2,false/0,nil/0,set/1,true/0,union/2,c_1/0,c_2/2,c_3/1,c_4/0,c_5/0,c_6/0}
Obligation:
Full
basic terms: {mem#,or#}/{=,false,nil,set,true,union}
Applied Processor:
WeightGap {wgDimension = 1, wgDegree = 0, 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(or) = {1,2},
uargs(or#) = {1,2},
uargs(c_3) = {1}
Following symbols are considered usable:
{}
TcT has computed the following interpretation:
p(=) = [10]
p(false) = [0]
p(mem) = [4] x2 + [10]
p(nil) = [0]
p(or) = [1] x1 + [1] x2 + [10]
p(set) = [0]
p(true) = [0]
p(union) = [1] x1 + [1] x2 + [5]
p(mem#) = [4] x2 + [0]
p(or#) = [1] x1 + [1] x2 + [0]
p(c_1) = [0]
p(c_2) = [0]
p(c_3) = [1] x1 + [0]
p(c_4) = [0]
p(c_5) = [0]
p(c_6) = [0]
Following rules are strictly oriented:
mem(x,nil()) = [10]
> [0]
= false()
or(x,true()) = [1] x + [10]
> [0]
= true()
or(false(),false()) = [10]
> [0]
= false()
or(true(),y) = [1] y + [10]
> [0]
= true()
Following rules are (at-least) weakly oriented:
mem#(x,nil()) = [0]
>= [0]
= c_1()
mem#(x,set(y)) = [0]
>= [0]
= c_2(x,y)
mem#(x,union(y,z)) = [4] y + [4] z + [20]
>= [4] y + [4] z + [20]
= c_3(or#(mem(x,y),mem(x,z)))
or#(x,true()) = [1] x + [0]
>= [0]
= c_4()
or#(false(),false()) = [0]
>= [0]
= c_5()
or#(true(),y) = [1] y + [0]
>= [0]
= c_6()
mem(x,set(y)) = [10]
>= [10]
= =(x,y)
mem(x,union(y,z)) = [4] y + [4] z + [30]
>= [4] y + [4] z + [30]
= or(mem(x,y),mem(x,z))
Further, it can be verified that all rules not oriented are covered by the weightgap condition.
*** 1.1.1.1.1.1 Progress [(O(1),O(n^1))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
mem(x,union(y,z)) -> or(mem(x,y),mem(x,z))
Weak DP Rules:
mem#(x,nil()) -> c_1()
mem#(x,set(y)) -> c_2(x,y)
mem#(x,union(y,z)) -> c_3(or#(mem(x,y),mem(x,z)))
or#(x,true()) -> c_4()
or#(false(),false()) -> c_5()
or#(true(),y) -> c_6()
Weak TRS Rules:
mem(x,nil()) -> false()
mem(x,set(y)) -> =(x,y)
or(x,true()) -> true()
or(false(),false()) -> false()
or(true(),y) -> true()
Signature:
{mem/2,or/2,mem#/2,or#/2} / {=/2,false/0,nil/0,set/1,true/0,union/2,c_1/0,c_2/2,c_3/1,c_4/0,c_5/0,c_6/0}
Obligation:
Full
basic terms: {mem#,or#}/{=,false,nil,set,true,union}
Applied Processor:
WeightGap {wgDimension = 1, wgDegree = 0, 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(or) = {1,2},
uargs(or#) = {1,2},
uargs(c_3) = {1}
Following symbols are considered usable:
{}
TcT has computed the following interpretation:
p(=) = [1] x2 + [5]
p(false) = [1]
p(mem) = [7] x2 + [5]
p(nil) = [0]
p(or) = [1] x1 + [1] x2 + [5]
p(set) = [1] x1 + [0]
p(true) = [10]
p(union) = [1] x1 + [1] x2 + [3]
p(mem#) = [8] x2 + [6]
p(or#) = [1] x1 + [1] x2 + [1]
p(c_1) = [6]
p(c_2) = [8] x2 + [1]
p(c_3) = [1] x1 + [1]
p(c_4) = [8]
p(c_5) = [3]
p(c_6) = [11]
Following rules are strictly oriented:
mem(x,union(y,z)) = [7] y + [7] z + [26]
> [7] y + [7] z + [15]
= or(mem(x,y),mem(x,z))
Following rules are (at-least) weakly oriented:
mem#(x,nil()) = [6]
>= [6]
= c_1()
mem#(x,set(y)) = [8] y + [6]
>= [8] y + [1]
= c_2(x,y)
mem#(x,union(y,z)) = [8] y + [8] z + [30]
>= [7] y + [7] z + [12]
= c_3(or#(mem(x,y),mem(x,z)))
or#(x,true()) = [1] x + [11]
>= [8]
= c_4()
or#(false(),false()) = [3]
>= [3]
= c_5()
or#(true(),y) = [1] y + [11]
>= [11]
= c_6()
mem(x,nil()) = [5]
>= [1]
= false()
mem(x,set(y)) = [7] y + [5]
>= [1] y + [5]
= =(x,y)
or(x,true()) = [1] x + [15]
>= [10]
= true()
or(false(),false()) = [7]
>= [1]
= false()
or(true(),y) = [1] y + [15]
>= [10]
= true()
Further, it can be verified that all rules not oriented are covered by the weightgap condition.
*** 1.1.1.1.1.1.1 Progress [(O(1),O(1))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
Weak DP Rules:
mem#(x,nil()) -> c_1()
mem#(x,set(y)) -> c_2(x,y)
mem#(x,union(y,z)) -> c_3(or#(mem(x,y),mem(x,z)))
or#(x,true()) -> c_4()
or#(false(),false()) -> c_5()
or#(true(),y) -> c_6()
Weak TRS Rules:
mem(x,nil()) -> false()
mem(x,set(y)) -> =(x,y)
mem(x,union(y,z)) -> or(mem(x,y),mem(x,z))
or(x,true()) -> true()
or(false(),false()) -> false()
or(true(),y) -> true()
Signature:
{mem/2,or/2,mem#/2,or#/2} / {=/2,false/0,nil/0,set/1,true/0,union/2,c_1/0,c_2/2,c_3/1,c_4/0,c_5/0,c_6/0}
Obligation:
Full
basic terms: {mem#,or#}/{=,false,nil,set,true,union}
Applied Processor:
EmptyProcessor
Proof:
The problem is already closed. The intended complexity is O(1).