0 QTRS
↳1 DependencyPairsProof (⇔)
↳2 QDP
↳3 DependencyGraphProof (⇔)
↳4 QDP
↳5 QDPSizeChangeProof (⇔)
↳6 TRUE
app(id, x) → x
app(plus, 0) → id
app(app(plus, app(s, x)), y) → app(s, app(app(plus, x), y))
APP(app(plus, app(s, x)), y) → APP(s, app(app(plus, x), y))
APP(app(plus, app(s, x)), y) → APP(app(plus, x), y)
APP(app(plus, app(s, x)), y) → APP(plus, x)
app(id, x) → x
app(plus, 0) → id
app(app(plus, app(s, x)), y) → app(s, app(app(plus, x), y))
APP(app(plus, app(s, x)), y) → APP(app(plus, x), y)
app(id, x) → x
app(plus, 0) → id
app(app(plus, app(s, x)), y) → app(s, app(app(plus, x), y))
Order:Combined order from the following AFS and order.
app(x1, x2) = app(x2)
plus = plus
0 = 0
id = id
s = s
Recursive path order with status [RPO].
Quasi-Precedence:
app1 > [plus, 0, id]
app1: multiset
plus: multiset
0: multiset
id: multiset
s: multiset
AFS:
app(x1, x2) = app(x2)
plus = plus
0 = 0
id = id
s = s
From the DPs we obtained the following set of size-change graphs:
We oriented the following set of usable rules [AAECC05,FROCOS05].
app(plus, 0) → id