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

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

(0) Obligation:

Clauses:

goal(Name, Code) :- ','(eq(Name, .(First, Others)), ','(reduce(Others, s(0), First, Reduced), eq(Code, Reduced))).
reduce(X1, s(s(s(s(0)))), X2, []) :- !.
reduce([], X3, X4, []) :- !.
reduce(.(Current, Others), Count, Current, Code) :- ','(vowel_h_w_y(Current), ','(!, reduce(Others, Count, Current, Code))).
reduce(.(Letter, Others), Count, Letter, Code) :- ','(!, reduce(Others, Count, Letter, Code)).
reduce(.(Current, Others), Count, X5, .(Current, Code)) :- reduce(Others, s(Count), Current, Code).
vowel_h_w_y(97).
vowel_h_w_y(101).
vowel_h_w_y(105).
vowel_h_w_y(111).
vowel_h_w_y(117).
vowel_h_w_y(104).
vowel_h_w_y(119).
vowel_h_w_y(121).
eq(X, X).

Queries:

goal(g,a).

(1) CutEliminatorProof (SOUND transformation)

Eliminated all cuts by simply ignoring them[PROLOG].

(2) Obligation:

Clauses:

goal(Name, Code) :- ','(eq(Name, .(First, Others)), ','(reduce(Others, s(0), First, Reduced), eq(Code, Reduced))).
reduce(X1, s(s(s(s(0)))), X2, []) :- true.
reduce([], X3, X4, []) :- true.
reduce(.(Current, Others), Count, Current, Code) :- ','(vowel_h_w_y(Current), reduce(Others, Count, Current, Code)).
reduce(.(Letter, Others), Count, Letter, Code) :- reduce(Others, Count, Letter, Code).
reduce(.(Current, Others), Count, X5, .(Current, Code)) :- reduce(Others, s(Count), Current, Code).
vowel_h_w_y(97).
vowel_h_w_y(101).
vowel_h_w_y(105).
vowel_h_w_y(111).
vowel_h_w_y(117).
vowel_h_w_y(104).
vowel_h_w_y(119).
vowel_h_w_y(121).
eq(X, X).

Queries:

goal(g,a).

(3) UndefinedPredicateHandlerProof (SOUND transformation)

Added facts for all undefined predicates [PROLOG].

(4) Obligation:

Clauses:

goal(Name, Code) :- ','(eq(Name, .(First, Others)), ','(reduce(Others, s(0), First, Reduced), eq(Code, Reduced))).
reduce(X1, s(s(s(s(0)))), X2, []) :- true.
reduce([], X3, X4, []) :- true.
reduce(.(Current, Others), Count, Current, Code) :- ','(vowel_h_w_y(Current), reduce(Others, Count, Current, Code)).
reduce(.(Letter, Others), Count, Letter, Code) :- reduce(Others, Count, Letter, Code).
reduce(.(Current, Others), Count, X5, .(Current, Code)) :- reduce(Others, s(Count), Current, Code).
vowel_h_w_y(97).
vowel_h_w_y(101).
vowel_h_w_y(105).
vowel_h_w_y(111).
vowel_h_w_y(117).
vowel_h_w_y(104).
vowel_h_w_y(119).
vowel_h_w_y(121).
eq(X, X).
true.

Queries:

goal(g,a).

(5) PrologToPiTRSProof (SOUND transformation)

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

goal_in_ga(Name, Code) → U1_ga(Name, Code, eq_in_ga(Name, .(First, Others)))
eq_in_ga(X, X) → eq_out_ga(X, X)
U1_ga(Name, Code, eq_out_ga(Name, .(First, Others))) → U2_ga(Name, Code, reduce_in_ggaa(Others, s(0), First, Reduced))
reduce_in_ggaa(X1, s(s(s(s(0)))), X2, []) → U4_ggaa(X1, X2, true_in_)
true_in_ → true_out_
U4_ggaa(X1, X2, true_out_) → reduce_out_ggaa(X1, s(s(s(s(0)))), X2, [])
reduce_in_ggaa([], X3, X4, []) → U5_ggaa(X3, X4, true_in_)
U5_ggaa(X3, X4, true_out_) → reduce_out_ggaa([], X3, X4, [])
reduce_in_ggaa(.(Current, Others), Count, Current, Code) → U6_ggaa(Current, Others, Count, Code, vowel_h_w_y_in_a(Current))
vowel_h_w_y_in_a(97) → vowel_h_w_y_out_a(97)
vowel_h_w_y_in_a(101) → vowel_h_w_y_out_a(101)
vowel_h_w_y_in_a(105) → vowel_h_w_y_out_a(105)
vowel_h_w_y_in_a(111) → vowel_h_w_y_out_a(111)
vowel_h_w_y_in_a(117) → vowel_h_w_y_out_a(117)
vowel_h_w_y_in_a(104) → vowel_h_w_y_out_a(104)
vowel_h_w_y_in_a(119) → vowel_h_w_y_out_a(119)
vowel_h_w_y_in_a(121) → vowel_h_w_y_out_a(121)
U6_ggaa(Current, Others, Count, Code, vowel_h_w_y_out_a(Current)) → U7_ggaa(Current, Others, Count, Code, reduce_in_ggga(Others, Count, Current, Code))
reduce_in_ggga(X1, s(s(s(s(0)))), X2, []) → U4_ggga(X1, X2, true_in_)
U4_ggga(X1, X2, true_out_) → reduce_out_ggga(X1, s(s(s(s(0)))), X2, [])
reduce_in_ggga([], X3, X4, []) → U5_ggga(X3, X4, true_in_)
U5_ggga(X3, X4, true_out_) → reduce_out_ggga([], X3, X4, [])
reduce_in_ggga(.(Current, Others), Count, Current, Code) → U6_ggga(Current, Others, Count, Code, vowel_h_w_y_in_g(Current))
vowel_h_w_y_in_g(97) → vowel_h_w_y_out_g(97)
vowel_h_w_y_in_g(101) → vowel_h_w_y_out_g(101)
vowel_h_w_y_in_g(105) → vowel_h_w_y_out_g(105)
vowel_h_w_y_in_g(111) → vowel_h_w_y_out_g(111)
vowel_h_w_y_in_g(117) → vowel_h_w_y_out_g(117)
vowel_h_w_y_in_g(104) → vowel_h_w_y_out_g(104)
vowel_h_w_y_in_g(119) → vowel_h_w_y_out_g(119)
vowel_h_w_y_in_g(121) → vowel_h_w_y_out_g(121)
U6_ggga(Current, Others, Count, Code, vowel_h_w_y_out_g(Current)) → U7_ggga(Current, Others, Count, Code, reduce_in_ggga(Others, Count, Current, Code))
reduce_in_ggga(.(Letter, Others), Count, Letter, Code) → U8_ggga(Letter, Others, Count, Code, reduce_in_ggga(Others, Count, Letter, Code))
reduce_in_ggga(.(Current, Others), Count, X5, .(Current, Code)) → U9_ggga(Current, Others, Count, X5, Code, reduce_in_ggaa(Others, s(Count), Current, Code))
reduce_in_ggaa(.(Letter, Others), Count, Letter, Code) → U8_ggaa(Letter, Others, Count, Code, reduce_in_ggaa(Others, Count, Letter, Code))
reduce_in_ggaa(.(Current, Others), Count, X5, .(Current, Code)) → U9_ggaa(Current, Others, Count, X5, Code, reduce_in_ggaa(Others, s(Count), Current, Code))
U9_ggaa(Current, Others, Count, X5, Code, reduce_out_ggaa(Others, s(Count), Current, Code)) → reduce_out_ggaa(.(Current, Others), Count, X5, .(Current, Code))
U8_ggaa(Letter, Others, Count, Code, reduce_out_ggaa(Others, Count, Letter, Code)) → reduce_out_ggaa(.(Letter, Others), Count, Letter, Code)
U9_ggga(Current, Others, Count, X5, Code, reduce_out_ggaa(Others, s(Count), Current, Code)) → reduce_out_ggga(.(Current, Others), Count, X5, .(Current, Code))
U8_ggga(Letter, Others, Count, Code, reduce_out_ggga(Others, Count, Letter, Code)) → reduce_out_ggga(.(Letter, Others), Count, Letter, Code)
U7_ggga(Current, Others, Count, Code, reduce_out_ggga(Others, Count, Current, Code)) → reduce_out_ggga(.(Current, Others), Count, Current, Code)
U7_ggaa(Current, Others, Count, Code, reduce_out_ggga(Others, Count, Current, Code)) → reduce_out_ggaa(.(Current, Others), Count, Current, Code)
U2_ga(Name, Code, reduce_out_ggaa(Others, s(0), First, Reduced)) → U3_ga(Name, Code, eq_in_ag(Code, Reduced))
eq_in_ag(X, X) → eq_out_ag(X, X)
U3_ga(Name, Code, eq_out_ag(Code, Reduced)) → goal_out_ga(Name, Code)

The argument filtering Pi contains the following mapping:
goal_in_ga(x1, x2)  =  goal_in_ga(x1)
U1_ga(x1, x2, x3)  =  U1_ga(x3)
eq_in_ga(x1, x2)  =  eq_in_ga(x1)
.(x1, x2)  =  .(x2)
eq_out_ga(x1, x2)  =  eq_out_ga(x2)
U2_ga(x1, x2, x3)  =  U2_ga(x3)
reduce_in_ggaa(x1, x2, x3, x4)  =  reduce_in_ggaa(x1, x2)
s(x1)  =  s(x1)
0  =  0
U4_ggaa(x1, x2, x3)  =  U4_ggaa(x3)
true_in_  =  true_in_
true_out_  =  true_out_
reduce_out_ggaa(x1, x2, x3, x4)  =  reduce_out_ggaa(x4)
[]  =  []
U5_ggaa(x1, x2, x3)  =  U5_ggaa(x3)
U6_ggaa(x1, x2, x3, x4, x5)  =  U6_ggaa(x2, x3, x5)
vowel_h_w_y_in_a(x1)  =  vowel_h_w_y_in_a
vowel_h_w_y_out_a(x1)  =  vowel_h_w_y_out_a(x1)
U7_ggaa(x1, x2, x3, x4, x5)  =  U7_ggaa(x5)
reduce_in_ggga(x1, x2, x3, x4)  =  reduce_in_ggga(x1, x2, x3)
U4_ggga(x1, x2, x3)  =  U4_ggga(x3)
reduce_out_ggga(x1, x2, x3, x4)  =  reduce_out_ggga(x4)
U5_ggga(x1, x2, x3)  =  U5_ggga(x3)
U6_ggga(x1, x2, x3, x4, x5)  =  U6_ggga(x1, x2, x3, x5)
vowel_h_w_y_in_g(x1)  =  vowel_h_w_y_in_g(x1)
97  =  97
vowel_h_w_y_out_g(x1)  =  vowel_h_w_y_out_g
101  =  101
105  =  105
111  =  111
117  =  117
104  =  104
119  =  119
121  =  121
U7_ggga(x1, x2, x3, x4, x5)  =  U7_ggga(x5)
U8_ggga(x1, x2, x3, x4, x5)  =  U8_ggga(x5)
U9_ggga(x1, x2, x3, x4, x5, x6)  =  U9_ggga(x6)
U8_ggaa(x1, x2, x3, x4, x5)  =  U8_ggaa(x5)
U9_ggaa(x1, x2, x3, x4, x5, x6)  =  U9_ggaa(x6)
U3_ga(x1, x2, x3)  =  U3_ga(x3)
eq_in_ag(x1, x2)  =  eq_in_ag(x2)
eq_out_ag(x1, x2)  =  eq_out_ag(x1)
goal_out_ga(x1, x2)  =  goal_out_ga(x2)

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog

(6) Obligation:

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

goal_in_ga(Name, Code) → U1_ga(Name, Code, eq_in_ga(Name, .(First, Others)))
eq_in_ga(X, X) → eq_out_ga(X, X)
U1_ga(Name, Code, eq_out_ga(Name, .(First, Others))) → U2_ga(Name, Code, reduce_in_ggaa(Others, s(0), First, Reduced))
reduce_in_ggaa(X1, s(s(s(s(0)))), X2, []) → U4_ggaa(X1, X2, true_in_)
true_in_ → true_out_
U4_ggaa(X1, X2, true_out_) → reduce_out_ggaa(X1, s(s(s(s(0)))), X2, [])
reduce_in_ggaa([], X3, X4, []) → U5_ggaa(X3, X4, true_in_)
U5_ggaa(X3, X4, true_out_) → reduce_out_ggaa([], X3, X4, [])
reduce_in_ggaa(.(Current, Others), Count, Current, Code) → U6_ggaa(Current, Others, Count, Code, vowel_h_w_y_in_a(Current))
vowel_h_w_y_in_a(97) → vowel_h_w_y_out_a(97)
vowel_h_w_y_in_a(101) → vowel_h_w_y_out_a(101)
vowel_h_w_y_in_a(105) → vowel_h_w_y_out_a(105)
vowel_h_w_y_in_a(111) → vowel_h_w_y_out_a(111)
vowel_h_w_y_in_a(117) → vowel_h_w_y_out_a(117)
vowel_h_w_y_in_a(104) → vowel_h_w_y_out_a(104)
vowel_h_w_y_in_a(119) → vowel_h_w_y_out_a(119)
vowel_h_w_y_in_a(121) → vowel_h_w_y_out_a(121)
U6_ggaa(Current, Others, Count, Code, vowel_h_w_y_out_a(Current)) → U7_ggaa(Current, Others, Count, Code, reduce_in_ggga(Others, Count, Current, Code))
reduce_in_ggga(X1, s(s(s(s(0)))), X2, []) → U4_ggga(X1, X2, true_in_)
U4_ggga(X1, X2, true_out_) → reduce_out_ggga(X1, s(s(s(s(0)))), X2, [])
reduce_in_ggga([], X3, X4, []) → U5_ggga(X3, X4, true_in_)
U5_ggga(X3, X4, true_out_) → reduce_out_ggga([], X3, X4, [])
reduce_in_ggga(.(Current, Others), Count, Current, Code) → U6_ggga(Current, Others, Count, Code, vowel_h_w_y_in_g(Current))
vowel_h_w_y_in_g(97) → vowel_h_w_y_out_g(97)
vowel_h_w_y_in_g(101) → vowel_h_w_y_out_g(101)
vowel_h_w_y_in_g(105) → vowel_h_w_y_out_g(105)
vowel_h_w_y_in_g(111) → vowel_h_w_y_out_g(111)
vowel_h_w_y_in_g(117) → vowel_h_w_y_out_g(117)
vowel_h_w_y_in_g(104) → vowel_h_w_y_out_g(104)
vowel_h_w_y_in_g(119) → vowel_h_w_y_out_g(119)
vowel_h_w_y_in_g(121) → vowel_h_w_y_out_g(121)
U6_ggga(Current, Others, Count, Code, vowel_h_w_y_out_g(Current)) → U7_ggga(Current, Others, Count, Code, reduce_in_ggga(Others, Count, Current, Code))
reduce_in_ggga(.(Letter, Others), Count, Letter, Code) → U8_ggga(Letter, Others, Count, Code, reduce_in_ggga(Others, Count, Letter, Code))
reduce_in_ggga(.(Current, Others), Count, X5, .(Current, Code)) → U9_ggga(Current, Others, Count, X5, Code, reduce_in_ggaa(Others, s(Count), Current, Code))
reduce_in_ggaa(.(Letter, Others), Count, Letter, Code) → U8_ggaa(Letter, Others, Count, Code, reduce_in_ggaa(Others, Count, Letter, Code))
reduce_in_ggaa(.(Current, Others), Count, X5, .(Current, Code)) → U9_ggaa(Current, Others, Count, X5, Code, reduce_in_ggaa(Others, s(Count), Current, Code))
U9_ggaa(Current, Others, Count, X5, Code, reduce_out_ggaa(Others, s(Count), Current, Code)) → reduce_out_ggaa(.(Current, Others), Count, X5, .(Current, Code))
U8_ggaa(Letter, Others, Count, Code, reduce_out_ggaa(Others, Count, Letter, Code)) → reduce_out_ggaa(.(Letter, Others), Count, Letter, Code)
U9_ggga(Current, Others, Count, X5, Code, reduce_out_ggaa(Others, s(Count), Current, Code)) → reduce_out_ggga(.(Current, Others), Count, X5, .(Current, Code))
U8_ggga(Letter, Others, Count, Code, reduce_out_ggga(Others, Count, Letter, Code)) → reduce_out_ggga(.(Letter, Others), Count, Letter, Code)
U7_ggga(Current, Others, Count, Code, reduce_out_ggga(Others, Count, Current, Code)) → reduce_out_ggga(.(Current, Others), Count, Current, Code)
U7_ggaa(Current, Others, Count, Code, reduce_out_ggga(Others, Count, Current, Code)) → reduce_out_ggaa(.(Current, Others), Count, Current, Code)
U2_ga(Name, Code, reduce_out_ggaa(Others, s(0), First, Reduced)) → U3_ga(Name, Code, eq_in_ag(Code, Reduced))
eq_in_ag(X, X) → eq_out_ag(X, X)
U3_ga(Name, Code, eq_out_ag(Code, Reduced)) → goal_out_ga(Name, Code)

The argument filtering Pi contains the following mapping:
goal_in_ga(x1, x2)  =  goal_in_ga(x1)
U1_ga(x1, x2, x3)  =  U1_ga(x3)
eq_in_ga(x1, x2)  =  eq_in_ga(x1)
.(x1, x2)  =  .(x2)
eq_out_ga(x1, x2)  =  eq_out_ga(x2)
U2_ga(x1, x2, x3)  =  U2_ga(x3)
reduce_in_ggaa(x1, x2, x3, x4)  =  reduce_in_ggaa(x1, x2)
s(x1)  =  s(x1)
0  =  0
U4_ggaa(x1, x2, x3)  =  U4_ggaa(x3)
true_in_  =  true_in_
true_out_  =  true_out_
reduce_out_ggaa(x1, x2, x3, x4)  =  reduce_out_ggaa(x4)
[]  =  []
U5_ggaa(x1, x2, x3)  =  U5_ggaa(x3)
U6_ggaa(x1, x2, x3, x4, x5)  =  U6_ggaa(x2, x3, x5)
vowel_h_w_y_in_a(x1)  =  vowel_h_w_y_in_a
vowel_h_w_y_out_a(x1)  =  vowel_h_w_y_out_a(x1)
U7_ggaa(x1, x2, x3, x4, x5)  =  U7_ggaa(x5)
reduce_in_ggga(x1, x2, x3, x4)  =  reduce_in_ggga(x1, x2, x3)
U4_ggga(x1, x2, x3)  =  U4_ggga(x3)
reduce_out_ggga(x1, x2, x3, x4)  =  reduce_out_ggga(x4)
U5_ggga(x1, x2, x3)  =  U5_ggga(x3)
U6_ggga(x1, x2, x3, x4, x5)  =  U6_ggga(x1, x2, x3, x5)
vowel_h_w_y_in_g(x1)  =  vowel_h_w_y_in_g(x1)
97  =  97
vowel_h_w_y_out_g(x1)  =  vowel_h_w_y_out_g
101  =  101
105  =  105
111  =  111
117  =  117
104  =  104
119  =  119
121  =  121
U7_ggga(x1, x2, x3, x4, x5)  =  U7_ggga(x5)
U8_ggga(x1, x2, x3, x4, x5)  =  U8_ggga(x5)
U9_ggga(x1, x2, x3, x4, x5, x6)  =  U9_ggga(x6)
U8_ggaa(x1, x2, x3, x4, x5)  =  U8_ggaa(x5)
U9_ggaa(x1, x2, x3, x4, x5, x6)  =  U9_ggaa(x6)
U3_ga(x1, x2, x3)  =  U3_ga(x3)
eq_in_ag(x1, x2)  =  eq_in_ag(x2)
eq_out_ag(x1, x2)  =  eq_out_ag(x1)
goal_out_ga(x1, x2)  =  goal_out_ga(x2)

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

GOAL_IN_GA(Name, Code) → U1_GA(Name, Code, eq_in_ga(Name, .(First, Others)))
GOAL_IN_GA(Name, Code) → EQ_IN_GA(Name, .(First, Others))
U1_GA(Name, Code, eq_out_ga(Name, .(First, Others))) → U2_GA(Name, Code, reduce_in_ggaa(Others, s(0), First, Reduced))
U1_GA(Name, Code, eq_out_ga(Name, .(First, Others))) → REDUCE_IN_GGAA(Others, s(0), First, Reduced)
REDUCE_IN_GGAA(X1, s(s(s(s(0)))), X2, []) → U4_GGAA(X1, X2, true_in_)
REDUCE_IN_GGAA(X1, s(s(s(s(0)))), X2, []) → TRUE_IN_
REDUCE_IN_GGAA([], X3, X4, []) → U5_GGAA(X3, X4, true_in_)
REDUCE_IN_GGAA([], X3, X4, []) → TRUE_IN_
REDUCE_IN_GGAA(.(Current, Others), Count, Current, Code) → U6_GGAA(Current, Others, Count, Code, vowel_h_w_y_in_a(Current))
REDUCE_IN_GGAA(.(Current, Others), Count, Current, Code) → VOWEL_H_W_Y_IN_A(Current)
U6_GGAA(Current, Others, Count, Code, vowel_h_w_y_out_a(Current)) → U7_GGAA(Current, Others, Count, Code, reduce_in_ggga(Others, Count, Current, Code))
U6_GGAA(Current, Others, Count, Code, vowel_h_w_y_out_a(Current)) → REDUCE_IN_GGGA(Others, Count, Current, Code)
REDUCE_IN_GGGA(X1, s(s(s(s(0)))), X2, []) → U4_GGGA(X1, X2, true_in_)
REDUCE_IN_GGGA(X1, s(s(s(s(0)))), X2, []) → TRUE_IN_
REDUCE_IN_GGGA([], X3, X4, []) → U5_GGGA(X3, X4, true_in_)
REDUCE_IN_GGGA([], X3, X4, []) → TRUE_IN_
REDUCE_IN_GGGA(.(Current, Others), Count, Current, Code) → U6_GGGA(Current, Others, Count, Code, vowel_h_w_y_in_g(Current))
REDUCE_IN_GGGA(.(Current, Others), Count, Current, Code) → VOWEL_H_W_Y_IN_G(Current)
U6_GGGA(Current, Others, Count, Code, vowel_h_w_y_out_g(Current)) → U7_GGGA(Current, Others, Count, Code, reduce_in_ggga(Others, Count, Current, Code))
U6_GGGA(Current, Others, Count, Code, vowel_h_w_y_out_g(Current)) → REDUCE_IN_GGGA(Others, Count, Current, Code)
REDUCE_IN_GGGA(.(Letter, Others), Count, Letter, Code) → U8_GGGA(Letter, Others, Count, Code, reduce_in_ggga(Others, Count, Letter, Code))
REDUCE_IN_GGGA(.(Letter, Others), Count, Letter, Code) → REDUCE_IN_GGGA(Others, Count, Letter, Code)
REDUCE_IN_GGGA(.(Current, Others), Count, X5, .(Current, Code)) → U9_GGGA(Current, Others, Count, X5, Code, reduce_in_ggaa(Others, s(Count), Current, Code))
REDUCE_IN_GGGA(.(Current, Others), Count, X5, .(Current, Code)) → REDUCE_IN_GGAA(Others, s(Count), Current, Code)
REDUCE_IN_GGAA(.(Letter, Others), Count, Letter, Code) → U8_GGAA(Letter, Others, Count, Code, reduce_in_ggaa(Others, Count, Letter, Code))
REDUCE_IN_GGAA(.(Letter, Others), Count, Letter, Code) → REDUCE_IN_GGAA(Others, Count, Letter, Code)
REDUCE_IN_GGAA(.(Current, Others), Count, X5, .(Current, Code)) → U9_GGAA(Current, Others, Count, X5, Code, reduce_in_ggaa(Others, s(Count), Current, Code))
REDUCE_IN_GGAA(.(Current, Others), Count, X5, .(Current, Code)) → REDUCE_IN_GGAA(Others, s(Count), Current, Code)
U2_GA(Name, Code, reduce_out_ggaa(Others, s(0), First, Reduced)) → U3_GA(Name, Code, eq_in_ag(Code, Reduced))
U2_GA(Name, Code, reduce_out_ggaa(Others, s(0), First, Reduced)) → EQ_IN_AG(Code, Reduced)

The TRS R consists of the following rules:

goal_in_ga(Name, Code) → U1_ga(Name, Code, eq_in_ga(Name, .(First, Others)))
eq_in_ga(X, X) → eq_out_ga(X, X)
U1_ga(Name, Code, eq_out_ga(Name, .(First, Others))) → U2_ga(Name, Code, reduce_in_ggaa(Others, s(0), First, Reduced))
reduce_in_ggaa(X1, s(s(s(s(0)))), X2, []) → U4_ggaa(X1, X2, true_in_)
true_in_ → true_out_
U4_ggaa(X1, X2, true_out_) → reduce_out_ggaa(X1, s(s(s(s(0)))), X2, [])
reduce_in_ggaa([], X3, X4, []) → U5_ggaa(X3, X4, true_in_)
U5_ggaa(X3, X4, true_out_) → reduce_out_ggaa([], X3, X4, [])
reduce_in_ggaa(.(Current, Others), Count, Current, Code) → U6_ggaa(Current, Others, Count, Code, vowel_h_w_y_in_a(Current))
vowel_h_w_y_in_a(97) → vowel_h_w_y_out_a(97)
vowel_h_w_y_in_a(101) → vowel_h_w_y_out_a(101)
vowel_h_w_y_in_a(105) → vowel_h_w_y_out_a(105)
vowel_h_w_y_in_a(111) → vowel_h_w_y_out_a(111)
vowel_h_w_y_in_a(117) → vowel_h_w_y_out_a(117)
vowel_h_w_y_in_a(104) → vowel_h_w_y_out_a(104)
vowel_h_w_y_in_a(119) → vowel_h_w_y_out_a(119)
vowel_h_w_y_in_a(121) → vowel_h_w_y_out_a(121)
U6_ggaa(Current, Others, Count, Code, vowel_h_w_y_out_a(Current)) → U7_ggaa(Current, Others, Count, Code, reduce_in_ggga(Others, Count, Current, Code))
reduce_in_ggga(X1, s(s(s(s(0)))), X2, []) → U4_ggga(X1, X2, true_in_)
U4_ggga(X1, X2, true_out_) → reduce_out_ggga(X1, s(s(s(s(0)))), X2, [])
reduce_in_ggga([], X3, X4, []) → U5_ggga(X3, X4, true_in_)
U5_ggga(X3, X4, true_out_) → reduce_out_ggga([], X3, X4, [])
reduce_in_ggga(.(Current, Others), Count, Current, Code) → U6_ggga(Current, Others, Count, Code, vowel_h_w_y_in_g(Current))
vowel_h_w_y_in_g(97) → vowel_h_w_y_out_g(97)
vowel_h_w_y_in_g(101) → vowel_h_w_y_out_g(101)
vowel_h_w_y_in_g(105) → vowel_h_w_y_out_g(105)
vowel_h_w_y_in_g(111) → vowel_h_w_y_out_g(111)
vowel_h_w_y_in_g(117) → vowel_h_w_y_out_g(117)
vowel_h_w_y_in_g(104) → vowel_h_w_y_out_g(104)
vowel_h_w_y_in_g(119) → vowel_h_w_y_out_g(119)
vowel_h_w_y_in_g(121) → vowel_h_w_y_out_g(121)
U6_ggga(Current, Others, Count, Code, vowel_h_w_y_out_g(Current)) → U7_ggga(Current, Others, Count, Code, reduce_in_ggga(Others, Count, Current, Code))
reduce_in_ggga(.(Letter, Others), Count, Letter, Code) → U8_ggga(Letter, Others, Count, Code, reduce_in_ggga(Others, Count, Letter, Code))
reduce_in_ggga(.(Current, Others), Count, X5, .(Current, Code)) → U9_ggga(Current, Others, Count, X5, Code, reduce_in_ggaa(Others, s(Count), Current, Code))
reduce_in_ggaa(.(Letter, Others), Count, Letter, Code) → U8_ggaa(Letter, Others, Count, Code, reduce_in_ggaa(Others, Count, Letter, Code))
reduce_in_ggaa(.(Current, Others), Count, X5, .(Current, Code)) → U9_ggaa(Current, Others, Count, X5, Code, reduce_in_ggaa(Others, s(Count), Current, Code))
U9_ggaa(Current, Others, Count, X5, Code, reduce_out_ggaa(Others, s(Count), Current, Code)) → reduce_out_ggaa(.(Current, Others), Count, X5, .(Current, Code))
U8_ggaa(Letter, Others, Count, Code, reduce_out_ggaa(Others, Count, Letter, Code)) → reduce_out_ggaa(.(Letter, Others), Count, Letter, Code)
U9_ggga(Current, Others, Count, X5, Code, reduce_out_ggaa(Others, s(Count), Current, Code)) → reduce_out_ggga(.(Current, Others), Count, X5, .(Current, Code))
U8_ggga(Letter, Others, Count, Code, reduce_out_ggga(Others, Count, Letter, Code)) → reduce_out_ggga(.(Letter, Others), Count, Letter, Code)
U7_ggga(Current, Others, Count, Code, reduce_out_ggga(Others, Count, Current, Code)) → reduce_out_ggga(.(Current, Others), Count, Current, Code)
U7_ggaa(Current, Others, Count, Code, reduce_out_ggga(Others, Count, Current, Code)) → reduce_out_ggaa(.(Current, Others), Count, Current, Code)
U2_ga(Name, Code, reduce_out_ggaa(Others, s(0), First, Reduced)) → U3_ga(Name, Code, eq_in_ag(Code, Reduced))
eq_in_ag(X, X) → eq_out_ag(X, X)
U3_ga(Name, Code, eq_out_ag(Code, Reduced)) → goal_out_ga(Name, Code)

The argument filtering Pi contains the following mapping:
goal_in_ga(x1, x2)  =  goal_in_ga(x1)
U1_ga(x1, x2, x3)  =  U1_ga(x3)
eq_in_ga(x1, x2)  =  eq_in_ga(x1)
.(x1, x2)  =  .(x2)
eq_out_ga(x1, x2)  =  eq_out_ga(x2)
U2_ga(x1, x2, x3)  =  U2_ga(x3)
reduce_in_ggaa(x1, x2, x3, x4)  =  reduce_in_ggaa(x1, x2)
s(x1)  =  s(x1)
0  =  0
U4_ggaa(x1, x2, x3)  =  U4_ggaa(x3)
true_in_  =  true_in_
true_out_  =  true_out_
reduce_out_ggaa(x1, x2, x3, x4)  =  reduce_out_ggaa(x4)
[]  =  []
U5_ggaa(x1, x2, x3)  =  U5_ggaa(x3)
U6_ggaa(x1, x2, x3, x4, x5)  =  U6_ggaa(x2, x3, x5)
vowel_h_w_y_in_a(x1)  =  vowel_h_w_y_in_a
vowel_h_w_y_out_a(x1)  =  vowel_h_w_y_out_a(x1)
U7_ggaa(x1, x2, x3, x4, x5)  =  U7_ggaa(x5)
reduce_in_ggga(x1, x2, x3, x4)  =  reduce_in_ggga(x1, x2, x3)
U4_ggga(x1, x2, x3)  =  U4_ggga(x3)
reduce_out_ggga(x1, x2, x3, x4)  =  reduce_out_ggga(x4)
U5_ggga(x1, x2, x3)  =  U5_ggga(x3)
U6_ggga(x1, x2, x3, x4, x5)  =  U6_ggga(x1, x2, x3, x5)
vowel_h_w_y_in_g(x1)  =  vowel_h_w_y_in_g(x1)
97  =  97
vowel_h_w_y_out_g(x1)  =  vowel_h_w_y_out_g
101  =  101
105  =  105
111  =  111
117  =  117
104  =  104
119  =  119
121  =  121
U7_ggga(x1, x2, x3, x4, x5)  =  U7_ggga(x5)
U8_ggga(x1, x2, x3, x4, x5)  =  U8_ggga(x5)
U9_ggga(x1, x2, x3, x4, x5, x6)  =  U9_ggga(x6)
U8_ggaa(x1, x2, x3, x4, x5)  =  U8_ggaa(x5)
U9_ggaa(x1, x2, x3, x4, x5, x6)  =  U9_ggaa(x6)
U3_ga(x1, x2, x3)  =  U3_ga(x3)
eq_in_ag(x1, x2)  =  eq_in_ag(x2)
eq_out_ag(x1, x2)  =  eq_out_ag(x1)
goal_out_ga(x1, x2)  =  goal_out_ga(x2)
GOAL_IN_GA(x1, x2)  =  GOAL_IN_GA(x1)
U1_GA(x1, x2, x3)  =  U1_GA(x3)
EQ_IN_GA(x1, x2)  =  EQ_IN_GA(x1)
U2_GA(x1, x2, x3)  =  U2_GA(x3)
REDUCE_IN_GGAA(x1, x2, x3, x4)  =  REDUCE_IN_GGAA(x1, x2)
U4_GGAA(x1, x2, x3)  =  U4_GGAA(x3)
TRUE_IN_  =  TRUE_IN_
U5_GGAA(x1, x2, x3)  =  U5_GGAA(x3)
U6_GGAA(x1, x2, x3, x4, x5)  =  U6_GGAA(x2, x3, x5)
VOWEL_H_W_Y_IN_A(x1)  =  VOWEL_H_W_Y_IN_A
U7_GGAA(x1, x2, x3, x4, x5)  =  U7_GGAA(x5)
REDUCE_IN_GGGA(x1, x2, x3, x4)  =  REDUCE_IN_GGGA(x1, x2, x3)
U4_GGGA(x1, x2, x3)  =  U4_GGGA(x3)
U5_GGGA(x1, x2, x3)  =  U5_GGGA(x3)
U6_GGGA(x1, x2, x3, x4, x5)  =  U6_GGGA(x1, x2, x3, x5)
VOWEL_H_W_Y_IN_G(x1)  =  VOWEL_H_W_Y_IN_G(x1)
U7_GGGA(x1, x2, x3, x4, x5)  =  U7_GGGA(x5)
U8_GGGA(x1, x2, x3, x4, x5)  =  U8_GGGA(x5)
U9_GGGA(x1, x2, x3, x4, x5, x6)  =  U9_GGGA(x6)
U8_GGAA(x1, x2, x3, x4, x5)  =  U8_GGAA(x5)
U9_GGAA(x1, x2, x3, x4, x5, x6)  =  U9_GGAA(x6)
U3_GA(x1, x2, x3)  =  U3_GA(x3)
EQ_IN_AG(x1, x2)  =  EQ_IN_AG(x2)

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

(8) Obligation:

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

GOAL_IN_GA(Name, Code) → U1_GA(Name, Code, eq_in_ga(Name, .(First, Others)))
GOAL_IN_GA(Name, Code) → EQ_IN_GA(Name, .(First, Others))
U1_GA(Name, Code, eq_out_ga(Name, .(First, Others))) → U2_GA(Name, Code, reduce_in_ggaa(Others, s(0), First, Reduced))
U1_GA(Name, Code, eq_out_ga(Name, .(First, Others))) → REDUCE_IN_GGAA(Others, s(0), First, Reduced)
REDUCE_IN_GGAA(X1, s(s(s(s(0)))), X2, []) → U4_GGAA(X1, X2, true_in_)
REDUCE_IN_GGAA(X1, s(s(s(s(0)))), X2, []) → TRUE_IN_
REDUCE_IN_GGAA([], X3, X4, []) → U5_GGAA(X3, X4, true_in_)
REDUCE_IN_GGAA([], X3, X4, []) → TRUE_IN_
REDUCE_IN_GGAA(.(Current, Others), Count, Current, Code) → U6_GGAA(Current, Others, Count, Code, vowel_h_w_y_in_a(Current))
REDUCE_IN_GGAA(.(Current, Others), Count, Current, Code) → VOWEL_H_W_Y_IN_A(Current)
U6_GGAA(Current, Others, Count, Code, vowel_h_w_y_out_a(Current)) → U7_GGAA(Current, Others, Count, Code, reduce_in_ggga(Others, Count, Current, Code))
U6_GGAA(Current, Others, Count, Code, vowel_h_w_y_out_a(Current)) → REDUCE_IN_GGGA(Others, Count, Current, Code)
REDUCE_IN_GGGA(X1, s(s(s(s(0)))), X2, []) → U4_GGGA(X1, X2, true_in_)
REDUCE_IN_GGGA(X1, s(s(s(s(0)))), X2, []) → TRUE_IN_
REDUCE_IN_GGGA([], X3, X4, []) → U5_GGGA(X3, X4, true_in_)
REDUCE_IN_GGGA([], X3, X4, []) → TRUE_IN_
REDUCE_IN_GGGA(.(Current, Others), Count, Current, Code) → U6_GGGA(Current, Others, Count, Code, vowel_h_w_y_in_g(Current))
REDUCE_IN_GGGA(.(Current, Others), Count, Current, Code) → VOWEL_H_W_Y_IN_G(Current)
U6_GGGA(Current, Others, Count, Code, vowel_h_w_y_out_g(Current)) → U7_GGGA(Current, Others, Count, Code, reduce_in_ggga(Others, Count, Current, Code))
U6_GGGA(Current, Others, Count, Code, vowel_h_w_y_out_g(Current)) → REDUCE_IN_GGGA(Others, Count, Current, Code)
REDUCE_IN_GGGA(.(Letter, Others), Count, Letter, Code) → U8_GGGA(Letter, Others, Count, Code, reduce_in_ggga(Others, Count, Letter, Code))
REDUCE_IN_GGGA(.(Letter, Others), Count, Letter, Code) → REDUCE_IN_GGGA(Others, Count, Letter, Code)
REDUCE_IN_GGGA(.(Current, Others), Count, X5, .(Current, Code)) → U9_GGGA(Current, Others, Count, X5, Code, reduce_in_ggaa(Others, s(Count), Current, Code))
REDUCE_IN_GGGA(.(Current, Others), Count, X5, .(Current, Code)) → REDUCE_IN_GGAA(Others, s(Count), Current, Code)
REDUCE_IN_GGAA(.(Letter, Others), Count, Letter, Code) → U8_GGAA(Letter, Others, Count, Code, reduce_in_ggaa(Others, Count, Letter, Code))
REDUCE_IN_GGAA(.(Letter, Others), Count, Letter, Code) → REDUCE_IN_GGAA(Others, Count, Letter, Code)
REDUCE_IN_GGAA(.(Current, Others), Count, X5, .(Current, Code)) → U9_GGAA(Current, Others, Count, X5, Code, reduce_in_ggaa(Others, s(Count), Current, Code))
REDUCE_IN_GGAA(.(Current, Others), Count, X5, .(Current, Code)) → REDUCE_IN_GGAA(Others, s(Count), Current, Code)
U2_GA(Name, Code, reduce_out_ggaa(Others, s(0), First, Reduced)) → U3_GA(Name, Code, eq_in_ag(Code, Reduced))
U2_GA(Name, Code, reduce_out_ggaa(Others, s(0), First, Reduced)) → EQ_IN_AG(Code, Reduced)

The TRS R consists of the following rules:

goal_in_ga(Name, Code) → U1_ga(Name, Code, eq_in_ga(Name, .(First, Others)))
eq_in_ga(X, X) → eq_out_ga(X, X)
U1_ga(Name, Code, eq_out_ga(Name, .(First, Others))) → U2_ga(Name, Code, reduce_in_ggaa(Others, s(0), First, Reduced))
reduce_in_ggaa(X1, s(s(s(s(0)))), X2, []) → U4_ggaa(X1, X2, true_in_)
true_in_ → true_out_
U4_ggaa(X1, X2, true_out_) → reduce_out_ggaa(X1, s(s(s(s(0)))), X2, [])
reduce_in_ggaa([], X3, X4, []) → U5_ggaa(X3, X4, true_in_)
U5_ggaa(X3, X4, true_out_) → reduce_out_ggaa([], X3, X4, [])
reduce_in_ggaa(.(Current, Others), Count, Current, Code) → U6_ggaa(Current, Others, Count, Code, vowel_h_w_y_in_a(Current))
vowel_h_w_y_in_a(97) → vowel_h_w_y_out_a(97)
vowel_h_w_y_in_a(101) → vowel_h_w_y_out_a(101)
vowel_h_w_y_in_a(105) → vowel_h_w_y_out_a(105)
vowel_h_w_y_in_a(111) → vowel_h_w_y_out_a(111)
vowel_h_w_y_in_a(117) → vowel_h_w_y_out_a(117)
vowel_h_w_y_in_a(104) → vowel_h_w_y_out_a(104)
vowel_h_w_y_in_a(119) → vowel_h_w_y_out_a(119)
vowel_h_w_y_in_a(121) → vowel_h_w_y_out_a(121)
U6_ggaa(Current, Others, Count, Code, vowel_h_w_y_out_a(Current)) → U7_ggaa(Current, Others, Count, Code, reduce_in_ggga(Others, Count, Current, Code))
reduce_in_ggga(X1, s(s(s(s(0)))), X2, []) → U4_ggga(X1, X2, true_in_)
U4_ggga(X1, X2, true_out_) → reduce_out_ggga(X1, s(s(s(s(0)))), X2, [])
reduce_in_ggga([], X3, X4, []) → U5_ggga(X3, X4, true_in_)
U5_ggga(X3, X4, true_out_) → reduce_out_ggga([], X3, X4, [])
reduce_in_ggga(.(Current, Others), Count, Current, Code) → U6_ggga(Current, Others, Count, Code, vowel_h_w_y_in_g(Current))
vowel_h_w_y_in_g(97) → vowel_h_w_y_out_g(97)
vowel_h_w_y_in_g(101) → vowel_h_w_y_out_g(101)
vowel_h_w_y_in_g(105) → vowel_h_w_y_out_g(105)
vowel_h_w_y_in_g(111) → vowel_h_w_y_out_g(111)
vowel_h_w_y_in_g(117) → vowel_h_w_y_out_g(117)
vowel_h_w_y_in_g(104) → vowel_h_w_y_out_g(104)
vowel_h_w_y_in_g(119) → vowel_h_w_y_out_g(119)
vowel_h_w_y_in_g(121) → vowel_h_w_y_out_g(121)
U6_ggga(Current, Others, Count, Code, vowel_h_w_y_out_g(Current)) → U7_ggga(Current, Others, Count, Code, reduce_in_ggga(Others, Count, Current, Code))
reduce_in_ggga(.(Letter, Others), Count, Letter, Code) → U8_ggga(Letter, Others, Count, Code, reduce_in_ggga(Others, Count, Letter, Code))
reduce_in_ggga(.(Current, Others), Count, X5, .(Current, Code)) → U9_ggga(Current, Others, Count, X5, Code, reduce_in_ggaa(Others, s(Count), Current, Code))
reduce_in_ggaa(.(Letter, Others), Count, Letter, Code) → U8_ggaa(Letter, Others, Count, Code, reduce_in_ggaa(Others, Count, Letter, Code))
reduce_in_ggaa(.(Current, Others), Count, X5, .(Current, Code)) → U9_ggaa(Current, Others, Count, X5, Code, reduce_in_ggaa(Others, s(Count), Current, Code))
U9_ggaa(Current, Others, Count, X5, Code, reduce_out_ggaa(Others, s(Count), Current, Code)) → reduce_out_ggaa(.(Current, Others), Count, X5, .(Current, Code))
U8_ggaa(Letter, Others, Count, Code, reduce_out_ggaa(Others, Count, Letter, Code)) → reduce_out_ggaa(.(Letter, Others), Count, Letter, Code)
U9_ggga(Current, Others, Count, X5, Code, reduce_out_ggaa(Others, s(Count), Current, Code)) → reduce_out_ggga(.(Current, Others), Count, X5, .(Current, Code))
U8_ggga(Letter, Others, Count, Code, reduce_out_ggga(Others, Count, Letter, Code)) → reduce_out_ggga(.(Letter, Others), Count, Letter, Code)
U7_ggga(Current, Others, Count, Code, reduce_out_ggga(Others, Count, Current, Code)) → reduce_out_ggga(.(Current, Others), Count, Current, Code)
U7_ggaa(Current, Others, Count, Code, reduce_out_ggga(Others, Count, Current, Code)) → reduce_out_ggaa(.(Current, Others), Count, Current, Code)
U2_ga(Name, Code, reduce_out_ggaa(Others, s(0), First, Reduced)) → U3_ga(Name, Code, eq_in_ag(Code, Reduced))
eq_in_ag(X, X) → eq_out_ag(X, X)
U3_ga(Name, Code, eq_out_ag(Code, Reduced)) → goal_out_ga(Name, Code)

The argument filtering Pi contains the following mapping:
goal_in_ga(x1, x2)  =  goal_in_ga(x1)
U1_ga(x1, x2, x3)  =  U1_ga(x3)
eq_in_ga(x1, x2)  =  eq_in_ga(x1)
.(x1, x2)  =  .(x2)
eq_out_ga(x1, x2)  =  eq_out_ga(x2)
U2_ga(x1, x2, x3)  =  U2_ga(x3)
reduce_in_ggaa(x1, x2, x3, x4)  =  reduce_in_ggaa(x1, x2)
s(x1)  =  s(x1)
0  =  0
U4_ggaa(x1, x2, x3)  =  U4_ggaa(x3)
true_in_  =  true_in_
true_out_  =  true_out_
reduce_out_ggaa(x1, x2, x3, x4)  =  reduce_out_ggaa(x4)
[]  =  []
U5_ggaa(x1, x2, x3)  =  U5_ggaa(x3)
U6_ggaa(x1, x2, x3, x4, x5)  =  U6_ggaa(x2, x3, x5)
vowel_h_w_y_in_a(x1)  =  vowel_h_w_y_in_a
vowel_h_w_y_out_a(x1)  =  vowel_h_w_y_out_a(x1)
U7_ggaa(x1, x2, x3, x4, x5)  =  U7_ggaa(x5)
reduce_in_ggga(x1, x2, x3, x4)  =  reduce_in_ggga(x1, x2, x3)
U4_ggga(x1, x2, x3)  =  U4_ggga(x3)
reduce_out_ggga(x1, x2, x3, x4)  =  reduce_out_ggga(x4)
U5_ggga(x1, x2, x3)  =  U5_ggga(x3)
U6_ggga(x1, x2, x3, x4, x5)  =  U6_ggga(x1, x2, x3, x5)
vowel_h_w_y_in_g(x1)  =  vowel_h_w_y_in_g(x1)
97  =  97
vowel_h_w_y_out_g(x1)  =  vowel_h_w_y_out_g
101  =  101
105  =  105
111  =  111
117  =  117
104  =  104
119  =  119
121  =  121
U7_ggga(x1, x2, x3, x4, x5)  =  U7_ggga(x5)
U8_ggga(x1, x2, x3, x4, x5)  =  U8_ggga(x5)
U9_ggga(x1, x2, x3, x4, x5, x6)  =  U9_ggga(x6)
U8_ggaa(x1, x2, x3, x4, x5)  =  U8_ggaa(x5)
U9_ggaa(x1, x2, x3, x4, x5, x6)  =  U9_ggaa(x6)
U3_ga(x1, x2, x3)  =  U3_ga(x3)
eq_in_ag(x1, x2)  =  eq_in_ag(x2)
eq_out_ag(x1, x2)  =  eq_out_ag(x1)
goal_out_ga(x1, x2)  =  goal_out_ga(x2)
GOAL_IN_GA(x1, x2)  =  GOAL_IN_GA(x1)
U1_GA(x1, x2, x3)  =  U1_GA(x3)
EQ_IN_GA(x1, x2)  =  EQ_IN_GA(x1)
U2_GA(x1, x2, x3)  =  U2_GA(x3)
REDUCE_IN_GGAA(x1, x2, x3, x4)  =  REDUCE_IN_GGAA(x1, x2)
U4_GGAA(x1, x2, x3)  =  U4_GGAA(x3)
TRUE_IN_  =  TRUE_IN_
U5_GGAA(x1, x2, x3)  =  U5_GGAA(x3)
U6_GGAA(x1, x2, x3, x4, x5)  =  U6_GGAA(x2, x3, x5)
VOWEL_H_W_Y_IN_A(x1)  =  VOWEL_H_W_Y_IN_A
U7_GGAA(x1, x2, x3, x4, x5)  =  U7_GGAA(x5)
REDUCE_IN_GGGA(x1, x2, x3, x4)  =  REDUCE_IN_GGGA(x1, x2, x3)
U4_GGGA(x1, x2, x3)  =  U4_GGGA(x3)
U5_GGGA(x1, x2, x3)  =  U5_GGGA(x3)
U6_GGGA(x1, x2, x3, x4, x5)  =  U6_GGGA(x1, x2, x3, x5)
VOWEL_H_W_Y_IN_G(x1)  =  VOWEL_H_W_Y_IN_G(x1)
U7_GGGA(x1, x2, x3, x4, x5)  =  U7_GGGA(x5)
U8_GGGA(x1, x2, x3, x4, x5)  =  U8_GGGA(x5)
U9_GGGA(x1, x2, x3, x4, x5, x6)  =  U9_GGGA(x6)
U8_GGAA(x1, x2, x3, x4, x5)  =  U8_GGAA(x5)
U9_GGAA(x1, x2, x3, x4, x5, x6)  =  U9_GGAA(x6)
U3_GA(x1, x2, x3)  =  U3_GA(x3)
EQ_IN_AG(x1, x2)  =  EQ_IN_AG(x2)

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

(9) DependencyGraphProof (EQUIVALENT transformation)

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

(10) Obligation:

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

REDUCE_IN_GGAA(.(Current, Others), Count, Current, Code) → U6_GGAA(Current, Others, Count, Code, vowel_h_w_y_in_a(Current))
U6_GGAA(Current, Others, Count, Code, vowel_h_w_y_out_a(Current)) → REDUCE_IN_GGGA(Others, Count, Current, Code)
REDUCE_IN_GGGA(.(Current, Others), Count, Current, Code) → U6_GGGA(Current, Others, Count, Code, vowel_h_w_y_in_g(Current))
U6_GGGA(Current, Others, Count, Code, vowel_h_w_y_out_g(Current)) → REDUCE_IN_GGGA(Others, Count, Current, Code)
REDUCE_IN_GGGA(.(Letter, Others), Count, Letter, Code) → REDUCE_IN_GGGA(Others, Count, Letter, Code)
REDUCE_IN_GGGA(.(Current, Others), Count, X5, .(Current, Code)) → REDUCE_IN_GGAA(Others, s(Count), Current, Code)
REDUCE_IN_GGAA(.(Letter, Others), Count, Letter, Code) → REDUCE_IN_GGAA(Others, Count, Letter, Code)
REDUCE_IN_GGAA(.(Current, Others), Count, X5, .(Current, Code)) → REDUCE_IN_GGAA(Others, s(Count), Current, Code)

The TRS R consists of the following rules:

goal_in_ga(Name, Code) → U1_ga(Name, Code, eq_in_ga(Name, .(First, Others)))
eq_in_ga(X, X) → eq_out_ga(X, X)
U1_ga(Name, Code, eq_out_ga(Name, .(First, Others))) → U2_ga(Name, Code, reduce_in_ggaa(Others, s(0), First, Reduced))
reduce_in_ggaa(X1, s(s(s(s(0)))), X2, []) → U4_ggaa(X1, X2, true_in_)
true_in_ → true_out_
U4_ggaa(X1, X2, true_out_) → reduce_out_ggaa(X1, s(s(s(s(0)))), X2, [])
reduce_in_ggaa([], X3, X4, []) → U5_ggaa(X3, X4, true_in_)
U5_ggaa(X3, X4, true_out_) → reduce_out_ggaa([], X3, X4, [])
reduce_in_ggaa(.(Current, Others), Count, Current, Code) → U6_ggaa(Current, Others, Count, Code, vowel_h_w_y_in_a(Current))
vowel_h_w_y_in_a(97) → vowel_h_w_y_out_a(97)
vowel_h_w_y_in_a(101) → vowel_h_w_y_out_a(101)
vowel_h_w_y_in_a(105) → vowel_h_w_y_out_a(105)
vowel_h_w_y_in_a(111) → vowel_h_w_y_out_a(111)
vowel_h_w_y_in_a(117) → vowel_h_w_y_out_a(117)
vowel_h_w_y_in_a(104) → vowel_h_w_y_out_a(104)
vowel_h_w_y_in_a(119) → vowel_h_w_y_out_a(119)
vowel_h_w_y_in_a(121) → vowel_h_w_y_out_a(121)
U6_ggaa(Current, Others, Count, Code, vowel_h_w_y_out_a(Current)) → U7_ggaa(Current, Others, Count, Code, reduce_in_ggga(Others, Count, Current, Code))
reduce_in_ggga(X1, s(s(s(s(0)))), X2, []) → U4_ggga(X1, X2, true_in_)
U4_ggga(X1, X2, true_out_) → reduce_out_ggga(X1, s(s(s(s(0)))), X2, [])
reduce_in_ggga([], X3, X4, []) → U5_ggga(X3, X4, true_in_)
U5_ggga(X3, X4, true_out_) → reduce_out_ggga([], X3, X4, [])
reduce_in_ggga(.(Current, Others), Count, Current, Code) → U6_ggga(Current, Others, Count, Code, vowel_h_w_y_in_g(Current))
vowel_h_w_y_in_g(97) → vowel_h_w_y_out_g(97)
vowel_h_w_y_in_g(101) → vowel_h_w_y_out_g(101)
vowel_h_w_y_in_g(105) → vowel_h_w_y_out_g(105)
vowel_h_w_y_in_g(111) → vowel_h_w_y_out_g(111)
vowel_h_w_y_in_g(117) → vowel_h_w_y_out_g(117)
vowel_h_w_y_in_g(104) → vowel_h_w_y_out_g(104)
vowel_h_w_y_in_g(119) → vowel_h_w_y_out_g(119)
vowel_h_w_y_in_g(121) → vowel_h_w_y_out_g(121)
U6_ggga(Current, Others, Count, Code, vowel_h_w_y_out_g(Current)) → U7_ggga(Current, Others, Count, Code, reduce_in_ggga(Others, Count, Current, Code))
reduce_in_ggga(.(Letter, Others), Count, Letter, Code) → U8_ggga(Letter, Others, Count, Code, reduce_in_ggga(Others, Count, Letter, Code))
reduce_in_ggga(.(Current, Others), Count, X5, .(Current, Code)) → U9_ggga(Current, Others, Count, X5, Code, reduce_in_ggaa(Others, s(Count), Current, Code))
reduce_in_ggaa(.(Letter, Others), Count, Letter, Code) → U8_ggaa(Letter, Others, Count, Code, reduce_in_ggaa(Others, Count, Letter, Code))
reduce_in_ggaa(.(Current, Others), Count, X5, .(Current, Code)) → U9_ggaa(Current, Others, Count, X5, Code, reduce_in_ggaa(Others, s(Count), Current, Code))
U9_ggaa(Current, Others, Count, X5, Code, reduce_out_ggaa(Others, s(Count), Current, Code)) → reduce_out_ggaa(.(Current, Others), Count, X5, .(Current, Code))
U8_ggaa(Letter, Others, Count, Code, reduce_out_ggaa(Others, Count, Letter, Code)) → reduce_out_ggaa(.(Letter, Others), Count, Letter, Code)
U9_ggga(Current, Others, Count, X5, Code, reduce_out_ggaa(Others, s(Count), Current, Code)) → reduce_out_ggga(.(Current, Others), Count, X5, .(Current, Code))
U8_ggga(Letter, Others, Count, Code, reduce_out_ggga(Others, Count, Letter, Code)) → reduce_out_ggga(.(Letter, Others), Count, Letter, Code)
U7_ggga(Current, Others, Count, Code, reduce_out_ggga(Others, Count, Current, Code)) → reduce_out_ggga(.(Current, Others), Count, Current, Code)
U7_ggaa(Current, Others, Count, Code, reduce_out_ggga(Others, Count, Current, Code)) → reduce_out_ggaa(.(Current, Others), Count, Current, Code)
U2_ga(Name, Code, reduce_out_ggaa(Others, s(0), First, Reduced)) → U3_ga(Name, Code, eq_in_ag(Code, Reduced))
eq_in_ag(X, X) → eq_out_ag(X, X)
U3_ga(Name, Code, eq_out_ag(Code, Reduced)) → goal_out_ga(Name, Code)

The argument filtering Pi contains the following mapping:
goal_in_ga(x1, x2)  =  goal_in_ga(x1)
U1_ga(x1, x2, x3)  =  U1_ga(x3)
eq_in_ga(x1, x2)  =  eq_in_ga(x1)
.(x1, x2)  =  .(x2)
eq_out_ga(x1, x2)  =  eq_out_ga(x2)
U2_ga(x1, x2, x3)  =  U2_ga(x3)
reduce_in_ggaa(x1, x2, x3, x4)  =  reduce_in_ggaa(x1, x2)
s(x1)  =  s(x1)
0  =  0
U4_ggaa(x1, x2, x3)  =  U4_ggaa(x3)
true_in_  =  true_in_
true_out_  =  true_out_
reduce_out_ggaa(x1, x2, x3, x4)  =  reduce_out_ggaa(x4)
[]  =  []
U5_ggaa(x1, x2, x3)  =  U5_ggaa(x3)
U6_ggaa(x1, x2, x3, x4, x5)  =  U6_ggaa(x2, x3, x5)
vowel_h_w_y_in_a(x1)  =  vowel_h_w_y_in_a
vowel_h_w_y_out_a(x1)  =  vowel_h_w_y_out_a(x1)
U7_ggaa(x1, x2, x3, x4, x5)  =  U7_ggaa(x5)
reduce_in_ggga(x1, x2, x3, x4)  =  reduce_in_ggga(x1, x2, x3)
U4_ggga(x1, x2, x3)  =  U4_ggga(x3)
reduce_out_ggga(x1, x2, x3, x4)  =  reduce_out_ggga(x4)
U5_ggga(x1, x2, x3)  =  U5_ggga(x3)
U6_ggga(x1, x2, x3, x4, x5)  =  U6_ggga(x1, x2, x3, x5)
vowel_h_w_y_in_g(x1)  =  vowel_h_w_y_in_g(x1)
97  =  97
vowel_h_w_y_out_g(x1)  =  vowel_h_w_y_out_g
101  =  101
105  =  105
111  =  111
117  =  117
104  =  104
119  =  119
121  =  121
U7_ggga(x1, x2, x3, x4, x5)  =  U7_ggga(x5)
U8_ggga(x1, x2, x3, x4, x5)  =  U8_ggga(x5)
U9_ggga(x1, x2, x3, x4, x5, x6)  =  U9_ggga(x6)
U8_ggaa(x1, x2, x3, x4, x5)  =  U8_ggaa(x5)
U9_ggaa(x1, x2, x3, x4, x5, x6)  =  U9_ggaa(x6)
U3_ga(x1, x2, x3)  =  U3_ga(x3)
eq_in_ag(x1, x2)  =  eq_in_ag(x2)
eq_out_ag(x1, x2)  =  eq_out_ag(x1)
goal_out_ga(x1, x2)  =  goal_out_ga(x2)
REDUCE_IN_GGAA(x1, x2, x3, x4)  =  REDUCE_IN_GGAA(x1, x2)
U6_GGAA(x1, x2, x3, x4, x5)  =  U6_GGAA(x2, x3, x5)
REDUCE_IN_GGGA(x1, x2, x3, x4)  =  REDUCE_IN_GGGA(x1, x2, x3)
U6_GGGA(x1, x2, x3, x4, x5)  =  U6_GGGA(x1, x2, x3, x5)

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

(11) PrologToPiTRSProof (SOUND transformation)

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

goal_in_ga(Name, Code) → U1_ga(Name, Code, eq_in_ga(Name, .(First, Others)))
eq_in_ga(X, X) → eq_out_ga(X, X)
U1_ga(Name, Code, eq_out_ga(Name, .(First, Others))) → U2_ga(Name, Code, reduce_in_ggaa(Others, s(0), First, Reduced))
reduce_in_ggaa(X1, s(s(s(s(0)))), X2, []) → U4_ggaa(X1, X2, true_in_)
true_in_ → true_out_
U4_ggaa(X1, X2, true_out_) → reduce_out_ggaa(X1, s(s(s(s(0)))), X2, [])
reduce_in_ggaa([], X3, X4, []) → U5_ggaa(X3, X4, true_in_)
U5_ggaa(X3, X4, true_out_) → reduce_out_ggaa([], X3, X4, [])
reduce_in_ggaa(.(Current, Others), Count, Current, Code) → U6_ggaa(Current, Others, Count, Code, vowel_h_w_y_in_a(Current))
vowel_h_w_y_in_a(97) → vowel_h_w_y_out_a(97)
vowel_h_w_y_in_a(101) → vowel_h_w_y_out_a(101)
vowel_h_w_y_in_a(105) → vowel_h_w_y_out_a(105)
vowel_h_w_y_in_a(111) → vowel_h_w_y_out_a(111)
vowel_h_w_y_in_a(117) → vowel_h_w_y_out_a(117)
vowel_h_w_y_in_a(104) → vowel_h_w_y_out_a(104)
vowel_h_w_y_in_a(119) → vowel_h_w_y_out_a(119)
vowel_h_w_y_in_a(121) → vowel_h_w_y_out_a(121)
U6_ggaa(Current, Others, Count, Code, vowel_h_w_y_out_a(Current)) → U7_ggaa(Current, Others, Count, Code, reduce_in_ggga(Others, Count, Current, Code))
reduce_in_ggga(X1, s(s(s(s(0)))), X2, []) → U4_ggga(X1, X2, true_in_)
U4_ggga(X1, X2, true_out_) → reduce_out_ggga(X1, s(s(s(s(0)))), X2, [])
reduce_in_ggga([], X3, X4, []) → U5_ggga(X3, X4, true_in_)
U5_ggga(X3, X4, true_out_) → reduce_out_ggga([], X3, X4, [])
reduce_in_ggga(.(Current, Others), Count, Current, Code) → U6_ggga(Current, Others, Count, Code, vowel_h_w_y_in_g(Current))
vowel_h_w_y_in_g(97) → vowel_h_w_y_out_g(97)
vowel_h_w_y_in_g(101) → vowel_h_w_y_out_g(101)
vowel_h_w_y_in_g(105) → vowel_h_w_y_out_g(105)
vowel_h_w_y_in_g(111) → vowel_h_w_y_out_g(111)
vowel_h_w_y_in_g(117) → vowel_h_w_y_out_g(117)
vowel_h_w_y_in_g(104) → vowel_h_w_y_out_g(104)
vowel_h_w_y_in_g(119) → vowel_h_w_y_out_g(119)
vowel_h_w_y_in_g(121) → vowel_h_w_y_out_g(121)
U6_ggga(Current, Others, Count, Code, vowel_h_w_y_out_g(Current)) → U7_ggga(Current, Others, Count, Code, reduce_in_ggga(Others, Count, Current, Code))
reduce_in_ggga(.(Letter, Others), Count, Letter, Code) → U8_ggga(Letter, Others, Count, Code, reduce_in_ggga(Others, Count, Letter, Code))
reduce_in_ggga(.(Current, Others), Count, X5, .(Current, Code)) → U9_ggga(Current, Others, Count, X5, Code, reduce_in_ggaa(Others, s(Count), Current, Code))
reduce_in_ggaa(.(Letter, Others), Count, Letter, Code) → U8_ggaa(Letter, Others, Count, Code, reduce_in_ggaa(Others, Count, Letter, Code))
reduce_in_ggaa(.(Current, Others), Count, X5, .(Current, Code)) → U9_ggaa(Current, Others, Count, X5, Code, reduce_in_ggaa(Others, s(Count), Current, Code))
U9_ggaa(Current, Others, Count, X5, Code, reduce_out_ggaa(Others, s(Count), Current, Code)) → reduce_out_ggaa(.(Current, Others), Count, X5, .(Current, Code))
U8_ggaa(Letter, Others, Count, Code, reduce_out_ggaa(Others, Count, Letter, Code)) → reduce_out_ggaa(.(Letter, Others), Count, Letter, Code)
U9_ggga(Current, Others, Count, X5, Code, reduce_out_ggaa(Others, s(Count), Current, Code)) → reduce_out_ggga(.(Current, Others), Count, X5, .(Current, Code))
U8_ggga(Letter, Others, Count, Code, reduce_out_ggga(Others, Count, Letter, Code)) → reduce_out_ggga(.(Letter, Others), Count, Letter, Code)
U7_ggga(Current, Others, Count, Code, reduce_out_ggga(Others, Count, Current, Code)) → reduce_out_ggga(.(Current, Others), Count, Current, Code)
U7_ggaa(Current, Others, Count, Code, reduce_out_ggga(Others, Count, Current, Code)) → reduce_out_ggaa(.(Current, Others), Count, Current, Code)
U2_ga(Name, Code, reduce_out_ggaa(Others, s(0), First, Reduced)) → U3_ga(Name, Code, eq_in_ag(Code, Reduced))
eq_in_ag(X, X) → eq_out_ag(X, X)
U3_ga(Name, Code, eq_out_ag(Code, Reduced)) → goal_out_ga(Name, Code)

The argument filtering Pi contains the following mapping:
goal_in_ga(x1, x2)  =  goal_in_ga(x1)
U1_ga(x1, x2, x3)  =  U1_ga(x1, x3)
eq_in_ga(x1, x2)  =  eq_in_ga(x1)
.(x1, x2)  =  .(x2)
eq_out_ga(x1, x2)  =  eq_out_ga(x1, x2)
U2_ga(x1, x2, x3)  =  U2_ga(x1, x3)
reduce_in_ggaa(x1, x2, x3, x4)  =  reduce_in_ggaa(x1, x2)
s(x1)  =  s(x1)
0  =  0
U4_ggaa(x1, x2, x3)  =  U4_ggaa(x1, x3)
true_in_  =  true_in_
true_out_  =  true_out_
reduce_out_ggaa(x1, x2, x3, x4)  =  reduce_out_ggaa(x1, x2, x4)
[]  =  []
U5_ggaa(x1, x2, x3)  =  U5_ggaa(x1, x3)
U6_ggaa(x1, x2, x3, x4, x5)  =  U6_ggaa(x2, x3, x5)
vowel_h_w_y_in_a(x1)  =  vowel_h_w_y_in_a
vowel_h_w_y_out_a(x1)  =  vowel_h_w_y_out_a(x1)
U7_ggaa(x1, x2, x3, x4, x5)  =  U7_ggaa(x2, x3, x5)
reduce_in_ggga(x1, x2, x3, x4)  =  reduce_in_ggga(x1, x2, x3)
U4_ggga(x1, x2, x3)  =  U4_ggga(x1, x2, x3)
reduce_out_ggga(x1, x2, x3, x4)  =  reduce_out_ggga(x1, x2, x3, x4)
U5_ggga(x1, x2, x3)  =  U5_ggga(x1, x2, x3)
U6_ggga(x1, x2, x3, x4, x5)  =  U6_ggga(x1, x2, x3, x5)
vowel_h_w_y_in_g(x1)  =  vowel_h_w_y_in_g(x1)
97  =  97
vowel_h_w_y_out_g(x1)  =  vowel_h_w_y_out_g(x1)
101  =  101
105  =  105
111  =  111
117  =  117
104  =  104
119  =  119
121  =  121
U7_ggga(x1, x2, x3, x4, x5)  =  U7_ggga(x1, x2, x3, x5)
U8_ggga(x1, x2, x3, x4, x5)  =  U8_ggga(x1, x2, x3, x5)
U9_ggga(x1, x2, x3, x4, x5, x6)  =  U9_ggga(x2, x3, x4, x6)
U8_ggaa(x1, x2, x3, x4, x5)  =  U8_ggaa(x2, x3, x5)
U9_ggaa(x1, x2, x3, x4, x5, x6)  =  U9_ggaa(x2, x3, x6)
U3_ga(x1, x2, x3)  =  U3_ga(x1, x3)
eq_in_ag(x1, x2)  =  eq_in_ag(x2)
eq_out_ag(x1, x2)  =  eq_out_ag(x1, x2)
goal_out_ga(x1, x2)  =  goal_out_ga(x1, x2)

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog

(12) Obligation:

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

goal_in_ga(Name, Code) → U1_ga(Name, Code, eq_in_ga(Name, .(First, Others)))
eq_in_ga(X, X) → eq_out_ga(X, X)
U1_ga(Name, Code, eq_out_ga(Name, .(First, Others))) → U2_ga(Name, Code, reduce_in_ggaa(Others, s(0), First, Reduced))
reduce_in_ggaa(X1, s(s(s(s(0)))), X2, []) → U4_ggaa(X1, X2, true_in_)
true_in_ → true_out_
U4_ggaa(X1, X2, true_out_) → reduce_out_ggaa(X1, s(s(s(s(0)))), X2, [])
reduce_in_ggaa([], X3, X4, []) → U5_ggaa(X3, X4, true_in_)
U5_ggaa(X3, X4, true_out_) → reduce_out_ggaa([], X3, X4, [])
reduce_in_ggaa(.(Current, Others), Count, Current, Code) → U6_ggaa(Current, Others, Count, Code, vowel_h_w_y_in_a(Current))
vowel_h_w_y_in_a(97) → vowel_h_w_y_out_a(97)
vowel_h_w_y_in_a(101) → vowel_h_w_y_out_a(101)
vowel_h_w_y_in_a(105) → vowel_h_w_y_out_a(105)
vowel_h_w_y_in_a(111) → vowel_h_w_y_out_a(111)
vowel_h_w_y_in_a(117) → vowel_h_w_y_out_a(117)
vowel_h_w_y_in_a(104) → vowel_h_w_y_out_a(104)
vowel_h_w_y_in_a(119) → vowel_h_w_y_out_a(119)
vowel_h_w_y_in_a(121) → vowel_h_w_y_out_a(121)
U6_ggaa(Current, Others, Count, Code, vowel_h_w_y_out_a(Current)) → U7_ggaa(Current, Others, Count, Code, reduce_in_ggga(Others, Count, Current, Code))
reduce_in_ggga(X1, s(s(s(s(0)))), X2, []) → U4_ggga(X1, X2, true_in_)
U4_ggga(X1, X2, true_out_) → reduce_out_ggga(X1, s(s(s(s(0)))), X2, [])
reduce_in_ggga([], X3, X4, []) → U5_ggga(X3, X4, true_in_)
U5_ggga(X3, X4, true_out_) → reduce_out_ggga([], X3, X4, [])
reduce_in_ggga(.(Current, Others), Count, Current, Code) → U6_ggga(Current, Others, Count, Code, vowel_h_w_y_in_g(Current))
vowel_h_w_y_in_g(97) → vowel_h_w_y_out_g(97)
vowel_h_w_y_in_g(101) → vowel_h_w_y_out_g(101)
vowel_h_w_y_in_g(105) → vowel_h_w_y_out_g(105)
vowel_h_w_y_in_g(111) → vowel_h_w_y_out_g(111)
vowel_h_w_y_in_g(117) → vowel_h_w_y_out_g(117)
vowel_h_w_y_in_g(104) → vowel_h_w_y_out_g(104)
vowel_h_w_y_in_g(119) → vowel_h_w_y_out_g(119)
vowel_h_w_y_in_g(121) → vowel_h_w_y_out_g(121)
U6_ggga(Current, Others, Count, Code, vowel_h_w_y_out_g(Current)) → U7_ggga(Current, Others, Count, Code, reduce_in_ggga(Others, Count, Current, Code))
reduce_in_ggga(.(Letter, Others), Count, Letter, Code) → U8_ggga(Letter, Others, Count, Code, reduce_in_ggga(Others, Count, Letter, Code))
reduce_in_ggga(.(Current, Others), Count, X5, .(Current, Code)) → U9_ggga(Current, Others, Count, X5, Code, reduce_in_ggaa(Others, s(Count), Current, Code))
reduce_in_ggaa(.(Letter, Others), Count, Letter, Code) → U8_ggaa(Letter, Others, Count, Code, reduce_in_ggaa(Others, Count, Letter, Code))
reduce_in_ggaa(.(Current, Others), Count, X5, .(Current, Code)) → U9_ggaa(Current, Others, Count, X5, Code, reduce_in_ggaa(Others, s(Count), Current, Code))
U9_ggaa(Current, Others, Count, X5, Code, reduce_out_ggaa(Others, s(Count), Current, Code)) → reduce_out_ggaa(.(Current, Others), Count, X5, .(Current, Code))
U8_ggaa(Letter, Others, Count, Code, reduce_out_ggaa(Others, Count, Letter, Code)) → reduce_out_ggaa(.(Letter, Others), Count, Letter, Code)
U9_ggga(Current, Others, Count, X5, Code, reduce_out_ggaa(Others, s(Count), Current, Code)) → reduce_out_ggga(.(Current, Others), Count, X5, .(Current, Code))
U8_ggga(Letter, Others, Count, Code, reduce_out_ggga(Others, Count, Letter, Code)) → reduce_out_ggga(.(Letter, Others), Count, Letter, Code)
U7_ggga(Current, Others, Count, Code, reduce_out_ggga(Others, Count, Current, Code)) → reduce_out_ggga(.(Current, Others), Count, Current, Code)
U7_ggaa(Current, Others, Count, Code, reduce_out_ggga(Others, Count, Current, Code)) → reduce_out_ggaa(.(Current, Others), Count, Current, Code)
U2_ga(Name, Code, reduce_out_ggaa(Others, s(0), First, Reduced)) → U3_ga(Name, Code, eq_in_ag(Code, Reduced))
eq_in_ag(X, X) → eq_out_ag(X, X)
U3_ga(Name, Code, eq_out_ag(Code, Reduced)) → goal_out_ga(Name, Code)

The argument filtering Pi contains the following mapping:
goal_in_ga(x1, x2)  =  goal_in_ga(x1)
U1_ga(x1, x2, x3)  =  U1_ga(x1, x3)
eq_in_ga(x1, x2)  =  eq_in_ga(x1)
.(x1, x2)  =  .(x2)
eq_out_ga(x1, x2)  =  eq_out_ga(x1, x2)
U2_ga(x1, x2, x3)  =  U2_ga(x1, x3)
reduce_in_ggaa(x1, x2, x3, x4)  =  reduce_in_ggaa(x1, x2)
s(x1)  =  s(x1)
0  =  0
U4_ggaa(x1, x2, x3)  =  U4_ggaa(x1, x3)
true_in_  =  true_in_
true_out_  =  true_out_
reduce_out_ggaa(x1, x2, x3, x4)  =  reduce_out_ggaa(x1, x2, x4)
[]  =  []
U5_ggaa(x1, x2, x3)  =  U5_ggaa(x1, x3)
U6_ggaa(x1, x2, x3, x4, x5)  =  U6_ggaa(x2, x3, x5)
vowel_h_w_y_in_a(x1)  =  vowel_h_w_y_in_a
vowel_h_w_y_out_a(x1)  =  vowel_h_w_y_out_a(x1)
U7_ggaa(x1, x2, x3, x4, x5)  =  U7_ggaa(x2, x3, x5)
reduce_in_ggga(x1, x2, x3, x4)  =  reduce_in_ggga(x1, x2, x3)
U4_ggga(x1, x2, x3)  =  U4_ggga(x1, x2, x3)
reduce_out_ggga(x1, x2, x3, x4)  =  reduce_out_ggga(x1, x2, x3, x4)
U5_ggga(x1, x2, x3)  =  U5_ggga(x1, x2, x3)
U6_ggga(x1, x2, x3, x4, x5)  =  U6_ggga(x1, x2, x3, x5)
vowel_h_w_y_in_g(x1)  =  vowel_h_w_y_in_g(x1)
97  =  97
vowel_h_w_y_out_g(x1)  =  vowel_h_w_y_out_g(x1)
101  =  101
105  =  105
111  =  111
117  =  117
104  =  104
119  =  119
121  =  121
U7_ggga(x1, x2, x3, x4, x5)  =  U7_ggga(x1, x2, x3, x5)
U8_ggga(x1, x2, x3, x4, x5)  =  U8_ggga(x1, x2, x3, x5)
U9_ggga(x1, x2, x3, x4, x5, x6)  =  U9_ggga(x2, x3, x4, x6)
U8_ggaa(x1, x2, x3, x4, x5)  =  U8_ggaa(x2, x3, x5)
U9_ggaa(x1, x2, x3, x4, x5, x6)  =  U9_ggaa(x2, x3, x6)
U3_ga(x1, x2, x3)  =  U3_ga(x1, x3)
eq_in_ag(x1, x2)  =  eq_in_ag(x2)
eq_out_ag(x1, x2)  =  eq_out_ag(x1, x2)
goal_out_ga(x1, x2)  =  goal_out_ga(x1, x2)

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

GOAL_IN_GA(Name, Code) → U1_GA(Name, Code, eq_in_ga(Name, .(First, Others)))
GOAL_IN_GA(Name, Code) → EQ_IN_GA(Name, .(First, Others))
U1_GA(Name, Code, eq_out_ga(Name, .(First, Others))) → U2_GA(Name, Code, reduce_in_ggaa(Others, s(0), First, Reduced))
U1_GA(Name, Code, eq_out_ga(Name, .(First, Others))) → REDUCE_IN_GGAA(Others, s(0), First, Reduced)
REDUCE_IN_GGAA(X1, s(s(s(s(0)))), X2, []) → U4_GGAA(X1, X2, true_in_)
REDUCE_IN_GGAA(X1, s(s(s(s(0)))), X2, []) → TRUE_IN_
REDUCE_IN_GGAA([], X3, X4, []) → U5_GGAA(X3, X4, true_in_)
REDUCE_IN_GGAA([], X3, X4, []) → TRUE_IN_
REDUCE_IN_GGAA(.(Current, Others), Count, Current, Code) → U6_GGAA(Current, Others, Count, Code, vowel_h_w_y_in_a(Current))
REDUCE_IN_GGAA(.(Current, Others), Count, Current, Code) → VOWEL_H_W_Y_IN_A(Current)
U6_GGAA(Current, Others, Count, Code, vowel_h_w_y_out_a(Current)) → U7_GGAA(Current, Others, Count, Code, reduce_in_ggga(Others, Count, Current, Code))
U6_GGAA(Current, Others, Count, Code, vowel_h_w_y_out_a(Current)) → REDUCE_IN_GGGA(Others, Count, Current, Code)
REDUCE_IN_GGGA(X1, s(s(s(s(0)))), X2, []) → U4_GGGA(X1, X2, true_in_)
REDUCE_IN_GGGA(X1, s(s(s(s(0)))), X2, []) → TRUE_IN_
REDUCE_IN_GGGA([], X3, X4, []) → U5_GGGA(X3, X4, true_in_)
REDUCE_IN_GGGA([], X3, X4, []) → TRUE_IN_
REDUCE_IN_GGGA(.(Current, Others), Count, Current, Code) → U6_GGGA(Current, Others, Count, Code, vowel_h_w_y_in_g(Current))
REDUCE_IN_GGGA(.(Current, Others), Count, Current, Code) → VOWEL_H_W_Y_IN_G(Current)
U6_GGGA(Current, Others, Count, Code, vowel_h_w_y_out_g(Current)) → U7_GGGA(Current, Others, Count, Code, reduce_in_ggga(Others, Count, Current, Code))
U6_GGGA(Current, Others, Count, Code, vowel_h_w_y_out_g(Current)) → REDUCE_IN_GGGA(Others, Count, Current, Code)
REDUCE_IN_GGGA(.(Letter, Others), Count, Letter, Code) → U8_GGGA(Letter, Others, Count, Code, reduce_in_ggga(Others, Count, Letter, Code))
REDUCE_IN_GGGA(.(Letter, Others), Count, Letter, Code) → REDUCE_IN_GGGA(Others, Count, Letter, Code)
REDUCE_IN_GGGA(.(Current, Others), Count, X5, .(Current, Code)) → U9_GGGA(Current, Others, Count, X5, Code, reduce_in_ggaa(Others, s(Count), Current, Code))
REDUCE_IN_GGGA(.(Current, Others), Count, X5, .(Current, Code)) → REDUCE_IN_GGAA(Others, s(Count), Current, Code)
REDUCE_IN_GGAA(.(Letter, Others), Count, Letter, Code) → U8_GGAA(Letter, Others, Count, Code, reduce_in_ggaa(Others, Count, Letter, Code))
REDUCE_IN_GGAA(.(Letter, Others), Count, Letter, Code) → REDUCE_IN_GGAA(Others, Count, Letter, Code)
REDUCE_IN_GGAA(.(Current, Others), Count, X5, .(Current, Code)) → U9_GGAA(Current, Others, Count, X5, Code, reduce_in_ggaa(Others, s(Count), Current, Code))
REDUCE_IN_GGAA(.(Current, Others), Count, X5, .(Current, Code)) → REDUCE_IN_GGAA(Others, s(Count), Current, Code)
U2_GA(Name, Code, reduce_out_ggaa(Others, s(0), First, Reduced)) → U3_GA(Name, Code, eq_in_ag(Code, Reduced))
U2_GA(Name, Code, reduce_out_ggaa(Others, s(0), First, Reduced)) → EQ_IN_AG(Code, Reduced)

The TRS R consists of the following rules:

goal_in_ga(Name, Code) → U1_ga(Name, Code, eq_in_ga(Name, .(First, Others)))
eq_in_ga(X, X) → eq_out_ga(X, X)
U1_ga(Name, Code, eq_out_ga(Name, .(First, Others))) → U2_ga(Name, Code, reduce_in_ggaa(Others, s(0), First, Reduced))
reduce_in_ggaa(X1, s(s(s(s(0)))), X2, []) → U4_ggaa(X1, X2, true_in_)
true_in_ → true_out_
U4_ggaa(X1, X2, true_out_) → reduce_out_ggaa(X1, s(s(s(s(0)))), X2, [])
reduce_in_ggaa([], X3, X4, []) → U5_ggaa(X3, X4, true_in_)
U5_ggaa(X3, X4, true_out_) → reduce_out_ggaa([], X3, X4, [])
reduce_in_ggaa(.(Current, Others), Count, Current, Code) → U6_ggaa(Current, Others, Count, Code, vowel_h_w_y_in_a(Current))
vowel_h_w_y_in_a(97) → vowel_h_w_y_out_a(97)
vowel_h_w_y_in_a(101) → vowel_h_w_y_out_a(101)
vowel_h_w_y_in_a(105) → vowel_h_w_y_out_a(105)
vowel_h_w_y_in_a(111) → vowel_h_w_y_out_a(111)
vowel_h_w_y_in_a(117) → vowel_h_w_y_out_a(117)
vowel_h_w_y_in_a(104) → vowel_h_w_y_out_a(104)
vowel_h_w_y_in_a(119) → vowel_h_w_y_out_a(119)
vowel_h_w_y_in_a(121) → vowel_h_w_y_out_a(121)
U6_ggaa(Current, Others, Count, Code, vowel_h_w_y_out_a(Current)) → U7_ggaa(Current, Others, Count, Code, reduce_in_ggga(Others, Count, Current, Code))
reduce_in_ggga(X1, s(s(s(s(0)))), X2, []) → U4_ggga(X1, X2, true_in_)
U4_ggga(X1, X2, true_out_) → reduce_out_ggga(X1, s(s(s(s(0)))), X2, [])
reduce_in_ggga([], X3, X4, []) → U5_ggga(X3, X4, true_in_)
U5_ggga(X3, X4, true_out_) → reduce_out_ggga([], X3, X4, [])
reduce_in_ggga(.(Current, Others), Count, Current, Code) → U6_ggga(Current, Others, Count, Code, vowel_h_w_y_in_g(Current))
vowel_h_w_y_in_g(97) → vowel_h_w_y_out_g(97)
vowel_h_w_y_in_g(101) → vowel_h_w_y_out_g(101)
vowel_h_w_y_in_g(105) → vowel_h_w_y_out_g(105)
vowel_h_w_y_in_g(111) → vowel_h_w_y_out_g(111)
vowel_h_w_y_in_g(117) → vowel_h_w_y_out_g(117)
vowel_h_w_y_in_g(104) → vowel_h_w_y_out_g(104)
vowel_h_w_y_in_g(119) → vowel_h_w_y_out_g(119)
vowel_h_w_y_in_g(121) → vowel_h_w_y_out_g(121)
U6_ggga(Current, Others, Count, Code, vowel_h_w_y_out_g(Current)) → U7_ggga(Current, Others, Count, Code, reduce_in_ggga(Others, Count, Current, Code))
reduce_in_ggga(.(Letter, Others), Count, Letter, Code) → U8_ggga(Letter, Others, Count, Code, reduce_in_ggga(Others, Count, Letter, Code))
reduce_in_ggga(.(Current, Others), Count, X5, .(Current, Code)) → U9_ggga(Current, Others, Count, X5, Code, reduce_in_ggaa(Others, s(Count), Current, Code))
reduce_in_ggaa(.(Letter, Others), Count, Letter, Code) → U8_ggaa(Letter, Others, Count, Code, reduce_in_ggaa(Others, Count, Letter, Code))
reduce_in_ggaa(.(Current, Others), Count, X5, .(Current, Code)) → U9_ggaa(Current, Others, Count, X5, Code, reduce_in_ggaa(Others, s(Count), Current, Code))
U9_ggaa(Current, Others, Count, X5, Code, reduce_out_ggaa(Others, s(Count), Current, Code)) → reduce_out_ggaa(.(Current, Others), Count, X5, .(Current, Code))
U8_ggaa(Letter, Others, Count, Code, reduce_out_ggaa(Others, Count, Letter, Code)) → reduce_out_ggaa(.(Letter, Others), Count, Letter, Code)
U9_ggga(Current, Others, Count, X5, Code, reduce_out_ggaa(Others, s(Count), Current, Code)) → reduce_out_ggga(.(Current, Others), Count, X5, .(Current, Code))
U8_ggga(Letter, Others, Count, Code, reduce_out_ggga(Others, Count, Letter, Code)) → reduce_out_ggga(.(Letter, Others), Count, Letter, Code)
U7_ggga(Current, Others, Count, Code, reduce_out_ggga(Others, Count, Current, Code)) → reduce_out_ggga(.(Current, Others), Count, Current, Code)
U7_ggaa(Current, Others, Count, Code, reduce_out_ggga(Others, Count, Current, Code)) → reduce_out_ggaa(.(Current, Others), Count, Current, Code)
U2_ga(Name, Code, reduce_out_ggaa(Others, s(0), First, Reduced)) → U3_ga(Name, Code, eq_in_ag(Code, Reduced))
eq_in_ag(X, X) → eq_out_ag(X, X)
U3_ga(Name, Code, eq_out_ag(Code, Reduced)) → goal_out_ga(Name, Code)

The argument filtering Pi contains the following mapping:
goal_in_ga(x1, x2)  =  goal_in_ga(x1)
U1_ga(x1, x2, x3)  =  U1_ga(x1, x3)
eq_in_ga(x1, x2)  =  eq_in_ga(x1)
.(x1, x2)  =  .(x2)
eq_out_ga(x1, x2)  =  eq_out_ga(x1, x2)
U2_ga(x1, x2, x3)  =  U2_ga(x1, x3)
reduce_in_ggaa(x1, x2, x3, x4)  =  reduce_in_ggaa(x1, x2)
s(x1)  =  s(x1)
0  =  0
U4_ggaa(x1, x2, x3)  =  U4_ggaa(x1, x3)
true_in_  =  true_in_
true_out_  =  true_out_
reduce_out_ggaa(x1, x2, x3, x4)  =  reduce_out_ggaa(x1, x2, x4)
[]  =  []
U5_ggaa(x1, x2, x3)  =  U5_ggaa(x1, x3)
U6_ggaa(x1, x2, x3, x4, x5)  =  U6_ggaa(x2, x3, x5)
vowel_h_w_y_in_a(x1)  =  vowel_h_w_y_in_a
vowel_h_w_y_out_a(x1)  =  vowel_h_w_y_out_a(x1)
U7_ggaa(x1, x2, x3, x4, x5)  =  U7_ggaa(x2, x3, x5)
reduce_in_ggga(x1, x2, x3, x4)  =  reduce_in_ggga(x1, x2, x3)
U4_ggga(x1, x2, x3)  =  U4_ggga(x1, x2, x3)
reduce_out_ggga(x1, x2, x3, x4)  =  reduce_out_ggga(x1, x2, x3, x4)
U5_ggga(x1, x2, x3)  =  U5_ggga(x1, x2, x3)
U6_ggga(x1, x2, x3, x4, x5)  =  U6_ggga(x1, x2, x3, x5)
vowel_h_w_y_in_g(x1)  =  vowel_h_w_y_in_g(x1)
97  =  97
vowel_h_w_y_out_g(x1)  =  vowel_h_w_y_out_g(x1)
101  =  101
105  =  105
111  =  111
117  =  117
104  =  104
119  =  119
121  =  121
U7_ggga(x1, x2, x3, x4, x5)  =  U7_ggga(x1, x2, x3, x5)
U8_ggga(x1, x2, x3, x4, x5)  =  U8_ggga(x1, x2, x3, x5)
U9_ggga(x1, x2, x3, x4, x5, x6)  =  U9_ggga(x2, x3, x4, x6)
U8_ggaa(x1, x2, x3, x4, x5)  =  U8_ggaa(x2, x3, x5)
U9_ggaa(x1, x2, x3, x4, x5, x6)  =  U9_ggaa(x2, x3, x6)
U3_ga(x1, x2, x3)  =  U3_ga(x1, x3)
eq_in_ag(x1, x2)  =  eq_in_ag(x2)
eq_out_ag(x1, x2)  =  eq_out_ag(x1, x2)
goal_out_ga(x1, x2)  =  goal_out_ga(x1, x2)
GOAL_IN_GA(x1, x2)  =  GOAL_IN_GA(x1)
U1_GA(x1, x2, x3)  =  U1_GA(x1, x3)
EQ_IN_GA(x1, x2)  =  EQ_IN_GA(x1)
U2_GA(x1, x2, x3)  =  U2_GA(x1, x3)
REDUCE_IN_GGAA(x1, x2, x3, x4)  =  REDUCE_IN_GGAA(x1, x2)
U4_GGAA(x1, x2, x3)  =  U4_GGAA(x1, x3)
TRUE_IN_  =  TRUE_IN_
U5_GGAA(x1, x2, x3)  =  U5_GGAA(x1, x3)
U6_GGAA(x1, x2, x3, x4, x5)  =  U6_GGAA(x2, x3, x5)
VOWEL_H_W_Y_IN_A(x1)  =  VOWEL_H_W_Y_IN_A
U7_GGAA(x1, x2, x3, x4, x5)  =  U7_GGAA(x2, x3, x5)
REDUCE_IN_GGGA(x1, x2, x3, x4)  =  REDUCE_IN_GGGA(x1, x2, x3)
U4_GGGA(x1, x2, x3)  =  U4_GGGA(x1, x2, x3)
U5_GGGA(x1, x2, x3)  =  U5_GGGA(x1, x2, x3)
U6_GGGA(x1, x2, x3, x4, x5)  =  U6_GGGA(x1, x2, x3, x5)
VOWEL_H_W_Y_IN_G(x1)  =  VOWEL_H_W_Y_IN_G(x1)
U7_GGGA(x1, x2, x3, x4, x5)  =  U7_GGGA(x1, x2, x3, x5)
U8_GGGA(x1, x2, x3, x4, x5)  =  U8_GGGA(x1, x2, x3, x5)
U9_GGGA(x1, x2, x3, x4, x5, x6)  =  U9_GGGA(x2, x3, x4, x6)
U8_GGAA(x1, x2, x3, x4, x5)  =  U8_GGAA(x2, x3, x5)
U9_GGAA(x1, x2, x3, x4, x5, x6)  =  U9_GGAA(x2, x3, x6)
U3_GA(x1, x2, x3)  =  U3_GA(x1, x3)
EQ_IN_AG(x1, x2)  =  EQ_IN_AG(x2)

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

(14) Obligation:

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

GOAL_IN_GA(Name, Code) → U1_GA(Name, Code, eq_in_ga(Name, .(First, Others)))
GOAL_IN_GA(Name, Code) → EQ_IN_GA(Name, .(First, Others))
U1_GA(Name, Code, eq_out_ga(Name, .(First, Others))) → U2_GA(Name, Code, reduce_in_ggaa(Others, s(0), First, Reduced))
U1_GA(Name, Code, eq_out_ga(Name, .(First, Others))) → REDUCE_IN_GGAA(Others, s(0), First, Reduced)
REDUCE_IN_GGAA(X1, s(s(s(s(0)))), X2, []) → U4_GGAA(X1, X2, true_in_)
REDUCE_IN_GGAA(X1, s(s(s(s(0)))), X2, []) → TRUE_IN_
REDUCE_IN_GGAA([], X3, X4, []) → U5_GGAA(X3, X4, true_in_)
REDUCE_IN_GGAA([], X3, X4, []) → TRUE_IN_
REDUCE_IN_GGAA(.(Current, Others), Count, Current, Code) → U6_GGAA(Current, Others, Count, Code, vowel_h_w_y_in_a(Current))
REDUCE_IN_GGAA(.(Current, Others), Count, Current, Code) → VOWEL_H_W_Y_IN_A(Current)
U6_GGAA(Current, Others, Count, Code, vowel_h_w_y_out_a(Current)) → U7_GGAA(Current, Others, Count, Code, reduce_in_ggga(Others, Count, Current, Code))
U6_GGAA(Current, Others, Count, Code, vowel_h_w_y_out_a(Current)) → REDUCE_IN_GGGA(Others, Count, Current, Code)
REDUCE_IN_GGGA(X1, s(s(s(s(0)))), X2, []) → U4_GGGA(X1, X2, true_in_)
REDUCE_IN_GGGA(X1, s(s(s(s(0)))), X2, []) → TRUE_IN_
REDUCE_IN_GGGA([], X3, X4, []) → U5_GGGA(X3, X4, true_in_)
REDUCE_IN_GGGA([], X3, X4, []) → TRUE_IN_
REDUCE_IN_GGGA(.(Current, Others), Count, Current, Code) → U6_GGGA(Current, Others, Count, Code, vowel_h_w_y_in_g(Current))
REDUCE_IN_GGGA(.(Current, Others), Count, Current, Code) → VOWEL_H_W_Y_IN_G(Current)
U6_GGGA(Current, Others, Count, Code, vowel_h_w_y_out_g(Current)) → U7_GGGA(Current, Others, Count, Code, reduce_in_ggga(Others, Count, Current, Code))
U6_GGGA(Current, Others, Count, Code, vowel_h_w_y_out_g(Current)) → REDUCE_IN_GGGA(Others, Count, Current, Code)
REDUCE_IN_GGGA(.(Letter, Others), Count, Letter, Code) → U8_GGGA(Letter, Others, Count, Code, reduce_in_ggga(Others, Count, Letter, Code))
REDUCE_IN_GGGA(.(Letter, Others), Count, Letter, Code) → REDUCE_IN_GGGA(Others, Count, Letter, Code)
REDUCE_IN_GGGA(.(Current, Others), Count, X5, .(Current, Code)) → U9_GGGA(Current, Others, Count, X5, Code, reduce_in_ggaa(Others, s(Count), Current, Code))
REDUCE_IN_GGGA(.(Current, Others), Count, X5, .(Current, Code)) → REDUCE_IN_GGAA(Others, s(Count), Current, Code)
REDUCE_IN_GGAA(.(Letter, Others), Count, Letter, Code) → U8_GGAA(Letter, Others, Count, Code, reduce_in_ggaa(Others, Count, Letter, Code))
REDUCE_IN_GGAA(.(Letter, Others), Count, Letter, Code) → REDUCE_IN_GGAA(Others, Count, Letter, Code)
REDUCE_IN_GGAA(.(Current, Others), Count, X5, .(Current, Code)) → U9_GGAA(Current, Others, Count, X5, Code, reduce_in_ggaa(Others, s(Count), Current, Code))
REDUCE_IN_GGAA(.(Current, Others), Count, X5, .(Current, Code)) → REDUCE_IN_GGAA(Others, s(Count), Current, Code)
U2_GA(Name, Code, reduce_out_ggaa(Others, s(0), First, Reduced)) → U3_GA(Name, Code, eq_in_ag(Code, Reduced))
U2_GA(Name, Code, reduce_out_ggaa(Others, s(0), First, Reduced)) → EQ_IN_AG(Code, Reduced)

The TRS R consists of the following rules:

goal_in_ga(Name, Code) → U1_ga(Name, Code, eq_in_ga(Name, .(First, Others)))
eq_in_ga(X, X) → eq_out_ga(X, X)
U1_ga(Name, Code, eq_out_ga(Name, .(First, Others))) → U2_ga(Name, Code, reduce_in_ggaa(Others, s(0), First, Reduced))
reduce_in_ggaa(X1, s(s(s(s(0)))), X2, []) → U4_ggaa(X1, X2, true_in_)
true_in_ → true_out_
U4_ggaa(X1, X2, true_out_) → reduce_out_ggaa(X1, s(s(s(s(0)))), X2, [])
reduce_in_ggaa([], X3, X4, []) → U5_ggaa(X3, X4, true_in_)
U5_ggaa(X3, X4, true_out_) → reduce_out_ggaa([], X3, X4, [])
reduce_in_ggaa(.(Current, Others), Count, Current, Code) → U6_ggaa(Current, Others, Count, Code, vowel_h_w_y_in_a(Current))
vowel_h_w_y_in_a(97) → vowel_h_w_y_out_a(97)
vowel_h_w_y_in_a(101) → vowel_h_w_y_out_a(101)
vowel_h_w_y_in_a(105) → vowel_h_w_y_out_a(105)
vowel_h_w_y_in_a(111) → vowel_h_w_y_out_a(111)
vowel_h_w_y_in_a(117) → vowel_h_w_y_out_a(117)
vowel_h_w_y_in_a(104) → vowel_h_w_y_out_a(104)
vowel_h_w_y_in_a(119) → vowel_h_w_y_out_a(119)
vowel_h_w_y_in_a(121) → vowel_h_w_y_out_a(121)
U6_ggaa(Current, Others, Count, Code, vowel_h_w_y_out_a(Current)) → U7_ggaa(Current, Others, Count, Code, reduce_in_ggga(Others, Count, Current, Code))
reduce_in_ggga(X1, s(s(s(s(0)))), X2, []) → U4_ggga(X1, X2, true_in_)
U4_ggga(X1, X2, true_out_) → reduce_out_ggga(X1, s(s(s(s(0)))), X2, [])
reduce_in_ggga([], X3, X4, []) → U5_ggga(X3, X4, true_in_)
U5_ggga(X3, X4, true_out_) → reduce_out_ggga([], X3, X4, [])
reduce_in_ggga(.(Current, Others), Count, Current, Code) → U6_ggga(Current, Others, Count, Code, vowel_h_w_y_in_g(Current))
vowel_h_w_y_in_g(97) → vowel_h_w_y_out_g(97)
vowel_h_w_y_in_g(101) → vowel_h_w_y_out_g(101)
vowel_h_w_y_in_g(105) → vowel_h_w_y_out_g(105)
vowel_h_w_y_in_g(111) → vowel_h_w_y_out_g(111)
vowel_h_w_y_in_g(117) → vowel_h_w_y_out_g(117)
vowel_h_w_y_in_g(104) → vowel_h_w_y_out_g(104)
vowel_h_w_y_in_g(119) → vowel_h_w_y_out_g(119)
vowel_h_w_y_in_g(121) → vowel_h_w_y_out_g(121)
U6_ggga(Current, Others, Count, Code, vowel_h_w_y_out_g(Current)) → U7_ggga(Current, Others, Count, Code, reduce_in_ggga(Others, Count, Current, Code))
reduce_in_ggga(.(Letter, Others), Count, Letter, Code) → U8_ggga(Letter, Others, Count, Code, reduce_in_ggga(Others, Count, Letter, Code))
reduce_in_ggga(.(Current, Others), Count, X5, .(Current, Code)) → U9_ggga(Current, Others, Count, X5, Code, reduce_in_ggaa(Others, s(Count), Current, Code))
reduce_in_ggaa(.(Letter, Others), Count, Letter, Code) → U8_ggaa(Letter, Others, Count, Code, reduce_in_ggaa(Others, Count, Letter, Code))
reduce_in_ggaa(.(Current, Others), Count, X5, .(Current, Code)) → U9_ggaa(Current, Others, Count, X5, Code, reduce_in_ggaa(Others, s(Count), Current, Code))
U9_ggaa(Current, Others, Count, X5, Code, reduce_out_ggaa(Others, s(Count), Current, Code)) → reduce_out_ggaa(.(Current, Others), Count, X5, .(Current, Code))
U8_ggaa(Letter, Others, Count, Code, reduce_out_ggaa(Others, Count, Letter, Code)) → reduce_out_ggaa(.(Letter, Others), Count, Letter, Code)
U9_ggga(Current, Others, Count, X5, Code, reduce_out_ggaa(Others, s(Count), Current, Code)) → reduce_out_ggga(.(Current, Others), Count, X5, .(Current, Code))
U8_ggga(Letter, Others, Count, Code, reduce_out_ggga(Others, Count, Letter, Code)) → reduce_out_ggga(.(Letter, Others), Count, Letter, Code)
U7_ggga(Current, Others, Count, Code, reduce_out_ggga(Others, Count, Current, Code)) → reduce_out_ggga(.(Current, Others), Count, Current, Code)
U7_ggaa(Current, Others, Count, Code, reduce_out_ggga(Others, Count, Current, Code)) → reduce_out_ggaa(.(Current, Others), Count, Current, Code)
U2_ga(Name, Code, reduce_out_ggaa(Others, s(0), First, Reduced)) → U3_ga(Name, Code, eq_in_ag(Code, Reduced))
eq_in_ag(X, X) → eq_out_ag(X, X)
U3_ga(Name, Code, eq_out_ag(Code, Reduced)) → goal_out_ga(Name, Code)

The argument filtering Pi contains the following mapping:
goal_in_ga(x1, x2)  =  goal_in_ga(x1)
U1_ga(x1, x2, x3)  =  U1_ga(x1, x3)
eq_in_ga(x1, x2)  =  eq_in_ga(x1)
.(x1, x2)  =  .(x2)
eq_out_ga(x1, x2)  =  eq_out_ga(x1, x2)
U2_ga(x1, x2, x3)  =  U2_ga(x1, x3)
reduce_in_ggaa(x1, x2, x3, x4)  =  reduce_in_ggaa(x1, x2)
s(x1)  =  s(x1)
0  =  0
U4_ggaa(x1, x2, x3)  =  U4_ggaa(x1, x3)
true_in_  =  true_in_
true_out_  =  true_out_
reduce_out_ggaa(x1, x2, x3, x4)  =  reduce_out_ggaa(x1, x2, x4)
[]  =  []
U5_ggaa(x1, x2, x3)  =  U5_ggaa(x1, x3)
U6_ggaa(x1, x2, x3, x4, x5)  =  U6_ggaa(x2, x3, x5)
vowel_h_w_y_in_a(x1)  =  vowel_h_w_y_in_a
vowel_h_w_y_out_a(x1)  =  vowel_h_w_y_out_a(x1)
U7_ggaa(x1, x2, x3, x4, x5)  =  U7_ggaa(x2, x3, x5)
reduce_in_ggga(x1, x2, x3, x4)  =  reduce_in_ggga(x1, x2, x3)
U4_ggga(x1, x2, x3)  =  U4_ggga(x1, x2, x3)
reduce_out_ggga(x1, x2, x3, x4)  =  reduce_out_ggga(x1, x2, x3, x4)
U5_ggga(x1, x2, x3)  =  U5_ggga(x1, x2, x3)
U6_ggga(x1, x2, x3, x4, x5)  =  U6_ggga(x1, x2, x3, x5)
vowel_h_w_y_in_g(x1)  =  vowel_h_w_y_in_g(x1)
97  =  97
vowel_h_w_y_out_g(x1)  =  vowel_h_w_y_out_g(x1)
101  =  101
105  =  105
111  =  111
117  =  117
104  =  104
119  =  119
121  =  121
U7_ggga(x1, x2, x3, x4, x5)  =  U7_ggga(x1, x2, x3, x5)
U8_ggga(x1, x2, x3, x4, x5)  =  U8_ggga(x1, x2, x3, x5)
U9_ggga(x1, x2, x3, x4, x5, x6)  =  U9_ggga(x2, x3, x4, x6)
U8_ggaa(x1, x2, x3, x4, x5)  =  U8_ggaa(x2, x3, x5)
U9_ggaa(x1, x2, x3, x4, x5, x6)  =  U9_ggaa(x2, x3, x6)
U3_ga(x1, x2, x3)  =  U3_ga(x1, x3)
eq_in_ag(x1, x2)  =  eq_in_ag(x2)
eq_out_ag(x1, x2)  =  eq_out_ag(x1, x2)
goal_out_ga(x1, x2)  =  goal_out_ga(x1, x2)
GOAL_IN_GA(x1, x2)  =  GOAL_IN_GA(x1)
U1_GA(x1, x2, x3)  =  U1_GA(x1, x3)
EQ_IN_GA(x1, x2)  =  EQ_IN_GA(x1)
U2_GA(x1, x2, x3)  =  U2_GA(x1, x3)
REDUCE_IN_GGAA(x1, x2, x3, x4)  =  REDUCE_IN_GGAA(x1, x2)
U4_GGAA(x1, x2, x3)  =  U4_GGAA(x1, x3)
TRUE_IN_  =  TRUE_IN_
U5_GGAA(x1, x2, x3)  =  U5_GGAA(x1, x3)
U6_GGAA(x1, x2, x3, x4, x5)  =  U6_GGAA(x2, x3, x5)
VOWEL_H_W_Y_IN_A(x1)  =  VOWEL_H_W_Y_IN_A
U7_GGAA(x1, x2, x3, x4, x5)  =  U7_GGAA(x2, x3, x5)
REDUCE_IN_GGGA(x1, x2, x3, x4)  =  REDUCE_IN_GGGA(x1, x2, x3)
U4_GGGA(x1, x2, x3)  =  U4_GGGA(x1, x2, x3)
U5_GGGA(x1, x2, x3)  =  U5_GGGA(x1, x2, x3)
U6_GGGA(x1, x2, x3, x4, x5)  =  U6_GGGA(x1, x2, x3, x5)
VOWEL_H_W_Y_IN_G(x1)  =  VOWEL_H_W_Y_IN_G(x1)
U7_GGGA(x1, x2, x3, x4, x5)  =  U7_GGGA(x1, x2, x3, x5)
U8_GGGA(x1, x2, x3, x4, x5)  =  U8_GGGA(x1, x2, x3, x5)
U9_GGGA(x1, x2, x3, x4, x5, x6)  =  U9_GGGA(x2, x3, x4, x6)
U8_GGAA(x1, x2, x3, x4, x5)  =  U8_GGAA(x2, x3, x5)
U9_GGAA(x1, x2, x3, x4, x5, x6)  =  U9_GGAA(x2, x3, x6)
U3_GA(x1, x2, x3)  =  U3_GA(x1, x3)
EQ_IN_AG(x1, x2)  =  EQ_IN_AG(x2)

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

(15) DependencyGraphProof (EQUIVALENT transformation)

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

(16) Obligation:

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

REDUCE_IN_GGAA(.(Current, Others), Count, Current, Code) → U6_GGAA(Current, Others, Count, Code, vowel_h_w_y_in_a(Current))
U6_GGAA(Current, Others, Count, Code, vowel_h_w_y_out_a(Current)) → REDUCE_IN_GGGA(Others, Count, Current, Code)
REDUCE_IN_GGGA(.(Current, Others), Count, Current, Code) → U6_GGGA(Current, Others, Count, Code, vowel_h_w_y_in_g(Current))
U6_GGGA(Current, Others, Count, Code, vowel_h_w_y_out_g(Current)) → REDUCE_IN_GGGA(Others, Count, Current, Code)
REDUCE_IN_GGGA(.(Letter, Others), Count, Letter, Code) → REDUCE_IN_GGGA(Others, Count, Letter, Code)
REDUCE_IN_GGGA(.(Current, Others), Count, X5, .(Current, Code)) → REDUCE_IN_GGAA(Others, s(Count), Current, Code)
REDUCE_IN_GGAA(.(Letter, Others), Count, Letter, Code) → REDUCE_IN_GGAA(Others, Count, Letter, Code)
REDUCE_IN_GGAA(.(Current, Others), Count, X5, .(Current, Code)) → REDUCE_IN_GGAA(Others, s(Count), Current, Code)

The TRS R consists of the following rules:

goal_in_ga(Name, Code) → U1_ga(Name, Code, eq_in_ga(Name, .(First, Others)))
eq_in_ga(X, X) → eq_out_ga(X, X)
U1_ga(Name, Code, eq_out_ga(Name, .(First, Others))) → U2_ga(Name, Code, reduce_in_ggaa(Others, s(0), First, Reduced))
reduce_in_ggaa(X1, s(s(s(s(0)))), X2, []) → U4_ggaa(X1, X2, true_in_)
true_in_ → true_out_
U4_ggaa(X1, X2, true_out_) → reduce_out_ggaa(X1, s(s(s(s(0)))), X2, [])
reduce_in_ggaa([], X3, X4, []) → U5_ggaa(X3, X4, true_in_)
U5_ggaa(X3, X4, true_out_) → reduce_out_ggaa([], X3, X4, [])
reduce_in_ggaa(.(Current, Others), Count, Current, Code) → U6_ggaa(Current, Others, Count, Code, vowel_h_w_y_in_a(Current))
vowel_h_w_y_in_a(97) → vowel_h_w_y_out_a(97)
vowel_h_w_y_in_a(101) → vowel_h_w_y_out_a(101)
vowel_h_w_y_in_a(105) → vowel_h_w_y_out_a(105)
vowel_h_w_y_in_a(111) → vowel_h_w_y_out_a(111)
vowel_h_w_y_in_a(117) → vowel_h_w_y_out_a(117)
vowel_h_w_y_in_a(104) → vowel_h_w_y_out_a(104)
vowel_h_w_y_in_a(119) → vowel_h_w_y_out_a(119)
vowel_h_w_y_in_a(121) → vowel_h_w_y_out_a(121)
U6_ggaa(Current, Others, Count, Code, vowel_h_w_y_out_a(Current)) → U7_ggaa(Current, Others, Count, Code, reduce_in_ggga(Others, Count, Current, Code))
reduce_in_ggga(X1, s(s(s(s(0)))), X2, []) → U4_ggga(X1, X2, true_in_)
U4_ggga(X1, X2, true_out_) → reduce_out_ggga(X1, s(s(s(s(0)))), X2, [])
reduce_in_ggga([], X3, X4, []) → U5_ggga(X3, X4, true_in_)
U5_ggga(X3, X4, true_out_) → reduce_out_ggga([], X3, X4, [])
reduce_in_ggga(.(Current, Others), Count, Current, Code) → U6_ggga(Current, Others, Count, Code, vowel_h_w_y_in_g(Current))
vowel_h_w_y_in_g(97) → vowel_h_w_y_out_g(97)
vowel_h_w_y_in_g(101) → vowel_h_w_y_out_g(101)
vowel_h_w_y_in_g(105) → vowel_h_w_y_out_g(105)
vowel_h_w_y_in_g(111) → vowel_h_w_y_out_g(111)
vowel_h_w_y_in_g(117) → vowel_h_w_y_out_g(117)
vowel_h_w_y_in_g(104) → vowel_h_w_y_out_g(104)
vowel_h_w_y_in_g(119) → vowel_h_w_y_out_g(119)
vowel_h_w_y_in_g(121) → vowel_h_w_y_out_g(121)
U6_ggga(Current, Others, Count, Code, vowel_h_w_y_out_g(Current)) → U7_ggga(Current, Others, Count, Code, reduce_in_ggga(Others, Count, Current, Code))
reduce_in_ggga(.(Letter, Others), Count, Letter, Code) → U8_ggga(Letter, Others, Count, Code, reduce_in_ggga(Others, Count, Letter, Code))
reduce_in_ggga(.(Current, Others), Count, X5, .(Current, Code)) → U9_ggga(Current, Others, Count, X5, Code, reduce_in_ggaa(Others, s(Count), Current, Code))
reduce_in_ggaa(.(Letter, Others), Count, Letter, Code) → U8_ggaa(Letter, Others, Count, Code, reduce_in_ggaa(Others, Count, Letter, Code))
reduce_in_ggaa(.(Current, Others), Count, X5, .(Current, Code)) → U9_ggaa(Current, Others, Count, X5, Code, reduce_in_ggaa(Others, s(Count), Current, Code))
U9_ggaa(Current, Others, Count, X5, Code, reduce_out_ggaa(Others, s(Count), Current, Code)) → reduce_out_ggaa(.(Current, Others), Count, X5, .(Current, Code))
U8_ggaa(Letter, Others, Count, Code, reduce_out_ggaa(Others, Count, Letter, Code)) → reduce_out_ggaa(.(Letter, Others), Count, Letter, Code)
U9_ggga(Current, Others, Count, X5, Code, reduce_out_ggaa(Others, s(Count), Current, Code)) → reduce_out_ggga(.(Current, Others), Count, X5, .(Current, Code))
U8_ggga(Letter, Others, Count, Code, reduce_out_ggga(Others, Count, Letter, Code)) → reduce_out_ggga(.(Letter, Others), Count, Letter, Code)
U7_ggga(Current, Others, Count, Code, reduce_out_ggga(Others, Count, Current, Code)) → reduce_out_ggga(.(Current, Others), Count, Current, Code)
U7_ggaa(Current, Others, Count, Code, reduce_out_ggga(Others, Count, Current, Code)) → reduce_out_ggaa(.(Current, Others), Count, Current, Code)
U2_ga(Name, Code, reduce_out_ggaa(Others, s(0), First, Reduced)) → U3_ga(Name, Code, eq_in_ag(Code, Reduced))
eq_in_ag(X, X) → eq_out_ag(X, X)
U3_ga(Name, Code, eq_out_ag(Code, Reduced)) → goal_out_ga(Name, Code)

The argument filtering Pi contains the following mapping:
goal_in_ga(x1, x2)  =  goal_in_ga(x1)
U1_ga(x1, x2, x3)  =  U1_ga(x1, x3)
eq_in_ga(x1, x2)  =  eq_in_ga(x1)
.(x1, x2)  =  .(x2)
eq_out_ga(x1, x2)  =  eq_out_ga(x1, x2)
U2_ga(x1, x2, x3)  =  U2_ga(x1, x3)
reduce_in_ggaa(x1, x2, x3, x4)  =  reduce_in_ggaa(x1, x2)
s(x1)  =  s(x1)
0  =  0
U4_ggaa(x1, x2, x3)  =  U4_ggaa(x1, x3)
true_in_  =  true_in_
true_out_  =  true_out_
reduce_out_ggaa(x1, x2, x3, x4)  =  reduce_out_ggaa(x1, x2, x4)
[]  =  []
U5_ggaa(x1, x2, x3)  =  U5_ggaa(x1, x3)
U6_ggaa(x1, x2, x3, x4, x5)  =  U6_ggaa(x2, x3, x5)
vowel_h_w_y_in_a(x1)  =  vowel_h_w_y_in_a
vowel_h_w_y_out_a(x1)  =  vowel_h_w_y_out_a(x1)
U7_ggaa(x1, x2, x3, x4, x5)  =  U7_ggaa(x2, x3, x5)
reduce_in_ggga(x1, x2, x3, x4)  =  reduce_in_ggga(x1, x2, x3)
U4_ggga(x1, x2, x3)  =  U4_ggga(x1, x2, x3)
reduce_out_ggga(x1, x2, x3, x4)  =  reduce_out_ggga(x1, x2, x3, x4)
U5_ggga(x1, x2, x3)  =  U5_ggga(x1, x2, x3)
U6_ggga(x1, x2, x3, x4, x5)  =  U6_ggga(x1, x2, x3, x5)
vowel_h_w_y_in_g(x1)  =  vowel_h_w_y_in_g(x1)
97  =  97
vowel_h_w_y_out_g(x1)  =  vowel_h_w_y_out_g(x1)
101  =  101
105  =  105
111  =  111
117  =  117
104  =  104
119  =  119
121  =  121
U7_ggga(x1, x2, x3, x4, x5)  =  U7_ggga(x1, x2, x3, x5)
U8_ggga(x1, x2, x3, x4, x5)  =  U8_ggga(x1, x2, x3, x5)
U9_ggga(x1, x2, x3, x4, x5, x6)  =  U9_ggga(x2, x3, x4, x6)
U8_ggaa(x1, x2, x3, x4, x5)  =  U8_ggaa(x2, x3, x5)
U9_ggaa(x1, x2, x3, x4, x5, x6)  =  U9_ggaa(x2, x3, x6)
U3_ga(x1, x2, x3)  =  U3_ga(x1, x3)
eq_in_ag(x1, x2)  =  eq_in_ag(x2)
eq_out_ag(x1, x2)  =  eq_out_ag(x1, x2)
goal_out_ga(x1, x2)  =  goal_out_ga(x1, x2)
REDUCE_IN_GGAA(x1, x2, x3, x4)  =  REDUCE_IN_GGAA(x1, x2)
U6_GGAA(x1, x2, x3, x4, x5)  =  U6_GGAA(x2, x3, x5)
REDUCE_IN_GGGA(x1, x2, x3, x4)  =  REDUCE_IN_GGGA(x1, x2, x3)
U6_GGGA(x1, x2, x3, x4, x5)  =  U6_GGGA(x1, x2, x3, x5)

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

(17) UsableRulesProof (EQUIVALENT transformation)

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

(18) Obligation:

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

REDUCE_IN_GGAA(.(Current, Others), Count, Current, Code) → U6_GGAA(Current, Others, Count, Code, vowel_h_w_y_in_a(Current))
U6_GGAA(Current, Others, Count, Code, vowel_h_w_y_out_a(Current)) → REDUCE_IN_GGGA(Others, Count, Current, Code)
REDUCE_IN_GGGA(.(Current, Others), Count, Current, Code) → U6_GGGA(Current, Others, Count, Code, vowel_h_w_y_in_g(Current))
U6_GGGA(Current, Others, Count, Code, vowel_h_w_y_out_g(Current)) → REDUCE_IN_GGGA(Others, Count, Current, Code)
REDUCE_IN_GGGA(.(Letter, Others), Count, Letter, Code) → REDUCE_IN_GGGA(Others, Count, Letter, Code)
REDUCE_IN_GGGA(.(Current, Others), Count, X5, .(Current, Code)) → REDUCE_IN_GGAA(Others, s(Count), Current, Code)
REDUCE_IN_GGAA(.(Letter, Others), Count, Letter, Code) → REDUCE_IN_GGAA(Others, Count, Letter, Code)
REDUCE_IN_GGAA(.(Current, Others), Count, X5, .(Current, Code)) → REDUCE_IN_GGAA(Others, s(Count), Current, Code)

The TRS R consists of the following rules:

vowel_h_w_y_in_a(97) → vowel_h_w_y_out_a(97)
vowel_h_w_y_in_a(101) → vowel_h_w_y_out_a(101)
vowel_h_w_y_in_a(105) → vowel_h_w_y_out_a(105)
vowel_h_w_y_in_a(111) → vowel_h_w_y_out_a(111)
vowel_h_w_y_in_a(117) → vowel_h_w_y_out_a(117)
vowel_h_w_y_in_a(104) → vowel_h_w_y_out_a(104)
vowel_h_w_y_in_a(119) → vowel_h_w_y_out_a(119)
vowel_h_w_y_in_a(121) → vowel_h_w_y_out_a(121)
vowel_h_w_y_in_g(97) → vowel_h_w_y_out_g(97)
vowel_h_w_y_in_g(101) → vowel_h_w_y_out_g(101)
vowel_h_w_y_in_g(105) → vowel_h_w_y_out_g(105)
vowel_h_w_y_in_g(111) → vowel_h_w_y_out_g(111)
vowel_h_w_y_in_g(117) → vowel_h_w_y_out_g(117)
vowel_h_w_y_in_g(104) → vowel_h_w_y_out_g(104)
vowel_h_w_y_in_g(119) → vowel_h_w_y_out_g(119)
vowel_h_w_y_in_g(121) → vowel_h_w_y_out_g(121)

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x2)
s(x1)  =  s(x1)
vowel_h_w_y_in_a(x1)  =  vowel_h_w_y_in_a
vowel_h_w_y_out_a(x1)  =  vowel_h_w_y_out_a(x1)
vowel_h_w_y_in_g(x1)  =  vowel_h_w_y_in_g(x1)
97  =  97
vowel_h_w_y_out_g(x1)  =  vowel_h_w_y_out_g(x1)
101  =  101
105  =  105
111  =  111
117  =  117
104  =  104
119  =  119
121  =  121
REDUCE_IN_GGAA(x1, x2, x3, x4)  =  REDUCE_IN_GGAA(x1, x2)
U6_GGAA(x1, x2, x3, x4, x5)  =  U6_GGAA(x2, x3, x5)
REDUCE_IN_GGGA(x1, x2, x3, x4)  =  REDUCE_IN_GGGA(x1, x2, x3)
U6_GGGA(x1, x2, x3, x4, x5)  =  U6_GGGA(x1, x2, x3, x5)

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:

REDUCE_IN_GGAA(.(Others), Count) → U6_GGAA(Others, Count, vowel_h_w_y_in_a)
U6_GGAA(Others, Count, vowel_h_w_y_out_a(Current)) → REDUCE_IN_GGGA(Others, Count, Current)
REDUCE_IN_GGGA(.(Others), Count, Current) → U6_GGGA(Current, Others, Count, vowel_h_w_y_in_g(Current))
U6_GGGA(Current, Others, Count, vowel_h_w_y_out_g(Current)) → REDUCE_IN_GGGA(Others, Count, Current)
REDUCE_IN_GGGA(.(Others), Count, Letter) → REDUCE_IN_GGGA(Others, Count, Letter)
REDUCE_IN_GGGA(.(Others), Count, X5) → REDUCE_IN_GGAA(Others, s(Count))
REDUCE_IN_GGAA(.(Others), Count) → REDUCE_IN_GGAA(Others, Count)
REDUCE_IN_GGAA(.(Others), Count) → REDUCE_IN_GGAA(Others, s(Count))

The TRS R consists of the following rules:

vowel_h_w_y_in_a → vowel_h_w_y_out_a(97)
vowel_h_w_y_in_a → vowel_h_w_y_out_a(101)
vowel_h_w_y_in_a → vowel_h_w_y_out_a(105)
vowel_h_w_y_in_a → vowel_h_w_y_out_a(111)
vowel_h_w_y_in_a → vowel_h_w_y_out_a(117)
vowel_h_w_y_in_a → vowel_h_w_y_out_a(104)
vowel_h_w_y_in_a → vowel_h_w_y_out_a(119)
vowel_h_w_y_in_a → vowel_h_w_y_out_a(121)
vowel_h_w_y_in_g(97) → vowel_h_w_y_out_g(97)
vowel_h_w_y_in_g(101) → vowel_h_w_y_out_g(101)
vowel_h_w_y_in_g(105) → vowel_h_w_y_out_g(105)
vowel_h_w_y_in_g(111) → vowel_h_w_y_out_g(111)
vowel_h_w_y_in_g(117) → vowel_h_w_y_out_g(117)
vowel_h_w_y_in_g(104) → vowel_h_w_y_out_g(104)
vowel_h_w_y_in_g(119) → vowel_h_w_y_out_g(119)
vowel_h_w_y_in_g(121) → vowel_h_w_y_out_g(121)

The set Q consists of the following terms:

vowel_h_w_y_in_a
vowel_h_w_y_in_g(x0)

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

(21) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • U6_GGAA(Others, Count, vowel_h_w_y_out_a(Current)) → REDUCE_IN_GGGA(Others, Count, Current)
    The graph contains the following edges 1 >= 1, 2 >= 2, 3 > 3

  • REDUCE_IN_GGGA(.(Others), Count, X5) → REDUCE_IN_GGAA(Others, s(Count))
    The graph contains the following edges 1 > 1

  • REDUCE_IN_GGAA(.(Others), Count) → U6_GGAA(Others, Count, vowel_h_w_y_in_a)
    The graph contains the following edges 1 > 1, 2 >= 2

  • U6_GGGA(Current, Others, Count, vowel_h_w_y_out_g(Current)) → REDUCE_IN_GGGA(Others, Count, Current)
    The graph contains the following edges 2 >= 1, 3 >= 2, 1 >= 3, 4 > 3

  • REDUCE_IN_GGGA(.(Others), Count, Letter) → REDUCE_IN_GGGA(Others, Count, Letter)
    The graph contains the following edges 1 > 1, 2 >= 2, 3 >= 3

  • REDUCE_IN_GGGA(.(Others), Count, Current) → U6_GGGA(Current, Others, Count, vowel_h_w_y_in_g(Current))
    The graph contains the following edges 3 >= 1, 1 > 2, 2 >= 3

  • REDUCE_IN_GGAA(.(Others), Count) → REDUCE_IN_GGAA(Others, Count)
    The graph contains the following edges 1 > 1, 2 >= 2

  • REDUCE_IN_GGAA(.(Others), Count) → REDUCE_IN_GGAA(Others, s(Count))
    The graph contains the following edges 1 > 1

(22) TRUE