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

(0) Obligation:

Clauses:

normal(F, N) :- ','(rewrite(F, F1), normal(F1, N)).
normal(F, F).
rewrite(op(op(A, B), C), op(A, op(B, C))).
rewrite(op(A, op(B, C)), op(A, L)) :- rewrite(op(B, C), L).

Query: normal(g,a)

(1) PrologToPiTRSViaGraphTransformerProof (SOUND transformation)

Transformed Prolog program to (Pi-)TRS.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
1 [label="A: normal(T1, T2)\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
5 [label="5: normal(T1, T2), SCOPE: 1, CLAUSE: 0 | normal(T1, T2), SCOPE: 1, CLAUSE: 1\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
8 [label="8: ','(rewrite(T5, X5), normal(X5, T7)) | normal(T5, T2), SCOPE: 1, CLAUSE: 1\n\nT5 is ground\nX5 is free", fontsize=16, style=filled, fillcolor=lightyellow];
9 [label="9: ','(rewrite(T5, X5), normal(X5, T7)), SCOPE: 2, CLAUSE: 2 | ','(rewrite(T5, X5), normal(X5, T7)), SCOPE: 2, CLAUSE: 3 | ?_2 | normal(T5, T2), SCOPE: 1, CLAUSE: 1\n\nT5 is ground\nX5 is free", fontsize=16, style=filled, fillcolor=lightyellow];
13 [label="13: ','(rewrite(T5, X5), normal(X5, T7)), SCOPE: 2, CLAUSE: 2\n\nT5 is ground\nX5 is free", fontsize=16, style=filled, fillcolor=lightyellow];
15 [label="15: ','(rewrite(T5, X5), normal(X5, T7)), SCOPE: 2, CLAUSE: 3 | ?_2 | normal(T5, T2), SCOPE: 1, CLAUSE: 1\n\nT5 is ground\nX5 is free", fontsize=16, style=filled, fillcolor=lightyellow];
17 [label="17: normal(op(T20, op(T21, T22)), T7)\n\nT20 is ground\nT21 is ground\nT22 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
18 [label="18: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
25 [label="25: ','(rewrite(T5, X5), normal(X5, T7)), SCOPE: 2, CLAUSE: 3\n\nT5 is ground\nX5 is free", fontsize=16, style=filled, fillcolor=lightyellow];
26 [label="26: ?_2 | normal(T5, T2), SCOPE: 1, CLAUSE: 1\n\nT5 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
34 [label="B: ','(rewrite(op(T40, T41), X48), normal(op(T39, X48), T7))\n\nT39 is ground\nT40 is ground\nT41 is ground\nX48 is free", fontsize=16, style=filled, fillcolor=lightyellow];
35 [label="35: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
36 [label="C: rewrite(op(T40, T41), X48)\n\nT40 is ground\nT41 is ground\nX48 is free", fontsize=16, style=filled, fillcolor=lightyellow];
37 [label="37: normal(op(T39, T48), T7)\n\nT39 is ground\nT48 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
42 [label="42: rewrite(op(T40, T41), X48), SCOPE: 3, CLAUSE: 2 | rewrite(op(T40, T41), X48), SCOPE: 3, CLAUSE: 3\n\nT40 is ground\nT41 is ground\nX48 is free", fontsize=16, style=filled, fillcolor=lightyellow];
43 [label="43: rewrite(op(T40, T41), X48), SCOPE: 3, CLAUSE: 2\n\nT40 is ground\nT41 is ground\nX48 is free", fontsize=16, style=filled, fillcolor=lightyellow];
44 [label="44: rewrite(op(T40, T41), X48), SCOPE: 3, CLAUSE: 3\n\nT40 is ground\nT41 is ground\nX48 is free", fontsize=16, style=filled, fillcolor=lightyellow];
48 [label="48: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
49 [label="49: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
50 [label="50: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
53 [label="53: rewrite(op(T77, T78), X90)\n\nT77 is ground\nT78 is ground\nX90 is free", fontsize=16, style=filled, fillcolor=lightyellow];
54 [label="54: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
56 [label="56: normal(T5, T2), SCOPE: 1, CLAUSE: 1\n\nT5 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
57 [label="57: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
58 [label="58: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
59 [label="59: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
60 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
1 -> 60 [arrowhead = none ];
60 -> 5;

61 [label="ONLY EVAL with clause\nnormal(X3, X4) :- ','(rewrite(X3, X5), normal(X5, X4)).\nand substitutionT1 -> T5,\nX3 -> T5,\nT2 -> T7,\nX4 -> T7,\nT6 -> T7", fontsize=14, style = filled, fillcolor = lightblue];
5 -> 61 [arrowhead = none ];
61 -> 8;

62 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
8 -> 62 [arrowhead = none ];
62 -> 9;

63 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
9 -> 63 [arrowhead = none ];
63 -> 13;

64 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
9 -> 64 [arrowhead = none ];
64 -> 15;

65 [label="EVAL with clause\nrewrite(op(op(X18, X19), X20), op(X18, op(X19, X20))).\nand substitutionX18 -> T20,\nX19 -> T21,\nX20 -> T22,\nT5 -> op(op(T20, T21), T22),\nX5 -> op(T20, op(T21, T22))", fontsize=14, style = filled, fillcolor = lightblue];
13 -> 65 [arrowhead = none ];
65 -> 17;

66 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
13 -> 66 [arrowhead = none ];
66 -> 18;

67 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
15 -> 67 [arrowhead = none ];
67 -> 25;

68 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
15 -> 68 [arrowhead = none ];
68 -> 26;

69 [label="INSTANCE with matching:\nT1 -> op(T20, op(T21, T22))\nT2 -> T7", fontsize=14, style = filled, fillcolor = lightgrey];
17 -> 69 [arrowhead = none , style=dashed];
69 -> 1[style=dashed];

70 [label="EVAL with clause\nrewrite(op(X44, op(X45, X46)), op(X44, X47)) :- rewrite(op(X45, X46), X47).\nand substitutionX44 -> T39,\nX45 -> T40,\nX46 -> T41,\nT5 -> op(T39, op(T40, T41)),\nX47 -> X48,\nX5 -> op(T39, X48)", fontsize=14, style = filled, fillcolor = lightblue];
25 -> 70 [arrowhead = none ];
70 -> 34;

71 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
25 -> 71 [arrowhead = none ];
71 -> 35;

72 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
26 -> 72 [arrowhead = none ];
72 -> 56;

73 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
34 -> 73 [arrowhead = none ];
73 -> 36;

74 [label="SPLIT 2\nnew knowledge:\nT40 is ground\nT41 is ground\nT48 is ground\nreplacements:X48 -> T48", fontsize=14, style = filled, fillcolor = violet];
34 -> 74 [arrowhead = none ];
74 -> 37;

75 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
36 -> 75 [arrowhead = none ];
75 -> 42;

76 [label="INSTANCE with matching:\nT1 -> op(T39, T48)\nT2 -> T7", fontsize=14, style = filled, fillcolor = lightgrey];
37 -> 76 [arrowhead = none , style=dashed];
76 -> 1[style=dashed];

77 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
42 -> 77 [arrowhead = none ];
77 -> 43;

78 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
42 -> 78 [arrowhead = none ];
78 -> 44;

79 [label="EVAL with clause\nrewrite(op(op(X73, X74), X75), op(X73, op(X74, X75))).\nand substitutionX73 -> T67,\nX74 -> T68,\nT40 -> op(T67, T68),\nT41 -> T69,\nX75 -> T69,\nX48 -> op(T67, op(T68, T69))", fontsize=14, style = filled, fillcolor = lightblue];
43 -> 79 [arrowhead = none ];
79 -> 48;

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

81 [label="EVAL with clause\nrewrite(op(X86, op(X87, X88)), op(X86, X89)) :- rewrite(op(X87, X88), X89).\nand substitutionT40 -> T76,\nX86 -> T76,\nX87 -> T77,\nX88 -> T78,\nT41 -> op(T77, T78),\nX89 -> X90,\nX48 -> op(T76, X90)", fontsize=14, style = filled, fillcolor = lightblue];
44 -> 81 [arrowhead = none ];
81 -> 53;

82 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
44 -> 82 [arrowhead = none ];
82 -> 54;

83 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
48 -> 83 [arrowhead = none ];
83 -> 50;

84 [label="INSTANCE with matching:\nT40 -> T77\nT41 -> T78\nX48 -> X90", fontsize=14, style = filled, fillcolor = lightgrey];
53 -> 84 [arrowhead = none , style=dashed];
84 -> 36[style=dashed];

85 [label="EVAL with clause\nnormal(X102, X102).\nand substitutionT5 -> T90,\nX102 -> T90,\nT2 -> T90", fontsize=14, style = filled, fillcolor = lightblue];
56 -> 85 [arrowhead = none ];
85 -> 57;

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

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

}

(2) Obligation:

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

normalA_in_ga(op(op(T20, T21), T22), T7) → U1_ga(T20, T21, T22, T7, normalA_in_ga(op(T20, op(T21, T22)), T7))
normalA_in_ga(op(T39, op(T40, T41)), T7) → U2_ga(T39, T40, T41, T7, pB_in_ggaga(T40, T41, X48, T39, T7))
pB_in_ggaga(T40, T41, T48, T39, T7) → U4_ggaga(T40, T41, T48, T39, T7, rewriteC_in_gga(T40, T41, T48))
rewriteC_in_gga(op(T67, T68), T69, op(T67, op(T68, T69))) → rewriteC_out_gga(op(T67, T68), T69, op(T67, op(T68, T69)))
rewriteC_in_gga(T76, op(T77, T78), op(T76, X90)) → U3_gga(T76, T77, T78, X90, rewriteC_in_gga(T77, T78, X90))
U3_gga(T76, T77, T78, X90, rewriteC_out_gga(T77, T78, X90)) → rewriteC_out_gga(T76, op(T77, T78), op(T76, X90))
U4_ggaga(T40, T41, T48, T39, T7, rewriteC_out_gga(T40, T41, T48)) → U5_ggaga(T40, T41, T48, T39, T7, normalA_in_ga(op(T39, T48), T7))
normalA_in_ga(T90, T90) → normalA_out_ga(T90, T90)
U5_ggaga(T40, T41, T48, T39, T7, normalA_out_ga(op(T39, T48), T7)) → pB_out_ggaga(T40, T41, T48, T39, T7)
U2_ga(T39, T40, T41, T7, pB_out_ggaga(T40, T41, X48, T39, T7)) → normalA_out_ga(op(T39, op(T40, T41)), T7)
U1_ga(T20, T21, T22, T7, normalA_out_ga(op(T20, op(T21, T22)), T7)) → normalA_out_ga(op(op(T20, T21), T22), T7)

The argument filtering Pi contains the following mapping:
normalA_in_ga(x1, x2)  =  normalA_in_ga(x1)
op(x1, x2)  =  op(x1, x2)
U1_ga(x1, x2, x3, x4, x5)  =  U1_ga(x1, x2, x3, x5)
U2_ga(x1, x2, x3, x4, x5)  =  U2_ga(x1, x2, x3, x5)
pB_in_ggaga(x1, x2, x3, x4, x5)  =  pB_in_ggaga(x1, x2, x4)
U4_ggaga(x1, x2, x3, x4, x5, x6)  =  U4_ggaga(x1, x2, x4, x6)
rewriteC_in_gga(x1, x2, x3)  =  rewriteC_in_gga(x1, x2)
rewriteC_out_gga(x1, x2, x3)  =  rewriteC_out_gga(x1, x2, x3)
U3_gga(x1, x2, x3, x4, x5)  =  U3_gga(x1, x2, x3, x5)
U5_ggaga(x1, x2, x3, x4, x5, x6)  =  U5_ggaga(x1, x2, x3, x4, x6)
normalA_out_ga(x1, x2)  =  normalA_out_ga(x1, x2)
pB_out_ggaga(x1, x2, x3, x4, x5)  =  pB_out_ggaga(x1, x2, x3, x4, x5)

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

NORMALA_IN_GA(op(op(T20, T21), T22), T7) → U1_GA(T20, T21, T22, T7, normalA_in_ga(op(T20, op(T21, T22)), T7))
NORMALA_IN_GA(op(op(T20, T21), T22), T7) → NORMALA_IN_GA(op(T20, op(T21, T22)), T7)
NORMALA_IN_GA(op(T39, op(T40, T41)), T7) → U2_GA(T39, T40, T41, T7, pB_in_ggaga(T40, T41, X48, T39, T7))
NORMALA_IN_GA(op(T39, op(T40, T41)), T7) → PB_IN_GGAGA(T40, T41, X48, T39, T7)
PB_IN_GGAGA(T40, T41, T48, T39, T7) → U4_GGAGA(T40, T41, T48, T39, T7, rewriteC_in_gga(T40, T41, T48))
PB_IN_GGAGA(T40, T41, T48, T39, T7) → REWRITEC_IN_GGA(T40, T41, T48)
REWRITEC_IN_GGA(T76, op(T77, T78), op(T76, X90)) → U3_GGA(T76, T77, T78, X90, rewriteC_in_gga(T77, T78, X90))
REWRITEC_IN_GGA(T76, op(T77, T78), op(T76, X90)) → REWRITEC_IN_GGA(T77, T78, X90)
U4_GGAGA(T40, T41, T48, T39, T7, rewriteC_out_gga(T40, T41, T48)) → U5_GGAGA(T40, T41, T48, T39, T7, normalA_in_ga(op(T39, T48), T7))
U4_GGAGA(T40, T41, T48, T39, T7, rewriteC_out_gga(T40, T41, T48)) → NORMALA_IN_GA(op(T39, T48), T7)

The TRS R consists of the following rules:

normalA_in_ga(op(op(T20, T21), T22), T7) → U1_ga(T20, T21, T22, T7, normalA_in_ga(op(T20, op(T21, T22)), T7))
normalA_in_ga(op(T39, op(T40, T41)), T7) → U2_ga(T39, T40, T41, T7, pB_in_ggaga(T40, T41, X48, T39, T7))
pB_in_ggaga(T40, T41, T48, T39, T7) → U4_ggaga(T40, T41, T48, T39, T7, rewriteC_in_gga(T40, T41, T48))
rewriteC_in_gga(op(T67, T68), T69, op(T67, op(T68, T69))) → rewriteC_out_gga(op(T67, T68), T69, op(T67, op(T68, T69)))
rewriteC_in_gga(T76, op(T77, T78), op(T76, X90)) → U3_gga(T76, T77, T78, X90, rewriteC_in_gga(T77, T78, X90))
U3_gga(T76, T77, T78, X90, rewriteC_out_gga(T77, T78, X90)) → rewriteC_out_gga(T76, op(T77, T78), op(T76, X90))
U4_ggaga(T40, T41, T48, T39, T7, rewriteC_out_gga(T40, T41, T48)) → U5_ggaga(T40, T41, T48, T39, T7, normalA_in_ga(op(T39, T48), T7))
normalA_in_ga(T90, T90) → normalA_out_ga(T90, T90)
U5_ggaga(T40, T41, T48, T39, T7, normalA_out_ga(op(T39, T48), T7)) → pB_out_ggaga(T40, T41, T48, T39, T7)
U2_ga(T39, T40, T41, T7, pB_out_ggaga(T40, T41, X48, T39, T7)) → normalA_out_ga(op(T39, op(T40, T41)), T7)
U1_ga(T20, T21, T22, T7, normalA_out_ga(op(T20, op(T21, T22)), T7)) → normalA_out_ga(op(op(T20, T21), T22), T7)

The argument filtering Pi contains the following mapping:
normalA_in_ga(x1, x2)  =  normalA_in_ga(x1)
op(x1, x2)  =  op(x1, x2)
U1_ga(x1, x2, x3, x4, x5)  =  U1_ga(x1, x2, x3, x5)
U2_ga(x1, x2, x3, x4, x5)  =  U2_ga(x1, x2, x3, x5)
pB_in_ggaga(x1, x2, x3, x4, x5)  =  pB_in_ggaga(x1, x2, x4)
U4_ggaga(x1, x2, x3, x4, x5, x6)  =  U4_ggaga(x1, x2, x4, x6)
rewriteC_in_gga(x1, x2, x3)  =  rewriteC_in_gga(x1, x2)
rewriteC_out_gga(x1, x2, x3)  =  rewriteC_out_gga(x1, x2, x3)
U3_gga(x1, x2, x3, x4, x5)  =  U3_gga(x1, x2, x3, x5)
U5_ggaga(x1, x2, x3, x4, x5, x6)  =  U5_ggaga(x1, x2, x3, x4, x6)
normalA_out_ga(x1, x2)  =  normalA_out_ga(x1, x2)
pB_out_ggaga(x1, x2, x3, x4, x5)  =  pB_out_ggaga(x1, x2, x3, x4, x5)
NORMALA_IN_GA(x1, x2)  =  NORMALA_IN_GA(x1)
U1_GA(x1, x2, x3, x4, x5)  =  U1_GA(x1, x2, x3, x5)
U2_GA(x1, x2, x3, x4, x5)  =  U2_GA(x1, x2, x3, x5)
PB_IN_GGAGA(x1, x2, x3, x4, x5)  =  PB_IN_GGAGA(x1, x2, x4)
U4_GGAGA(x1, x2, x3, x4, x5, x6)  =  U4_GGAGA(x1, x2, x4, x6)
REWRITEC_IN_GGA(x1, x2, x3)  =  REWRITEC_IN_GGA(x1, x2)
U3_GGA(x1, x2, x3, x4, x5)  =  U3_GGA(x1, x2, x3, x5)
U5_GGAGA(x1, x2, x3, x4, x5, x6)  =  U5_GGAGA(x1, x2, x3, x4, x6)

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

(4) Obligation:

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

NORMALA_IN_GA(op(op(T20, T21), T22), T7) → U1_GA(T20, T21, T22, T7, normalA_in_ga(op(T20, op(T21, T22)), T7))
NORMALA_IN_GA(op(op(T20, T21), T22), T7) → NORMALA_IN_GA(op(T20, op(T21, T22)), T7)
NORMALA_IN_GA(op(T39, op(T40, T41)), T7) → U2_GA(T39, T40, T41, T7, pB_in_ggaga(T40, T41, X48, T39, T7))
NORMALA_IN_GA(op(T39, op(T40, T41)), T7) → PB_IN_GGAGA(T40, T41, X48, T39, T7)
PB_IN_GGAGA(T40, T41, T48, T39, T7) → U4_GGAGA(T40, T41, T48, T39, T7, rewriteC_in_gga(T40, T41, T48))
PB_IN_GGAGA(T40, T41, T48, T39, T7) → REWRITEC_IN_GGA(T40, T41, T48)
REWRITEC_IN_GGA(T76, op(T77, T78), op(T76, X90)) → U3_GGA(T76, T77, T78, X90, rewriteC_in_gga(T77, T78, X90))
REWRITEC_IN_GGA(T76, op(T77, T78), op(T76, X90)) → REWRITEC_IN_GGA(T77, T78, X90)
U4_GGAGA(T40, T41, T48, T39, T7, rewriteC_out_gga(T40, T41, T48)) → U5_GGAGA(T40, T41, T48, T39, T7, normalA_in_ga(op(T39, T48), T7))
U4_GGAGA(T40, T41, T48, T39, T7, rewriteC_out_gga(T40, T41, T48)) → NORMALA_IN_GA(op(T39, T48), T7)

The TRS R consists of the following rules:

normalA_in_ga(op(op(T20, T21), T22), T7) → U1_ga(T20, T21, T22, T7, normalA_in_ga(op(T20, op(T21, T22)), T7))
normalA_in_ga(op(T39, op(T40, T41)), T7) → U2_ga(T39, T40, T41, T7, pB_in_ggaga(T40, T41, X48, T39, T7))
pB_in_ggaga(T40, T41, T48, T39, T7) → U4_ggaga(T40, T41, T48, T39, T7, rewriteC_in_gga(T40, T41, T48))
rewriteC_in_gga(op(T67, T68), T69, op(T67, op(T68, T69))) → rewriteC_out_gga(op(T67, T68), T69, op(T67, op(T68, T69)))
rewriteC_in_gga(T76, op(T77, T78), op(T76, X90)) → U3_gga(T76, T77, T78, X90, rewriteC_in_gga(T77, T78, X90))
U3_gga(T76, T77, T78, X90, rewriteC_out_gga(T77, T78, X90)) → rewriteC_out_gga(T76, op(T77, T78), op(T76, X90))
U4_ggaga(T40, T41, T48, T39, T7, rewriteC_out_gga(T40, T41, T48)) → U5_ggaga(T40, T41, T48, T39, T7, normalA_in_ga(op(T39, T48), T7))
normalA_in_ga(T90, T90) → normalA_out_ga(T90, T90)
U5_ggaga(T40, T41, T48, T39, T7, normalA_out_ga(op(T39, T48), T7)) → pB_out_ggaga(T40, T41, T48, T39, T7)
U2_ga(T39, T40, T41, T7, pB_out_ggaga(T40, T41, X48, T39, T7)) → normalA_out_ga(op(T39, op(T40, T41)), T7)
U1_ga(T20, T21, T22, T7, normalA_out_ga(op(T20, op(T21, T22)), T7)) → normalA_out_ga(op(op(T20, T21), T22), T7)

The argument filtering Pi contains the following mapping:
normalA_in_ga(x1, x2)  =  normalA_in_ga(x1)
op(x1, x2)  =  op(x1, x2)
U1_ga(x1, x2, x3, x4, x5)  =  U1_ga(x1, x2, x3, x5)
U2_ga(x1, x2, x3, x4, x5)  =  U2_ga(x1, x2, x3, x5)
pB_in_ggaga(x1, x2, x3, x4, x5)  =  pB_in_ggaga(x1, x2, x4)
U4_ggaga(x1, x2, x3, x4, x5, x6)  =  U4_ggaga(x1, x2, x4, x6)
rewriteC_in_gga(x1, x2, x3)  =  rewriteC_in_gga(x1, x2)
rewriteC_out_gga(x1, x2, x3)  =  rewriteC_out_gga(x1, x2, x3)
U3_gga(x1, x2, x3, x4, x5)  =  U3_gga(x1, x2, x3, x5)
U5_ggaga(x1, x2, x3, x4, x5, x6)  =  U5_ggaga(x1, x2, x3, x4, x6)
normalA_out_ga(x1, x2)  =  normalA_out_ga(x1, x2)
pB_out_ggaga(x1, x2, x3, x4, x5)  =  pB_out_ggaga(x1, x2, x3, x4, x5)
NORMALA_IN_GA(x1, x2)  =  NORMALA_IN_GA(x1)
U1_GA(x1, x2, x3, x4, x5)  =  U1_GA(x1, x2, x3, x5)
U2_GA(x1, x2, x3, x4, x5)  =  U2_GA(x1, x2, x3, x5)
PB_IN_GGAGA(x1, x2, x3, x4, x5)  =  PB_IN_GGAGA(x1, x2, x4)
U4_GGAGA(x1, x2, x3, x4, x5, x6)  =  U4_GGAGA(x1, x2, x4, x6)
REWRITEC_IN_GGA(x1, x2, x3)  =  REWRITEC_IN_GGA(x1, x2)
U3_GGA(x1, x2, x3, x4, x5)  =  U3_GGA(x1, x2, x3, x5)
U5_GGAGA(x1, x2, x3, x4, x5, x6)  =  U5_GGAGA(x1, x2, x3, x4, x6)

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

(5) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 2 SCCs with 5 less nodes.

(6) Complex Obligation (AND)

(7) Obligation:

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

REWRITEC_IN_GGA(T76, op(T77, T78), op(T76, X90)) → REWRITEC_IN_GGA(T77, T78, X90)

The TRS R consists of the following rules:

normalA_in_ga(op(op(T20, T21), T22), T7) → U1_ga(T20, T21, T22, T7, normalA_in_ga(op(T20, op(T21, T22)), T7))
normalA_in_ga(op(T39, op(T40, T41)), T7) → U2_ga(T39, T40, T41, T7, pB_in_ggaga(T40, T41, X48, T39, T7))
pB_in_ggaga(T40, T41, T48, T39, T7) → U4_ggaga(T40, T41, T48, T39, T7, rewriteC_in_gga(T40, T41, T48))
rewriteC_in_gga(op(T67, T68), T69, op(T67, op(T68, T69))) → rewriteC_out_gga(op(T67, T68), T69, op(T67, op(T68, T69)))
rewriteC_in_gga(T76, op(T77, T78), op(T76, X90)) → U3_gga(T76, T77, T78, X90, rewriteC_in_gga(T77, T78, X90))
U3_gga(T76, T77, T78, X90, rewriteC_out_gga(T77, T78, X90)) → rewriteC_out_gga(T76, op(T77, T78), op(T76, X90))
U4_ggaga(T40, T41, T48, T39, T7, rewriteC_out_gga(T40, T41, T48)) → U5_ggaga(T40, T41, T48, T39, T7, normalA_in_ga(op(T39, T48), T7))
normalA_in_ga(T90, T90) → normalA_out_ga(T90, T90)
U5_ggaga(T40, T41, T48, T39, T7, normalA_out_ga(op(T39, T48), T7)) → pB_out_ggaga(T40, T41, T48, T39, T7)
U2_ga(T39, T40, T41, T7, pB_out_ggaga(T40, T41, X48, T39, T7)) → normalA_out_ga(op(T39, op(T40, T41)), T7)
U1_ga(T20, T21, T22, T7, normalA_out_ga(op(T20, op(T21, T22)), T7)) → normalA_out_ga(op(op(T20, T21), T22), T7)

The argument filtering Pi contains the following mapping:
normalA_in_ga(x1, x2)  =  normalA_in_ga(x1)
op(x1, x2)  =  op(x1, x2)
U1_ga(x1, x2, x3, x4, x5)  =  U1_ga(x1, x2, x3, x5)
U2_ga(x1, x2, x3, x4, x5)  =  U2_ga(x1, x2, x3, x5)
pB_in_ggaga(x1, x2, x3, x4, x5)  =  pB_in_ggaga(x1, x2, x4)
U4_ggaga(x1, x2, x3, x4, x5, x6)  =  U4_ggaga(x1, x2, x4, x6)
rewriteC_in_gga(x1, x2, x3)  =  rewriteC_in_gga(x1, x2)
rewriteC_out_gga(x1, x2, x3)  =  rewriteC_out_gga(x1, x2, x3)
U3_gga(x1, x2, x3, x4, x5)  =  U3_gga(x1, x2, x3, x5)
U5_ggaga(x1, x2, x3, x4, x5, x6)  =  U5_ggaga(x1, x2, x3, x4, x6)
normalA_out_ga(x1, x2)  =  normalA_out_ga(x1, x2)
pB_out_ggaga(x1, x2, x3, x4, x5)  =  pB_out_ggaga(x1, x2, x3, x4, x5)
REWRITEC_IN_GGA(x1, x2, x3)  =  REWRITEC_IN_GGA(x1, x2)

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

(8) UsableRulesProof (EQUIVALENT transformation)

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

(9) Obligation:

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

REWRITEC_IN_GGA(T76, op(T77, T78), op(T76, X90)) → REWRITEC_IN_GGA(T77, T78, X90)

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

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

(10) PiDPToQDPProof (SOUND transformation)

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

(11) Obligation:

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

REWRITEC_IN_GGA(T76, op(T77, T78)) → REWRITEC_IN_GGA(T77, T78)

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

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

• REWRITEC_IN_GGA(T76, op(T77, T78)) → REWRITEC_IN_GGA(T77, T78)
  The graph contains the following edges 2 > 1, 2 > 2

(13) YES

(14) Obligation:

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

NORMALA_IN_GA(op(T39, op(T40, T41)), T7) → PB_IN_GGAGA(T40, T41, X48, T39, T7)
PB_IN_GGAGA(T40, T41, T48, T39, T7) → U4_GGAGA(T40, T41, T48, T39, T7, rewriteC_in_gga(T40, T41, T48))
U4_GGAGA(T40, T41, T48, T39, T7, rewriteC_out_gga(T40, T41, T48)) → NORMALA_IN_GA(op(T39, T48), T7)
NORMALA_IN_GA(op(op(T20, T21), T22), T7) → NORMALA_IN_GA(op(T20, op(T21, T22)), T7)

The TRS R consists of the following rules:

normalA_in_ga(op(op(T20, T21), T22), T7) → U1_ga(T20, T21, T22, T7, normalA_in_ga(op(T20, op(T21, T22)), T7))
normalA_in_ga(op(T39, op(T40, T41)), T7) → U2_ga(T39, T40, T41, T7, pB_in_ggaga(T40, T41, X48, T39, T7))
pB_in_ggaga(T40, T41, T48, T39, T7) → U4_ggaga(T40, T41, T48, T39, T7, rewriteC_in_gga(T40, T41, T48))
rewriteC_in_gga(op(T67, T68), T69, op(T67, op(T68, T69))) → rewriteC_out_gga(op(T67, T68), T69, op(T67, op(T68, T69)))
rewriteC_in_gga(T76, op(T77, T78), op(T76, X90)) → U3_gga(T76, T77, T78, X90, rewriteC_in_gga(T77, T78, X90))
U3_gga(T76, T77, T78, X90, rewriteC_out_gga(T77, T78, X90)) → rewriteC_out_gga(T76, op(T77, T78), op(T76, X90))
U4_ggaga(T40, T41, T48, T39, T7, rewriteC_out_gga(T40, T41, T48)) → U5_ggaga(T40, T41, T48, T39, T7, normalA_in_ga(op(T39, T48), T7))
normalA_in_ga(T90, T90) → normalA_out_ga(T90, T90)
U5_ggaga(T40, T41, T48, T39, T7, normalA_out_ga(op(T39, T48), T7)) → pB_out_ggaga(T40, T41, T48, T39, T7)
U2_ga(T39, T40, T41, T7, pB_out_ggaga(T40, T41, X48, T39, T7)) → normalA_out_ga(op(T39, op(T40, T41)), T7)
U1_ga(T20, T21, T22, T7, normalA_out_ga(op(T20, op(T21, T22)), T7)) → normalA_out_ga(op(op(T20, T21), T22), T7)

The argument filtering Pi contains the following mapping:
normalA_in_ga(x1, x2)  =  normalA_in_ga(x1)
op(x1, x2)  =  op(x1, x2)
U1_ga(x1, x2, x3, x4, x5)  =  U1_ga(x1, x2, x3, x5)
U2_ga(x1, x2, x3, x4, x5)  =  U2_ga(x1, x2, x3, x5)
pB_in_ggaga(x1, x2, x3, x4, x5)  =  pB_in_ggaga(x1, x2, x4)
U4_ggaga(x1, x2, x3, x4, x5, x6)  =  U4_ggaga(x1, x2, x4, x6)
rewriteC_in_gga(x1, x2, x3)  =  rewriteC_in_gga(x1, x2)
rewriteC_out_gga(x1, x2, x3)  =  rewriteC_out_gga(x1, x2, x3)
U3_gga(x1, x2, x3, x4, x5)  =  U3_gga(x1, x2, x3, x5)
U5_ggaga(x1, x2, x3, x4, x5, x6)  =  U5_ggaga(x1, x2, x3, x4, x6)
normalA_out_ga(x1, x2)  =  normalA_out_ga(x1, x2)
pB_out_ggaga(x1, x2, x3, x4, x5)  =  pB_out_ggaga(x1, x2, x3, x4, x5)
NORMALA_IN_GA(x1, x2)  =  NORMALA_IN_GA(x1)
PB_IN_GGAGA(x1, x2, x3, x4, x5)  =  PB_IN_GGAGA(x1, x2, x4)
U4_GGAGA(x1, x2, x3, x4, x5, x6)  =  U4_GGAGA(x1, x2, x4, x6)

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

(15) UsableRulesProof (EQUIVALENT transformation)

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

(16) Obligation:

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

NORMALA_IN_GA(op(T39, op(T40, T41)), T7) → PB_IN_GGAGA(T40, T41, X48, T39, T7)
PB_IN_GGAGA(T40, T41, T48, T39, T7) → U4_GGAGA(T40, T41, T48, T39, T7, rewriteC_in_gga(T40, T41, T48))
U4_GGAGA(T40, T41, T48, T39, T7, rewriteC_out_gga(T40, T41, T48)) → NORMALA_IN_GA(op(T39, T48), T7)
NORMALA_IN_GA(op(op(T20, T21), T22), T7) → NORMALA_IN_GA(op(T20, op(T21, T22)), T7)

The TRS R consists of the following rules:

rewriteC_in_gga(op(T67, T68), T69, op(T67, op(T68, T69))) → rewriteC_out_gga(op(T67, T68), T69, op(T67, op(T68, T69)))
rewriteC_in_gga(T76, op(T77, T78), op(T76, X90)) → U3_gga(T76, T77, T78, X90, rewriteC_in_gga(T77, T78, X90))
U3_gga(T76, T77, T78, X90, rewriteC_out_gga(T77, T78, X90)) → rewriteC_out_gga(T76, op(T77, T78), op(T76, X90))

The argument filtering Pi contains the following mapping:
op(x1, x2)  =  op(x1, x2)
rewriteC_in_gga(x1, x2, x3)  =  rewriteC_in_gga(x1, x2)
rewriteC_out_gga(x1, x2, x3)  =  rewriteC_out_gga(x1, x2, x3)
U3_gga(x1, x2, x3, x4, x5)  =  U3_gga(x1, x2, x3, x5)
NORMALA_IN_GA(x1, x2)  =  NORMALA_IN_GA(x1)
PB_IN_GGAGA(x1, x2, x3, x4, x5)  =  PB_IN_GGAGA(x1, x2, x4)
U4_GGAGA(x1, x2, x3, x4, x5, x6)  =  U4_GGAGA(x1, x2, x4, x6)

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

(17) PiDPToQDPProof (SOUND transformation)

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

(18) Obligation:

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

NORMALA_IN_GA(op(T39, op(T40, T41))) → PB_IN_GGAGA(T40, T41, T39)
PB_IN_GGAGA(T40, T41, T39) → U4_GGAGA(T40, T41, T39, rewriteC_in_gga(T40, T41))
U4_GGAGA(T40, T41, T39, rewriteC_out_gga(T40, T41, T48)) → NORMALA_IN_GA(op(T39, T48))
NORMALA_IN_GA(op(op(T20, T21), T22)) → NORMALA_IN_GA(op(T20, op(T21, T22)))

The TRS R consists of the following rules:

rewriteC_in_gga(op(T67, T68), T69) → rewriteC_out_gga(op(T67, T68), T69, op(T67, op(T68, T69)))
rewriteC_in_gga(T76, op(T77, T78)) → U3_gga(T76, T77, T78, rewriteC_in_gga(T77, T78))
U3_gga(T76, T77, T78, rewriteC_out_gga(T77, T78, X90)) → rewriteC_out_gga(T76, op(T77, T78), op(T76, X90))

The set Q consists of the following terms:

rewriteC_in_gga(x0, x1)
U3_gga(x0, x1, x2, x3)

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

(19) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04,JAR06].

The following pairs can be oriented strictly and are deleted.

NORMALA_IN_GA(op(op(T20, T21), T22)) → NORMALA_IN_GA(op(T20, op(T21, T22)))

The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial interpretation [POLO]:

POL(NORMALA_IN_GA(x₁)) = x₁   
POL(PB_IN_GGAGA(x₁, x₂, x₃)) = 1 + x₃   
POL(U3_gga(x₁, x₂, x₃, x₄)) = 0   
POL(U4_GGAGA(x₁, x₂, x₃, x₄)) = 1 + x₃   
POL(op(x₁, x₂)) = 1 + x₁   
POL(rewriteC_in_gga(x₁, x₂)) = 0   
POL(rewriteC_out_gga(x₁, x₂, x₃)) = 0   

The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:
none

(20) Obligation:

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

NORMALA_IN_GA(op(T39, op(T40, T41))) → PB_IN_GGAGA(T40, T41, T39)
PB_IN_GGAGA(T40, T41, T39) → U4_GGAGA(T40, T41, T39, rewriteC_in_gga(T40, T41))
U4_GGAGA(T40, T41, T39, rewriteC_out_gga(T40, T41, T48)) → NORMALA_IN_GA(op(T39, T48))

The TRS R consists of the following rules:

rewriteC_in_gga(op(T67, T68), T69) → rewriteC_out_gga(op(T67, T68), T69, op(T67, op(T68, T69)))
rewriteC_in_gga(T76, op(T77, T78)) → U3_gga(T76, T77, T78, rewriteC_in_gga(T77, T78))
U3_gga(T76, T77, T78, rewriteC_out_gga(T77, T78, X90)) → rewriteC_out_gga(T76, op(T77, T78), op(T76, X90))

The set Q consists of the following terms:

rewriteC_in_gga(x0, x1)
U3_gga(x0, x1, x2, x3)

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

(21) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04,JAR06].

The following pairs can be oriented strictly and are deleted.

PB_IN_GGAGA(T40, T41, T39) → U4_GGAGA(T40, T41, T39, rewriteC_in_gga(T40, T41))
U4_GGAGA(T40, T41, T39, rewriteC_out_gga(T40, T41, T48)) → NORMALA_IN_GA(op(T39, T48))

The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial Order [NEGPOLO,POLO] with Interpretation:

POL( U4_GGAGA(x₁, ..., x₄) ) = max{0, 2x₃ + x₄ - 1}

POL( rewriteC_in_gga(x₁, x₂) ) = 2x₁ + x₂ + 2

POL( op(x₁, x₂) ) = 2x₁ + x₂ + 2

POL( rewriteC_out_gga(x₁, ..., x₃) ) = x₃ + 2

POL( U3_gga(x₁, ..., x₄) ) = 2x₁ + x₄ + 2

POL( NORMALA_IN_GA(x₁) ) = max{0, x₁ - 2}

POL( PB_IN_GGAGA(x₁, ..., x₃) ) = 2x₁ + x₂ + 2x₃ + 2

The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:

rewriteC_in_gga(op(T67, T68), T69) → rewriteC_out_gga(op(T67, T68), T69, op(T67, op(T68, T69)))
rewriteC_in_gga(T76, op(T77, T78)) → U3_gga(T76, T77, T78, rewriteC_in_gga(T77, T78))
U3_gga(T76, T77, T78, rewriteC_out_gga(T77, T78, X90)) → rewriteC_out_gga(T76, op(T77, T78), op(T76, X90))

(22) Obligation:

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

NORMALA_IN_GA(op(T39, op(T40, T41))) → PB_IN_GGAGA(T40, T41, T39)

The TRS R consists of the following rules:

rewriteC_in_gga(op(T67, T68), T69) → rewriteC_out_gga(op(T67, T68), T69, op(T67, op(T68, T69)))
rewriteC_in_gga(T76, op(T77, T78)) → U3_gga(T76, T77, T78, rewriteC_in_gga(T77, T78))
U3_gga(T76, T77, T78, rewriteC_out_gga(T77, T78, X90)) → rewriteC_out_gga(T76, op(T77, T78), op(T76, X90))

The set Q consists of the following terms:

rewriteC_in_gga(x0, x1)
U3_gga(x0, x1, x2, x3)

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

(23) DependencyGraphProof (EQUIVALENT transformation)

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

(24) TRUE