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

(0) Obligation:

Clauses:

p(X, X).
p(f(X), g(Y)) :- ','(p(f(X), f(Z)), p(Z, g(W))).

Query: p(g,a)

(1) PrologToPiTRSViaGraphTransformerProof (SOUND transformation)

Transformed Prolog program to (Pi-)TRS.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
2 [label="A: p(T1, T2)\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
4 [label="4: p(T1, T2), SCOPE: 1, CLAUSE: 0 | p(T1, T2), SCOPE: 1, CLAUSE: 1\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
10 [label="10: true | p(T4, T2), SCOPE: 1, CLAUSE: 1\n\nT4 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
11 [label="11: p(T1, T2), SCOPE: 1, CLAUSE: 1\n\nT1 is ground\nX2 is free\np(T1, T2) !=? p(X2, X2)", fontsize=16, style=filled, fillcolor=lightyellow];
12 [label="12: p(T4, T2), SCOPE: 1, CLAUSE: 1\n\nT4 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
27 [label="B: ','(p(f(T7), f(X7)), p(X7, g(X8)))\n\nT7 is ground\nX7 is free\nX8 is free", fontsize=16, style=filled, fillcolor=lightyellow];
28 [label="28: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
31 [label="31: ','(p(f(T7), f(X7)), p(X7, g(X8))), SCOPE: 2, CLAUSE: 0 | ','(p(f(T7), f(X7)), p(X7, g(X8))), SCOPE: 2, CLAUSE: 1\n\nT7 is ground\nX7 is free\nX8 is free", fontsize=16, style=filled, fillcolor=lightyellow];
38 [label="38: ','(p(f(T7), f(X7)), p(X7, g(X8))), SCOPE: 2, CLAUSE: 0\n\nT7 is ground\nX7 is free\nX8 is free", fontsize=16, style=filled, fillcolor=lightyellow];
39 [label="39: ','(p(f(T7), f(X7)), p(X7, g(X8))), SCOPE: 2, CLAUSE: 1\n\nT7 is ground\nX7 is free\nX8 is free", fontsize=16, style=filled, fillcolor=lightyellow];
45 [label="C: p(T21, g(X8))\n\nT21 is ground\nX8 is free", fontsize=16, style=filled, fillcolor=lightyellow];
48 [label="48: p(T21, g(X8)), SCOPE: 3, CLAUSE: 0 | p(T21, g(X8)), SCOPE: 3, CLAUSE: 1\n\nT21 is ground\nX8 is free", fontsize=16, style=filled, fillcolor=lightyellow];
49 [label="49: p(T21, g(X8)), SCOPE: 3, CLAUSE: 0\n\nT21 is ground\nX8 is free", fontsize=16, style=filled, fillcolor=lightyellow];
50 [label="50: p(T21, g(X8)), SCOPE: 3, CLAUSE: 1\n\nT21 is ground\nX8 is free", fontsize=16, style=filled, fillcolor=lightyellow];
55 [label="55: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
56 [label="56: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
57 [label="57: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
64 [label="64: ','(p(f(T38), f(X35)), p(X35, g(X36)))\n\nT38 is ground\nX35 is free\nX36 is free", fontsize=16, style=filled, fillcolor=lightyellow];
65 [label="65: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
70 [label="70: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
73 [label="73: ','(p(f(T43), f(X48)), p(X48, g(X49)))\n\nT43 is ground\nX2 is free\nX48 is free\nX49 is free\np(f(T43), T2) !=? p(X2, X2)", fontsize=16, style=filled, fillcolor=lightyellow];
74 [label="74: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
76 [label="76: ','(p(f(T43), f(X48)), p(X48, g(X49))), SCOPE: 4, CLAUSE: 0 | ','(p(f(T43), f(X48)), p(X48, g(X49))), SCOPE: 4, CLAUSE: 1\n\nT43 is ground\nX2 is free\nX48 is free\nX49 is free\np(f(T43), T2) !=? p(X2, X2)", fontsize=16, style=filled, fillcolor=lightyellow];
80 [label="80: ','(p(f(T43), f(X48)), p(X48, g(X49))), SCOPE: 4, CLAUSE: 0\n\nT43 is ground\nX2 is free\nX48 is free\nX49 is free\np(f(T43), T2) !=? p(X2, X2)", fontsize=16, style=filled, fillcolor=lightyellow];
82 [label="82: ','(p(f(T43), f(X48)), p(X48, g(X49))), SCOPE: 4, CLAUSE: 1\n\nT43 is ground\nX2 is free\nX48 is free\nX49 is free\np(f(T43), T2) !=? p(X2, X2)", fontsize=16, style=filled, fillcolor=lightyellow];
86 [label="86: p(T57, g(X49))\n\nT57 is ground\nX2 is free\nX49 is free\np(f(T57), T2) !=? p(X2, X2)", fontsize=16, style=filled, fillcolor=lightyellow];
87 [label="87: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
88 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
2 -> 88 [arrowhead = none ];
88 -> 4;

89 [label="EVAL with clause\np(X2, X2).\nand substitutionT1 -> T4,\nX2 -> T4,\nT2 -> T4", fontsize=14, style = filled, fillcolor = lightblue];
4 -> 89 [arrowhead = none ];
89 -> 10;

90 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
4 -> 90 [arrowhead = none ];
90 -> 11;

91 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
10 -> 91 [arrowhead = none ];
91 -> 12;

92 [label="EVAL with clause\np(f(X46), g(X47)) :- ','(p(f(X46), f(X48)), p(X48, g(X49))).\nand substitutionX46 -> T43,\nT1 -> f(T43),\nX47 -> T44,\nT2 -> g(T44)", fontsize=14, style = filled, fillcolor = lightblue];
11 -> 92 [arrowhead = none ];
92 -> 73;

93 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
11 -> 93 [arrowhead = none ];
93 -> 74;

94 [label="EVAL with clause\np(f(X5), g(X6)) :- ','(p(f(X5), f(X7)), p(X7, g(X8))).\nand substitutionX5 -> T7,\nT4 -> f(T7),\nX6 -> T8,\nT2 -> g(T8)", fontsize=14, style = filled, fillcolor = lightblue];
12 -> 94 [arrowhead = none ];
94 -> 27;

95 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
12 -> 95 [arrowhead = none ];
95 -> 28;

96 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
27 -> 96 [arrowhead = none ];
96 -> 31;

97 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
31 -> 97 [arrowhead = none ];
97 -> 38;

98 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
31 -> 98 [arrowhead = none ];
98 -> 39;

99 [label="ONLY EVAL with clause\np(X17, X17).\nand substitutionT7 -> T21,\nX17 -> f(T21),\nX7 -> T21", fontsize=14, style = filled, fillcolor = lightblue];
38 -> 99 [arrowhead = none ];
99 -> 45;

100 [label="BACKTRACK\nfor clause: p(f(X), g(Y)) :- ','(p(f(X), f(Z)), p(Z, g(W)))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
39 -> 100 [arrowhead = none ];
100 -> 70;

101 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
45 -> 101 [arrowhead = none ];
101 -> 48;

102 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
48 -> 102 [arrowhead = none ];
102 -> 49;

103 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
48 -> 103 [arrowhead = none ];
103 -> 50;

104 [label="EVAL with clause\np(X24, X24).\nand substitutionT21 -> g(T35),\nX24 -> g(T35),\nX8 -> T35,\nT34 -> g(T35)", fontsize=14, style = filled, fillcolor = lightblue];
49 -> 104 [arrowhead = none ];
104 -> 55;

105 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
49 -> 105 [arrowhead = none ];
105 -> 56;

106 [label="EVAL with clause\np(f(X33), g(X34)) :- ','(p(f(X33), f(X35)), p(X35, g(X36))).\nand substitutionX33 -> T38,\nT21 -> f(T38),\nX8 -> X37,\nX34 -> X37", fontsize=14, style = filled, fillcolor = lightblue];
50 -> 106 [arrowhead = none ];
106 -> 64;

107 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
50 -> 107 [arrowhead = none ];
107 -> 65;

108 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
55 -> 108 [arrowhead = none ];
108 -> 57;

109 [label="INSTANCE with matching:\nT7 -> T38\nX7 -> X35\nX8 -> X36", fontsize=14, style = filled, fillcolor = lightgrey];
64 -> 109 [arrowhead = none , style=dashed];
109 -> 27[style=dashed];

110 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
73 -> 110 [arrowhead = none ];
110 -> 76;

111 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
76 -> 111 [arrowhead = none ];
111 -> 80;

112 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
76 -> 112 [arrowhead = none ];
112 -> 82;

113 [label="ONLY EVAL with clause\np(X58, X58).\nand substitutionT43 -> T57,\nX58 -> f(T57),\nX48 -> T57", fontsize=14, style = filled, fillcolor = lightblue];
80 -> 113 [arrowhead = none ];
113 -> 86;

114 [label="BACKTRACK\nfor clause: p(f(X), g(Y)) :- ','(p(f(X), f(Z)), p(Z, g(W)))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
82 -> 114 [arrowhead = none ];
114 -> 87;

115 [label="INSTANCE with matching:\nT21 -> T57\nX8 -> X49", fontsize=14, style = filled, fillcolor = lightgrey];
86 -> 115 [arrowhead = none , style=dashed];
115 -> 45[style=dashed];

}

(2) Obligation:

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

pA_in_ga(T4, T4) → pA_out_ga(T4, T4)
pA_in_ga(f(T7), g(T8)) → U1_ga(T7, T8, pB_in_gaa(T7, X7, X8))
pB_in_gaa(T21, T21, X8) → U3_gaa(T21, X8, pC_in_ga(T21, X8))
pC_in_ga(g(T35), T35) → pC_out_ga(g(T35), T35)
pC_in_ga(f(T38), X37) → U4_ga(T38, X37, pB_in_gaa(T38, X35, X36))
U4_ga(T38, X37, pB_out_gaa(T38, X35, X36)) → pC_out_ga(f(T38), X37)
U3_gaa(T21, X8, pC_out_ga(T21, X8)) → pB_out_gaa(T21, T21, X8)
U1_ga(T7, T8, pB_out_gaa(T7, X7, X8)) → pA_out_ga(f(T7), g(T8))
pA_in_ga(f(T57), g(T44)) → U2_ga(T57, T44, pC_in_ga(T57, X49))
U2_ga(T57, T44, pC_out_ga(T57, X49)) → pA_out_ga(f(T57), g(T44))

The argument filtering Pi contains the following mapping:
pA_in_ga(x1, x2)  =  pA_in_ga(x1)
pA_out_ga(x1, x2)  =  pA_out_ga(x1, x2)
f(x1)  =  f(x1)
U1_ga(x1, x2, x3)  =  U1_ga(x1, x3)
pB_in_gaa(x1, x2, x3)  =  pB_in_gaa(x1)
U3_gaa(x1, x2, x3)  =  U3_gaa(x1, x3)
pC_in_ga(x1, x2)  =  pC_in_ga(x1)
g(x1)  =  g
pC_out_ga(x1, x2)  =  pC_out_ga(x1)
U4_ga(x1, x2, x3)  =  U4_ga(x1, x3)
pB_out_gaa(x1, x2, x3)  =  pB_out_gaa(x1, x2)
U2_ga(x1, x2, x3)  =  U2_ga(x1, x3)

(3) DependencyPairsProof (EQUIVALENT transformation)

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

PA_IN_GA(f(T7), g(T8)) → U1_GA(T7, T8, pB_in_gaa(T7, X7, X8))
PA_IN_GA(f(T7), g(T8)) → PB_IN_GAA(T7, X7, X8)
PB_IN_GAA(T21, T21, X8) → U3_GAA(T21, X8, pC_in_ga(T21, X8))
PB_IN_GAA(T21, T21, X8) → PC_IN_GA(T21, X8)
PC_IN_GA(f(T38), X37) → U4_GA(T38, X37, pB_in_gaa(T38, X35, X36))
PC_IN_GA(f(T38), X37) → PB_IN_GAA(T38, X35, X36)
PA_IN_GA(f(T57), g(T44)) → U2_GA(T57, T44, pC_in_ga(T57, X49))
PA_IN_GA(f(T57), g(T44)) → PC_IN_GA(T57, X49)

The TRS R consists of the following rules:

pA_in_ga(T4, T4) → pA_out_ga(T4, T4)
pA_in_ga(f(T7), g(T8)) → U1_ga(T7, T8, pB_in_gaa(T7, X7, X8))
pB_in_gaa(T21, T21, X8) → U3_gaa(T21, X8, pC_in_ga(T21, X8))
pC_in_ga(g(T35), T35) → pC_out_ga(g(T35), T35)
pC_in_ga(f(T38), X37) → U4_ga(T38, X37, pB_in_gaa(T38, X35, X36))
U4_ga(T38, X37, pB_out_gaa(T38, X35, X36)) → pC_out_ga(f(T38), X37)
U3_gaa(T21, X8, pC_out_ga(T21, X8)) → pB_out_gaa(T21, T21, X8)
U1_ga(T7, T8, pB_out_gaa(T7, X7, X8)) → pA_out_ga(f(T7), g(T8))
pA_in_ga(f(T57), g(T44)) → U2_ga(T57, T44, pC_in_ga(T57, X49))
U2_ga(T57, T44, pC_out_ga(T57, X49)) → pA_out_ga(f(T57), g(T44))

The argument filtering Pi contains the following mapping:
pA_in_ga(x1, x2)  =  pA_in_ga(x1)
pA_out_ga(x1, x2)  =  pA_out_ga(x1, x2)
f(x1)  =  f(x1)
U1_ga(x1, x2, x3)  =  U1_ga(x1, x3)
pB_in_gaa(x1, x2, x3)  =  pB_in_gaa(x1)
U3_gaa(x1, x2, x3)  =  U3_gaa(x1, x3)
pC_in_ga(x1, x2)  =  pC_in_ga(x1)
g(x1)  =  g
pC_out_ga(x1, x2)  =  pC_out_ga(x1)
U4_ga(x1, x2, x3)  =  U4_ga(x1, x3)
pB_out_gaa(x1, x2, x3)  =  pB_out_gaa(x1, x2)
U2_ga(x1, x2, x3)  =  U2_ga(x1, x3)
PA_IN_GA(x1, x2)  =  PA_IN_GA(x1)
U1_GA(x1, x2, x3)  =  U1_GA(x1, x3)
PB_IN_GAA(x1, x2, x3)  =  PB_IN_GAA(x1)
U3_GAA(x1, x2, x3)  =  U3_GAA(x1, x3)
PC_IN_GA(x1, x2)  =  PC_IN_GA(x1)
U4_GA(x1, x2, x3)  =  U4_GA(x1, x3)
U2_GA(x1, x2, x3)  =  U2_GA(x1, x3)

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

(4) Obligation:

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

PA_IN_GA(f(T7), g(T8)) → U1_GA(T7, T8, pB_in_gaa(T7, X7, X8))
PA_IN_GA(f(T7), g(T8)) → PB_IN_GAA(T7, X7, X8)
PB_IN_GAA(T21, T21, X8) → U3_GAA(T21, X8, pC_in_ga(T21, X8))
PB_IN_GAA(T21, T21, X8) → PC_IN_GA(T21, X8)
PC_IN_GA(f(T38), X37) → U4_GA(T38, X37, pB_in_gaa(T38, X35, X36))
PC_IN_GA(f(T38), X37) → PB_IN_GAA(T38, X35, X36)
PA_IN_GA(f(T57), g(T44)) → U2_GA(T57, T44, pC_in_ga(T57, X49))
PA_IN_GA(f(T57), g(T44)) → PC_IN_GA(T57, X49)

The TRS R consists of the following rules:

pA_in_ga(T4, T4) → pA_out_ga(T4, T4)
pA_in_ga(f(T7), g(T8)) → U1_ga(T7, T8, pB_in_gaa(T7, X7, X8))
pB_in_gaa(T21, T21, X8) → U3_gaa(T21, X8, pC_in_ga(T21, X8))
pC_in_ga(g(T35), T35) → pC_out_ga(g(T35), T35)
pC_in_ga(f(T38), X37) → U4_ga(T38, X37, pB_in_gaa(T38, X35, X36))
U4_ga(T38, X37, pB_out_gaa(T38, X35, X36)) → pC_out_ga(f(T38), X37)
U3_gaa(T21, X8, pC_out_ga(T21, X8)) → pB_out_gaa(T21, T21, X8)
U1_ga(T7, T8, pB_out_gaa(T7, X7, X8)) → pA_out_ga(f(T7), g(T8))
pA_in_ga(f(T57), g(T44)) → U2_ga(T57, T44, pC_in_ga(T57, X49))
U2_ga(T57, T44, pC_out_ga(T57, X49)) → pA_out_ga(f(T57), g(T44))

The argument filtering Pi contains the following mapping:
pA_in_ga(x1, x2)  =  pA_in_ga(x1)
pA_out_ga(x1, x2)  =  pA_out_ga(x1, x2)
f(x1)  =  f(x1)
U1_ga(x1, x2, x3)  =  U1_ga(x1, x3)
pB_in_gaa(x1, x2, x3)  =  pB_in_gaa(x1)
U3_gaa(x1, x2, x3)  =  U3_gaa(x1, x3)
pC_in_ga(x1, x2)  =  pC_in_ga(x1)
g(x1)  =  g
pC_out_ga(x1, x2)  =  pC_out_ga(x1)
U4_ga(x1, x2, x3)  =  U4_ga(x1, x3)
pB_out_gaa(x1, x2, x3)  =  pB_out_gaa(x1, x2)
U2_ga(x1, x2, x3)  =  U2_ga(x1, x3)
PA_IN_GA(x1, x2)  =  PA_IN_GA(x1)
U1_GA(x1, x2, x3)  =  U1_GA(x1, x3)
PB_IN_GAA(x1, x2, x3)  =  PB_IN_GAA(x1)
U3_GAA(x1, x2, x3)  =  U3_GAA(x1, x3)
PC_IN_GA(x1, x2)  =  PC_IN_GA(x1)
U4_GA(x1, x2, x3)  =  U4_GA(x1, x3)
U2_GA(x1, x2, x3)  =  U2_GA(x1, x3)

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

(5) DependencyGraphProof (EQUIVALENT transformation)

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

(6) Obligation:

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

PB_IN_GAA(T21, T21, X8) → PC_IN_GA(T21, X8)
PC_IN_GA(f(T38), X37) → PB_IN_GAA(T38, X35, X36)

The TRS R consists of the following rules:

pA_in_ga(T4, T4) → pA_out_ga(T4, T4)
pA_in_ga(f(T7), g(T8)) → U1_ga(T7, T8, pB_in_gaa(T7, X7, X8))
pB_in_gaa(T21, T21, X8) → U3_gaa(T21, X8, pC_in_ga(T21, X8))
pC_in_ga(g(T35), T35) → pC_out_ga(g(T35), T35)
pC_in_ga(f(T38), X37) → U4_ga(T38, X37, pB_in_gaa(T38, X35, X36))
U4_ga(T38, X37, pB_out_gaa(T38, X35, X36)) → pC_out_ga(f(T38), X37)
U3_gaa(T21, X8, pC_out_ga(T21, X8)) → pB_out_gaa(T21, T21, X8)
U1_ga(T7, T8, pB_out_gaa(T7, X7, X8)) → pA_out_ga(f(T7), g(T8))
pA_in_ga(f(T57), g(T44)) → U2_ga(T57, T44, pC_in_ga(T57, X49))
U2_ga(T57, T44, pC_out_ga(T57, X49)) → pA_out_ga(f(T57), g(T44))

The argument filtering Pi contains the following mapping:
pA_in_ga(x1, x2)  =  pA_in_ga(x1)
pA_out_ga(x1, x2)  =  pA_out_ga(x1, x2)
f(x1)  =  f(x1)
U1_ga(x1, x2, x3)  =  U1_ga(x1, x3)
pB_in_gaa(x1, x2, x3)  =  pB_in_gaa(x1)
U3_gaa(x1, x2, x3)  =  U3_gaa(x1, x3)
pC_in_ga(x1, x2)  =  pC_in_ga(x1)
g(x1)  =  g
pC_out_ga(x1, x2)  =  pC_out_ga(x1)
U4_ga(x1, x2, x3)  =  U4_ga(x1, x3)
pB_out_gaa(x1, x2, x3)  =  pB_out_gaa(x1, x2)
U2_ga(x1, x2, x3)  =  U2_ga(x1, x3)
PB_IN_GAA(x1, x2, x3)  =  PB_IN_GAA(x1)
PC_IN_GA(x1, x2)  =  PC_IN_GA(x1)

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

(7) UsableRulesProof (EQUIVALENT transformation)

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

(8) Obligation:

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

PB_IN_GAA(T21, T21, X8) → PC_IN_GA(T21, X8)
PC_IN_GA(f(T38), X37) → PB_IN_GAA(T38, X35, X36)

R is empty.
The argument filtering Pi contains the following mapping:
f(x1)  =  f(x1)
PB_IN_GAA(x1, x2, x3)  =  PB_IN_GAA(x1)
PC_IN_GA(x1, x2)  =  PC_IN_GA(x1)

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

(9) PiDPToQDPProof (SOUND transformation)

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

(10) Obligation:

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

PB_IN_GAA(T21) → PC_IN_GA(T21)
PC_IN_GA(f(T38)) → PB_IN_GAA(T38)

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

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

• PC_IN_GA(f(T38)) → PB_IN_GAA(T38)
  The graph contains the following edges 1 > 1

• PB_IN_GAA(T21) → PC_IN_GA(T21)
  The graph contains the following edges 1 >= 1

(12) YES