MAYBE
* Step 1: InnermostRuleRemoval MAYBE
+ Considered Problem:
- Strict TRS:
and(x,false()) -> false()
and(true(),true()) -> true()
f(0()) -> true()
f(s(x)) -> h(x)
g(s(x),s(y)) -> if(and(f(s(x)),f(s(y)))
,t(g(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0())))))
,g(minus(m(x,y),n(x,y)),n(s(x),s(y))))
gt(0(),y) -> false()
gt(s(x),0()) -> true()
gt(s(x),s(y)) -> gt(x,y)
h(0()) -> false()
h(s(x)) -> f(x)
id(x) -> x
if(false(),x,y) -> y
if(true(),x,y) -> x
k(0(),s(y)) -> 0()
k(s(x),s(y)) -> s(k(minus(x,y),s(y)))
m(x,0()) -> x
m(0(),y) -> y
m(s(x),s(y)) -> s(m(x,y))
minus(x,0()) -> x
minus(s(x),s(y)) -> minus(x,y)
n(x,0()) -> 0()
n(0(),y) -> 0()
n(s(x),s(y)) -> s(n(x,y))
not(x) -> if(x,false(),true())
p(0(),y) -> y
p(id(x),s(y)) -> s(p(x,if(gt(s(y),y),y,s(y))))
p(s(x),x) -> p(if(gt(x,x),id(x),id(x)),s(x))
p(s(x),s(y)) -> s(s(p(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y)))))
t(x) -> p(x,x)
- Signature:
{and/2,f/1,g/2,gt/2,h/1,id/1,if/3,k/2,m/2,minus/2,n/2,not/1,p/2,t/1} / {0/0,false/0,s/1,true/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {and,f,g,gt,h,id,if,k,m,minus,n,not,p
,t} and constructors {0,false,s,true}
+ Applied Processor:
InnermostRuleRemoval
+ Details:
Arguments of following rules are not normal-forms.
p(id(x),s(y)) -> s(p(x,if(gt(s(y),y),y,s(y))))
All above mentioned rules can be savely removed.
* Step 2: DependencyPairs MAYBE
+ Considered Problem:
- Strict TRS:
and(x,false()) -> false()
and(true(),true()) -> true()
f(0()) -> true()
f(s(x)) -> h(x)
g(s(x),s(y)) -> if(and(f(s(x)),f(s(y)))
,t(g(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0())))))
,g(minus(m(x,y),n(x,y)),n(s(x),s(y))))
gt(0(),y) -> false()
gt(s(x),0()) -> true()
gt(s(x),s(y)) -> gt(x,y)
h(0()) -> false()
h(s(x)) -> f(x)
id(x) -> x
if(false(),x,y) -> y
if(true(),x,y) -> x
k(0(),s(y)) -> 0()
k(s(x),s(y)) -> s(k(minus(x,y),s(y)))
m(x,0()) -> x
m(0(),y) -> y
m(s(x),s(y)) -> s(m(x,y))
minus(x,0()) -> x
minus(s(x),s(y)) -> minus(x,y)
n(x,0()) -> 0()
n(0(),y) -> 0()
n(s(x),s(y)) -> s(n(x,y))
not(x) -> if(x,false(),true())
p(0(),y) -> y
p(s(x),x) -> p(if(gt(x,x),id(x),id(x)),s(x))
p(s(x),s(y)) -> s(s(p(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y)))))
t(x) -> p(x,x)
- Signature:
{and/2,f/1,g/2,gt/2,h/1,id/1,if/3,k/2,m/2,minus/2,n/2,not/1,p/2,t/1} / {0/0,false/0,s/1,true/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {and,f,g,gt,h,id,if,k,m,minus,n,not,p
,t} and constructors {0,false,s,true}
+ Applied Processor:
DependencyPairs {dpKind_ = DT}
+ Details:
We add the following dependency tuples:
Strict DPs
and#(x,false()) -> c_1()
and#(true(),true()) -> c_2()
f#(0()) -> c_3()
f#(s(x)) -> c_4(h#(x))
g#(s(x),s(y)) -> c_5(if#(and(f(s(x)),f(s(y)))
,t(g(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0())))))
,g(minus(m(x,y),n(x,y)),n(s(x),s(y))))
,and#(f(s(x)),f(s(y)))
,f#(s(x))
,f#(s(y))
,t#(g(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0())))))
,g#(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0()))))
,k#(minus(m(x,y),n(x,y)),s(s(0())))
,minus#(m(x,y),n(x,y))
,m#(x,y)
,n#(x,y)
,k#(n(s(x),s(y)),s(s(0())))
,n#(s(x),s(y))
,g#(minus(m(x,y),n(x,y)),n(s(x),s(y)))
,minus#(m(x,y),n(x,y))
,m#(x,y)
,n#(x,y)
,n#(s(x),s(y)))
gt#(0(),y) -> c_6()
gt#(s(x),0()) -> c_7()
gt#(s(x),s(y)) -> c_8(gt#(x,y))
h#(0()) -> c_9()
h#(s(x)) -> c_10(f#(x))
id#(x) -> c_11()
if#(false(),x,y) -> c_12()
if#(true(),x,y) -> c_13()
k#(0(),s(y)) -> c_14()
k#(s(x),s(y)) -> c_15(k#(minus(x,y),s(y)),minus#(x,y))
m#(x,0()) -> c_16()
m#(0(),y) -> c_17()
m#(s(x),s(y)) -> c_18(m#(x,y))
minus#(x,0()) -> c_19()
minus#(s(x),s(y)) -> c_20(minus#(x,y))
n#(x,0()) -> c_21()
n#(0(),y) -> c_22()
n#(s(x),s(y)) -> c_23(n#(x,y))
not#(x) -> c_24(if#(x,false(),true()))
p#(0(),y) -> c_25()
p#(s(x),x) -> c_26(p#(if(gt(x,x),id(x),id(x)),s(x)),if#(gt(x,x),id(x),id(x)),gt#(x,x),id#(x),id#(x))
p#(s(x),s(y)) -> c_27(p#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y)))
,if#(gt(x,y),x,y)
,gt#(x,y)
,if#(not(gt(x,y)),id(x),id(y))
,not#(gt(x,y))
,gt#(x,y)
,id#(x)
,id#(y))
t#(x) -> c_28(p#(x,x))
Weak DPs
and mark the set of starting terms.
* Step 3: PredecessorEstimation MAYBE
+ Considered Problem:
- Strict DPs:
and#(x,false()) -> c_1()
and#(true(),true()) -> c_2()
f#(0()) -> c_3()
f#(s(x)) -> c_4(h#(x))
g#(s(x),s(y)) -> c_5(if#(and(f(s(x)),f(s(y)))
,t(g(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0())))))
,g(minus(m(x,y),n(x,y)),n(s(x),s(y))))
,and#(f(s(x)),f(s(y)))
,f#(s(x))
,f#(s(y))
,t#(g(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0())))))
,g#(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0()))))
,k#(minus(m(x,y),n(x,y)),s(s(0())))
,minus#(m(x,y),n(x,y))
,m#(x,y)
,n#(x,y)
,k#(n(s(x),s(y)),s(s(0())))
,n#(s(x),s(y))
,g#(minus(m(x,y),n(x,y)),n(s(x),s(y)))
,minus#(m(x,y),n(x,y))
,m#(x,y)
,n#(x,y)
,n#(s(x),s(y)))
gt#(0(),y) -> c_6()
gt#(s(x),0()) -> c_7()
gt#(s(x),s(y)) -> c_8(gt#(x,y))
h#(0()) -> c_9()
h#(s(x)) -> c_10(f#(x))
id#(x) -> c_11()
if#(false(),x,y) -> c_12()
if#(true(),x,y) -> c_13()
k#(0(),s(y)) -> c_14()
k#(s(x),s(y)) -> c_15(k#(minus(x,y),s(y)),minus#(x,y))
m#(x,0()) -> c_16()
m#(0(),y) -> c_17()
m#(s(x),s(y)) -> c_18(m#(x,y))
minus#(x,0()) -> c_19()
minus#(s(x),s(y)) -> c_20(minus#(x,y))
n#(x,0()) -> c_21()
n#(0(),y) -> c_22()
n#(s(x),s(y)) -> c_23(n#(x,y))
not#(x) -> c_24(if#(x,false(),true()))
p#(0(),y) -> c_25()
p#(s(x),x) -> c_26(p#(if(gt(x,x),id(x),id(x)),s(x)),if#(gt(x,x),id(x),id(x)),gt#(x,x),id#(x),id#(x))
p#(s(x),s(y)) -> c_27(p#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y)))
,if#(gt(x,y),x,y)
,gt#(x,y)
,if#(not(gt(x,y)),id(x),id(y))
,not#(gt(x,y))
,gt#(x,y)
,id#(x)
,id#(y))
t#(x) -> c_28(p#(x,x))
- Weak TRS:
and(x,false()) -> false()
and(true(),true()) -> true()
f(0()) -> true()
f(s(x)) -> h(x)
g(s(x),s(y)) -> if(and(f(s(x)),f(s(y)))
,t(g(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0())))))
,g(minus(m(x,y),n(x,y)),n(s(x),s(y))))
gt(0(),y) -> false()
gt(s(x),0()) -> true()
gt(s(x),s(y)) -> gt(x,y)
h(0()) -> false()
h(s(x)) -> f(x)
id(x) -> x
if(false(),x,y) -> y
if(true(),x,y) -> x
k(0(),s(y)) -> 0()
k(s(x),s(y)) -> s(k(minus(x,y),s(y)))
m(x,0()) -> x
m(0(),y) -> y
m(s(x),s(y)) -> s(m(x,y))
minus(x,0()) -> x
minus(s(x),s(y)) -> minus(x,y)
n(x,0()) -> 0()
n(0(),y) -> 0()
n(s(x),s(y)) -> s(n(x,y))
not(x) -> if(x,false(),true())
p(0(),y) -> y
p(s(x),x) -> p(if(gt(x,x),id(x),id(x)),s(x))
p(s(x),s(y)) -> s(s(p(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y)))))
t(x) -> p(x,x)
- Signature:
{and/2,f/1,g/2,gt/2,h/1,id/1,if/3,k/2,m/2,minus/2,n/2,not/1,p/2,t/1,and#/2,f#/1,g#/2,gt#/2,h#/1,id#/1,if#/3
,k#/2,m#/2,minus#/2,n#/2,not#/1,p#/2,t#/1} / {0/0,false/0,s/1,true/0,c_1/0,c_2/0,c_3/0,c_4/1,c_5/17,c_6/0
,c_7/0,c_8/1,c_9/0,c_10/1,c_11/0,c_12/0,c_13/0,c_14/0,c_15/2,c_16/0,c_17/0,c_18/1,c_19/0,c_20/1,c_21/0
,c_22/0,c_23/1,c_24/1,c_25/0,c_26/5,c_27/8,c_28/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {and#,f#,g#,gt#,h#,id#,if#,k#,m#,minus#,n#,not#,p#
,t#} and constructors {0,false,s,true}
+ Applied Processor:
PredecessorEstimation {onSelection = all simple predecessor estimation selector}
+ Details:
We estimate the number of application of
{1,2,3,6,7,9,11,12,13,14,16,17,19,21,22,25}
by application of
Pre({1,2,3,6,7,9,11,12,13,14,16,17,19,21,22,25}) = {4,5,8,10,15,18,20,23,24,26,27,28}.
Here rules are labelled as follows:
1: and#(x,false()) -> c_1()
2: and#(true(),true()) -> c_2()
3: f#(0()) -> c_3()
4: f#(s(x)) -> c_4(h#(x))
5: g#(s(x),s(y)) -> c_5(if#(and(f(s(x)),f(s(y)))
,t(g(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0())))))
,g(minus(m(x,y),n(x,y)),n(s(x),s(y))))
,and#(f(s(x)),f(s(y)))
,f#(s(x))
,f#(s(y))
,t#(g(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0())))))
,g#(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0()))))
,k#(minus(m(x,y),n(x,y)),s(s(0())))
,minus#(m(x,y),n(x,y))
,m#(x,y)
,n#(x,y)
,k#(n(s(x),s(y)),s(s(0())))
,n#(s(x),s(y))
,g#(minus(m(x,y),n(x,y)),n(s(x),s(y)))
,minus#(m(x,y),n(x,y))
,m#(x,y)
,n#(x,y)
,n#(s(x),s(y)))
6: gt#(0(),y) -> c_6()
7: gt#(s(x),0()) -> c_7()
8: gt#(s(x),s(y)) -> c_8(gt#(x,y))
9: h#(0()) -> c_9()
10: h#(s(x)) -> c_10(f#(x))
11: id#(x) -> c_11()
12: if#(false(),x,y) -> c_12()
13: if#(true(),x,y) -> c_13()
14: k#(0(),s(y)) -> c_14()
15: k#(s(x),s(y)) -> c_15(k#(minus(x,y),s(y)),minus#(x,y))
16: m#(x,0()) -> c_16()
17: m#(0(),y) -> c_17()
18: m#(s(x),s(y)) -> c_18(m#(x,y))
19: minus#(x,0()) -> c_19()
20: minus#(s(x),s(y)) -> c_20(minus#(x,y))
21: n#(x,0()) -> c_21()
22: n#(0(),y) -> c_22()
23: n#(s(x),s(y)) -> c_23(n#(x,y))
24: not#(x) -> c_24(if#(x,false(),true()))
25: p#(0(),y) -> c_25()
26: p#(s(x),x) -> c_26(p#(if(gt(x,x),id(x),id(x)),s(x)),if#(gt(x,x),id(x),id(x)),gt#(x,x),id#(x),id#(x))
27: p#(s(x),s(y)) -> c_27(p#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y)))
,if#(gt(x,y),x,y)
,gt#(x,y)
,if#(not(gt(x,y)),id(x),id(y))
,not#(gt(x,y))
,gt#(x,y)
,id#(x)
,id#(y))
28: t#(x) -> c_28(p#(x,x))
* Step 4: PredecessorEstimation MAYBE
+ Considered Problem:
- Strict DPs:
f#(s(x)) -> c_4(h#(x))
g#(s(x),s(y)) -> c_5(if#(and(f(s(x)),f(s(y)))
,t(g(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0())))))
,g(minus(m(x,y),n(x,y)),n(s(x),s(y))))
,and#(f(s(x)),f(s(y)))
,f#(s(x))
,f#(s(y))
,t#(g(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0())))))
,g#(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0()))))
,k#(minus(m(x,y),n(x,y)),s(s(0())))
,minus#(m(x,y),n(x,y))
,m#(x,y)
,n#(x,y)
,k#(n(s(x),s(y)),s(s(0())))
,n#(s(x),s(y))
,g#(minus(m(x,y),n(x,y)),n(s(x),s(y)))
,minus#(m(x,y),n(x,y))
,m#(x,y)
,n#(x,y)
,n#(s(x),s(y)))
gt#(s(x),s(y)) -> c_8(gt#(x,y))
h#(s(x)) -> c_10(f#(x))
k#(s(x),s(y)) -> c_15(k#(minus(x,y),s(y)),minus#(x,y))
m#(s(x),s(y)) -> c_18(m#(x,y))
minus#(s(x),s(y)) -> c_20(minus#(x,y))
n#(s(x),s(y)) -> c_23(n#(x,y))
not#(x) -> c_24(if#(x,false(),true()))
p#(s(x),x) -> c_26(p#(if(gt(x,x),id(x),id(x)),s(x)),if#(gt(x,x),id(x),id(x)),gt#(x,x),id#(x),id#(x))
p#(s(x),s(y)) -> c_27(p#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y)))
,if#(gt(x,y),x,y)
,gt#(x,y)
,if#(not(gt(x,y)),id(x),id(y))
,not#(gt(x,y))
,gt#(x,y)
,id#(x)
,id#(y))
t#(x) -> c_28(p#(x,x))
- Weak DPs:
and#(x,false()) -> c_1()
and#(true(),true()) -> c_2()
f#(0()) -> c_3()
gt#(0(),y) -> c_6()
gt#(s(x),0()) -> c_7()
h#(0()) -> c_9()
id#(x) -> c_11()
if#(false(),x,y) -> c_12()
if#(true(),x,y) -> c_13()
k#(0(),s(y)) -> c_14()
m#(x,0()) -> c_16()
m#(0(),y) -> c_17()
minus#(x,0()) -> c_19()
n#(x,0()) -> c_21()
n#(0(),y) -> c_22()
p#(0(),y) -> c_25()
- Weak TRS:
and(x,false()) -> false()
and(true(),true()) -> true()
f(0()) -> true()
f(s(x)) -> h(x)
g(s(x),s(y)) -> if(and(f(s(x)),f(s(y)))
,t(g(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0())))))
,g(minus(m(x,y),n(x,y)),n(s(x),s(y))))
gt(0(),y) -> false()
gt(s(x),0()) -> true()
gt(s(x),s(y)) -> gt(x,y)
h(0()) -> false()
h(s(x)) -> f(x)
id(x) -> x
if(false(),x,y) -> y
if(true(),x,y) -> x
k(0(),s(y)) -> 0()
k(s(x),s(y)) -> s(k(minus(x,y),s(y)))
m(x,0()) -> x
m(0(),y) -> y
m(s(x),s(y)) -> s(m(x,y))
minus(x,0()) -> x
minus(s(x),s(y)) -> minus(x,y)
n(x,0()) -> 0()
n(0(),y) -> 0()
n(s(x),s(y)) -> s(n(x,y))
not(x) -> if(x,false(),true())
p(0(),y) -> y
p(s(x),x) -> p(if(gt(x,x),id(x),id(x)),s(x))
p(s(x),s(y)) -> s(s(p(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y)))))
t(x) -> p(x,x)
- Signature:
{and/2,f/1,g/2,gt/2,h/1,id/1,if/3,k/2,m/2,minus/2,n/2,not/1,p/2,t/1,and#/2,f#/1,g#/2,gt#/2,h#/1,id#/1,if#/3
,k#/2,m#/2,minus#/2,n#/2,not#/1,p#/2,t#/1} / {0/0,false/0,s/1,true/0,c_1/0,c_2/0,c_3/0,c_4/1,c_5/17,c_6/0
,c_7/0,c_8/1,c_9/0,c_10/1,c_11/0,c_12/0,c_13/0,c_14/0,c_15/2,c_16/0,c_17/0,c_18/1,c_19/0,c_20/1,c_21/0
,c_22/0,c_23/1,c_24/1,c_25/0,c_26/5,c_27/8,c_28/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {and#,f#,g#,gt#,h#,id#,if#,k#,m#,minus#,n#,not#,p#
,t#} and constructors {0,false,s,true}
+ Applied Processor:
PredecessorEstimation {onSelection = all simple predecessor estimation selector}
+ Details:
We estimate the number of application of
{9}
by application of
Pre({9}) = {11}.
Here rules are labelled as follows:
1: f#(s(x)) -> c_4(h#(x))
2: g#(s(x),s(y)) -> c_5(if#(and(f(s(x)),f(s(y)))
,t(g(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0())))))
,g(minus(m(x,y),n(x,y)),n(s(x),s(y))))
,and#(f(s(x)),f(s(y)))
,f#(s(x))
,f#(s(y))
,t#(g(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0())))))
,g#(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0()))))
,k#(minus(m(x,y),n(x,y)),s(s(0())))
,minus#(m(x,y),n(x,y))
,m#(x,y)
,n#(x,y)
,k#(n(s(x),s(y)),s(s(0())))
,n#(s(x),s(y))
,g#(minus(m(x,y),n(x,y)),n(s(x),s(y)))
,minus#(m(x,y),n(x,y))
,m#(x,y)
,n#(x,y)
,n#(s(x),s(y)))
3: gt#(s(x),s(y)) -> c_8(gt#(x,y))
4: h#(s(x)) -> c_10(f#(x))
5: k#(s(x),s(y)) -> c_15(k#(minus(x,y),s(y)),minus#(x,y))
6: m#(s(x),s(y)) -> c_18(m#(x,y))
7: minus#(s(x),s(y)) -> c_20(minus#(x,y))
8: n#(s(x),s(y)) -> c_23(n#(x,y))
9: not#(x) -> c_24(if#(x,false(),true()))
10: p#(s(x),x) -> c_26(p#(if(gt(x,x),id(x),id(x)),s(x)),if#(gt(x,x),id(x),id(x)),gt#(x,x),id#(x),id#(x))
11: p#(s(x),s(y)) -> c_27(p#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y)))
,if#(gt(x,y),x,y)
,gt#(x,y)
,if#(not(gt(x,y)),id(x),id(y))
,not#(gt(x,y))
,gt#(x,y)
,id#(x)
,id#(y))
12: t#(x) -> c_28(p#(x,x))
13: and#(x,false()) -> c_1()
14: and#(true(),true()) -> c_2()
15: f#(0()) -> c_3()
16: gt#(0(),y) -> c_6()
17: gt#(s(x),0()) -> c_7()
18: h#(0()) -> c_9()
19: id#(x) -> c_11()
20: if#(false(),x,y) -> c_12()
21: if#(true(),x,y) -> c_13()
22: k#(0(),s(y)) -> c_14()
23: m#(x,0()) -> c_16()
24: m#(0(),y) -> c_17()
25: minus#(x,0()) -> c_19()
26: n#(x,0()) -> c_21()
27: n#(0(),y) -> c_22()
28: p#(0(),y) -> c_25()
* Step 5: RemoveWeakSuffixes MAYBE
+ Considered Problem:
- Strict DPs:
f#(s(x)) -> c_4(h#(x))
g#(s(x),s(y)) -> c_5(if#(and(f(s(x)),f(s(y)))
,t(g(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0())))))
,g(minus(m(x,y),n(x,y)),n(s(x),s(y))))
,and#(f(s(x)),f(s(y)))
,f#(s(x))
,f#(s(y))
,t#(g(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0())))))
,g#(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0()))))
,k#(minus(m(x,y),n(x,y)),s(s(0())))
,minus#(m(x,y),n(x,y))
,m#(x,y)
,n#(x,y)
,k#(n(s(x),s(y)),s(s(0())))
,n#(s(x),s(y))
,g#(minus(m(x,y),n(x,y)),n(s(x),s(y)))
,minus#(m(x,y),n(x,y))
,m#(x,y)
,n#(x,y)
,n#(s(x),s(y)))
gt#(s(x),s(y)) -> c_8(gt#(x,y))
h#(s(x)) -> c_10(f#(x))
k#(s(x),s(y)) -> c_15(k#(minus(x,y),s(y)),minus#(x,y))
m#(s(x),s(y)) -> c_18(m#(x,y))
minus#(s(x),s(y)) -> c_20(minus#(x,y))
n#(s(x),s(y)) -> c_23(n#(x,y))
p#(s(x),x) -> c_26(p#(if(gt(x,x),id(x),id(x)),s(x)),if#(gt(x,x),id(x),id(x)),gt#(x,x),id#(x),id#(x))
p#(s(x),s(y)) -> c_27(p#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y)))
,if#(gt(x,y),x,y)
,gt#(x,y)
,if#(not(gt(x,y)),id(x),id(y))
,not#(gt(x,y))
,gt#(x,y)
,id#(x)
,id#(y))
t#(x) -> c_28(p#(x,x))
- Weak DPs:
and#(x,false()) -> c_1()
and#(true(),true()) -> c_2()
f#(0()) -> c_3()
gt#(0(),y) -> c_6()
gt#(s(x),0()) -> c_7()
h#(0()) -> c_9()
id#(x) -> c_11()
if#(false(),x,y) -> c_12()
if#(true(),x,y) -> c_13()
k#(0(),s(y)) -> c_14()
m#(x,0()) -> c_16()
m#(0(),y) -> c_17()
minus#(x,0()) -> c_19()
n#(x,0()) -> c_21()
n#(0(),y) -> c_22()
not#(x) -> c_24(if#(x,false(),true()))
p#(0(),y) -> c_25()
- Weak TRS:
and(x,false()) -> false()
and(true(),true()) -> true()
f(0()) -> true()
f(s(x)) -> h(x)
g(s(x),s(y)) -> if(and(f(s(x)),f(s(y)))
,t(g(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0())))))
,g(minus(m(x,y),n(x,y)),n(s(x),s(y))))
gt(0(),y) -> false()
gt(s(x),0()) -> true()
gt(s(x),s(y)) -> gt(x,y)
h(0()) -> false()
h(s(x)) -> f(x)
id(x) -> x
if(false(),x,y) -> y
if(true(),x,y) -> x
k(0(),s(y)) -> 0()
k(s(x),s(y)) -> s(k(minus(x,y),s(y)))
m(x,0()) -> x
m(0(),y) -> y
m(s(x),s(y)) -> s(m(x,y))
minus(x,0()) -> x
minus(s(x),s(y)) -> minus(x,y)
n(x,0()) -> 0()
n(0(),y) -> 0()
n(s(x),s(y)) -> s(n(x,y))
not(x) -> if(x,false(),true())
p(0(),y) -> y
p(s(x),x) -> p(if(gt(x,x),id(x),id(x)),s(x))
p(s(x),s(y)) -> s(s(p(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y)))))
t(x) -> p(x,x)
- Signature:
{and/2,f/1,g/2,gt/2,h/1,id/1,if/3,k/2,m/2,minus/2,n/2,not/1,p/2,t/1,and#/2,f#/1,g#/2,gt#/2,h#/1,id#/1,if#/3
,k#/2,m#/2,minus#/2,n#/2,not#/1,p#/2,t#/1} / {0/0,false/0,s/1,true/0,c_1/0,c_2/0,c_3/0,c_4/1,c_5/17,c_6/0
,c_7/0,c_8/1,c_9/0,c_10/1,c_11/0,c_12/0,c_13/0,c_14/0,c_15/2,c_16/0,c_17/0,c_18/1,c_19/0,c_20/1,c_21/0
,c_22/0,c_23/1,c_24/1,c_25/0,c_26/5,c_27/8,c_28/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {and#,f#,g#,gt#,h#,id#,if#,k#,m#,minus#,n#,not#,p#
,t#} and constructors {0,false,s,true}
+ Applied Processor:
RemoveWeakSuffixes
+ Details:
Consider the dependency graph
1:S:f#(s(x)) -> c_4(h#(x))
-->_1 h#(s(x)) -> c_10(f#(x)):4
-->_1 h#(0()) -> c_9():17
2:S:g#(s(x),s(y)) -> c_5(if#(and(f(s(x)),f(s(y)))
,t(g(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0())))))
,g(minus(m(x,y),n(x,y)),n(s(x),s(y))))
,and#(f(s(x)),f(s(y)))
,f#(s(x))
,f#(s(y))
,t#(g(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0())))))
,g#(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0()))))
,k#(minus(m(x,y),n(x,y)),s(s(0())))
,minus#(m(x,y),n(x,y))
,m#(x,y)
,n#(x,y)
,k#(n(s(x),s(y)),s(s(0())))
,n#(s(x),s(y))
,g#(minus(m(x,y),n(x,y)),n(s(x),s(y)))
,minus#(m(x,y),n(x,y))
,m#(x,y)
,n#(x,y)
,n#(s(x),s(y)))
-->_5 t#(x) -> c_28(p#(x,x)):11
-->_17 n#(s(x),s(y)) -> c_23(n#(x,y)):8
-->_16 n#(s(x),s(y)) -> c_23(n#(x,y)):8
-->_12 n#(s(x),s(y)) -> c_23(n#(x,y)):8
-->_10 n#(s(x),s(y)) -> c_23(n#(x,y)):8
-->_14 minus#(s(x),s(y)) -> c_20(minus#(x,y)):7
-->_8 minus#(s(x),s(y)) -> c_20(minus#(x,y)):7
-->_15 m#(s(x),s(y)) -> c_18(m#(x,y)):6
-->_9 m#(s(x),s(y)) -> c_18(m#(x,y)):6
-->_11 k#(s(x),s(y)) -> c_15(k#(minus(x,y),s(y)),minus#(x,y)):5
-->_7 k#(s(x),s(y)) -> c_15(k#(minus(x,y),s(y)),minus#(x,y)):5
-->_16 n#(0(),y) -> c_22():26
-->_10 n#(0(),y) -> c_22():26
-->_16 n#(x,0()) -> c_21():25
-->_10 n#(x,0()) -> c_21():25
-->_14 minus#(x,0()) -> c_19():24
-->_8 minus#(x,0()) -> c_19():24
-->_15 m#(0(),y) -> c_17():23
-->_9 m#(0(),y) -> c_17():23
-->_15 m#(x,0()) -> c_16():22
-->_9 m#(x,0()) -> c_16():22
-->_11 k#(0(),s(y)) -> c_14():21
-->_7 k#(0(),s(y)) -> c_14():21
-->_1 if#(true(),x,y) -> c_13():20
-->_1 if#(false(),x,y) -> c_12():19
-->_2 and#(true(),true()) -> c_2():13
-->_2 and#(x,false()) -> c_1():12
-->_13 g#(s(x),s(y)) -> c_5(if#(and(f(s(x)),f(s(y)))
,t(g(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0())))))
,g(minus(m(x,y),n(x,y)),n(s(x),s(y))))
,and#(f(s(x)),f(s(y)))
,f#(s(x))
,f#(s(y))
,t#(g(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0())))))
,g#(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0()))))
,k#(minus(m(x,y),n(x,y)),s(s(0())))
,minus#(m(x,y),n(x,y))
,m#(x,y)
,n#(x,y)
,k#(n(s(x),s(y)),s(s(0())))
,n#(s(x),s(y))
,g#(minus(m(x,y),n(x,y)),n(s(x),s(y)))
,minus#(m(x,y),n(x,y))
,m#(x,y)
,n#(x,y)
,n#(s(x),s(y))):2
-->_6 g#(s(x),s(y)) -> c_5(if#(and(f(s(x)),f(s(y)))
,t(g(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0())))))
,g(minus(m(x,y),n(x,y)),n(s(x),s(y))))
,and#(f(s(x)),f(s(y)))
,f#(s(x))
,f#(s(y))
,t#(g(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0())))))
,g#(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0()))))
,k#(minus(m(x,y),n(x,y)),s(s(0())))
,minus#(m(x,y),n(x,y))
,m#(x,y)
,n#(x,y)
,k#(n(s(x),s(y)),s(s(0())))
,n#(s(x),s(y))
,g#(minus(m(x,y),n(x,y)),n(s(x),s(y)))
,minus#(m(x,y),n(x,y))
,m#(x,y)
,n#(x,y)
,n#(s(x),s(y))):2
-->_4 f#(s(x)) -> c_4(h#(x)):1
-->_3 f#(s(x)) -> c_4(h#(x)):1
3:S:gt#(s(x),s(y)) -> c_8(gt#(x,y))
-->_1 gt#(s(x),0()) -> c_7():16
-->_1 gt#(0(),y) -> c_6():15
-->_1 gt#(s(x),s(y)) -> c_8(gt#(x,y)):3
4:S:h#(s(x)) -> c_10(f#(x))
-->_1 f#(0()) -> c_3():14
-->_1 f#(s(x)) -> c_4(h#(x)):1
5:S:k#(s(x),s(y)) -> c_15(k#(minus(x,y),s(y)),minus#(x,y))
-->_2 minus#(s(x),s(y)) -> c_20(minus#(x,y)):7
-->_2 minus#(x,0()) -> c_19():24
-->_1 k#(0(),s(y)) -> c_14():21
-->_1 k#(s(x),s(y)) -> c_15(k#(minus(x,y),s(y)),minus#(x,y)):5
6:S:m#(s(x),s(y)) -> c_18(m#(x,y))
-->_1 m#(0(),y) -> c_17():23
-->_1 m#(x,0()) -> c_16():22
-->_1 m#(s(x),s(y)) -> c_18(m#(x,y)):6
7:S:minus#(s(x),s(y)) -> c_20(minus#(x,y))
-->_1 minus#(x,0()) -> c_19():24
-->_1 minus#(s(x),s(y)) -> c_20(minus#(x,y)):7
8:S:n#(s(x),s(y)) -> c_23(n#(x,y))
-->_1 n#(0(),y) -> c_22():26
-->_1 n#(x,0()) -> c_21():25
-->_1 n#(s(x),s(y)) -> c_23(n#(x,y)):8
9:S:p#(s(x),x) -> c_26(p#(if(gt(x,x),id(x),id(x)),s(x)),if#(gt(x,x),id(x),id(x)),gt#(x,x),id#(x),id#(x))
-->_1 p#(s(x),s(y)) -> c_27(p#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y)))
,if#(gt(x,y),x,y)
,gt#(x,y)
,if#(not(gt(x,y)),id(x),id(y))
,not#(gt(x,y))
,gt#(x,y)
,id#(x)
,id#(y)):10
-->_1 p#(0(),y) -> c_25():28
-->_2 if#(true(),x,y) -> c_13():20
-->_2 if#(false(),x,y) -> c_12():19
-->_5 id#(x) -> c_11():18
-->_4 id#(x) -> c_11():18
-->_3 gt#(0(),y) -> c_6():15
-->_1 p#(s(x),x) -> c_26(p#(if(gt(x,x),id(x),id(x)),s(x))
,if#(gt(x,x),id(x),id(x))
,gt#(x,x)
,id#(x)
,id#(x)):9
-->_3 gt#(s(x),s(y)) -> c_8(gt#(x,y)):3
10:S:p#(s(x),s(y)) -> c_27(p#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y)))
,if#(gt(x,y),x,y)
,gt#(x,y)
,if#(not(gt(x,y)),id(x),id(y))
,not#(gt(x,y))
,gt#(x,y)
,id#(x)
,id#(y))
-->_5 not#(x) -> c_24(if#(x,false(),true())):27
-->_1 p#(0(),y) -> c_25():28
-->_4 if#(true(),x,y) -> c_13():20
-->_2 if#(true(),x,y) -> c_13():20
-->_4 if#(false(),x,y) -> c_12():19
-->_2 if#(false(),x,y) -> c_12():19
-->_8 id#(x) -> c_11():18
-->_7 id#(x) -> c_11():18
-->_6 gt#(s(x),0()) -> c_7():16
-->_3 gt#(s(x),0()) -> c_7():16
-->_6 gt#(0(),y) -> c_6():15
-->_3 gt#(0(),y) -> c_6():15
-->_1 p#(s(x),s(y)) -> c_27(p#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y)))
,if#(gt(x,y),x,y)
,gt#(x,y)
,if#(not(gt(x,y)),id(x),id(y))
,not#(gt(x,y))
,gt#(x,y)
,id#(x)
,id#(y)):10
-->_1 p#(s(x),x) -> c_26(p#(if(gt(x,x),id(x),id(x)),s(x))
,if#(gt(x,x),id(x),id(x))
,gt#(x,x)
,id#(x)
,id#(x)):9
-->_6 gt#(s(x),s(y)) -> c_8(gt#(x,y)):3
-->_3 gt#(s(x),s(y)) -> c_8(gt#(x,y)):3
11:S:t#(x) -> c_28(p#(x,x))
-->_1 p#(0(),y) -> c_25():28
-->_1 p#(s(x),s(y)) -> c_27(p#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y)))
,if#(gt(x,y),x,y)
,gt#(x,y)
,if#(not(gt(x,y)),id(x),id(y))
,not#(gt(x,y))
,gt#(x,y)
,id#(x)
,id#(y)):10
12:W:and#(x,false()) -> c_1()
13:W:and#(true(),true()) -> c_2()
14:W:f#(0()) -> c_3()
15:W:gt#(0(),y) -> c_6()
16:W:gt#(s(x),0()) -> c_7()
17:W:h#(0()) -> c_9()
18:W:id#(x) -> c_11()
19:W:if#(false(),x,y) -> c_12()
20:W:if#(true(),x,y) -> c_13()
21:W:k#(0(),s(y)) -> c_14()
22:W:m#(x,0()) -> c_16()
23:W:m#(0(),y) -> c_17()
24:W:minus#(x,0()) -> c_19()
25:W:n#(x,0()) -> c_21()
26:W:n#(0(),y) -> c_22()
27:W:not#(x) -> c_24(if#(x,false(),true()))
-->_1 if#(true(),x,y) -> c_13():20
-->_1 if#(false(),x,y) -> c_12():19
28:W:p#(0(),y) -> c_25()
The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
12: and#(x,false()) -> c_1()
13: and#(true(),true()) -> c_2()
21: k#(0(),s(y)) -> c_14()
22: m#(x,0()) -> c_16()
23: m#(0(),y) -> c_17()
24: minus#(x,0()) -> c_19()
25: n#(x,0()) -> c_21()
26: n#(0(),y) -> c_22()
15: gt#(0(),y) -> c_6()
16: gt#(s(x),0()) -> c_7()
18: id#(x) -> c_11()
27: not#(x) -> c_24(if#(x,false(),true()))
19: if#(false(),x,y) -> c_12()
20: if#(true(),x,y) -> c_13()
28: p#(0(),y) -> c_25()
17: h#(0()) -> c_9()
14: f#(0()) -> c_3()
* Step 6: SimplifyRHS MAYBE
+ Considered Problem:
- Strict DPs:
f#(s(x)) -> c_4(h#(x))
g#(s(x),s(y)) -> c_5(if#(and(f(s(x)),f(s(y)))
,t(g(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0())))))
,g(minus(m(x,y),n(x,y)),n(s(x),s(y))))
,and#(f(s(x)),f(s(y)))
,f#(s(x))
,f#(s(y))
,t#(g(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0())))))
,g#(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0()))))
,k#(minus(m(x,y),n(x,y)),s(s(0())))
,minus#(m(x,y),n(x,y))
,m#(x,y)
,n#(x,y)
,k#(n(s(x),s(y)),s(s(0())))
,n#(s(x),s(y))
,g#(minus(m(x,y),n(x,y)),n(s(x),s(y)))
,minus#(m(x,y),n(x,y))
,m#(x,y)
,n#(x,y)
,n#(s(x),s(y)))
gt#(s(x),s(y)) -> c_8(gt#(x,y))
h#(s(x)) -> c_10(f#(x))
k#(s(x),s(y)) -> c_15(k#(minus(x,y),s(y)),minus#(x,y))
m#(s(x),s(y)) -> c_18(m#(x,y))
minus#(s(x),s(y)) -> c_20(minus#(x,y))
n#(s(x),s(y)) -> c_23(n#(x,y))
p#(s(x),x) -> c_26(p#(if(gt(x,x),id(x),id(x)),s(x)),if#(gt(x,x),id(x),id(x)),gt#(x,x),id#(x),id#(x))
p#(s(x),s(y)) -> c_27(p#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y)))
,if#(gt(x,y),x,y)
,gt#(x,y)
,if#(not(gt(x,y)),id(x),id(y))
,not#(gt(x,y))
,gt#(x,y)
,id#(x)
,id#(y))
t#(x) -> c_28(p#(x,x))
- Weak TRS:
and(x,false()) -> false()
and(true(),true()) -> true()
f(0()) -> true()
f(s(x)) -> h(x)
g(s(x),s(y)) -> if(and(f(s(x)),f(s(y)))
,t(g(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0())))))
,g(minus(m(x,y),n(x,y)),n(s(x),s(y))))
gt(0(),y) -> false()
gt(s(x),0()) -> true()
gt(s(x),s(y)) -> gt(x,y)
h(0()) -> false()
h(s(x)) -> f(x)
id(x) -> x
if(false(),x,y) -> y
if(true(),x,y) -> x
k(0(),s(y)) -> 0()
k(s(x),s(y)) -> s(k(minus(x,y),s(y)))
m(x,0()) -> x
m(0(),y) -> y
m(s(x),s(y)) -> s(m(x,y))
minus(x,0()) -> x
minus(s(x),s(y)) -> minus(x,y)
n(x,0()) -> 0()
n(0(),y) -> 0()
n(s(x),s(y)) -> s(n(x,y))
not(x) -> if(x,false(),true())
p(0(),y) -> y
p(s(x),x) -> p(if(gt(x,x),id(x),id(x)),s(x))
p(s(x),s(y)) -> s(s(p(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y)))))
t(x) -> p(x,x)
- Signature:
{and/2,f/1,g/2,gt/2,h/1,id/1,if/3,k/2,m/2,minus/2,n/2,not/1,p/2,t/1,and#/2,f#/1,g#/2,gt#/2,h#/1,id#/1,if#/3
,k#/2,m#/2,minus#/2,n#/2,not#/1,p#/2,t#/1} / {0/0,false/0,s/1,true/0,c_1/0,c_2/0,c_3/0,c_4/1,c_5/17,c_6/0
,c_7/0,c_8/1,c_9/0,c_10/1,c_11/0,c_12/0,c_13/0,c_14/0,c_15/2,c_16/0,c_17/0,c_18/1,c_19/0,c_20/1,c_21/0
,c_22/0,c_23/1,c_24/1,c_25/0,c_26/5,c_27/8,c_28/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {and#,f#,g#,gt#,h#,id#,if#,k#,m#,minus#,n#,not#,p#
,t#} and constructors {0,false,s,true}
+ Applied Processor:
SimplifyRHS
+ Details:
Consider the dependency graph
1:S:f#(s(x)) -> c_4(h#(x))
-->_1 h#(s(x)) -> c_10(f#(x)):4
2:S:g#(s(x),s(y)) -> c_5(if#(and(f(s(x)),f(s(y)))
,t(g(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0())))))
,g(minus(m(x,y),n(x,y)),n(s(x),s(y))))
,and#(f(s(x)),f(s(y)))
,f#(s(x))
,f#(s(y))
,t#(g(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0())))))
,g#(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0()))))
,k#(minus(m(x,y),n(x,y)),s(s(0())))
,minus#(m(x,y),n(x,y))
,m#(x,y)
,n#(x,y)
,k#(n(s(x),s(y)),s(s(0())))
,n#(s(x),s(y))
,g#(minus(m(x,y),n(x,y)),n(s(x),s(y)))
,minus#(m(x,y),n(x,y))
,m#(x,y)
,n#(x,y)
,n#(s(x),s(y)))
-->_5 t#(x) -> c_28(p#(x,x)):11
-->_17 n#(s(x),s(y)) -> c_23(n#(x,y)):8
-->_16 n#(s(x),s(y)) -> c_23(n#(x,y)):8
-->_12 n#(s(x),s(y)) -> c_23(n#(x,y)):8
-->_10 n#(s(x),s(y)) -> c_23(n#(x,y)):8
-->_14 minus#(s(x),s(y)) -> c_20(minus#(x,y)):7
-->_8 minus#(s(x),s(y)) -> c_20(minus#(x,y)):7
-->_15 m#(s(x),s(y)) -> c_18(m#(x,y)):6
-->_9 m#(s(x),s(y)) -> c_18(m#(x,y)):6
-->_11 k#(s(x),s(y)) -> c_15(k#(minus(x,y),s(y)),minus#(x,y)):5
-->_7 k#(s(x),s(y)) -> c_15(k#(minus(x,y),s(y)),minus#(x,y)):5
-->_13 g#(s(x),s(y)) -> c_5(if#(and(f(s(x)),f(s(y)))
,t(g(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0())))))
,g(minus(m(x,y),n(x,y)),n(s(x),s(y))))
,and#(f(s(x)),f(s(y)))
,f#(s(x))
,f#(s(y))
,t#(g(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0())))))
,g#(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0()))))
,k#(minus(m(x,y),n(x,y)),s(s(0())))
,minus#(m(x,y),n(x,y))
,m#(x,y)
,n#(x,y)
,k#(n(s(x),s(y)),s(s(0())))
,n#(s(x),s(y))
,g#(minus(m(x,y),n(x,y)),n(s(x),s(y)))
,minus#(m(x,y),n(x,y))
,m#(x,y)
,n#(x,y)
,n#(s(x),s(y))):2
-->_6 g#(s(x),s(y)) -> c_5(if#(and(f(s(x)),f(s(y)))
,t(g(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0())))))
,g(minus(m(x,y),n(x,y)),n(s(x),s(y))))
,and#(f(s(x)),f(s(y)))
,f#(s(x))
,f#(s(y))
,t#(g(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0())))))
,g#(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0()))))
,k#(minus(m(x,y),n(x,y)),s(s(0())))
,minus#(m(x,y),n(x,y))
,m#(x,y)
,n#(x,y)
,k#(n(s(x),s(y)),s(s(0())))
,n#(s(x),s(y))
,g#(minus(m(x,y),n(x,y)),n(s(x),s(y)))
,minus#(m(x,y),n(x,y))
,m#(x,y)
,n#(x,y)
,n#(s(x),s(y))):2
-->_4 f#(s(x)) -> c_4(h#(x)):1
-->_3 f#(s(x)) -> c_4(h#(x)):1
3:S:gt#(s(x),s(y)) -> c_8(gt#(x,y))
-->_1 gt#(s(x),s(y)) -> c_8(gt#(x,y)):3
4:S:h#(s(x)) -> c_10(f#(x))
-->_1 f#(s(x)) -> c_4(h#(x)):1
5:S:k#(s(x),s(y)) -> c_15(k#(minus(x,y),s(y)),minus#(x,y))
-->_2 minus#(s(x),s(y)) -> c_20(minus#(x,y)):7
-->_1 k#(s(x),s(y)) -> c_15(k#(minus(x,y),s(y)),minus#(x,y)):5
6:S:m#(s(x),s(y)) -> c_18(m#(x,y))
-->_1 m#(s(x),s(y)) -> c_18(m#(x,y)):6
7:S:minus#(s(x),s(y)) -> c_20(minus#(x,y))
-->_1 minus#(s(x),s(y)) -> c_20(minus#(x,y)):7
8:S:n#(s(x),s(y)) -> c_23(n#(x,y))
-->_1 n#(s(x),s(y)) -> c_23(n#(x,y)):8
9:S:p#(s(x),x) -> c_26(p#(if(gt(x,x),id(x),id(x)),s(x)),if#(gt(x,x),id(x),id(x)),gt#(x,x),id#(x),id#(x))
-->_1 p#(s(x),s(y)) -> c_27(p#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y)))
,if#(gt(x,y),x,y)
,gt#(x,y)
,if#(not(gt(x,y)),id(x),id(y))
,not#(gt(x,y))
,gt#(x,y)
,id#(x)
,id#(y)):10
-->_1 p#(s(x),x) -> c_26(p#(if(gt(x,x),id(x),id(x)),s(x))
,if#(gt(x,x),id(x),id(x))
,gt#(x,x)
,id#(x)
,id#(x)):9
-->_3 gt#(s(x),s(y)) -> c_8(gt#(x,y)):3
10:S:p#(s(x),s(y)) -> c_27(p#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y)))
,if#(gt(x,y),x,y)
,gt#(x,y)
,if#(not(gt(x,y)),id(x),id(y))
,not#(gt(x,y))
,gt#(x,y)
,id#(x)
,id#(y))
-->_1 p#(s(x),s(y)) -> c_27(p#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y)))
,if#(gt(x,y),x,y)
,gt#(x,y)
,if#(not(gt(x,y)),id(x),id(y))
,not#(gt(x,y))
,gt#(x,y)
,id#(x)
,id#(y)):10
-->_1 p#(s(x),x) -> c_26(p#(if(gt(x,x),id(x),id(x)),s(x))
,if#(gt(x,x),id(x),id(x))
,gt#(x,x)
,id#(x)
,id#(x)):9
-->_6 gt#(s(x),s(y)) -> c_8(gt#(x,y)):3
-->_3 gt#(s(x),s(y)) -> c_8(gt#(x,y)):3
11:S:t#(x) -> c_28(p#(x,x))
-->_1 p#(s(x),s(y)) -> c_27(p#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y)))
,if#(gt(x,y),x,y)
,gt#(x,y)
,if#(not(gt(x,y)),id(x),id(y))
,not#(gt(x,y))
,gt#(x,y)
,id#(x)
,id#(y)):10
Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified:
g#(s(x),s(y)) -> c_5(f#(s(x))
,f#(s(y))
,t#(g(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0())))))
,g#(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0()))))
,k#(minus(m(x,y),n(x,y)),s(s(0())))
,minus#(m(x,y),n(x,y))
,m#(x,y)
,n#(x,y)
,k#(n(s(x),s(y)),s(s(0())))
,n#(s(x),s(y))
,g#(minus(m(x,y),n(x,y)),n(s(x),s(y)))
,minus#(m(x,y),n(x,y))
,m#(x,y)
,n#(x,y)
,n#(s(x),s(y)))
p#(s(x),x) -> c_26(p#(if(gt(x,x),id(x),id(x)),s(x)),gt#(x,x))
p#(s(x),s(y)) -> c_27(p#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))),gt#(x,y),gt#(x,y))
* Step 7: Failure MAYBE
+ Considered Problem:
- Strict DPs:
f#(s(x)) -> c_4(h#(x))
g#(s(x),s(y)) -> c_5(f#(s(x))
,f#(s(y))
,t#(g(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0())))))
,g#(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0()))))
,k#(minus(m(x,y),n(x,y)),s(s(0())))
,minus#(m(x,y),n(x,y))
,m#(x,y)
,n#(x,y)
,k#(n(s(x),s(y)),s(s(0())))
,n#(s(x),s(y))
,g#(minus(m(x,y),n(x,y)),n(s(x),s(y)))
,minus#(m(x,y),n(x,y))
,m#(x,y)
,n#(x,y)
,n#(s(x),s(y)))
gt#(s(x),s(y)) -> c_8(gt#(x,y))
h#(s(x)) -> c_10(f#(x))
k#(s(x),s(y)) -> c_15(k#(minus(x,y),s(y)),minus#(x,y))
m#(s(x),s(y)) -> c_18(m#(x,y))
minus#(s(x),s(y)) -> c_20(minus#(x,y))
n#(s(x),s(y)) -> c_23(n#(x,y))
p#(s(x),x) -> c_26(p#(if(gt(x,x),id(x),id(x)),s(x)),gt#(x,x))
p#(s(x),s(y)) -> c_27(p#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))),gt#(x,y),gt#(x,y))
t#(x) -> c_28(p#(x,x))
- Weak TRS:
and(x,false()) -> false()
and(true(),true()) -> true()
f(0()) -> true()
f(s(x)) -> h(x)
g(s(x),s(y)) -> if(and(f(s(x)),f(s(y)))
,t(g(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0())))))
,g(minus(m(x,y),n(x,y)),n(s(x),s(y))))
gt(0(),y) -> false()
gt(s(x),0()) -> true()
gt(s(x),s(y)) -> gt(x,y)
h(0()) -> false()
h(s(x)) -> f(x)
id(x) -> x
if(false(),x,y) -> y
if(true(),x,y) -> x
k(0(),s(y)) -> 0()
k(s(x),s(y)) -> s(k(minus(x,y),s(y)))
m(x,0()) -> x
m(0(),y) -> y
m(s(x),s(y)) -> s(m(x,y))
minus(x,0()) -> x
minus(s(x),s(y)) -> minus(x,y)
n(x,0()) -> 0()
n(0(),y) -> 0()
n(s(x),s(y)) -> s(n(x,y))
not(x) -> if(x,false(),true())
p(0(),y) -> y
p(s(x),x) -> p(if(gt(x,x),id(x),id(x)),s(x))
p(s(x),s(y)) -> s(s(p(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y)))))
t(x) -> p(x,x)
- Signature:
{and/2,f/1,g/2,gt/2,h/1,id/1,if/3,k/2,m/2,minus/2,n/2,not/1,p/2,t/1,and#/2,f#/1,g#/2,gt#/2,h#/1,id#/1,if#/3
,k#/2,m#/2,minus#/2,n#/2,not#/1,p#/2,t#/1} / {0/0,false/0,s/1,true/0,c_1/0,c_2/0,c_3/0,c_4/1,c_5/15,c_6/0
,c_7/0,c_8/1,c_9/0,c_10/1,c_11/0,c_12/0,c_13/0,c_14/0,c_15/2,c_16/0,c_17/0,c_18/1,c_19/0,c_20/1,c_21/0
,c_22/0,c_23/1,c_24/1,c_25/0,c_26/2,c_27/3,c_28/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {and#,f#,g#,gt#,h#,id#,if#,k#,m#,minus#,n#,not#,p#
,t#} and constructors {0,false,s,true}
+ Applied Processor:
EmptyProcessor
+ Details:
The problem is still open.
MAYBE