* Step 1: Sum WORST_CASE(Omega(n^1),?)
+ Considered Problem:
- Strict TRS:
intersect'ii'in(Xs,cons(X0,Ys)) -> u'1'1(intersect'ii'in(Xs,Ys))
intersect'ii'in(cons(X,X0),cons(X,X1)) -> intersect'ii'out()
intersect'ii'in(cons(X0,Xs),Ys) -> u'2'1(intersect'ii'in(Xs,Ys))
reduce'ii'in(sequent(Fs,cons(if(A,B),Gs)),NF) -> u'8'1(reduce'ii'in(sequent(Fs,cons(x'2b(x'2d(B),A),Gs))
,NF))
reduce'ii'in(sequent(Fs,cons(iff(A,B),Gs)),NF) -> u'9'1(reduce'ii'in(sequent(Fs
,cons(x'2a(if(A,B),if(B,A)),Gs))
,NF))
reduce'ii'in(sequent(Fs,cons(x'2a(G1,G2),Gs)),NF) -> u'12'1(reduce'ii'in(sequent(Fs,cons(G1,Gs)),NF)
,Fs
,G2
,Gs
,NF)
reduce'ii'in(sequent(Fs,cons(x'2b(G1,G2),Gs)),NF) -> u'11'1(reduce'ii'in(sequent(Fs,cons(G1,cons(G2,Gs)))
,NF))
reduce'ii'in(sequent(Fs,cons(x'2d(G1),Gs)),NF) -> u'13'1(reduce'ii'in(sequent(cons(G1,Fs),Gs),NF))
reduce'ii'in(sequent(cons(if(A,B),Fs),Gs),NF) -> u'3'1(reduce'ii'in(sequent(cons(x'2b(x'2d(B),A),Fs),Gs)
,NF))
reduce'ii'in(sequent(cons(iff(A,B),Fs),Gs),NF) -> u'4'1(reduce'ii'in(sequent(cons(x'2a(if(A,B),if(B,A)),Fs)
,Gs)
,NF))
reduce'ii'in(sequent(cons(p(V),Fs),Gs),sequent(Left,Right)) -> u'10'1(reduce'ii'in(sequent(Fs,Gs)
,sequent(cons(p(V),Left)
,Right)))
reduce'ii'in(sequent(cons(x'2a(F1,F2),Fs),Gs),NF) -> u'5'1(reduce'ii'in(sequent(cons(F1,cons(F2,Fs)),Gs)
,NF))
reduce'ii'in(sequent(cons(x'2b(F1,F2),Fs),Gs),NF) -> u'6'1(reduce'ii'in(sequent(cons(F1,Fs),Gs),NF)
,F2
,Fs
,Gs
,NF)
reduce'ii'in(sequent(cons(x'2d(F1),Fs),Gs),NF) -> u'7'1(reduce'ii'in(sequent(Fs,cons(F1,Gs)),NF))
reduce'ii'in(sequent(nil(),cons(p(V),Gs)),sequent(Left,Right)) -> u'14'1(reduce'ii'in(sequent(nil(),Gs)
,sequent(Left
,cons(p(V)
,Right))))
reduce'ii'in(sequent(nil(),nil()),sequent(F1,F2)) -> u'15'1(intersect'ii'in(F1,F2))
tautology'i'in(F) -> u'16'1(reduce'ii'in(sequent(nil(),cons(F,nil())),sequent(nil(),nil())))
u'1'1(intersect'ii'out()) -> intersect'ii'out()
u'10'1(reduce'ii'out()) -> reduce'ii'out()
u'11'1(reduce'ii'out()) -> reduce'ii'out()
u'12'1(reduce'ii'out(),Fs,G2,Gs,NF) -> u'12'2(reduce'ii'in(sequent(Fs,cons(G2,Gs)),NF))
u'12'2(reduce'ii'out()) -> reduce'ii'out()
u'13'1(reduce'ii'out()) -> reduce'ii'out()
u'14'1(reduce'ii'out()) -> reduce'ii'out()
u'15'1(intersect'ii'out()) -> reduce'ii'out()
u'16'1(reduce'ii'out()) -> tautology'i'out()
u'2'1(intersect'ii'out()) -> intersect'ii'out()
u'3'1(reduce'ii'out()) -> reduce'ii'out()
u'4'1(reduce'ii'out()) -> reduce'ii'out()
u'5'1(reduce'ii'out()) -> reduce'ii'out()
u'6'1(reduce'ii'out(),F2,Fs,Gs,NF) -> u'6'2(reduce'ii'in(sequent(cons(F2,Fs),Gs),NF))
u'6'2(reduce'ii'out()) -> reduce'ii'out()
u'7'1(reduce'ii'out()) -> reduce'ii'out()
u'8'1(reduce'ii'out()) -> reduce'ii'out()
u'9'1(reduce'ii'out()) -> reduce'ii'out()
- Signature:
{intersect'ii'in/2,reduce'ii'in/2,tautology'i'in/1,u'1'1/1,u'10'1/1,u'11'1/1,u'12'1/5,u'12'2/1,u'13'1/1
,u'14'1/1,u'15'1/1,u'16'1/1,u'2'1/1,u'3'1/1,u'4'1/1,u'5'1/1,u'6'1/5,u'6'2/1,u'7'1/1,u'8'1/1
,u'9'1/1} / {cons/2,if/2,iff/2,intersect'ii'out/0,nil/0,p/1,reduce'ii'out/0,sequent/2,tautology'i'out/0
,x'2a/2,x'2b/2,x'2d/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {intersect'ii'in,reduce'ii'in,tautology'i'in,u'1'1,u'10'1
,u'11'1,u'12'1,u'12'2,u'13'1,u'14'1,u'15'1,u'16'1,u'2'1,u'3'1,u'4'1,u'5'1,u'6'1,u'6'2,u'7'1,u'8'1
,u'9'1} and constructors {cons,if,iff,intersect'ii'out,nil,p,reduce'ii'out,sequent,tautology'i'out,x'2a,x'2b
,x'2d}
+ Applied Processor:
Sum {left = someStrategy, right = someStrategy}
+ Details:
()
* Step 2: DecreasingLoops WORST_CASE(Omega(n^1),?)
+ Considered Problem:
- Strict TRS:
intersect'ii'in(Xs,cons(X0,Ys)) -> u'1'1(intersect'ii'in(Xs,Ys))
intersect'ii'in(cons(X,X0),cons(X,X1)) -> intersect'ii'out()
intersect'ii'in(cons(X0,Xs),Ys) -> u'2'1(intersect'ii'in(Xs,Ys))
reduce'ii'in(sequent(Fs,cons(if(A,B),Gs)),NF) -> u'8'1(reduce'ii'in(sequent(Fs,cons(x'2b(x'2d(B),A),Gs))
,NF))
reduce'ii'in(sequent(Fs,cons(iff(A,B),Gs)),NF) -> u'9'1(reduce'ii'in(sequent(Fs
,cons(x'2a(if(A,B),if(B,A)),Gs))
,NF))
reduce'ii'in(sequent(Fs,cons(x'2a(G1,G2),Gs)),NF) -> u'12'1(reduce'ii'in(sequent(Fs,cons(G1,Gs)),NF)
,Fs
,G2
,Gs
,NF)
reduce'ii'in(sequent(Fs,cons(x'2b(G1,G2),Gs)),NF) -> u'11'1(reduce'ii'in(sequent(Fs,cons(G1,cons(G2,Gs)))
,NF))
reduce'ii'in(sequent(Fs,cons(x'2d(G1),Gs)),NF) -> u'13'1(reduce'ii'in(sequent(cons(G1,Fs),Gs),NF))
reduce'ii'in(sequent(cons(if(A,B),Fs),Gs),NF) -> u'3'1(reduce'ii'in(sequent(cons(x'2b(x'2d(B),A),Fs),Gs)
,NF))
reduce'ii'in(sequent(cons(iff(A,B),Fs),Gs),NF) -> u'4'1(reduce'ii'in(sequent(cons(x'2a(if(A,B),if(B,A)),Fs)
,Gs)
,NF))
reduce'ii'in(sequent(cons(p(V),Fs),Gs),sequent(Left,Right)) -> u'10'1(reduce'ii'in(sequent(Fs,Gs)
,sequent(cons(p(V),Left)
,Right)))
reduce'ii'in(sequent(cons(x'2a(F1,F2),Fs),Gs),NF) -> u'5'1(reduce'ii'in(sequent(cons(F1,cons(F2,Fs)),Gs)
,NF))
reduce'ii'in(sequent(cons(x'2b(F1,F2),Fs),Gs),NF) -> u'6'1(reduce'ii'in(sequent(cons(F1,Fs),Gs),NF)
,F2
,Fs
,Gs
,NF)
reduce'ii'in(sequent(cons(x'2d(F1),Fs),Gs),NF) -> u'7'1(reduce'ii'in(sequent(Fs,cons(F1,Gs)),NF))
reduce'ii'in(sequent(nil(),cons(p(V),Gs)),sequent(Left,Right)) -> u'14'1(reduce'ii'in(sequent(nil(),Gs)
,sequent(Left
,cons(p(V)
,Right))))
reduce'ii'in(sequent(nil(),nil()),sequent(F1,F2)) -> u'15'1(intersect'ii'in(F1,F2))
tautology'i'in(F) -> u'16'1(reduce'ii'in(sequent(nil(),cons(F,nil())),sequent(nil(),nil())))
u'1'1(intersect'ii'out()) -> intersect'ii'out()
u'10'1(reduce'ii'out()) -> reduce'ii'out()
u'11'1(reduce'ii'out()) -> reduce'ii'out()
u'12'1(reduce'ii'out(),Fs,G2,Gs,NF) -> u'12'2(reduce'ii'in(sequent(Fs,cons(G2,Gs)),NF))
u'12'2(reduce'ii'out()) -> reduce'ii'out()
u'13'1(reduce'ii'out()) -> reduce'ii'out()
u'14'1(reduce'ii'out()) -> reduce'ii'out()
u'15'1(intersect'ii'out()) -> reduce'ii'out()
u'16'1(reduce'ii'out()) -> tautology'i'out()
u'2'1(intersect'ii'out()) -> intersect'ii'out()
u'3'1(reduce'ii'out()) -> reduce'ii'out()
u'4'1(reduce'ii'out()) -> reduce'ii'out()
u'5'1(reduce'ii'out()) -> reduce'ii'out()
u'6'1(reduce'ii'out(),F2,Fs,Gs,NF) -> u'6'2(reduce'ii'in(sequent(cons(F2,Fs),Gs),NF))
u'6'2(reduce'ii'out()) -> reduce'ii'out()
u'7'1(reduce'ii'out()) -> reduce'ii'out()
u'8'1(reduce'ii'out()) -> reduce'ii'out()
u'9'1(reduce'ii'out()) -> reduce'ii'out()
- Signature:
{intersect'ii'in/2,reduce'ii'in/2,tautology'i'in/1,u'1'1/1,u'10'1/1,u'11'1/1,u'12'1/5,u'12'2/1,u'13'1/1
,u'14'1/1,u'15'1/1,u'16'1/1,u'2'1/1,u'3'1/1,u'4'1/1,u'5'1/1,u'6'1/5,u'6'2/1,u'7'1/1,u'8'1/1
,u'9'1/1} / {cons/2,if/2,iff/2,intersect'ii'out/0,nil/0,p/1,reduce'ii'out/0,sequent/2,tautology'i'out/0
,x'2a/2,x'2b/2,x'2d/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {intersect'ii'in,reduce'ii'in,tautology'i'in,u'1'1,u'10'1
,u'11'1,u'12'1,u'12'2,u'13'1,u'14'1,u'15'1,u'16'1,u'2'1,u'3'1,u'4'1,u'5'1,u'6'1,u'6'2,u'7'1,u'8'1
,u'9'1} and constructors {cons,if,iff,intersect'ii'out,nil,p,reduce'ii'out,sequent,tautology'i'out,x'2a,x'2b
,x'2d}
+ Applied Processor:
DecreasingLoops {bound = AnyLoop, narrow = 10}
+ Details:
The system has following decreasing Loops:
intersect'ii'in(x,z){z -> cons(y,z)} =
intersect'ii'in(x,cons(y,z)) ->^+ u'1'1(intersect'ii'in(x,z))
= C[intersect'ii'in(x,z) = intersect'ii'in(x,z){}]
WORST_CASE(Omega(n^1),?)