(0) Obligation:
Q restricted rewrite system:
The TRS R consists of the following rules:
a__f(b, X, c) → a__f(X, a__c, X)
a__c → b
mark(f(X1, X2, X3)) → a__f(X1, mark(X2), X3)
mark(c) → a__c
mark(b) → b
a__f(X1, X2, X3) → f(X1, X2, X3)
a__c → c
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:
A__F(b, X, c) → A__F(X, a__c, X)
A__F(b, X, c) → A__C
MARK(f(X1, X2, X3)) → A__F(X1, mark(X2), X3)
MARK(f(X1, X2, X3)) → MARK(X2)
MARK(c) → A__C
The TRS R consists of the following rules:
a__f(b, X, c) → a__f(X, a__c, X)
a__c → b
mark(f(X1, X2, X3)) → a__f(X1, mark(X2), X3)
mark(c) → a__c
mark(b) → b
a__f(X1, X2, X3) → f(X1, X2, X3)
a__c → c
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 3 less nodes.
(4) Complex Obligation (AND)
(5) Obligation:
Q DP problem:
The TRS P consists of the following rules:
A__F(b, X, c) → A__F(X, a__c, X)
The TRS R consists of the following rules:
a__f(b, X, c) → a__f(X, a__c, X)
a__c → b
mark(f(X1, X2, X3)) → a__f(X1, mark(X2), X3)
mark(c) → a__c
mark(b) → b
a__f(X1, X2, X3) → f(X1, X2, X3)
a__c → c
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(6) Obligation:
Q DP problem:
The TRS P consists of the following rules:
MARK(f(X1, X2, X3)) → MARK(X2)
The TRS R consists of the following rules:
a__f(b, X, c) → a__f(X, a__c, X)
a__c → b
mark(f(X1, X2, X3)) → a__f(X1, mark(X2), X3)
mark(c) → a__c
mark(b) → b
a__f(X1, X2, X3) → f(X1, X2, X3)
a__c → c
Q is empty.
We have to consider all minimal (P,Q,R)-chains.