NO Termination w.r.t. Q proof of Applicative_05_Ex2_8_1ConstSubstFix.ari

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

0 QTRS
↳1 Overlay + Local Confluence (⇔, 0 ms)
↳2 QTRS
↳3 DependencyPairsProof (⇔, 10 ms)
↳4 QDP
↳5 TransformationProof (⇔, 0 ms)
↳6 QDP
↳7 TransformationProof (⇔, 0 ms)
↳8 QDP
↳9 TransformationProof (⇔, 0 ms)
↳10 QDP
↳11 MNOCProof (⇔, 0 ms)
↳12 QDP
↳13 NonTerminationLoopProof (⇒, 0 ms)
↳14 NO

(0) Obligation:

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

app(app(const, x), y) → x
app(app(app(subst, f), g), x) → app(app(f, x), app(g, x))
app(app(fix, f), x) → app(app(f, app(fix, f)), x)

Q is empty.

(1) Overlay + Local Confluence (EQUIVALENT transformation)

The TRS is overlay and locally confluent. By [NOC] we can switch to innermost.

(2) Obligation:

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

app(app(const, x), y) → x
app(app(app(subst, f), g), x) → app(app(f, x), app(g, x))
app(app(fix, f), x) → app(app(f, app(fix, f)), x)

The set Q consists of the following terms:

app(app(const, x0), x1)
app(app(app(subst, x0), x1), x2)
app(app(fix, x0), x1)

(3) DependencyPairsProof (EQUIVALENT transformation)

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

(4) Obligation:

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

APP(app(app(subst, f), g), x) → APP(app(f, x), app(g, x))
APP(app(app(subst, f), g), x) → APP(f, x)
APP(app(app(subst, f), g), x) → APP(g, x)
APP(app(fix, f), x) → APP(app(f, app(fix, f)), x)
APP(app(fix, f), x) → APP(f, app(fix, f))

The TRS R consists of the following rules:

app(app(const, x), y) → x
app(app(app(subst, f), g), x) → app(app(f, x), app(g, x))
app(app(fix, f), x) → app(app(f, app(fix, f)), x)

The set Q consists of the following terms:

app(app(const, x0), x1)
app(app(app(subst, x0), x1), x2)
app(app(fix, x0), x1)

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

(5) TransformationProof (EQUIVALENT transformation)

By forward instantiating [JAR06] the rule APP(app(app(subst, f), g), x) → APP(f, x) we obtained the following new rules [LPAR04]:

APP(app(app(subst, app(app(subst, y_0), y_1)), x1), x2) → APP(app(app(subst, y_0), y_1), x2) → APP(app(app(subst, app(app(subst, y_0), y_1)), x1), x2) → APP(app(app(subst, y_0), y_1), x2)
APP(app(app(subst, app(fix, y_0)), x1), x2) → APP(app(fix, y_0), x2) → APP(app(app(subst, app(fix, y_0)), x1), x2) → APP(app(fix, y_0), x2)

(6) Obligation:

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

APP(app(app(subst, f), g), x) → APP(app(f, x), app(g, x))
APP(app(app(subst, f), g), x) → APP(g, x)
APP(app(fix, f), x) → APP(app(f, app(fix, f)), x)
APP(app(fix, f), x) → APP(f, app(fix, f))
APP(app(app(subst, app(app(subst, y_0), y_1)), x1), x2) → APP(app(app(subst, y_0), y_1), x2)
APP(app(app(subst, app(fix, y_0)), x1), x2) → APP(app(fix, y_0), x2)

The TRS R consists of the following rules:

app(app(const, x), y) → x
app(app(app(subst, f), g), x) → app(app(f, x), app(g, x))
app(app(fix, f), x) → app(app(f, app(fix, f)), x)

The set Q consists of the following terms:

app(app(const, x0), x1)
app(app(app(subst, x0), x1), x2)
app(app(fix, x0), x1)

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

(7) TransformationProof (EQUIVALENT transformation)

By forward instantiating [JAR06] the rule APP(app(app(subst, f), g), x) → APP(g, x) we obtained the following new rules [LPAR04]:

APP(app(app(subst, x0), app(app(subst, y_0), y_1)), x2) → APP(app(app(subst, y_0), y_1), x2) → APP(app(app(subst, x0), app(app(subst, y_0), y_1)), x2) → APP(app(app(subst, y_0), y_1), x2)
APP(app(app(subst, x0), app(fix, y_0)), x2) → APP(app(fix, y_0), x2) → APP(app(app(subst, x0), app(fix, y_0)), x2) → APP(app(fix, y_0), x2)
APP(app(app(subst, x0), app(app(subst, app(app(subst, y_0), y_1)), y_2)), x2) → APP(app(app(subst, app(app(subst, y_0), y_1)), y_2), x2) → APP(app(app(subst, x0), app(app(subst, app(app(subst, y_0), y_1)), y_2)), x2) → APP(app(app(subst, app(app(subst, y_0), y_1)), y_2), x2)
APP(app(app(subst, x0), app(app(subst, app(fix, y_0)), y_1)), x2) → APP(app(app(subst, app(fix, y_0)), y_1), x2) → APP(app(app(subst, x0), app(app(subst, app(fix, y_0)), y_1)), x2) → APP(app(app(subst, app(fix, y_0)), y_1), x2)

(8) Obligation:

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

APP(app(app(subst, f), g), x) → APP(app(f, x), app(g, x))
APP(app(fix, f), x) → APP(app(f, app(fix, f)), x)
APP(app(fix, f), x) → APP(f, app(fix, f))
APP(app(app(subst, app(app(subst, y_0), y_1)), x1), x2) → APP(app(app(subst, y_0), y_1), x2)
APP(app(app(subst, app(fix, y_0)), x1), x2) → APP(app(fix, y_0), x2)
APP(app(app(subst, x0), app(app(subst, y_0), y_1)), x2) → APP(app(app(subst, y_0), y_1), x2)
APP(app(app(subst, x0), app(fix, y_0)), x2) → APP(app(fix, y_0), x2)
APP(app(app(subst, x0), app(app(subst, app(app(subst, y_0), y_1)), y_2)), x2) → APP(app(app(subst, app(app(subst, y_0), y_1)), y_2), x2)
APP(app(app(subst, x0), app(app(subst, app(fix, y_0)), y_1)), x2) → APP(app(app(subst, app(fix, y_0)), y_1), x2)

The TRS R consists of the following rules:

app(app(const, x), y) → x
app(app(app(subst, f), g), x) → app(app(f, x), app(g, x))
app(app(fix, f), x) → app(app(f, app(fix, f)), x)

The set Q consists of the following terms:

app(app(const, x0), x1)
app(app(app(subst, x0), x1), x2)
app(app(fix, x0), x1)

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

(9) TransformationProof (EQUIVALENT transformation)

By forward instantiating [JAR06] the rule APP(app(fix, f), x) → APP(f, app(fix, f)) we obtained the following new rules [LPAR04]:

APP(app(fix, app(app(subst, y_0), y_1)), x1) → APP(app(app(subst, y_0), y_1), app(fix, app(app(subst, y_0), y_1))) → APP(app(fix, app(app(subst, y_0), y_1)), x1) → APP(app(app(subst, y_0), y_1), app(fix, app(app(subst, y_0), y_1)))
APP(app(fix, app(fix, y_0)), x1) → APP(app(fix, y_0), app(fix, app(fix, y_0))) → APP(app(fix, app(fix, y_0)), x1) → APP(app(fix, y_0), app(fix, app(fix, y_0)))
APP(app(fix, app(app(subst, app(app(subst, y_0), y_1)), y_2)), x1) → APP(app(app(subst, app(app(subst, y_0), y_1)), y_2), app(fix, app(app(subst, app(app(subst, y_0), y_1)), y_2))) → APP(app(fix, app(app(subst, app(app(subst, y_0), y_1)), y_2)), x1) → APP(app(app(subst, app(app(subst, y_0), y_1)), y_2), app(fix, app(app(subst, app(app(subst, y_0), y_1)), y_2)))
APP(app(fix, app(app(subst, app(fix, y_0)), y_1)), x1) → APP(app(app(subst, app(fix, y_0)), y_1), app(fix, app(app(subst, app(fix, y_0)), y_1))) → APP(app(fix, app(app(subst, app(fix, y_0)), y_1)), x1) → APP(app(app(subst, app(fix, y_0)), y_1), app(fix, app(app(subst, app(fix, y_0)), y_1)))
APP(app(fix, app(app(subst, y_0), app(app(subst, y_1), y_2))), x1) → APP(app(app(subst, y_0), app(app(subst, y_1), y_2)), app(fix, app(app(subst, y_0), app(app(subst, y_1), y_2)))) → APP(app(fix, app(app(subst, y_0), app(app(subst, y_1), y_2))), x1) → APP(app(app(subst, y_0), app(app(subst, y_1), y_2)), app(fix, app(app(subst, y_0), app(app(subst, y_1), y_2))))
APP(app(fix, app(app(subst, y_0), app(fix, y_1))), x1) → APP(app(app(subst, y_0), app(fix, y_1)), app(fix, app(app(subst, y_0), app(fix, y_1)))) → APP(app(fix, app(app(subst, y_0), app(fix, y_1))), x1) → APP(app(app(subst, y_0), app(fix, y_1)), app(fix, app(app(subst, y_0), app(fix, y_1))))
APP(app(fix, app(app(subst, y_0), app(app(subst, app(app(subst, y_1), y_2)), y_3))), x1) → APP(app(app(subst, y_0), app(app(subst, app(app(subst, y_1), y_2)), y_3)), app(fix, app(app(subst, y_0), app(app(subst, app(app(subst, y_1), y_2)), y_3)))) → APP(app(fix, app(app(subst, y_0), app(app(subst, app(app(subst, y_1), y_2)), y_3))), x1) → APP(app(app(subst, y_0), app(app(subst, app(app(subst, y_1), y_2)), y_3)), app(fix, app(app(subst, y_0), app(app(subst, app(app(subst, y_1), y_2)), y_3))))
APP(app(fix, app(app(subst, y_0), app(app(subst, app(fix, y_1)), y_2))), x1) → APP(app(app(subst, y_0), app(app(subst, app(fix, y_1)), y_2)), app(fix, app(app(subst, y_0), app(app(subst, app(fix, y_1)), y_2)))) → APP(app(fix, app(app(subst, y_0), app(app(subst, app(fix, y_1)), y_2))), x1) → APP(app(app(subst, y_0), app(app(subst, app(fix, y_1)), y_2)), app(fix, app(app(subst, y_0), app(app(subst, app(fix, y_1)), y_2))))

(10) Obligation:

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

APP(app(app(subst, f), g), x) → APP(app(f, x), app(g, x))
APP(app(fix, f), x) → APP(app(f, app(fix, f)), x)
APP(app(app(subst, app(app(subst, y_0), y_1)), x1), x2) → APP(app(app(subst, y_0), y_1), x2)
APP(app(app(subst, app(fix, y_0)), x1), x2) → APP(app(fix, y_0), x2)
APP(app(app(subst, x0), app(app(subst, y_0), y_1)), x2) → APP(app(app(subst, y_0), y_1), x2)
APP(app(app(subst, x0), app(fix, y_0)), x2) → APP(app(fix, y_0), x2)
APP(app(app(subst, x0), app(app(subst, app(app(subst, y_0), y_1)), y_2)), x2) → APP(app(app(subst, app(app(subst, y_0), y_1)), y_2), x2)
APP(app(app(subst, x0), app(app(subst, app(fix, y_0)), y_1)), x2) → APP(app(app(subst, app(fix, y_0)), y_1), x2)
APP(app(fix, app(app(subst, y_0), y_1)), x1) → APP(app(app(subst, y_0), y_1), app(fix, app(app(subst, y_0), y_1)))
APP(app(fix, app(fix, y_0)), x1) → APP(app(fix, y_0), app(fix, app(fix, y_0)))
APP(app(fix, app(app(subst, app(app(subst, y_0), y_1)), y_2)), x1) → APP(app(app(subst, app(app(subst, y_0), y_1)), y_2), app(fix, app(app(subst, app(app(subst, y_0), y_1)), y_2)))
APP(app(fix, app(app(subst, app(fix, y_0)), y_1)), x1) → APP(app(app(subst, app(fix, y_0)), y_1), app(fix, app(app(subst, app(fix, y_0)), y_1)))
APP(app(fix, app(app(subst, y_0), app(app(subst, y_1), y_2))), x1) → APP(app(app(subst, y_0), app(app(subst, y_1), y_2)), app(fix, app(app(subst, y_0), app(app(subst, y_1), y_2))))
APP(app(fix, app(app(subst, y_0), app(fix, y_1))), x1) → APP(app(app(subst, y_0), app(fix, y_1)), app(fix, app(app(subst, y_0), app(fix, y_1))))
APP(app(fix, app(app(subst, y_0), app(app(subst, app(app(subst, y_1), y_2)), y_3))), x1) → APP(app(app(subst, y_0), app(app(subst, app(app(subst, y_1), y_2)), y_3)), app(fix, app(app(subst, y_0), app(app(subst, app(app(subst, y_1), y_2)), y_3))))
APP(app(fix, app(app(subst, y_0), app(app(subst, app(fix, y_1)), y_2))), x1) → APP(app(app(subst, y_0), app(app(subst, app(fix, y_1)), y_2)), app(fix, app(app(subst, y_0), app(app(subst, app(fix, y_1)), y_2))))

The TRS R consists of the following rules:

app(app(const, x), y) → x
app(app(app(subst, f), g), x) → app(app(f, x), app(g, x))
app(app(fix, f), x) → app(app(f, app(fix, f)), x)

The set Q consists of the following terms:

app(app(const, x0), x1)
app(app(app(subst, x0), x1), x2)
app(app(fix, x0), x1)

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

(11) MNOCProof (EQUIVALENT transformation)

We use the modular non-overlap check [FROCOS05] to decrease Q to the empty set.

(12) Obligation:

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

APP(app(app(subst, f), g), x) → APP(app(f, x), app(g, x))
APP(app(fix, f), x) → APP(app(f, app(fix, f)), x)
APP(app(app(subst, app(app(subst, y_0), y_1)), x1), x2) → APP(app(app(subst, y_0), y_1), x2)
APP(app(app(subst, app(fix, y_0)), x1), x2) → APP(app(fix, y_0), x2)
APP(app(app(subst, x0), app(app(subst, y_0), y_1)), x2) → APP(app(app(subst, y_0), y_1), x2)
APP(app(app(subst, x0), app(fix, y_0)), x2) → APP(app(fix, y_0), x2)
APP(app(app(subst, x0), app(app(subst, app(app(subst, y_0), y_1)), y_2)), x2) → APP(app(app(subst, app(app(subst, y_0), y_1)), y_2), x2)
APP(app(app(subst, x0), app(app(subst, app(fix, y_0)), y_1)), x2) → APP(app(app(subst, app(fix, y_0)), y_1), x2)
APP(app(fix, app(app(subst, y_0), y_1)), x1) → APP(app(app(subst, y_0), y_1), app(fix, app(app(subst, y_0), y_1)))
APP(app(fix, app(fix, y_0)), x1) → APP(app(fix, y_0), app(fix, app(fix, y_0)))
APP(app(fix, app(app(subst, app(app(subst, y_0), y_1)), y_2)), x1) → APP(app(app(subst, app(app(subst, y_0), y_1)), y_2), app(fix, app(app(subst, app(app(subst, y_0), y_1)), y_2)))
APP(app(fix, app(app(subst, app(fix, y_0)), y_1)), x1) → APP(app(app(subst, app(fix, y_0)), y_1), app(fix, app(app(subst, app(fix, y_0)), y_1)))
APP(app(fix, app(app(subst, y_0), app(app(subst, y_1), y_2))), x1) → APP(app(app(subst, y_0), app(app(subst, y_1), y_2)), app(fix, app(app(subst, y_0), app(app(subst, y_1), y_2))))
APP(app(fix, app(app(subst, y_0), app(fix, y_1))), x1) → APP(app(app(subst, y_0), app(fix, y_1)), app(fix, app(app(subst, y_0), app(fix, y_1))))
APP(app(fix, app(app(subst, y_0), app(app(subst, app(app(subst, y_1), y_2)), y_3))), x1) → APP(app(app(subst, y_0), app(app(subst, app(app(subst, y_1), y_2)), y_3)), app(fix, app(app(subst, y_0), app(app(subst, app(app(subst, y_1), y_2)), y_3))))
APP(app(fix, app(app(subst, y_0), app(app(subst, app(fix, y_1)), y_2))), x1) → APP(app(app(subst, y_0), app(app(subst, app(fix, y_1)), y_2)), app(fix, app(app(subst, y_0), app(app(subst, app(fix, y_1)), y_2))))

The TRS R consists of the following rules:

app(app(const, x), y) → x
app(app(app(subst, f), g), x) → app(app(f, x), app(g, x))
app(app(fix, f), x) → app(app(f, app(fix, f)), x)

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

(13) NonTerminationLoopProof (COMPLETE transformation)

We used the non-termination processor [FROCOS05] to show that the DP problem is infinite.
Found a loop by narrowing to the left:

s = APP(app(app(fix, subst), x'), x) evaluates to t =APP(app(app(fix, subst), x), app(x', x))

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:
  • Matcher: [x' / x, x / app(x', x)]
  • Semiunifier: [ ]



Rewriting sequence

APP(app(app(fix, subst), x'), x) → APP(app(app(subst, app(fix, subst)), x'), x)
with rule app(app(fix, f'), x'') → app(app(f', app(fix, f')), x'') at position [0] and matcher [f' / subst, x'' / x']

APP(app(app(subst, app(fix, subst)), x'), x) → APP(app(app(fix, subst), x), app(x', x))
with rule APP(app(app(subst, f), g), x) → APP(app(f, x), app(g, x))

Now applying the matcher to the start term leads to a term which is equal to the last term in the rewriting sequence


All these steps are and every following step will be a correct step w.r.t to Q.



(14) NO