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

(0) Obligation:

Clauses:

add(X, 0, X).
add(X, Y, s(Z)) :- ','(\+(isZero(Y)), ','(p(Y, P), add(X, P, Z))).
p(0, 0).
p(s(X), X).
isZero(0).

Query: add(a,g,a)

(1) PrologToTRSTransformerProof (SOUND transformation)

Transformed Prolog program to TRS.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
1 [label="1: add(T1, T2, T3)\n\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
4 [label="4: add(T1, T2, T3), SCOPE: 1, CLAUSE: 0 | add(T1, T2, T3), SCOPE: 1, CLAUSE: 1\n\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
9 [label="9: true | add(T1, 0, T3), SCOPE: 1, CLAUSE: 1\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
13 [label="13: add(T1, T2, T3), SCOPE: 1, CLAUSE: 1\n\nT2 is ground\nX2 is free\nadd(T1, T2, T3) !=? add(X2, 0, X2)", fontsize=16, style=filled, fillcolor=lightyellow];
16 [label="16: add(T1, 0, T3), SCOPE: 1, CLAUSE: 1\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
18 [label="18: ','(\\+(isZero(0)), ','(p(0, X9), add(T10, X9, T11)))\n\nX9 is free", fontsize=16, style=filled, fillcolor=lightyellow];
20 [label="20: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
22 [label="22: ','(call(isZero(0)), ','(!_2, fail)) | ','(p(0, X9), add(T10, X9, T11))\n\nX9 is free", fontsize=16, style=filled, fillcolor=lightyellow];
26 [label="26: ','(isZero(0), ','(!_2, fail)) | ?_3 | ','(p(0, X9), add(T10, X9, T11))\n\nX9 is free", fontsize=16, style=filled, fillcolor=lightyellow];
28 [label="28: ','(isZero(0), ','(!_2, fail)), SCOPE: 4, CLAUSE: 4 | ?_4 | ?_3 | ','(p(0, X9), add(T10, X9, T11))\n\nX9 is free", fontsize=16, style=filled, fillcolor=lightyellow];
31 [label="31: ','(!_2, fail) | ?_4 | ?_3 | ','(p(0, X9), add(T10, X9, T11))\n\nX9 is free", fontsize=16, style=filled, fillcolor=lightyellow];
35 [label="35: fail\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
38 [label="38: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
46 [label="46: ','(\\+(isZero(T16)), ','(p(T16, X16), add(T18, X16, T19)))\n\nT16 is ground\nX2 is free\nX16 is free\nadd(T1, T16, T3) !=? add(X2, 0, X2)", fontsize=16, style=filled, fillcolor=lightyellow];
49 [label="49: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
51 [label="51: ','(call(isZero(T16)), ','(!_5, fail)) | ','(p(T16, X16), add(T18, X16, T19))\n\nT16 is ground\nX2 is free\nX16 is free\nadd(T1, T16, T3) !=? add(X2, 0, X2)", fontsize=16, style=filled, fillcolor=lightyellow];
53 [label="53: ','(isZero(T16), ','(!_5, fail)) | ?_6 | ','(p(T16, X16), add(T18, X16, T19))\n\nT16 is ground\nX2 is free\nX16 is free\nadd(T1, T16, T3) !=? add(X2, 0, X2)", fontsize=16, style=filled, fillcolor=lightyellow];
55 [label="55: ','(isZero(T16), ','(!_5, fail)), SCOPE: 7, CLAUSE: 4 | ?_7 | ?_6 | ','(p(T16, X16), add(T18, X16, T19))\n\nT16 is ground\nX2 is free\nX16 is free\nadd(T1, T16, T3) !=? add(X2, 0, X2)", fontsize=16, style=filled, fillcolor=lightyellow];
58 [label="58: ','(!_5, fail) | ?_7 | ?_6 | ','(p(0, X16), add(T18, X16, T19))\n\nX16 is free", fontsize=16, style=filled, fillcolor=lightyellow];
61 [label="61: ?_7 | ?_6 | ','(p(T16, X16), add(T18, X16, T19))\n\nT16 is ground\nX2 is free\nX16 is free\nadd(T1, T16, T3) !=? add(X2, 0, X2)\nisZero(T16) !=? isZero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
62 [label="62: fail\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
63 [label="63: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
65 [label="65: ?_6 | ','(p(T16, X16), add(T18, X16, T19))\n\nT16 is ground\nX2 is free\nX16 is free\nadd(T1, T16, T3) !=? add(X2, 0, X2)\nisZero(T16) !=? isZero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
68 [label="68: ','(p(T16, X16), add(T18, X16, T19))\n\nT16 is ground\nX2 is free\nX16 is free\nadd(T1, T16, T3) !=? add(X2, 0, X2)\nisZero(T16) !=? isZero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
71 [label="71: ','(p(T16, X16), add(T18, X16, T19)), SCOPE: 8, CLAUSE: 2 | ','(p(T16, X16), add(T18, X16, T19)), SCOPE: 8, CLAUSE: 3\n\nT16 is ground\nX2 is free\nX16 is free\nadd(T1, T16, T3) !=? add(X2, 0, X2)\nisZero(T16) !=? isZero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
72 [label="72: ','(p(T16, X16), add(T18, X16, T19)), SCOPE: 8, CLAUSE: 3\n\nT16 is ground\nX2 is free\nX16 is free\nadd(T1, T16, T3) !=? add(X2, 0, X2)\nisZero(T16) !=? isZero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
75 [label="75: add(T18, T24, T19)\n\nT24 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
76 [label="76: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
77 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
1 -> 77 [arrowhead = none ];
77 -> 4;

78 [label="EVAL with clause\nadd(X2, 0, X2).\nand substitutionT1 -> T5,\nX2 -> T5,\nT2 -> 0,\nT3 -> T5", fontsize=14, style = filled, fillcolor = lightblue];
4 -> 78 [arrowhead = none ];
78 -> 9;

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

80 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
9 -> 80 [arrowhead = none ];
80 -> 16;

81 [label="EVAL with clause\nadd(X13, X14, s(X15)) :- ','(\\+(isZero(X14)), ','(p(X14, X16), add(X13, X16, X15))).\nand substitutionT1 -> T18,\nX13 -> T18,\nT2 -> T16,\nX14 -> T16,\nX15 -> T19,\nT3 -> s(T19),\nT15 -> T18,\nT17 -> T19", fontsize=14, style = filled, fillcolor = lightblue];
13 -> 81 [arrowhead = none ];
81 -> 46;

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

83 [label="EVAL with clause\nadd(X6, X7, s(X8)) :- ','(\\+(isZero(X7)), ','(p(X7, X9), add(X6, X9, X8))).\nand substitutionT1 -> T10,\nX6 -> T10,\nX7 -> 0,\nX8 -> T11,\nT3 -> s(T11),\nT8 -> T10,\nT9 -> T11", fontsize=14, style = filled, fillcolor = lightblue];
16 -> 83 [arrowhead = none ];
83 -> 18;

84 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
16 -> 84 [arrowhead = none ];
84 -> 20;

85 [label="NOT", fontsize=14, style = filled, fillcolor = lightcyan];
18 -> 85 [arrowhead = none ];
85 -> 22;

86 [label="CALL", fontsize=14, style = filled, fillcolor = lightcyan];
22 -> 86 [arrowhead = none ];
86 -> 26;

87 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
26 -> 87 [arrowhead = none ];
87 -> 28;

88 [label="ONLY EVAL with clause\nisZero(0).\nand substitution", fontsize=14, style = filled, fillcolor = lightblue];
28 -> 88 [arrowhead = none ];
88 -> 31;

89 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
31 -> 89 [arrowhead = none ];
89 -> 35;

90 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
35 -> 90 [arrowhead = none ];
90 -> 38;

91 [label="NOT", fontsize=14, style = filled, fillcolor = lightcyan];
46 -> 91 [arrowhead = none ];
91 -> 51;

92 [label="CALL", fontsize=14, style = filled, fillcolor = lightcyan];
51 -> 92 [arrowhead = none ];
92 -> 53;

93 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
53 -> 93 [arrowhead = none ];
93 -> 55;

94 [label="EVAL with clause\nisZero(0).\nand substitutionT16 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
55 -> 94 [arrowhead = none ];
94 -> 58;

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

96 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
58 -> 96 [arrowhead = none ];
96 -> 62;

97 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
61 -> 97 [arrowhead = none ];
97 -> 65;

98 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
62 -> 98 [arrowhead = none ];
98 -> 63;

99 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
65 -> 99 [arrowhead = none ];
99 -> 68;

100 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
68 -> 100 [arrowhead = none ];
100 -> 71;

101 [label="BACKTRACK\nfor clause: p(0, 0)\nwith clash: (isZero(T16), isZero(0))", fontsize=14, style = filled, fillcolor = lightgreen];
71 -> 101 [arrowhead = none ];
101 -> 72;

102 [label="EVAL with clause\np(s(X21), X21).\nand substitutionX21 -> T24,\nT16 -> s(T24),\nX16 -> T24", fontsize=14, style = filled, fillcolor = lightblue];
72 -> 102 [arrowhead = none ];
102 -> 75;

103 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
72 -> 103 [arrowhead = none ];
103 -> 76;

104 [label="INSTANCE with matching:\nT1 -> T18\nT2 -> T24\nT3 -> T19", fontsize=14, style = filled, fillcolor = lightgrey];
75 -> 104 [arrowhead = none , style=dashed];
104 -> 1[style=dashed];

}

(2) Obligation:

Q restricted rewrite system:
The TRS R consists of the following rules:

f1_in(0) → f1_out1
f1_in(s(T24)) → U1(f1_in(T24), s(T24))
U1(f1_out1, s(T24)) → f1_out1

Q is empty.

(3) QTRSRRRProof (EQUIVALENT transformation)

Used ordering:
Polynomial interpretation [POLO]:

POL(0) = 0   
POL(U1(x₁, x₂)) = 1 + x₁ + x₂   
POL(f1_in(x₁)) = 2 + 2·x₁   
POL(f1_out1) = 0   
POL(s(x₁)) = 2 + 2·x₁   

With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:

f1_in(0) → f1_out1
f1_in(s(T24)) → U1(f1_in(T24), s(T24))
U1(f1_out1, s(T24)) → f1_out1

(4) Obligation:

Q restricted rewrite system:
R is empty.
Q is empty.

(5) RisEmptyProof (EQUIVALENT transformation)

The TRS R is empty. Hence, termination is trivially proven.

(6) YES