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

0 Prolog
↳1 BuiltinConflictTransformerProof (⇔, 0 ms)
↳2 Prolog
↳3 CutEliminatorProof (⇒, 0 ms)
↳4 Prolog
↳5 PrologToPiTRSProof (⇒, 0 ms)
↳6 PiTRS
↳7 DependencyPairsProof (⇔, 5 ms)
↳8 PiDP
↳9 DependencyGraphProof (⇔, 0 ms)
↳10 PiDP
↳11 UsableRulesProof (⇔, 0 ms)
↳12 PiDP
↳13 PiDPToQDPProof (⇒, 0 ms)
↳14 QDP
↳15 UsableRulesReductionPairsProof (⇔, 74 ms)
↳16 QDP
↳17 DependencyGraphProof (⇔, 0 ms)
↳18 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).

Query: append(g,a,a)

(1) BuiltinConflictTransformerProof (EQUIVALENT transformation)

Renamed defined predicates conflicting with built-in predicates [PROLOG].

(2) Obligation:

Clauses:

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

Query: append(g,a,a)

(3) CutEliminatorProof (SOUND transformation)

Eliminated all cuts by simply ignoring them[PROLOG].

(4) Obligation:

Clauses:

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

Query: append(g,a,a)

(5) PrologToPiTRSProof (SOUND transformation)

We use the technique of [TOCL09]. 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, user_defined_=_in_gg(X, []))
user_defined_=_in_gg(X, X) → user_defined_=_out_gg(X, X)
U1_gaa(X, Y, Z, user_defined_=_out_gg(X, [])) → U2_gaa(X, Y, Z, user_defined_=_in_aa(Y, Z))
user_defined_=_in_aa(X, X) → user_defined_=_out_aa(X, X)
U2_gaa(X, Y, Z, user_defined_=_out_aa(Y, Z)) → append_out_gaa(X, Y, Z)
append_in_gaa(X, Y, Z) → U3_gaa(X, Y, Z, user_defined_=_in_ga(X, .(H, Xs)))
user_defined_=_in_ga(X, X) → user_defined_=_out_ga(X, X)
U3_gaa(X, Y, Z, user_defined_=_out_ga(X, .(H, Xs))) → U4_gaa(X, Y, Z, Xs, user_defined_=_in_aa(Z, .(H, Zs)))
U4_gaa(X, Y, Z, Xs, user_defined_=_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)
user_defined_=_in_gg(x1, x2)  =  user_defined_=_in_gg(x1, x2)
user_defined_=_out_gg(x1, x2)  =  user_defined_=_out_gg
[]  =  []
U2_gaa(x1, x2, x3, x4)  =  U2_gaa(x4)
user_defined_=_in_aa(x1, x2)  =  user_defined_=_in_aa
user_defined_=_out_aa(x1, x2)  =  user_defined_=_out_aa
append_out_gaa(x1, x2, x3)  =  append_out_gaa
U3_gaa(x1, x2, x3, x4)  =  U3_gaa(x4)
user_defined_=_in_ga(x1, x2)  =  user_defined_=_in_ga(x1)
.(x1, x2)  =  .(x2)
user_defined_=_out_ga(x1, x2)  =  user_defined_=_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

(6) Obligation:

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

append_in_gaa(X, Y, Z) → U1_gaa(X, Y, Z, user_defined_=_in_gg(X, []))
user_defined_=_in_gg(X, X) → user_defined_=_out_gg(X, X)
U1_gaa(X, Y, Z, user_defined_=_out_gg(X, [])) → U2_gaa(X, Y, Z, user_defined_=_in_aa(Y, Z))
user_defined_=_in_aa(X, X) → user_defined_=_out_aa(X, X)
U2_gaa(X, Y, Z, user_defined_=_out_aa(Y, Z)) → append_out_gaa(X, Y, Z)
append_in_gaa(X, Y, Z) → U3_gaa(X, Y, Z, user_defined_=_in_ga(X, .(H, Xs)))
user_defined_=_in_ga(X, X) → user_defined_=_out_ga(X, X)
U3_gaa(X, Y, Z, user_defined_=_out_ga(X, .(H, Xs))) → U4_gaa(X, Y, Z, Xs, user_defined_=_in_aa(Z, .(H, Zs)))
U4_gaa(X, Y, Z, Xs, user_defined_=_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)
user_defined_=_in_gg(x1, x2)  =  user_defined_=_in_gg(x1, x2)
user_defined_=_out_gg(x1, x2)  =  user_defined_=_out_gg
[]  =  []
U2_gaa(x1, x2, x3, x4)  =  U2_gaa(x4)
user_defined_=_in_aa(x1, x2)  =  user_defined_=_in_aa
user_defined_=_out_aa(x1, x2)  =  user_defined_=_out_aa
append_out_gaa(x1, x2, x3)  =  append_out_gaa
U3_gaa(x1, x2, x3, x4)  =  U3_gaa(x4)
user_defined_=_in_ga(x1, x2)  =  user_defined_=_in_ga(x1)
.(x1, x2)  =  .(x2)
user_defined_=_out_ga(x1, x2)  =  user_defined_=_out_ga(x2)
U4_gaa(x1, x2, x3, x4, x5)  =  U4_gaa(x4, x5)
U5_gaa(x1, x2, x3, x4)  =  U5_gaa(x4)

(7) 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, user_defined_=_in_gg(X, []))
APPEND_IN_GAA(X, Y, Z) → USER_DEFINED_=_IN_GG(X, [])
U1_GAA(X, Y, Z, user_defined_=_out_gg(X, [])) → U2_GAA(X, Y, Z, user_defined_=_in_aa(Y, Z))
U1_GAA(X, Y, Z, user_defined_=_out_gg(X, [])) → USER_DEFINED_=_IN_AA(Y, Z)
APPEND_IN_GAA(X, Y, Z) → U3_GAA(X, Y, Z, user_defined_=_in_ga(X, .(H, Xs)))
APPEND_IN_GAA(X, Y, Z) → USER_DEFINED_=_IN_GA(X, .(H, Xs))
U3_GAA(X, Y, Z, user_defined_=_out_ga(X, .(H, Xs))) → U4_GAA(X, Y, Z, Xs, user_defined_=_in_aa(Z, .(H, Zs)))
U3_GAA(X, Y, Z, user_defined_=_out_ga(X, .(H, Xs))) → USER_DEFINED_=_IN_AA(Z, .(H, Zs))
U4_GAA(X, Y, Z, Xs, user_defined_=_out_aa(Z, .(H, Zs))) → U5_GAA(X, Y, Z, append_in_gaa(Xs, Y, Zs))
U4_GAA(X, Y, Z, Xs, user_defined_=_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, user_defined_=_in_gg(X, []))
user_defined_=_in_gg(X, X) → user_defined_=_out_gg(X, X)
U1_gaa(X, Y, Z, user_defined_=_out_gg(X, [])) → U2_gaa(X, Y, Z, user_defined_=_in_aa(Y, Z))
user_defined_=_in_aa(X, X) → user_defined_=_out_aa(X, X)
U2_gaa(X, Y, Z, user_defined_=_out_aa(Y, Z)) → append_out_gaa(X, Y, Z)
append_in_gaa(X, Y, Z) → U3_gaa(X, Y, Z, user_defined_=_in_ga(X, .(H, Xs)))
user_defined_=_in_ga(X, X) → user_defined_=_out_ga(X, X)
U3_gaa(X, Y, Z, user_defined_=_out_ga(X, .(H, Xs))) → U4_gaa(X, Y, Z, Xs, user_defined_=_in_aa(Z, .(H, Zs)))
U4_gaa(X, Y, Z, Xs, user_defined_=_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)
user_defined_=_in_gg(x1, x2)  =  user_defined_=_in_gg(x1, x2)
user_defined_=_out_gg(x1, x2)  =  user_defined_=_out_gg
[]  =  []
U2_gaa(x1, x2, x3, x4)  =  U2_gaa(x4)
user_defined_=_in_aa(x1, x2)  =  user_defined_=_in_aa
user_defined_=_out_aa(x1, x2)  =  user_defined_=_out_aa
append_out_gaa(x1, x2, x3)  =  append_out_gaa
U3_gaa(x1, x2, x3, x4)  =  U3_gaa(x4)
user_defined_=_in_ga(x1, x2)  =  user_defined_=_in_ga(x1)
.(x1, x2)  =  .(x2)
user_defined_=_out_ga(x1, x2)  =  user_defined_=_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)
USER_DEFINED_=_IN_GG(x1, x2)  =  USER_DEFINED_=_IN_GG(x1, x2)
U2_GAA(x1, x2, x3, x4)  =  U2_GAA(x4)
USER_DEFINED_=_IN_AA(x1, x2)  =  USER_DEFINED_=_IN_AA
U3_GAA(x1, x2, x3, x4)  =  U3_GAA(x4)
USER_DEFINED_=_IN_GA(x1, x2)  =  USER_DEFINED_=_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

(8) Obligation:

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

APPEND_IN_GAA(X, Y, Z) → U1_GAA(X, Y, Z, user_defined_=_in_gg(X, []))
APPEND_IN_GAA(X, Y, Z) → USER_DEFINED_=_IN_GG(X, [])
U1_GAA(X, Y, Z, user_defined_=_out_gg(X, [])) → U2_GAA(X, Y, Z, user_defined_=_in_aa(Y, Z))
U1_GAA(X, Y, Z, user_defined_=_out_gg(X, [])) → USER_DEFINED_=_IN_AA(Y, Z)
APPEND_IN_GAA(X, Y, Z) → U3_GAA(X, Y, Z, user_defined_=_in_ga(X, .(H, Xs)))
APPEND_IN_GAA(X, Y, Z) → USER_DEFINED_=_IN_GA(X, .(H, Xs))
U3_GAA(X, Y, Z, user_defined_=_out_ga(X, .(H, Xs))) → U4_GAA(X, Y, Z, Xs, user_defined_=_in_aa(Z, .(H, Zs)))
U3_GAA(X, Y, Z, user_defined_=_out_ga(X, .(H, Xs))) → USER_DEFINED_=_IN_AA(Z, .(H, Zs))
U4_GAA(X, Y, Z, Xs, user_defined_=_out_aa(Z, .(H, Zs))) → U5_GAA(X, Y, Z, append_in_gaa(Xs, Y, Zs))
U4_GAA(X, Y, Z, Xs, user_defined_=_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, user_defined_=_in_gg(X, []))
user_defined_=_in_gg(X, X) → user_defined_=_out_gg(X, X)
U1_gaa(X, Y, Z, user_defined_=_out_gg(X, [])) → U2_gaa(X, Y, Z, user_defined_=_in_aa(Y, Z))
user_defined_=_in_aa(X, X) → user_defined_=_out_aa(X, X)
U2_gaa(X, Y, Z, user_defined_=_out_aa(Y, Z)) → append_out_gaa(X, Y, Z)
append_in_gaa(X, Y, Z) → U3_gaa(X, Y, Z, user_defined_=_in_ga(X, .(H, Xs)))
user_defined_=_in_ga(X, X) → user_defined_=_out_ga(X, X)
U3_gaa(X, Y, Z, user_defined_=_out_ga(X, .(H, Xs))) → U4_gaa(X, Y, Z, Xs, user_defined_=_in_aa(Z, .(H, Zs)))
U4_gaa(X, Y, Z, Xs, user_defined_=_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)
user_defined_=_in_gg(x1, x2)  =  user_defined_=_in_gg(x1, x2)
user_defined_=_out_gg(x1, x2)  =  user_defined_=_out_gg
[]  =  []
U2_gaa(x1, x2, x3, x4)  =  U2_gaa(x4)
user_defined_=_in_aa(x1, x2)  =  user_defined_=_in_aa
user_defined_=_out_aa(x1, x2)  =  user_defined_=_out_aa
append_out_gaa(x1, x2, x3)  =  append_out_gaa
U3_gaa(x1, x2, x3, x4)  =  U3_gaa(x4)
user_defined_=_in_ga(x1, x2)  =  user_defined_=_in_ga(x1)
.(x1, x2)  =  .(x2)
user_defined_=_out_ga(x1, x2)  =  user_defined_=_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)
USER_DEFINED_=_IN_GG(x1, x2)  =  USER_DEFINED_=_IN_GG(x1, x2)
U2_GAA(x1, x2, x3, x4)  =  U2_GAA(x4)
USER_DEFINED_=_IN_AA(x1, x2)  =  USER_DEFINED_=_IN_AA
U3_GAA(x1, x2, x3, x4)  =  U3_GAA(x4)
USER_DEFINED_=_IN_GA(x1, x2)  =  USER_DEFINED_=_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

(9) DependencyGraphProof (EQUIVALENT transformation)

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

(10) Obligation:

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

APPEND_IN_GAA(X, Y, Z) → U3_GAA(X, Y, Z, user_defined_=_in_ga(X, .(H, Xs)))
U3_GAA(X, Y, Z, user_defined_=_out_ga(X, .(H, Xs))) → U4_GAA(X, Y, Z, Xs, user_defined_=_in_aa(Z, .(H, Zs)))
U4_GAA(X, Y, Z, Xs, user_defined_=_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, user_defined_=_in_gg(X, []))
user_defined_=_in_gg(X, X) → user_defined_=_out_gg(X, X)
U1_gaa(X, Y, Z, user_defined_=_out_gg(X, [])) → U2_gaa(X, Y, Z, user_defined_=_in_aa(Y, Z))
user_defined_=_in_aa(X, X) → user_defined_=_out_aa(X, X)
U2_gaa(X, Y, Z, user_defined_=_out_aa(Y, Z)) → append_out_gaa(X, Y, Z)
append_in_gaa(X, Y, Z) → U3_gaa(X, Y, Z, user_defined_=_in_ga(X, .(H, Xs)))
user_defined_=_in_ga(X, X) → user_defined_=_out_ga(X, X)
U3_gaa(X, Y, Z, user_defined_=_out_ga(X, .(H, Xs))) → U4_gaa(X, Y, Z, Xs, user_defined_=_in_aa(Z, .(H, Zs)))
U4_gaa(X, Y, Z, Xs, user_defined_=_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)
user_defined_=_in_gg(x1, x2)  =  user_defined_=_in_gg(x1, x2)
user_defined_=_out_gg(x1, x2)  =  user_defined_=_out_gg
[]  =  []
U2_gaa(x1, x2, x3, x4)  =  U2_gaa(x4)
user_defined_=_in_aa(x1, x2)  =  user_defined_=_in_aa
user_defined_=_out_aa(x1, x2)  =  user_defined_=_out_aa
append_out_gaa(x1, x2, x3)  =  append_out_gaa
U3_gaa(x1, x2, x3, x4)  =  U3_gaa(x4)
user_defined_=_in_ga(x1, x2)  =  user_defined_=_in_ga(x1)
.(x1, x2)  =  .(x2)
user_defined_=_out_ga(x1, x2)  =  user_defined_=_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

(11) UsableRulesProof (EQUIVALENT transformation)

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

(12) Obligation:

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

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

The TRS R consists of the following rules:

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

The argument filtering Pi contains the following mapping:
user_defined_=_in_aa(x1, x2)  =  user_defined_=_in_aa
user_defined_=_out_aa(x1, x2)  =  user_defined_=_out_aa
user_defined_=_in_ga(x1, x2)  =  user_defined_=_in_ga(x1)
.(x1, x2)  =  .(x2)
user_defined_=_out_ga(x1, x2)  =  user_defined_=_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

(13) PiDPToQDPProof (SOUND transformation)

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

(14) Obligation:

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

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

The TRS R consists of the following rules:

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

The set Q consists of the following terms:

user_defined_=_in_ga(x0)
user_defined_=_in_aa

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

(15) 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(user_defined_=_out_ga(.(Xs))) → U4_GAA(Xs, user_defined_=_in_aa)
No rules are removed from R.

Used ordering: POLO with Polynomial interpretation [POLO]:

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

(16) Obligation:

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

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

The TRS R consists of the following rules:

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

The set Q consists of the following terms:

user_defined_=_in_ga(x0)
user_defined_=_in_aa

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

(17) DependencyGraphProof (EQUIVALENT transformation)

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

(18) TRUE