YES Termination w.r.t. Q proof of SK90_4.30.ari

(0) Obligation:

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

f(nil) → nil
f(.(nil, y)) → .(nil, f(y))
f(.(.(x, y), z)) → f(.(x, .(y, z)))
g(nil) → nil
g(.(x, nil)) → .(g(x), nil)
g(.(x, .(y, z))) → g(.(.(x, y), z))

Q is empty.

(1) QTRSRRRProof (EQUIVALENT transformation)

Used ordering:
Polynomial interpretation [POLO]:

POL(.(x1, x2)) = 1 + x1 + x2   
POL(f(x1)) = 2 + x1   
POL(g(x1)) = 2 + x1   
POL(nil) = 1   
With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:

f(nil) → nil
g(nil) → nil


(2) Obligation:

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

f(.(nil, y)) → .(nil, f(y))
f(.(.(x, y), z)) → f(.(x, .(y, z)))
g(.(x, nil)) → .(g(x), nil)
g(.(x, .(y, z))) → g(.(.(x, y), z))

Q is empty.

(3) QTRSRRRProof (EQUIVALENT transformation)

Used ordering:
Polynomial interpretation [POLO]:

POL(.(x1, x2)) = 2 + x1 + x2   
POL(f(x1)) = 2·x1   
POL(g(x1)) = 2 + x1   
POL(nil) = 2   
With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:

f(.(nil, y)) → .(nil, f(y))


(4) Obligation:

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

f(.(.(x, y), z)) → f(.(x, .(y, z)))
g(.(x, nil)) → .(g(x), nil)
g(.(x, .(y, z))) → g(.(.(x, y), z))

Q is empty.

(5) QTRSRRRProof (EQUIVALENT transformation)

Used ordering:
Polynomial interpretation [POLO]:

POL(.(x1, x2)) = x1 + x2   
POL(f(x1)) = 2·x1   
POL(g(x1)) = 2 + 2·x1   
POL(nil) = 1   
With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:

g(.(x, nil)) → .(g(x), nil)


(6) Obligation:

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

f(.(.(x, y), z)) → f(.(x, .(y, z)))
g(.(x, .(y, z))) → g(.(.(x, y), z))

Q is empty.

(7) AAECC Innermost (EQUIVALENT transformation)

We have applied [NOC,AAECCNOC] to switch to innermost. The TRS R 1 is none

The TRS R 2 is

f(.(.(x, y), z)) → f(.(x, .(y, z)))
g(.(x, .(y, z))) → g(.(.(x, y), z))

The signature Sigma is {f, g}

(8) Obligation:

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

f(.(.(x, y), z)) → f(.(x, .(y, z)))
g(.(x, .(y, z))) → g(.(.(x, y), z))

The set Q consists of the following terms:

f(.(.(x0, x1), x2))
g(.(x0, .(x1, x2)))

(9) DependencyPairsProof (EQUIVALENT transformation)

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

(10) Obligation:

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

F(.(.(x, y), z)) → F(.(x, .(y, z)))
G(.(x, .(y, z))) → G(.(.(x, y), z))

The TRS R consists of the following rules:

f(.(.(x, y), z)) → f(.(x, .(y, z)))
g(.(x, .(y, z))) → g(.(.(x, y), z))

The set Q consists of the following terms:

f(.(.(x0, x1), x2))
g(.(x0, .(x1, x2)))

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

(11) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 2 SCCs.

(12) Complex Obligation (AND)

(13) Obligation:

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

G(.(x, .(y, z))) → G(.(.(x, y), z))

The TRS R consists of the following rules:

f(.(.(x, y), z)) → f(.(x, .(y, z)))
g(.(x, .(y, z))) → g(.(.(x, y), z))

The set Q consists of the following terms:

f(.(.(x0, x1), x2))
g(.(x0, .(x1, x2)))

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

(14) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(15) Obligation:

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

G(.(x, .(y, z))) → G(.(.(x, y), z))

R is empty.
The set Q consists of the following terms:

f(.(.(x0, x1), x2))
g(.(x0, .(x1, x2)))

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

(16) QReductionProof (EQUIVALENT transformation)

We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

f(.(.(x0, x1), x2))
g(.(x0, .(x1, x2)))

(17) Obligation:

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

G(.(x, .(y, z))) → G(.(.(x, y), z))

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

(18) MRRProof (EQUIVALENT transformation)

By using the rule removal processor [LPAR04] with the following ordering, at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.
Strictly oriented dependency pairs:

G(.(x, .(y, z))) → G(.(.(x, y), z))


Used ordering: Polynomial interpretation [POLO]:

POL(.(x1, x2)) = 2 + x1 + 2·x2   
POL(G(x1)) = 2·x1   

(19) Obligation:

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

(20) PisEmptyProof (EQUIVALENT transformation)

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

(21) YES

(22) Obligation:

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

F(.(.(x, y), z)) → F(.(x, .(y, z)))

The TRS R consists of the following rules:

f(.(.(x, y), z)) → f(.(x, .(y, z)))
g(.(x, .(y, z))) → g(.(.(x, y), z))

The set Q consists of the following terms:

f(.(.(x0, x1), x2))
g(.(x0, .(x1, x2)))

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

(23) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(24) Obligation:

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

F(.(.(x, y), z)) → F(.(x, .(y, z)))

R is empty.
The set Q consists of the following terms:

f(.(.(x0, x1), x2))
g(.(x0, .(x1, x2)))

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

(25) QReductionProof (EQUIVALENT transformation)

We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

f(.(.(x0, x1), x2))
g(.(x0, .(x1, x2)))

(26) Obligation:

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

F(.(.(x, y), z)) → F(.(x, .(y, z)))

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

(27) MRRProof (EQUIVALENT transformation)

By using the rule removal processor [LPAR04] with the following ordering, at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.
Strictly oriented dependency pairs:

F(.(.(x, y), z)) → F(.(x, .(y, z)))


Used ordering: Knuth-Bendix order [KBO] with precedence:
.2 > F1

and weight map:

F_1=1
._2=0

The variable weight is 1

(28) Obligation:

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

(29) PisEmptyProof (EQUIVALENT transformation)

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

(30) YES