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

0 Prolog
↳1 CutEliminatorProof (⇒, 0 ms)
↳2 Prolog
↳3 PrologToPiTRSProof (⇒, 65 ms)
↳4 PiTRS
↳5 DependencyPairsProof (⇔, 192 ms)
↳6 PiDP
↳7 DependencyGraphProof (⇔, 0 ms)
↳8 PiDP
↳9 UsableRulesProof (⇔, 0 ms)
↳10 PiDP
↳11 PiDPToQDPProof (⇒, 8 ms)
↳12 QDP
↳13 QDPSizeChangeProof (⇔, 0 ms)
↳14 YES

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

Query: 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, []).
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).

Query: goal(g,a)

(3) PrologToPiTRSProof (SOUND transformation)

We use the technique of [TOCL09]. 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, []) → reduce_out_ggaa(X1, s(s(s(s(0)))), X2, [])
reduce_in_ggaa([], X3, X4, []) → reduce_out_ggaa([], X3, X4, [])
reduce_in_ggaa(.(Current, Others), Count, Current, Code) → U4_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)
U4_ggaa(Current, Others, Count, Code, vowel_h_w_y_out_a(Current)) → U5_ggaa(Current, Others, Count, Code, reduce_in_ggga(Others, Count, Current, Code))
reduce_in_ggga(X1, s(s(s(s(0)))), X2, []) → reduce_out_ggga(X1, s(s(s(s(0)))), X2, [])
reduce_in_ggga([], X3, X4, []) → reduce_out_ggga([], X3, X4, [])
reduce_in_ggga(.(Current, Others), Count, Current, Code) → U4_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)
U4_ggga(Current, Others, Count, Code, vowel_h_w_y_out_g(Current)) → U5_ggga(Current, Others, Count, Code, reduce_in_ggga(Others, Count, Current, Code))
reduce_in_ggga(.(Letter, Others), Count, Letter, Code) → U6_ggga(Letter, Others, Count, Code, reduce_in_ggga(Others, Count, Letter, Code))
reduce_in_ggga(.(Current, Others), Count, X5, .(Current, Code)) → U7_ggga(Current, Others, Count, X5, Code, reduce_in_ggaa(Others, s(Count), Current, Code))
reduce_in_ggaa(.(Letter, Others), Count, Letter, Code) → U6_ggaa(Letter, Others, Count, Code, reduce_in_ggaa(Others, Count, Letter, Code))
reduce_in_ggaa(.(Current, Others), Count, X5, .(Current, Code)) → U7_ggaa(Current, Others, Count, X5, Code, reduce_in_ggaa(Others, s(Count), Current, Code))
U7_ggaa(Current, Others, Count, X5, Code, reduce_out_ggaa(Others, s(Count), Current, Code)) → reduce_out_ggaa(.(Current, Others), Count, X5, .(Current, Code))
U6_ggaa(Letter, Others, Count, Code, reduce_out_ggaa(Others, Count, Letter, Code)) → reduce_out_ggaa(.(Letter, Others), Count, Letter, Code)
U7_ggga(Current, Others, Count, X5, Code, reduce_out_ggaa(Others, s(Count), Current, Code)) → reduce_out_ggga(.(Current, Others), Count, X5, .(Current, Code))
U6_ggga(Letter, Others, Count, Code, reduce_out_ggga(Others, Count, Letter, Code)) → reduce_out_ggga(.(Letter, Others), Count, Letter, Code)
U5_ggga(Current, Others, Count, Code, reduce_out_ggga(Others, Count, Current, Code)) → reduce_out_ggga(.(Current, Others), Count, Current, Code)
U5_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
reduce_out_ggaa(x1, x2, x3, x4)  =  reduce_out_ggaa(x1, x2, x4)
[]  =  []
U4_ggaa(x1, x2, x3, x4, x5)  =  U4_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)
U5_ggaa(x1, x2, x3, x4, x5)  =  U5_ggaa(x2, x3, x5)
reduce_in_ggga(x1, x2, x3, x4)  =  reduce_in_ggga(x1, x2, x3)
reduce_out_ggga(x1, x2, x3, x4)  =  reduce_out_ggga(x1, x2, x3, x4)
U4_ggga(x1, x2, x3, x4, x5)  =  U4_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
U5_ggga(x1, x2, x3, x4, x5)  =  U5_ggga(x1, x2, x3, x5)
U6_ggga(x1, x2, x3, x4, x5)  =  U6_ggga(x1, x2, x3, x5)
U7_ggga(x1, x2, x3, x4, x5, x6)  =  U7_ggga(x2, x3, x4, x6)
U6_ggaa(x1, x2, x3, x4, x5)  =  U6_ggaa(x2, x3, x5)
U7_ggaa(x1, x2, x3, x4, x5, x6)  =  U7_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

(4) 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, []) → reduce_out_ggaa(X1, s(s(s(s(0)))), X2, [])
reduce_in_ggaa([], X3, X4, []) → reduce_out_ggaa([], X3, X4, [])
reduce_in_ggaa(.(Current, Others), Count, Current, Code) → U4_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)
U4_ggaa(Current, Others, Count, Code, vowel_h_w_y_out_a(Current)) → U5_ggaa(Current, Others, Count, Code, reduce_in_ggga(Others, Count, Current, Code))
reduce_in_ggga(X1, s(s(s(s(0)))), X2, []) → reduce_out_ggga(X1, s(s(s(s(0)))), X2, [])
reduce_in_ggga([], X3, X4, []) → reduce_out_ggga([], X3, X4, [])
reduce_in_ggga(.(Current, Others), Count, Current, Code) → U4_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)
U4_ggga(Current, Others, Count, Code, vowel_h_w_y_out_g(Current)) → U5_ggga(Current, Others, Count, Code, reduce_in_ggga(Others, Count, Current, Code))
reduce_in_ggga(.(Letter, Others), Count, Letter, Code) → U6_ggga(Letter, Others, Count, Code, reduce_in_ggga(Others, Count, Letter, Code))
reduce_in_ggga(.(Current, Others), Count, X5, .(Current, Code)) → U7_ggga(Current, Others, Count, X5, Code, reduce_in_ggaa(Others, s(Count), Current, Code))
reduce_in_ggaa(.(Letter, Others), Count, Letter, Code) → U6_ggaa(Letter, Others, Count, Code, reduce_in_ggaa(Others, Count, Letter, Code))
reduce_in_ggaa(.(Current, Others), Count, X5, .(Current, Code)) → U7_ggaa(Current, Others, Count, X5, Code, reduce_in_ggaa(Others, s(Count), Current, Code))
U7_ggaa(Current, Others, Count, X5, Code, reduce_out_ggaa(Others, s(Count), Current, Code)) → reduce_out_ggaa(.(Current, Others), Count, X5, .(Current, Code))
U6_ggaa(Letter, Others, Count, Code, reduce_out_ggaa(Others, Count, Letter, Code)) → reduce_out_ggaa(.(Letter, Others), Count, Letter, Code)
U7_ggga(Current, Others, Count, X5, Code, reduce_out_ggaa(Others, s(Count), Current, Code)) → reduce_out_ggga(.(Current, Others), Count, X5, .(Current, Code))
U6_ggga(Letter, Others, Count, Code, reduce_out_ggga(Others, Count, Letter, Code)) → reduce_out_ggga(.(Letter, Others), Count, Letter, Code)
U5_ggga(Current, Others, Count, Code, reduce_out_ggga(Others, Count, Current, Code)) → reduce_out_ggga(.(Current, Others), Count, Current, Code)
U5_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
reduce_out_ggaa(x1, x2, x3, x4)  =  reduce_out_ggaa(x1, x2, x4)
[]  =  []
U4_ggaa(x1, x2, x3, x4, x5)  =  U4_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)
U5_ggaa(x1, x2, x3, x4, x5)  =  U5_ggaa(x2, x3, x5)
reduce_in_ggga(x1, x2, x3, x4)  =  reduce_in_ggga(x1, x2, x3)
reduce_out_ggga(x1, x2, x3, x4)  =  reduce_out_ggga(x1, x2, x3, x4)
U4_ggga(x1, x2, x3, x4, x5)  =  U4_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
U5_ggga(x1, x2, x3, x4, x5)  =  U5_ggga(x1, x2, x3, x5)
U6_ggga(x1, x2, x3, x4, x5)  =  U6_ggga(x1, x2, x3, x5)
U7_ggga(x1, x2, x3, x4, x5, x6)  =  U7_ggga(x2, x3, x4, x6)
U6_ggaa(x1, x2, x3, x4, x5)  =  U6_ggaa(x2, x3, x5)
U7_ggaa(x1, x2, x3, x4, x5, x6)  =  U7_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)

(5) DependencyPairsProof (EQUIVALENT transformation)

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

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(.(Current, Others), Count, Current, Code) → U4_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)
U4_GGAA(Current, Others, Count, Code, vowel_h_w_y_out_a(Current)) → U5_GGAA(Current, Others, Count, Code, reduce_in_ggga(Others, Count, Current, Code))
U4_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) → U4_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)
U4_GGGA(Current, Others, Count, Code, vowel_h_w_y_out_g(Current)) → U5_GGGA(Current, Others, Count, Code, reduce_in_ggga(Others, Count, Current, Code))
U4_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) → U6_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)) → U7_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) → U6_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)) → U7_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, []) → reduce_out_ggaa(X1, s(s(s(s(0)))), X2, [])
reduce_in_ggaa([], X3, X4, []) → reduce_out_ggaa([], X3, X4, [])
reduce_in_ggaa(.(Current, Others), Count, Current, Code) → U4_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)
U4_ggaa(Current, Others, Count, Code, vowel_h_w_y_out_a(Current)) → U5_ggaa(Current, Others, Count, Code, reduce_in_ggga(Others, Count, Current, Code))
reduce_in_ggga(X1, s(s(s(s(0)))), X2, []) → reduce_out_ggga(X1, s(s(s(s(0)))), X2, [])
reduce_in_ggga([], X3, X4, []) → reduce_out_ggga([], X3, X4, [])
reduce_in_ggga(.(Current, Others), Count, Current, Code) → U4_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)
U4_ggga(Current, Others, Count, Code, vowel_h_w_y_out_g(Current)) → U5_ggga(Current, Others, Count, Code, reduce_in_ggga(Others, Count, Current, Code))
reduce_in_ggga(.(Letter, Others), Count, Letter, Code) → U6_ggga(Letter, Others, Count, Code, reduce_in_ggga(Others, Count, Letter, Code))
reduce_in_ggga(.(Current, Others), Count, X5, .(Current, Code)) → U7_ggga(Current, Others, Count, X5, Code, reduce_in_ggaa(Others, s(Count), Current, Code))
reduce_in_ggaa(.(Letter, Others), Count, Letter, Code) → U6_ggaa(Letter, Others, Count, Code, reduce_in_ggaa(Others, Count, Letter, Code))
reduce_in_ggaa(.(Current, Others), Count, X5, .(Current, Code)) → U7_ggaa(Current, Others, Count, X5, Code, reduce_in_ggaa(Others, s(Count), Current, Code))
U7_ggaa(Current, Others, Count, X5, Code, reduce_out_ggaa(Others, s(Count), Current, Code)) → reduce_out_ggaa(.(Current, Others), Count, X5, .(Current, Code))
U6_ggaa(Letter, Others, Count, Code, reduce_out_ggaa(Others, Count, Letter, Code)) → reduce_out_ggaa(.(Letter, Others), Count, Letter, Code)
U7_ggga(Current, Others, Count, X5, Code, reduce_out_ggaa(Others, s(Count), Current, Code)) → reduce_out_ggga(.(Current, Others), Count, X5, .(Current, Code))
U6_ggga(Letter, Others, Count, Code, reduce_out_ggga(Others, Count, Letter, Code)) → reduce_out_ggga(.(Letter, Others), Count, Letter, Code)
U5_ggga(Current, Others, Count, Code, reduce_out_ggga(Others, Count, Current, Code)) → reduce_out_ggga(.(Current, Others), Count, Current, Code)
U5_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
reduce_out_ggaa(x1, x2, x3, x4)  =  reduce_out_ggaa(x1, x2, x4)
[]  =  []
U4_ggaa(x1, x2, x3, x4, x5)  =  U4_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)
U5_ggaa(x1, x2, x3, x4, x5)  =  U5_ggaa(x2, x3, x5)
reduce_in_ggga(x1, x2, x3, x4)  =  reduce_in_ggga(x1, x2, x3)
reduce_out_ggga(x1, x2, x3, x4)  =  reduce_out_ggga(x1, x2, x3, x4)
U4_ggga(x1, x2, x3, x4, x5)  =  U4_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
U5_ggga(x1, x2, x3, x4, x5)  =  U5_ggga(x1, x2, x3, x5)
U6_ggga(x1, x2, x3, x4, x5)  =  U6_ggga(x1, x2, x3, x5)
U7_ggga(x1, x2, x3, x4, x5, x6)  =  U7_ggga(x2, x3, x4, x6)
U6_ggaa(x1, x2, x3, x4, x5)  =  U6_ggaa(x2, x3, x5)
U7_ggaa(x1, x2, x3, x4, x5, x6)  =  U7_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, x4, x5)  =  U4_GGAA(x2, x3, x5)
VOWEL_H_W_Y_IN_A(x1)  =  VOWEL_H_W_Y_IN_A
U5_GGAA(x1, x2, x3, x4, x5)  =  U5_GGAA(x2, x3, x5)
REDUCE_IN_GGGA(x1, x2, x3, x4)  =  REDUCE_IN_GGGA(x1, x2, x3)
U4_GGGA(x1, x2, x3, x4, x5)  =  U4_GGGA(x1, x2, x3, x5)
VOWEL_H_W_Y_IN_G(x1)  =  VOWEL_H_W_Y_IN_G(x1)
U5_GGGA(x1, x2, x3, x4, x5)  =  U5_GGGA(x1, x2, x3, x5)
U6_GGGA(x1, x2, x3, x4, x5)  =  U6_GGGA(x1, x2, x3, x5)
U7_GGGA(x1, x2, x3, x4, x5, x6)  =  U7_GGGA(x2, x3, x4, x6)
U6_GGAA(x1, x2, x3, x4, x5)  =  U6_GGAA(x2, x3, x5)
U7_GGAA(x1, x2, x3, x4, x5, x6)  =  U7_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

(6) 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(.(Current, Others), Count, Current, Code) → U4_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)
U4_GGAA(Current, Others, Count, Code, vowel_h_w_y_out_a(Current)) → U5_GGAA(Current, Others, Count, Code, reduce_in_ggga(Others, Count, Current, Code))
U4_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) → U4_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)
U4_GGGA(Current, Others, Count, Code, vowel_h_w_y_out_g(Current)) → U5_GGGA(Current, Others, Count, Code, reduce_in_ggga(Others, Count, Current, Code))
U4_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) → U6_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)) → U7_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) → U6_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)) → U7_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, []) → reduce_out_ggaa(X1, s(s(s(s(0)))), X2, [])
reduce_in_ggaa([], X3, X4, []) → reduce_out_ggaa([], X3, X4, [])
reduce_in_ggaa(.(Current, Others), Count, Current, Code) → U4_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)
U4_ggaa(Current, Others, Count, Code, vowel_h_w_y_out_a(Current)) → U5_ggaa(Current, Others, Count, Code, reduce_in_ggga(Others, Count, Current, Code))
reduce_in_ggga(X1, s(s(s(s(0)))), X2, []) → reduce_out_ggga(X1, s(s(s(s(0)))), X2, [])
reduce_in_ggga([], X3, X4, []) → reduce_out_ggga([], X3, X4, [])
reduce_in_ggga(.(Current, Others), Count, Current, Code) → U4_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)
U4_ggga(Current, Others, Count, Code, vowel_h_w_y_out_g(Current)) → U5_ggga(Current, Others, Count, Code, reduce_in_ggga(Others, Count, Current, Code))
reduce_in_ggga(.(Letter, Others), Count, Letter, Code) → U6_ggga(Letter, Others, Count, Code, reduce_in_ggga(Others, Count, Letter, Code))
reduce_in_ggga(.(Current, Others), Count, X5, .(Current, Code)) → U7_ggga(Current, Others, Count, X5, Code, reduce_in_ggaa(Others, s(Count), Current, Code))
reduce_in_ggaa(.(Letter, Others), Count, Letter, Code) → U6_ggaa(Letter, Others, Count, Code, reduce_in_ggaa(Others, Count, Letter, Code))
reduce_in_ggaa(.(Current, Others), Count, X5, .(Current, Code)) → U7_ggaa(Current, Others, Count, X5, Code, reduce_in_ggaa(Others, s(Count), Current, Code))
U7_ggaa(Current, Others, Count, X5, Code, reduce_out_ggaa(Others, s(Count), Current, Code)) → reduce_out_ggaa(.(Current, Others), Count, X5, .(Current, Code))
U6_ggaa(Letter, Others, Count, Code, reduce_out_ggaa(Others, Count, Letter, Code)) → reduce_out_ggaa(.(Letter, Others), Count, Letter, Code)
U7_ggga(Current, Others, Count, X5, Code, reduce_out_ggaa(Others, s(Count), Current, Code)) → reduce_out_ggga(.(Current, Others), Count, X5, .(Current, Code))
U6_ggga(Letter, Others, Count, Code, reduce_out_ggga(Others, Count, Letter, Code)) → reduce_out_ggga(.(Letter, Others), Count, Letter, Code)
U5_ggga(Current, Others, Count, Code, reduce_out_ggga(Others, Count, Current, Code)) → reduce_out_ggga(.(Current, Others), Count, Current, Code)
U5_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
reduce_out_ggaa(x1, x2, x3, x4)  =  reduce_out_ggaa(x1, x2, x4)
[]  =  []
U4_ggaa(x1, x2, x3, x4, x5)  =  U4_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)
U5_ggaa(x1, x2, x3, x4, x5)  =  U5_ggaa(x2, x3, x5)
reduce_in_ggga(x1, x2, x3, x4)  =  reduce_in_ggga(x1, x2, x3)
reduce_out_ggga(x1, x2, x3, x4)  =  reduce_out_ggga(x1, x2, x3, x4)
U4_ggga(x1, x2, x3, x4, x5)  =  U4_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
U5_ggga(x1, x2, x3, x4, x5)  =  U5_ggga(x1, x2, x3, x5)
U6_ggga(x1, x2, x3, x4, x5)  =  U6_ggga(x1, x2, x3, x5)
U7_ggga(x1, x2, x3, x4, x5, x6)  =  U7_ggga(x2, x3, x4, x6)
U6_ggaa(x1, x2, x3, x4, x5)  =  U6_ggaa(x2, x3, x5)
U7_ggaa(x1, x2, x3, x4, x5, x6)  =  U7_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, x4, x5)  =  U4_GGAA(x2, x3, x5)
VOWEL_H_W_Y_IN_A(x1)  =  VOWEL_H_W_Y_IN_A
U5_GGAA(x1, x2, x3, x4, x5)  =  U5_GGAA(x2, x3, x5)
REDUCE_IN_GGGA(x1, x2, x3, x4)  =  REDUCE_IN_GGGA(x1, x2, x3)
U4_GGGA(x1, x2, x3, x4, x5)  =  U4_GGGA(x1, x2, x3, x5)
VOWEL_H_W_Y_IN_G(x1)  =  VOWEL_H_W_Y_IN_G(x1)
U5_GGGA(x1, x2, x3, x4, x5)  =  U5_GGGA(x1, x2, x3, x5)
U6_GGGA(x1, x2, x3, x4, x5)  =  U6_GGGA(x1, x2, x3, x5)
U7_GGGA(x1, x2, x3, x4, x5, x6)  =  U7_GGGA(x2, x3, x4, x6)
U6_GGAA(x1, x2, x3, x4, x5)  =  U6_GGAA(x2, x3, x5)
U7_GGAA(x1, x2, x3, x4, x5, x6)  =  U7_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

(7) DependencyGraphProof (EQUIVALENT transformation)

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

(8) Obligation:

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

U4_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) → U4_GGGA(Current, Others, Count, Code, vowel_h_w_y_in_g(Current))
U4_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(.(Current, Others), Count, Current, Code) → U4_GGAA(Current, Others, Count, Code, vowel_h_w_y_in_a(Current))
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, []) → reduce_out_ggaa(X1, s(s(s(s(0)))), X2, [])
reduce_in_ggaa([], X3, X4, []) → reduce_out_ggaa([], X3, X4, [])
reduce_in_ggaa(.(Current, Others), Count, Current, Code) → U4_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)
U4_ggaa(Current, Others, Count, Code, vowel_h_w_y_out_a(Current)) → U5_ggaa(Current, Others, Count, Code, reduce_in_ggga(Others, Count, Current, Code))
reduce_in_ggga(X1, s(s(s(s(0)))), X2, []) → reduce_out_ggga(X1, s(s(s(s(0)))), X2, [])
reduce_in_ggga([], X3, X4, []) → reduce_out_ggga([], X3, X4, [])
reduce_in_ggga(.(Current, Others), Count, Current, Code) → U4_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)
U4_ggga(Current, Others, Count, Code, vowel_h_w_y_out_g(Current)) → U5_ggga(Current, Others, Count, Code, reduce_in_ggga(Others, Count, Current, Code))
reduce_in_ggga(.(Letter, Others), Count, Letter, Code) → U6_ggga(Letter, Others, Count, Code, reduce_in_ggga(Others, Count, Letter, Code))
reduce_in_ggga(.(Current, Others), Count, X5, .(Current, Code)) → U7_ggga(Current, Others, Count, X5, Code, reduce_in_ggaa(Others, s(Count), Current, Code))
reduce_in_ggaa(.(Letter, Others), Count, Letter, Code) → U6_ggaa(Letter, Others, Count, Code, reduce_in_ggaa(Others, Count, Letter, Code))
reduce_in_ggaa(.(Current, Others), Count, X5, .(Current, Code)) → U7_ggaa(Current, Others, Count, X5, Code, reduce_in_ggaa(Others, s(Count), Current, Code))
U7_ggaa(Current, Others, Count, X5, Code, reduce_out_ggaa(Others, s(Count), Current, Code)) → reduce_out_ggaa(.(Current, Others), Count, X5, .(Current, Code))
U6_ggaa(Letter, Others, Count, Code, reduce_out_ggaa(Others, Count, Letter, Code)) → reduce_out_ggaa(.(Letter, Others), Count, Letter, Code)
U7_ggga(Current, Others, Count, X5, Code, reduce_out_ggaa(Others, s(Count), Current, Code)) → reduce_out_ggga(.(Current, Others), Count, X5, .(Current, Code))
U6_ggga(Letter, Others, Count, Code, reduce_out_ggga(Others, Count, Letter, Code)) → reduce_out_ggga(.(Letter, Others), Count, Letter, Code)
U5_ggga(Current, Others, Count, Code, reduce_out_ggga(Others, Count, Current, Code)) → reduce_out_ggga(.(Current, Others), Count, Current, Code)
U5_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
reduce_out_ggaa(x1, x2, x3, x4)  =  reduce_out_ggaa(x1, x2, x4)
[]  =  []
U4_ggaa(x1, x2, x3, x4, x5)  =  U4_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)
U5_ggaa(x1, x2, x3, x4, x5)  =  U5_ggaa(x2, x3, x5)
reduce_in_ggga(x1, x2, x3, x4)  =  reduce_in_ggga(x1, x2, x3)
reduce_out_ggga(x1, x2, x3, x4)  =  reduce_out_ggga(x1, x2, x3, x4)
U4_ggga(x1, x2, x3, x4, x5)  =  U4_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
U5_ggga(x1, x2, x3, x4, x5)  =  U5_ggga(x1, x2, x3, x5)
U6_ggga(x1, x2, x3, x4, x5)  =  U6_ggga(x1, x2, x3, x5)
U7_ggga(x1, x2, x3, x4, x5, x6)  =  U7_ggga(x2, x3, x4, x6)
U6_ggaa(x1, x2, x3, x4, x5)  =  U6_ggaa(x2, x3, x5)
U7_ggaa(x1, x2, x3, x4, x5, x6)  =  U7_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)
U4_GGAA(x1, x2, x3, x4, x5)  =  U4_GGAA(x2, x3, x5)
REDUCE_IN_GGGA(x1, x2, x3, x4)  =  REDUCE_IN_GGGA(x1, x2, x3)
U4_GGGA(x1, x2, x3, x4, x5)  =  U4_GGGA(x1, x2, x3, x5)

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

(9) UsableRulesProof (EQUIVALENT transformation)

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

(10) Obligation:

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

U4_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) → U4_GGGA(Current, Others, Count, Code, vowel_h_w_y_in_g(Current))
U4_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(.(Current, Others), Count, Current, Code) → U4_GGAA(Current, Others, Count, Code, vowel_h_w_y_in_a(Current))
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_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)
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)

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)
U4_GGAA(x1, x2, x3, x4, x5)  =  U4_GGAA(x2, x3, x5)
REDUCE_IN_GGGA(x1, x2, x3, x4)  =  REDUCE_IN_GGGA(x1, x2, x3)
U4_GGGA(x1, x2, x3, x4, x5)  =  U4_GGGA(x1, x2, x3, x5)

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

(11) PiDPToQDPProof (SOUND transformation)

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

(12) Obligation:

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

U4_GGAA(Others, Count, vowel_h_w_y_out_a(Current)) → REDUCE_IN_GGGA(Others, Count, Current)
REDUCE_IN_GGGA(.(Others), Count, Current) → U4_GGGA(Current, Others, Count, vowel_h_w_y_in_g(Current))
U4_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) → U4_GGAA(Others, Count, vowel_h_w_y_in_a)
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_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)
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)

The set Q consists of the following terms:

vowel_h_w_y_in_g(x0)
vowel_h_w_y_in_a

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

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

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

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

  • U4_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

  • U4_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, Current) → U4_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_GGGA(.(Others), Count, X5) → REDUCE_IN_GGAA(Others, s(Count))
    The graph contains the following edges 1 > 1

  • 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

(14) YES