YES
Proof:
This system is confluent.
By \cite{ALS94}, Theorem 4.1.
This system is of type 3 or smaller.
This system is strongly deterministic.
All 2 critical pairs are joinable.
pair(0, s(x)) = pair(s(y), $1) <= lt(x, $2) = false, div(m(x, $2), s($2)) = pair(y, $1), lt(x, $2) = true:
This critical pair is unfeasible.
pair(s(x), y) = pair(0, s($1)) <= lt($1, $2) = true, lt($1, $2) = false, div(m($1, $2), s($2)) = pair(x, y):
This critical pair is unfeasible.
This system is of type 3 or smaller.
This system is deterministic.
Call external tool:
ttt2 - trs 30
Input:
lt(x, 0) -> false
lt(0, s(x)) -> true
lt(s(x), s(y)) -> lt(x, y)
m(0, s(y)) -> 0
m(x, 0) -> x
m(s(x), s(y)) -> m(x, y)
div(0, s(x)) -> pair(0, 0)
div(s(x), s(y)) -> pair(0, s(x))
div(s(x), s(y)) -> lt(x, y)
div(s(x), s(y)) -> pair(s(div(m(x, y), s(y))), div(m(x, y), s(y)))
div(s(x), s(y)) -> div(m(x, y), s(y))
m(x, y) -> x
m(x, y) -> y
pair(x, y) -> x
pair(x, y) -> y
s(x) -> x
div(x, y) -> x
div(x, y) -> y
lt(x, y) -> x
lt(x, y) -> y
Unfolding Processor:
loop length: 2
terms:
div(s(x588),s(s(x588)))
pair(s(div(m(x588,s(x588)),s(s(x588)))),div(m(x588,s(x588)),s(s(x588))))
context: pair(s([]),div(m(x588,s(x588)),s(s(x588))))
substitution:
x588 -> x588
Qed
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 optimized U(R).
Call external tool:
ttt2 - trs 30
Input:
lt(x, 0) -> false
lt(0, s(x)) -> true
lt(s(x), s(y)) -> lt(x, y)
m(0, s(y)) -> 0
m(x, 0) -> x
m(s(x), s(y)) -> m(x, y)
div(0, s(x)) -> pair(0, 0)
?2(true, x, y) -> pair(0, s(x))
div(s(x), s(y)) -> ?2(lt(x, y), x, y)
?1(pair(q, r), x, y) -> pair(s(q), r)
?2(false, x, y) -> ?1(div(m(x, y), s(y)), x, y)
DP Processor:
DPs:
lt#(s(x),s(y)) -> lt#(x,y)
m#(s(x),s(y)) -> m#(x,y)
div#(s(x),s(y)) -> lt#(x,y)
div#(s(x),s(y)) -> ?2#(lt(x,y),x,y)
?2#(false(),x,y) -> m#(x,y)
?2#(false(),x,y) -> div#(m(x,y),s(y))
?2#(false(),x,y) -> ?1#(div(m(x,y),s(y)),x,y)
TRS:
lt(x,0()) -> false()
lt(0(),s(x)) -> true()
lt(s(x),s(y)) -> lt(x,y)
m(0(),s(y)) -> 0()
m(x,0()) -> x
m(s(x),s(y)) -> m(x,y)
div(0(),s(x)) -> pair(0(),0())
?2(true(),x,y) -> pair(0(),s(x))
div(s(x),s(y)) -> ?2(lt(x,y),x,y)
?1(pair(q,r),x,y) -> pair(s(q),r)
?2(false(),x,y) -> ?1(div(m(x,y),s(y)),x,y)
TDG Processor:
DPs:
lt#(s(x),s(y)) -> lt#(x,y)
m#(s(x),s(y)) -> m#(x,y)
div#(s(x),s(y)) -> lt#(x,y)
div#(s(x),s(y)) -> ?2#(lt(x,y),x,y)
?2#(false(),x,y) -> m#(x,y)
?2#(false(),x,y) -> div#(m(x,y),s(y))
?2#(false(),x,y) -> ?1#(div(m(x,y),s(y)),x,y)
TRS:
lt(x,0()) -> false()
lt(0(),s(x)) -> true()
lt(s(x),s(y)) -> lt(x,y)
m(0(),s(y)) -> 0()
m(x,0()) -> x
m(s(x),s(y)) -> m(x,y)
div(0(),s(x)) -> pair(0(),0())
?2(true(),x,y) -> pair(0(),s(x))
div(s(x),s(y)) -> ?2(lt(x,y),x,y)
?1(pair(q,r),x,y) -> pair(s(q),r)
?2(false(),x,y) -> ?1(div(m(x,y),s(y)),x,y)
graph:
?2#(false(),x,y) -> div#(m(x,y),s(y)) ->
div#(s(x),s(y)) -> ?2#(lt(x,y),x,y)
?2#(false(),x,y) -> div#(m(x,y),s(y)) -> div#(s(x),s(y)) -> lt#(x,y)
?2#(false(),x,y) -> m#(x,y) -> m#(s(x),s(y)) -> m#(x,y)
div#(s(x),s(y)) -> ?2#(lt(x,y),x,y) ->
?2#(false(),x,y) -> ?1#(div(m(x,y),s(y)),x,y)
div#(s(x),s(y)) -> ?2#(lt(x,y),x,y) ->
?2#(false(),x,y) -> div#(m(x,y),s(y))
div#(s(x),s(y)) -> ?2#(lt(x,y),x,y) -> ?2#(false(),x,y) -> m#(x,y)
div#(s(x),s(y)) -> lt#(x,y) -> lt#(s(x),s(y)) -> lt#(x,y)
m#(s(x),s(y)) -> m#(x,y) -> m#(s(x),s(y)) -> m#(x,y)
lt#(s(x),s(y)) -> lt#(x,y) -> lt#(s(x),s(y)) -> lt#(x,y)
SCC Processor:
#sccs: 3
#rules: 4
#arcs: 9/49
DPs:
?2#(false(),x,y) -> div#(m(x,y),s(y))
div#(s(x),s(y)) -> ?2#(lt(x,y),x,y)
TRS:
lt(x,0()) -> false()
lt(0(),s(x)) -> true()
lt(s(x),s(y)) -> lt(x,y)
m(0(),s(y)) -> 0()
m(x,0()) -> x
m(s(x),s(y)) -> m(x,y)
div(0(),s(x)) -> pair(0(),0())
?2(true(),x,y) -> pair(0(),s(x))
div(s(x),s(y)) -> ?2(lt(x,y),x,y)
?1(pair(q,r),x,y) -> pair(s(q),r)
?2(false(),x,y) -> ?1(div(m(x,y),s(y)),x,y)
Usable Rule Processor:
DPs:
?2#(false(),x,y) -> div#(m(x,y),s(y))
div#(s(x),s(y)) -> ?2#(lt(x,y),x,y)
TRS:
m(0(),s(y)) -> 0()
m(x,0()) -> x
m(s(x),s(y)) -> m(x,y)
lt(x,0()) -> false()
lt(0(),s(x)) -> true()
lt(s(x),s(y)) -> lt(x,y)
Matrix Interpretation Processor: dim=2
usable rules:
m(0(),s(y)) -> 0()
m(x,0()) -> x
m(s(x),s(y)) -> m(x,y)
interpretation:
[0]
[true] = [0],
[0]
[lt](x0, x1) = [0],
[3 0] [1]
[s](x0) = [0 1]x0 + [0],
[1 0]
[m](x0, x1) = [1 2]x0,
[0]
[0] = [0],
[div#](x0, x1) = [1 0]x0 + [0 2]x1 + [2],
[?2#](x0, x1, x2) = [1 0]x1 + [0 2]x2 + [2],
[0]
[false] = [0]
orientation:
?2#(false(),x,y) = [1 0]x + [0 2]y + [2] >= [1 0]x + [0 2]y + [2] = div#(m(x,y),s(y))
div#(s(x),s(y)) = [3 0]x + [0 2]y + [3] >= [1 0]x + [0 2]y + [2] = ?2#(lt(x,y),x,y)
[0] [0]
m(0(),s(y)) = [0] >= [0] = 0()
[1 0]
m(x,0()) = [1 2]x >= x = x
[3 0] [1] [1 0]
m(s(x),s(y)) = [3 2]x + [1] >= [1 2]x = m(x,y)
[0] [0]
lt(x,0()) = [0] >= [0] = false()
[0] [0]
lt(0(),s(x)) = [0] >= [0] = true()
[0] [0]
lt(s(x),s(y)) = [0] >= [0] = lt(x,y)
problem:
DPs:
?2#(false(),x,y) -> div#(m(x,y),s(y))
TRS:
m(0(),s(y)) -> 0()
m(x,0()) -> x
m(s(x),s(y)) -> m(x,y)
lt(x,0()) -> false()
lt(0(),s(x)) -> true()
lt(s(x),s(y)) -> lt(x,y)
Restore Modifier:
DPs:
?2#(false(),x,y) -> div#(m(x,y),s(y))
TRS:
lt(x,0()) -> false()
lt(0(),s(x)) -> true()
lt(s(x),s(y)) -> lt(x,y)
m(0(),s(y)) -> 0()
m(x,0()) -> x
m(s(x),s(y)) -> m(x,y)
div(0(),s(x)) -> pair(0(),0())
?2(true(),x,y) -> pair(0(),s(x))
div(s(x),s(y)) -> ?2(lt(x,y),x,y)
?1(pair(q,r),x,y) -> pair(s(q),r)
?2(false(),x,y) -> ?1(div(m(x,y),s(y)),x,y)
EDG Processor:
DPs:
?2#(false(),x,y) -> div#(m(x,y),s(y))
TRS:
lt(x,0()) -> false()
lt(0(),s(x)) -> true()
lt(s(x),s(y)) -> lt(x,y)
m(0(),s(y)) -> 0()
m(x,0()) -> x
m(s(x),s(y)) -> m(x,y)
div(0(),s(x)) -> pair(0(),0())
?2(true(),x,y) -> pair(0(),s(x))
div(s(x),s(y)) -> ?2(lt(x,y),x,y)
?1(pair(q,r),x,y) -> pair(s(q),r)
?2(false(),x,y) -> ?1(div(m(x,y),s(y)),x,y)
graph:
Qed
DPs:
m#(s(x),s(y)) -> m#(x,y)
TRS:
lt(x,0()) -> false()
lt(0(),s(x)) -> true()
lt(s(x),s(y)) -> lt(x,y)
m(0(),s(y)) -> 0()
m(x,0()) -> x
m(s(x),s(y)) -> m(x,y)
div(0(),s(x)) -> pair(0(),0())
?2(true(),x,y) -> pair(0(),s(x))
div(s(x),s(y)) -> ?2(lt(x,y),x,y)
?1(pair(q,r),x,y) -> pair(s(q),r)
?2(false(),x,y) -> ?1(div(m(x,y),s(y)),x,y)
Subterm Criterion Processor:
simple projection:
pi(m#) = 0
problem:
DPs:
TRS:
lt(x,0()) -> false()
lt(0(),s(x)) -> true()
lt(s(x),s(y)) -> lt(x,y)
m(0(),s(y)) -> 0()
m(x,0()) -> x
m(s(x),s(y)) -> m(x,y)
div(0(),s(x)) -> pair(0(),0())
?2(true(),x,y) -> pair(0(),s(x))
div(s(x),s(y)) -> ?2(lt(x,y),x,y)
?1(pair(q,r),x,y) -> pair(s(q),r)
?2(false(),x,y) -> ?1(div(m(x,y),s(y)),x,y)
Qed
DPs:
lt#(s(x),s(y)) -> lt#(x,y)
TRS:
lt(x,0()) -> false()
lt(0(),s(x)) -> true()
lt(s(x),s(y)) -> lt(x,y)
m(0(),s(y)) -> 0()
m(x,0()) -> x
m(s(x),s(y)) -> m(x,y)
div(0(),s(x)) -> pair(0(),0())
?2(true(),x,y) -> pair(0(),s(x))
div(s(x),s(y)) -> ?2(lt(x,y),x,y)
?1(pair(q,r),x,y) -> pair(s(q),r)
?2(false(),x,y) -> ?1(div(m(x,y),s(y)),x,y)
Subterm Criterion Processor:
simple projection:
pi(lt#) = 0
problem:
DPs:
TRS:
lt(x,0()) -> false()
lt(0(),s(x)) -> true()
lt(s(x),s(y)) -> lt(x,y)
m(0(),s(y)) -> 0()
m(x,0()) -> x
m(s(x),s(y)) -> m(x,y)
div(0(),s(x)) -> pair(0(),0())
?2(true(),x,y) -> pair(0(),s(x))
div(s(x),s(y)) -> ?2(lt(x,y),x,y)
?1(pair(q,r),x,y) -> pair(s(q),r)
?2(false(),x,y) -> ?1(div(m(x,y),s(y)),x,y)
Qed