Termination w.r.t. Q proof of /tmp/tmpAG6RL5/Ex5_Zan97

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

0 QTRS

↳1 DependencyPairsProof (⇔)

↳2 QDP

↳3 DependencyGraphProof (⇔)

↳4 AND

  ↳5 QDP

    ↳6 QDPOrderProof (⇔)

    ↳7 QDP

    ↳8 QDPOrderProof (⇔)

    ↳9 QDP

    ↳10 QDPOrderProof (⇔)

    ↳11 QDP

    ↳12 PisEmptyProof (⇔)

    ↳13 TRUE

  ↳14 QDP

    ↳15 QDPOrderProof (⇔)

    ↳16 QDP

    ↳17 QDPOrderProof (⇔)

    ↳18 QDP

    ↳19 PisEmptyProof (⇔)

    ↳20 TRUE

  ↳21 QDP

    ↳22 QDPOrderProof (⇔)

    ↳23 QDP

    ↳24 QDPOrderProof (⇔)

    ↳25 QDP

    ↳26 PisEmptyProof (⇔)

    ↳27 TRUE

  ↳28 QDP

    ↳29 QDPOrderProof (⇔)

    ↳30 QDP

    ↳31 PisEmptyProof (⇔)

    ↳32 TRUE

  ↳33 QDP

(0) Obligation:

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

active(f(X)) → mark(if(X, c, f(true)))
active(if(true, X, Y)) → mark(X)
active(if(false, X, Y)) → mark(Y)
active(f(X)) → f(active(X))
active(if(X1, X2, X3)) → if(active(X1), X2, X3)
active(if(X1, X2, X3)) → if(X1, active(X2), X3)
f(mark(X)) → mark(f(X))
if(mark(X1), X2, X3) → mark(if(X1, X2, X3))
if(X1, mark(X2), X3) → mark(if(X1, X2, X3))
proper(f(X)) → f(proper(X))
proper(if(X1, X2, X3)) → if(proper(X1), proper(X2), proper(X3))
proper(c) → ok(c)
proper(true) → ok(true)
proper(false) → ok(false)
f(ok(X)) → ok(f(X))
if(ok(X1), ok(X2), ok(X3)) → ok(if(X1, X2, X3))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))

Q is empty.

(1) DependencyPairsProof (EQUIVALENT transformation)

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

(2) Obligation:

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

ACTIVE(f(X)) → IF(X, c, f(true))
ACTIVE(f(X)) → F(true)
ACTIVE(f(X)) → F(active(X))
ACTIVE(f(X)) → ACTIVE(X)
ACTIVE(if(X1, X2, X3)) → IF(active(X1), X2, X3)
ACTIVE(if(X1, X2, X3)) → ACTIVE(X1)
ACTIVE(if(X1, X2, X3)) → IF(X1, active(X2), X3)
ACTIVE(if(X1, X2, X3)) → ACTIVE(X2)
F(mark(X)) → F(X)
IF(mark(X1), X2, X3) → IF(X1, X2, X3)
IF(X1, mark(X2), X3) → IF(X1, X2, X3)
PROPER(f(X)) → F(proper(X))
PROPER(f(X)) → PROPER(X)
PROPER(if(X1, X2, X3)) → IF(proper(X1), proper(X2), proper(X3))
PROPER(if(X1, X2, X3)) → PROPER(X1)
PROPER(if(X1, X2, X3)) → PROPER(X2)
PROPER(if(X1, X2, X3)) → PROPER(X3)
F(ok(X)) → F(X)
IF(ok(X1), ok(X2), ok(X3)) → IF(X1, X2, X3)
TOP(mark(X)) → TOP(proper(X))
TOP(mark(X)) → PROPER(X)
TOP(ok(X)) → TOP(active(X))
TOP(ok(X)) → ACTIVE(X)

The TRS R consists of the following rules:

active(f(X)) → mark(if(X, c, f(true)))
active(if(true, X, Y)) → mark(X)
active(if(false, X, Y)) → mark(Y)
active(f(X)) → f(active(X))
active(if(X1, X2, X3)) → if(active(X1), X2, X3)
active(if(X1, X2, X3)) → if(X1, active(X2), X3)
f(mark(X)) → mark(f(X))
if(mark(X1), X2, X3) → mark(if(X1, X2, X3))
if(X1, mark(X2), X3) → mark(if(X1, X2, X3))
proper(f(X)) → f(proper(X))
proper(if(X1, X2, X3)) → if(proper(X1), proper(X2), proper(X3))
proper(c) → ok(c)
proper(true) → ok(true)
proper(false) → ok(false)
f(ok(X)) → ok(f(X))
if(ok(X1), ok(X2), ok(X3)) → ok(if(X1, X2, X3))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))

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

(3) DependencyGraphProof (EQUIVALENT transformation)

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

(4) Complex Obligation (AND)

(5) Obligation:

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

IF(X1, mark(X2), X3) → IF(X1, X2, X3)
IF(mark(X1), X2, X3) → IF(X1, X2, X3)
IF(ok(X1), ok(X2), ok(X3)) → IF(X1, X2, X3)

The TRS R consists of the following rules:

active(f(X)) → mark(if(X, c, f(true)))
active(if(true, X, Y)) → mark(X)
active(if(false, X, Y)) → mark(Y)
active(f(X)) → f(active(X))
active(if(X1, X2, X3)) → if(active(X1), X2, X3)
active(if(X1, X2, X3)) → if(X1, active(X2), X3)
f(mark(X)) → mark(f(X))
if(mark(X1), X2, X3) → mark(if(X1, X2, X3))
if(X1, mark(X2), X3) → mark(if(X1, X2, X3))
proper(f(X)) → f(proper(X))
proper(if(X1, X2, X3)) → if(proper(X1), proper(X2), proper(X3))
proper(c) → ok(c)
proper(true) → ok(true)
proper(false) → ok(false)
f(ok(X)) → ok(f(X))
if(ok(X1), ok(X2), ok(X3)) → ok(if(X1, X2, X3))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))

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

(6) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

IF(X1, mark(X2), X3) → IF(X1, X2, X3)

The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
IF(x1, x2, x3) = IF(x2, x3)
mark(x1) = mark(x1)
ok(x1) = x1
active(x1) = active(x1)
f(x1) = x1
if(x1, x2, x3) = if(x1, x2, x3)
c = c
true = true
false = false
proper(x1) = proper(x1)
top(x1) = top

Lexicographic path order with status [LPO].
Quasi-Precedence:

active₁ > [if₃, proper₁] > c
active₁ > [if₃, proper₁] > false > mark₁
active₁ > true > mark₁

Status:

IF₂: [1,2]
mark₁: [1]
active₁: [1]
if₃: [2,1,3]
c: []
true: []
false: []
proper₁: [1]
top: []

The following usable rules [FROCOS05] were oriented:

active(f(X)) → mark(if(X, c, f(true)))
active(if(true, X, Y)) → mark(X)
active(if(false, X, Y)) → mark(Y)
active(f(X)) → f(active(X))
active(if(X1, X2, X3)) → if(active(X1), X2, X3)
active(if(X1, X2, X3)) → if(X1, active(X2), X3)
f(mark(X)) → mark(f(X))
if(mark(X1), X2, X3) → mark(if(X1, X2, X3))
if(X1, mark(X2), X3) → mark(if(X1, X2, X3))
proper(f(X)) → f(proper(X))
proper(if(X1, X2, X3)) → if(proper(X1), proper(X2), proper(X3))
proper(c) → ok(c)
proper(true) → ok(true)
proper(false) → ok(false)
f(ok(X)) → ok(f(X))
if(ok(X1), ok(X2), ok(X3)) → ok(if(X1, X2, X3))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))

(7) Obligation:

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

IF(mark(X1), X2, X3) → IF(X1, X2, X3)
IF(ok(X1), ok(X2), ok(X3)) → IF(X1, X2, X3)

The TRS R consists of the following rules:

active(f(X)) → mark(if(X, c, f(true)))
active(if(true, X, Y)) → mark(X)
active(if(false, X, Y)) → mark(Y)
active(f(X)) → f(active(X))
active(if(X1, X2, X3)) → if(active(X1), X2, X3)
active(if(X1, X2, X3)) → if(X1, active(X2), X3)
f(mark(X)) → mark(f(X))
if(mark(X1), X2, X3) → mark(if(X1, X2, X3))
if(X1, mark(X2), X3) → mark(if(X1, X2, X3))
proper(f(X)) → f(proper(X))
proper(if(X1, X2, X3)) → if(proper(X1), proper(X2), proper(X3))
proper(c) → ok(c)
proper(true) → ok(true)
proper(false) → ok(false)
f(ok(X)) → ok(f(X))
if(ok(X1), ok(X2), ok(X3)) → ok(if(X1, X2, X3))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))

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

(8) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

IF(ok(X1), ok(X2), ok(X3)) → IF(X1, X2, X3)

The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
IF(x1, x2, x3) = x2
mark(x1) = mark
ok(x1) = ok(x1)
active(x1) = x1
f(x1) = f(x1)
if(x1, x2, x3) = if(x2)
c = c
true = true
false = false
proper(x1) = proper(x1)
top(x1) = top

Lexicographic path order with status [LPO].
Quasi-Precedence:

proper₁ > f₁ > c > [ok₁, if₁] > [mark, true, top]
proper₁ > false > [mark, true, top]

Status:

mark: []
ok₁: [1]
f₁: [1]
if₁: [1]
c: []
true: []
false: []
proper₁: [1]
top: []

The following usable rules [FROCOS05] were oriented:

active(f(X)) → mark(if(X, c, f(true)))
active(if(true, X, Y)) → mark(X)
active(if(false, X, Y)) → mark(Y)
active(f(X)) → f(active(X))
active(if(X1, X2, X3)) → if(active(X1), X2, X3)
active(if(X1, X2, X3)) → if(X1, active(X2), X3)
f(mark(X)) → mark(f(X))
if(mark(X1), X2, X3) → mark(if(X1, X2, X3))
if(X1, mark(X2), X3) → mark(if(X1, X2, X3))
proper(f(X)) → f(proper(X))
proper(if(X1, X2, X3)) → if(proper(X1), proper(X2), proper(X3))
proper(c) → ok(c)
proper(true) → ok(true)
proper(false) → ok(false)
f(ok(X)) → ok(f(X))
if(ok(X1), ok(X2), ok(X3)) → ok(if(X1, X2, X3))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))

(9) Obligation:

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

IF(mark(X1), X2, X3) → IF(X1, X2, X3)

The TRS R consists of the following rules:

active(f(X)) → mark(if(X, c, f(true)))
active(if(true, X, Y)) → mark(X)
active(if(false, X, Y)) → mark(Y)
active(f(X)) → f(active(X))
active(if(X1, X2, X3)) → if(active(X1), X2, X3)
active(if(X1, X2, X3)) → if(X1, active(X2), X3)
f(mark(X)) → mark(f(X))
if(mark(X1), X2, X3) → mark(if(X1, X2, X3))
if(X1, mark(X2), X3) → mark(if(X1, X2, X3))
proper(f(X)) → f(proper(X))
proper(if(X1, X2, X3)) → if(proper(X1), proper(X2), proper(X3))
proper(c) → ok(c)
proper(true) → ok(true)
proper(false) → ok(false)
f(ok(X)) → ok(f(X))
if(ok(X1), ok(X2), ok(X3)) → ok(if(X1, X2, X3))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))

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

(10) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

IF(mark(X1), X2, X3) → IF(X1, X2, X3)

The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
IF(x1, x2, x3) = IF(x1, x2, x3)
mark(x1) = mark(x1)
active(x1) = active(x1)
f(x1) = x1
if(x1, x2, x3) = if(x1, x2, x3)
c = c
true = true
false = false
proper(x1) = proper(x1)
ok(x1) = ok
top(x1) = top

Lexicographic path order with status [LPO].
Quasi-Precedence:

active₁ > [if₃, c, ok] > [IF₃, mark₁] > top
active₁ > true
false > [if₃, c, ok] > [IF₃, mark₁] > top
proper₁ > [if₃, c, ok] > [IF₃, mark₁] > top
proper₁ > true

Status:

IF₃: [1,2,3]
mark₁: [1]
active₁: [1]
if₃: [2,1,3]
c: []
true: []
false: []
proper₁: [1]
ok: []
top: []

The following usable rules [FROCOS05] were oriented:

active(f(X)) → mark(if(X, c, f(true)))
active(if(true, X, Y)) → mark(X)
active(if(false, X, Y)) → mark(Y)
active(f(X)) → f(active(X))
active(if(X1, X2, X3)) → if(active(X1), X2, X3)
active(if(X1, X2, X3)) → if(X1, active(X2), X3)
f(mark(X)) → mark(f(X))
if(mark(X1), X2, X3) → mark(if(X1, X2, X3))
if(X1, mark(X2), X3) → mark(if(X1, X2, X3))
proper(f(X)) → f(proper(X))
proper(if(X1, X2, X3)) → if(proper(X1), proper(X2), proper(X3))
proper(c) → ok(c)
proper(true) → ok(true)
proper(false) → ok(false)
f(ok(X)) → ok(f(X))
if(ok(X1), ok(X2), ok(X3)) → ok(if(X1, X2, X3))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))

(11) Obligation:

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

active(f(X)) → mark(if(X, c, f(true)))
active(if(true, X, Y)) → mark(X)
active(if(false, X, Y)) → mark(Y)
active(f(X)) → f(active(X))
active(if(X1, X2, X3)) → if(active(X1), X2, X3)
active(if(X1, X2, X3)) → if(X1, active(X2), X3)
f(mark(X)) → mark(f(X))
if(mark(X1), X2, X3) → mark(if(X1, X2, X3))
if(X1, mark(X2), X3) → mark(if(X1, X2, X3))
proper(f(X)) → f(proper(X))
proper(if(X1, X2, X3)) → if(proper(X1), proper(X2), proper(X3))
proper(c) → ok(c)
proper(true) → ok(true)
proper(false) → ok(false)
f(ok(X)) → ok(f(X))
if(ok(X1), ok(X2), ok(X3)) → ok(if(X1, X2, X3))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))

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

(12) PisEmptyProof (EQUIVALENT transformation)

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

(13) TRUE

(14) Obligation:

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

F(ok(X)) → F(X)
F(mark(X)) → F(X)

The TRS R consists of the following rules:

active(f(X)) → mark(if(X, c, f(true)))
active(if(true, X, Y)) → mark(X)
active(if(false, X, Y)) → mark(Y)
active(f(X)) → f(active(X))
active(if(X1, X2, X3)) → if(active(X1), X2, X3)
active(if(X1, X2, X3)) → if(X1, active(X2), X3)
f(mark(X)) → mark(f(X))
if(mark(X1), X2, X3) → mark(if(X1, X2, X3))
if(X1, mark(X2), X3) → mark(if(X1, X2, X3))
proper(f(X)) → f(proper(X))
proper(if(X1, X2, X3)) → if(proper(X1), proper(X2), proper(X3))
proper(c) → ok(c)
proper(true) → ok(true)
proper(false) → ok(false)
f(ok(X)) → ok(f(X))
if(ok(X1), ok(X2), ok(X3)) → ok(if(X1, X2, X3))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))

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

(15) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

F(ok(X)) → F(X)

The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
F(x1) = F(x1)
ok(x1) = ok(x1)
mark(x1) = x1
active(x1) = active(x1)
f(x1) = f(x1)
if(x1, x2, x3) = if(x1, x2, x3)
c = c
true = true
false = false
proper(x1) = proper(x1)
top(x1) = top

Lexicographic path order with status [LPO].
Quasi-Precedence:

[active₁, if₃, proper₁] > true > [ok₁, f₁, c]
[active₁, if₃, proper₁] > false > [ok₁, f₁, c]

Status:

F₁: [1]
ok₁: [1]
active₁: [1]
f₁: [1]
if₃: [2,1,3]
c: []
true: []
false: []
proper₁: [1]
top: []

The following usable rules [FROCOS05] were oriented:

active(f(X)) → mark(if(X, c, f(true)))
active(if(true, X, Y)) → mark(X)
active(if(false, X, Y)) → mark(Y)
active(f(X)) → f(active(X))
active(if(X1, X2, X3)) → if(active(X1), X2, X3)
active(if(X1, X2, X3)) → if(X1, active(X2), X3)
f(mark(X)) → mark(f(X))
if(mark(X1), X2, X3) → mark(if(X1, X2, X3))
if(X1, mark(X2), X3) → mark(if(X1, X2, X3))
proper(f(X)) → f(proper(X))
proper(if(X1, X2, X3)) → if(proper(X1), proper(X2), proper(X3))
proper(c) → ok(c)
proper(true) → ok(true)
proper(false) → ok(false)
f(ok(X)) → ok(f(X))
if(ok(X1), ok(X2), ok(X3)) → ok(if(X1, X2, X3))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))

(16) Obligation:

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

F(mark(X)) → F(X)

The TRS R consists of the following rules:

active(f(X)) → mark(if(X, c, f(true)))
active(if(true, X, Y)) → mark(X)
active(if(false, X, Y)) → mark(Y)
active(f(X)) → f(active(X))
active(if(X1, X2, X3)) → if(active(X1), X2, X3)
active(if(X1, X2, X3)) → if(X1, active(X2), X3)
f(mark(X)) → mark(f(X))
if(mark(X1), X2, X3) → mark(if(X1, X2, X3))
if(X1, mark(X2), X3) → mark(if(X1, X2, X3))
proper(f(X)) → f(proper(X))
proper(if(X1, X2, X3)) → if(proper(X1), proper(X2), proper(X3))
proper(c) → ok(c)
proper(true) → ok(true)
proper(false) → ok(false)
f(ok(X)) → ok(f(X))
if(ok(X1), ok(X2), ok(X3)) → ok(if(X1, X2, X3))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))

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

(17) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

F(mark(X)) → F(X)

The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
F(x1) = x1
mark(x1) = mark(x1)
active(x1) = active(x1)
f(x1) = f(x1)
if(x1, x2, x3) = if(x1, x2, x3)
c = c
true = true
false = false
proper(x1) = proper(x1)
ok(x1) = ok
top(x1) = top

Lexicographic path order with status [LPO].
Quasi-Precedence:

proper₁ > [ok, top] > [active₁, if₃, c] > f₁ > [mark₁, true, false]

Status:

mark₁: [1]
active₁: [1]
f₁: [1]
if₃: [1,3,2]
c: []
true: []
false: []
proper₁: [1]
ok: []
top: []

The following usable rules [FROCOS05] were oriented:

active(f(X)) → mark(if(X, c, f(true)))
active(if(true, X, Y)) → mark(X)
active(if(false, X, Y)) → mark(Y)
active(f(X)) → f(active(X))
active(if(X1, X2, X3)) → if(active(X1), X2, X3)
active(if(X1, X2, X3)) → if(X1, active(X2), X3)
f(mark(X)) → mark(f(X))
if(mark(X1), X2, X3) → mark(if(X1, X2, X3))
if(X1, mark(X2), X3) → mark(if(X1, X2, X3))
proper(f(X)) → f(proper(X))
proper(if(X1, X2, X3)) → if(proper(X1), proper(X2), proper(X3))
proper(c) → ok(c)
proper(true) → ok(true)
proper(false) → ok(false)
f(ok(X)) → ok(f(X))
if(ok(X1), ok(X2), ok(X3)) → ok(if(X1, X2, X3))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))

(18) Obligation:

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

active(f(X)) → mark(if(X, c, f(true)))
active(if(true, X, Y)) → mark(X)
active(if(false, X, Y)) → mark(Y)
active(f(X)) → f(active(X))
active(if(X1, X2, X3)) → if(active(X1), X2, X3)
active(if(X1, X2, X3)) → if(X1, active(X2), X3)
f(mark(X)) → mark(f(X))
if(mark(X1), X2, X3) → mark(if(X1, X2, X3))
if(X1, mark(X2), X3) → mark(if(X1, X2, X3))
proper(f(X)) → f(proper(X))
proper(if(X1, X2, X3)) → if(proper(X1), proper(X2), proper(X3))
proper(c) → ok(c)
proper(true) → ok(true)
proper(false) → ok(false)
f(ok(X)) → ok(f(X))
if(ok(X1), ok(X2), ok(X3)) → ok(if(X1, X2, X3))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))

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

(19) PisEmptyProof (EQUIVALENT transformation)

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

(20) TRUE

(21) Obligation:

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

PROPER(if(X1, X2, X3)) → PROPER(X1)
PROPER(f(X)) → PROPER(X)
PROPER(if(X1, X2, X3)) → PROPER(X2)
PROPER(if(X1, X2, X3)) → PROPER(X3)

The TRS R consists of the following rules:

active(f(X)) → mark(if(X, c, f(true)))
active(if(true, X, Y)) → mark(X)
active(if(false, X, Y)) → mark(Y)
active(f(X)) → f(active(X))
active(if(X1, X2, X3)) → if(active(X1), X2, X3)
active(if(X1, X2, X3)) → if(X1, active(X2), X3)
f(mark(X)) → mark(f(X))
if(mark(X1), X2, X3) → mark(if(X1, X2, X3))
if(X1, mark(X2), X3) → mark(if(X1, X2, X3))
proper(f(X)) → f(proper(X))
proper(if(X1, X2, X3)) → if(proper(X1), proper(X2), proper(X3))
proper(c) → ok(c)
proper(true) → ok(true)
proper(false) → ok(false)
f(ok(X)) → ok(f(X))
if(ok(X1), ok(X2), ok(X3)) → ok(if(X1, X2, X3))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))

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

(22) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

PROPER(if(X1, X2, X3)) → PROPER(X1)
PROPER(if(X1, X2, X3)) → PROPER(X2)
PROPER(if(X1, X2, X3)) → PROPER(X3)

The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
PROPER(x1) = x1
if(x1, x2, x3) = if(x1, x2, x3)
f(x1) = x1
active(x1) = active(x1)
mark(x1) = x1
c = c
true = true
false = false
proper(x1) = proper(x1)
ok(x1) = ok
top(x1) = top

Lexicographic path order with status [LPO].
Quasi-Precedence:

[active₁, c] > true > ok > if₃
[active₁, c] > true > ok > top
proper₁ > true > ok > if₃
proper₁ > true > ok > top
proper₁ > false > ok > if₃
proper₁ > false > ok > top

Status:

if₃: [1,3,2]
active₁: [1]
c: []
true: []
false: []
proper₁: [1]
ok: []
top: []

The following usable rules [FROCOS05] were oriented:

active(f(X)) → mark(if(X, c, f(true)))
active(if(true, X, Y)) → mark(X)
active(if(false, X, Y)) → mark(Y)
active(f(X)) → f(active(X))
active(if(X1, X2, X3)) → if(active(X1), X2, X3)
active(if(X1, X2, X3)) → if(X1, active(X2), X3)
f(mark(X)) → mark(f(X))
if(mark(X1), X2, X3) → mark(if(X1, X2, X3))
if(X1, mark(X2), X3) → mark(if(X1, X2, X3))
proper(f(X)) → f(proper(X))
proper(if(X1, X2, X3)) → if(proper(X1), proper(X2), proper(X3))
proper(c) → ok(c)
proper(true) → ok(true)
proper(false) → ok(false)
f(ok(X)) → ok(f(X))
if(ok(X1), ok(X2), ok(X3)) → ok(if(X1, X2, X3))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))

(23) Obligation:

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

PROPER(f(X)) → PROPER(X)

The TRS R consists of the following rules:

active(f(X)) → mark(if(X, c, f(true)))
active(if(true, X, Y)) → mark(X)
active(if(false, X, Y)) → mark(Y)
active(f(X)) → f(active(X))
active(if(X1, X2, X3)) → if(active(X1), X2, X3)
active(if(X1, X2, X3)) → if(X1, active(X2), X3)
f(mark(X)) → mark(f(X))
if(mark(X1), X2, X3) → mark(if(X1, X2, X3))
if(X1, mark(X2), X3) → mark(if(X1, X2, X3))
proper(f(X)) → f(proper(X))
proper(if(X1, X2, X3)) → if(proper(X1), proper(X2), proper(X3))
proper(c) → ok(c)
proper(true) → ok(true)
proper(false) → ok(false)
f(ok(X)) → ok(f(X))
if(ok(X1), ok(X2), ok(X3)) → ok(if(X1, X2, X3))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))

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

(24) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

PROPER(f(X)) → PROPER(X)

The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
PROPER(x1) = PROPER(x1)
f(x1) = f(x1)
active(x1) = active(x1)
mark(x1) = mark
if(x1, x2, x3) = x2
c = c
true = true
false = false
proper(x1) = proper(x1)
ok(x1) = ok
top(x1) = top

Lexicographic path order with status [LPO].
Quasi-Precedence:

PROPER₁ > mark
proper₁ > [f₁, active₁, c] > [true, ok, top] > mark
proper₁ > false > [true, ok, top] > mark

Status:

PROPER₁: [1]
f₁: [1]
active₁: [1]
mark: []
c: []
true: []
false: []
proper₁: [1]
ok: []
top: []

The following usable rules [FROCOS05] were oriented:

active(f(X)) → mark(if(X, c, f(true)))
active(if(true, X, Y)) → mark(X)
active(if(false, X, Y)) → mark(Y)
active(f(X)) → f(active(X))
active(if(X1, X2, X3)) → if(active(X1), X2, X3)
active(if(X1, X2, X3)) → if(X1, active(X2), X3)
f(mark(X)) → mark(f(X))
if(mark(X1), X2, X3) → mark(if(X1, X2, X3))
if(X1, mark(X2), X3) → mark(if(X1, X2, X3))
proper(f(X)) → f(proper(X))
proper(if(X1, X2, X3)) → if(proper(X1), proper(X2), proper(X3))
proper(c) → ok(c)
proper(true) → ok(true)
proper(false) → ok(false)
f(ok(X)) → ok(f(X))
if(ok(X1), ok(X2), ok(X3)) → ok(if(X1, X2, X3))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))

(25) Obligation:

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

active(f(X)) → mark(if(X, c, f(true)))
active(if(true, X, Y)) → mark(X)
active(if(false, X, Y)) → mark(Y)
active(f(X)) → f(active(X))
active(if(X1, X2, X3)) → if(active(X1), X2, X3)
active(if(X1, X2, X3)) → if(X1, active(X2), X3)
f(mark(X)) → mark(f(X))
if(mark(X1), X2, X3) → mark(if(X1, X2, X3))
if(X1, mark(X2), X3) → mark(if(X1, X2, X3))
proper(f(X)) → f(proper(X))
proper(if(X1, X2, X3)) → if(proper(X1), proper(X2), proper(X3))
proper(c) → ok(c)
proper(true) → ok(true)
proper(false) → ok(false)
f(ok(X)) → ok(f(X))
if(ok(X1), ok(X2), ok(X3)) → ok(if(X1, X2, X3))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))

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

(26) PisEmptyProof (EQUIVALENT transformation)

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

(27) TRUE

(28) Obligation:

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

ACTIVE(if(X1, X2, X3)) → ACTIVE(X1)
ACTIVE(f(X)) → ACTIVE(X)
ACTIVE(if(X1, X2, X3)) → ACTIVE(X2)

The TRS R consists of the following rules:

active(f(X)) → mark(if(X, c, f(true)))
active(if(true, X, Y)) → mark(X)
active(if(false, X, Y)) → mark(Y)
active(f(X)) → f(active(X))
active(if(X1, X2, X3)) → if(active(X1), X2, X3)
active(if(X1, X2, X3)) → if(X1, active(X2), X3)
f(mark(X)) → mark(f(X))
if(mark(X1), X2, X3) → mark(if(X1, X2, X3))
if(X1, mark(X2), X3) → mark(if(X1, X2, X3))
proper(f(X)) → f(proper(X))
proper(if(X1, X2, X3)) → if(proper(X1), proper(X2), proper(X3))
proper(c) → ok(c)
proper(true) → ok(true)
proper(false) → ok(false)
f(ok(X)) → ok(f(X))
if(ok(X1), ok(X2), ok(X3)) → ok(if(X1, X2, X3))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))

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

(29) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

ACTIVE(if(X1, X2, X3)) → ACTIVE(X1)
ACTIVE(f(X)) → ACTIVE(X)
ACTIVE(if(X1, X2, X3)) → ACTIVE(X2)

The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
ACTIVE(x1) = ACTIVE(x1)
if(x1, x2, x3) = if(x1, x2)
f(x1) = f(x1)
active(x1) = x1
mark(x1) = mark
c = c
true = true
false = false
proper(x1) = proper(x1)
ok(x1) = ok
top(x1) = top

Lexicographic path order with status [LPO].
Quasi-Precedence:

[ACTIVE₁, if₂, c, proper₁, ok] > f₁ > mark > top
[ACTIVE₁, if₂, c, proper₁, ok] > true > mark > top
[ACTIVE₁, if₂, c, proper₁, ok] > false > top

Status:

ACTIVE₁: [1]
if₂: [1,2]
f₁: [1]
mark: []
c: []
true: []
false: []
proper₁: [1]
ok: []
top: []

The following usable rules [FROCOS05] were oriented:

active(f(X)) → mark(if(X, c, f(true)))
active(if(true, X, Y)) → mark(X)
active(if(false, X, Y)) → mark(Y)
active(f(X)) → f(active(X))
active(if(X1, X2, X3)) → if(active(X1), X2, X3)
active(if(X1, X2, X3)) → if(X1, active(X2), X3)
f(mark(X)) → mark(f(X))
if(mark(X1), X2, X3) → mark(if(X1, X2, X3))
if(X1, mark(X2), X3) → mark(if(X1, X2, X3))
proper(f(X)) → f(proper(X))
proper(if(X1, X2, X3)) → if(proper(X1), proper(X2), proper(X3))
proper(c) → ok(c)
proper(true) → ok(true)
proper(false) → ok(false)
f(ok(X)) → ok(f(X))
if(ok(X1), ok(X2), ok(X3)) → ok(if(X1, X2, X3))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))

(30) Obligation:

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

active(f(X)) → mark(if(X, c, f(true)))
active(if(true, X, Y)) → mark(X)
active(if(false, X, Y)) → mark(Y)
active(f(X)) → f(active(X))
active(if(X1, X2, X3)) → if(active(X1), X2, X3)
active(if(X1, X2, X3)) → if(X1, active(X2), X3)
f(mark(X)) → mark(f(X))
if(mark(X1), X2, X3) → mark(if(X1, X2, X3))
if(X1, mark(X2), X3) → mark(if(X1, X2, X3))
proper(f(X)) → f(proper(X))
proper(if(X1, X2, X3)) → if(proper(X1), proper(X2), proper(X3))
proper(c) → ok(c)
proper(true) → ok(true)
proper(false) → ok(false)
f(ok(X)) → ok(f(X))
if(ok(X1), ok(X2), ok(X3)) → ok(if(X1, X2, X3))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))

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

(31) PisEmptyProof (EQUIVALENT transformation)

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

(32) TRUE

(33) Obligation:

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

TOP(ok(X)) → TOP(active(X))
TOP(mark(X)) → TOP(proper(X))

The TRS R consists of the following rules:

active(f(X)) → mark(if(X, c, f(true)))
active(if(true, X, Y)) → mark(X)
active(if(false, X, Y)) → mark(Y)
active(f(X)) → f(active(X))
active(if(X1, X2, X3)) → if(active(X1), X2, X3)
active(if(X1, X2, X3)) → if(X1, active(X2), X3)
f(mark(X)) → mark(f(X))
if(mark(X1), X2, X3) → mark(if(X1, X2, X3))
if(X1, mark(X2), X3) → mark(if(X1, X2, X3))
proper(f(X)) → f(proper(X))
proper(if(X1, X2, X3)) → if(proper(X1), proper(X2), proper(X3))
proper(c) → ok(c)
proper(true) → ok(true)
proper(false) → ok(false)
f(ok(X)) → ok(f(X))
if(ok(X1), ok(X2), ok(X3)) → ok(if(X1, X2, X3))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))

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