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

(0) Obligation:

Clauses:

e(L, T) :- t(L, T).
e(L, T) :- ','(t(L, .(plus, C)), e(C, T)).
t(L, T) :- n(L, T).
t(L, T) :- ','(n(L, .(star, C)), t(C, T)).
n(.(L, T), T) :- z(L).
n(.(lbrace, A), B) :- e(A, .(rbrace, B)).
z(a).
z(b).
z(c).

Queries:

e(g,a).

(1) PrologToPiTRSProof (SOUND transformation)

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

e_in_ga(L, T) → U1_ga(L, T, t_in_ga(L, T))
t_in_ga(L, T) → U4_ga(L, T, n_in_ga(L, T))
n_in_ga(.(L, T), T) → U7_ga(L, T, z_in_g(L))
z_in_g(a) → z_out_g(a)
z_in_g(b) → z_out_g(b)
z_in_g(c) → z_out_g(c)
U7_ga(L, T, z_out_g(L)) → n_out_ga(.(L, T), T)
n_in_ga(.(lbrace, A), B) → U8_ga(A, B, e_in_ga(A, .(rbrace, B)))
e_in_ga(L, T) → U2_ga(L, T, t_in_ga(L, .(plus, C)))
t_in_ga(L, T) → U5_ga(L, T, n_in_ga(L, .(star, C)))
U5_ga(L, T, n_out_ga(L, .(star, C))) → U6_ga(L, T, t_in_ga(C, T))
U6_ga(L, T, t_out_ga(C, T)) → t_out_ga(L, T)
U2_ga(L, T, t_out_ga(L, .(plus, C))) → U3_ga(L, T, e_in_ga(C, T))
U3_ga(L, T, e_out_ga(C, T)) → e_out_ga(L, T)
U8_ga(A, B, e_out_ga(A, .(rbrace, B))) → n_out_ga(.(lbrace, A), B)
U4_ga(L, T, n_out_ga(L, T)) → t_out_ga(L, T)
U1_ga(L, T, t_out_ga(L, T)) → e_out_ga(L, T)

The argument filtering Pi contains the following mapping:
e_in_ga(x1, x2)  =  e_in_ga(x1)
U1_ga(x1, x2, x3)  =  U1_ga(x3)
t_in_ga(x1, x2)  =  t_in_ga(x1)
U4_ga(x1, x2, x3)  =  U4_ga(x3)
n_in_ga(x1, x2)  =  n_in_ga(x1)
.(x1, x2)  =  .(x1, x2)
U7_ga(x1, x2, x3)  =  U7_ga(x2, x3)
z_in_g(x1)  =  z_in_g(x1)
a  =  a
z_out_g(x1)  =  z_out_g
b  =  b
c  =  c
n_out_ga(x1, x2)  =  n_out_ga(x2)
lbrace  =  lbrace
U8_ga(x1, x2, x3)  =  U8_ga(x3)
U2_ga(x1, x2, x3)  =  U2_ga(x3)
U5_ga(x1, x2, x3)  =  U5_ga(x3)
star  =  star
U6_ga(x1, x2, x3)  =  U6_ga(x3)
t_out_ga(x1, x2)  =  t_out_ga(x2)
plus  =  plus
U3_ga(x1, x2, x3)  =  U3_ga(x3)
e_out_ga(x1, x2)  =  e_out_ga(x2)
rbrace  =  rbrace

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog

(2) Obligation:

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

e_in_ga(L, T) → U1_ga(L, T, t_in_ga(L, T))
t_in_ga(L, T) → U4_ga(L, T, n_in_ga(L, T))
n_in_ga(.(L, T), T) → U7_ga(L, T, z_in_g(L))
z_in_g(a) → z_out_g(a)
z_in_g(b) → z_out_g(b)
z_in_g(c) → z_out_g(c)
U7_ga(L, T, z_out_g(L)) → n_out_ga(.(L, T), T)
n_in_ga(.(lbrace, A), B) → U8_ga(A, B, e_in_ga(A, .(rbrace, B)))
e_in_ga(L, T) → U2_ga(L, T, t_in_ga(L, .(plus, C)))
t_in_ga(L, T) → U5_ga(L, T, n_in_ga(L, .(star, C)))
U5_ga(L, T, n_out_ga(L, .(star, C))) → U6_ga(L, T, t_in_ga(C, T))
U6_ga(L, T, t_out_ga(C, T)) → t_out_ga(L, T)
U2_ga(L, T, t_out_ga(L, .(plus, C))) → U3_ga(L, T, e_in_ga(C, T))
U3_ga(L, T, e_out_ga(C, T)) → e_out_ga(L, T)
U8_ga(A, B, e_out_ga(A, .(rbrace, B))) → n_out_ga(.(lbrace, A), B)
U4_ga(L, T, n_out_ga(L, T)) → t_out_ga(L, T)
U1_ga(L, T, t_out_ga(L, T)) → e_out_ga(L, T)

The argument filtering Pi contains the following mapping:
e_in_ga(x1, x2)  =  e_in_ga(x1)
U1_ga(x1, x2, x3)  =  U1_ga(x3)
t_in_ga(x1, x2)  =  t_in_ga(x1)
U4_ga(x1, x2, x3)  =  U4_ga(x3)
n_in_ga(x1, x2)  =  n_in_ga(x1)
.(x1, x2)  =  .(x1, x2)
U7_ga(x1, x2, x3)  =  U7_ga(x2, x3)
z_in_g(x1)  =  z_in_g(x1)
a  =  a
z_out_g(x1)  =  z_out_g
b  =  b
c  =  c
n_out_ga(x1, x2)  =  n_out_ga(x2)
lbrace  =  lbrace
U8_ga(x1, x2, x3)  =  U8_ga(x3)
U2_ga(x1, x2, x3)  =  U2_ga(x3)
U5_ga(x1, x2, x3)  =  U5_ga(x3)
star  =  star
U6_ga(x1, x2, x3)  =  U6_ga(x3)
t_out_ga(x1, x2)  =  t_out_ga(x2)
plus  =  plus
U3_ga(x1, x2, x3)  =  U3_ga(x3)
e_out_ga(x1, x2)  =  e_out_ga(x2)
rbrace  =  rbrace

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

E_IN_GA(L, T) → U1_GA(L, T, t_in_ga(L, T))
E_IN_GA(L, T) → T_IN_GA(L, T)
T_IN_GA(L, T) → U4_GA(L, T, n_in_ga(L, T))
T_IN_GA(L, T) → N_IN_GA(L, T)
N_IN_GA(.(L, T), T) → U7_GA(L, T, z_in_g(L))
N_IN_GA(.(L, T), T) → Z_IN_G(L)
N_IN_GA(.(lbrace, A), B) → U8_GA(A, B, e_in_ga(A, .(rbrace, B)))
N_IN_GA(.(lbrace, A), B) → E_IN_GA(A, .(rbrace, B))
E_IN_GA(L, T) → U2_GA(L, T, t_in_ga(L, .(plus, C)))
E_IN_GA(L, T) → T_IN_GA(L, .(plus, C))
T_IN_GA(L, T) → U5_GA(L, T, n_in_ga(L, .(star, C)))
T_IN_GA(L, T) → N_IN_GA(L, .(star, C))
U5_GA(L, T, n_out_ga(L, .(star, C))) → U6_GA(L, T, t_in_ga(C, T))
U5_GA(L, T, n_out_ga(L, .(star, C))) → T_IN_GA(C, T)
U2_GA(L, T, t_out_ga(L, .(plus, C))) → U3_GA(L, T, e_in_ga(C, T))
U2_GA(L, T, t_out_ga(L, .(plus, C))) → E_IN_GA(C, T)

The TRS R consists of the following rules:

e_in_ga(L, T) → U1_ga(L, T, t_in_ga(L, T))
t_in_ga(L, T) → U4_ga(L, T, n_in_ga(L, T))
n_in_ga(.(L, T), T) → U7_ga(L, T, z_in_g(L))
z_in_g(a) → z_out_g(a)
z_in_g(b) → z_out_g(b)
z_in_g(c) → z_out_g(c)
U7_ga(L, T, z_out_g(L)) → n_out_ga(.(L, T), T)
n_in_ga(.(lbrace, A), B) → U8_ga(A, B, e_in_ga(A, .(rbrace, B)))
e_in_ga(L, T) → U2_ga(L, T, t_in_ga(L, .(plus, C)))
t_in_ga(L, T) → U5_ga(L, T, n_in_ga(L, .(star, C)))
U5_ga(L, T, n_out_ga(L, .(star, C))) → U6_ga(L, T, t_in_ga(C, T))
U6_ga(L, T, t_out_ga(C, T)) → t_out_ga(L, T)
U2_ga(L, T, t_out_ga(L, .(plus, C))) → U3_ga(L, T, e_in_ga(C, T))
U3_ga(L, T, e_out_ga(C, T)) → e_out_ga(L, T)
U8_ga(A, B, e_out_ga(A, .(rbrace, B))) → n_out_ga(.(lbrace, A), B)
U4_ga(L, T, n_out_ga(L, T)) → t_out_ga(L, T)
U1_ga(L, T, t_out_ga(L, T)) → e_out_ga(L, T)

The argument filtering Pi contains the following mapping:
e_in_ga(x1, x2)  =  e_in_ga(x1)
U1_ga(x1, x2, x3)  =  U1_ga(x3)
t_in_ga(x1, x2)  =  t_in_ga(x1)
U4_ga(x1, x2, x3)  =  U4_ga(x3)
n_in_ga(x1, x2)  =  n_in_ga(x1)
.(x1, x2)  =  .(x1, x2)
U7_ga(x1, x2, x3)  =  U7_ga(x2, x3)
z_in_g(x1)  =  z_in_g(x1)
a  =  a
z_out_g(x1)  =  z_out_g
b  =  b
c  =  c
n_out_ga(x1, x2)  =  n_out_ga(x2)
lbrace  =  lbrace
U8_ga(x1, x2, x3)  =  U8_ga(x3)
U2_ga(x1, x2, x3)  =  U2_ga(x3)
U5_ga(x1, x2, x3)  =  U5_ga(x3)
star  =  star
U6_ga(x1, x2, x3)  =  U6_ga(x3)
t_out_ga(x1, x2)  =  t_out_ga(x2)
plus  =  plus
U3_ga(x1, x2, x3)  =  U3_ga(x3)
e_out_ga(x1, x2)  =  e_out_ga(x2)
rbrace  =  rbrace
E_IN_GA(x1, x2)  =  E_IN_GA(x1)
U1_GA(x1, x2, x3)  =  U1_GA(x3)
T_IN_GA(x1, x2)  =  T_IN_GA(x1)
U4_GA(x1, x2, x3)  =  U4_GA(x3)
N_IN_GA(x1, x2)  =  N_IN_GA(x1)
U7_GA(x1, x2, x3)  =  U7_GA(x2, x3)
Z_IN_G(x1)  =  Z_IN_G(x1)
U8_GA(x1, x2, x3)  =  U8_GA(x3)
U2_GA(x1, x2, x3)  =  U2_GA(x3)
U5_GA(x1, x2, x3)  =  U5_GA(x3)
U6_GA(x1, x2, x3)  =  U6_GA(x3)
U3_GA(x1, x2, x3)  =  U3_GA(x3)

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

(4) Obligation:

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

E_IN_GA(L, T) → U1_GA(L, T, t_in_ga(L, T))
E_IN_GA(L, T) → T_IN_GA(L, T)
T_IN_GA(L, T) → U4_GA(L, T, n_in_ga(L, T))
T_IN_GA(L, T) → N_IN_GA(L, T)
N_IN_GA(.(L, T), T) → U7_GA(L, T, z_in_g(L))
N_IN_GA(.(L, T), T) → Z_IN_G(L)
N_IN_GA(.(lbrace, A), B) → U8_GA(A, B, e_in_ga(A, .(rbrace, B)))
N_IN_GA(.(lbrace, A), B) → E_IN_GA(A, .(rbrace, B))
E_IN_GA(L, T) → U2_GA(L, T, t_in_ga(L, .(plus, C)))
E_IN_GA(L, T) → T_IN_GA(L, .(plus, C))
T_IN_GA(L, T) → U5_GA(L, T, n_in_ga(L, .(star, C)))
T_IN_GA(L, T) → N_IN_GA(L, .(star, C))
U5_GA(L, T, n_out_ga(L, .(star, C))) → U6_GA(L, T, t_in_ga(C, T))
U5_GA(L, T, n_out_ga(L, .(star, C))) → T_IN_GA(C, T)
U2_GA(L, T, t_out_ga(L, .(plus, C))) → U3_GA(L, T, e_in_ga(C, T))
U2_GA(L, T, t_out_ga(L, .(plus, C))) → E_IN_GA(C, T)

The TRS R consists of the following rules:

e_in_ga(L, T) → U1_ga(L, T, t_in_ga(L, T))
t_in_ga(L, T) → U4_ga(L, T, n_in_ga(L, T))
n_in_ga(.(L, T), T) → U7_ga(L, T, z_in_g(L))
z_in_g(a) → z_out_g(a)
z_in_g(b) → z_out_g(b)
z_in_g(c) → z_out_g(c)
U7_ga(L, T, z_out_g(L)) → n_out_ga(.(L, T), T)
n_in_ga(.(lbrace, A), B) → U8_ga(A, B, e_in_ga(A, .(rbrace, B)))
e_in_ga(L, T) → U2_ga(L, T, t_in_ga(L, .(plus, C)))
t_in_ga(L, T) → U5_ga(L, T, n_in_ga(L, .(star, C)))
U5_ga(L, T, n_out_ga(L, .(star, C))) → U6_ga(L, T, t_in_ga(C, T))
U6_ga(L, T, t_out_ga(C, T)) → t_out_ga(L, T)
U2_ga(L, T, t_out_ga(L, .(plus, C))) → U3_ga(L, T, e_in_ga(C, T))
U3_ga(L, T, e_out_ga(C, T)) → e_out_ga(L, T)
U8_ga(A, B, e_out_ga(A, .(rbrace, B))) → n_out_ga(.(lbrace, A), B)
U4_ga(L, T, n_out_ga(L, T)) → t_out_ga(L, T)
U1_ga(L, T, t_out_ga(L, T)) → e_out_ga(L, T)

The argument filtering Pi contains the following mapping:
e_in_ga(x1, x2)  =  e_in_ga(x1)
U1_ga(x1, x2, x3)  =  U1_ga(x3)
t_in_ga(x1, x2)  =  t_in_ga(x1)
U4_ga(x1, x2, x3)  =  U4_ga(x3)
n_in_ga(x1, x2)  =  n_in_ga(x1)
.(x1, x2)  =  .(x1, x2)
U7_ga(x1, x2, x3)  =  U7_ga(x2, x3)
z_in_g(x1)  =  z_in_g(x1)
a  =  a
z_out_g(x1)  =  z_out_g
b  =  b
c  =  c
n_out_ga(x1, x2)  =  n_out_ga(x2)
lbrace  =  lbrace
U8_ga(x1, x2, x3)  =  U8_ga(x3)
U2_ga(x1, x2, x3)  =  U2_ga(x3)
U5_ga(x1, x2, x3)  =  U5_ga(x3)
star  =  star
U6_ga(x1, x2, x3)  =  U6_ga(x3)
t_out_ga(x1, x2)  =  t_out_ga(x2)
plus  =  plus
U3_ga(x1, x2, x3)  =  U3_ga(x3)
e_out_ga(x1, x2)  =  e_out_ga(x2)
rbrace  =  rbrace
E_IN_GA(x1, x2)  =  E_IN_GA(x1)
U1_GA(x1, x2, x3)  =  U1_GA(x3)
T_IN_GA(x1, x2)  =  T_IN_GA(x1)
U4_GA(x1, x2, x3)  =  U4_GA(x3)
N_IN_GA(x1, x2)  =  N_IN_GA(x1)
U7_GA(x1, x2, x3)  =  U7_GA(x2, x3)
Z_IN_G(x1)  =  Z_IN_G(x1)
U8_GA(x1, x2, x3)  =  U8_GA(x3)
U2_GA(x1, x2, x3)  =  U2_GA(x3)
U5_GA(x1, x2, x3)  =  U5_GA(x3)
U6_GA(x1, x2, x3)  =  U6_GA(x3)
U3_GA(x1, x2, x3)  =  U3_GA(x3)

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

(5) DependencyGraphProof (EQUIVALENT transformation)

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

(6) Obligation:

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

E_IN_GA(L, T) → T_IN_GA(L, T)
T_IN_GA(L, T) → N_IN_GA(L, T)
N_IN_GA(.(lbrace, A), B) → E_IN_GA(A, .(rbrace, B))
E_IN_GA(L, T) → U2_GA(L, T, t_in_ga(L, .(plus, C)))
U2_GA(L, T, t_out_ga(L, .(plus, C))) → E_IN_GA(C, T)
E_IN_GA(L, T) → T_IN_GA(L, .(plus, C))
T_IN_GA(L, T) → U5_GA(L, T, n_in_ga(L, .(star, C)))
U5_GA(L, T, n_out_ga(L, .(star, C))) → T_IN_GA(C, T)
T_IN_GA(L, T) → N_IN_GA(L, .(star, C))

The TRS R consists of the following rules:

e_in_ga(L, T) → U1_ga(L, T, t_in_ga(L, T))
t_in_ga(L, T) → U4_ga(L, T, n_in_ga(L, T))
n_in_ga(.(L, T), T) → U7_ga(L, T, z_in_g(L))
z_in_g(a) → z_out_g(a)
z_in_g(b) → z_out_g(b)
z_in_g(c) → z_out_g(c)
U7_ga(L, T, z_out_g(L)) → n_out_ga(.(L, T), T)
n_in_ga(.(lbrace, A), B) → U8_ga(A, B, e_in_ga(A, .(rbrace, B)))
e_in_ga(L, T) → U2_ga(L, T, t_in_ga(L, .(plus, C)))
t_in_ga(L, T) → U5_ga(L, T, n_in_ga(L, .(star, C)))
U5_ga(L, T, n_out_ga(L, .(star, C))) → U6_ga(L, T, t_in_ga(C, T))
U6_ga(L, T, t_out_ga(C, T)) → t_out_ga(L, T)
U2_ga(L, T, t_out_ga(L, .(plus, C))) → U3_ga(L, T, e_in_ga(C, T))
U3_ga(L, T, e_out_ga(C, T)) → e_out_ga(L, T)
U8_ga(A, B, e_out_ga(A, .(rbrace, B))) → n_out_ga(.(lbrace, A), B)
U4_ga(L, T, n_out_ga(L, T)) → t_out_ga(L, T)
U1_ga(L, T, t_out_ga(L, T)) → e_out_ga(L, T)

The argument filtering Pi contains the following mapping:
e_in_ga(x1, x2)  =  e_in_ga(x1)
U1_ga(x1, x2, x3)  =  U1_ga(x3)
t_in_ga(x1, x2)  =  t_in_ga(x1)
U4_ga(x1, x2, x3)  =  U4_ga(x3)
n_in_ga(x1, x2)  =  n_in_ga(x1)
.(x1, x2)  =  .(x1, x2)
U7_ga(x1, x2, x3)  =  U7_ga(x2, x3)
z_in_g(x1)  =  z_in_g(x1)
a  =  a
z_out_g(x1)  =  z_out_g
b  =  b
c  =  c
n_out_ga(x1, x2)  =  n_out_ga(x2)
lbrace  =  lbrace
U8_ga(x1, x2, x3)  =  U8_ga(x3)
U2_ga(x1, x2, x3)  =  U2_ga(x3)
U5_ga(x1, x2, x3)  =  U5_ga(x3)
star  =  star
U6_ga(x1, x2, x3)  =  U6_ga(x3)
t_out_ga(x1, x2)  =  t_out_ga(x2)
plus  =  plus
U3_ga(x1, x2, x3)  =  U3_ga(x3)
e_out_ga(x1, x2)  =  e_out_ga(x2)
rbrace  =  rbrace
E_IN_GA(x1, x2)  =  E_IN_GA(x1)
T_IN_GA(x1, x2)  =  T_IN_GA(x1)
N_IN_GA(x1, x2)  =  N_IN_GA(x1)
U2_GA(x1, x2, x3)  =  U2_GA(x3)
U5_GA(x1, x2, x3)  =  U5_GA(x3)

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

(7) PiDPToQDPProof (SOUND transformation)

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

(8) Obligation:

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

E_IN_GA(L) → T_IN_GA(L)
T_IN_GA(L) → N_IN_GA(L)
N_IN_GA(.(lbrace, A)) → E_IN_GA(A)
E_IN_GA(L) → U2_GA(t_in_ga(L))
U2_GA(t_out_ga(.(plus, C))) → E_IN_GA(C)
T_IN_GA(L) → U5_GA(n_in_ga(L))
U5_GA(n_out_ga(.(star, C))) → T_IN_GA(C)

The TRS R consists of the following rules:

e_in_ga(L) → U1_ga(t_in_ga(L))
t_in_ga(L) → U4_ga(n_in_ga(L))
n_in_ga(.(L, T)) → U7_ga(T, z_in_g(L))
z_in_g(a) → z_out_g
z_in_g(b) → z_out_g
z_in_g(c) → z_out_g
U7_ga(T, z_out_g) → n_out_ga(T)
n_in_ga(.(lbrace, A)) → U8_ga(e_in_ga(A))
e_in_ga(L) → U2_ga(t_in_ga(L))
t_in_ga(L) → U5_ga(n_in_ga(L))
U5_ga(n_out_ga(.(star, C))) → U6_ga(t_in_ga(C))
U6_ga(t_out_ga(T)) → t_out_ga(T)
U2_ga(t_out_ga(.(plus, C))) → U3_ga(e_in_ga(C))
U3_ga(e_out_ga(T)) → e_out_ga(T)
U8_ga(e_out_ga(.(rbrace, B))) → n_out_ga(B)
U4_ga(n_out_ga(T)) → t_out_ga(T)
U1_ga(t_out_ga(T)) → e_out_ga(T)

The set Q consists of the following terms:

e_in_ga(x0)
t_in_ga(x0)
n_in_ga(x0)
z_in_g(x0)
U7_ga(x0, x1)
U5_ga(x0)
U6_ga(x0)
U2_ga(x0)
U3_ga(x0)
U8_ga(x0)
U4_ga(x0)
U1_ga(x0)

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

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

N_IN_GA(.(lbrace, A)) → E_IN_GA(A)
U2_GA(t_out_ga(.(plus, C))) → E_IN_GA(C)
U5_GA(n_out_ga(.(star, C))) → T_IN_GA(C)

The following rules are removed from R:

n_in_ga(.(L, T)) → U7_ga(T, z_in_g(L))
n_in_ga(.(lbrace, A)) → U8_ga(e_in_ga(A))
U8_ga(e_out_ga(.(rbrace, B))) → n_out_ga(B)
U2_ga(t_out_ga(.(plus, C))) → U3_ga(e_in_ga(C))
U5_ga(n_out_ga(.(star, C))) → U6_ga(t_in_ga(C))
U6_ga(t_out_ga(T)) → t_out_ga(T)
U4_ga(n_out_ga(T)) → t_out_ga(T)
z_in_g(a) → z_out_g
z_in_g(b) → z_out_g
z_in_g(c) → z_out_g
U7_ga(T, z_out_g) → n_out_ga(T)

Used ordering: POLO with Polynomial interpretation [POLO]:

POL(.(x₁, x₂)) = x₁ + 2·x₂   
POL(E_IN_GA(x₁)) = 2·x₁   
POL(N_IN_GA(x₁)) = x₁   
POL(T_IN_GA(x₁)) = x₁   
POL(U1_ga(x₁)) = x₁   
POL(U2_GA(x₁)) = 2·x₁   
POL(U2_ga(x₁)) = x₁   
POL(U3_ga(x₁)) = x₁   
POL(U4_ga(x₁)) = x₁   
POL(U5_GA(x₁)) = x₁   
POL(U5_ga(x₁)) = x₁   
POL(U6_ga(x₁)) = 1 + 2·x₁   
POL(U7_ga(x₁, x₂)) = 2·x₁ + x₂   
POL(U8_ga(x₁)) = 1 + 2·x₁   
POL(a) = 2   
POL(b) = 2   
POL(c) = 2   
POL(e_in_ga(x₁)) = x₁   
POL(e_out_ga(x₁)) = x₁   
POL(lbrace) = 1   
POL(n_in_ga(x₁)) = x₁   
POL(n_out_ga(x₁)) = 1 + x₁   
POL(plus) = 0   
POL(rbrace) = 1   
POL(star) = 1   
POL(t_in_ga(x₁)) = x₁   
POL(t_out_ga(x₁)) = x₁   
POL(z_in_g(x₁)) = x₁   
POL(z_out_g) = 2   

(10) Obligation:

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

E_IN_GA(L) → T_IN_GA(L)
T_IN_GA(L) → N_IN_GA(L)
E_IN_GA(L) → U2_GA(t_in_ga(L))
T_IN_GA(L) → U5_GA(n_in_ga(L))

The TRS R consists of the following rules:

e_in_ga(L) → U1_ga(t_in_ga(L))
e_in_ga(L) → U2_ga(t_in_ga(L))
t_in_ga(L) → U4_ga(n_in_ga(L))
t_in_ga(L) → U5_ga(n_in_ga(L))
U3_ga(e_out_ga(T)) → e_out_ga(T)
U1_ga(t_out_ga(T)) → e_out_ga(T)

The set Q consists of the following terms:

e_in_ga(x0)
t_in_ga(x0)
n_in_ga(x0)
z_in_g(x0)
U7_ga(x0, x1)
U5_ga(x0)
U6_ga(x0)
U2_ga(x0)
U3_ga(x0)
U8_ga(x0)
U4_ga(x0)
U1_ga(x0)

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

(11) DependencyGraphProof (EQUIVALENT transformation)

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

(12) TRUE

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

e_in_ga(L, T) → U1_ga(L, T, t_in_ga(L, T))
t_in_ga(L, T) → U4_ga(L, T, n_in_ga(L, T))
n_in_ga(.(L, T), T) → U7_ga(L, T, z_in_g(L))
z_in_g(a) → z_out_g(a)
z_in_g(b) → z_out_g(b)
z_in_g(c) → z_out_g(c)
U7_ga(L, T, z_out_g(L)) → n_out_ga(.(L, T), T)
n_in_ga(.(lbrace, A), B) → U8_ga(A, B, e_in_ga(A, .(rbrace, B)))
e_in_ga(L, T) → U2_ga(L, T, t_in_ga(L, .(plus, C)))
t_in_ga(L, T) → U5_ga(L, T, n_in_ga(L, .(star, C)))
U5_ga(L, T, n_out_ga(L, .(star, C))) → U6_ga(L, T, t_in_ga(C, T))
U6_ga(L, T, t_out_ga(C, T)) → t_out_ga(L, T)
U2_ga(L, T, t_out_ga(L, .(plus, C))) → U3_ga(L, T, e_in_ga(C, T))
U3_ga(L, T, e_out_ga(C, T)) → e_out_ga(L, T)
U8_ga(A, B, e_out_ga(A, .(rbrace, B))) → n_out_ga(.(lbrace, A), B)
U4_ga(L, T, n_out_ga(L, T)) → t_out_ga(L, T)
U1_ga(L, T, t_out_ga(L, T)) → e_out_ga(L, T)

The argument filtering Pi contains the following mapping:
e_in_ga(x1, x2)  =  e_in_ga(x1)
U1_ga(x1, x2, x3)  =  U1_ga(x1, x3)
t_in_ga(x1, x2)  =  t_in_ga(x1)
U4_ga(x1, x2, x3)  =  U4_ga(x1, x3)
n_in_ga(x1, x2)  =  n_in_ga(x1)
.(x1, x2)  =  .(x1, x2)
U7_ga(x1, x2, x3)  =  U7_ga(x1, x2, x3)
z_in_g(x1)  =  z_in_g(x1)
a  =  a
z_out_g(x1)  =  z_out_g(x1)
b  =  b
c  =  c
n_out_ga(x1, x2)  =  n_out_ga(x1, x2)
lbrace  =  lbrace
U8_ga(x1, x2, x3)  =  U8_ga(x1, x3)
U2_ga(x1, x2, x3)  =  U2_ga(x1, x3)
U5_ga(x1, x2, x3)  =  U5_ga(x1, x3)
star  =  star
U6_ga(x1, x2, x3)  =  U6_ga(x1, x3)
t_out_ga(x1, x2)  =  t_out_ga(x1, x2)
plus  =  plus
U3_ga(x1, x2, x3)  =  U3_ga(x1, x3)
e_out_ga(x1, x2)  =  e_out_ga(x1, x2)
rbrace  =  rbrace

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog

(14) Obligation:

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

e_in_ga(L, T) → U1_ga(L, T, t_in_ga(L, T))
t_in_ga(L, T) → U4_ga(L, T, n_in_ga(L, T))
n_in_ga(.(L, T), T) → U7_ga(L, T, z_in_g(L))
z_in_g(a) → z_out_g(a)
z_in_g(b) → z_out_g(b)
z_in_g(c) → z_out_g(c)
U7_ga(L, T, z_out_g(L)) → n_out_ga(.(L, T), T)
n_in_ga(.(lbrace, A), B) → U8_ga(A, B, e_in_ga(A, .(rbrace, B)))
e_in_ga(L, T) → U2_ga(L, T, t_in_ga(L, .(plus, C)))
t_in_ga(L, T) → U5_ga(L, T, n_in_ga(L, .(star, C)))
U5_ga(L, T, n_out_ga(L, .(star, C))) → U6_ga(L, T, t_in_ga(C, T))
U6_ga(L, T, t_out_ga(C, T)) → t_out_ga(L, T)
U2_ga(L, T, t_out_ga(L, .(plus, C))) → U3_ga(L, T, e_in_ga(C, T))
U3_ga(L, T, e_out_ga(C, T)) → e_out_ga(L, T)
U8_ga(A, B, e_out_ga(A, .(rbrace, B))) → n_out_ga(.(lbrace, A), B)
U4_ga(L, T, n_out_ga(L, T)) → t_out_ga(L, T)
U1_ga(L, T, t_out_ga(L, T)) → e_out_ga(L, T)

The argument filtering Pi contains the following mapping:
e_in_ga(x1, x2)  =  e_in_ga(x1)
U1_ga(x1, x2, x3)  =  U1_ga(x1, x3)
t_in_ga(x1, x2)  =  t_in_ga(x1)
U4_ga(x1, x2, x3)  =  U4_ga(x1, x3)
n_in_ga(x1, x2)  =  n_in_ga(x1)
.(x1, x2)  =  .(x1, x2)
U7_ga(x1, x2, x3)  =  U7_ga(x1, x2, x3)
z_in_g(x1)  =  z_in_g(x1)
a  =  a
z_out_g(x1)  =  z_out_g(x1)
b  =  b
c  =  c
n_out_ga(x1, x2)  =  n_out_ga(x1, x2)
lbrace  =  lbrace
U8_ga(x1, x2, x3)  =  U8_ga(x1, x3)
U2_ga(x1, x2, x3)  =  U2_ga(x1, x3)
U5_ga(x1, x2, x3)  =  U5_ga(x1, x3)
star  =  star
U6_ga(x1, x2, x3)  =  U6_ga(x1, x3)
t_out_ga(x1, x2)  =  t_out_ga(x1, x2)
plus  =  plus
U3_ga(x1, x2, x3)  =  U3_ga(x1, x3)
e_out_ga(x1, x2)  =  e_out_ga(x1, x2)
rbrace  =  rbrace

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

E_IN_GA(L, T) → U1_GA(L, T, t_in_ga(L, T))
E_IN_GA(L, T) → T_IN_GA(L, T)
T_IN_GA(L, T) → U4_GA(L, T, n_in_ga(L, T))
T_IN_GA(L, T) → N_IN_GA(L, T)
N_IN_GA(.(L, T), T) → U7_GA(L, T, z_in_g(L))
N_IN_GA(.(L, T), T) → Z_IN_G(L)
N_IN_GA(.(lbrace, A), B) → U8_GA(A, B, e_in_ga(A, .(rbrace, B)))
N_IN_GA(.(lbrace, A), B) → E_IN_GA(A, .(rbrace, B))
E_IN_GA(L, T) → U2_GA(L, T, t_in_ga(L, .(plus, C)))
E_IN_GA(L, T) → T_IN_GA(L, .(plus, C))
T_IN_GA(L, T) → U5_GA(L, T, n_in_ga(L, .(star, C)))
T_IN_GA(L, T) → N_IN_GA(L, .(star, C))
U5_GA(L, T, n_out_ga(L, .(star, C))) → U6_GA(L, T, t_in_ga(C, T))
U5_GA(L, T, n_out_ga(L, .(star, C))) → T_IN_GA(C, T)
U2_GA(L, T, t_out_ga(L, .(plus, C))) → U3_GA(L, T, e_in_ga(C, T))
U2_GA(L, T, t_out_ga(L, .(plus, C))) → E_IN_GA(C, T)

The TRS R consists of the following rules:

e_in_ga(L, T) → U1_ga(L, T, t_in_ga(L, T))
t_in_ga(L, T) → U4_ga(L, T, n_in_ga(L, T))
n_in_ga(.(L, T), T) → U7_ga(L, T, z_in_g(L))
z_in_g(a) → z_out_g(a)
z_in_g(b) → z_out_g(b)
z_in_g(c) → z_out_g(c)
U7_ga(L, T, z_out_g(L)) → n_out_ga(.(L, T), T)
n_in_ga(.(lbrace, A), B) → U8_ga(A, B, e_in_ga(A, .(rbrace, B)))
e_in_ga(L, T) → U2_ga(L, T, t_in_ga(L, .(plus, C)))
t_in_ga(L, T) → U5_ga(L, T, n_in_ga(L, .(star, C)))
U5_ga(L, T, n_out_ga(L, .(star, C))) → U6_ga(L, T, t_in_ga(C, T))
U6_ga(L, T, t_out_ga(C, T)) → t_out_ga(L, T)
U2_ga(L, T, t_out_ga(L, .(plus, C))) → U3_ga(L, T, e_in_ga(C, T))
U3_ga(L, T, e_out_ga(C, T)) → e_out_ga(L, T)
U8_ga(A, B, e_out_ga(A, .(rbrace, B))) → n_out_ga(.(lbrace, A), B)
U4_ga(L, T, n_out_ga(L, T)) → t_out_ga(L, T)
U1_ga(L, T, t_out_ga(L, T)) → e_out_ga(L, T)

The argument filtering Pi contains the following mapping:
e_in_ga(x1, x2)  =  e_in_ga(x1)
U1_ga(x1, x2, x3)  =  U1_ga(x1, x3)
t_in_ga(x1, x2)  =  t_in_ga(x1)
U4_ga(x1, x2, x3)  =  U4_ga(x1, x3)
n_in_ga(x1, x2)  =  n_in_ga(x1)
.(x1, x2)  =  .(x1, x2)
U7_ga(x1, x2, x3)  =  U7_ga(x1, x2, x3)
z_in_g(x1)  =  z_in_g(x1)
a  =  a
z_out_g(x1)  =  z_out_g(x1)
b  =  b
c  =  c
n_out_ga(x1, x2)  =  n_out_ga(x1, x2)
lbrace  =  lbrace
U8_ga(x1, x2, x3)  =  U8_ga(x1, x3)
U2_ga(x1, x2, x3)  =  U2_ga(x1, x3)
U5_ga(x1, x2, x3)  =  U5_ga(x1, x3)
star  =  star
U6_ga(x1, x2, x3)  =  U6_ga(x1, x3)
t_out_ga(x1, x2)  =  t_out_ga(x1, x2)
plus  =  plus
U3_ga(x1, x2, x3)  =  U3_ga(x1, x3)
e_out_ga(x1, x2)  =  e_out_ga(x1, x2)
rbrace  =  rbrace
E_IN_GA(x1, x2)  =  E_IN_GA(x1)
U1_GA(x1, x2, x3)  =  U1_GA(x1, x3)
T_IN_GA(x1, x2)  =  T_IN_GA(x1)
U4_GA(x1, x2, x3)  =  U4_GA(x1, x3)
N_IN_GA(x1, x2)  =  N_IN_GA(x1)
U7_GA(x1, x2, x3)  =  U7_GA(x1, x2, x3)
Z_IN_G(x1)  =  Z_IN_G(x1)
U8_GA(x1, x2, x3)  =  U8_GA(x1, x3)
U2_GA(x1, x2, x3)  =  U2_GA(x1, x3)
U5_GA(x1, x2, x3)  =  U5_GA(x1, x3)
U6_GA(x1, x2, x3)  =  U6_GA(x1, x3)
U3_GA(x1, x2, x3)  =  U3_GA(x1, x3)

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

(16) Obligation:

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

E_IN_GA(L, T) → U1_GA(L, T, t_in_ga(L, T))
E_IN_GA(L, T) → T_IN_GA(L, T)
T_IN_GA(L, T) → U4_GA(L, T, n_in_ga(L, T))
T_IN_GA(L, T) → N_IN_GA(L, T)
N_IN_GA(.(L, T), T) → U7_GA(L, T, z_in_g(L))
N_IN_GA(.(L, T), T) → Z_IN_G(L)
N_IN_GA(.(lbrace, A), B) → U8_GA(A, B, e_in_ga(A, .(rbrace, B)))
N_IN_GA(.(lbrace, A), B) → E_IN_GA(A, .(rbrace, B))
E_IN_GA(L, T) → U2_GA(L, T, t_in_ga(L, .(plus, C)))
E_IN_GA(L, T) → T_IN_GA(L, .(plus, C))
T_IN_GA(L, T) → U5_GA(L, T, n_in_ga(L, .(star, C)))
T_IN_GA(L, T) → N_IN_GA(L, .(star, C))
U5_GA(L, T, n_out_ga(L, .(star, C))) → U6_GA(L, T, t_in_ga(C, T))
U5_GA(L, T, n_out_ga(L, .(star, C))) → T_IN_GA(C, T)
U2_GA(L, T, t_out_ga(L, .(plus, C))) → U3_GA(L, T, e_in_ga(C, T))
U2_GA(L, T, t_out_ga(L, .(plus, C))) → E_IN_GA(C, T)

The TRS R consists of the following rules:

e_in_ga(L, T) → U1_ga(L, T, t_in_ga(L, T))
t_in_ga(L, T) → U4_ga(L, T, n_in_ga(L, T))
n_in_ga(.(L, T), T) → U7_ga(L, T, z_in_g(L))
z_in_g(a) → z_out_g(a)
z_in_g(b) → z_out_g(b)
z_in_g(c) → z_out_g(c)
U7_ga(L, T, z_out_g(L)) → n_out_ga(.(L, T), T)
n_in_ga(.(lbrace, A), B) → U8_ga(A, B, e_in_ga(A, .(rbrace, B)))
e_in_ga(L, T) → U2_ga(L, T, t_in_ga(L, .(plus, C)))
t_in_ga(L, T) → U5_ga(L, T, n_in_ga(L, .(star, C)))
U5_ga(L, T, n_out_ga(L, .(star, C))) → U6_ga(L, T, t_in_ga(C, T))
U6_ga(L, T, t_out_ga(C, T)) → t_out_ga(L, T)
U2_ga(L, T, t_out_ga(L, .(plus, C))) → U3_ga(L, T, e_in_ga(C, T))
U3_ga(L, T, e_out_ga(C, T)) → e_out_ga(L, T)
U8_ga(A, B, e_out_ga(A, .(rbrace, B))) → n_out_ga(.(lbrace, A), B)
U4_ga(L, T, n_out_ga(L, T)) → t_out_ga(L, T)
U1_ga(L, T, t_out_ga(L, T)) → e_out_ga(L, T)

The argument filtering Pi contains the following mapping:
e_in_ga(x1, x2)  =  e_in_ga(x1)
U1_ga(x1, x2, x3)  =  U1_ga(x1, x3)
t_in_ga(x1, x2)  =  t_in_ga(x1)
U4_ga(x1, x2, x3)  =  U4_ga(x1, x3)
n_in_ga(x1, x2)  =  n_in_ga(x1)
.(x1, x2)  =  .(x1, x2)
U7_ga(x1, x2, x3)  =  U7_ga(x1, x2, x3)
z_in_g(x1)  =  z_in_g(x1)
a  =  a
z_out_g(x1)  =  z_out_g(x1)
b  =  b
c  =  c
n_out_ga(x1, x2)  =  n_out_ga(x1, x2)
lbrace  =  lbrace
U8_ga(x1, x2, x3)  =  U8_ga(x1, x3)
U2_ga(x1, x2, x3)  =  U2_ga(x1, x3)
U5_ga(x1, x2, x3)  =  U5_ga(x1, x3)
star  =  star
U6_ga(x1, x2, x3)  =  U6_ga(x1, x3)
t_out_ga(x1, x2)  =  t_out_ga(x1, x2)
plus  =  plus
U3_ga(x1, x2, x3)  =  U3_ga(x1, x3)
e_out_ga(x1, x2)  =  e_out_ga(x1, x2)
rbrace  =  rbrace
E_IN_GA(x1, x2)  =  E_IN_GA(x1)
U1_GA(x1, x2, x3)  =  U1_GA(x1, x3)
T_IN_GA(x1, x2)  =  T_IN_GA(x1)
U4_GA(x1, x2, x3)  =  U4_GA(x1, x3)
N_IN_GA(x1, x2)  =  N_IN_GA(x1)
U7_GA(x1, x2, x3)  =  U7_GA(x1, x2, x3)
Z_IN_G(x1)  =  Z_IN_G(x1)
U8_GA(x1, x2, x3)  =  U8_GA(x1, x3)
U2_GA(x1, x2, x3)  =  U2_GA(x1, x3)
U5_GA(x1, x2, x3)  =  U5_GA(x1, x3)
U6_GA(x1, x2, x3)  =  U6_GA(x1, x3)
U3_GA(x1, x2, x3)  =  U3_GA(x1, x3)

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:

E_IN_GA(L, T) → T_IN_GA(L, T)
T_IN_GA(L, T) → N_IN_GA(L, T)
N_IN_GA(.(lbrace, A), B) → E_IN_GA(A, .(rbrace, B))
E_IN_GA(L, T) → U2_GA(L, T, t_in_ga(L, .(plus, C)))
U2_GA(L, T, t_out_ga(L, .(plus, C))) → E_IN_GA(C, T)
E_IN_GA(L, T) → T_IN_GA(L, .(plus, C))
T_IN_GA(L, T) → U5_GA(L, T, n_in_ga(L, .(star, C)))
U5_GA(L, T, n_out_ga(L, .(star, C))) → T_IN_GA(C, T)
T_IN_GA(L, T) → N_IN_GA(L, .(star, C))

The TRS R consists of the following rules:

e_in_ga(L, T) → U1_ga(L, T, t_in_ga(L, T))
t_in_ga(L, T) → U4_ga(L, T, n_in_ga(L, T))
n_in_ga(.(L, T), T) → U7_ga(L, T, z_in_g(L))
z_in_g(a) → z_out_g(a)
z_in_g(b) → z_out_g(b)
z_in_g(c) → z_out_g(c)
U7_ga(L, T, z_out_g(L)) → n_out_ga(.(L, T), T)
n_in_ga(.(lbrace, A), B) → U8_ga(A, B, e_in_ga(A, .(rbrace, B)))
e_in_ga(L, T) → U2_ga(L, T, t_in_ga(L, .(plus, C)))
t_in_ga(L, T) → U5_ga(L, T, n_in_ga(L, .(star, C)))
U5_ga(L, T, n_out_ga(L, .(star, C))) → U6_ga(L, T, t_in_ga(C, T))
U6_ga(L, T, t_out_ga(C, T)) → t_out_ga(L, T)
U2_ga(L, T, t_out_ga(L, .(plus, C))) → U3_ga(L, T, e_in_ga(C, T))
U3_ga(L, T, e_out_ga(C, T)) → e_out_ga(L, T)
U8_ga(A, B, e_out_ga(A, .(rbrace, B))) → n_out_ga(.(lbrace, A), B)
U4_ga(L, T, n_out_ga(L, T)) → t_out_ga(L, T)
U1_ga(L, T, t_out_ga(L, T)) → e_out_ga(L, T)

The argument filtering Pi contains the following mapping:
e_in_ga(x1, x2)  =  e_in_ga(x1)
U1_ga(x1, x2, x3)  =  U1_ga(x1, x3)
t_in_ga(x1, x2)  =  t_in_ga(x1)
U4_ga(x1, x2, x3)  =  U4_ga(x1, x3)
n_in_ga(x1, x2)  =  n_in_ga(x1)
.(x1, x2)  =  .(x1, x2)
U7_ga(x1, x2, x3)  =  U7_ga(x1, x2, x3)
z_in_g(x1)  =  z_in_g(x1)
a  =  a
z_out_g(x1)  =  z_out_g(x1)
b  =  b
c  =  c
n_out_ga(x1, x2)  =  n_out_ga(x1, x2)
lbrace  =  lbrace
U8_ga(x1, x2, x3)  =  U8_ga(x1, x3)
U2_ga(x1, x2, x3)  =  U2_ga(x1, x3)
U5_ga(x1, x2, x3)  =  U5_ga(x1, x3)
star  =  star
U6_ga(x1, x2, x3)  =  U6_ga(x1, x3)
t_out_ga(x1, x2)  =  t_out_ga(x1, x2)
plus  =  plus
U3_ga(x1, x2, x3)  =  U3_ga(x1, x3)
e_out_ga(x1, x2)  =  e_out_ga(x1, x2)
rbrace  =  rbrace
E_IN_GA(x1, x2)  =  E_IN_GA(x1)
T_IN_GA(x1, x2)  =  T_IN_GA(x1)
N_IN_GA(x1, x2)  =  N_IN_GA(x1)
U2_GA(x1, x2, x3)  =  U2_GA(x1, x3)
U5_GA(x1, x2, x3)  =  U5_GA(x1, x3)

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

(19) PiDPToQDPProof (SOUND transformation)

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

(20) Obligation:

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

E_IN_GA(L) → T_IN_GA(L)
T_IN_GA(L) → N_IN_GA(L)
N_IN_GA(.(lbrace, A)) → E_IN_GA(A)
E_IN_GA(L) → U2_GA(L, t_in_ga(L))
U2_GA(L, t_out_ga(L, .(plus, C))) → E_IN_GA(C)
T_IN_GA(L) → U5_GA(L, n_in_ga(L))
U5_GA(L, n_out_ga(L, .(star, C))) → T_IN_GA(C)

The TRS R consists of the following rules:

e_in_ga(L) → U1_ga(L, t_in_ga(L))
t_in_ga(L) → U4_ga(L, n_in_ga(L))
n_in_ga(.(L, T)) → U7_ga(L, T, z_in_g(L))
z_in_g(a) → z_out_g(a)
z_in_g(b) → z_out_g(b)
z_in_g(c) → z_out_g(c)
U7_ga(L, T, z_out_g(L)) → n_out_ga(.(L, T), T)
n_in_ga(.(lbrace, A)) → U8_ga(A, e_in_ga(A))
e_in_ga(L) → U2_ga(L, t_in_ga(L))
t_in_ga(L) → U5_ga(L, n_in_ga(L))
U5_ga(L, n_out_ga(L, .(star, C))) → U6_ga(L, t_in_ga(C))
U6_ga(L, t_out_ga(C, T)) → t_out_ga(L, T)
U2_ga(L, t_out_ga(L, .(plus, C))) → U3_ga(L, e_in_ga(C))
U3_ga(L, e_out_ga(C, T)) → e_out_ga(L, T)
U8_ga(A, e_out_ga(A, .(rbrace, B))) → n_out_ga(.(lbrace, A), B)
U4_ga(L, n_out_ga(L, T)) → t_out_ga(L, T)
U1_ga(L, t_out_ga(L, T)) → e_out_ga(L, T)

The set Q consists of the following terms:

e_in_ga(x0)
t_in_ga(x0)
n_in_ga(x0)
z_in_g(x0)
U7_ga(x0, x1, x2)
U5_ga(x0, x1)
U6_ga(x0, x1)
U2_ga(x0, x1)
U3_ga(x0, x1)
U8_ga(x0, x1)
U4_ga(x0, x1)
U1_ga(x0, x1)

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