(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) DependencyPairsProof (EQUIVALENT transformation)

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

(2) Obligation:

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

REC(rec(x)) → SENT(rec(x))
REC(sent(x)) → SENT(rec(x))
REC(sent(x)) → REC(x)
REC(no(x)) → SENT(rec(x))
REC(no(x)) → REC(x)
REC(bot) → SENT(bot)
REC(up(x)) → REC(x)
SENT(up(x)) → SENT(x)
NO(up(x)) → NO(x)
TOP(rec(up(x))) → TOP(check(rec(x)))
TOP(rec(up(x))) → CHECK(rec(x))
TOP(rec(up(x))) → REC(x)
TOP(sent(up(x))) → TOP(check(rec(x)))
TOP(sent(up(x))) → CHECK(rec(x))
TOP(sent(up(x))) → REC(x)
TOP(no(up(x))) → TOP(check(rec(x)))
TOP(no(up(x))) → CHECK(rec(x))
TOP(no(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(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.
We have to consider all minimal (P,Q,R)-chains.

(3) DependencyGraphProof (EQUIVALENT transformation)

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

(4) Complex Obligation (AND)

(5) 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(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.
We have to consider all minimal (P,Q,R)-chains.

(6) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


NO(up(x)) → NO(x)
The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
NO(x1)  =  NO(x1)
up(x1)  =  up(x1)
rec(x1)  =  rec(x1)
sent(x1)  =  sent(x1)
no(x1)  =  no(x1)
bot  =  bot
top(x1)  =  top
check(x1)  =  check(x1)

Recursive Path Order [RPO].
Precedence:
NO1 > up1
bot > sent1 > up1
check1 > rec1 > sent1 > up1
check1 > rec1 > top > up1
check1 > no1 > sent1 > up1

The following usable rules [FROCOS05] were oriented:

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)

(7) Obligation:

Q DP problem:
P is empty.
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.
We have to consider all minimal (P,Q,R)-chains.

(8) PisEmptyProof (EQUIVALENT transformation)

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

(9) TRUE

(10) 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(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.
We have to consider all minimal (P,Q,R)-chains.

(11) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


SENT(up(x)) → SENT(x)
The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
SENT(x1)  =  SENT(x1)
up(x1)  =  up(x1)
rec(x1)  =  rec(x1)
sent(x1)  =  sent(x1)
no(x1)  =  no(x1)
bot  =  bot
top(x1)  =  top
check(x1)  =  check(x1)

Recursive Path Order [RPO].
Precedence:
SENT1 > up1
bot > sent1 > up1
check1 > rec1 > sent1 > up1
check1 > rec1 > top > up1
check1 > no1 > sent1 > up1

The following usable rules [FROCOS05] were oriented:

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)

(12) Obligation:

Q DP problem:
P is empty.
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.
We have to consider all minimal (P,Q,R)-chains.

(13) PisEmptyProof (EQUIVALENT transformation)

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

(14) TRUE

(15) Obligation:

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

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

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.
We have to consider all minimal (P,Q,R)-chains.

(16) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


REC(no(x)) → REC(x)
The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
REC(x1)  =  REC(x1)
no(x1)  =  no(x1)
sent(x1)  =  x1
up(x1)  =  x1
rec(x1)  =  x1
bot  =  bot
top(x1)  =  x1
check(x1)  =  x1

Recursive Path Order [RPO].
Precedence:
no1 > REC1

The following usable rules [FROCOS05] were oriented:

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)

(17) Obligation:

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

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

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.
We have to consider all minimal (P,Q,R)-chains.

(18) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


REC(sent(x)) → REC(x)
REC(up(x)) → REC(x)
The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
REC(x1)  =  REC(x1)
sent(x1)  =  sent(x1)
up(x1)  =  up(x1)
rec(x1)  =  rec(x1)
no(x1)  =  no(x1)
bot  =  bot
top(x1)  =  top
check(x1)  =  check(x1)

Recursive Path Order [RPO].
Precedence:
REC1 > up1
bot > sent1 > up1
top > up1
check1 > rec1 > sent1 > up1
check1 > no1 > up1

The following usable rules [FROCOS05] were oriented:

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)

(19) Obligation:

Q DP problem:
P is empty.
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.
We have to consider all minimal (P,Q,R)-chains.

(20) PisEmptyProof (EQUIVALENT transformation)

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

(21) TRUE

(22) 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(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.
We have to consider all minimal (P,Q,R)-chains.

(23) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


CHECK(no(x)) → CHECK(x)
The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
CHECK(x1)  =  CHECK(x1)
sent(x1)  =  x1
up(x1)  =  x1
rec(x1)  =  x1
no(x1)  =  no(x1)
bot  =  bot
top(x1)  =  top(x1)
check(x1)  =  x1

Recursive Path Order [RPO].
Precedence:
no1 > CHECK1

The following usable rules [FROCOS05] were oriented:

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)

(24) 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)

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.
We have to consider all minimal (P,Q,R)-chains.

(25) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


CHECK(rec(x)) → CHECK(x)
The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
CHECK(x1)  =  CHECK(x1)
sent(x1)  =  x1
up(x1)  =  x1
rec(x1)  =  rec(x1)
no(x1)  =  x1
bot  =  bot
top(x1)  =  top
check(x1)  =  x1

Recursive Path Order [RPO].
Precedence:
rec1 > CHECK1
rec1 > top

The following usable rules [FROCOS05] were oriented:

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)

(26) Obligation:

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

CHECK(sent(x)) → CHECK(x)
CHECK(up(x)) → CHECK(x)

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.
We have to consider all minimal (P,Q,R)-chains.

(27) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


CHECK(sent(x)) → CHECK(x)
CHECK(up(x)) → CHECK(x)
The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
CHECK(x1)  =  CHECK(x1)
sent(x1)  =  sent(x1)
up(x1)  =  up(x1)
rec(x1)  =  rec(x1)
no(x1)  =  no(x1)
bot  =  bot
top(x1)  =  top
check(x1)  =  check(x1)

Recursive Path Order [RPO].
Precedence:
CHECK1 > up1
bot > sent1 > up1
top > up1
check1 > rec1 > sent1 > up1
check1 > no1 > up1

The following usable rules [FROCOS05] were oriented:

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)

(28) Obligation:

Q DP problem:
P is empty.
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.
We have to consider all minimal (P,Q,R)-chains.

(29) PisEmptyProof (EQUIVALENT transformation)

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

(30) TRUE

(31) Obligation:

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

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

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.
We have to consider all minimal (P,Q,R)-chains.

(32) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


TOP(no(up(x))) → TOP(check(rec(x)))
The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
TOP(x1)  =  x1
sent(x1)  =  x1
up(x1)  =  x1
check(x1)  =  x1
rec(x1)  =  x1
no(x1)  =  no(x1)
bot  =  bot
top(x1)  =  top

Recursive Path Order [RPO].
Precedence:
no1 > top

The following usable rules [FROCOS05] were oriented:

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)

(33) Obligation:

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

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

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.
We have to consider all minimal (P,Q,R)-chains.