YES
0 QTRS
↳1 QTRSRRRProof (⇔, 0 ms)
↳2 QTRS
↳3 QTRSRRRProof (⇔, 6 ms)
↳4 QTRS
↳5 QTRSRRRProof (⇔, 0 ms)
↳6 QTRS
↳7 RisEmptyProof (⇔, 0 ms)
↳8 YES
app(nil, y) → y
app(add(n, x), y) → add(n, app(x, y))
reverse(nil) → nil
reverse(add(n, x)) → app(reverse(x), add(n, nil))
shuffle(nil) → nil
shuffle(add(n, x)) → add(n, shuffle(reverse(x)))
With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:
POL(add(x1, x2)) = 2 + x1 + x2
POL(app(x1, x2)) = x1 + x2
POL(nil) = 0
POL(reverse(x1)) = x1
POL(shuffle(x1)) = 2 + 2·x1
shuffle(nil) → nil
shuffle(add(n, x)) → add(n, shuffle(reverse(x)))
app(nil, y) → y
app(add(n, x), y) → add(n, app(x, y))
reverse(nil) → nil
reverse(add(n, x)) → app(reverse(x), add(n, nil))
With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:
POL(add(x1, x2)) = 2 + x1 + x2
POL(app(x1, x2)) = x1 + x2
POL(nil) = 0
POL(reverse(x1)) = 2 + 2·x1
reverse(nil) → nil
reverse(add(n, x)) → app(reverse(x), add(n, nil))
app(nil, y) → y
app(add(n, x), y) → add(n, app(x, y))
app2 > add2 > nil
nil=1
app_2=0
add_2=0
app(nil, y) → y
app(add(n, x), y) → add(n, app(x, y))