Left Termination proof of /tmp/tmpmaOu3N/giesl97.pl

Left Termination of the query pattern f_in_3(g, a, a) w.r.t. the given Prolog program could not be shown:

0 Prolog

↳1 CutEliminatorProof (⇐)

↳2 Prolog

  ↳3 PrologToPiTRSProof (⇐)

    ↳4 PiTRS

    ↳5 DependencyPairsProof (⇔)

    ↳6 PiDP

    ↳7 DependencyGraphProof (⇔)

    ↳8 PiDP

    ↳9 PiDPToQDPProof (⇐)

    ↳10 QDP

    ↳11 UsableRulesReductionPairsProof (⇔)

    ↳12 QDP

    ↳13 Narrowing (⇐)

    ↳14 QDP

    ↳15 Instantiation (⇔)

    ↳16 QDP

    ↳17 Instantiation (⇔)

    ↳18 QDP

    ↳19 Narrowing (⇐)

    ↳20 QDP

    ↳21 Rewriting (⇔)

    ↳22 QDP

    ↳23 Rewriting (⇔)

    ↳24 QDP

    ↳25 Rewriting (⇔)

    ↳26 QDP

    ↳27 ForwardInstantiation (⇔)

    ↳28 QDP

    ↳29 NonTerminationProof (⇔)

    ↳30 FALSE

  ↳31 PrologToPiTRSProof (⇐)

    ↳32 PiTRS

    ↳33 DependencyPairsProof (⇔)

    ↳34 PiDP

    ↳35 DependencyGraphProof (⇔)

    ↳36 PiDP

    ↳37 PiDPToQDPProof (⇐)

    ↳38 QDP

    ↳39 Narrowing (⇐)

    ↳40 QDP

    ↳41 Instantiation (⇔)

    ↳42 QDP

    ↳43 Instantiation (⇔)

    ↳44 QDP

    ↳45 QDPOrderProof (⇔)

    ↳46 QDP

    ↳47 DependencyGraphProof (⇔)

    ↳48 QDP

      ↳49 Instantiation (⇔)

        ↳50 QDP

      ↳51 Instantiation (⇔)

        ↳52 QDP

        ↳53 Narrowing (⇐)

        ↳54 QDP

        ↳55 Rewriting (⇔)

        ↳56 QDP

        ↳57 Rewriting (⇔)

        ↳58 QDP

        ↳59 Rewriting (⇔)

        ↳60 QDP

        ↳61 ForwardInstantiation (⇔)

        ↳62 QDP

        ↳63 NonTerminationProof (⇔)

        ↳64 FALSE

(0) Obligation:

Clauses:

f(0, Y, Z) :- ','(!, eq(Z, 0)).
f(X, Y, Z) :- ','(p(X, P), ','(f(P, Y, U), f(U, Y, Z))).
p(0, 0).
p(s(X), X).
eq(X, X).

Queries:

f(g,a,a).

(1) CutEliminatorProof (SOUND transformation)

Eliminated all cuts by simply ignoring them[PROLOG].

(2) Obligation:

Clauses:

f(0, Y, Z) :- eq(Z, 0).
f(X, Y, Z) :- ','(p(X, P), ','(f(P, Y, U), f(U, Y, Z))).
p(0, 0).
p(s(X), X).
eq(X, X).

Queries:

f(g,a,a).

(3) PrologToPiTRSProof (SOUND transformation)

We use the technique of [LOPSTR]. With regard to the inferred argument filtering the predicates were used in the following modes:
f_in: (b,f,f)
Transforming Prolog into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:

f_in_gaa(0, Y, Z) → U1_gaa(Y, Z, eq_in_ag(Z, 0))
eq_in_ag(X, X) → eq_out_ag(X, X)
U1_gaa(Y, Z, eq_out_ag(Z, 0)) → f_out_gaa(0, Y, Z)
f_in_gaa(X, Y, Z) → U2_gaa(X, Y, Z, p_in_ga(X, P))
p_in_ga(0, 0) → p_out_ga(0, 0)
p_in_ga(s(X), X) → p_out_ga(s(X), X)
U2_gaa(X, Y, Z, p_out_ga(X, P)) → U3_gaa(X, Y, Z, P, f_in_gaa(P, Y, U))
U3_gaa(X, Y, Z, P, f_out_gaa(P, Y, U)) → U4_gaa(X, Y, Z, f_in_gaa(U, Y, Z))
U4_gaa(X, Y, Z, f_out_gaa(U, Y, Z)) → f_out_gaa(X, Y, Z)

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog

(4) Obligation:

Pi-finite rewrite system:
The TRS R consists of the following rules:

f_in_gaa(0, Y, Z) → U1_gaa(Y, Z, eq_in_ag(Z, 0))
eq_in_ag(X, X) → eq_out_ag(X, X)
U1_gaa(Y, Z, eq_out_ag(Z, 0)) → f_out_gaa(0, Y, Z)
f_in_gaa(X, Y, Z) → U2_gaa(X, Y, Z, p_in_ga(X, P))
p_in_ga(0, 0) → p_out_ga(0, 0)
p_in_ga(s(X), X) → p_out_ga(s(X), X)
U2_gaa(X, Y, Z, p_out_ga(X, P)) → U3_gaa(X, Y, Z, P, f_in_gaa(P, Y, U))
U3_gaa(X, Y, Z, P, f_out_gaa(P, Y, U)) → U4_gaa(X, Y, Z, f_in_gaa(U, Y, Z))
U4_gaa(X, Y, Z, f_out_gaa(U, Y, Z)) → f_out_gaa(X, Y, Z)

(5) DependencyPairsProof (EQUIVALENT transformation)

Using Dependency Pairs [AG00,LOPSTR] we result in the following initial DP problem:
Pi DP problem:
The TRS P consists of the following rules:

F_IN_GAA(0, Y, Z) → U1_GAA(Y, Z, eq_in_ag(Z, 0))
F_IN_GAA(0, Y, Z) → EQ_IN_AG(Z, 0)
F_IN_GAA(X, Y, Z) → U2_GAA(X, Y, Z, p_in_ga(X, P))
F_IN_GAA(X, Y, Z) → P_IN_GA(X, P)
U2_GAA(X, Y, Z, p_out_ga(X, P)) → U3_GAA(X, Y, Z, P, f_in_gaa(P, Y, U))
U2_GAA(X, Y, Z, p_out_ga(X, P)) → F_IN_GAA(P, Y, U)
U3_GAA(X, Y, Z, P, f_out_gaa(P, Y, U)) → U4_GAA(X, Y, Z, f_in_gaa(U, Y, Z))
U3_GAA(X, Y, Z, P, f_out_gaa(P, Y, U)) → F_IN_GAA(U, Y, Z)

The TRS R consists of the following rules:

f_in_gaa(0, Y, Z) → U1_gaa(Y, Z, eq_in_ag(Z, 0))
eq_in_ag(X, X) → eq_out_ag(X, X)
U1_gaa(Y, Z, eq_out_ag(Z, 0)) → f_out_gaa(0, Y, Z)
f_in_gaa(X, Y, Z) → U2_gaa(X, Y, Z, p_in_ga(X, P))
p_in_ga(0, 0) → p_out_ga(0, 0)
p_in_ga(s(X), X) → p_out_ga(s(X), X)
U2_gaa(X, Y, Z, p_out_ga(X, P)) → U3_gaa(X, Y, Z, P, f_in_gaa(P, Y, U))
U3_gaa(X, Y, Z, P, f_out_gaa(P, Y, U)) → U4_gaa(X, Y, Z, f_in_gaa(U, Y, Z))
U4_gaa(X, Y, Z, f_out_gaa(U, Y, Z)) → f_out_gaa(X, Y, Z)

The argument filtering Pi contains the following mapping:
f_in_gaa(x1, x2, x3) = f_in_gaa(x1)
0 = 0
U1_gaa(x1, x2, x3) = U1_gaa(x3)
eq_in_ag(x1, x2) = eq_in_ag(x2)
eq_out_ag(x1, x2) = eq_out_ag(x1)
f_out_gaa(x1, x2, x3) = f_out_gaa(x3)
U2_gaa(x1, x2, x3, x4) = U2_gaa(x4)
p_in_ga(x1, x2) = p_in_ga(x1)
p_out_ga(x1, x2) = p_out_ga(x2)
s(x1) = s(x1)
U3_gaa(x1, x2, x3, x4, x5) = U3_gaa(x5)
U4_gaa(x1, x2, x3, x4) = U4_gaa(x4)
F_IN_GAA(x1, x2, x3) = F_IN_GAA(x1)
U1_GAA(x1, x2, x3) = U1_GAA(x3)
EQ_IN_AG(x1, x2) = EQ_IN_AG(x2)
U2_GAA(x1, x2, x3, x4) = U2_GAA(x4)
P_IN_GA(x1, x2) = P_IN_GA(x1)
U3_GAA(x1, x2, x3, x4, x5) = U3_GAA(x5)
U4_GAA(x1, x2, x3, x4) = U4_GAA(x4)

We have to consider all (P,R,Pi)-chains

(6) Obligation:

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

F_IN_GAA(0, Y, Z) → U1_GAA(Y, Z, eq_in_ag(Z, 0))
F_IN_GAA(0, Y, Z) → EQ_IN_AG(Z, 0)
F_IN_GAA(X, Y, Z) → U2_GAA(X, Y, Z, p_in_ga(X, P))
F_IN_GAA(X, Y, Z) → P_IN_GA(X, P)
U2_GAA(X, Y, Z, p_out_ga(X, P)) → U3_GAA(X, Y, Z, P, f_in_gaa(P, Y, U))
U2_GAA(X, Y, Z, p_out_ga(X, P)) → F_IN_GAA(P, Y, U)
U3_GAA(X, Y, Z, P, f_out_gaa(P, Y, U)) → U4_GAA(X, Y, Z, f_in_gaa(U, Y, Z))
U3_GAA(X, Y, Z, P, f_out_gaa(P, Y, U)) → F_IN_GAA(U, Y, Z)

The TRS R consists of the following rules:

f_in_gaa(0, Y, Z) → U1_gaa(Y, Z, eq_in_ag(Z, 0))
eq_in_ag(X, X) → eq_out_ag(X, X)
U1_gaa(Y, Z, eq_out_ag(Z, 0)) → f_out_gaa(0, Y, Z)
f_in_gaa(X, Y, Z) → U2_gaa(X, Y, Z, p_in_ga(X, P))
p_in_ga(0, 0) → p_out_ga(0, 0)
p_in_ga(s(X), X) → p_out_ga(s(X), X)
U2_gaa(X, Y, Z, p_out_ga(X, P)) → U3_gaa(X, Y, Z, P, f_in_gaa(P, Y, U))
U3_gaa(X, Y, Z, P, f_out_gaa(P, Y, U)) → U4_gaa(X, Y, Z, f_in_gaa(U, Y, Z))
U4_gaa(X, Y, Z, f_out_gaa(U, Y, Z)) → f_out_gaa(X, Y, Z)

(7) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 1 SCC with 4 less nodes.

(8) Obligation:

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

F_IN_GAA(X, Y, Z) → U2_GAA(X, Y, Z, p_in_ga(X, P))
U2_GAA(X, Y, Z, p_out_ga(X, P)) → U3_GAA(X, Y, Z, P, f_in_gaa(P, Y, U))
U3_GAA(X, Y, Z, P, f_out_gaa(P, Y, U)) → F_IN_GAA(U, Y, Z)
U2_GAA(X, Y, Z, p_out_ga(X, P)) → F_IN_GAA(P, Y, U)

The TRS R consists of the following rules:

f_in_gaa(0, Y, Z) → U1_gaa(Y, Z, eq_in_ag(Z, 0))
eq_in_ag(X, X) → eq_out_ag(X, X)
U1_gaa(Y, Z, eq_out_ag(Z, 0)) → f_out_gaa(0, Y, Z)
f_in_gaa(X, Y, Z) → U2_gaa(X, Y, Z, p_in_ga(X, P))
p_in_ga(0, 0) → p_out_ga(0, 0)
p_in_ga(s(X), X) → p_out_ga(s(X), X)
U2_gaa(X, Y, Z, p_out_ga(X, P)) → U3_gaa(X, Y, Z, P, f_in_gaa(P, Y, U))
U3_gaa(X, Y, Z, P, f_out_gaa(P, Y, U)) → U4_gaa(X, Y, Z, f_in_gaa(U, Y, Z))
U4_gaa(X, Y, Z, f_out_gaa(U, Y, Z)) → f_out_gaa(X, Y, Z)

The argument filtering Pi contains the following mapping:
f_in_gaa(x1, x2, x3) = f_in_gaa(x1)
0 = 0
U1_gaa(x1, x2, x3) = U1_gaa(x3)
eq_in_ag(x1, x2) = eq_in_ag(x2)
eq_out_ag(x1, x2) = eq_out_ag(x1)
f_out_gaa(x1, x2, x3) = f_out_gaa(x3)
U2_gaa(x1, x2, x3, x4) = U2_gaa(x4)
p_in_ga(x1, x2) = p_in_ga(x1)
p_out_ga(x1, x2) = p_out_ga(x2)
s(x1) = s(x1)
U3_gaa(x1, x2, x3, x4, x5) = U3_gaa(x5)
U4_gaa(x1, x2, x3, x4) = U4_gaa(x4)
F_IN_GAA(x1, x2, x3) = F_IN_GAA(x1)
U2_GAA(x1, x2, x3, x4) = U2_GAA(x4)
U3_GAA(x1, x2, x3, x4, x5) = U3_GAA(x5)

We have to consider all (P,R,Pi)-chains

(9) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(10) Obligation:

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

F_IN_GAA(X) → U2_GAA(p_in_ga(X))
U2_GAA(p_out_ga(P)) → U3_GAA(f_in_gaa(P))
U3_GAA(f_out_gaa(U)) → F_IN_GAA(U)
U2_GAA(p_out_ga(P)) → F_IN_GAA(P)

The TRS R consists of the following rules:

f_in_gaa(0) → U1_gaa(eq_in_ag(0))
eq_in_ag(X) → eq_out_ag(X)
U1_gaa(eq_out_ag(Z)) → f_out_gaa(Z)
f_in_gaa(X) → U2_gaa(p_in_ga(X))
p_in_ga(0) → p_out_ga(0)
p_in_ga(s(X)) → p_out_ga(X)
U2_gaa(p_out_ga(P)) → U3_gaa(f_in_gaa(P))
U3_gaa(f_out_gaa(U)) → U4_gaa(f_in_gaa(U))
U4_gaa(f_out_gaa(Z)) → f_out_gaa(Z)

The set Q consists of the following terms:

f_in_gaa(x0)
eq_in_ag(x0)
U1_gaa(x0)
p_in_ga(x0)
U2_gaa(x0)
U3_gaa(x0)
U4_gaa(x0)

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

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

No dependency pairs are removed.

The following rules are removed from R:

p_in_ga(s(X)) → p_out_ga(X)

Used ordering: POLO with Polynomial interpretation [POLO]:

POL(0) = 0
POL(F_IN_GAA(x₁)) = 2·x₁
POL(U1_gaa(x₁)) = x₁
POL(U2_GAA(x₁)) = x₁
POL(U2_gaa(x₁)) = x₁
POL(U3_GAA(x₁)) = x₁
POL(U3_gaa(x₁)) = x₁
POL(U4_gaa(x₁)) = x₁
POL(eq_in_ag(x₁)) = 2·x₁
POL(eq_out_ag(x₁)) = 2·x₁
POL(f_in_gaa(x₁)) = 2·x₁
POL(f_out_gaa(x₁)) = 2·x₁
POL(p_in_ga(x₁)) = 2·x₁
POL(p_out_ga(x₁)) = 2·x₁
POL(s(x₁)) = 1 + 2·x₁

(12) Obligation:

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

F_IN_GAA(X) → U2_GAA(p_in_ga(X))
U2_GAA(p_out_ga(P)) → U3_GAA(f_in_gaa(P))
U3_GAA(f_out_gaa(U)) → F_IN_GAA(U)
U2_GAA(p_out_ga(P)) → F_IN_GAA(P)

The TRS R consists of the following rules:

f_in_gaa(0) → U1_gaa(eq_in_ag(0))
f_in_gaa(X) → U2_gaa(p_in_ga(X))
p_in_ga(0) → p_out_ga(0)
U2_gaa(p_out_ga(P)) → U3_gaa(f_in_gaa(P))
U3_gaa(f_out_gaa(U)) → U4_gaa(f_in_gaa(U))
U4_gaa(f_out_gaa(Z)) → f_out_gaa(Z)
eq_in_ag(X) → eq_out_ag(X)
U1_gaa(eq_out_ag(Z)) → f_out_gaa(Z)

The set Q consists of the following terms:

f_in_gaa(x0)
eq_in_ag(x0)
U1_gaa(x0)
p_in_ga(x0)
U2_gaa(x0)
U3_gaa(x0)
U4_gaa(x0)

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

(13) Narrowing (SOUND transformation)

By narrowing [LPAR04] the rule F_IN_GAA(X) → U2_GAA(p_in_ga(X)) at position [0] we obtained the following new rules [LPAR04]:

F_IN_GAA(0) → U2_GAA(p_out_ga(0))

(14) Obligation:

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

U2_GAA(p_out_ga(P)) → U3_GAA(f_in_gaa(P))
U3_GAA(f_out_gaa(U)) → F_IN_GAA(U)
U2_GAA(p_out_ga(P)) → F_IN_GAA(P)
F_IN_GAA(0) → U2_GAA(p_out_ga(0))

The TRS R consists of the following rules:

f_in_gaa(0) → U1_gaa(eq_in_ag(0))
f_in_gaa(X) → U2_gaa(p_in_ga(X))
p_in_ga(0) → p_out_ga(0)
U2_gaa(p_out_ga(P)) → U3_gaa(f_in_gaa(P))
U3_gaa(f_out_gaa(U)) → U4_gaa(f_in_gaa(U))
U4_gaa(f_out_gaa(Z)) → f_out_gaa(Z)
eq_in_ag(X) → eq_out_ag(X)
U1_gaa(eq_out_ag(Z)) → f_out_gaa(Z)

The set Q consists of the following terms:

f_in_gaa(x0)
eq_in_ag(x0)
U1_gaa(x0)
p_in_ga(x0)
U2_gaa(x0)
U3_gaa(x0)
U4_gaa(x0)

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

(15) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule U2_GAA(p_out_ga(P)) → U3_GAA(f_in_gaa(P)) we obtained the following new rules [LPAR04]:

U2_GAA(p_out_ga(0)) → U3_GAA(f_in_gaa(0))

(16) Obligation:

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

U3_GAA(f_out_gaa(U)) → F_IN_GAA(U)
U2_GAA(p_out_ga(P)) → F_IN_GAA(P)
F_IN_GAA(0) → U2_GAA(p_out_ga(0))
U2_GAA(p_out_ga(0)) → U3_GAA(f_in_gaa(0))

The TRS R consists of the following rules:

f_in_gaa(0) → U1_gaa(eq_in_ag(0))
f_in_gaa(X) → U2_gaa(p_in_ga(X))
p_in_ga(0) → p_out_ga(0)
U2_gaa(p_out_ga(P)) → U3_gaa(f_in_gaa(P))
U3_gaa(f_out_gaa(U)) → U4_gaa(f_in_gaa(U))
U4_gaa(f_out_gaa(Z)) → f_out_gaa(Z)
eq_in_ag(X) → eq_out_ag(X)
U1_gaa(eq_out_ag(Z)) → f_out_gaa(Z)

The set Q consists of the following terms:

f_in_gaa(x0)
eq_in_ag(x0)
U1_gaa(x0)
p_in_ga(x0)
U2_gaa(x0)
U3_gaa(x0)
U4_gaa(x0)

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

(17) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule U2_GAA(p_out_ga(P)) → F_IN_GAA(P) we obtained the following new rules [LPAR04]:

U2_GAA(p_out_ga(0)) → F_IN_GAA(0)

(18) Obligation:

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

U3_GAA(f_out_gaa(U)) → F_IN_GAA(U)
F_IN_GAA(0) → U2_GAA(p_out_ga(0))
U2_GAA(p_out_ga(0)) → U3_GAA(f_in_gaa(0))
U2_GAA(p_out_ga(0)) → F_IN_GAA(0)

The TRS R consists of the following rules:

f_in_gaa(0) → U1_gaa(eq_in_ag(0))
f_in_gaa(X) → U2_gaa(p_in_ga(X))
p_in_ga(0) → p_out_ga(0)
U2_gaa(p_out_ga(P)) → U3_gaa(f_in_gaa(P))
U3_gaa(f_out_gaa(U)) → U4_gaa(f_in_gaa(U))
U4_gaa(f_out_gaa(Z)) → f_out_gaa(Z)
eq_in_ag(X) → eq_out_ag(X)
U1_gaa(eq_out_ag(Z)) → f_out_gaa(Z)

The set Q consists of the following terms:

f_in_gaa(x0)
eq_in_ag(x0)
U1_gaa(x0)
p_in_ga(x0)
U2_gaa(x0)
U3_gaa(x0)
U4_gaa(x0)

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

(19) Narrowing (SOUND transformation)

By narrowing [LPAR04] the rule U2_GAA(p_out_ga(0)) → U3_GAA(f_in_gaa(0)) at position [0] we obtained the following new rules [LPAR04]:

U2_GAA(p_out_ga(0)) → U3_GAA(U1_gaa(eq_in_ag(0)))
U2_GAA(p_out_ga(0)) → U3_GAA(U2_gaa(p_in_ga(0)))

(20) Obligation:

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

U3_GAA(f_out_gaa(U)) → F_IN_GAA(U)
F_IN_GAA(0) → U2_GAA(p_out_ga(0))
U2_GAA(p_out_ga(0)) → F_IN_GAA(0)
U2_GAA(p_out_ga(0)) → U3_GAA(U1_gaa(eq_in_ag(0)))
U2_GAA(p_out_ga(0)) → U3_GAA(U2_gaa(p_in_ga(0)))

The TRS R consists of the following rules:

f_in_gaa(0) → U1_gaa(eq_in_ag(0))
f_in_gaa(X) → U2_gaa(p_in_ga(X))
p_in_ga(0) → p_out_ga(0)
U2_gaa(p_out_ga(P)) → U3_gaa(f_in_gaa(P))
U3_gaa(f_out_gaa(U)) → U4_gaa(f_in_gaa(U))
U4_gaa(f_out_gaa(Z)) → f_out_gaa(Z)
eq_in_ag(X) → eq_out_ag(X)
U1_gaa(eq_out_ag(Z)) → f_out_gaa(Z)

The set Q consists of the following terms:

f_in_gaa(x0)
eq_in_ag(x0)
U1_gaa(x0)
p_in_ga(x0)
U2_gaa(x0)
U3_gaa(x0)
U4_gaa(x0)

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

(21) Rewriting (EQUIVALENT transformation)

By rewriting [LPAR04] the rule U2_GAA(p_out_ga(0)) → U3_GAA(U1_gaa(eq_in_ag(0))) at position [0,0] we obtained the following new rules [LPAR04]:

U2_GAA(p_out_ga(0)) → U3_GAA(U1_gaa(eq_out_ag(0)))

(22) Obligation:

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

U3_GAA(f_out_gaa(U)) → F_IN_GAA(U)
F_IN_GAA(0) → U2_GAA(p_out_ga(0))
U2_GAA(p_out_ga(0)) → F_IN_GAA(0)
U2_GAA(p_out_ga(0)) → U3_GAA(U2_gaa(p_in_ga(0)))
U2_GAA(p_out_ga(0)) → U3_GAA(U1_gaa(eq_out_ag(0)))

The TRS R consists of the following rules:

f_in_gaa(0) → U1_gaa(eq_in_ag(0))
f_in_gaa(X) → U2_gaa(p_in_ga(X))
p_in_ga(0) → p_out_ga(0)
U2_gaa(p_out_ga(P)) → U3_gaa(f_in_gaa(P))
U3_gaa(f_out_gaa(U)) → U4_gaa(f_in_gaa(U))
U4_gaa(f_out_gaa(Z)) → f_out_gaa(Z)
eq_in_ag(X) → eq_out_ag(X)
U1_gaa(eq_out_ag(Z)) → f_out_gaa(Z)

The set Q consists of the following terms:

f_in_gaa(x0)
eq_in_ag(x0)
U1_gaa(x0)
p_in_ga(x0)
U2_gaa(x0)
U3_gaa(x0)
U4_gaa(x0)

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

(23) Rewriting (EQUIVALENT transformation)

By rewriting [LPAR04] the rule U2_GAA(p_out_ga(0)) → U3_GAA(U2_gaa(p_in_ga(0))) at position [0,0] we obtained the following new rules [LPAR04]:

U2_GAA(p_out_ga(0)) → U3_GAA(U2_gaa(p_out_ga(0)))

(24) Obligation:

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

U3_GAA(f_out_gaa(U)) → F_IN_GAA(U)
F_IN_GAA(0) → U2_GAA(p_out_ga(0))
U2_GAA(p_out_ga(0)) → F_IN_GAA(0)
U2_GAA(p_out_ga(0)) → U3_GAA(U1_gaa(eq_out_ag(0)))
U2_GAA(p_out_ga(0)) → U3_GAA(U2_gaa(p_out_ga(0)))

The TRS R consists of the following rules:

f_in_gaa(0) → U1_gaa(eq_in_ag(0))
f_in_gaa(X) → U2_gaa(p_in_ga(X))
p_in_ga(0) → p_out_ga(0)
U2_gaa(p_out_ga(P)) → U3_gaa(f_in_gaa(P))
U3_gaa(f_out_gaa(U)) → U4_gaa(f_in_gaa(U))
U4_gaa(f_out_gaa(Z)) → f_out_gaa(Z)
eq_in_ag(X) → eq_out_ag(X)
U1_gaa(eq_out_ag(Z)) → f_out_gaa(Z)

The set Q consists of the following terms:

f_in_gaa(x0)
eq_in_ag(x0)
U1_gaa(x0)
p_in_ga(x0)
U2_gaa(x0)
U3_gaa(x0)
U4_gaa(x0)

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

(25) Rewriting (EQUIVALENT transformation)

By rewriting [LPAR04] the rule U2_GAA(p_out_ga(0)) → U3_GAA(U1_gaa(eq_out_ag(0))) at position [0] we obtained the following new rules [LPAR04]:

U2_GAA(p_out_ga(0)) → U3_GAA(f_out_gaa(0))

(26) Obligation:

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

U3_GAA(f_out_gaa(U)) → F_IN_GAA(U)
F_IN_GAA(0) → U2_GAA(p_out_ga(0))
U2_GAA(p_out_ga(0)) → F_IN_GAA(0)
U2_GAA(p_out_ga(0)) → U3_GAA(U2_gaa(p_out_ga(0)))
U2_GAA(p_out_ga(0)) → U3_GAA(f_out_gaa(0))

The TRS R consists of the following rules:

f_in_gaa(0) → U1_gaa(eq_in_ag(0))
f_in_gaa(X) → U2_gaa(p_in_ga(X))
p_in_ga(0) → p_out_ga(0)
U2_gaa(p_out_ga(P)) → U3_gaa(f_in_gaa(P))
U3_gaa(f_out_gaa(U)) → U4_gaa(f_in_gaa(U))
U4_gaa(f_out_gaa(Z)) → f_out_gaa(Z)
eq_in_ag(X) → eq_out_ag(X)
U1_gaa(eq_out_ag(Z)) → f_out_gaa(Z)

The set Q consists of the following terms:

f_in_gaa(x0)
eq_in_ag(x0)
U1_gaa(x0)
p_in_ga(x0)
U2_gaa(x0)
U3_gaa(x0)
U4_gaa(x0)

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

(27) ForwardInstantiation (EQUIVALENT transformation)

By forward instantiating [JAR06] the rule U3_GAA(f_out_gaa(U)) → F_IN_GAA(U) we obtained the following new rules [LPAR04]:

U3_GAA(f_out_gaa(0)) → F_IN_GAA(0)

(28) Obligation:

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

F_IN_GAA(0) → U2_GAA(p_out_ga(0))
U2_GAA(p_out_ga(0)) → F_IN_GAA(0)
U2_GAA(p_out_ga(0)) → U3_GAA(U2_gaa(p_out_ga(0)))
U2_GAA(p_out_ga(0)) → U3_GAA(f_out_gaa(0))
U3_GAA(f_out_gaa(0)) → F_IN_GAA(0)

The TRS R consists of the following rules:

f_in_gaa(0) → U1_gaa(eq_in_ag(0))
f_in_gaa(X) → U2_gaa(p_in_ga(X))
p_in_ga(0) → p_out_ga(0)
U2_gaa(p_out_ga(P)) → U3_gaa(f_in_gaa(P))
U3_gaa(f_out_gaa(U)) → U4_gaa(f_in_gaa(U))
U4_gaa(f_out_gaa(Z)) → f_out_gaa(Z)
eq_in_ag(X) → eq_out_ag(X)
U1_gaa(eq_out_ag(Z)) → f_out_gaa(Z)

The set Q consists of the following terms:

f_in_gaa(x0)
eq_in_ag(x0)
U1_gaa(x0)
p_in_ga(x0)
U2_gaa(x0)
U3_gaa(x0)
U4_gaa(x0)

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

(29) NonTerminationProof (EQUIVALENT 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 = U2_GAA(p_out_ga(0)) evaluates to t =U2_GAA(p_out_ga(0))

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:

Semiunifier: [ ]
Matcher: [ ]

Rewriting sequence

U2_GAA(p_out_ga(0)) → F_IN_GAA(0)
with rule U2_GAA(p_out_ga(0)) → F_IN_GAA(0) at position [] and matcher [ ]

F_IN_GAA(0) → U2_GAA(p_out_ga(0))
with rule F_IN_GAA(0) → U2_GAA(p_out_ga(0))

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.

(30) FALSE

(31) PrologToPiTRSProof (SOUND transformation)

f_in_gaa(0, Y, Z) → U1_gaa(Y, Z, eq_in_ag(Z, 0))
eq_in_ag(X, X) → eq_out_ag(X, X)
U1_gaa(Y, Z, eq_out_ag(Z, 0)) → f_out_gaa(0, Y, Z)
f_in_gaa(X, Y, Z) → U2_gaa(X, Y, Z, p_in_ga(X, P))
p_in_ga(0, 0) → p_out_ga(0, 0)
p_in_ga(s(X), X) → p_out_ga(s(X), X)
U2_gaa(X, Y, Z, p_out_ga(X, P)) → U3_gaa(X, Y, Z, P, f_in_gaa(P, Y, U))
U3_gaa(X, Y, Z, P, f_out_gaa(P, Y, U)) → U4_gaa(X, Y, Z, f_in_gaa(U, Y, Z))
U4_gaa(X, Y, Z, f_out_gaa(U, Y, Z)) → f_out_gaa(X, Y, Z)

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog

(32) Obligation:

Pi-finite rewrite system:
The TRS R consists of the following rules:

f_in_gaa(0, Y, Z) → U1_gaa(Y, Z, eq_in_ag(Z, 0))
eq_in_ag(X, X) → eq_out_ag(X, X)
U1_gaa(Y, Z, eq_out_ag(Z, 0)) → f_out_gaa(0, Y, Z)
f_in_gaa(X, Y, Z) → U2_gaa(X, Y, Z, p_in_ga(X, P))
p_in_ga(0, 0) → p_out_ga(0, 0)
p_in_ga(s(X), X) → p_out_ga(s(X), X)
U2_gaa(X, Y, Z, p_out_ga(X, P)) → U3_gaa(X, Y, Z, P, f_in_gaa(P, Y, U))
U3_gaa(X, Y, Z, P, f_out_gaa(P, Y, U)) → U4_gaa(X, Y, Z, f_in_gaa(U, Y, Z))
U4_gaa(X, Y, Z, f_out_gaa(U, Y, Z)) → f_out_gaa(X, Y, Z)

(33) DependencyPairsProof (EQUIVALENT transformation)

Using Dependency Pairs [AG00,LOPSTR] we result in the following initial DP problem:
Pi DP problem:
The TRS P consists of the following rules:

F_IN_GAA(0, Y, Z) → U1_GAA(Y, Z, eq_in_ag(Z, 0))
F_IN_GAA(0, Y, Z) → EQ_IN_AG(Z, 0)
F_IN_GAA(X, Y, Z) → U2_GAA(X, Y, Z, p_in_ga(X, P))
F_IN_GAA(X, Y, Z) → P_IN_GA(X, P)
U2_GAA(X, Y, Z, p_out_ga(X, P)) → U3_GAA(X, Y, Z, P, f_in_gaa(P, Y, U))
U2_GAA(X, Y, Z, p_out_ga(X, P)) → F_IN_GAA(P, Y, U)
U3_GAA(X, Y, Z, P, f_out_gaa(P, Y, U)) → U4_GAA(X, Y, Z, f_in_gaa(U, Y, Z))
U3_GAA(X, Y, Z, P, f_out_gaa(P, Y, U)) → F_IN_GAA(U, Y, Z)

The TRS R consists of the following rules:

f_in_gaa(0, Y, Z) → U1_gaa(Y, Z, eq_in_ag(Z, 0))
eq_in_ag(X, X) → eq_out_ag(X, X)
U1_gaa(Y, Z, eq_out_ag(Z, 0)) → f_out_gaa(0, Y, Z)
f_in_gaa(X, Y, Z) → U2_gaa(X, Y, Z, p_in_ga(X, P))
p_in_ga(0, 0) → p_out_ga(0, 0)
p_in_ga(s(X), X) → p_out_ga(s(X), X)
U2_gaa(X, Y, Z, p_out_ga(X, P)) → U3_gaa(X, Y, Z, P, f_in_gaa(P, Y, U))
U3_gaa(X, Y, Z, P, f_out_gaa(P, Y, U)) → U4_gaa(X, Y, Z, f_in_gaa(U, Y, Z))
U4_gaa(X, Y, Z, f_out_gaa(U, Y, Z)) → f_out_gaa(X, Y, Z)

The argument filtering Pi contains the following mapping:
f_in_gaa(x1, x2, x3) = f_in_gaa(x1)
0 = 0
U1_gaa(x1, x2, x3) = U1_gaa(x3)
eq_in_ag(x1, x2) = eq_in_ag(x2)
eq_out_ag(x1, x2) = eq_out_ag(x1, x2)
f_out_gaa(x1, x2, x3) = f_out_gaa(x1, x3)
U2_gaa(x1, x2, x3, x4) = U2_gaa(x1, x4)
p_in_ga(x1, x2) = p_in_ga(x1)
p_out_ga(x1, x2) = p_out_ga(x1, x2)
s(x1) = s(x1)
U3_gaa(x1, x2, x3, x4, x5) = U3_gaa(x1, x5)
U4_gaa(x1, x2, x3, x4) = U4_gaa(x1, x4)
F_IN_GAA(x1, x2, x3) = F_IN_GAA(x1)
U1_GAA(x1, x2, x3) = U1_GAA(x3)
EQ_IN_AG(x1, x2) = EQ_IN_AG(x2)
U2_GAA(x1, x2, x3, x4) = U2_GAA(x1, x4)
P_IN_GA(x1, x2) = P_IN_GA(x1)
U3_GAA(x1, x2, x3, x4, x5) = U3_GAA(x1, x5)
U4_GAA(x1, x2, x3, x4) = U4_GAA(x1, x4)

We have to consider all (P,R,Pi)-chains

(34) Obligation:

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

F_IN_GAA(0, Y, Z) → U1_GAA(Y, Z, eq_in_ag(Z, 0))
F_IN_GAA(0, Y, Z) → EQ_IN_AG(Z, 0)
F_IN_GAA(X, Y, Z) → U2_GAA(X, Y, Z, p_in_ga(X, P))
F_IN_GAA(X, Y, Z) → P_IN_GA(X, P)
U2_GAA(X, Y, Z, p_out_ga(X, P)) → U3_GAA(X, Y, Z, P, f_in_gaa(P, Y, U))
U2_GAA(X, Y, Z, p_out_ga(X, P)) → F_IN_GAA(P, Y, U)
U3_GAA(X, Y, Z, P, f_out_gaa(P, Y, U)) → U4_GAA(X, Y, Z, f_in_gaa(U, Y, Z))
U3_GAA(X, Y, Z, P, f_out_gaa(P, Y, U)) → F_IN_GAA(U, Y, Z)

The TRS R consists of the following rules:

f_in_gaa(0, Y, Z) → U1_gaa(Y, Z, eq_in_ag(Z, 0))
eq_in_ag(X, X) → eq_out_ag(X, X)
U1_gaa(Y, Z, eq_out_ag(Z, 0)) → f_out_gaa(0, Y, Z)
f_in_gaa(X, Y, Z) → U2_gaa(X, Y, Z, p_in_ga(X, P))
p_in_ga(0, 0) → p_out_ga(0, 0)
p_in_ga(s(X), X) → p_out_ga(s(X), X)
U2_gaa(X, Y, Z, p_out_ga(X, P)) → U3_gaa(X, Y, Z, P, f_in_gaa(P, Y, U))
U3_gaa(X, Y, Z, P, f_out_gaa(P, Y, U)) → U4_gaa(X, Y, Z, f_in_gaa(U, Y, Z))
U4_gaa(X, Y, Z, f_out_gaa(U, Y, Z)) → f_out_gaa(X, Y, Z)

The argument filtering Pi contains the following mapping:
f_in_gaa(x1, x2, x3) = f_in_gaa(x1)
0 = 0
U1_gaa(x1, x2, x3) = U1_gaa(x3)
eq_in_ag(x1, x2) = eq_in_ag(x2)
eq_out_ag(x1, x2) = eq_out_ag(x1, x2)
f_out_gaa(x1, x2, x3) = f_out_gaa(x1, x3)
U2_gaa(x1, x2, x3, x4) = U2_gaa(x1, x4)
p_in_ga(x1, x2) = p_in_ga(x1)
p_out_ga(x1, x2) = p_out_ga(x1, x2)
s(x1) = s(x1)
U3_gaa(x1, x2, x3, x4, x5) = U3_gaa(x1, x5)
U4_gaa(x1, x2, x3, x4) = U4_gaa(x1, x4)
F_IN_GAA(x1, x2, x3) = F_IN_GAA(x1)
U1_GAA(x1, x2, x3) = U1_GAA(x3)
EQ_IN_AG(x1, x2) = EQ_IN_AG(x2)
U2_GAA(x1, x2, x3, x4) = U2_GAA(x1, x4)
P_IN_GA(x1, x2) = P_IN_GA(x1)
U3_GAA(x1, x2, x3, x4, x5) = U3_GAA(x1, x5)
U4_GAA(x1, x2, x3, x4) = U4_GAA(x1, x4)

We have to consider all (P,R,Pi)-chains

(35) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 1 SCC with 4 less nodes.

(36) Obligation:

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

F_IN_GAA(X, Y, Z) → U2_GAA(X, Y, Z, p_in_ga(X, P))
U2_GAA(X, Y, Z, p_out_ga(X, P)) → U3_GAA(X, Y, Z, P, f_in_gaa(P, Y, U))
U3_GAA(X, Y, Z, P, f_out_gaa(P, Y, U)) → F_IN_GAA(U, Y, Z)
U2_GAA(X, Y, Z, p_out_ga(X, P)) → F_IN_GAA(P, Y, U)

The TRS R consists of the following rules:

f_in_gaa(0, Y, Z) → U1_gaa(Y, Z, eq_in_ag(Z, 0))
eq_in_ag(X, X) → eq_out_ag(X, X)
U1_gaa(Y, Z, eq_out_ag(Z, 0)) → f_out_gaa(0, Y, Z)
f_in_gaa(X, Y, Z) → U2_gaa(X, Y, Z, p_in_ga(X, P))
p_in_ga(0, 0) → p_out_ga(0, 0)
p_in_ga(s(X), X) → p_out_ga(s(X), X)
U2_gaa(X, Y, Z, p_out_ga(X, P)) → U3_gaa(X, Y, Z, P, f_in_gaa(P, Y, U))
U3_gaa(X, Y, Z, P, f_out_gaa(P, Y, U)) → U4_gaa(X, Y, Z, f_in_gaa(U, Y, Z))
U4_gaa(X, Y, Z, f_out_gaa(U, Y, Z)) → f_out_gaa(X, Y, Z)

The argument filtering Pi contains the following mapping:
f_in_gaa(x1, x2, x3) = f_in_gaa(x1)
0 = 0
U1_gaa(x1, x2, x3) = U1_gaa(x3)
eq_in_ag(x1, x2) = eq_in_ag(x2)
eq_out_ag(x1, x2) = eq_out_ag(x1, x2)
f_out_gaa(x1, x2, x3) = f_out_gaa(x1, x3)
U2_gaa(x1, x2, x3, x4) = U2_gaa(x1, x4)
p_in_ga(x1, x2) = p_in_ga(x1)
p_out_ga(x1, x2) = p_out_ga(x1, x2)
s(x1) = s(x1)
U3_gaa(x1, x2, x3, x4, x5) = U3_gaa(x1, x5)
U4_gaa(x1, x2, x3, x4) = U4_gaa(x1, x4)
F_IN_GAA(x1, x2, x3) = F_IN_GAA(x1)
U2_GAA(x1, x2, x3, x4) = U2_GAA(x1, x4)
U3_GAA(x1, x2, x3, x4, x5) = U3_GAA(x1, x5)

We have to consider all (P,R,Pi)-chains

(37) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(38) Obligation:

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

F_IN_GAA(X) → U2_GAA(X, p_in_ga(X))
U2_GAA(X, p_out_ga(X, P)) → U3_GAA(X, f_in_gaa(P))
U3_GAA(X, f_out_gaa(P, U)) → F_IN_GAA(U)
U2_GAA(X, p_out_ga(X, P)) → F_IN_GAA(P)

The TRS R consists of the following rules:

f_in_gaa(0) → U1_gaa(eq_in_ag(0))
eq_in_ag(X) → eq_out_ag(X, X)
U1_gaa(eq_out_ag(Z, 0)) → f_out_gaa(0, Z)
f_in_gaa(X) → U2_gaa(X, p_in_ga(X))
p_in_ga(0) → p_out_ga(0, 0)
p_in_ga(s(X)) → p_out_ga(s(X), X)
U2_gaa(X, p_out_ga(X, P)) → U3_gaa(X, f_in_gaa(P))
U3_gaa(X, f_out_gaa(P, U)) → U4_gaa(X, f_in_gaa(U))
U4_gaa(X, f_out_gaa(U, Z)) → f_out_gaa(X, Z)

The set Q consists of the following terms:

f_in_gaa(x0)
eq_in_ag(x0)
U1_gaa(x0)
p_in_ga(x0)
U2_gaa(x0, x1)
U3_gaa(x0, x1)
U4_gaa(x0, x1)

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

(39) Narrowing (SOUND transformation)

By narrowing [LPAR04] the rule F_IN_GAA(X) → U2_GAA(X, p_in_ga(X)) at position [1] we obtained the following new rules [LPAR04]:

F_IN_GAA(0) → U2_GAA(0, p_out_ga(0, 0))
F_IN_GAA(s(x0)) → U2_GAA(s(x0), p_out_ga(s(x0), x0))

(40) Obligation:

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

U2_GAA(X, p_out_ga(X, P)) → U3_GAA(X, f_in_gaa(P))
U3_GAA(X, f_out_gaa(P, U)) → F_IN_GAA(U)
U2_GAA(X, p_out_ga(X, P)) → F_IN_GAA(P)
F_IN_GAA(0) → U2_GAA(0, p_out_ga(0, 0))
F_IN_GAA(s(x0)) → U2_GAA(s(x0), p_out_ga(s(x0), x0))

The TRS R consists of the following rules:

f_in_gaa(0) → U1_gaa(eq_in_ag(0))
eq_in_ag(X) → eq_out_ag(X, X)
U1_gaa(eq_out_ag(Z, 0)) → f_out_gaa(0, Z)
f_in_gaa(X) → U2_gaa(X, p_in_ga(X))
p_in_ga(0) → p_out_ga(0, 0)
p_in_ga(s(X)) → p_out_ga(s(X), X)
U2_gaa(X, p_out_ga(X, P)) → U3_gaa(X, f_in_gaa(P))
U3_gaa(X, f_out_gaa(P, U)) → U4_gaa(X, f_in_gaa(U))
U4_gaa(X, f_out_gaa(U, Z)) → f_out_gaa(X, Z)

The set Q consists of the following terms:

f_in_gaa(x0)
eq_in_ag(x0)
U1_gaa(x0)
p_in_ga(x0)
U2_gaa(x0, x1)
U3_gaa(x0, x1)
U4_gaa(x0, x1)

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

(41) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule U2_GAA(X, p_out_ga(X, P)) → U3_GAA(X, f_in_gaa(P)) we obtained the following new rules [LPAR04]:

U2_GAA(0, p_out_ga(0, 0)) → U3_GAA(0, f_in_gaa(0))
U2_GAA(s(z0), p_out_ga(s(z0), z0)) → U3_GAA(s(z0), f_in_gaa(z0))

(42) Obligation:

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

U3_GAA(X, f_out_gaa(P, U)) → F_IN_GAA(U)
U2_GAA(X, p_out_ga(X, P)) → F_IN_GAA(P)
F_IN_GAA(0) → U2_GAA(0, p_out_ga(0, 0))
F_IN_GAA(s(x0)) → U2_GAA(s(x0), p_out_ga(s(x0), x0))
U2_GAA(0, p_out_ga(0, 0)) → U3_GAA(0, f_in_gaa(0))
U2_GAA(s(z0), p_out_ga(s(z0), z0)) → U3_GAA(s(z0), f_in_gaa(z0))

The TRS R consists of the following rules:

f_in_gaa(0) → U1_gaa(eq_in_ag(0))
eq_in_ag(X) → eq_out_ag(X, X)
U1_gaa(eq_out_ag(Z, 0)) → f_out_gaa(0, Z)
f_in_gaa(X) → U2_gaa(X, p_in_ga(X))
p_in_ga(0) → p_out_ga(0, 0)
p_in_ga(s(X)) → p_out_ga(s(X), X)
U2_gaa(X, p_out_ga(X, P)) → U3_gaa(X, f_in_gaa(P))
U3_gaa(X, f_out_gaa(P, U)) → U4_gaa(X, f_in_gaa(U))
U4_gaa(X, f_out_gaa(U, Z)) → f_out_gaa(X, Z)

The set Q consists of the following terms:

f_in_gaa(x0)
eq_in_ag(x0)
U1_gaa(x0)
p_in_ga(x0)
U2_gaa(x0, x1)
U3_gaa(x0, x1)
U4_gaa(x0, x1)

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

(43) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule U2_GAA(X, p_out_ga(X, P)) → F_IN_GAA(P) we obtained the following new rules [LPAR04]:

U2_GAA(0, p_out_ga(0, 0)) → F_IN_GAA(0)
U2_GAA(s(z0), p_out_ga(s(z0), z0)) → F_IN_GAA(z0)

(44) Obligation:

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

U3_GAA(X, f_out_gaa(P, U)) → F_IN_GAA(U)
F_IN_GAA(0) → U2_GAA(0, p_out_ga(0, 0))
F_IN_GAA(s(x0)) → U2_GAA(s(x0), p_out_ga(s(x0), x0))
U2_GAA(0, p_out_ga(0, 0)) → U3_GAA(0, f_in_gaa(0))
U2_GAA(s(z0), p_out_ga(s(z0), z0)) → U3_GAA(s(z0), f_in_gaa(z0))
U2_GAA(0, p_out_ga(0, 0)) → F_IN_GAA(0)
U2_GAA(s(z0), p_out_ga(s(z0), z0)) → F_IN_GAA(z0)

The TRS R consists of the following rules:

f_in_gaa(0) → U1_gaa(eq_in_ag(0))
eq_in_ag(X) → eq_out_ag(X, X)
U1_gaa(eq_out_ag(Z, 0)) → f_out_gaa(0, Z)
f_in_gaa(X) → U2_gaa(X, p_in_ga(X))
p_in_ga(0) → p_out_ga(0, 0)
p_in_ga(s(X)) → p_out_ga(s(X), X)
U2_gaa(X, p_out_ga(X, P)) → U3_gaa(X, f_in_gaa(P))
U3_gaa(X, f_out_gaa(P, U)) → U4_gaa(X, f_in_gaa(U))
U4_gaa(X, f_out_gaa(U, Z)) → f_out_gaa(X, Z)

The set Q consists of the following terms:

f_in_gaa(x0)
eq_in_ag(x0)
U1_gaa(x0)
p_in_ga(x0)
U2_gaa(x0, x1)
U3_gaa(x0, x1)
U4_gaa(x0, x1)

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

(45) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

F_IN_GAA(s(x0)) → U2_GAA(s(x0), p_out_ga(s(x0), x0))

The remaining pairs can at least be oriented weakly.
Used ordering: Matrix interpretation [MATRO]:

POL(U3_GAA(x₁, x₂)) = 0 +
[ 0, 1 ]

· x₁ +
[ 0, 1 ]

· x₂

POL(f_out_gaa(x₁, x₂)) =
/ 0 \

\ 0 /

+
/ 0 0 \

\ 0 0 /

· x₁ +
/ 0 0 \

\ 1 0 /

· x₂

POL(F_IN_GAA(x₁)) = 0 +
[ 1, 0 ]

· x₁

POL(0) =
/ 0 \

\ 0 /

POL(U2_GAA(x₁, x₂)) = 0 +
[ 0, 0 ]

· x₁ +
[ 0, 1 ]

· x₂

POL(p_out_ga(x₁, x₂)) =
/ 0 \

\ 0 /

+
/ 1 0 \

\ 0 0 /

· x₁ +
/ 1 0 \

\ 1 0 /

· x₂

POL(s(x₁)) =
/ 1 \

\ 0 /

+
/ 1 0 \

\ 0 0 /

· x₁

POL(f_in_gaa(x₁)) =
/ 1 \

\ 0 /

+
/ 1 1 \

\ 0 0 /

· x₁

POL(U1_gaa(x₁)) =
/ 0 \

\ 0 /

+
/ 0 0 \

\ 1 0 /

· x₁

POL(eq_in_ag(x₁)) =
/ 0 \

\ 0 /

+
/ 1 0 \

\ 1 1 /

· x₁

POL(U2_gaa(x₁, x₂)) =
/ 0 \

\ 0 /

+
/ 0 1 \

\ 0 0 /

· x₁ +
/ 0 0 \

\ 0 0 /

· x₂

POL(p_in_ga(x₁)) =
/ 0 \

\ 0 /

+
/ 0 0 \

\ 0 0 /

· x₁

POL(U3_gaa(x₁, x₂)) =
/ 0 \

\ 0 /

+
/ 0 1 \

\ 0 0 /

· x₁ +
/ 0 0 \

\ 0 0 /

· x₂

POL(U4_gaa(x₁, x₂)) =
/ 0 \

\ 0 /

+
/ 0 1 \

\ 0 0 /

· x₁ +
/ 0 1 \

\ 0 1 /

· x₂

POL(eq_out_ag(x₁, x₂)) =
/ 0 \

\ 0 /

+
/ 1 0 \

\ 0 0 /

· x₁ +
/ 0 0 \

\ 0 0 /

· x₂

The following usable rules [FROCOS05] were oriented:

f_in_gaa(0) → U1_gaa(eq_in_ag(0))
f_in_gaa(X) → U2_gaa(X, p_in_ga(X))
U2_gaa(X, p_out_ga(X, P)) → U3_gaa(X, f_in_gaa(P))
U3_gaa(X, f_out_gaa(P, U)) → U4_gaa(X, f_in_gaa(U))
U4_gaa(X, f_out_gaa(U, Z)) → f_out_gaa(X, Z)
eq_in_ag(X) → eq_out_ag(X, X)
U1_gaa(eq_out_ag(Z, 0)) → f_out_gaa(0, Z)

(46) Obligation:

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

U3_GAA(X, f_out_gaa(P, U)) → F_IN_GAA(U)
F_IN_GAA(0) → U2_GAA(0, p_out_ga(0, 0))
U2_GAA(0, p_out_ga(0, 0)) → U3_GAA(0, f_in_gaa(0))
U2_GAA(s(z0), p_out_ga(s(z0), z0)) → U3_GAA(s(z0), f_in_gaa(z0))
U2_GAA(0, p_out_ga(0, 0)) → F_IN_GAA(0)
U2_GAA(s(z0), p_out_ga(s(z0), z0)) → F_IN_GAA(z0)

The TRS R consists of the following rules:

f_in_gaa(0) → U1_gaa(eq_in_ag(0))
eq_in_ag(X) → eq_out_ag(X, X)
U1_gaa(eq_out_ag(Z, 0)) → f_out_gaa(0, Z)
f_in_gaa(X) → U2_gaa(X, p_in_ga(X))
p_in_ga(0) → p_out_ga(0, 0)
p_in_ga(s(X)) → p_out_ga(s(X), X)
U2_gaa(X, p_out_ga(X, P)) → U3_gaa(X, f_in_gaa(P))
U3_gaa(X, f_out_gaa(P, U)) → U4_gaa(X, f_in_gaa(U))
U4_gaa(X, f_out_gaa(U, Z)) → f_out_gaa(X, Z)

The set Q consists of the following terms:

f_in_gaa(x0)
eq_in_ag(x0)
U1_gaa(x0)
p_in_ga(x0)
U2_gaa(x0, x1)
U3_gaa(x0, x1)
U4_gaa(x0, x1)

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

(47) DependencyGraphProof (EQUIVALENT transformation)

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

(48) Obligation:

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

F_IN_GAA(0) → U2_GAA(0, p_out_ga(0, 0))
U2_GAA(0, p_out_ga(0, 0)) → U3_GAA(0, f_in_gaa(0))
U3_GAA(X, f_out_gaa(P, U)) → F_IN_GAA(U)
U2_GAA(0, p_out_ga(0, 0)) → F_IN_GAA(0)

The TRS R consists of the following rules:

f_in_gaa(0) → U1_gaa(eq_in_ag(0))
eq_in_ag(X) → eq_out_ag(X, X)
U1_gaa(eq_out_ag(Z, 0)) → f_out_gaa(0, Z)
f_in_gaa(X) → U2_gaa(X, p_in_ga(X))
p_in_ga(0) → p_out_ga(0, 0)
p_in_ga(s(X)) → p_out_ga(s(X), X)
U2_gaa(X, p_out_ga(X, P)) → U3_gaa(X, f_in_gaa(P))
U3_gaa(X, f_out_gaa(P, U)) → U4_gaa(X, f_in_gaa(U))
U4_gaa(X, f_out_gaa(U, Z)) → f_out_gaa(X, Z)

The set Q consists of the following terms:

f_in_gaa(x0)
eq_in_ag(x0)
U1_gaa(x0)
p_in_ga(x0)
U2_gaa(x0, x1)
U3_gaa(x0, x1)
U4_gaa(x0, x1)

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

(49) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule U3_GAA(X, f_out_gaa(P, U)) → F_IN_GAA(U) we obtained the following new rules [LPAR04]:

U3_GAA(0, f_out_gaa(x1, x2)) → F_IN_GAA(x2)

(50) Obligation:

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

F_IN_GAA(0) → U2_GAA(0, p_out_ga(0, 0))
U2_GAA(0, p_out_ga(0, 0)) → U3_GAA(0, f_in_gaa(0))
U2_GAA(0, p_out_ga(0, 0)) → F_IN_GAA(0)
U3_GAA(0, f_out_gaa(x1, x2)) → F_IN_GAA(x2)

The TRS R consists of the following rules:

f_in_gaa(0) → U1_gaa(eq_in_ag(0))
eq_in_ag(X) → eq_out_ag(X, X)
U1_gaa(eq_out_ag(Z, 0)) → f_out_gaa(0, Z)
f_in_gaa(X) → U2_gaa(X, p_in_ga(X))
p_in_ga(0) → p_out_ga(0, 0)
p_in_ga(s(X)) → p_out_ga(s(X), X)
U2_gaa(X, p_out_ga(X, P)) → U3_gaa(X, f_in_gaa(P))
U3_gaa(X, f_out_gaa(P, U)) → U4_gaa(X, f_in_gaa(U))
U4_gaa(X, f_out_gaa(U, Z)) → f_out_gaa(X, Z)

The set Q consists of the following terms:

f_in_gaa(x0)
eq_in_ag(x0)
U1_gaa(x0)
p_in_ga(x0)
U2_gaa(x0, x1)
U3_gaa(x0, x1)
U4_gaa(x0, x1)

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

(51) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule U3_GAA(X, f_out_gaa(P, U)) → F_IN_GAA(U) we obtained the following new rules [LPAR04]:

U3_GAA(0, f_out_gaa(x1, x2)) → F_IN_GAA(x2)

(52) Obligation:

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

F_IN_GAA(0) → U2_GAA(0, p_out_ga(0, 0))
U2_GAA(0, p_out_ga(0, 0)) → U3_GAA(0, f_in_gaa(0))
U2_GAA(0, p_out_ga(0, 0)) → F_IN_GAA(0)
U3_GAA(0, f_out_gaa(x1, x2)) → F_IN_GAA(x2)

The TRS R consists of the following rules:

f_in_gaa(0) → U1_gaa(eq_in_ag(0))
eq_in_ag(X) → eq_out_ag(X, X)
U1_gaa(eq_out_ag(Z, 0)) → f_out_gaa(0, Z)
f_in_gaa(X) → U2_gaa(X, p_in_ga(X))
p_in_ga(0) → p_out_ga(0, 0)
p_in_ga(s(X)) → p_out_ga(s(X), X)
U2_gaa(X, p_out_ga(X, P)) → U3_gaa(X, f_in_gaa(P))
U3_gaa(X, f_out_gaa(P, U)) → U4_gaa(X, f_in_gaa(U))
U4_gaa(X, f_out_gaa(U, Z)) → f_out_gaa(X, Z)

The set Q consists of the following terms:

f_in_gaa(x0)
eq_in_ag(x0)
U1_gaa(x0)
p_in_ga(x0)
U2_gaa(x0, x1)
U3_gaa(x0, x1)
U4_gaa(x0, x1)

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

(53) Narrowing (SOUND transformation)

By narrowing [LPAR04] the rule U2_GAA(0, p_out_ga(0, 0)) → U3_GAA(0, f_in_gaa(0)) at position [1] we obtained the following new rules [LPAR04]:

U2_GAA(0, p_out_ga(0, 0)) → U3_GAA(0, U1_gaa(eq_in_ag(0)))
U2_GAA(0, p_out_ga(0, 0)) → U3_GAA(0, U2_gaa(0, p_in_ga(0)))

(54) Obligation:

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

F_IN_GAA(0) → U2_GAA(0, p_out_ga(0, 0))
U2_GAA(0, p_out_ga(0, 0)) → F_IN_GAA(0)
U3_GAA(0, f_out_gaa(x1, x2)) → F_IN_GAA(x2)
U2_GAA(0, p_out_ga(0, 0)) → U3_GAA(0, U1_gaa(eq_in_ag(0)))
U2_GAA(0, p_out_ga(0, 0)) → U3_GAA(0, U2_gaa(0, p_in_ga(0)))

The TRS R consists of the following rules:

f_in_gaa(0) → U1_gaa(eq_in_ag(0))
eq_in_ag(X) → eq_out_ag(X, X)
U1_gaa(eq_out_ag(Z, 0)) → f_out_gaa(0, Z)
f_in_gaa(X) → U2_gaa(X, p_in_ga(X))
p_in_ga(0) → p_out_ga(0, 0)
p_in_ga(s(X)) → p_out_ga(s(X), X)
U2_gaa(X, p_out_ga(X, P)) → U3_gaa(X, f_in_gaa(P))
U3_gaa(X, f_out_gaa(P, U)) → U4_gaa(X, f_in_gaa(U))
U4_gaa(X, f_out_gaa(U, Z)) → f_out_gaa(X, Z)

The set Q consists of the following terms:

f_in_gaa(x0)
eq_in_ag(x0)
U1_gaa(x0)
p_in_ga(x0)
U2_gaa(x0, x1)
U3_gaa(x0, x1)
U4_gaa(x0, x1)

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

(55) Rewriting (EQUIVALENT transformation)

By rewriting [LPAR04] the rule U2_GAA(0, p_out_ga(0, 0)) → U3_GAA(0, U1_gaa(eq_in_ag(0))) at position [1,0] we obtained the following new rules [LPAR04]:

U2_GAA(0, p_out_ga(0, 0)) → U3_GAA(0, U1_gaa(eq_out_ag(0, 0)))

(56) Obligation:

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

F_IN_GAA(0) → U2_GAA(0, p_out_ga(0, 0))
U2_GAA(0, p_out_ga(0, 0)) → F_IN_GAA(0)
U3_GAA(0, f_out_gaa(x1, x2)) → F_IN_GAA(x2)
U2_GAA(0, p_out_ga(0, 0)) → U3_GAA(0, U2_gaa(0, p_in_ga(0)))
U2_GAA(0, p_out_ga(0, 0)) → U3_GAA(0, U1_gaa(eq_out_ag(0, 0)))

The TRS R consists of the following rules:

f_in_gaa(0) → U1_gaa(eq_in_ag(0))
eq_in_ag(X) → eq_out_ag(X, X)
U1_gaa(eq_out_ag(Z, 0)) → f_out_gaa(0, Z)
f_in_gaa(X) → U2_gaa(X, p_in_ga(X))
p_in_ga(0) → p_out_ga(0, 0)
p_in_ga(s(X)) → p_out_ga(s(X), X)
U2_gaa(X, p_out_ga(X, P)) → U3_gaa(X, f_in_gaa(P))
U3_gaa(X, f_out_gaa(P, U)) → U4_gaa(X, f_in_gaa(U))
U4_gaa(X, f_out_gaa(U, Z)) → f_out_gaa(X, Z)

The set Q consists of the following terms:

f_in_gaa(x0)
eq_in_ag(x0)
U1_gaa(x0)
p_in_ga(x0)
U2_gaa(x0, x1)
U3_gaa(x0, x1)
U4_gaa(x0, x1)

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

(57) Rewriting (EQUIVALENT transformation)

By rewriting [LPAR04] the rule U2_GAA(0, p_out_ga(0, 0)) → U3_GAA(0, U2_gaa(0, p_in_ga(0))) at position [1,1] we obtained the following new rules [LPAR04]:

U2_GAA(0, p_out_ga(0, 0)) → U3_GAA(0, U2_gaa(0, p_out_ga(0, 0)))

(58) Obligation:

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

F_IN_GAA(0) → U2_GAA(0, p_out_ga(0, 0))
U2_GAA(0, p_out_ga(0, 0)) → F_IN_GAA(0)
U3_GAA(0, f_out_gaa(x1, x2)) → F_IN_GAA(x2)
U2_GAA(0, p_out_ga(0, 0)) → U3_GAA(0, U1_gaa(eq_out_ag(0, 0)))
U2_GAA(0, p_out_ga(0, 0)) → U3_GAA(0, U2_gaa(0, p_out_ga(0, 0)))

The TRS R consists of the following rules:

f_in_gaa(0) → U1_gaa(eq_in_ag(0))
eq_in_ag(X) → eq_out_ag(X, X)
U1_gaa(eq_out_ag(Z, 0)) → f_out_gaa(0, Z)
f_in_gaa(X) → U2_gaa(X, p_in_ga(X))
p_in_ga(0) → p_out_ga(0, 0)
p_in_ga(s(X)) → p_out_ga(s(X), X)
U2_gaa(X, p_out_ga(X, P)) → U3_gaa(X, f_in_gaa(P))
U3_gaa(X, f_out_gaa(P, U)) → U4_gaa(X, f_in_gaa(U))
U4_gaa(X, f_out_gaa(U, Z)) → f_out_gaa(X, Z)

The set Q consists of the following terms:

f_in_gaa(x0)
eq_in_ag(x0)
U1_gaa(x0)
p_in_ga(x0)
U2_gaa(x0, x1)
U3_gaa(x0, x1)
U4_gaa(x0, x1)

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

(59) Rewriting (EQUIVALENT transformation)

By rewriting [LPAR04] the rule U2_GAA(0, p_out_ga(0, 0)) → U3_GAA(0, U1_gaa(eq_out_ag(0, 0))) at position [1] we obtained the following new rules [LPAR04]:

U2_GAA(0, p_out_ga(0, 0)) → U3_GAA(0, f_out_gaa(0, 0))

(60) Obligation:

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

F_IN_GAA(0) → U2_GAA(0, p_out_ga(0, 0))
U2_GAA(0, p_out_ga(0, 0)) → F_IN_GAA(0)
U3_GAA(0, f_out_gaa(x1, x2)) → F_IN_GAA(x2)
U2_GAA(0, p_out_ga(0, 0)) → U3_GAA(0, U2_gaa(0, p_out_ga(0, 0)))
U2_GAA(0, p_out_ga(0, 0)) → U3_GAA(0, f_out_gaa(0, 0))

The TRS R consists of the following rules:

f_in_gaa(0) → U1_gaa(eq_in_ag(0))
eq_in_ag(X) → eq_out_ag(X, X)
U1_gaa(eq_out_ag(Z, 0)) → f_out_gaa(0, Z)
f_in_gaa(X) → U2_gaa(X, p_in_ga(X))
p_in_ga(0) → p_out_ga(0, 0)
p_in_ga(s(X)) → p_out_ga(s(X), X)
U2_gaa(X, p_out_ga(X, P)) → U3_gaa(X, f_in_gaa(P))
U3_gaa(X, f_out_gaa(P, U)) → U4_gaa(X, f_in_gaa(U))
U4_gaa(X, f_out_gaa(U, Z)) → f_out_gaa(X, Z)

The set Q consists of the following terms:

f_in_gaa(x0)
eq_in_ag(x0)
U1_gaa(x0)
p_in_ga(x0)
U2_gaa(x0, x1)
U3_gaa(x0, x1)
U4_gaa(x0, x1)

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

(61) ForwardInstantiation (EQUIVALENT transformation)

By forward instantiating [JAR06] the rule U3_GAA(0, f_out_gaa(x1, x2)) → F_IN_GAA(x2) we obtained the following new rules [LPAR04]:

U3_GAA(0, f_out_gaa(x0, 0)) → F_IN_GAA(0)

(62) Obligation:

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

F_IN_GAA(0) → U2_GAA(0, p_out_ga(0, 0))
U2_GAA(0, p_out_ga(0, 0)) → F_IN_GAA(0)
U2_GAA(0, p_out_ga(0, 0)) → U3_GAA(0, U2_gaa(0, p_out_ga(0, 0)))
U2_GAA(0, p_out_ga(0, 0)) → U3_GAA(0, f_out_gaa(0, 0))
U3_GAA(0, f_out_gaa(x0, 0)) → F_IN_GAA(0)

The TRS R consists of the following rules:

f_in_gaa(0) → U1_gaa(eq_in_ag(0))
eq_in_ag(X) → eq_out_ag(X, X)
U1_gaa(eq_out_ag(Z, 0)) → f_out_gaa(0, Z)
f_in_gaa(X) → U2_gaa(X, p_in_ga(X))
p_in_ga(0) → p_out_ga(0, 0)
p_in_ga(s(X)) → p_out_ga(s(X), X)
U2_gaa(X, p_out_ga(X, P)) → U3_gaa(X, f_in_gaa(P))
U3_gaa(X, f_out_gaa(P, U)) → U4_gaa(X, f_in_gaa(U))
U4_gaa(X, f_out_gaa(U, Z)) → f_out_gaa(X, Z)

The set Q consists of the following terms:

f_in_gaa(x0)
eq_in_ag(x0)
U1_gaa(x0)
p_in_ga(x0)
U2_gaa(x0, x1)
U3_gaa(x0, x1)
U4_gaa(x0, x1)

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

(63) NonTerminationProof (EQUIVALENT 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 = U2_GAA(0, p_out_ga(0, 0)) evaluates to t =U2_GAA(0, p_out_ga(0, 0))

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:

Matcher: [ ]
Semiunifier: [ ]

Rewriting sequence

U2_GAA(0, p_out_ga(0, 0)) → F_IN_GAA(0)
with rule U2_GAA(0, p_out_ga(0, 0)) → F_IN_GAA(0) at position [] and matcher [ ]

F_IN_GAA(0) → U2_GAA(0, p_out_ga(0, 0))
with rule F_IN_GAA(0) → U2_GAA(0, p_out_ga(0, 0))

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.

(0) Obligation:

(1) CutEliminatorProof (SOUND transformation)

(2) Obligation:

(3) PrologToPiTRSProof (SOUND transformation)

(4) Obligation:

(5) DependencyPairsProof (EQUIVALENT transformation)

(6) Obligation:

(7) DependencyGraphProof (EQUIVALENT transformation)

(8) Obligation:

(9) PiDPToQDPProof (SOUND transformation)

(10) Obligation:

(11) UsableRulesReductionPairsProof (EQUIVALENT transformation)

(12) Obligation:

(13) Narrowing (SOUND transformation)

(14) Obligation:

(15) Instantiation (EQUIVALENT transformation)

(16) Obligation:

(17) Instantiation (EQUIVALENT transformation)

(18) Obligation:

(19) Narrowing (SOUND transformation)

(20) Obligation:

(21) Rewriting (EQUIVALENT transformation)

(22) Obligation:

(23) Rewriting (EQUIVALENT transformation)

(24) Obligation:

(25) Rewriting (EQUIVALENT transformation)

(26) Obligation:

(27) ForwardInstantiation (EQUIVALENT transformation)

(28) Obligation:

(29) NonTerminationProof (EQUIVALENT transformation)

(30) FALSE

(31) PrologToPiTRSProof (SOUND transformation)

(32) Obligation:

(33) DependencyPairsProof (EQUIVALENT transformation)

(34) Obligation:

(35) DependencyGraphProof (EQUIVALENT transformation)

(36) Obligation:

(37) PiDPToQDPProof (SOUND transformation)

(38) Obligation:

(39) Narrowing (SOUND transformation)

(40) Obligation:

(41) Instantiation (EQUIVALENT transformation)

(42) Obligation:

(43) Instantiation (EQUIVALENT transformation)

(44) Obligation:

(45) QDPOrderProof (EQUIVALENT transformation)

(46) Obligation:

(47) DependencyGraphProof (EQUIVALENT transformation)

(48) Obligation:

(49) Instantiation (EQUIVALENT transformation)

(50) Obligation:

(51) Instantiation (EQUIVALENT transformation)

(52) Obligation:

(53) Narrowing (SOUND transformation)

(54) Obligation:

(55) Rewriting (EQUIVALENT transformation)

(56) Obligation:

(57) Rewriting (EQUIVALENT transformation)

(58) Obligation:

(59) Rewriting (EQUIVALENT transformation)

(60) Obligation:

(61) ForwardInstantiation (EQUIVALENT transformation)

(62) Obligation:

(63) NonTerminationProof (EQUIVALENT transformation)

(64) FALSE