Termination w.r.t. Q of the given QTRS could be proven:

0 QTRS
  ↳1 QTRS Reverse (⇔)
    ↳2 QTRS
  ↳3 QTRS Reverse (⇔)
    ↳4 QTRS
  ↳5 QTRSRRRProof (⇔)
    ↳6 QTRS
    ↳7 DependencyPairsProof (⇔)
    ↳8 QDP
    ↳9 DependencyGraphProof (⇔)
    ↳10 AND
      ↳11 QDP
        ↳12 UsableRulesProof (⇔)
          ↳13 QDP
          ↳14 UsableRulesReductionPairsProof (⇔)
          ↳15 QDP
          ↳16 PisEmptyProof (⇔)
          ↳17 TRUE
        ↳18 UsableRulesProof (⇔)
          ↳19 QDP
      ↳20 QDP
        ↳21 UsableRulesProof (⇔)
          ↳22 QDP
          ↳23 UsableRulesReductionPairsProof (⇔)
          ↳24 QDP
          ↳25 PisEmptyProof (⇔)
          ↳26 TRUE
        ↳27 UsableRulesProof (⇔)
          ↳28 QDP
      ↳29 QDP
        ↳30 UsableRulesProof (⇔)
          ↳31 QDP
          ↳32 UsableRulesReductionPairsProof (⇔)
          ↳33 QDP
          ↳34 PisEmptyProof (⇔)
          ↳35 TRUE
        ↳36 UsableRulesProof (⇔)
          ↳37 QDP
      ↳38 QDP
        ↳39 UsableRulesProof (⇔)
          ↳40 QDP
          ↳41 UsableRulesReductionPairsProof (⇔)
          ↳42 QDP
          ↳43 PisEmptyProof (⇔)
          ↳44 TRUE
        ↳45 UsableRulesProof (⇔)
          ↳46 QDP
      ↳47 QDP
        ↳48 UsableRulesProof (⇔)
          ↳49 QDP
          ↳50 MRRProof (⇔)
          ↳51 QDP
          ↳52 MRRProof (⇔)
          ↳53 QDP
          ↳54 QDPOrderProof (⇔)
          ↳55 QDP
          ↳56 PisEmptyProof (⇔)
          ↳57 TRUE
        ↳58 UsableRulesProof (⇔)
          ↳59 QDP

(0) Obligation:

Q restricted rewrite system:
The TRS R consists of the following rules:

rec(rec(x)) → sent(rec(x))
rec(sent(x)) → sent(rec(x))
rec(no(x)) → sent(rec(x))
rec(bot) → up(sent(bot))
rec(up(x)) → up(rec(x))
sent(up(x)) → up(sent(x))
no(up(x)) → up(no(x))
top(rec(up(x))) → top(check(rec(x)))
top(sent(up(x))) → top(check(rec(x)))
top(no(up(x))) → top(check(rec(x)))
check(up(x)) → up(check(x))
check(sent(x)) → sent(check(x))
check(rec(x)) → rec(check(x))
check(no(x)) → no(check(x))
check(no(x)) → no(x)

Q is empty.

(1) QTRS Reverse (EQUIVALENT transformation)

We applied the QTRS Reverse Processor [REVERSE].

(2) Obligation:

Q restricted rewrite system:
The TRS R consists of the following rules:

rec(rec(x)) → rec(sent(x))
sent(rec(x)) → rec(sent(x))
no(rec(x)) → rec(sent(x))
bot'(rec(x)) → bot'(sent(up(x)))
up(rec(x)) → rec(up(x))
up(sent(x)) → sent(up(x))
up(no(x)) → no(up(x))
up(rec(top(x))) → rec(check(top(x)))
up(sent(top(x))) → rec(check(top(x)))
up(no(top(x))) → rec(check(top(x)))
up(check(x)) → check(up(x))
sent(check(x)) → check(sent(x))
rec(check(x)) → check(rec(x))
no(check(x)) → check(no(x))
no(check(x)) → no(x)

Q is empty.

(3) QTRS Reverse (EQUIVALENT transformation)

We applied the QTRS Reverse Processor [REVERSE].

(4) Obligation:

Q restricted rewrite system:
The TRS R consists of the following rules:

rec(rec(x)) → rec(sent(x))
sent(rec(x)) → rec(sent(x))
no(rec(x)) → rec(sent(x))
bot'(rec(x)) → bot'(sent(up(x)))
up(rec(x)) → rec(up(x))
up(sent(x)) → sent(up(x))
up(no(x)) → no(up(x))
up(rec(top(x))) → rec(check(top(x)))
up(sent(top(x))) → rec(check(top(x)))
up(no(top(x))) → rec(check(top(x)))
up(check(x)) → check(up(x))
sent(check(x)) → check(sent(x))
rec(check(x)) → check(rec(x))
no(check(x)) → check(no(x))
no(check(x)) → no(x)

Q is empty.

(5) QTRSRRRProof (EQUIVALENT transformation)

Used ordering:
Polynomial interpretation [POLO]:

POL(bot) = 0   
POL(check(x1)) = x1   
POL(no(x1)) = 1 + x1   
POL(rec(x1)) = 1 + x1   
POL(sent(x1)) = x1   
POL(top(x1)) = x1   
POL(up(x1)) = 1 + x1   
With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:

rec(rec(x)) → sent(rec(x))
rec(no(x)) → sent(rec(x))
top(rec(up(x))) → top(check(rec(x)))
top(no(up(x))) → top(check(rec(x)))


(6) Obligation:

Q restricted rewrite system:
The TRS R consists of the following rules:

rec(sent(x)) → sent(rec(x))
rec(bot) → up(sent(bot))
rec(up(x)) → up(rec(x))
sent(up(x)) → up(sent(x))
no(up(x)) → up(no(x))
top(sent(up(x))) → top(check(rec(x)))
check(up(x)) → up(check(x))
check(sent(x)) → sent(check(x))
check(rec(x)) → rec(check(x))
check(no(x)) → no(check(x))
check(no(x)) → no(x)

Q is empty.

(7) DependencyPairsProof (EQUIVALENT transformation)

Using Dependency Pairs [AG00,LPAR04] we result in the following initial DP problem.

(8) Obligation:

Q DP problem:
The TRS P consists of the following rules:

REC(sent(x)) → SENT(rec(x))
REC(sent(x)) → REC(x)
REC(bot) → SENT(bot)
REC(up(x)) → REC(x)
SENT(up(x)) → SENT(x)
NO(up(x)) → NO(x)
TOP(sent(up(x))) → TOP(check(rec(x)))
TOP(sent(up(x))) → CHECK(rec(x))
TOP(sent(up(x))) → REC(x)
CHECK(up(x)) → CHECK(x)
CHECK(sent(x)) → SENT(check(x))
CHECK(sent(x)) → CHECK(x)
CHECK(rec(x)) → REC(check(x))
CHECK(rec(x)) → CHECK(x)
CHECK(no(x)) → NO(check(x))
CHECK(no(x)) → CHECK(x)

The TRS R consists of the following rules:

rec(sent(x)) → sent(rec(x))
rec(bot) → up(sent(bot))
rec(up(x)) → up(rec(x))
sent(up(x)) → up(sent(x))
no(up(x)) → up(no(x))
top(sent(up(x))) → top(check(rec(x)))
check(up(x)) → up(check(x))
check(sent(x)) → sent(check(x))
check(rec(x)) → rec(check(x))
check(no(x)) → no(check(x))
check(no(x)) → no(x)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(9) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 5 SCCs with 7 less nodes.

(10) Complex Obligation (AND)

(11) Obligation:

Q DP problem:
The TRS P consists of the following rules:

NO(up(x)) → NO(x)

The TRS R consists of the following rules:

rec(sent(x)) → sent(rec(x))
rec(bot) → up(sent(bot))
rec(up(x)) → up(rec(x))
sent(up(x)) → up(sent(x))
no(up(x)) → up(no(x))
top(sent(up(x))) → top(check(rec(x)))
check(up(x)) → up(check(x))
check(sent(x)) → sent(check(x))
check(rec(x)) → rec(check(x))
check(no(x)) → no(check(x))
check(no(x)) → no(x)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(12) UsableRulesProof (EQUIVALENT transformation)

We can use the usable rules and reduction pair processor [LPAR04] with the Ce-compatible extension of the polynomial order that maps every function symbol to the sum of its arguments. Then, we can delete all non-usable rules [FROCOS05] from R.

(13) Obligation:

Q DP problem:
The TRS P consists of the following rules:

NO(up(x)) → NO(x)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(14) UsableRulesReductionPairsProof (EQUIVALENT transformation)

By using the usable rules with reduction pair processor [LPAR04] with a polynomial ordering [POLO], all dependency pairs and the corresponding usable rules [FROCOS05] can be oriented non-strictly. All non-usable rules are removed, and those dependency pairs and usable rules that have been oriented strictly or contain non-usable symbols in their left-hand side are removed as well.

The following dependency pairs can be deleted:

NO(up(x)) → NO(x)
No rules are removed from R.

Used ordering: POLO with Polynomial interpretation [POLO]:

POL(NO(x1)) = 2·x1   
POL(up(x1)) = 2·x1   

(15) Obligation:

Q DP problem:
P is empty.
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(16) PisEmptyProof (EQUIVALENT transformation)

The TRS P is empty. Hence, there is no (P,Q,R) chain.

(17) TRUE

(18) UsableRulesProof (EQUIVALENT transformation)

We can use the usable rules and reduction pair processor [LPAR04] with the Ce-compatible extension of the polynomial order that maps every function symbol to the sum of its arguments. Then, we can delete all non-usable rules [FROCOS05] from R.

(19) Obligation:

Q DP problem:
The TRS P consists of the following rules:

NO(up(x)) → NO(x)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(20) Obligation:

Q DP problem:
The TRS P consists of the following rules:

SENT(up(x)) → SENT(x)

The TRS R consists of the following rules:

rec(sent(x)) → sent(rec(x))
rec(bot) → up(sent(bot))
rec(up(x)) → up(rec(x))
sent(up(x)) → up(sent(x))
no(up(x)) → up(no(x))
top(sent(up(x))) → top(check(rec(x)))
check(up(x)) → up(check(x))
check(sent(x)) → sent(check(x))
check(rec(x)) → rec(check(x))
check(no(x)) → no(check(x))
check(no(x)) → no(x)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(21) UsableRulesProof (EQUIVALENT transformation)

We can use the usable rules and reduction pair processor [LPAR04] with the Ce-compatible extension of the polynomial order that maps every function symbol to the sum of its arguments. Then, we can delete all non-usable rules [FROCOS05] from R.

(22) Obligation:

Q DP problem:
The TRS P consists of the following rules:

SENT(up(x)) → SENT(x)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(23) UsableRulesReductionPairsProof (EQUIVALENT transformation)

By using the usable rules with reduction pair processor [LPAR04] with a polynomial ordering [POLO], all dependency pairs and the corresponding usable rules [FROCOS05] can be oriented non-strictly. All non-usable rules are removed, and those dependency pairs and usable rules that have been oriented strictly or contain non-usable symbols in their left-hand side are removed as well.

The following dependency pairs can be deleted:

SENT(up(x)) → SENT(x)
No rules are removed from R.

Used ordering: POLO with Polynomial interpretation [POLO]:

POL(SENT(x1)) = 2·x1   
POL(up(x1)) = 2·x1   

(24) Obligation:

Q DP problem:
P is empty.
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(25) PisEmptyProof (EQUIVALENT transformation)

The TRS P is empty. Hence, there is no (P,Q,R) chain.

(26) TRUE

(27) UsableRulesProof (EQUIVALENT transformation)

We can use the usable rules and reduction pair processor [LPAR04] with the Ce-compatible extension of the polynomial order that maps every function symbol to the sum of its arguments. Then, we can delete all non-usable rules [FROCOS05] from R.

(28) Obligation:

Q DP problem:
The TRS P consists of the following rules:

SENT(up(x)) → SENT(x)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(29) Obligation:

Q DP problem:
The TRS P consists of the following rules:

REC(up(x)) → REC(x)
REC(sent(x)) → REC(x)

The TRS R consists of the following rules:

rec(sent(x)) → sent(rec(x))
rec(bot) → up(sent(bot))
rec(up(x)) → up(rec(x))
sent(up(x)) → up(sent(x))
no(up(x)) → up(no(x))
top(sent(up(x))) → top(check(rec(x)))
check(up(x)) → up(check(x))
check(sent(x)) → sent(check(x))
check(rec(x)) → rec(check(x))
check(no(x)) → no(check(x))
check(no(x)) → no(x)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(30) UsableRulesProof (EQUIVALENT transformation)

We can use the usable rules and reduction pair processor [LPAR04] with the Ce-compatible extension of the polynomial order that maps every function symbol to the sum of its arguments. Then, we can delete all non-usable rules [FROCOS05] from R.

(31) Obligation:

Q DP problem:
The TRS P consists of the following rules:

REC(up(x)) → REC(x)
REC(sent(x)) → REC(x)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(32) UsableRulesReductionPairsProof (EQUIVALENT transformation)

By using the usable rules with reduction pair processor [LPAR04] with a polynomial ordering [POLO], all dependency pairs and the corresponding usable rules [FROCOS05] can be oriented non-strictly. All non-usable rules are removed, and those dependency pairs and usable rules that have been oriented strictly or contain non-usable symbols in their left-hand side are removed as well.

The following dependency pairs can be deleted:

REC(up(x)) → REC(x)
REC(sent(x)) → REC(x)
No rules are removed from R.

Used ordering: POLO with Polynomial interpretation [POLO]:

POL(REC(x1)) = 2·x1   
POL(sent(x1)) = 2·x1   
POL(up(x1)) = 2·x1   

(33) Obligation:

Q DP problem:
P is empty.
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(34) PisEmptyProof (EQUIVALENT transformation)

The TRS P is empty. Hence, there is no (P,Q,R) chain.

(35) TRUE

(36) UsableRulesProof (EQUIVALENT transformation)

We can use the usable rules and reduction pair processor [LPAR04] with the Ce-compatible extension of the polynomial order that maps every function symbol to the sum of its arguments. Then, we can delete all non-usable rules [FROCOS05] from R.

(37) Obligation:

Q DP problem:
The TRS P consists of the following rules:

REC(up(x)) → REC(x)
REC(sent(x)) → REC(x)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(38) Obligation:

Q DP problem:
The TRS P consists of the following rules:

CHECK(sent(x)) → CHECK(x)
CHECK(up(x)) → CHECK(x)
CHECK(rec(x)) → CHECK(x)
CHECK(no(x)) → CHECK(x)

The TRS R consists of the following rules:

rec(sent(x)) → sent(rec(x))
rec(bot) → up(sent(bot))
rec(up(x)) → up(rec(x))
sent(up(x)) → up(sent(x))
no(up(x)) → up(no(x))
top(sent(up(x))) → top(check(rec(x)))
check(up(x)) → up(check(x))
check(sent(x)) → sent(check(x))
check(rec(x)) → rec(check(x))
check(no(x)) → no(check(x))
check(no(x)) → no(x)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(39) UsableRulesProof (EQUIVALENT transformation)

We can use the usable rules and reduction pair processor [LPAR04] with the Ce-compatible extension of the polynomial order that maps every function symbol to the sum of its arguments. Then, we can delete all non-usable rules [FROCOS05] from R.

(40) Obligation:

Q DP problem:
The TRS P consists of the following rules:

CHECK(sent(x)) → CHECK(x)
CHECK(up(x)) → CHECK(x)
CHECK(rec(x)) → CHECK(x)
CHECK(no(x)) → CHECK(x)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(41) UsableRulesReductionPairsProof (EQUIVALENT transformation)

By using the usable rules with reduction pair processor [LPAR04] with a polynomial ordering [POLO], all dependency pairs and the corresponding usable rules [FROCOS05] can be oriented non-strictly. All non-usable rules are removed, and those dependency pairs and usable rules that have been oriented strictly or contain non-usable symbols in their left-hand side are removed as well.

The following dependency pairs can be deleted:

CHECK(sent(x)) → CHECK(x)
CHECK(up(x)) → CHECK(x)
CHECK(rec(x)) → CHECK(x)
CHECK(no(x)) → CHECK(x)
No rules are removed from R.

Used ordering: POLO with Polynomial interpretation [POLO]:

POL(CHECK(x1)) = 2·x1   
POL(no(x1)) = 2·x1   
POL(rec(x1)) = 2·x1   
POL(sent(x1)) = 2·x1   
POL(up(x1)) = 2·x1   

(42) Obligation:

Q DP problem:
P is empty.
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(43) PisEmptyProof (EQUIVALENT transformation)

The TRS P is empty. Hence, there is no (P,Q,R) chain.

(44) TRUE

(45) UsableRulesProof (EQUIVALENT transformation)

We can use the usable rules and reduction pair processor [LPAR04] with the Ce-compatible extension of the polynomial order that maps every function symbol to the sum of its arguments. Then, we can delete all non-usable rules [FROCOS05] from R.

(46) Obligation:

Q DP problem:
The TRS P consists of the following rules:

CHECK(sent(x)) → CHECK(x)
CHECK(up(x)) → CHECK(x)
CHECK(rec(x)) → CHECK(x)
CHECK(no(x)) → CHECK(x)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(47) Obligation:

Q DP problem:
The TRS P consists of the following rules:

TOP(sent(up(x))) → TOP(check(rec(x)))

The TRS R consists of the following rules:

rec(sent(x)) → sent(rec(x))
rec(bot) → up(sent(bot))
rec(up(x)) → up(rec(x))
sent(up(x)) → up(sent(x))
no(up(x)) → up(no(x))
top(sent(up(x))) → top(check(rec(x)))
check(up(x)) → up(check(x))
check(sent(x)) → sent(check(x))
check(rec(x)) → rec(check(x))
check(no(x)) → no(check(x))
check(no(x)) → no(x)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(48) UsableRulesProof (EQUIVALENT transformation)

We can use the usable rules and reduction pair processor [LPAR04] with the Ce-compatible extension of the polynomial order that maps every function symbol to the sum of its arguments. Then, we can delete all non-usable rules [FROCOS05] from R.

(49) Obligation:

Q DP problem:
The TRS P consists of the following rules:

TOP(sent(up(x))) → TOP(check(rec(x)))

The TRS R consists of the following rules:

rec(sent(x)) → sent(rec(x))
rec(bot) → up(sent(bot))
rec(up(x)) → up(rec(x))
check(up(x)) → up(check(x))
check(sent(x)) → sent(check(x))
check(rec(x)) → rec(check(x))
check(no(x)) → no(check(x))
check(no(x)) → no(x)
no(up(x)) → up(no(x))
sent(up(x)) → up(sent(x))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(50) MRRProof (EQUIVALENT transformation)

By using the rule removal processor [LPAR04] with the following ordering, at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.

Strictly oriented rules of the TRS R:

no(up(x)) → up(no(x))

Used ordering: Polynomial interpretation [POLO]:

POL(TOP(x1)) = 2·x1   
POL(bot) = 0   
POL(check(x1)) = x1   
POL(no(x1)) = 2·x1   
POL(rec(x1)) = 1 + 2·x1   
POL(sent(x1)) = x1   
POL(up(x1)) = 1 + 2·x1   

(51) Obligation:

Q DP problem:
The TRS P consists of the following rules:

TOP(sent(up(x))) → TOP(check(rec(x)))

The TRS R consists of the following rules:

rec(sent(x)) → sent(rec(x))
rec(bot) → up(sent(bot))
rec(up(x)) → up(rec(x))
check(up(x)) → up(check(x))
check(sent(x)) → sent(check(x))
check(rec(x)) → rec(check(x))
check(no(x)) → no(check(x))
check(no(x)) → no(x)
sent(up(x)) → up(sent(x))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(52) MRRProof (EQUIVALENT transformation)

By using the rule removal processor [LPAR04] with the following ordering, at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.

Strictly oriented rules of the TRS R:

check(no(x)) → no(check(x))
check(no(x)) → no(x)

Used ordering: Polynomial interpretation [POLO]:

POL(TOP(x1)) = 2·x1   
POL(bot) = 0   
POL(check(x1)) = 2·x1   
POL(no(x1)) = 1 + 2·x1   
POL(rec(x1)) = x1   
POL(sent(x1)) = x1   
POL(up(x1)) = 2·x1   

(53) Obligation:

Q DP problem:
The TRS P consists of the following rules:

TOP(sent(up(x))) → TOP(check(rec(x)))

The TRS R consists of the following rules:

rec(sent(x)) → sent(rec(x))
rec(bot) → up(sent(bot))
rec(up(x)) → up(rec(x))
check(up(x)) → up(check(x))
check(sent(x)) → sent(check(x))
check(rec(x)) → rec(check(x))
sent(up(x)) → up(sent(x))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(54) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


TOP(sent(up(x))) → TOP(check(rec(x)))
The remaining pairs can at least be oriented weakly.
Used ordering: Matrix interpretation [MATRO] with arctic natural numbers [ARCTIC]:

POL(TOP(x1)) =
/0A\
\-I/
 +
/0A1A\
\-I-I/
·x1

POL(sent(x1)) =
/-I\
\-I/
 +
/0A0A\
\-I0A/
·x1

POL(up(x1)) =
/1A\
\-I/
 +
/1A0A\
\-I1A/
·x1

POL(check(x1)) =
/0A\
\-I/
 +
/0A0A\
\-I-I/
·x1

POL(rec(x1)) =
/-I\
\-I/
 +
/0A1A\
\-I1A/
·x1

POL(bot) =
/0A\
\0A/

The following usable rules [FROCOS05] were oriented:

rec(bot) → up(sent(bot))
rec(sent(x)) → sent(rec(x))
check(up(x)) → up(check(x))
rec(up(x)) → up(rec(x))
check(rec(x)) → rec(check(x))
check(sent(x)) → sent(check(x))
sent(up(x)) → up(sent(x))

(55) Obligation:

Q DP problem:
P is empty.
The TRS R consists of the following rules:

rec(sent(x)) → sent(rec(x))
rec(bot) → up(sent(bot))
rec(up(x)) → up(rec(x))
check(up(x)) → up(check(x))
check(sent(x)) → sent(check(x))
check(rec(x)) → rec(check(x))
sent(up(x)) → up(sent(x))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(56) PisEmptyProof (EQUIVALENT transformation)

The TRS P is empty. Hence, there is no (P,Q,R) chain.

(57) TRUE

(58) UsableRulesProof (EQUIVALENT transformation)

We can use the usable rules and reduction pair processor [LPAR04] with the Ce-compatible extension of the polynomial order that maps every function symbol to the sum of its arguments. Then, we can delete all non-usable rules [FROCOS05] from R.

(59) Obligation:

Q DP problem:
The TRS P consists of the following rules:

TOP(sent(up(x))) → TOP(check(rec(x)))

The TRS R consists of the following rules:

rec(sent(x)) → sent(rec(x))
rec(bot) → up(sent(bot))
rec(up(x)) → up(rec(x))
check(up(x)) → up(check(x))
check(sent(x)) → sent(check(x))
check(rec(x)) → rec(check(x))
check(no(x)) → no(check(x))
check(no(x)) → no(x)
no(up(x)) → up(no(x))
sent(up(x)) → up(sent(x))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.