Left Termination of the query pattern append_in_3(g, a, a) w.r.t. the given Prolog program could successfully be proven:

0 Prolog
↳1 CutEliminatorProof (⇐)
↳2 Prolog
  ↳3 PrologToPiTRSProof (⇐)
    ↳4 PiTRS
    ↳5 DependencyPairsProof (⇔)
    ↳6 PiDP
    ↳7 DependencyGraphProof (⇔)
    ↳8 PiDP
    ↳9 UsableRulesProof (⇔)
    ↳10 PiDP
    ↳11 PiDPToQDPProof (⇐)
    ↳12 QDP
  ↳13 PrologToPiTRSProof (⇐)
    ↳14 PiTRS
    ↳15 DependencyPairsProof (⇔)
    ↳16 PiDP
    ↳17 DependencyGraphProof (⇔)
    ↳18 PiDP
    ↳19 UsableRulesProof (⇔)
    ↳20 PiDP
    ↳21 PiDPToQDPProof (⇐)
    ↳22 QDP
    ↳23 UsableRulesReductionPairsProof (⇔)
    ↳24 QDP
    ↳25 DependencyGraphProof (⇔)
    ↳26 TRUE

(0) Obligation:

Clauses:

append(X, Y, Z) :- ','(=(X, []), ','(!, =(Y, Z))).
append(X, Y, Z) :- ','(=(X, .(H, Xs)), ','(!, ','(=(Z, .(H, Zs)), append(Xs, Y, Zs)))).
=(X, X).

Queries:

append(g,a,a).

(1) CutEliminatorProof (SOUND transformation)

Eliminated all cuts by simply ignoring them[PROLOG].

(2) Obligation:

Clauses:

append(X, Y, Z) :- ','(=(X, []), =(Y, Z)).
append(X, Y, Z) :- ','(=(X, .(H, Xs)), ','(=(Z, .(H, Zs)), append(Xs, Y, Zs))).
=(X, X).

Queries:

append(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:
append_in: (b,f,f)
Transforming Prolog into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:

append_in_gaa(X, Y, Z) → U1_gaa(X, Y, Z, =_in_gg(X, []))
=_in_gg(X, X) → =_out_gg(X, X)
U1_gaa(X, Y, Z, =_out_gg(X, [])) → U2_gaa(X, Y, Z, =_in_aa(Y, Z))
=_in_aa(X, X) → =_out_aa(X, X)
U2_gaa(X, Y, Z, =_out_aa(Y, Z)) → append_out_gaa(X, Y, Z)
append_in_gaa(X, Y, Z) → U3_gaa(X, Y, Z, =_in_ga(X, .(H, Xs)))
=_in_ga(X, X) → =_out_ga(X, X)
U3_gaa(X, Y, Z, =_out_ga(X, .(H, Xs))) → U4_gaa(X, Y, Z, Xs, =_in_aa(Z, .(H, Zs)))
U4_gaa(X, Y, Z, Xs, =_out_aa(Z, .(H, Zs))) → U5_gaa(X, Y, Z, append_in_gaa(Xs, Y, Zs))
U5_gaa(X, Y, Z, append_out_gaa(Xs, Y, Zs)) → append_out_gaa(X, Y, Z)

The argument filtering Pi contains the following mapping:
append_in_gaa(x1, x2, x3)  =  append_in_gaa(x1)
U1_gaa(x1, x2, x3, x4)  =  U1_gaa(x1, x4)
=_in_gg(x1, x2)  =  =_in_gg(x1, x2)
=_out_gg(x1, x2)  =  =_out_gg(x1, x2)
[]  =  []
U2_gaa(x1, x2, x3, x4)  =  U2_gaa(x1, x4)
=_in_aa(x1, x2)  =  =_in_aa
=_out_aa(x1, x2)  =  =_out_aa
append_out_gaa(x1, x2, x3)  =  append_out_gaa(x1)
U3_gaa(x1, x2, x3, x4)  =  U3_gaa(x1, x4)
=_in_ga(x1, x2)  =  =_in_ga(x1)
.(x1, x2)  =  .(x2)
=_out_ga(x1, x2)  =  =_out_ga(x1, x2)
U4_gaa(x1, x2, x3, x4, x5)  =  U4_gaa(x1, x4, x5)
U5_gaa(x1, x2, x3, x4)  =  U5_gaa(x1, x4)

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog

(4) Obligation:

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

append_in_gaa(X, Y, Z) → U1_gaa(X, Y, Z, =_in_gg(X, []))
=_in_gg(X, X) → =_out_gg(X, X)
U1_gaa(X, Y, Z, =_out_gg(X, [])) → U2_gaa(X, Y, Z, =_in_aa(Y, Z))
=_in_aa(X, X) → =_out_aa(X, X)
U2_gaa(X, Y, Z, =_out_aa(Y, Z)) → append_out_gaa(X, Y, Z)
append_in_gaa(X, Y, Z) → U3_gaa(X, Y, Z, =_in_ga(X, .(H, Xs)))
=_in_ga(X, X) → =_out_ga(X, X)
U3_gaa(X, Y, Z, =_out_ga(X, .(H, Xs))) → U4_gaa(X, Y, Z, Xs, =_in_aa(Z, .(H, Zs)))
U4_gaa(X, Y, Z, Xs, =_out_aa(Z, .(H, Zs))) → U5_gaa(X, Y, Z, append_in_gaa(Xs, Y, Zs))
U5_gaa(X, Y, Z, append_out_gaa(Xs, Y, Zs)) → append_out_gaa(X, Y, Z)

The argument filtering Pi contains the following mapping:
append_in_gaa(x1, x2, x3)  =  append_in_gaa(x1)
U1_gaa(x1, x2, x3, x4)  =  U1_gaa(x1, x4)
=_in_gg(x1, x2)  =  =_in_gg(x1, x2)
=_out_gg(x1, x2)  =  =_out_gg(x1, x2)
[]  =  []
U2_gaa(x1, x2, x3, x4)  =  U2_gaa(x1, x4)
=_in_aa(x1, x2)  =  =_in_aa
=_out_aa(x1, x2)  =  =_out_aa
append_out_gaa(x1, x2, x3)  =  append_out_gaa(x1)
U3_gaa(x1, x2, x3, x4)  =  U3_gaa(x1, x4)
=_in_ga(x1, x2)  =  =_in_ga(x1)
.(x1, x2)  =  .(x2)
=_out_ga(x1, x2)  =  =_out_ga(x1, x2)
U4_gaa(x1, x2, x3, x4, x5)  =  U4_gaa(x1, x4, x5)
U5_gaa(x1, x2, x3, x4)  =  U5_gaa(x1, x4)

(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:

APPEND_IN_GAA(X, Y, Z) → U1_GAA(X, Y, Z, =_in_gg(X, []))
APPEND_IN_GAA(X, Y, Z) → =_IN_GG(X, [])
U1_GAA(X, Y, Z, =_out_gg(X, [])) → U2_GAA(X, Y, Z, =_in_aa(Y, Z))
U1_GAA(X, Y, Z, =_out_gg(X, [])) → =_IN_AA(Y, Z)
APPEND_IN_GAA(X, Y, Z) → U3_GAA(X, Y, Z, =_in_ga(X, .(H, Xs)))
APPEND_IN_GAA(X, Y, Z) → =_IN_GA(X, .(H, Xs))
U3_GAA(X, Y, Z, =_out_ga(X, .(H, Xs))) → U4_GAA(X, Y, Z, Xs, =_in_aa(Z, .(H, Zs)))
U3_GAA(X, Y, Z, =_out_ga(X, .(H, Xs))) → =_IN_AA(Z, .(H, Zs))
U4_GAA(X, Y, Z, Xs, =_out_aa(Z, .(H, Zs))) → U5_GAA(X, Y, Z, append_in_gaa(Xs, Y, Zs))
U4_GAA(X, Y, Z, Xs, =_out_aa(Z, .(H, Zs))) → APPEND_IN_GAA(Xs, Y, Zs)

The TRS R consists of the following rules:

append_in_gaa(X, Y, Z) → U1_gaa(X, Y, Z, =_in_gg(X, []))
=_in_gg(X, X) → =_out_gg(X, X)
U1_gaa(X, Y, Z, =_out_gg(X, [])) → U2_gaa(X, Y, Z, =_in_aa(Y, Z))
=_in_aa(X, X) → =_out_aa(X, X)
U2_gaa(X, Y, Z, =_out_aa(Y, Z)) → append_out_gaa(X, Y, Z)
append_in_gaa(X, Y, Z) → U3_gaa(X, Y, Z, =_in_ga(X, .(H, Xs)))
=_in_ga(X, X) → =_out_ga(X, X)
U3_gaa(X, Y, Z, =_out_ga(X, .(H, Xs))) → U4_gaa(X, Y, Z, Xs, =_in_aa(Z, .(H, Zs)))
U4_gaa(X, Y, Z, Xs, =_out_aa(Z, .(H, Zs))) → U5_gaa(X, Y, Z, append_in_gaa(Xs, Y, Zs))
U5_gaa(X, Y, Z, append_out_gaa(Xs, Y, Zs)) → append_out_gaa(X, Y, Z)

The argument filtering Pi contains the following mapping:
append_in_gaa(x1, x2, x3)  =  append_in_gaa(x1)
U1_gaa(x1, x2, x3, x4)  =  U1_gaa(x1, x4)
=_in_gg(x1, x2)  =  =_in_gg(x1, x2)
=_out_gg(x1, x2)  =  =_out_gg(x1, x2)
[]  =  []
U2_gaa(x1, x2, x3, x4)  =  U2_gaa(x1, x4)
=_in_aa(x1, x2)  =  =_in_aa
=_out_aa(x1, x2)  =  =_out_aa
append_out_gaa(x1, x2, x3)  =  append_out_gaa(x1)
U3_gaa(x1, x2, x3, x4)  =  U3_gaa(x1, x4)
=_in_ga(x1, x2)  =  =_in_ga(x1)
.(x1, x2)  =  .(x2)
=_out_ga(x1, x2)  =  =_out_ga(x1, x2)
U4_gaa(x1, x2, x3, x4, x5)  =  U4_gaa(x1, x4, x5)
U5_gaa(x1, x2, x3, x4)  =  U5_gaa(x1, x4)
APPEND_IN_GAA(x1, x2, x3)  =  APPEND_IN_GAA(x1)
U1_GAA(x1, x2, x3, x4)  =  U1_GAA(x1, x4)
=_IN_GG(x1, x2)  =  =_IN_GG(x1, x2)
U2_GAA(x1, x2, x3, x4)  =  U2_GAA(x1, x4)
=_IN_AA(x1, x2)  =  =_IN_AA
U3_GAA(x1, x2, x3, x4)  =  U3_GAA(x1, x4)
=_IN_GA(x1, x2)  =  =_IN_GA(x1)
U4_GAA(x1, x2, x3, x4, x5)  =  U4_GAA(x1, x4, x5)
U5_GAA(x1, x2, x3, x4)  =  U5_GAA(x1, x4)

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

(6) Obligation:

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

APPEND_IN_GAA(X, Y, Z) → U1_GAA(X, Y, Z, =_in_gg(X, []))
APPEND_IN_GAA(X, Y, Z) → =_IN_GG(X, [])
U1_GAA(X, Y, Z, =_out_gg(X, [])) → U2_GAA(X, Y, Z, =_in_aa(Y, Z))
U1_GAA(X, Y, Z, =_out_gg(X, [])) → =_IN_AA(Y, Z)
APPEND_IN_GAA(X, Y, Z) → U3_GAA(X, Y, Z, =_in_ga(X, .(H, Xs)))
APPEND_IN_GAA(X, Y, Z) → =_IN_GA(X, .(H, Xs))
U3_GAA(X, Y, Z, =_out_ga(X, .(H, Xs))) → U4_GAA(X, Y, Z, Xs, =_in_aa(Z, .(H, Zs)))
U3_GAA(X, Y, Z, =_out_ga(X, .(H, Xs))) → =_IN_AA(Z, .(H, Zs))
U4_GAA(X, Y, Z, Xs, =_out_aa(Z, .(H, Zs))) → U5_GAA(X, Y, Z, append_in_gaa(Xs, Y, Zs))
U4_GAA(X, Y, Z, Xs, =_out_aa(Z, .(H, Zs))) → APPEND_IN_GAA(Xs, Y, Zs)

The TRS R consists of the following rules:

append_in_gaa(X, Y, Z) → U1_gaa(X, Y, Z, =_in_gg(X, []))
=_in_gg(X, X) → =_out_gg(X, X)
U1_gaa(X, Y, Z, =_out_gg(X, [])) → U2_gaa(X, Y, Z, =_in_aa(Y, Z))
=_in_aa(X, X) → =_out_aa(X, X)
U2_gaa(X, Y, Z, =_out_aa(Y, Z)) → append_out_gaa(X, Y, Z)
append_in_gaa(X, Y, Z) → U3_gaa(X, Y, Z, =_in_ga(X, .(H, Xs)))
=_in_ga(X, X) → =_out_ga(X, X)
U3_gaa(X, Y, Z, =_out_ga(X, .(H, Xs))) → U4_gaa(X, Y, Z, Xs, =_in_aa(Z, .(H, Zs)))
U4_gaa(X, Y, Z, Xs, =_out_aa(Z, .(H, Zs))) → U5_gaa(X, Y, Z, append_in_gaa(Xs, Y, Zs))
U5_gaa(X, Y, Z, append_out_gaa(Xs, Y, Zs)) → append_out_gaa(X, Y, Z)

The argument filtering Pi contains the following mapping:
append_in_gaa(x1, x2, x3)  =  append_in_gaa(x1)
U1_gaa(x1, x2, x3, x4)  =  U1_gaa(x1, x4)
=_in_gg(x1, x2)  =  =_in_gg(x1, x2)
=_out_gg(x1, x2)  =  =_out_gg(x1, x2)
[]  =  []
U2_gaa(x1, x2, x3, x4)  =  U2_gaa(x1, x4)
=_in_aa(x1, x2)  =  =_in_aa
=_out_aa(x1, x2)  =  =_out_aa
append_out_gaa(x1, x2, x3)  =  append_out_gaa(x1)
U3_gaa(x1, x2, x3, x4)  =  U3_gaa(x1, x4)
=_in_ga(x1, x2)  =  =_in_ga(x1)
.(x1, x2)  =  .(x2)
=_out_ga(x1, x2)  =  =_out_ga(x1, x2)
U4_gaa(x1, x2, x3, x4, x5)  =  U4_gaa(x1, x4, x5)
U5_gaa(x1, x2, x3, x4)  =  U5_gaa(x1, x4)
APPEND_IN_GAA(x1, x2, x3)  =  APPEND_IN_GAA(x1)
U1_GAA(x1, x2, x3, x4)  =  U1_GAA(x1, x4)
=_IN_GG(x1, x2)  =  =_IN_GG(x1, x2)
U2_GAA(x1, x2, x3, x4)  =  U2_GAA(x1, x4)
=_IN_AA(x1, x2)  =  =_IN_AA
U3_GAA(x1, x2, x3, x4)  =  U3_GAA(x1, x4)
=_IN_GA(x1, x2)  =  =_IN_GA(x1)
U4_GAA(x1, x2, x3, x4, x5)  =  U4_GAA(x1, x4, x5)
U5_GAA(x1, x2, x3, x4)  =  U5_GAA(x1, x4)

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

(7) DependencyGraphProof (EQUIVALENT transformation)

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

(8) Obligation:

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

APPEND_IN_GAA(X, Y, Z) → U3_GAA(X, Y, Z, =_in_ga(X, .(H, Xs)))
U3_GAA(X, Y, Z, =_out_ga(X, .(H, Xs))) → U4_GAA(X, Y, Z, Xs, =_in_aa(Z, .(H, Zs)))
U4_GAA(X, Y, Z, Xs, =_out_aa(Z, .(H, Zs))) → APPEND_IN_GAA(Xs, Y, Zs)

The TRS R consists of the following rules:

append_in_gaa(X, Y, Z) → U1_gaa(X, Y, Z, =_in_gg(X, []))
=_in_gg(X, X) → =_out_gg(X, X)
U1_gaa(X, Y, Z, =_out_gg(X, [])) → U2_gaa(X, Y, Z, =_in_aa(Y, Z))
=_in_aa(X, X) → =_out_aa(X, X)
U2_gaa(X, Y, Z, =_out_aa(Y, Z)) → append_out_gaa(X, Y, Z)
append_in_gaa(X, Y, Z) → U3_gaa(X, Y, Z, =_in_ga(X, .(H, Xs)))
=_in_ga(X, X) → =_out_ga(X, X)
U3_gaa(X, Y, Z, =_out_ga(X, .(H, Xs))) → U4_gaa(X, Y, Z, Xs, =_in_aa(Z, .(H, Zs)))
U4_gaa(X, Y, Z, Xs, =_out_aa(Z, .(H, Zs))) → U5_gaa(X, Y, Z, append_in_gaa(Xs, Y, Zs))
U5_gaa(X, Y, Z, append_out_gaa(Xs, Y, Zs)) → append_out_gaa(X, Y, Z)

The argument filtering Pi contains the following mapping:
append_in_gaa(x1, x2, x3)  =  append_in_gaa(x1)
U1_gaa(x1, x2, x3, x4)  =  U1_gaa(x1, x4)
=_in_gg(x1, x2)  =  =_in_gg(x1, x2)
=_out_gg(x1, x2)  =  =_out_gg(x1, x2)
[]  =  []
U2_gaa(x1, x2, x3, x4)  =  U2_gaa(x1, x4)
=_in_aa(x1, x2)  =  =_in_aa
=_out_aa(x1, x2)  =  =_out_aa
append_out_gaa(x1, x2, x3)  =  append_out_gaa(x1)
U3_gaa(x1, x2, x3, x4)  =  U3_gaa(x1, x4)
=_in_ga(x1, x2)  =  =_in_ga(x1)
.(x1, x2)  =  .(x2)
=_out_ga(x1, x2)  =  =_out_ga(x1, x2)
U4_gaa(x1, x2, x3, x4, x5)  =  U4_gaa(x1, x4, x5)
U5_gaa(x1, x2, x3, x4)  =  U5_gaa(x1, x4)
APPEND_IN_GAA(x1, x2, x3)  =  APPEND_IN_GAA(x1)
U3_GAA(x1, x2, x3, x4)  =  U3_GAA(x1, x4)
U4_GAA(x1, x2, x3, x4, x5)  =  U4_GAA(x1, x4, x5)

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

(9) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(10) Obligation:

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

APPEND_IN_GAA(X, Y, Z) → U3_GAA(X, Y, Z, =_in_ga(X, .(H, Xs)))
U3_GAA(X, Y, Z, =_out_ga(X, .(H, Xs))) → U4_GAA(X, Y, Z, Xs, =_in_aa(Z, .(H, Zs)))
U4_GAA(X, Y, Z, Xs, =_out_aa(Z, .(H, Zs))) → APPEND_IN_GAA(Xs, Y, Zs)

The TRS R consists of the following rules:

=_in_ga(X, X) → =_out_ga(X, X)
=_in_aa(X, X) → =_out_aa(X, X)

The argument filtering Pi contains the following mapping:
=_in_aa(x1, x2)  =  =_in_aa
=_out_aa(x1, x2)  =  =_out_aa
=_in_ga(x1, x2)  =  =_in_ga(x1)
.(x1, x2)  =  .(x2)
=_out_ga(x1, x2)  =  =_out_ga(x1, x2)
APPEND_IN_GAA(x1, x2, x3)  =  APPEND_IN_GAA(x1)
U3_GAA(x1, x2, x3, x4)  =  U3_GAA(x1, x4)
U4_GAA(x1, x2, x3, x4, x5)  =  U4_GAA(x1, x4, x5)

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

(11) PiDPToQDPProof (SOUND transformation)

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

(12) Obligation:

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

APPEND_IN_GAA(X) → U3_GAA(X, =_in_ga(X))
U3_GAA(X, =_out_ga(X, .(Xs))) → U4_GAA(X, Xs, =_in_aa)
U4_GAA(X, Xs, =_out_aa) → APPEND_IN_GAA(Xs)

The TRS R consists of the following rules:

=_in_ga(X) → =_out_ga(X, X)
=_in_aa → =_out_aa

The set Q consists of the following terms:

=_in_ga(x0)
=_in_aa

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

(13) PrologToPiTRSProof (SOUND transformation)

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

append_in_gaa(X, Y, Z) → U1_gaa(X, Y, Z, =_in_gg(X, []))
=_in_gg(X, X) → =_out_gg(X, X)
U1_gaa(X, Y, Z, =_out_gg(X, [])) → U2_gaa(X, Y, Z, =_in_aa(Y, Z))
=_in_aa(X, X) → =_out_aa(X, X)
U2_gaa(X, Y, Z, =_out_aa(Y, Z)) → append_out_gaa(X, Y, Z)
append_in_gaa(X, Y, Z) → U3_gaa(X, Y, Z, =_in_ga(X, .(H, Xs)))
=_in_ga(X, X) → =_out_ga(X, X)
U3_gaa(X, Y, Z, =_out_ga(X, .(H, Xs))) → U4_gaa(X, Y, Z, Xs, =_in_aa(Z, .(H, Zs)))
U4_gaa(X, Y, Z, Xs, =_out_aa(Z, .(H, Zs))) → U5_gaa(X, Y, Z, append_in_gaa(Xs, Y, Zs))
U5_gaa(X, Y, Z, append_out_gaa(Xs, Y, Zs)) → append_out_gaa(X, Y, Z)

The argument filtering Pi contains the following mapping:
append_in_gaa(x1, x2, x3)  =  append_in_gaa(x1)
U1_gaa(x1, x2, x3, x4)  =  U1_gaa(x4)
=_in_gg(x1, x2)  =  =_in_gg(x1, x2)
=_out_gg(x1, x2)  =  =_out_gg
[]  =  []
U2_gaa(x1, x2, x3, x4)  =  U2_gaa(x4)
=_in_aa(x1, x2)  =  =_in_aa
=_out_aa(x1, x2)  =  =_out_aa
append_out_gaa(x1, x2, x3)  =  append_out_gaa
U3_gaa(x1, x2, x3, x4)  =  U3_gaa(x4)
=_in_ga(x1, x2)  =  =_in_ga(x1)
.(x1, x2)  =  .(x2)
=_out_ga(x1, x2)  =  =_out_ga(x2)
U4_gaa(x1, x2, x3, x4, x5)  =  U4_gaa(x4, x5)
U5_gaa(x1, x2, x3, x4)  =  U5_gaa(x4)

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog

(14) Obligation:

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

append_in_gaa(X, Y, Z) → U1_gaa(X, Y, Z, =_in_gg(X, []))
=_in_gg(X, X) → =_out_gg(X, X)
U1_gaa(X, Y, Z, =_out_gg(X, [])) → U2_gaa(X, Y, Z, =_in_aa(Y, Z))
=_in_aa(X, X) → =_out_aa(X, X)
U2_gaa(X, Y, Z, =_out_aa(Y, Z)) → append_out_gaa(X, Y, Z)
append_in_gaa(X, Y, Z) → U3_gaa(X, Y, Z, =_in_ga(X, .(H, Xs)))
=_in_ga(X, X) → =_out_ga(X, X)
U3_gaa(X, Y, Z, =_out_ga(X, .(H, Xs))) → U4_gaa(X, Y, Z, Xs, =_in_aa(Z, .(H, Zs)))
U4_gaa(X, Y, Z, Xs, =_out_aa(Z, .(H, Zs))) → U5_gaa(X, Y, Z, append_in_gaa(Xs, Y, Zs))
U5_gaa(X, Y, Z, append_out_gaa(Xs, Y, Zs)) → append_out_gaa(X, Y, Z)

The argument filtering Pi contains the following mapping:
append_in_gaa(x1, x2, x3)  =  append_in_gaa(x1)
U1_gaa(x1, x2, x3, x4)  =  U1_gaa(x4)
=_in_gg(x1, x2)  =  =_in_gg(x1, x2)
=_out_gg(x1, x2)  =  =_out_gg
[]  =  []
U2_gaa(x1, x2, x3, x4)  =  U2_gaa(x4)
=_in_aa(x1, x2)  =  =_in_aa
=_out_aa(x1, x2)  =  =_out_aa
append_out_gaa(x1, x2, x3)  =  append_out_gaa
U3_gaa(x1, x2, x3, x4)  =  U3_gaa(x4)
=_in_ga(x1, x2)  =  =_in_ga(x1)
.(x1, x2)  =  .(x2)
=_out_ga(x1, x2)  =  =_out_ga(x2)
U4_gaa(x1, x2, x3, x4, x5)  =  U4_gaa(x4, x5)
U5_gaa(x1, x2, x3, x4)  =  U5_gaa(x4)

(15) 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:

APPEND_IN_GAA(X, Y, Z) → U1_GAA(X, Y, Z, =_in_gg(X, []))
APPEND_IN_GAA(X, Y, Z) → =_IN_GG(X, [])
U1_GAA(X, Y, Z, =_out_gg(X, [])) → U2_GAA(X, Y, Z, =_in_aa(Y, Z))
U1_GAA(X, Y, Z, =_out_gg(X, [])) → =_IN_AA(Y, Z)
APPEND_IN_GAA(X, Y, Z) → U3_GAA(X, Y, Z, =_in_ga(X, .(H, Xs)))
APPEND_IN_GAA(X, Y, Z) → =_IN_GA(X, .(H, Xs))
U3_GAA(X, Y, Z, =_out_ga(X, .(H, Xs))) → U4_GAA(X, Y, Z, Xs, =_in_aa(Z, .(H, Zs)))
U3_GAA(X, Y, Z, =_out_ga(X, .(H, Xs))) → =_IN_AA(Z, .(H, Zs))
U4_GAA(X, Y, Z, Xs, =_out_aa(Z, .(H, Zs))) → U5_GAA(X, Y, Z, append_in_gaa(Xs, Y, Zs))
U4_GAA(X, Y, Z, Xs, =_out_aa(Z, .(H, Zs))) → APPEND_IN_GAA(Xs, Y, Zs)

The TRS R consists of the following rules:

append_in_gaa(X, Y, Z) → U1_gaa(X, Y, Z, =_in_gg(X, []))
=_in_gg(X, X) → =_out_gg(X, X)
U1_gaa(X, Y, Z, =_out_gg(X, [])) → U2_gaa(X, Y, Z, =_in_aa(Y, Z))
=_in_aa(X, X) → =_out_aa(X, X)
U2_gaa(X, Y, Z, =_out_aa(Y, Z)) → append_out_gaa(X, Y, Z)
append_in_gaa(X, Y, Z) → U3_gaa(X, Y, Z, =_in_ga(X, .(H, Xs)))
=_in_ga(X, X) → =_out_ga(X, X)
U3_gaa(X, Y, Z, =_out_ga(X, .(H, Xs))) → U4_gaa(X, Y, Z, Xs, =_in_aa(Z, .(H, Zs)))
U4_gaa(X, Y, Z, Xs, =_out_aa(Z, .(H, Zs))) → U5_gaa(X, Y, Z, append_in_gaa(Xs, Y, Zs))
U5_gaa(X, Y, Z, append_out_gaa(Xs, Y, Zs)) → append_out_gaa(X, Y, Z)

The argument filtering Pi contains the following mapping:
append_in_gaa(x1, x2, x3)  =  append_in_gaa(x1)
U1_gaa(x1, x2, x3, x4)  =  U1_gaa(x4)
=_in_gg(x1, x2)  =  =_in_gg(x1, x2)
=_out_gg(x1, x2)  =  =_out_gg
[]  =  []
U2_gaa(x1, x2, x3, x4)  =  U2_gaa(x4)
=_in_aa(x1, x2)  =  =_in_aa
=_out_aa(x1, x2)  =  =_out_aa
append_out_gaa(x1, x2, x3)  =  append_out_gaa
U3_gaa(x1, x2, x3, x4)  =  U3_gaa(x4)
=_in_ga(x1, x2)  =  =_in_ga(x1)
.(x1, x2)  =  .(x2)
=_out_ga(x1, x2)  =  =_out_ga(x2)
U4_gaa(x1, x2, x3, x4, x5)  =  U4_gaa(x4, x5)
U5_gaa(x1, x2, x3, x4)  =  U5_gaa(x4)
APPEND_IN_GAA(x1, x2, x3)  =  APPEND_IN_GAA(x1)
U1_GAA(x1, x2, x3, x4)  =  U1_GAA(x4)
=_IN_GG(x1, x2)  =  =_IN_GG(x1, x2)
U2_GAA(x1, x2, x3, x4)  =  U2_GAA(x4)
=_IN_AA(x1, x2)  =  =_IN_AA
U3_GAA(x1, x2, x3, x4)  =  U3_GAA(x4)
=_IN_GA(x1, x2)  =  =_IN_GA(x1)
U4_GAA(x1, x2, x3, x4, x5)  =  U4_GAA(x4, x5)
U5_GAA(x1, x2, x3, x4)  =  U5_GAA(x4)

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

(16) Obligation:

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

APPEND_IN_GAA(X, Y, Z) → U1_GAA(X, Y, Z, =_in_gg(X, []))
APPEND_IN_GAA(X, Y, Z) → =_IN_GG(X, [])
U1_GAA(X, Y, Z, =_out_gg(X, [])) → U2_GAA(X, Y, Z, =_in_aa(Y, Z))
U1_GAA(X, Y, Z, =_out_gg(X, [])) → =_IN_AA(Y, Z)
APPEND_IN_GAA(X, Y, Z) → U3_GAA(X, Y, Z, =_in_ga(X, .(H, Xs)))
APPEND_IN_GAA(X, Y, Z) → =_IN_GA(X, .(H, Xs))
U3_GAA(X, Y, Z, =_out_ga(X, .(H, Xs))) → U4_GAA(X, Y, Z, Xs, =_in_aa(Z, .(H, Zs)))
U3_GAA(X, Y, Z, =_out_ga(X, .(H, Xs))) → =_IN_AA(Z, .(H, Zs))
U4_GAA(X, Y, Z, Xs, =_out_aa(Z, .(H, Zs))) → U5_GAA(X, Y, Z, append_in_gaa(Xs, Y, Zs))
U4_GAA(X, Y, Z, Xs, =_out_aa(Z, .(H, Zs))) → APPEND_IN_GAA(Xs, Y, Zs)

The TRS R consists of the following rules:

append_in_gaa(X, Y, Z) → U1_gaa(X, Y, Z, =_in_gg(X, []))
=_in_gg(X, X) → =_out_gg(X, X)
U1_gaa(X, Y, Z, =_out_gg(X, [])) → U2_gaa(X, Y, Z, =_in_aa(Y, Z))
=_in_aa(X, X) → =_out_aa(X, X)
U2_gaa(X, Y, Z, =_out_aa(Y, Z)) → append_out_gaa(X, Y, Z)
append_in_gaa(X, Y, Z) → U3_gaa(X, Y, Z, =_in_ga(X, .(H, Xs)))
=_in_ga(X, X) → =_out_ga(X, X)
U3_gaa(X, Y, Z, =_out_ga(X, .(H, Xs))) → U4_gaa(X, Y, Z, Xs, =_in_aa(Z, .(H, Zs)))
U4_gaa(X, Y, Z, Xs, =_out_aa(Z, .(H, Zs))) → U5_gaa(X, Y, Z, append_in_gaa(Xs, Y, Zs))
U5_gaa(X, Y, Z, append_out_gaa(Xs, Y, Zs)) → append_out_gaa(X, Y, Z)

The argument filtering Pi contains the following mapping:
append_in_gaa(x1, x2, x3)  =  append_in_gaa(x1)
U1_gaa(x1, x2, x3, x4)  =  U1_gaa(x4)
=_in_gg(x1, x2)  =  =_in_gg(x1, x2)
=_out_gg(x1, x2)  =  =_out_gg
[]  =  []
U2_gaa(x1, x2, x3, x4)  =  U2_gaa(x4)
=_in_aa(x1, x2)  =  =_in_aa
=_out_aa(x1, x2)  =  =_out_aa
append_out_gaa(x1, x2, x3)  =  append_out_gaa
U3_gaa(x1, x2, x3, x4)  =  U3_gaa(x4)
=_in_ga(x1, x2)  =  =_in_ga(x1)
.(x1, x2)  =  .(x2)
=_out_ga(x1, x2)  =  =_out_ga(x2)
U4_gaa(x1, x2, x3, x4, x5)  =  U4_gaa(x4, x5)
U5_gaa(x1, x2, x3, x4)  =  U5_gaa(x4)
APPEND_IN_GAA(x1, x2, x3)  =  APPEND_IN_GAA(x1)
U1_GAA(x1, x2, x3, x4)  =  U1_GAA(x4)
=_IN_GG(x1, x2)  =  =_IN_GG(x1, x2)
U2_GAA(x1, x2, x3, x4)  =  U2_GAA(x4)
=_IN_AA(x1, x2)  =  =_IN_AA
U3_GAA(x1, x2, x3, x4)  =  U3_GAA(x4)
=_IN_GA(x1, x2)  =  =_IN_GA(x1)
U4_GAA(x1, x2, x3, x4, x5)  =  U4_GAA(x4, x5)
U5_GAA(x1, x2, x3, x4)  =  U5_GAA(x4)

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

(17) DependencyGraphProof (EQUIVALENT transformation)

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

(18) Obligation:

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

APPEND_IN_GAA(X, Y, Z) → U3_GAA(X, Y, Z, =_in_ga(X, .(H, Xs)))
U3_GAA(X, Y, Z, =_out_ga(X, .(H, Xs))) → U4_GAA(X, Y, Z, Xs, =_in_aa(Z, .(H, Zs)))
U4_GAA(X, Y, Z, Xs, =_out_aa(Z, .(H, Zs))) → APPEND_IN_GAA(Xs, Y, Zs)

The TRS R consists of the following rules:

append_in_gaa(X, Y, Z) → U1_gaa(X, Y, Z, =_in_gg(X, []))
=_in_gg(X, X) → =_out_gg(X, X)
U1_gaa(X, Y, Z, =_out_gg(X, [])) → U2_gaa(X, Y, Z, =_in_aa(Y, Z))
=_in_aa(X, X) → =_out_aa(X, X)
U2_gaa(X, Y, Z, =_out_aa(Y, Z)) → append_out_gaa(X, Y, Z)
append_in_gaa(X, Y, Z) → U3_gaa(X, Y, Z, =_in_ga(X, .(H, Xs)))
=_in_ga(X, X) → =_out_ga(X, X)
U3_gaa(X, Y, Z, =_out_ga(X, .(H, Xs))) → U4_gaa(X, Y, Z, Xs, =_in_aa(Z, .(H, Zs)))
U4_gaa(X, Y, Z, Xs, =_out_aa(Z, .(H, Zs))) → U5_gaa(X, Y, Z, append_in_gaa(Xs, Y, Zs))
U5_gaa(X, Y, Z, append_out_gaa(Xs, Y, Zs)) → append_out_gaa(X, Y, Z)

The argument filtering Pi contains the following mapping:
append_in_gaa(x1, x2, x3)  =  append_in_gaa(x1)
U1_gaa(x1, x2, x3, x4)  =  U1_gaa(x4)
=_in_gg(x1, x2)  =  =_in_gg(x1, x2)
=_out_gg(x1, x2)  =  =_out_gg
[]  =  []
U2_gaa(x1, x2, x3, x4)  =  U2_gaa(x4)
=_in_aa(x1, x2)  =  =_in_aa
=_out_aa(x1, x2)  =  =_out_aa
append_out_gaa(x1, x2, x3)  =  append_out_gaa
U3_gaa(x1, x2, x3, x4)  =  U3_gaa(x4)
=_in_ga(x1, x2)  =  =_in_ga(x1)
.(x1, x2)  =  .(x2)
=_out_ga(x1, x2)  =  =_out_ga(x2)
U4_gaa(x1, x2, x3, x4, x5)  =  U4_gaa(x4, x5)
U5_gaa(x1, x2, x3, x4)  =  U5_gaa(x4)
APPEND_IN_GAA(x1, x2, x3)  =  APPEND_IN_GAA(x1)
U3_GAA(x1, x2, x3, x4)  =  U3_GAA(x4)
U4_GAA(x1, x2, x3, x4, x5)  =  U4_GAA(x4, x5)

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

(19) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(20) Obligation:

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

APPEND_IN_GAA(X, Y, Z) → U3_GAA(X, Y, Z, =_in_ga(X, .(H, Xs)))
U3_GAA(X, Y, Z, =_out_ga(X, .(H, Xs))) → U4_GAA(X, Y, Z, Xs, =_in_aa(Z, .(H, Zs)))
U4_GAA(X, Y, Z, Xs, =_out_aa(Z, .(H, Zs))) → APPEND_IN_GAA(Xs, Y, Zs)

The TRS R consists of the following rules:

=_in_ga(X, X) → =_out_ga(X, X)
=_in_aa(X, X) → =_out_aa(X, X)

The argument filtering Pi contains the following mapping:
=_in_aa(x1, x2)  =  =_in_aa
=_out_aa(x1, x2)  =  =_out_aa
=_in_ga(x1, x2)  =  =_in_ga(x1)
.(x1, x2)  =  .(x2)
=_out_ga(x1, x2)  =  =_out_ga(x2)
APPEND_IN_GAA(x1, x2, x3)  =  APPEND_IN_GAA(x1)
U3_GAA(x1, x2, x3, x4)  =  U3_GAA(x4)
U4_GAA(x1, x2, x3, x4, x5)  =  U4_GAA(x4, x5)

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

(21) PiDPToQDPProof (SOUND transformation)

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

(22) Obligation:

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

APPEND_IN_GAA(X) → U3_GAA(=_in_ga(X))
U3_GAA(=_out_ga(.(Xs))) → U4_GAA(Xs, =_in_aa)
U4_GAA(Xs, =_out_aa) → APPEND_IN_GAA(Xs)

The TRS R consists of the following rules:

=_in_ga(X) → =_out_ga(X)
=_in_aa → =_out_aa

The set Q consists of the following terms:

=_in_ga(x0)
=_in_aa

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

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

The following dependency pairs can be deleted:

U3_GAA(=_out_ga(.(Xs))) → U4_GAA(Xs, =_in_aa)
No rules are removed from R.

Used ordering: POLO with Polynomial interpretation [POLO]:

POL(.(x1)) = 2 + 2·x1   
POL(=_in_aa) = 0   
POL(=_in_ga(x1)) = x1   
POL(=_out_aa) = 0   
POL(=_out_ga(x1)) = x1   
POL(APPEND_IN_GAA(x1)) = 1 + x1   
POL(U3_GAA(x1)) = 1 + x1   
POL(U4_GAA(x1, x2)) = 1 + 2·x1 + x2   

(24) Obligation:

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

APPEND_IN_GAA(X) → U3_GAA(=_in_ga(X))
U4_GAA(Xs, =_out_aa) → APPEND_IN_GAA(Xs)

The TRS R consists of the following rules:

=_in_ga(X) → =_out_ga(X)
=_in_aa → =_out_aa

The set Q consists of the following terms:

=_in_ga(x0)
=_in_aa

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

(25) DependencyGraphProof (EQUIVALENT transformation)

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

(26) TRUE