Termination w.r.t. Q proof of Secret_05_TRS

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

0 QTRS

↳1 DependencyPairsProof (⇔, 22 ms)

↳2 QDP

↳3 DependencyGraphProof (⇔, 0 ms)

↳4 AND

    ↳5 QDP

        ↳6 UsableRulesProof (⇔, 0 ms)

        ↳7 QDP

        ↳8 QDPSizeChangeProof (⇔, 0 ms)

        ↳9 YES

    ↳10 QDP

        ↳11 QDPOrderProof (⇔, 356 ms)

        ↳12 QDP

        ↳13 QDPOrderProof (⇔, 303 ms)

        ↳14 QDP

        ↳15 QDPOrderProof (⇔, 282 ms)

        ↳16 QDP

        ↳17 DependencyGraphProof (⇔, 0 ms)

        ↳18 QDP

        ↳19 UsableRulesProof (⇔, 0 ms)

        ↳20 QDP

        ↳21 UsableRulesReductionPairsProof (⇔, 0 ms)

        ↳22 QDP

        ↳23 PisEmptyProof (⇔, 0 ms)

        ↳24 YES

(0) Obligation:

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

intersect'ii'in(cons(X, X0), cons(X, X1)) → intersect'ii'out
intersect'ii'in(Xs, cons(X0, Ys)) → u'1'1(intersect'ii'in(Xs, Ys))
u'1'1(intersect'ii'out) → intersect'ii'out
intersect'ii'in(cons(X0, Xs), Ys) → u'2'1(intersect'ii'in(Xs, Ys))
u'2'1(intersect'ii'out) → intersect'ii'out
reduce'ii'in(sequent(cons(if(A, B), Fs), Gs), NF) → u'3'1(reduce'ii'in(sequent(cons(x'2b(x'2d(B), A), Fs), Gs), NF))
u'3'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(cons(iff(A, B), Fs), Gs), NF) → u'4'1(reduce'ii'in(sequent(cons(x'2a(if(A, B), if(B, A)), Fs), Gs), NF))
u'4'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(cons(x'2a(F1, F2), Fs), Gs), NF) → u'5'1(reduce'ii'in(sequent(cons(F1, cons(F2, Fs)), Gs), NF))
u'5'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(cons(x'2b(F1, F2), Fs), Gs), NF) → u'6'1(reduce'ii'in(sequent(cons(F1, Fs), Gs), NF), F2, Fs, Gs, NF)
u'6'1(reduce'ii'out, F2, Fs, Gs, NF) → u'6'2(reduce'ii'in(sequent(cons(F2, Fs), Gs), NF))
u'6'2(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(cons(x'2d(F1), Fs), Gs), NF) → u'7'1(reduce'ii'in(sequent(Fs, cons(F1, Gs)), NF))
u'7'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(Fs, cons(if(A, B), Gs)), NF) → u'8'1(reduce'ii'in(sequent(Fs, cons(x'2b(x'2d(B), A), Gs)), NF))
u'8'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(Fs, cons(iff(A, B), Gs)), NF) → u'9'1(reduce'ii'in(sequent(Fs, cons(x'2a(if(A, B), if(B, A)), Gs)), NF))
u'9'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(cons(p(V), Fs), Gs), sequent(Left, Right)) → u'10'1(reduce'ii'in(sequent(Fs, Gs), sequent(cons(p(V), Left), Right)))
u'10'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(Fs, cons(x'2b(G1, G2), Gs)), NF) → u'11'1(reduce'ii'in(sequent(Fs, cons(G1, cons(G2, Gs))), NF))
u'11'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(Fs, cons(x'2a(G1, G2), Gs)), NF) → u'12'1(reduce'ii'in(sequent(Fs, cons(G1, Gs)), NF), Fs, G2, Gs, NF)
u'12'1(reduce'ii'out, Fs, G2, Gs, NF) → u'12'2(reduce'ii'in(sequent(Fs, cons(G2, Gs)), NF))
u'12'2(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(Fs, cons(x'2d(G1), Gs)), NF) → u'13'1(reduce'ii'in(sequent(cons(G1, Fs), Gs), NF))
u'13'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(nil, cons(p(V), Gs)), sequent(Left, Right)) → u'14'1(reduce'ii'in(sequent(nil, Gs), sequent(Left, cons(p(V), Right))))
u'14'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(nil, nil), sequent(F1, F2)) → u'15'1(intersect'ii'in(F1, F2))
u'15'1(intersect'ii'out) → reduce'ii'out
tautology'i'in(F) → u'16'1(reduce'ii'in(sequent(nil, cons(F, nil)), sequent(nil, nil)))
u'16'1(reduce'ii'out) → tautology'i'out

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:

INTERSECT'II'IN(Xs, cons(X0, Ys)) → U'1'1(intersect'ii'in(Xs, Ys))
INTERSECT'II'IN(Xs, cons(X0, Ys)) → INTERSECT'II'IN(Xs, Ys)
INTERSECT'II'IN(cons(X0, Xs), Ys) → U'2'1(intersect'ii'in(Xs, Ys))
INTERSECT'II'IN(cons(X0, Xs), Ys) → INTERSECT'II'IN(Xs, Ys)
REDUCE'II'IN(sequent(cons(if(A, B), Fs), Gs), NF) → U'3'1(reduce'ii'in(sequent(cons(x'2b(x'2d(B), A), Fs), Gs), NF))
REDUCE'II'IN(sequent(cons(if(A, B), Fs), Gs), NF) → REDUCE'II'IN(sequent(cons(x'2b(x'2d(B), A), Fs), Gs), NF)
REDUCE'II'IN(sequent(cons(iff(A, B), Fs), Gs), NF) → U'4'1(reduce'ii'in(sequent(cons(x'2a(if(A, B), if(B, A)), Fs), Gs), NF))
REDUCE'II'IN(sequent(cons(iff(A, B), Fs), Gs), NF) → REDUCE'II'IN(sequent(cons(x'2a(if(A, B), if(B, A)), Fs), Gs), NF)
REDUCE'II'IN(sequent(cons(x'2a(F1, F2), Fs), Gs), NF) → U'5'1(reduce'ii'in(sequent(cons(F1, cons(F2, Fs)), Gs), NF))
REDUCE'II'IN(sequent(cons(x'2a(F1, F2), Fs), Gs), NF) → REDUCE'II'IN(sequent(cons(F1, cons(F2, Fs)), Gs), NF)
REDUCE'II'IN(sequent(cons(x'2b(F1, F2), Fs), Gs), NF) → U'6'1(reduce'ii'in(sequent(cons(F1, Fs), Gs), NF), F2, Fs, Gs, NF)
REDUCE'II'IN(sequent(cons(x'2b(F1, F2), Fs), Gs), NF) → REDUCE'II'IN(sequent(cons(F1, Fs), Gs), NF)
U'6'1(reduce'ii'out, F2, Fs, Gs, NF) → U'6'2(reduce'ii'in(sequent(cons(F2, Fs), Gs), NF))
U'6'1(reduce'ii'out, F2, Fs, Gs, NF) → REDUCE'II'IN(sequent(cons(F2, Fs), Gs), NF)
REDUCE'II'IN(sequent(cons(x'2d(F1), Fs), Gs), NF) → U'7'1(reduce'ii'in(sequent(Fs, cons(F1, Gs)), NF))
REDUCE'II'IN(sequent(cons(x'2d(F1), Fs), Gs), NF) → REDUCE'II'IN(sequent(Fs, cons(F1, Gs)), NF)
REDUCE'II'IN(sequent(Fs, cons(if(A, B), Gs)), NF) → U'8'1(reduce'ii'in(sequent(Fs, cons(x'2b(x'2d(B), A), Gs)), NF))
REDUCE'II'IN(sequent(Fs, cons(if(A, B), Gs)), NF) → REDUCE'II'IN(sequent(Fs, cons(x'2b(x'2d(B), A), Gs)), NF)
REDUCE'II'IN(sequent(Fs, cons(iff(A, B), Gs)), NF) → U'9'1(reduce'ii'in(sequent(Fs, cons(x'2a(if(A, B), if(B, A)), Gs)), NF))
REDUCE'II'IN(sequent(Fs, cons(iff(A, B), Gs)), NF) → REDUCE'II'IN(sequent(Fs, cons(x'2a(if(A, B), if(B, A)), Gs)), NF)
REDUCE'II'IN(sequent(cons(p(V), Fs), Gs), sequent(Left, Right)) → U'10'1(reduce'ii'in(sequent(Fs, Gs), sequent(cons(p(V), Left), Right)))
REDUCE'II'IN(sequent(cons(p(V), Fs), Gs), sequent(Left, Right)) → REDUCE'II'IN(sequent(Fs, Gs), sequent(cons(p(V), Left), Right))
REDUCE'II'IN(sequent(Fs, cons(x'2b(G1, G2), Gs)), NF) → U'11'1(reduce'ii'in(sequent(Fs, cons(G1, cons(G2, Gs))), NF))
REDUCE'II'IN(sequent(Fs, cons(x'2b(G1, G2), Gs)), NF) → REDUCE'II'IN(sequent(Fs, cons(G1, cons(G2, Gs))), NF)
REDUCE'II'IN(sequent(Fs, cons(x'2a(G1, G2), Gs)), NF) → U'12'1(reduce'ii'in(sequent(Fs, cons(G1, Gs)), NF), Fs, G2, Gs, NF)
REDUCE'II'IN(sequent(Fs, cons(x'2a(G1, G2), Gs)), NF) → REDUCE'II'IN(sequent(Fs, cons(G1, Gs)), NF)
U'12'1(reduce'ii'out, Fs, G2, Gs, NF) → U'12'2(reduce'ii'in(sequent(Fs, cons(G2, Gs)), NF))
U'12'1(reduce'ii'out, Fs, G2, Gs, NF) → REDUCE'II'IN(sequent(Fs, cons(G2, Gs)), NF)
REDUCE'II'IN(sequent(Fs, cons(x'2d(G1), Gs)), NF) → U'13'1(reduce'ii'in(sequent(cons(G1, Fs), Gs), NF))
REDUCE'II'IN(sequent(Fs, cons(x'2d(G1), Gs)), NF) → REDUCE'II'IN(sequent(cons(G1, Fs), Gs), NF)
REDUCE'II'IN(sequent(nil, cons(p(V), Gs)), sequent(Left, Right)) → U'14'1(reduce'ii'in(sequent(nil, Gs), sequent(Left, cons(p(V), Right))))
REDUCE'II'IN(sequent(nil, cons(p(V), Gs)), sequent(Left, Right)) → REDUCE'II'IN(sequent(nil, Gs), sequent(Left, cons(p(V), Right)))
REDUCE'II'IN(sequent(nil, nil), sequent(F1, F2)) → U'15'1(intersect'ii'in(F1, F2))
REDUCE'II'IN(sequent(nil, nil), sequent(F1, F2)) → INTERSECT'II'IN(F1, F2)
TAUTOLOGY'I'IN(F) → U'16'1(reduce'ii'in(sequent(nil, cons(F, nil)), sequent(nil, nil)))
TAUTOLOGY'I'IN(F) → REDUCE'II'IN(sequent(nil, cons(F, nil)), sequent(nil, nil))

The TRS R consists of the following rules:

intersect'ii'in(cons(X, X0), cons(X, X1)) → intersect'ii'out
intersect'ii'in(Xs, cons(X0, Ys)) → u'1'1(intersect'ii'in(Xs, Ys))
u'1'1(intersect'ii'out) → intersect'ii'out
intersect'ii'in(cons(X0, Xs), Ys) → u'2'1(intersect'ii'in(Xs, Ys))
u'2'1(intersect'ii'out) → intersect'ii'out
reduce'ii'in(sequent(cons(if(A, B), Fs), Gs), NF) → u'3'1(reduce'ii'in(sequent(cons(x'2b(x'2d(B), A), Fs), Gs), NF))
u'3'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(cons(iff(A, B), Fs), Gs), NF) → u'4'1(reduce'ii'in(sequent(cons(x'2a(if(A, B), if(B, A)), Fs), Gs), NF))
u'4'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(cons(x'2a(F1, F2), Fs), Gs), NF) → u'5'1(reduce'ii'in(sequent(cons(F1, cons(F2, Fs)), Gs), NF))
u'5'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(cons(x'2b(F1, F2), Fs), Gs), NF) → u'6'1(reduce'ii'in(sequent(cons(F1, Fs), Gs), NF), F2, Fs, Gs, NF)
u'6'1(reduce'ii'out, F2, Fs, Gs, NF) → u'6'2(reduce'ii'in(sequent(cons(F2, Fs), Gs), NF))
u'6'2(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(cons(x'2d(F1), Fs), Gs), NF) → u'7'1(reduce'ii'in(sequent(Fs, cons(F1, Gs)), NF))
u'7'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(Fs, cons(if(A, B), Gs)), NF) → u'8'1(reduce'ii'in(sequent(Fs, cons(x'2b(x'2d(B), A), Gs)), NF))
u'8'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(Fs, cons(iff(A, B), Gs)), NF) → u'9'1(reduce'ii'in(sequent(Fs, cons(x'2a(if(A, B), if(B, A)), Gs)), NF))
u'9'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(cons(p(V), Fs), Gs), sequent(Left, Right)) → u'10'1(reduce'ii'in(sequent(Fs, Gs), sequent(cons(p(V), Left), Right)))
u'10'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(Fs, cons(x'2b(G1, G2), Gs)), NF) → u'11'1(reduce'ii'in(sequent(Fs, cons(G1, cons(G2, Gs))), NF))
u'11'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(Fs, cons(x'2a(G1, G2), Gs)), NF) → u'12'1(reduce'ii'in(sequent(Fs, cons(G1, Gs)), NF), Fs, G2, Gs, NF)
u'12'1(reduce'ii'out, Fs, G2, Gs, NF) → u'12'2(reduce'ii'in(sequent(Fs, cons(G2, Gs)), NF))
u'12'2(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(Fs, cons(x'2d(G1), Gs)), NF) → u'13'1(reduce'ii'in(sequent(cons(G1, Fs), Gs), NF))
u'13'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(nil, cons(p(V), Gs)), sequent(Left, Right)) → u'14'1(reduce'ii'in(sequent(nil, Gs), sequent(Left, cons(p(V), Right))))
u'14'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(nil, nil), sequent(F1, F2)) → u'15'1(intersect'ii'in(F1, F2))
u'15'1(intersect'ii'out) → reduce'ii'out
tautology'i'in(F) → u'16'1(reduce'ii'in(sequent(nil, cons(F, nil)), sequent(nil, nil)))
u'16'1(reduce'ii'out) → tautology'i'out

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 2 SCCs with 18 less nodes.

(4) Complex Obligation (AND)

(5) Obligation:

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

INTERSECT'II'IN(cons(X0, Xs), Ys) → INTERSECT'II'IN(Xs, Ys)
INTERSECT'II'IN(Xs, cons(X0, Ys)) → INTERSECT'II'IN(Xs, Ys)

The TRS R consists of the following rules:

intersect'ii'in(cons(X, X0), cons(X, X1)) → intersect'ii'out
intersect'ii'in(Xs, cons(X0, Ys)) → u'1'1(intersect'ii'in(Xs, Ys))
u'1'1(intersect'ii'out) → intersect'ii'out
intersect'ii'in(cons(X0, Xs), Ys) → u'2'1(intersect'ii'in(Xs, Ys))
u'2'1(intersect'ii'out) → intersect'ii'out
reduce'ii'in(sequent(cons(if(A, B), Fs), Gs), NF) → u'3'1(reduce'ii'in(sequent(cons(x'2b(x'2d(B), A), Fs), Gs), NF))
u'3'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(cons(iff(A, B), Fs), Gs), NF) → u'4'1(reduce'ii'in(sequent(cons(x'2a(if(A, B), if(B, A)), Fs), Gs), NF))
u'4'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(cons(x'2a(F1, F2), Fs), Gs), NF) → u'5'1(reduce'ii'in(sequent(cons(F1, cons(F2, Fs)), Gs), NF))
u'5'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(cons(x'2b(F1, F2), Fs), Gs), NF) → u'6'1(reduce'ii'in(sequent(cons(F1, Fs), Gs), NF), F2, Fs, Gs, NF)
u'6'1(reduce'ii'out, F2, Fs, Gs, NF) → u'6'2(reduce'ii'in(sequent(cons(F2, Fs), Gs), NF))
u'6'2(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(cons(x'2d(F1), Fs), Gs), NF) → u'7'1(reduce'ii'in(sequent(Fs, cons(F1, Gs)), NF))
u'7'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(Fs, cons(if(A, B), Gs)), NF) → u'8'1(reduce'ii'in(sequent(Fs, cons(x'2b(x'2d(B), A), Gs)), NF))
u'8'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(Fs, cons(iff(A, B), Gs)), NF) → u'9'1(reduce'ii'in(sequent(Fs, cons(x'2a(if(A, B), if(B, A)), Gs)), NF))
u'9'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(cons(p(V), Fs), Gs), sequent(Left, Right)) → u'10'1(reduce'ii'in(sequent(Fs, Gs), sequent(cons(p(V), Left), Right)))
u'10'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(Fs, cons(x'2b(G1, G2), Gs)), NF) → u'11'1(reduce'ii'in(sequent(Fs, cons(G1, cons(G2, Gs))), NF))
u'11'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(Fs, cons(x'2a(G1, G2), Gs)), NF) → u'12'1(reduce'ii'in(sequent(Fs, cons(G1, Gs)), NF), Fs, G2, Gs, NF)
u'12'1(reduce'ii'out, Fs, G2, Gs, NF) → u'12'2(reduce'ii'in(sequent(Fs, cons(G2, Gs)), NF))
u'12'2(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(Fs, cons(x'2d(G1), Gs)), NF) → u'13'1(reduce'ii'in(sequent(cons(G1, Fs), Gs), NF))
u'13'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(nil, cons(p(V), Gs)), sequent(Left, Right)) → u'14'1(reduce'ii'in(sequent(nil, Gs), sequent(Left, cons(p(V), Right))))
u'14'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(nil, nil), sequent(F1, F2)) → u'15'1(intersect'ii'in(F1, F2))
u'15'1(intersect'ii'out) → reduce'ii'out
tautology'i'in(F) → u'16'1(reduce'ii'in(sequent(nil, cons(F, nil)), sequent(nil, nil)))
u'16'1(reduce'ii'out) → tautology'i'out

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

(6) 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.

(7) Obligation:

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

INTERSECT'II'IN(cons(X0, Xs), Ys) → INTERSECT'II'IN(Xs, Ys)
INTERSECT'II'IN(Xs, cons(X0, Ys)) → INTERSECT'II'IN(Xs, Ys)

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

(8) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

INTERSECT'II'IN(cons(X0, Xs), Ys) → INTERSECT'II'IN(Xs, Ys)
The graph contains the following edges 1 > 1, 2 >= 2
INTERSECT'II'IN(Xs, cons(X0, Ys)) → INTERSECT'II'IN(Xs, Ys)
The graph contains the following edges 1 >= 1, 2 > 2

(9) YES

(10) Obligation:

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

REDUCE'II'IN(sequent(cons(x'2b(F1, F2), Fs), Gs), NF) → U'6'1(reduce'ii'in(sequent(cons(F1, Fs), Gs), NF), F2, Fs, Gs, NF)
U'6'1(reduce'ii'out, F2, Fs, Gs, NF) → REDUCE'II'IN(sequent(cons(F2, Fs), Gs), NF)
REDUCE'II'IN(sequent(cons(if(A, B), Fs), Gs), NF) → REDUCE'II'IN(sequent(cons(x'2b(x'2d(B), A), Fs), Gs), NF)
REDUCE'II'IN(sequent(cons(x'2b(F1, F2), Fs), Gs), NF) → REDUCE'II'IN(sequent(cons(F1, Fs), Gs), NF)
REDUCE'II'IN(sequent(cons(iff(A, B), Fs), Gs), NF) → REDUCE'II'IN(sequent(cons(x'2a(if(A, B), if(B, A)), Fs), Gs), NF)
REDUCE'II'IN(sequent(cons(x'2a(F1, F2), Fs), Gs), NF) → REDUCE'II'IN(sequent(cons(F1, cons(F2, Fs)), Gs), NF)
REDUCE'II'IN(sequent(cons(x'2d(F1), Fs), Gs), NF) → REDUCE'II'IN(sequent(Fs, cons(F1, Gs)), NF)
REDUCE'II'IN(sequent(Fs, cons(if(A, B), Gs)), NF) → REDUCE'II'IN(sequent(Fs, cons(x'2b(x'2d(B), A), Gs)), NF)
REDUCE'II'IN(sequent(cons(p(V), Fs), Gs), sequent(Left, Right)) → REDUCE'II'IN(sequent(Fs, Gs), sequent(cons(p(V), Left), Right))
REDUCE'II'IN(sequent(Fs, cons(iff(A, B), Gs)), NF) → REDUCE'II'IN(sequent(Fs, cons(x'2a(if(A, B), if(B, A)), Gs)), NF)
REDUCE'II'IN(sequent(Fs, cons(x'2a(G1, G2), Gs)), NF) → U'12'1(reduce'ii'in(sequent(Fs, cons(G1, Gs)), NF), Fs, G2, Gs, NF)
U'12'1(reduce'ii'out, Fs, G2, Gs, NF) → REDUCE'II'IN(sequent(Fs, cons(G2, Gs)), NF)
REDUCE'II'IN(sequent(Fs, cons(x'2b(G1, G2), Gs)), NF) → REDUCE'II'IN(sequent(Fs, cons(G1, cons(G2, Gs))), NF)
REDUCE'II'IN(sequent(Fs, cons(x'2a(G1, G2), Gs)), NF) → REDUCE'II'IN(sequent(Fs, cons(G1, Gs)), NF)
REDUCE'II'IN(sequent(Fs, cons(x'2d(G1), Gs)), NF) → REDUCE'II'IN(sequent(cons(G1, Fs), Gs), NF)
REDUCE'II'IN(sequent(nil, cons(p(V), Gs)), sequent(Left, Right)) → REDUCE'II'IN(sequent(nil, Gs), sequent(Left, cons(p(V), Right)))

The TRS R consists of the following rules:

intersect'ii'in(cons(X, X0), cons(X, X1)) → intersect'ii'out
intersect'ii'in(Xs, cons(X0, Ys)) → u'1'1(intersect'ii'in(Xs, Ys))
u'1'1(intersect'ii'out) → intersect'ii'out
intersect'ii'in(cons(X0, Xs), Ys) → u'2'1(intersect'ii'in(Xs, Ys))
u'2'1(intersect'ii'out) → intersect'ii'out
reduce'ii'in(sequent(cons(if(A, B), Fs), Gs), NF) → u'3'1(reduce'ii'in(sequent(cons(x'2b(x'2d(B), A), Fs), Gs), NF))
u'3'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(cons(iff(A, B), Fs), Gs), NF) → u'4'1(reduce'ii'in(sequent(cons(x'2a(if(A, B), if(B, A)), Fs), Gs), NF))
u'4'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(cons(x'2a(F1, F2), Fs), Gs), NF) → u'5'1(reduce'ii'in(sequent(cons(F1, cons(F2, Fs)), Gs), NF))
u'5'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(cons(x'2b(F1, F2), Fs), Gs), NF) → u'6'1(reduce'ii'in(sequent(cons(F1, Fs), Gs), NF), F2, Fs, Gs, NF)
u'6'1(reduce'ii'out, F2, Fs, Gs, NF) → u'6'2(reduce'ii'in(sequent(cons(F2, Fs), Gs), NF))
u'6'2(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(cons(x'2d(F1), Fs), Gs), NF) → u'7'1(reduce'ii'in(sequent(Fs, cons(F1, Gs)), NF))
u'7'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(Fs, cons(if(A, B), Gs)), NF) → u'8'1(reduce'ii'in(sequent(Fs, cons(x'2b(x'2d(B), A), Gs)), NF))
u'8'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(Fs, cons(iff(A, B), Gs)), NF) → u'9'1(reduce'ii'in(sequent(Fs, cons(x'2a(if(A, B), if(B, A)), Gs)), NF))
u'9'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(cons(p(V), Fs), Gs), sequent(Left, Right)) → u'10'1(reduce'ii'in(sequent(Fs, Gs), sequent(cons(p(V), Left), Right)))
u'10'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(Fs, cons(x'2b(G1, G2), Gs)), NF) → u'11'1(reduce'ii'in(sequent(Fs, cons(G1, cons(G2, Gs))), NF))
u'11'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(Fs, cons(x'2a(G1, G2), Gs)), NF) → u'12'1(reduce'ii'in(sequent(Fs, cons(G1, Gs)), NF), Fs, G2, Gs, NF)
u'12'1(reduce'ii'out, Fs, G2, Gs, NF) → u'12'2(reduce'ii'in(sequent(Fs, cons(G2, Gs)), NF))
u'12'2(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(Fs, cons(x'2d(G1), Gs)), NF) → u'13'1(reduce'ii'in(sequent(cons(G1, Fs), Gs), NF))
u'13'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(nil, cons(p(V), Gs)), sequent(Left, Right)) → u'14'1(reduce'ii'in(sequent(nil, Gs), sequent(Left, cons(p(V), Right))))
u'14'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(nil, nil), sequent(F1, F2)) → u'15'1(intersect'ii'in(F1, F2))
u'15'1(intersect'ii'out) → reduce'ii'out
tautology'i'in(F) → u'16'1(reduce'ii'in(sequent(nil, cons(F, nil)), sequent(nil, nil)))
u'16'1(reduce'ii'out) → tautology'i'out

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

(11) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04,JAR06].

The following pairs can be oriented strictly and are deleted.

REDUCE'II'IN(sequent(cons(p(V), Fs), Gs), sequent(Left, Right)) → REDUCE'II'IN(sequent(Fs, Gs), sequent(cons(p(V), Left), Right))
REDUCE'II'IN(sequent(nil, cons(p(V), Gs)), sequent(Left, Right)) → REDUCE'II'IN(sequent(nil, Gs), sequent(Left, cons(p(V), Right)))

The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial Order [NEGPOLO,POLO] with Interpretation:

POL( U'12'1(x₁, ..., x₅) ) = x₁ + 2x₂ + 2x₃ + 2x₄ + 1

POL( U'6'1(x₁, ..., x₅) ) = x₁ + 2x₂ + 2x₃ + 2x₄ + 1

POL( reduce'ii'in(x₁, x₂) ) = 2

POL( sequent(x₁, x₂) ) = 2x₁ + 2x₂ + 1

POL( cons(x₁, x₂) ) = x₁ + x₂

POL( if(x₁, x₂) ) = x₁ + x₂

POL( u'3'1(x₁) ) = x₁

POL( x'2b(x₁, x₂) ) = x₁ + x₂

POL( x'2d(x₁) ) = x₁

POL( iff(x₁, x₂) ) = 2x₁ + 2x₂

POL( u'4'1(x₁) ) = x₁

POL( x'2a(x₁, x₂) ) = x₁ + x₂

POL( u'5'1(x₁) ) = x₁

POL( u'6'1(x₁, ..., x₅) ) = max{0, 2x₁ - 2}

POL( u'7'1(x₁) ) = x₁

POL( u'8'1(x₁) ) = max{0, 2x₁ - 2}

POL( u'9'1(x₁) ) = x₁

POL( p(x₁) ) = 2

POL( u'10'1(x₁) ) = x₁

POL( u'11'1(x₁) ) = 2

POL( u'12'1(x₁, ..., x₅) ) = x₁

POL( u'13'1(x₁) ) = 2

POL( nil ) = 0

POL( u'14'1(x₁) ) = 2

POL( reduce'ii'out ) = 2

POL( u'15'1(x₁) ) = max{0, 2x₁ - 2}

POL( intersect'ii'in(x₁, x₂) ) = 2

POL( u'12'2(x₁) ) = max{0, 2x₁ - 2}

POL( u'6'2(x₁) ) = max{0, 2x₁ - 2}

POL( intersect'ii'out ) = 2

POL( u'1'1(x₁) ) = max{0, 2x₁ - 2}

POL( u'2'1(x₁) ) = 2

POL( REDUCE'II'IN(x₁, x₂) ) = x₁ + 2

The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:

reduce'ii'in(sequent(cons(if(A, B), Fs), Gs), NF) → u'3'1(reduce'ii'in(sequent(cons(x'2b(x'2d(B), A), Fs), Gs), NF))
reduce'ii'in(sequent(cons(iff(A, B), Fs), Gs), NF) → u'4'1(reduce'ii'in(sequent(cons(x'2a(if(A, B), if(B, A)), Fs), Gs), NF))
reduce'ii'in(sequent(cons(x'2a(F1, F2), Fs), Gs), NF) → u'5'1(reduce'ii'in(sequent(cons(F1, cons(F2, Fs)), Gs), NF))
reduce'ii'in(sequent(cons(x'2b(F1, F2), Fs), Gs), NF) → u'6'1(reduce'ii'in(sequent(cons(F1, Fs), Gs), NF), F2, Fs, Gs, NF)
reduce'ii'in(sequent(cons(x'2d(F1), Fs), Gs), NF) → u'7'1(reduce'ii'in(sequent(Fs, cons(F1, Gs)), NF))
reduce'ii'in(sequent(Fs, cons(if(A, B), Gs)), NF) → u'8'1(reduce'ii'in(sequent(Fs, cons(x'2b(x'2d(B), A), Gs)), NF))
reduce'ii'in(sequent(Fs, cons(iff(A, B), Gs)), NF) → u'9'1(reduce'ii'in(sequent(Fs, cons(x'2a(if(A, B), if(B, A)), Gs)), NF))
reduce'ii'in(sequent(cons(p(V), Fs), Gs), sequent(Left, Right)) → u'10'1(reduce'ii'in(sequent(Fs, Gs), sequent(cons(p(V), Left), Right)))
reduce'ii'in(sequent(Fs, cons(x'2b(G1, G2), Gs)), NF) → u'11'1(reduce'ii'in(sequent(Fs, cons(G1, cons(G2, Gs))), NF))
reduce'ii'in(sequent(Fs, cons(x'2a(G1, G2), Gs)), NF) → u'12'1(reduce'ii'in(sequent(Fs, cons(G1, Gs)), NF), Fs, G2, Gs, NF)
reduce'ii'in(sequent(Fs, cons(x'2d(G1), Gs)), NF) → u'13'1(reduce'ii'in(sequent(cons(G1, Fs), Gs), NF))
reduce'ii'in(sequent(nil, cons(p(V), Gs)), sequent(Left, Right)) → u'14'1(reduce'ii'in(sequent(nil, Gs), sequent(Left, cons(p(V), Right))))
u'3'1(reduce'ii'out) → reduce'ii'out
u'4'1(reduce'ii'out) → reduce'ii'out
u'5'1(reduce'ii'out) → reduce'ii'out
u'7'1(reduce'ii'out) → reduce'ii'out
u'8'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(nil, nil), sequent(F1, F2)) → u'15'1(intersect'ii'in(F1, F2))
u'10'1(reduce'ii'out) → reduce'ii'out
u'9'1(reduce'ii'out) → reduce'ii'out
u'11'1(reduce'ii'out) → reduce'ii'out
u'13'1(reduce'ii'out) → reduce'ii'out
u'14'1(reduce'ii'out) → reduce'ii'out
u'12'1(reduce'ii'out, Fs, G2, Gs, NF) → u'12'2(reduce'ii'in(sequent(Fs, cons(G2, Gs)), NF))
u'12'2(reduce'ii'out) → reduce'ii'out
u'6'1(reduce'ii'out, F2, Fs, Gs, NF) → u'6'2(reduce'ii'in(sequent(cons(F2, Fs), Gs), NF))
u'6'2(reduce'ii'out) → reduce'ii'out
intersect'ii'in(cons(X, X0), cons(X, X1)) → intersect'ii'out
intersect'ii'in(Xs, cons(X0, Ys)) → u'1'1(intersect'ii'in(Xs, Ys))
intersect'ii'in(cons(X0, Xs), Ys) → u'2'1(intersect'ii'in(Xs, Ys))
u'15'1(intersect'ii'out) → reduce'ii'out
u'2'1(intersect'ii'out) → intersect'ii'out
u'1'1(intersect'ii'out) → intersect'ii'out

(12) Obligation:

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

REDUCE'II'IN(sequent(cons(x'2b(F1, F2), Fs), Gs), NF) → U'6'1(reduce'ii'in(sequent(cons(F1, Fs), Gs), NF), F2, Fs, Gs, NF)
U'6'1(reduce'ii'out, F2, Fs, Gs, NF) → REDUCE'II'IN(sequent(cons(F2, Fs), Gs), NF)
REDUCE'II'IN(sequent(cons(if(A, B), Fs), Gs), NF) → REDUCE'II'IN(sequent(cons(x'2b(x'2d(B), A), Fs), Gs), NF)
REDUCE'II'IN(sequent(cons(x'2b(F1, F2), Fs), Gs), NF) → REDUCE'II'IN(sequent(cons(F1, Fs), Gs), NF)
REDUCE'II'IN(sequent(cons(iff(A, B), Fs), Gs), NF) → REDUCE'II'IN(sequent(cons(x'2a(if(A, B), if(B, A)), Fs), Gs), NF)
REDUCE'II'IN(sequent(cons(x'2a(F1, F2), Fs), Gs), NF) → REDUCE'II'IN(sequent(cons(F1, cons(F2, Fs)), Gs), NF)
REDUCE'II'IN(sequent(cons(x'2d(F1), Fs), Gs), NF) → REDUCE'II'IN(sequent(Fs, cons(F1, Gs)), NF)
REDUCE'II'IN(sequent(Fs, cons(if(A, B), Gs)), NF) → REDUCE'II'IN(sequent(Fs, cons(x'2b(x'2d(B), A), Gs)), NF)
REDUCE'II'IN(sequent(Fs, cons(iff(A, B), Gs)), NF) → REDUCE'II'IN(sequent(Fs, cons(x'2a(if(A, B), if(B, A)), Gs)), NF)
REDUCE'II'IN(sequent(Fs, cons(x'2a(G1, G2), Gs)), NF) → U'12'1(reduce'ii'in(sequent(Fs, cons(G1, Gs)), NF), Fs, G2, Gs, NF)
U'12'1(reduce'ii'out, Fs, G2, Gs, NF) → REDUCE'II'IN(sequent(Fs, cons(G2, Gs)), NF)
REDUCE'II'IN(sequent(Fs, cons(x'2b(G1, G2), Gs)), NF) → REDUCE'II'IN(sequent(Fs, cons(G1, cons(G2, Gs))), NF)
REDUCE'II'IN(sequent(Fs, cons(x'2a(G1, G2), Gs)), NF) → REDUCE'II'IN(sequent(Fs, cons(G1, Gs)), NF)
REDUCE'II'IN(sequent(Fs, cons(x'2d(G1), Gs)), NF) → REDUCE'II'IN(sequent(cons(G1, Fs), Gs), NF)

The TRS R consists of the following rules:

intersect'ii'in(cons(X, X0), cons(X, X1)) → intersect'ii'out
intersect'ii'in(Xs, cons(X0, Ys)) → u'1'1(intersect'ii'in(Xs, Ys))
u'1'1(intersect'ii'out) → intersect'ii'out
intersect'ii'in(cons(X0, Xs), Ys) → u'2'1(intersect'ii'in(Xs, Ys))
u'2'1(intersect'ii'out) → intersect'ii'out
reduce'ii'in(sequent(cons(if(A, B), Fs), Gs), NF) → u'3'1(reduce'ii'in(sequent(cons(x'2b(x'2d(B), A), Fs), Gs), NF))
u'3'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(cons(iff(A, B), Fs), Gs), NF) → u'4'1(reduce'ii'in(sequent(cons(x'2a(if(A, B), if(B, A)), Fs), Gs), NF))
u'4'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(cons(x'2a(F1, F2), Fs), Gs), NF) → u'5'1(reduce'ii'in(sequent(cons(F1, cons(F2, Fs)), Gs), NF))
u'5'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(cons(x'2b(F1, F2), Fs), Gs), NF) → u'6'1(reduce'ii'in(sequent(cons(F1, Fs), Gs), NF), F2, Fs, Gs, NF)
u'6'1(reduce'ii'out, F2, Fs, Gs, NF) → u'6'2(reduce'ii'in(sequent(cons(F2, Fs), Gs), NF))
u'6'2(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(cons(x'2d(F1), Fs), Gs), NF) → u'7'1(reduce'ii'in(sequent(Fs, cons(F1, Gs)), NF))
u'7'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(Fs, cons(if(A, B), Gs)), NF) → u'8'1(reduce'ii'in(sequent(Fs, cons(x'2b(x'2d(B), A), Gs)), NF))
u'8'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(Fs, cons(iff(A, B), Gs)), NF) → u'9'1(reduce'ii'in(sequent(Fs, cons(x'2a(if(A, B), if(B, A)), Gs)), NF))
u'9'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(cons(p(V), Fs), Gs), sequent(Left, Right)) → u'10'1(reduce'ii'in(sequent(Fs, Gs), sequent(cons(p(V), Left), Right)))
u'10'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(Fs, cons(x'2b(G1, G2), Gs)), NF) → u'11'1(reduce'ii'in(sequent(Fs, cons(G1, cons(G2, Gs))), NF))
u'11'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(Fs, cons(x'2a(G1, G2), Gs)), NF) → u'12'1(reduce'ii'in(sequent(Fs, cons(G1, Gs)), NF), Fs, G2, Gs, NF)
u'12'1(reduce'ii'out, Fs, G2, Gs, NF) → u'12'2(reduce'ii'in(sequent(Fs, cons(G2, Gs)), NF))
u'12'2(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(Fs, cons(x'2d(G1), Gs)), NF) → u'13'1(reduce'ii'in(sequent(cons(G1, Fs), Gs), NF))
u'13'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(nil, cons(p(V), Gs)), sequent(Left, Right)) → u'14'1(reduce'ii'in(sequent(nil, Gs), sequent(Left, cons(p(V), Right))))
u'14'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(nil, nil), sequent(F1, F2)) → u'15'1(intersect'ii'in(F1, F2))
u'15'1(intersect'ii'out) → reduce'ii'out
tautology'i'in(F) → u'16'1(reduce'ii'in(sequent(nil, cons(F, nil)), sequent(nil, nil)))
u'16'1(reduce'ii'out) → tautology'i'out

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

(13) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04,JAR06].

The following pairs can be oriented strictly and are deleted.

REDUCE'II'IN(sequent(cons(iff(A, B), Fs), Gs), NF) → REDUCE'II'IN(sequent(cons(x'2a(if(A, B), if(B, A)), Fs), Gs), NF)
REDUCE'II'IN(sequent(Fs, cons(iff(A, B), Gs)), NF) → REDUCE'II'IN(sequent(Fs, cons(x'2a(if(A, B), if(B, A)), Gs)), NF)

The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial Order [NEGPOLO,POLO] with Interpretation:

POL( U'12'1(x₁, ..., x₅) ) = max{0, 2x₁ + 2x₂ + 2x₃ + 2x₄ + 2x₅ - 2}

POL( U'6'1(x₁, ..., x₅) ) = 2x₂ + 2x₃ + 2x₄ + 2x₅ + 2

POL( reduce'ii'in(x₁, x₂) ) = 2

POL( sequent(x₁, x₂) ) = 2x₁ + 2x₂ + 1

POL( cons(x₁, x₂) ) = x₁ + x₂

POL( if(x₁, x₂) ) = x₁ + x₂

POL( u'3'1(x₁) ) = 2

POL( x'2b(x₁, x₂) ) = x₁ + x₂

POL( x'2d(x₁) ) = x₁

POL( iff(x₁, x₂) ) = 2x₁ + 2x₂ + 1

POL( u'4'1(x₁) ) = 2

POL( x'2a(x₁, x₂) ) = x₁ + x₂

POL( u'5'1(x₁) ) = x₁

POL( u'6'1(x₁, ..., x₅) ) = x₁

POL( u'7'1(x₁) ) = 2

POL( u'8'1(x₁) ) = 2

POL( u'9'1(x₁) ) = x₁

POL( p(x₁) ) = 0

POL( u'10'1(x₁) ) = 2

POL( u'11'1(x₁) ) = 2

POL( u'12'1(x₁, ..., x₅) ) = max{0, 2x₁ - 2}

POL( u'13'1(x₁) ) = max{0, 2x₁ - 2}

POL( nil ) = 0

POL( u'14'1(x₁) ) = x₁

POL( reduce'ii'out ) = 2

POL( u'15'1(x₁) ) = 2

POL( intersect'ii'in(x₁, x₂) ) = x₂ + 1

POL( u'12'2(x₁) ) = x₁

POL( u'6'2(x₁) ) = x₁

POL( intersect'ii'out ) = 1

POL( u'1'1(x₁) ) = max{0, x₁ - 1}

POL( u'2'1(x₁) ) = max{0, -2}

POL( REDUCE'II'IN(x₁, x₂) ) = x₁ + 2x₂ + 1

The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:

reduce'ii'in(sequent(cons(if(A, B), Fs), Gs), NF) → u'3'1(reduce'ii'in(sequent(cons(x'2b(x'2d(B), A), Fs), Gs), NF))
reduce'ii'in(sequent(cons(iff(A, B), Fs), Gs), NF) → u'4'1(reduce'ii'in(sequent(cons(x'2a(if(A, B), if(B, A)), Fs), Gs), NF))
reduce'ii'in(sequent(cons(x'2a(F1, F2), Fs), Gs), NF) → u'5'1(reduce'ii'in(sequent(cons(F1, cons(F2, Fs)), Gs), NF))
reduce'ii'in(sequent(cons(x'2b(F1, F2), Fs), Gs), NF) → u'6'1(reduce'ii'in(sequent(cons(F1, Fs), Gs), NF), F2, Fs, Gs, NF)
reduce'ii'in(sequent(cons(x'2d(F1), Fs), Gs), NF) → u'7'1(reduce'ii'in(sequent(Fs, cons(F1, Gs)), NF))
reduce'ii'in(sequent(Fs, cons(if(A, B), Gs)), NF) → u'8'1(reduce'ii'in(sequent(Fs, cons(x'2b(x'2d(B), A), Gs)), NF))
reduce'ii'in(sequent(Fs, cons(iff(A, B), Gs)), NF) → u'9'1(reduce'ii'in(sequent(Fs, cons(x'2a(if(A, B), if(B, A)), Gs)), NF))
reduce'ii'in(sequent(cons(p(V), Fs), Gs), sequent(Left, Right)) → u'10'1(reduce'ii'in(sequent(Fs, Gs), sequent(cons(p(V), Left), Right)))
reduce'ii'in(sequent(Fs, cons(x'2b(G1, G2), Gs)), NF) → u'11'1(reduce'ii'in(sequent(Fs, cons(G1, cons(G2, Gs))), NF))
reduce'ii'in(sequent(Fs, cons(x'2a(G1, G2), Gs)), NF) → u'12'1(reduce'ii'in(sequent(Fs, cons(G1, Gs)), NF), Fs, G2, Gs, NF)
reduce'ii'in(sequent(Fs, cons(x'2d(G1), Gs)), NF) → u'13'1(reduce'ii'in(sequent(cons(G1, Fs), Gs), NF))
reduce'ii'in(sequent(nil, cons(p(V), Gs)), sequent(Left, Right)) → u'14'1(reduce'ii'in(sequent(nil, Gs), sequent(Left, cons(p(V), Right))))
u'3'1(reduce'ii'out) → reduce'ii'out
u'4'1(reduce'ii'out) → reduce'ii'out
u'5'1(reduce'ii'out) → reduce'ii'out
u'7'1(reduce'ii'out) → reduce'ii'out
u'8'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(nil, nil), sequent(F1, F2)) → u'15'1(intersect'ii'in(F1, F2))
u'10'1(reduce'ii'out) → reduce'ii'out
u'9'1(reduce'ii'out) → reduce'ii'out
u'11'1(reduce'ii'out) → reduce'ii'out
u'13'1(reduce'ii'out) → reduce'ii'out
u'14'1(reduce'ii'out) → reduce'ii'out
u'12'1(reduce'ii'out, Fs, G2, Gs, NF) → u'12'2(reduce'ii'in(sequent(Fs, cons(G2, Gs)), NF))
u'12'2(reduce'ii'out) → reduce'ii'out
u'6'1(reduce'ii'out, F2, Fs, Gs, NF) → u'6'2(reduce'ii'in(sequent(cons(F2, Fs), Gs), NF))
u'6'2(reduce'ii'out) → reduce'ii'out
u'15'1(intersect'ii'out) → reduce'ii'out

(14) Obligation:

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

REDUCE'II'IN(sequent(cons(x'2b(F1, F2), Fs), Gs), NF) → U'6'1(reduce'ii'in(sequent(cons(F1, Fs), Gs), NF), F2, Fs, Gs, NF)
U'6'1(reduce'ii'out, F2, Fs, Gs, NF) → REDUCE'II'IN(sequent(cons(F2, Fs), Gs), NF)
REDUCE'II'IN(sequent(cons(if(A, B), Fs), Gs), NF) → REDUCE'II'IN(sequent(cons(x'2b(x'2d(B), A), Fs), Gs), NF)
REDUCE'II'IN(sequent(cons(x'2b(F1, F2), Fs), Gs), NF) → REDUCE'II'IN(sequent(cons(F1, Fs), Gs), NF)
REDUCE'II'IN(sequent(cons(x'2a(F1, F2), Fs), Gs), NF) → REDUCE'II'IN(sequent(cons(F1, cons(F2, Fs)), Gs), NF)
REDUCE'II'IN(sequent(cons(x'2d(F1), Fs), Gs), NF) → REDUCE'II'IN(sequent(Fs, cons(F1, Gs)), NF)
REDUCE'II'IN(sequent(Fs, cons(if(A, B), Gs)), NF) → REDUCE'II'IN(sequent(Fs, cons(x'2b(x'2d(B), A), Gs)), NF)
REDUCE'II'IN(sequent(Fs, cons(x'2a(G1, G2), Gs)), NF) → U'12'1(reduce'ii'in(sequent(Fs, cons(G1, Gs)), NF), Fs, G2, Gs, NF)
U'12'1(reduce'ii'out, Fs, G2, Gs, NF) → REDUCE'II'IN(sequent(Fs, cons(G2, Gs)), NF)
REDUCE'II'IN(sequent(Fs, cons(x'2b(G1, G2), Gs)), NF) → REDUCE'II'IN(sequent(Fs, cons(G1, cons(G2, Gs))), NF)
REDUCE'II'IN(sequent(Fs, cons(x'2a(G1, G2), Gs)), NF) → REDUCE'II'IN(sequent(Fs, cons(G1, Gs)), NF)
REDUCE'II'IN(sequent(Fs, cons(x'2d(G1), Gs)), NF) → REDUCE'II'IN(sequent(cons(G1, Fs), Gs), NF)

The TRS R consists of the following rules:

intersect'ii'in(cons(X, X0), cons(X, X1)) → intersect'ii'out
intersect'ii'in(Xs, cons(X0, Ys)) → u'1'1(intersect'ii'in(Xs, Ys))
u'1'1(intersect'ii'out) → intersect'ii'out
intersect'ii'in(cons(X0, Xs), Ys) → u'2'1(intersect'ii'in(Xs, Ys))
u'2'1(intersect'ii'out) → intersect'ii'out
reduce'ii'in(sequent(cons(if(A, B), Fs), Gs), NF) → u'3'1(reduce'ii'in(sequent(cons(x'2b(x'2d(B), A), Fs), Gs), NF))
u'3'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(cons(iff(A, B), Fs), Gs), NF) → u'4'1(reduce'ii'in(sequent(cons(x'2a(if(A, B), if(B, A)), Fs), Gs), NF))
u'4'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(cons(x'2a(F1, F2), Fs), Gs), NF) → u'5'1(reduce'ii'in(sequent(cons(F1, cons(F2, Fs)), Gs), NF))
u'5'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(cons(x'2b(F1, F2), Fs), Gs), NF) → u'6'1(reduce'ii'in(sequent(cons(F1, Fs), Gs), NF), F2, Fs, Gs, NF)
u'6'1(reduce'ii'out, F2, Fs, Gs, NF) → u'6'2(reduce'ii'in(sequent(cons(F2, Fs), Gs), NF))
u'6'2(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(cons(x'2d(F1), Fs), Gs), NF) → u'7'1(reduce'ii'in(sequent(Fs, cons(F1, Gs)), NF))
u'7'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(Fs, cons(if(A, B), Gs)), NF) → u'8'1(reduce'ii'in(sequent(Fs, cons(x'2b(x'2d(B), A), Gs)), NF))
u'8'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(Fs, cons(iff(A, B), Gs)), NF) → u'9'1(reduce'ii'in(sequent(Fs, cons(x'2a(if(A, B), if(B, A)), Gs)), NF))
u'9'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(cons(p(V), Fs), Gs), sequent(Left, Right)) → u'10'1(reduce'ii'in(sequent(Fs, Gs), sequent(cons(p(V), Left), Right)))
u'10'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(Fs, cons(x'2b(G1, G2), Gs)), NF) → u'11'1(reduce'ii'in(sequent(Fs, cons(G1, cons(G2, Gs))), NF))
u'11'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(Fs, cons(x'2a(G1, G2), Gs)), NF) → u'12'1(reduce'ii'in(sequent(Fs, cons(G1, Gs)), NF), Fs, G2, Gs, NF)
u'12'1(reduce'ii'out, Fs, G2, Gs, NF) → u'12'2(reduce'ii'in(sequent(Fs, cons(G2, Gs)), NF))
u'12'2(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(Fs, cons(x'2d(G1), Gs)), NF) → u'13'1(reduce'ii'in(sequent(cons(G1, Fs), Gs), NF))
u'13'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(nil, cons(p(V), Gs)), sequent(Left, Right)) → u'14'1(reduce'ii'in(sequent(nil, Gs), sequent(Left, cons(p(V), Right))))
u'14'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(nil, nil), sequent(F1, F2)) → u'15'1(intersect'ii'in(F1, F2))
u'15'1(intersect'ii'out) → reduce'ii'out
tautology'i'in(F) → u'16'1(reduce'ii'in(sequent(nil, cons(F, nil)), sequent(nil, nil)))
u'16'1(reduce'ii'out) → tautology'i'out

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

(15) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04,JAR06].

The following pairs can be oriented strictly and are deleted.

REDUCE'II'IN(sequent(cons(x'2b(F1, F2), Fs), Gs), NF) → U'6'1(reduce'ii'in(sequent(cons(F1, Fs), Gs), NF), F2, Fs, Gs, NF)
REDUCE'II'IN(sequent(cons(x'2b(F1, F2), Fs), Gs), NF) → REDUCE'II'IN(sequent(cons(F1, Fs), Gs), NF)
REDUCE'II'IN(sequent(cons(x'2a(F1, F2), Fs), Gs), NF) → REDUCE'II'IN(sequent(cons(F1, cons(F2, Fs)), Gs), NF)
REDUCE'II'IN(sequent(cons(x'2d(F1), Fs), Gs), NF) → REDUCE'II'IN(sequent(Fs, cons(F1, Gs)), NF)
REDUCE'II'IN(sequent(Fs, cons(x'2a(G1, G2), Gs)), NF) → U'12'1(reduce'ii'in(sequent(Fs, cons(G1, Gs)), NF), Fs, G2, Gs, NF)
REDUCE'II'IN(sequent(Fs, cons(x'2b(G1, G2), Gs)), NF) → REDUCE'II'IN(sequent(Fs, cons(G1, cons(G2, Gs))), NF)
REDUCE'II'IN(sequent(Fs, cons(x'2a(G1, G2), Gs)), NF) → REDUCE'II'IN(sequent(Fs, cons(G1, Gs)), NF)
REDUCE'II'IN(sequent(Fs, cons(x'2d(G1), Gs)), NF) → REDUCE'II'IN(sequent(cons(G1, Fs), Gs), NF)

The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial Order [NEGPOLO,POLO] with Interpretation:

POL( U'12'1(x₁, ..., x₅) ) = x₂ + x₃ + x₄ + 2

POL( U'6'1(x₁, ..., x₅) ) = 2x₂ + x₃ + x₄ + 2

POL( reduce'ii'in(x₁, x₂) ) = max{0, x₁ - 1}

POL( sequent(x₁, x₂) ) = x₁ + x₂ + 1

POL( cons(x₁, x₂) ) = x₁ + x₂

POL( if(x₁, x₂) ) = 2x₁ + x₂ + 2

POL( u'3'1(x₁) ) = x₁ + 1

POL( x'2b(x₁, x₂) ) = x₁ + 2x₂ + 1

POL( x'2d(x₁) ) = x₁ + 1

POL( iff(x₁, x₂) ) = 0

POL( u'4'1(x₁) ) = max{0, -2}

POL( x'2a(x₁, x₂) ) = x₁ + x₂ + 2

POL( u'5'1(x₁) ) = 1

POL( u'6'1(x₁, ..., x₅) ) = 2x₂ + x₃ + x₄ + 1

POL( u'7'1(x₁) ) = max{0, 2x₁ - 2}

POL( u'8'1(x₁) ) = 0

POL( u'9'1(x₁) ) = max{0, -1}

POL( p(x₁) ) = 0

POL( u'10'1(x₁) ) = 1

POL( u'11'1(x₁) ) = x₁ + 1

POL( u'12'1(x₁, ..., x₅) ) = 2x₁ + x₃ + 2x₄ + 2

POL( u'13'1(x₁) ) = 2x₁ + 1

POL( nil ) = 0

POL( u'14'1(x₁) ) = 0

POL( reduce'ii'out ) = 1

POL( u'15'1(x₁) ) = 2x₁ + 2

POL( intersect'ii'in(x₁, x₂) ) = 0

POL( u'12'2(x₁) ) = max{0, -2}

POL( u'6'2(x₁) ) = x₁ + 1

POL( intersect'ii'out ) = 0

POL( u'1'1(x₁) ) = max{0, -2}

POL( u'2'1(x₁) ) = max{0, 2x₁ - 2}

POL( REDUCE'II'IN(x₁, x₂) ) = x₁ + 1

The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:
none

(16) Obligation:

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

U'6'1(reduce'ii'out, F2, Fs, Gs, NF) → REDUCE'II'IN(sequent(cons(F2, Fs), Gs), NF)
REDUCE'II'IN(sequent(cons(if(A, B), Fs), Gs), NF) → REDUCE'II'IN(sequent(cons(x'2b(x'2d(B), A), Fs), Gs), NF)
REDUCE'II'IN(sequent(Fs, cons(if(A, B), Gs)), NF) → REDUCE'II'IN(sequent(Fs, cons(x'2b(x'2d(B), A), Gs)), NF)
U'12'1(reduce'ii'out, Fs, G2, Gs, NF) → REDUCE'II'IN(sequent(Fs, cons(G2, Gs)), NF)

The TRS R consists of the following rules:

intersect'ii'in(cons(X, X0), cons(X, X1)) → intersect'ii'out
intersect'ii'in(Xs, cons(X0, Ys)) → u'1'1(intersect'ii'in(Xs, Ys))
u'1'1(intersect'ii'out) → intersect'ii'out
intersect'ii'in(cons(X0, Xs), Ys) → u'2'1(intersect'ii'in(Xs, Ys))
u'2'1(intersect'ii'out) → intersect'ii'out
reduce'ii'in(sequent(cons(if(A, B), Fs), Gs), NF) → u'3'1(reduce'ii'in(sequent(cons(x'2b(x'2d(B), A), Fs), Gs), NF))
u'3'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(cons(iff(A, B), Fs), Gs), NF) → u'4'1(reduce'ii'in(sequent(cons(x'2a(if(A, B), if(B, A)), Fs), Gs), NF))
u'4'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(cons(x'2a(F1, F2), Fs), Gs), NF) → u'5'1(reduce'ii'in(sequent(cons(F1, cons(F2, Fs)), Gs), NF))
u'5'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(cons(x'2b(F1, F2), Fs), Gs), NF) → u'6'1(reduce'ii'in(sequent(cons(F1, Fs), Gs), NF), F2, Fs, Gs, NF)
u'6'1(reduce'ii'out, F2, Fs, Gs, NF) → u'6'2(reduce'ii'in(sequent(cons(F2, Fs), Gs), NF))
u'6'2(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(cons(x'2d(F1), Fs), Gs), NF) → u'7'1(reduce'ii'in(sequent(Fs, cons(F1, Gs)), NF))
u'7'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(Fs, cons(if(A, B), Gs)), NF) → u'8'1(reduce'ii'in(sequent(Fs, cons(x'2b(x'2d(B), A), Gs)), NF))
u'8'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(Fs, cons(iff(A, B), Gs)), NF) → u'9'1(reduce'ii'in(sequent(Fs, cons(x'2a(if(A, B), if(B, A)), Gs)), NF))
u'9'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(cons(p(V), Fs), Gs), sequent(Left, Right)) → u'10'1(reduce'ii'in(sequent(Fs, Gs), sequent(cons(p(V), Left), Right)))
u'10'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(Fs, cons(x'2b(G1, G2), Gs)), NF) → u'11'1(reduce'ii'in(sequent(Fs, cons(G1, cons(G2, Gs))), NF))
u'11'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(Fs, cons(x'2a(G1, G2), Gs)), NF) → u'12'1(reduce'ii'in(sequent(Fs, cons(G1, Gs)), NF), Fs, G2, Gs, NF)
u'12'1(reduce'ii'out, Fs, G2, Gs, NF) → u'12'2(reduce'ii'in(sequent(Fs, cons(G2, Gs)), NF))
u'12'2(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(Fs, cons(x'2d(G1), Gs)), NF) → u'13'1(reduce'ii'in(sequent(cons(G1, Fs), Gs), NF))
u'13'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(nil, cons(p(V), Gs)), sequent(Left, Right)) → u'14'1(reduce'ii'in(sequent(nil, Gs), sequent(Left, cons(p(V), Right))))
u'14'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(nil, nil), sequent(F1, F2)) → u'15'1(intersect'ii'in(F1, F2))
u'15'1(intersect'ii'out) → reduce'ii'out
tautology'i'in(F) → u'16'1(reduce'ii'in(sequent(nil, cons(F, nil)), sequent(nil, nil)))
u'16'1(reduce'ii'out) → tautology'i'out

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

(17) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 2 less nodes.

(18) Obligation:

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

REDUCE'II'IN(sequent(Fs, cons(if(A, B), Gs)), NF) → REDUCE'II'IN(sequent(Fs, cons(x'2b(x'2d(B), A), Gs)), NF)
REDUCE'II'IN(sequent(cons(if(A, B), Fs), Gs), NF) → REDUCE'II'IN(sequent(cons(x'2b(x'2d(B), A), Fs), Gs), NF)

The TRS R consists of the following rules:

intersect'ii'in(cons(X, X0), cons(X, X1)) → intersect'ii'out
intersect'ii'in(Xs, cons(X0, Ys)) → u'1'1(intersect'ii'in(Xs, Ys))
u'1'1(intersect'ii'out) → intersect'ii'out
intersect'ii'in(cons(X0, Xs), Ys) → u'2'1(intersect'ii'in(Xs, Ys))
u'2'1(intersect'ii'out) → intersect'ii'out
reduce'ii'in(sequent(cons(if(A, B), Fs), Gs), NF) → u'3'1(reduce'ii'in(sequent(cons(x'2b(x'2d(B), A), Fs), Gs), NF))
u'3'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(cons(iff(A, B), Fs), Gs), NF) → u'4'1(reduce'ii'in(sequent(cons(x'2a(if(A, B), if(B, A)), Fs), Gs), NF))
u'4'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(cons(x'2a(F1, F2), Fs), Gs), NF) → u'5'1(reduce'ii'in(sequent(cons(F1, cons(F2, Fs)), Gs), NF))
u'5'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(cons(x'2b(F1, F2), Fs), Gs), NF) → u'6'1(reduce'ii'in(sequent(cons(F1, Fs), Gs), NF), F2, Fs, Gs, NF)
u'6'1(reduce'ii'out, F2, Fs, Gs, NF) → u'6'2(reduce'ii'in(sequent(cons(F2, Fs), Gs), NF))
u'6'2(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(cons(x'2d(F1), Fs), Gs), NF) → u'7'1(reduce'ii'in(sequent(Fs, cons(F1, Gs)), NF))
u'7'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(Fs, cons(if(A, B), Gs)), NF) → u'8'1(reduce'ii'in(sequent(Fs, cons(x'2b(x'2d(B), A), Gs)), NF))
u'8'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(Fs, cons(iff(A, B), Gs)), NF) → u'9'1(reduce'ii'in(sequent(Fs, cons(x'2a(if(A, B), if(B, A)), Gs)), NF))
u'9'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(cons(p(V), Fs), Gs), sequent(Left, Right)) → u'10'1(reduce'ii'in(sequent(Fs, Gs), sequent(cons(p(V), Left), Right)))
u'10'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(Fs, cons(x'2b(G1, G2), Gs)), NF) → u'11'1(reduce'ii'in(sequent(Fs, cons(G1, cons(G2, Gs))), NF))
u'11'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(Fs, cons(x'2a(G1, G2), Gs)), NF) → u'12'1(reduce'ii'in(sequent(Fs, cons(G1, Gs)), NF), Fs, G2, Gs, NF)
u'12'1(reduce'ii'out, Fs, G2, Gs, NF) → u'12'2(reduce'ii'in(sequent(Fs, cons(G2, Gs)), NF))
u'12'2(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(Fs, cons(x'2d(G1), Gs)), NF) → u'13'1(reduce'ii'in(sequent(cons(G1, Fs), Gs), NF))
u'13'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(nil, cons(p(V), Gs)), sequent(Left, Right)) → u'14'1(reduce'ii'in(sequent(nil, Gs), sequent(Left, cons(p(V), Right))))
u'14'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(nil, nil), sequent(F1, F2)) → u'15'1(intersect'ii'in(F1, F2))
u'15'1(intersect'ii'out) → reduce'ii'out
tautology'i'in(F) → u'16'1(reduce'ii'in(sequent(nil, cons(F, nil)), sequent(nil, nil)))
u'16'1(reduce'ii'out) → tautology'i'out

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

(19) UsableRulesProof (EQUIVALENT transformation)

(20) Obligation:

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

REDUCE'II'IN(sequent(Fs, cons(if(A, B), Gs)), NF) → REDUCE'II'IN(sequent(Fs, cons(x'2b(x'2d(B), A), Gs)), NF)
REDUCE'II'IN(sequent(cons(if(A, B), Fs), Gs), NF) → REDUCE'II'IN(sequent(cons(x'2b(x'2d(B), A), Fs), Gs), NF)

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

(21) 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:

REDUCE'II'IN(sequent(Fs, cons(if(A, B), Gs)), NF) → REDUCE'II'IN(sequent(Fs, cons(x'2b(x'2d(B), A), Gs)), NF)
REDUCE'II'IN(sequent(cons(if(A, B), Fs), Gs), NF) → REDUCE'II'IN(sequent(cons(x'2b(x'2d(B), A), Fs), Gs), NF)

No rules are removed from R.

Used ordering: POLO with Polynomial interpretation [POLO]:

POL(REDUCE'II'IN(x₁, x₂)) = x₁ + x₂
POL(cons(x₁, x₂)) = 2·x₁ + x₂
POL(if(x₁, x₂)) = x₁ + 2·x₂
POL(sequent(x₁, x₂)) = x₁ + x₂
POL(x'2b(x₁, x₂)) = x₁ + x₂
POL(x'2d(x₁)) = x₁

(22) Obligation:

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

(23) PisEmptyProof (EQUIVALENT transformation)

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

(0) Obligation:

(1) DependencyPairsProof (EQUIVALENT transformation)

(2) Obligation:

(3) DependencyGraphProof (EQUIVALENT transformation)

(4) Complex Obligation (AND)

(5) Obligation:

(6) UsableRulesProof (EQUIVALENT transformation)

(7) Obligation:

(8) QDPSizeChangeProof (EQUIVALENT transformation)

(9) YES

(10) Obligation:

(11) QDPOrderProof (EQUIVALENT transformation)

(12) Obligation:

(13) QDPOrderProof (EQUIVALENT transformation)

(14) Obligation:

(15) QDPOrderProof (EQUIVALENT transformation)

(16) Obligation:

(17) DependencyGraphProof (EQUIVALENT transformation)

(18) Obligation:

(19) UsableRulesProof (EQUIVALENT transformation)

(20) Obligation:

(21) UsableRulesReductionPairsProof (EQUIVALENT transformation)

(22) Obligation:

(23) PisEmptyProof (EQUIVALENT transformation)

(24) YES