YES
Proof:
This system is quasi-decreasing.
By \cite{O02}, p. 214, Proposition 7.2.50.
This system is of type 3 or smaller.
This system is deterministic.
System R transformed to U(R).
Call external tool:
ttt2 - trs 30
Input:
ssp'(xs, 0) -> nil
?6(ys', y', ws, v, w) -> cons(y', ys')
?5(w, y', ws, v) -> ?6(ssp'(ws, w), y', ws, v, w)
ssp'(cons(y', ws), v) -> ?5(sub(v, y'), y', ws, v)
?4(ys', y', xs', w, v, zs, x') -> cons(y', ys')
?3(w, y', xs', v, zs, x') -> ?4(ssp'(cons(x', zs), w), y', xs', w, v, zs, x')
?2(tp2(y', zs), x', xs', v) -> ?3(sub(v, y'), y', xs', v, zs, x')
ssp'(cons(x', xs'), v) -> ?2(get(xs'), x', xs', v)
sub(z, 0) -> z
?7(z, v, w) -> z
sub(s(v), s(w)) -> ?7(sub(v, w), v, w)
get(cons(y, ys)) -> tp2(y, ys)
?1(tp2(y, zs), x', xs') -> tp2(y, cons(x', zs))
get(cons(x', xs')) -> ?1(get(xs'), x', xs')
DP Processor:
DPs:
?5#(w,y',ws,v) -> ssp'#(ws,w)
?5#(w,y',ws,v) -> ?6#(ssp'(ws,w),y',ws,v,w)
ssp'#(cons(y',ws),v) -> sub#(v,y')
ssp'#(cons(y',ws),v) -> ?5#(sub(v,y'),y',ws,v)
?3#(w,y',xs',v,zs,x') -> ssp'#(cons(x',zs),w)
?3#(w,y',xs',v,zs,x') -> ?4#(ssp'(cons(x',zs),w),y',xs',w,v,zs,x')
?2#(tp2(y',zs),x',xs',v) -> sub#(v,y')
?2#(tp2(y',zs),x',xs',v) -> ?3#(sub(v,y'),y',xs',v,zs,x')
ssp'#(cons(x',xs'),v) -> get#(xs')
ssp'#(cons(x',xs'),v) -> ?2#(get(xs'),x',xs',v)
sub#(s(v),s(w)) -> sub#(v,w)
sub#(s(v),s(w)) -> ?7#(sub(v,w),v,w)
get#(cons(x',xs')) -> get#(xs')
get#(cons(x',xs')) -> ?1#(get(xs'),x',xs')
TRS:
ssp'(xs,0()) -> nil()
?6(ys',y',ws,v,w) -> cons(y',ys')
?5(w,y',ws,v) -> ?6(ssp'(ws,w),y',ws,v,w)
ssp'(cons(y',ws),v) -> ?5(sub(v,y'),y',ws,v)
?4(ys',y',xs',w,v,zs,x') -> cons(y',ys')
?3(w,y',xs',v,zs,x') -> ?4(ssp'(cons(x',zs),w),y',xs',w,v,zs,x')
?2(tp2(y',zs),x',xs',v) -> ?3(sub(v,y'),y',xs',v,zs,x')
ssp'(cons(x',xs'),v) -> ?2(get(xs'),x',xs',v)
sub(z,0()) -> z
?7(z,v,w) -> z
sub(s(v),s(w)) -> ?7(sub(v,w),v,w)
get(cons(y,ys)) -> tp2(y,ys)
?1(tp2(y,zs),x',xs') -> tp2(y,cons(x',zs))
get(cons(x',xs')) -> ?1(get(xs'),x',xs')
TDG Processor:
DPs:
?5#(w,y',ws,v) -> ssp'#(ws,w)
?5#(w,y',ws,v) -> ?6#(ssp'(ws,w),y',ws,v,w)
ssp'#(cons(y',ws),v) -> sub#(v,y')
ssp'#(cons(y',ws),v) -> ?5#(sub(v,y'),y',ws,v)
?3#(w,y',xs',v,zs,x') -> ssp'#(cons(x',zs),w)
?3#(w,y',xs',v,zs,x') -> ?4#(ssp'(cons(x',zs),w),y',xs',w,v,zs,x')
?2#(tp2(y',zs),x',xs',v) -> sub#(v,y')
?2#(tp2(y',zs),x',xs',v) -> ?3#(sub(v,y'),y',xs',v,zs,x')
ssp'#(cons(x',xs'),v) -> get#(xs')
ssp'#(cons(x',xs'),v) -> ?2#(get(xs'),x',xs',v)
sub#(s(v),s(w)) -> sub#(v,w)
sub#(s(v),s(w)) -> ?7#(sub(v,w),v,w)
get#(cons(x',xs')) -> get#(xs')
get#(cons(x',xs')) -> ?1#(get(xs'),x',xs')
TRS:
ssp'(xs,0()) -> nil()
?6(ys',y',ws,v,w) -> cons(y',ys')
?5(w,y',ws,v) -> ?6(ssp'(ws,w),y',ws,v,w)
ssp'(cons(y',ws),v) -> ?5(sub(v,y'),y',ws,v)
?4(ys',y',xs',w,v,zs,x') -> cons(y',ys')
?3(w,y',xs',v,zs,x') -> ?4(ssp'(cons(x',zs),w),y',xs',w,v,zs,x')
?2(tp2(y',zs),x',xs',v) -> ?3(sub(v,y'),y',xs',v,zs,x')
ssp'(cons(x',xs'),v) -> ?2(get(xs'),x',xs',v)
sub(z,0()) -> z
?7(z,v,w) -> z
sub(s(v),s(w)) -> ?7(sub(v,w),v,w)
get(cons(y,ys)) -> tp2(y,ys)
?1(tp2(y,zs),x',xs') -> tp2(y,cons(x',zs))
get(cons(x',xs')) -> ?1(get(xs'),x',xs')
graph:
get#(cons(x',xs')) -> get#(xs') ->
get#(cons(x',xs')) -> ?1#(get(xs'),x',xs')
get#(cons(x',xs')) -> get#(xs') ->
get#(cons(x',xs')) -> get#(xs')
?2#(tp2(y',zs),x',xs',v) -> ?3#(sub(v,y'),y',xs',v,zs,x') ->
?3#(w,y',xs',v,zs,x') -> ?4#(ssp'(cons(x',zs),w),y',xs',w,v,zs,x')
?2#(tp2(y',zs),x',xs',v) -> ?3#(sub(v,y'),y',xs',v,zs,x') ->
?3#(w,y',xs',v,zs,x') -> ssp'#(cons(x',zs),w)
?2#(tp2(y',zs),x',xs',v) -> sub#(v,y') ->
sub#(s(v),s(w)) -> ?7#(sub(v,w),v,w)
?2#(tp2(y',zs),x',xs',v) -> sub#(v,y') ->
sub#(s(v),s(w)) -> sub#(v,w)
?3#(w,y',xs',v,zs,x') -> ssp'#(cons(x',zs),w) ->
ssp'#(cons(x',xs'),v) -> ?2#(get(xs'),x',xs',v)
?3#(w,y',xs',v,zs,x') -> ssp'#(cons(x',zs),w) ->
ssp'#(cons(x',xs'),v) -> get#(xs')
?3#(w,y',xs',v,zs,x') -> ssp'#(cons(x',zs),w) ->
ssp'#(cons(y',ws),v) -> ?5#(sub(v,y'),y',ws,v)
?3#(w,y',xs',v,zs,x') -> ssp'#(cons(x',zs),w) ->
ssp'#(cons(y',ws),v) -> sub#(v,y')
sub#(s(v),s(w)) -> sub#(v,w) ->
sub#(s(v),s(w)) -> ?7#(sub(v,w),v,w)
sub#(s(v),s(w)) -> sub#(v,w) -> sub#(s(v),s(w)) -> sub#(v,w)
?5#(w,y',ws,v) -> ssp'#(ws,w) ->
ssp'#(cons(x',xs'),v) -> ?2#(get(xs'),x',xs',v)
?5#(w,y',ws,v) -> ssp'#(ws,w) ->
ssp'#(cons(x',xs'),v) -> get#(xs')
?5#(w,y',ws,v) -> ssp'#(ws,w) ->
ssp'#(cons(y',ws),v) -> ?5#(sub(v,y'),y',ws,v)
?5#(w,y',ws,v) -> ssp'#(ws,w) ->
ssp'#(cons(y',ws),v) -> sub#(v,y')
ssp'#(cons(x',xs'),v) -> get#(xs') ->
get#(cons(x',xs')) -> ?1#(get(xs'),x',xs')
ssp'#(cons(x',xs'),v) -> get#(xs') ->
get#(cons(x',xs')) -> get#(xs')
ssp'#(cons(x',xs'),v) -> ?2#(get(xs'),x',xs',v) ->
?2#(tp2(y',zs),x',xs',v) -> ?3#(sub(v,y'),y',xs',v,zs,x')
ssp'#(cons(x',xs'),v) -> ?2#(get(xs'),x',xs',v) ->
?2#(tp2(y',zs),x',xs',v) -> sub#(v,y')
ssp'#(cons(y',ws),v) -> sub#(v,y') ->
sub#(s(v),s(w)) -> ?7#(sub(v,w),v,w)
ssp'#(cons(y',ws),v) -> sub#(v,y') ->
sub#(s(v),s(w)) -> sub#(v,w)
ssp'#(cons(y',ws),v) -> ?5#(sub(v,y'),y',ws,v) ->
?5#(w,y',ws,v) -> ?6#(ssp'(ws,w),y',ws,v,w)
ssp'#(cons(y',ws),v) -> ?5#(sub(v,y'),y',ws,v) -> ?5#(w,y',ws,v) -> ssp'#(ws,w)
SCC Processor:
#sccs: 3
#rules: 7
#arcs: 24/196
DPs:
?2#(tp2(y',zs),x',xs',v) -> ?3#(sub(v,y'),y',xs',v,zs,x')
?3#(w,y',xs',v,zs,x') -> ssp'#(cons(x',zs),w)
ssp'#(cons(y',ws),v) -> ?5#(sub(v,y'),y',ws,v)
?5#(w,y',ws,v) -> ssp'#(ws,w)
ssp'#(cons(x',xs'),v) -> ?2#(get(xs'),x',xs',v)
TRS:
ssp'(xs,0()) -> nil()
?6(ys',y',ws,v,w) -> cons(y',ys')
?5(w,y',ws,v) -> ?6(ssp'(ws,w),y',ws,v,w)
ssp'(cons(y',ws),v) -> ?5(sub(v,y'),y',ws,v)
?4(ys',y',xs',w,v,zs,x') -> cons(y',ys')
?3(w,y',xs',v,zs,x') -> ?4(ssp'(cons(x',zs),w),y',xs',w,v,zs,x')
?2(tp2(y',zs),x',xs',v) -> ?3(sub(v,y'),y',xs',v,zs,x')
ssp'(cons(x',xs'),v) -> ?2(get(xs'),x',xs',v)
sub(z,0()) -> z
?7(z,v,w) -> z
sub(s(v),s(w)) -> ?7(sub(v,w),v,w)
get(cons(y,ys)) -> tp2(y,ys)
?1(tp2(y,zs),x',xs') -> tp2(y,cons(x',zs))
get(cons(x',xs')) -> ?1(get(xs'),x',xs')
Usable Rule Processor:
DPs:
?2#(tp2(y',zs),x',xs',v) -> ?3#(sub(v,y'),y',xs',v,zs,x')
?3#(w,y',xs',v,zs,x') -> ssp'#(cons(x',zs),w)
ssp'#(cons(y',ws),v) -> ?5#(sub(v,y'),y',ws,v)
?5#(w,y',ws,v) -> ssp'#(ws,w)
ssp'#(cons(x',xs'),v) -> ?2#(get(xs'),x',xs',v)
TRS:
sub(z,0()) -> z
sub(s(v),s(w)) -> ?7(sub(v,w),v,w)
?7(z,v,w) -> z
get(cons(y,ys)) -> tp2(y,ys)
get(cons(x',xs')) -> ?1(get(xs'),x',xs')
?1(tp2(y,zs),x',xs') -> tp2(y,cons(x',zs))
Matrix Interpretation Processor: dim=2
usable rules:
get(cons(y,ys)) -> tp2(y,ys)
get(cons(x',xs')) -> ?1(get(xs'),x',xs')
?1(tp2(y,zs),x',xs') -> tp2(y,cons(x',zs))
interpretation:
[1 2] [0]
[cons](x0, x1) = [1 0]x0 + x1 + [1],
[ssp'#](x0, x1) = [0 2]x0,
[?2#](x0, x1, x2, x3) = [2 0]x0 + [2 0]x1,
[?5#](x0, x1, x2, x3) = [1 0]x1 + [0 2]x2 + [2],
[1]
[0] = [0],
[?3#](x0, x1, x2, x3, x4, x5) = [0 2]x4 + [2 0]x5 + [2],
[1 0] [1 0] [0 0] [1]
[?1](x0, x1, x2) = [0 0]x0 + [1 0]x1 + [1 0]x2 + [2],
[0 2] [0 0] [0 1]
[?7](x0, x1, x2) = [1 2]x0 + [1 0]x1 + [0 0]x2,
[0 1] [1]
[get](x0) = [1 0]x0 + [2],
[0 1] [1]
[tp2](x0, x1) = [0 0]x1 + [0],
[0 1]
[s](x0) = [0 2]x0,
[0 0] [0 1] [3]
[sub](x0, x1) = [1 0]x0 + [1 0]x1 + [0]
orientation:
?2#(tp2(y',zs),x',xs',v) = [2 0]x' + [0 2]zs + [2] >= [2 0]x' + [0 2]zs + [2] = ?3#(sub(v,y'),y',xs',v,zs,x')
?3#(w,y',xs',v,zs,x') = [2 0]x' + [0 2]zs + [2] >= [2 0]x' + [0 2]zs + [2] = ssp'#(cons(x',zs),w)
ssp'#(cons(y',ws),v) = [0 2]ws + [2 0]y' + [2] >= [0 2]ws + [1 0]y' + [2] = ?5#(sub(v,y'),y',ws,v)
?5#(w,y',ws,v) = [0 2]ws + [1 0]y' + [2] >= [0 2]ws = ssp'#(ws,w)
ssp'#(cons(x',xs'),v) = [2 0]x' + [0 2]xs' + [2] >= [2 0]x' + [0 2]xs' + [2] = ?2#(get(xs'),x',xs',v)
[0 0] [3]
sub(z,0()) = [1 0]z + [1] >= z = z
[0 0] [0 2] [3] [2 0] [2 1] [0]
sub(s(v),s(w)) = [0 1]v + [0 1]w + [0] >= [3 0]v + [2 1]w + [3] = ?7(sub(v,w),v,w)
[0 0] [0 1] [0 2]
?7(z,v,w) = [1 0]v + [0 0]w + [1 2]z >= z = z
[1 0] [0 1] [2] [0 1] [1]
get(cons(y,ys)) = [1 2]y + [1 0]ys + [2] >= [0 0]ys + [0] = tp2(y,ys)
[1 0] [0 1] [2] [1 0] [0 1] [2]
get(cons(x',xs')) = [1 2]x' + [1 0]xs' + [2] >= [1 0]x' + [1 0]xs' + [2] = ?1(get(xs'),x',xs')
[1 0] [0 0] [0 1] [2] [1 0] [0 1] [2]
?1(tp2(y,zs),x',xs') = [1 0]x' + [1 0]xs' + [0 0]zs + [2] >= [0 0]x' + [0 0]zs + [0] = tp2(y,cons(x',zs))
problem:
DPs:
?2#(tp2(y',zs),x',xs',v) -> ?3#(sub(v,y'),y',xs',v,zs,x')
?3#(w,y',xs',v,zs,x') -> ssp'#(cons(x',zs),w)
ssp'#(cons(y',ws),v) -> ?5#(sub(v,y'),y',ws,v)
ssp'#(cons(x',xs'),v) -> ?2#(get(xs'),x',xs',v)
TRS:
sub(z,0()) -> z
sub(s(v),s(w)) -> ?7(sub(v,w),v,w)
?7(z,v,w) -> z
get(cons(y,ys)) -> tp2(y,ys)
get(cons(x',xs')) -> ?1(get(xs'),x',xs')
?1(tp2(y,zs),x',xs') -> tp2(y,cons(x',zs))
Restore Modifier:
DPs:
?2#(tp2(y',zs),x',xs',v) -> ?3#(sub(v,y'),y',xs',v,zs,x')
?3#(w,y',xs',v,zs,x') -> ssp'#(cons(x',zs),w)
ssp'#(cons(y',ws),v) -> ?5#(sub(v,y'),y',ws,v)
ssp'#(cons(x',xs'),v) -> ?2#(get(xs'),x',xs',v)
TRS:
ssp'(xs,0()) -> nil()
?6(ys',y',ws,v,w) -> cons(y',ys')
?5(w,y',ws,v) -> ?6(ssp'(ws,w),y',ws,v,w)
ssp'(cons(y',ws),v) -> ?5(sub(v,y'),y',ws,v)
?4(ys',y',xs',w,v,zs,x') -> cons(y',ys')
?3(w,y',xs',v,zs,x') -> ?4(ssp'(cons(x',zs),w),y',xs',w,v,zs,x')
?2(tp2(y',zs),x',xs',v) -> ?3(sub(v,y'),y',xs',v,zs,x')
ssp'(cons(x',xs'),v) -> ?2(get(xs'),x',xs',v)
sub(z,0()) -> z
?7(z,v,w) -> z
sub(s(v),s(w)) -> ?7(sub(v,w),v,w)
get(cons(y,ys)) -> tp2(y,ys)
?1(tp2(y,zs),x',xs') -> tp2(y,cons(x',zs))
get(cons(x',xs')) -> ?1(get(xs'),x',xs')
EDG Processor:
DPs:
?2#(tp2(y',zs),x',xs',v) -> ?3#(sub(v,y'),y',xs',v,zs,x')
?3#(w,y',xs',v,zs,x') -> ssp'#(cons(x',zs),w)
ssp'#(cons(y',ws),v) -> ?5#(sub(v,y'),y',ws,v)
ssp'#(cons(x',xs'),v) -> ?2#(get(xs'),x',xs',v)
TRS:
ssp'(xs,0()) -> nil()
?6(ys',y',ws,v,w) -> cons(y',ys')
?5(w,y',ws,v) -> ?6(ssp'(ws,w),y',ws,v,w)
ssp'(cons(y',ws),v) -> ?5(sub(v,y'),y',ws,v)
?4(ys',y',xs',w,v,zs,x') -> cons(y',ys')
?3(w,y',xs',v,zs,x') -> ?4(ssp'(cons(x',zs),w),y',xs',w,v,zs,x')
?2(tp2(y',zs),x',xs',v) -> ?3(sub(v,y'),y',xs',v,zs,x')
ssp'(cons(x',xs'),v) -> ?2(get(xs'),x',xs',v)
sub(z,0()) -> z
?7(z,v,w) -> z
sub(s(v),s(w)) -> ?7(sub(v,w),v,w)
get(cons(y,ys)) -> tp2(y,ys)
?1(tp2(y,zs),x',xs') -> tp2(y,cons(x',zs))
get(cons(x',xs')) -> ?1(get(xs'),x',xs')
graph:
?2#(tp2(y',zs),x',xs',v) -> ?3#(sub(v,y'),y',xs',v,zs,x') ->
?3#(w,y',xs',v,zs,x') -> ssp'#(cons(x',zs),w)
?3#(w,y',xs',v,zs,x') -> ssp'#(cons(x',zs),w) ->
ssp'#(cons(y',ws),v) -> ?5#(sub(v,y'),y',ws,v)
?3#(w,y',xs',v,zs,x') -> ssp'#(cons(x',zs),w) ->
ssp'#(cons(x',xs'),v) -> ?2#(get(xs'),x',xs',v)
ssp'#(cons(x',xs'),v) -> ?2#(get(xs'),x',xs',v) ->
?2#(tp2(y',zs),x',xs',v) -> ?3#(sub(v,y'),y',xs',v,zs,x')
SCC Processor:
#sccs: 1
#rules: 3
#arcs: 4/16
DPs:
?2#(tp2(y',zs),x',xs',v) -> ?3#(sub(v,y'),y',xs',v,zs,x')
?3#(w,y',xs',v,zs,x') -> ssp'#(cons(x',zs),w)
ssp'#(cons(x',xs'),v) -> ?2#(get(xs'),x',xs',v)
TRS:
ssp'(xs,0()) -> nil()
?6(ys',y',ws,v,w) -> cons(y',ys')
?5(w,y',ws,v) -> ?6(ssp'(ws,w),y',ws,v,w)
ssp'(cons(y',ws),v) -> ?5(sub(v,y'),y',ws,v)
?4(ys',y',xs',w,v,zs,x') -> cons(y',ys')
?3(w,y',xs',v,zs,x') -> ?4(ssp'(cons(x',zs),w),y',xs',w,v,zs,x')
?2(tp2(y',zs),x',xs',v) -> ?3(sub(v,y'),y',xs',v,zs,x')
ssp'(cons(x',xs'),v) -> ?2(get(xs'),x',xs',v)
sub(z,0()) -> z
?7(z,v,w) -> z
sub(s(v),s(w)) -> ?7(sub(v,w),v,w)
get(cons(y,ys)) -> tp2(y,ys)
?1(tp2(y,zs),x',xs') -> tp2(y,cons(x',zs))
get(cons(x',xs')) -> ?1(get(xs'),x',xs')
Usable Rule Processor:
DPs:
?2#(tp2(y',zs),x',xs',v) -> ?3#(sub(v,y'),y',xs',v,zs,x')
?3#(w,y',xs',v,zs,x') -> ssp'#(cons(x',zs),w)
ssp'#(cons(x',xs'),v) -> ?2#(get(xs'),x',xs',v)
TRS:
sub(z,0()) -> z
sub(s(v),s(w)) -> ?7(sub(v,w),v,w)
?7(z,v,w) -> z
get(cons(y,ys)) -> tp2(y,ys)
get(cons(x',xs')) -> ?1(get(xs'),x',xs')
?1(tp2(y,zs),x',xs') -> tp2(y,cons(x',zs))
Matrix Interpretation Processor: dim=2
usable rules:
get(cons(y,ys)) -> tp2(y,ys)
get(cons(x',xs')) -> ?1(get(xs'),x',xs')
?1(tp2(y,zs),x',xs') -> tp2(y,cons(x',zs))
interpretation:
[1 0] [1]
[cons](x0, x1) = [2 0]x1 + [0],
[ssp'#](x0, x1) = [0 1]x0 + [2],
[?2#](x0, x1, x2, x3) = [2 0]x0 + [1],
[0]
[0] = [2],
[?3#](x0, x1, x2, x3, x4, x5) = [2 0]x4 + [3],
[1 0] [1]
[?1](x0, x1, x2) = [2 0]x0 + [0],
[0 0] [0 2] [1 2] [1]
[?7](x0, x1, x2) = [0 1]x0 + [0 0]x1 + [1 0]x2 + [0],
[get](x0) = x0,
[1 0] [1]
[tp2](x0, x1) = [2 0]x1 + [0],
[0 0] [0]
[s](x0) = [1 0]x0 + [1],
[0 1] [0 1] [1]
[sub](x0, x1) = [0 2]x0 + [1 0]x1 + [0]
orientation:
?2#(tp2(y',zs),x',xs',v) = [2 0]zs + [3] >= [2 0]zs + [3] = ?3#(sub(v,y'),y',xs',v,zs,x')
?3#(w,y',xs',v,zs,x') = [2 0]zs + [3] >= [2 0]zs + [2] = ssp'#(cons(x',zs),w)
ssp'#(cons(x',xs'),v) = [2 0]xs' + [2] >= [2 0]xs' + [1] = ?2#(get(xs'),x',xs',v)
[0 1] [3]
sub(z,0()) = [0 2]z + [0] >= z = z
[1 0] [1 0] [3] [0 2] [1 2] [1]
sub(s(v),s(w)) = [2 0]v + [0 0]w + [2] >= [0 2]v + [2 0]w + [0] = ?7(sub(v,w),v,w)
[0 2] [1 2] [0 0] [1]
?7(z,v,w) = [0 0]v + [1 0]w + [0 1]z + [0] >= z = z
[1 0] [1] [1 0] [1]
get(cons(y,ys)) = [2 0]ys + [0] >= [2 0]ys + [0] = tp2(y,ys)
[1 0] [1] [1 0] [1]
get(cons(x',xs')) = [2 0]xs' + [0] >= [2 0]xs' + [0] = ?1(get(xs'),x',xs')
[1 0] [2] [1 0] [2]
?1(tp2(y,zs),x',xs') = [2 0]zs + [2] >= [2 0]zs + [2] = tp2(y,cons(x',zs))
problem:
DPs:
?2#(tp2(y',zs),x',xs',v) -> ?3#(sub(v,y'),y',xs',v,zs,x')
TRS:
sub(z,0()) -> z
sub(s(v),s(w)) -> ?7(sub(v,w),v,w)
?7(z,v,w) -> z
get(cons(y,ys)) -> tp2(y,ys)
get(cons(x',xs')) -> ?1(get(xs'),x',xs')
?1(tp2(y,zs),x',xs') -> tp2(y,cons(x',zs))
Restore Modifier:
DPs:
?2#(tp2(y',zs),x',xs',v) -> ?3#(sub(v,y'),y',xs',v,zs,x')
TRS:
ssp'(xs,0()) -> nil()
?6(ys',y',ws,v,w) -> cons(y',ys')
?5(w,y',ws,v) -> ?6(ssp'(ws,w),y',ws,v,w)
ssp'(cons(y',ws),v) -> ?5(sub(v,y'),y',ws,v)
?4(ys',y',xs',w,v,zs,x') -> cons(y',ys')
?3(w,y',xs',v,zs,x') -> ?4(ssp'(cons(x',zs),w),y',xs',w,v,zs,x')
?2(tp2(y',zs),x',xs',v) -> ?3(sub(v,y'),y',xs',v,zs,x')
ssp'(cons(x',xs'),v) -> ?2(get(xs'),x',xs',v)
sub(z,0()) -> z
?7(z,v,w) -> z
sub(s(v),s(w)) -> ?7(sub(v,w),v,w)
get(cons(y,ys)) -> tp2(y,ys)
?1(tp2(y,zs),x',xs') -> tp2(y,cons(x',zs))
get(cons(x',xs')) -> ?1(get(xs'),x',xs')
EDG Processor:
DPs:
?2#(tp2(y',zs),x',xs',v) -> ?3#(sub(v,y'),y',xs',v,zs,x')
TRS:
ssp'(xs,0()) -> nil()
?6(ys',y',ws,v,w) -> cons(y',ys')
?5(w,y',ws,v) -> ?6(ssp'(ws,w),y',ws,v,w)
ssp'(cons(y',ws),v) -> ?5(sub(v,y'),y',ws,v)
?4(ys',y',xs',w,v,zs,x') -> cons(y',ys')
?3(w,y',xs',v,zs,x') -> ?4(ssp'(cons(x',zs),w),y',xs',w,v,zs,x')
?2(tp2(y',zs),x',xs',v) -> ?3(sub(v,y'),y',xs',v,zs,x')
ssp'(cons(x',xs'),v) -> ?2(get(xs'),x',xs',v)
sub(z,0()) -> z
?7(z,v,w) -> z
sub(s(v),s(w)) -> ?7(sub(v,w),v,w)
get(cons(y,ys)) -> tp2(y,ys)
?1(tp2(y,zs),x',xs') -> tp2(y,cons(x',zs))
get(cons(x',xs')) -> ?1(get(xs'),x',xs')
graph:
Qed
DPs:
sub#(s(v),s(w)) -> sub#(v,w)
TRS:
ssp'(xs,0()) -> nil()
?6(ys',y',ws,v,w) -> cons(y',ys')
?5(w,y',ws,v) -> ?6(ssp'(ws,w),y',ws,v,w)
ssp'(cons(y',ws),v) -> ?5(sub(v,y'),y',ws,v)
?4(ys',y',xs',w,v,zs,x') -> cons(y',ys')
?3(w,y',xs',v,zs,x') -> ?4(ssp'(cons(x',zs),w),y',xs',w,v,zs,x')
?2(tp2(y',zs),x',xs',v) -> ?3(sub(v,y'),y',xs',v,zs,x')
ssp'(cons(x',xs'),v) -> ?2(get(xs'),x',xs',v)
sub(z,0()) -> z
?7(z,v,w) -> z
sub(s(v),s(w)) -> ?7(sub(v,w),v,w)
get(cons(y,ys)) -> tp2(y,ys)
?1(tp2(y,zs),x',xs') -> tp2(y,cons(x',zs))
get(cons(x',xs')) -> ?1(get(xs'),x',xs')
Subterm Criterion Processor:
simple projection:
pi(sub#) = 0
problem:
DPs:
TRS:
ssp'(xs,0()) -> nil()
?6(ys',y',ws,v,w) -> cons(y',ys')
?5(w,y',ws,v) -> ?6(ssp'(ws,w),y',ws,v,w)
ssp'(cons(y',ws),v) -> ?5(sub(v,y'),y',ws,v)
?4(ys',y',xs',w,v,zs,x') -> cons(y',ys')
?3(w,y',xs',v,zs,x') -> ?4(ssp'(cons(x',zs),w),y',xs',w,v,zs,x')
?2(tp2(y',zs),x',xs',v) -> ?3(sub(v,y'),y',xs',v,zs,x')
ssp'(cons(x',xs'),v) -> ?2(get(xs'),x',xs',v)
sub(z,0()) -> z
?7(z,v,w) -> z
sub(s(v),s(w)) -> ?7(sub(v,w),v,w)
get(cons(y,ys)) -> tp2(y,ys)
?1(tp2(y,zs),x',xs') -> tp2(y,cons(x',zs))
get(cons(x',xs')) -> ?1(get(xs'),x',xs')
Qed
DPs:
get#(cons(x',xs')) -> get#(xs')
TRS:
ssp'(xs,0()) -> nil()
?6(ys',y',ws,v,w) -> cons(y',ys')
?5(w,y',ws,v) -> ?6(ssp'(ws,w),y',ws,v,w)
ssp'(cons(y',ws),v) -> ?5(sub(v,y'),y',ws,v)
?4(ys',y',xs',w,v,zs,x') -> cons(y',ys')
?3(w,y',xs',v,zs,x') -> ?4(ssp'(cons(x',zs),w),y',xs',w,v,zs,x')
?2(tp2(y',zs),x',xs',v) -> ?3(sub(v,y'),y',xs',v,zs,x')
ssp'(cons(x',xs'),v) -> ?2(get(xs'),x',xs',v)
sub(z,0()) -> z
?7(z,v,w) -> z
sub(s(v),s(w)) -> ?7(sub(v,w),v,w)
get(cons(y,ys)) -> tp2(y,ys)
?1(tp2(y,zs),x',xs') -> tp2(y,cons(x',zs))
get(cons(x',xs')) -> ?1(get(xs'),x',xs')
Subterm Criterion Processor:
simple projection:
pi(get#) = 0
problem:
DPs:
TRS:
ssp'(xs,0()) -> nil()
?6(ys',y',ws,v,w) -> cons(y',ys')
?5(w,y',ws,v) -> ?6(ssp'(ws,w),y',ws,v,w)
ssp'(cons(y',ws),v) -> ?5(sub(v,y'),y',ws,v)
?4(ys',y',xs',w,v,zs,x') -> cons(y',ys')
?3(w,y',xs',v,zs,x') -> ?4(ssp'(cons(x',zs),w),y',xs',w,v,zs,x')
?2(tp2(y',zs),x',xs',v) -> ?3(sub(v,y'),y',xs',v,zs,x')
ssp'(cons(x',xs'),v) -> ?2(get(xs'),x',xs',v)
sub(z,0()) -> z
?7(z,v,w) -> z
sub(s(v),s(w)) -> ?7(sub(v,w),v,w)
get(cons(y,ys)) -> tp2(y,ys)
?1(tp2(y,zs),x',xs') -> tp2(y,cons(x',zs))
get(cons(x',xs')) -> ?1(get(xs'),x',xs')
Qed