Termination Proof using AProVE

Term Rewriting System R:
[x]
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)

Innermost Termination of R to be shown.

     ↳Dependency Pair Analysis

R contains the following Dependency Pairs:

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)

Furthermore, R contains six SCCs.

     ↳DPs

       →DP Problem 1

         ↳Forward Instantiation Transformation

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳FwdInst

       →DP Problem 4

         ↳FwdInst

       →DP Problem 5

         ↳FwdInst

       →DP Problem 6

         ↳FwdInst

Dependency Pair:

SENT(up(x)) -> SENT(x)

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)

Strategy:

innermost

On this DP problem, a Forward Instantiation SCC transformation can be performed.
As a result of transforming the rule

SENT(up(x)) -> SENT(x)

one new Dependency Pair is created:

SENT(up(up(x''))) -> SENT(up(x''))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳FwdInst

           →DP Problem 7

             ↳Forward Instantiation Transformation

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳FwdInst

       →DP Problem 4

         ↳FwdInst

       →DP Problem 5

         ↳FwdInst

       →DP Problem 6

         ↳FwdInst

Dependency Pair:

SENT(up(up(x''))) -> SENT(up(x''))

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)

Strategy:

innermost

On this DP problem, a Forward Instantiation SCC transformation can be performed.
As a result of transforming the rule

SENT(up(up(x''))) -> SENT(up(x''))

one new Dependency Pair is created:

SENT(up(up(up(x'''')))) -> SENT(up(up(x'''')))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳FwdInst

           →DP Problem 7

             ↳FwdInst

...

               →DP Problem 8

                 ↳Argument Filtering and Ordering

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳FwdInst

       →DP Problem 4

         ↳FwdInst

       →DP Problem 5

         ↳FwdInst

       →DP Problem 6

         ↳FwdInst

Dependency Pair:

SENT(up(up(up(x'''')))) -> SENT(up(up(x'''')))

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)

Strategy:

innermost

The following dependency pair can be strictly oriented:

SENT(up(up(up(x'''')))) -> SENT(up(up(x'''')))

There are no usable rules for innermost that need to be oriented.
Used ordering: Polynomial ordering with Polynomial interpretation:

POL(up(x₁)) = 1 + x₁

POL(SENT(x₁)) = 1 + x₁

resulting in one new DP problem.
Used Argument Filtering System:

SENT(x₁) -> SENT(x₁)
up(x₁) -> up(x₁)

     ↳DPs

       →DP Problem 1

         ↳FwdInst

           →DP Problem 7

             ↳FwdInst

...

               →DP Problem 9

                 ↳Dependency Graph

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳FwdInst

       →DP Problem 4

         ↳FwdInst

       →DP Problem 5

         ↳FwdInst

       →DP Problem 6

         ↳FwdInst

Dependency Pair:

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)

Strategy:

innermost

Using the Dependency Graph resulted in no new DP problems.

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳Forward Instantiation Transformation

       →DP Problem 3

         ↳FwdInst

       →DP Problem 4

         ↳FwdInst

       →DP Problem 5

         ↳FwdInst

       →DP Problem 6

         ↳FwdInst

Dependency Pair:

NO(up(x)) -> NO(x)

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)

Strategy:

innermost

On this DP problem, a Forward Instantiation SCC transformation can be performed.
As a result of transforming the rule

NO(up(x)) -> NO(x)

one new Dependency Pair is created:

NO(up(up(x''))) -> NO(up(x''))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

           →DP Problem 10

             ↳Forward Instantiation Transformation

       →DP Problem 3

         ↳FwdInst

       →DP Problem 4

         ↳FwdInst

       →DP Problem 5

         ↳FwdInst

       →DP Problem 6

         ↳FwdInst

Dependency Pair:

NO(up(up(x''))) -> NO(up(x''))

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)

Strategy:

innermost

On this DP problem, a Forward Instantiation SCC transformation can be performed.
As a result of transforming the rule

NO(up(up(x''))) -> NO(up(x''))

one new Dependency Pair is created:

NO(up(up(up(x'''')))) -> NO(up(up(x'''')))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

           →DP Problem 10

             ↳FwdInst

...

               →DP Problem 11

                 ↳Argument Filtering and Ordering

       →DP Problem 3

         ↳FwdInst

       →DP Problem 4

         ↳FwdInst

       →DP Problem 5

         ↳FwdInst

       →DP Problem 6

         ↳FwdInst

Dependency Pair:

NO(up(up(up(x'''')))) -> NO(up(up(x'''')))

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)

Strategy:

innermost

The following dependency pair can be strictly oriented:

NO(up(up(up(x'''')))) -> NO(up(up(x'''')))

There are no usable rules for innermost that need to be oriented.
Used ordering: Polynomial ordering with Polynomial interpretation:

POL(NO(x₁)) = 1 + x₁

POL(up(x₁)) = 1 + x₁

resulting in one new DP problem.
Used Argument Filtering System:

NO(x₁) -> NO(x₁)
up(x₁) -> up(x₁)

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

           →DP Problem 10

             ↳FwdInst

...

               →DP Problem 12

                 ↳Dependency Graph

       →DP Problem 3

         ↳FwdInst

       →DP Problem 4

         ↳FwdInst

       →DP Problem 5

         ↳FwdInst

       →DP Problem 6

         ↳FwdInst

Dependency Pair:

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)

Strategy:

innermost

Using the Dependency Graph resulted in no new DP problems.

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳Forward Instantiation Transformation

       →DP Problem 4

         ↳FwdInst

       →DP Problem 5

         ↳FwdInst

       →DP Problem 6

         ↳FwdInst

Dependency Pair:

REC(up(x)) -> REC(x)

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)

Strategy:

innermost

On this DP problem, a Forward Instantiation SCC transformation can be performed.
As a result of transforming the rule

REC(up(x)) -> REC(x)

one new Dependency Pair is created:

REC(up(up(x''))) -> REC(up(x''))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳FwdInst

           →DP Problem 13

             ↳Forward Instantiation Transformation

       →DP Problem 4

         ↳FwdInst

       →DP Problem 5

         ↳FwdInst

       →DP Problem 6

         ↳FwdInst

Dependency Pair:

REC(up(up(x''))) -> REC(up(x''))

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)

Strategy:

innermost

On this DP problem, a Forward Instantiation SCC transformation can be performed.
As a result of transforming the rule

REC(up(up(x''))) -> REC(up(x''))

one new Dependency Pair is created:

REC(up(up(up(x'''')))) -> REC(up(up(x'''')))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳FwdInst

           →DP Problem 13

             ↳FwdInst

...

               →DP Problem 14

                 ↳Argument Filtering and Ordering

       →DP Problem 4

         ↳FwdInst

       →DP Problem 5

         ↳FwdInst

       →DP Problem 6

         ↳FwdInst

Dependency Pair:

REC(up(up(up(x'''')))) -> REC(up(up(x'''')))

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)

Strategy:

innermost

The following dependency pair can be strictly oriented:

REC(up(up(up(x'''')))) -> REC(up(up(x'''')))

There are no usable rules for innermost that need to be oriented.
Used ordering: Polynomial ordering with Polynomial interpretation:

POL(up(x₁)) = 1 + x₁

POL(REC(x₁)) = 1 + x₁

resulting in one new DP problem.
Used Argument Filtering System:

REC(x₁) -> REC(x₁)
up(x₁) -> up(x₁)

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳FwdInst

           →DP Problem 13

             ↳FwdInst

...

               →DP Problem 15

                 ↳Dependency Graph

       →DP Problem 4

         ↳FwdInst

       →DP Problem 5

         ↳FwdInst

       →DP Problem 6

         ↳FwdInst

Dependency Pair:

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)

Strategy:

innermost

Using the Dependency Graph resulted in no new DP problems.

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳FwdInst

       →DP Problem 4

         ↳Forward Instantiation Transformation

       →DP Problem 5

         ↳FwdInst

       →DP Problem 6

         ↳FwdInst

Dependency Pairs:

REC(no(x)) -> REC(x)
REC(sent(x)) -> REC(x)

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)

Strategy:

innermost

On this DP problem, a Forward Instantiation SCC transformation can be performed.
As a result of transforming the rule

REC(sent(x)) -> REC(x)

two new Dependency Pairs are created:

REC(sent(sent(x''))) -> REC(sent(x''))
REC(sent(no(x''))) -> REC(no(x''))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳FwdInst

       →DP Problem 4

         ↳FwdInst

           →DP Problem 16

             ↳Forward Instantiation Transformation

       →DP Problem 5

         ↳FwdInst

       →DP Problem 6

         ↳FwdInst

Dependency Pairs:

REC(sent(no(x''))) -> REC(no(x''))
REC(sent(sent(x''))) -> REC(sent(x''))
REC(no(x)) -> REC(x)

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)

Strategy:

innermost

On this DP problem, a Forward Instantiation SCC transformation can be performed.
As a result of transforming the rule

REC(no(x)) -> REC(x)

three new Dependency Pairs are created:

REC(no(no(x''))) -> REC(no(x''))
REC(no(sent(sent(x'''')))) -> REC(sent(sent(x'''')))
REC(no(sent(no(x'''')))) -> REC(sent(no(x'''')))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳FwdInst

       →DP Problem 4

         ↳FwdInst

           →DP Problem 16

             ↳FwdInst

...

               →DP Problem 17

                 ↳Forward Instantiation Transformation

       →DP Problem 5

         ↳FwdInst

       →DP Problem 6

         ↳FwdInst

Dependency Pairs:

REC(no(sent(no(x'''')))) -> REC(sent(no(x'''')))
REC(sent(sent(x''))) -> REC(sent(x''))
REC(no(sent(sent(x'''')))) -> REC(sent(sent(x'''')))
REC(no(no(x''))) -> REC(no(x''))
REC(sent(no(x''))) -> REC(no(x''))

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)

Strategy:

innermost

On this DP problem, a Forward Instantiation SCC transformation can be performed.
As a result of transforming the rule

REC(sent(sent(x''))) -> REC(sent(x''))

two new Dependency Pairs are created:

REC(sent(sent(sent(x'''')))) -> REC(sent(sent(x'''')))
REC(sent(sent(no(x'''')))) -> REC(sent(no(x'''')))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳FwdInst

       →DP Problem 4

         ↳FwdInst

           →DP Problem 16

             ↳FwdInst

...

               →DP Problem 18

                 ↳Forward Instantiation Transformation

       →DP Problem 5

         ↳FwdInst

       →DP Problem 6

         ↳FwdInst

Dependency Pairs:

REC(sent(sent(no(x'''')))) -> REC(sent(no(x'''')))
REC(sent(sent(sent(x'''')))) -> REC(sent(sent(x'''')))
REC(no(sent(sent(x'''')))) -> REC(sent(sent(x'''')))
REC(no(no(x''))) -> REC(no(x''))
REC(sent(no(x''))) -> REC(no(x''))
REC(no(sent(no(x'''')))) -> REC(sent(no(x'''')))

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)

Strategy:

innermost

On this DP problem, a Forward Instantiation SCC transformation can be performed.
As a result of transforming the rule

REC(sent(no(x''))) -> REC(no(x''))

three new Dependency Pairs are created:

REC(sent(no(no(x'''')))) -> REC(no(no(x'''')))
REC(sent(no(sent(sent(x''''''))))) -> REC(no(sent(sent(x''''''))))
REC(sent(no(sent(no(x''''''))))) -> REC(no(sent(no(x''''''))))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳FwdInst

       →DP Problem 4

         ↳FwdInst

           →DP Problem 16

             ↳FwdInst

...

               →DP Problem 19

                 ↳Forward Instantiation Transformation

       →DP Problem 5

         ↳FwdInst

       →DP Problem 6

         ↳FwdInst

Dependency Pairs:

REC(sent(no(sent(no(x''''''))))) -> REC(no(sent(no(x''''''))))
REC(sent(no(sent(sent(x''''''))))) -> REC(no(sent(sent(x''''''))))
REC(no(sent(no(x'''')))) -> REC(sent(no(x'''')))
REC(sent(sent(sent(x'''')))) -> REC(sent(sent(x'''')))
REC(no(sent(sent(x'''')))) -> REC(sent(sent(x'''')))
REC(no(no(x''))) -> REC(no(x''))
REC(sent(no(no(x'''')))) -> REC(no(no(x'''')))
REC(sent(sent(no(x'''')))) -> REC(sent(no(x'''')))

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)

Strategy:

innermost

On this DP problem, a Forward Instantiation SCC transformation can be performed.
As a result of transforming the rule

REC(no(no(x''))) -> REC(no(x''))

three new Dependency Pairs are created:

REC(no(no(no(x'''')))) -> REC(no(no(x'''')))
REC(no(no(sent(sent(x''''''))))) -> REC(no(sent(sent(x''''''))))
REC(no(no(sent(no(x''''''))))) -> REC(no(sent(no(x''''''))))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳FwdInst

       →DP Problem 4

         ↳FwdInst

           →DP Problem 16

             ↳FwdInst

...

               →DP Problem 20

                 ↳Forward Instantiation Transformation

       →DP Problem 5

         ↳FwdInst

       →DP Problem 6

         ↳FwdInst

Dependency Pairs:

REC(no(no(sent(no(x''''''))))) -> REC(no(sent(no(x''''''))))
REC(sent(no(sent(sent(x''''''))))) -> REC(no(sent(sent(x''''''))))
REC(sent(sent(no(x'''')))) -> REC(sent(no(x'''')))
REC(sent(sent(sent(x'''')))) -> REC(sent(sent(x'''')))
REC(no(sent(sent(x'''')))) -> REC(sent(sent(x'''')))
REC(no(no(sent(sent(x''''''))))) -> REC(no(sent(sent(x''''''))))
REC(no(no(no(x'''')))) -> REC(no(no(x'''')))
REC(sent(no(no(x'''')))) -> REC(no(no(x'''')))
REC(no(sent(no(x'''')))) -> REC(sent(no(x'''')))
REC(sent(no(sent(no(x''''''))))) -> REC(no(sent(no(x''''''))))

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)

Strategy:

innermost

On this DP problem, a Forward Instantiation SCC transformation can be performed.
As a result of transforming the rule

REC(no(sent(sent(x'''')))) -> REC(sent(sent(x'''')))

two new Dependency Pairs are created:

REC(no(sent(sent(sent(x''''''))))) -> REC(sent(sent(sent(x''''''))))
REC(no(sent(sent(no(x''''''))))) -> REC(sent(sent(no(x''''''))))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳FwdInst

       →DP Problem 4

         ↳FwdInst

           →DP Problem 16

             ↳FwdInst

...

               →DP Problem 21

                 ↳Forward Instantiation Transformation

       →DP Problem 5

         ↳FwdInst

       →DP Problem 6

         ↳FwdInst

Dependency Pairs:

REC(sent(no(sent(no(x''''''))))) -> REC(no(sent(no(x''''''))))
REC(no(sent(sent(no(x''''''))))) -> REC(sent(sent(no(x''''''))))
REC(sent(no(sent(sent(x''''''))))) -> REC(no(sent(sent(x''''''))))
REC(sent(sent(no(x'''')))) -> REC(sent(no(x'''')))
REC(sent(sent(sent(x'''')))) -> REC(sent(sent(x'''')))
REC(no(sent(sent(sent(x''''''))))) -> REC(sent(sent(sent(x''''''))))
REC(no(no(sent(sent(x''''''))))) -> REC(no(sent(sent(x''''''))))
REC(no(no(no(x'''')))) -> REC(no(no(x'''')))
REC(sent(no(no(x'''')))) -> REC(no(no(x'''')))
REC(no(sent(no(x'''')))) -> REC(sent(no(x'''')))
REC(no(no(sent(no(x''''''))))) -> REC(no(sent(no(x''''''))))

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)

Strategy:

innermost

On this DP problem, a Forward Instantiation SCC transformation can be performed.
As a result of transforming the rule

REC(no(sent(no(x'''')))) -> REC(sent(no(x'''')))

three new Dependency Pairs are created:

REC(no(sent(no(no(x''''''))))) -> REC(sent(no(no(x''''''))))
REC(no(sent(no(sent(sent(x'''''''')))))) -> REC(sent(no(sent(sent(x'''''''')))))
REC(no(sent(no(sent(no(x'''''''')))))) -> REC(sent(no(sent(no(x'''''''')))))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳FwdInst

       →DP Problem 4

         ↳FwdInst

           →DP Problem 16

             ↳FwdInst

...

               →DP Problem 22

                 ↳Argument Filtering and Ordering

       →DP Problem 5

         ↳FwdInst

       →DP Problem 6

         ↳FwdInst

Dependency Pairs:

REC(no(sent(no(sent(no(x'''''''')))))) -> REC(sent(no(sent(no(x'''''''')))))
REC(no(sent(no(sent(sent(x'''''''')))))) -> REC(sent(no(sent(sent(x'''''''')))))
REC(no(no(sent(no(x''''''))))) -> REC(no(sent(no(x''''''))))
REC(no(sent(sent(no(x''''''))))) -> REC(sent(sent(no(x''''''))))
REC(sent(no(sent(sent(x''''''))))) -> REC(no(sent(sent(x''''''))))
REC(sent(sent(no(x'''')))) -> REC(sent(no(x'''')))
REC(sent(sent(sent(x'''')))) -> REC(sent(sent(x'''')))
REC(no(sent(sent(sent(x''''''))))) -> REC(sent(sent(sent(x''''''))))
REC(no(no(sent(sent(x''''''))))) -> REC(no(sent(sent(x''''''))))
REC(no(no(no(x'''')))) -> REC(no(no(x'''')))
REC(sent(no(no(x'''')))) -> REC(no(no(x'''')))
REC(no(sent(no(no(x''''''))))) -> REC(sent(no(no(x''''''))))
REC(sent(no(sent(no(x''''''))))) -> REC(no(sent(no(x''''''))))

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)

Strategy:

innermost

The following dependency pairs can be strictly oriented:

REC(no(sent(no(sent(no(x'''''''')))))) -> REC(sent(no(sent(no(x'''''''')))))
REC(no(sent(no(sent(sent(x'''''''')))))) -> REC(sent(no(sent(sent(x'''''''')))))
REC(no(no(sent(no(x''''''))))) -> REC(no(sent(no(x''''''))))
REC(no(sent(sent(no(x''''''))))) -> REC(sent(sent(no(x''''''))))
REC(no(sent(sent(sent(x''''''))))) -> REC(sent(sent(sent(x''''''))))
REC(no(no(sent(sent(x''''''))))) -> REC(no(sent(sent(x''''''))))
REC(no(no(no(x'''')))) -> REC(no(no(x'''')))
REC(no(sent(no(no(x''''''))))) -> REC(sent(no(no(x''''''))))

The following usable rules for innermost can be oriented:

no(up(x)) -> up(no(x))
sent(up(x)) -> up(sent(x))

Used ordering: Polynomial ordering with Polynomial interpretation:

POL(no(x₁)) = 1 + x₁

POL(up(x₁)) = x₁

POL(REC(x₁)) = 1 + x₁

POL(sent(x₁)) = x₁

resulting in one new DP problem.
Used Argument Filtering System:

REC(x₁) -> REC(x₁)
no(x₁) -> no(x₁)
sent(x₁) -> sent(x₁)
up(x₁) -> up(x₁)

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳FwdInst

       →DP Problem 4

         ↳FwdInst

           →DP Problem 16

             ↳FwdInst

...

               →DP Problem 23

                 ↳Dependency Graph

       →DP Problem 5

         ↳FwdInst

       →DP Problem 6

         ↳FwdInst

Dependency Pairs:

REC(sent(no(sent(sent(x''''''))))) -> REC(no(sent(sent(x''''''))))
REC(sent(sent(no(x'''')))) -> REC(sent(no(x'''')))
REC(sent(sent(sent(x'''')))) -> REC(sent(sent(x'''')))
REC(sent(no(no(x'''')))) -> REC(no(no(x'''')))
REC(sent(no(sent(no(x''''''))))) -> REC(no(sent(no(x''''''))))

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)

Strategy:

innermost

Using the Dependency Graph the DP problem was split into 1 DP problems.

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳FwdInst

       →DP Problem 4

         ↳FwdInst

           →DP Problem 16

             ↳FwdInst

...

               →DP Problem 24

                 ↳Argument Filtering and Ordering

       →DP Problem 5

         ↳FwdInst

       →DP Problem 6

         ↳FwdInst

Dependency Pair:

REC(sent(sent(sent(x'''')))) -> REC(sent(sent(x'''')))

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)

Strategy:

innermost

The following dependency pair can be strictly oriented:

REC(sent(sent(sent(x'''')))) -> REC(sent(sent(x'''')))

The following usable rule for innermost can be oriented:

sent(up(x)) -> up(sent(x))

Used ordering: Polynomial ordering with Polynomial interpretation:

POL(up(x₁)) = x₁

POL(REC(x₁)) = 1 + x₁

POL(sent(x₁)) = 1 + x₁

resulting in one new DP problem.
Used Argument Filtering System:

REC(x₁) -> REC(x₁)
sent(x₁) -> sent(x₁)
up(x₁) -> up(x₁)

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳FwdInst

       →DP Problem 4

         ↳FwdInst

           →DP Problem 16

             ↳FwdInst

...

               →DP Problem 25

                 ↳Dependency Graph

       →DP Problem 5

         ↳FwdInst

       →DP Problem 6

         ↳FwdInst

Dependency Pair:

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)

Strategy:

innermost

Using the Dependency Graph resulted in no new DP problems.

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳FwdInst

       →DP Problem 4

         ↳FwdInst

       →DP Problem 5

         ↳Forward Instantiation Transformation

       →DP Problem 6

         ↳FwdInst

Dependency Pair:

CHECK(up(x)) -> CHECK(x)

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)

Strategy:

innermost

On this DP problem, a Forward Instantiation SCC transformation can be performed.
As a result of transforming the rule

CHECK(up(x)) -> CHECK(x)

one new Dependency Pair is created:

CHECK(up(up(x''))) -> CHECK(up(x''))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳FwdInst

       →DP Problem 4

         ↳FwdInst

       →DP Problem 5

         ↳FwdInst

           →DP Problem 26

             ↳Forward Instantiation Transformation

       →DP Problem 6

         ↳FwdInst

Dependency Pair:

CHECK(up(up(x''))) -> CHECK(up(x''))

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)

Strategy:

innermost

On this DP problem, a Forward Instantiation SCC transformation can be performed.
As a result of transforming the rule

CHECK(up(up(x''))) -> CHECK(up(x''))

one new Dependency Pair is created:

CHECK(up(up(up(x'''')))) -> CHECK(up(up(x'''')))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳FwdInst

       →DP Problem 4

         ↳FwdInst

       →DP Problem 5

         ↳FwdInst

           →DP Problem 26

             ↳FwdInst

...

               →DP Problem 27

                 ↳Argument Filtering and Ordering

       →DP Problem 6

         ↳FwdInst

Dependency Pair:

CHECK(up(up(up(x'''')))) -> CHECK(up(up(x'''')))

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)

Strategy:

innermost

The following dependency pair can be strictly oriented:

CHECK(up(up(up(x'''')))) -> CHECK(up(up(x'''')))

There are no usable rules for innermost that need to be oriented.
Used ordering: Polynomial ordering with Polynomial interpretation:

POL(up(x₁)) = 1 + x₁

POL(CHECK(x₁)) = 1 + x₁

resulting in one new DP problem.
Used Argument Filtering System:

CHECK(x₁) -> CHECK(x₁)
up(x₁) -> up(x₁)

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳FwdInst

       →DP Problem 4

         ↳FwdInst

       →DP Problem 5

         ↳FwdInst

           →DP Problem 26

             ↳FwdInst

...

               →DP Problem 28

                 ↳Dependency Graph

       →DP Problem 6

         ↳FwdInst

Dependency Pair:

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)

Strategy:

innermost

Using the Dependency Graph resulted in no new DP problems.

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳FwdInst

       →DP Problem 4

         ↳FwdInst

       →DP Problem 5

         ↳FwdInst

       →DP Problem 6

         ↳Forward Instantiation Transformation

Dependency Pairs:

CHECK(no(x)) -> CHECK(x)
CHECK(sent(x)) -> CHECK(x)

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)

Strategy:

innermost

On this DP problem, a Forward Instantiation SCC transformation can be performed.
As a result of transforming the rule

CHECK(sent(x)) -> CHECK(x)

two new Dependency Pairs are created:

CHECK(sent(sent(x''))) -> CHECK(sent(x''))
CHECK(sent(no(x''))) -> CHECK(no(x''))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳FwdInst

       →DP Problem 4

         ↳FwdInst

       →DP Problem 5

         ↳FwdInst

       →DP Problem 6

         ↳FwdInst

           →DP Problem 29

             ↳Forward Instantiation Transformation

Dependency Pairs:

CHECK(sent(no(x''))) -> CHECK(no(x''))
CHECK(sent(sent(x''))) -> CHECK(sent(x''))
CHECK(no(x)) -> CHECK(x)

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)

Strategy:

innermost

On this DP problem, a Forward Instantiation SCC transformation can be performed.
As a result of transforming the rule

CHECK(no(x)) -> CHECK(x)

three new Dependency Pairs are created:

CHECK(no(no(x''))) -> CHECK(no(x''))
CHECK(no(sent(sent(x'''')))) -> CHECK(sent(sent(x'''')))
CHECK(no(sent(no(x'''')))) -> CHECK(sent(no(x'''')))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳FwdInst

       →DP Problem 4

         ↳FwdInst

       →DP Problem 5

         ↳FwdInst

       →DP Problem 6

         ↳FwdInst

           →DP Problem 29

             ↳FwdInst

...

               →DP Problem 30

                 ↳Forward Instantiation Transformation

Dependency Pairs:

CHECK(no(sent(no(x'''')))) -> CHECK(sent(no(x'''')))
CHECK(sent(sent(x''))) -> CHECK(sent(x''))
CHECK(no(sent(sent(x'''')))) -> CHECK(sent(sent(x'''')))
CHECK(no(no(x''))) -> CHECK(no(x''))
CHECK(sent(no(x''))) -> CHECK(no(x''))

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)

Strategy:

innermost

On this DP problem, a Forward Instantiation SCC transformation can be performed.
As a result of transforming the rule

CHECK(sent(sent(x''))) -> CHECK(sent(x''))

two new Dependency Pairs are created:

CHECK(sent(sent(sent(x'''')))) -> CHECK(sent(sent(x'''')))
CHECK(sent(sent(no(x'''')))) -> CHECK(sent(no(x'''')))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳FwdInst

       →DP Problem 4

         ↳FwdInst

       →DP Problem 5

         ↳FwdInst

       →DP Problem 6

         ↳FwdInst

           →DP Problem 29

             ↳FwdInst

...

               →DP Problem 31

                 ↳Forward Instantiation Transformation

Dependency Pairs:

CHECK(sent(sent(no(x'''')))) -> CHECK(sent(no(x'''')))
CHECK(sent(sent(sent(x'''')))) -> CHECK(sent(sent(x'''')))
CHECK(no(sent(sent(x'''')))) -> CHECK(sent(sent(x'''')))
CHECK(no(no(x''))) -> CHECK(no(x''))
CHECK(sent(no(x''))) -> CHECK(no(x''))
CHECK(no(sent(no(x'''')))) -> CHECK(sent(no(x'''')))

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)

Strategy:

innermost

On this DP problem, a Forward Instantiation SCC transformation can be performed.
As a result of transforming the rule

CHECK(sent(no(x''))) -> CHECK(no(x''))

three new Dependency Pairs are created:

CHECK(sent(no(no(x'''')))) -> CHECK(no(no(x'''')))
CHECK(sent(no(sent(sent(x''''''))))) -> CHECK(no(sent(sent(x''''''))))
CHECK(sent(no(sent(no(x''''''))))) -> CHECK(no(sent(no(x''''''))))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳FwdInst

       →DP Problem 4

         ↳FwdInst

       →DP Problem 5

         ↳FwdInst

       →DP Problem 6

         ↳FwdInst

           →DP Problem 29

             ↳FwdInst

...

               →DP Problem 32

                 ↳Forward Instantiation Transformation

Dependency Pairs:

CHECK(sent(no(sent(no(x''''''))))) -> CHECK(no(sent(no(x''''''))))
CHECK(sent(no(sent(sent(x''''''))))) -> CHECK(no(sent(sent(x''''''))))
CHECK(no(sent(no(x'''')))) -> CHECK(sent(no(x'''')))
CHECK(sent(sent(sent(x'''')))) -> CHECK(sent(sent(x'''')))
CHECK(no(sent(sent(x'''')))) -> CHECK(sent(sent(x'''')))
CHECK(no(no(x''))) -> CHECK(no(x''))
CHECK(sent(no(no(x'''')))) -> CHECK(no(no(x'''')))
CHECK(sent(sent(no(x'''')))) -> CHECK(sent(no(x'''')))

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)

Strategy:

innermost

On this DP problem, a Forward Instantiation SCC transformation can be performed.
As a result of transforming the rule

CHECK(no(no(x''))) -> CHECK(no(x''))

three new Dependency Pairs are created:

CHECK(no(no(no(x'''')))) -> CHECK(no(no(x'''')))
CHECK(no(no(sent(sent(x''''''))))) -> CHECK(no(sent(sent(x''''''))))
CHECK(no(no(sent(no(x''''''))))) -> CHECK(no(sent(no(x''''''))))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳FwdInst

       →DP Problem 4

         ↳FwdInst

       →DP Problem 5

         ↳FwdInst

       →DP Problem 6

         ↳FwdInst

           →DP Problem 29

             ↳FwdInst

...

               →DP Problem 33

                 ↳Forward Instantiation Transformation

Dependency Pairs:

CHECK(no(no(sent(no(x''''''))))) -> CHECK(no(sent(no(x''''''))))
CHECK(sent(no(sent(sent(x''''''))))) -> CHECK(no(sent(sent(x''''''))))
CHECK(sent(sent(no(x'''')))) -> CHECK(sent(no(x'''')))
CHECK(sent(sent(sent(x'''')))) -> CHECK(sent(sent(x'''')))
CHECK(no(sent(sent(x'''')))) -> CHECK(sent(sent(x'''')))
CHECK(no(no(sent(sent(x''''''))))) -> CHECK(no(sent(sent(x''''''))))
CHECK(no(no(no(x'''')))) -> CHECK(no(no(x'''')))
CHECK(sent(no(no(x'''')))) -> CHECK(no(no(x'''')))
CHECK(no(sent(no(x'''')))) -> CHECK(sent(no(x'''')))
CHECK(sent(no(sent(no(x''''''))))) -> CHECK(no(sent(no(x''''''))))

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)

Strategy:

innermost

On this DP problem, a Forward Instantiation SCC transformation can be performed.
As a result of transforming the rule

CHECK(no(sent(sent(x'''')))) -> CHECK(sent(sent(x'''')))

two new Dependency Pairs are created:

CHECK(no(sent(sent(sent(x''''''))))) -> CHECK(sent(sent(sent(x''''''))))
CHECK(no(sent(sent(no(x''''''))))) -> CHECK(sent(sent(no(x''''''))))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳FwdInst

       →DP Problem 4

         ↳FwdInst

       →DP Problem 5

         ↳FwdInst

       →DP Problem 6

         ↳FwdInst

           →DP Problem 29

             ↳FwdInst

...

               →DP Problem 34

                 ↳Forward Instantiation Transformation

Dependency Pairs:

CHECK(sent(no(sent(no(x''''''))))) -> CHECK(no(sent(no(x''''''))))
CHECK(no(sent(sent(no(x''''''))))) -> CHECK(sent(sent(no(x''''''))))
CHECK(sent(no(sent(sent(x''''''))))) -> CHECK(no(sent(sent(x''''''))))
CHECK(sent(sent(no(x'''')))) -> CHECK(sent(no(x'''')))
CHECK(sent(sent(sent(x'''')))) -> CHECK(sent(sent(x'''')))
CHECK(no(sent(sent(sent(x''''''))))) -> CHECK(sent(sent(sent(x''''''))))
CHECK(no(no(sent(sent(x''''''))))) -> CHECK(no(sent(sent(x''''''))))
CHECK(no(no(no(x'''')))) -> CHECK(no(no(x'''')))
CHECK(sent(no(no(x'''')))) -> CHECK(no(no(x'''')))
CHECK(no(sent(no(x'''')))) -> CHECK(sent(no(x'''')))
CHECK(no(no(sent(no(x''''''))))) -> CHECK(no(sent(no(x''''''))))

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)

Strategy:

innermost

On this DP problem, a Forward Instantiation SCC transformation can be performed.
As a result of transforming the rule

CHECK(no(sent(no(x'''')))) -> CHECK(sent(no(x'''')))

three new Dependency Pairs are created:

CHECK(no(sent(no(no(x''''''))))) -> CHECK(sent(no(no(x''''''))))
CHECK(no(sent(no(sent(sent(x'''''''')))))) -> CHECK(sent(no(sent(sent(x'''''''')))))
CHECK(no(sent(no(sent(no(x'''''''')))))) -> CHECK(sent(no(sent(no(x'''''''')))))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳FwdInst

       →DP Problem 4

         ↳FwdInst

       →DP Problem 5

         ↳FwdInst

       →DP Problem 6

         ↳FwdInst

           →DP Problem 29

             ↳FwdInst

...

               →DP Problem 35

                 ↳Argument Filtering and Ordering

Dependency Pairs:

CHECK(no(sent(no(sent(no(x'''''''')))))) -> CHECK(sent(no(sent(no(x'''''''')))))
CHECK(no(sent(no(sent(sent(x'''''''')))))) -> CHECK(sent(no(sent(sent(x'''''''')))))
CHECK(no(no(sent(no(x''''''))))) -> CHECK(no(sent(no(x''''''))))
CHECK(no(sent(sent(no(x''''''))))) -> CHECK(sent(sent(no(x''''''))))
CHECK(sent(no(sent(sent(x''''''))))) -> CHECK(no(sent(sent(x''''''))))
CHECK(sent(sent(no(x'''')))) -> CHECK(sent(no(x'''')))
CHECK(sent(sent(sent(x'''')))) -> CHECK(sent(sent(x'''')))
CHECK(no(sent(sent(sent(x''''''))))) -> CHECK(sent(sent(sent(x''''''))))
CHECK(no(no(sent(sent(x''''''))))) -> CHECK(no(sent(sent(x''''''))))
CHECK(no(no(no(x'''')))) -> CHECK(no(no(x'''')))
CHECK(sent(no(no(x'''')))) -> CHECK(no(no(x'''')))
CHECK(no(sent(no(no(x''''''))))) -> CHECK(sent(no(no(x''''''))))
CHECK(sent(no(sent(no(x''''''))))) -> CHECK(no(sent(no(x''''''))))

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)

Strategy:

innermost

The following dependency pairs can be strictly oriented:

CHECK(no(sent(no(sent(no(x'''''''')))))) -> CHECK(sent(no(sent(no(x'''''''')))))
CHECK(no(sent(no(sent(sent(x'''''''')))))) -> CHECK(sent(no(sent(sent(x'''''''')))))
CHECK(no(no(sent(no(x''''''))))) -> CHECK(no(sent(no(x''''''))))
CHECK(no(sent(sent(no(x''''''))))) -> CHECK(sent(sent(no(x''''''))))
CHECK(no(sent(sent(sent(x''''''))))) -> CHECK(sent(sent(sent(x''''''))))
CHECK(no(no(sent(sent(x''''''))))) -> CHECK(no(sent(sent(x''''''))))
CHECK(no(no(no(x'''')))) -> CHECK(no(no(x'''')))
CHECK(no(sent(no(no(x''''''))))) -> CHECK(sent(no(no(x''''''))))

The following usable rules for innermost can be oriented:

no(up(x)) -> up(no(x))
sent(up(x)) -> up(sent(x))

Used ordering: Polynomial ordering with Polynomial interpretation:

POL(no(x₁)) = 1 + x₁

POL(up(x₁)) = x₁

POL(CHECK(x₁)) = 1 + x₁

POL(sent(x₁)) = x₁

resulting in one new DP problem.
Used Argument Filtering System:

CHECK(x₁) -> CHECK(x₁)
no(x₁) -> no(x₁)
sent(x₁) -> sent(x₁)
up(x₁) -> up(x₁)

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳FwdInst

       →DP Problem 4

         ↳FwdInst

       →DP Problem 5

         ↳FwdInst

       →DP Problem 6

         ↳FwdInst

           →DP Problem 29

             ↳FwdInst

...

               →DP Problem 36

                 ↳Dependency Graph

Dependency Pairs:

CHECK(sent(no(sent(sent(x''''''))))) -> CHECK(no(sent(sent(x''''''))))
CHECK(sent(sent(no(x'''')))) -> CHECK(sent(no(x'''')))
CHECK(sent(sent(sent(x'''')))) -> CHECK(sent(sent(x'''')))
CHECK(sent(no(no(x'''')))) -> CHECK(no(no(x'''')))
CHECK(sent(no(sent(no(x''''''))))) -> CHECK(no(sent(no(x''''''))))

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)

Strategy:

innermost

Using the Dependency Graph the DP problem was split into 1 DP problems.

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳FwdInst

       →DP Problem 4

         ↳FwdInst

       →DP Problem 5

         ↳FwdInst

       →DP Problem 6

         ↳FwdInst

           →DP Problem 29

             ↳FwdInst

...

               →DP Problem 37

                 ↳Argument Filtering and Ordering

Dependency Pair:

CHECK(sent(sent(sent(x'''')))) -> CHECK(sent(sent(x'''')))

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)

Strategy:

innermost

The following dependency pair can be strictly oriented:

CHECK(sent(sent(sent(x'''')))) -> CHECK(sent(sent(x'''')))

The following usable rule for innermost can be oriented:

sent(up(x)) -> up(sent(x))

Used ordering: Polynomial ordering with Polynomial interpretation:

POL(up(x₁)) = x₁

POL(CHECK(x₁)) = 1 + x₁

POL(sent(x₁)) = 1 + x₁

resulting in one new DP problem.
Used Argument Filtering System:

CHECK(x₁) -> CHECK(x₁)
sent(x₁) -> sent(x₁)
up(x₁) -> up(x₁)

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳FwdInst

       →DP Problem 4

         ↳FwdInst

       →DP Problem 5

         ↳FwdInst

       →DP Problem 6

         ↳FwdInst

           →DP Problem 29

             ↳FwdInst

...

               →DP Problem 38

                 ↳Dependency Graph

Dependency Pair:

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)

Strategy:

innermost

Using the Dependency Graph resulted in no new DP problems.

Innermost Termination of R successfully shown.
Duration:
0:03 minutes

POL(no(x₁))	= 1 + x₁
POL(up(x₁))	= x₁
POL(REC(x₁))	= 1 + x₁
POL(sent(x₁))	= x₁

POL(up(x₁))	= x₁
POL(CHECK(x₁))	= 1 + x₁
POL(sent(x₁))	= 1 + x₁