0 QTRS
↳1 DependencyPairsProof (⇔)
↳2 QDP
↳3 DependencyGraphProof (⇔)
↳4 QDP
↳5 QDPOrderProof (⇔)
↳6 QDP
↳7 QDPOrderProof (⇔)
↳8 QDP
↳9 QDPOrderProof (⇔)
↳10 QDP
↳11 PisEmptyProof (⇔)
↳12 TRUE
ack_in(0, n) → ack_out(s(n))
ack_in(s(m), 0) → u11(ack_in(m, s(0)))
u11(ack_out(n)) → ack_out(n)
ack_in(s(m), s(n)) → u21(ack_in(s(m), n), m)
u21(ack_out(n), m) → u22(ack_in(m, n))
u22(ack_out(n)) → ack_out(n)
ACK_IN(s(m), 0) → U11(ack_in(m, s(0)))
ACK_IN(s(m), 0) → ACK_IN(m, s(0))
ACK_IN(s(m), s(n)) → U21(ack_in(s(m), n), m)
ACK_IN(s(m), s(n)) → ACK_IN(s(m), n)
U21(ack_out(n), m) → U22(ack_in(m, n))
U21(ack_out(n), m) → ACK_IN(m, n)
ack_in(0, n) → ack_out(s(n))
ack_in(s(m), 0) → u11(ack_in(m, s(0)))
u11(ack_out(n)) → ack_out(n)
ack_in(s(m), s(n)) → u21(ack_in(s(m), n), m)
u21(ack_out(n), m) → u22(ack_in(m, n))
u22(ack_out(n)) → ack_out(n)
ACK_IN(s(m), s(n)) → U21(ack_in(s(m), n), m)
U21(ack_out(n), m) → ACK_IN(m, n)
ACK_IN(s(m), 0) → ACK_IN(m, s(0))
ACK_IN(s(m), s(n)) → ACK_IN(s(m), n)
ack_in(0, n) → ack_out(s(n))
ack_in(s(m), 0) → u11(ack_in(m, s(0)))
u11(ack_out(n)) → ack_out(n)
ack_in(s(m), s(n)) → u21(ack_in(s(m), n), m)
u21(ack_out(n), m) → u22(ack_in(m, n))
u22(ack_out(n)) → ack_out(n)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
ACK_IN(s(m), 0) → ACK_IN(m, s(0))
[ackout, 0, u22] > [s1, u111]
s1: multiset
ackout: []
0: multiset
u111: multiset
u22: []
ack_in(s(m), 0) → u11(ack_in(m, s(0)))
ack_in(s(m), s(n)) → u21(ack_in(s(m), n), m)
u21(ack_out(n), m) → u22(ack_in(m, n))
ack_in(0, n) → ack_out(s(n))
u11(ack_out(n)) → ack_out(n)
u22(ack_out(n)) → ack_out(n)
ACK_IN(s(m), s(n)) → U21(ack_in(s(m), n), m)
U21(ack_out(n), m) → ACK_IN(m, n)
ACK_IN(s(m), s(n)) → ACK_IN(s(m), n)
ack_in(0, n) → ack_out(s(n))
ack_in(s(m), 0) → u11(ack_in(m, s(0)))
u11(ack_out(n)) → ack_out(n)
ack_in(s(m), s(n)) → u21(ack_in(s(m), n), m)
u21(ack_out(n), m) → u22(ack_in(m, n))
u22(ack_out(n)) → ack_out(n)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
ACK_IN(s(m), s(n)) → U21(ack_in(s(m), n), m)
U21(ack_out(n), m) → ACK_IN(m, n)
[ackin2, ackout, u22] > 0 > u111 > s1
[ackin2, ackout, u22] > u21 > s1
s1: multiset
ackin2: multiset
ackout: multiset
0: multiset
u111: multiset
u21: multiset
u22: multiset
ACK_IN(s(m), s(n)) → ACK_IN(s(m), n)
ack_in(0, n) → ack_out(s(n))
ack_in(s(m), 0) → u11(ack_in(m, s(0)))
u11(ack_out(n)) → ack_out(n)
ack_in(s(m), s(n)) → u21(ack_in(s(m), n), m)
u21(ack_out(n), m) → u22(ack_in(m, n))
u22(ack_out(n)) → ack_out(n)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
ACK_IN(s(m), s(n)) → ACK_IN(s(m), n)
trivial
s1: multiset
ack_in(0, n) → ack_out(s(n))
ack_in(s(m), 0) → u11(ack_in(m, s(0)))
u11(ack_out(n)) → ack_out(n)
ack_in(s(m), s(n)) → u21(ack_in(s(m), n), m)
u21(ack_out(n), m) → u22(ack_in(m, n))
u22(ack_out(n)) → ack_out(n)