(0) Obligation:
Clauses:
average(0, 0, 0).
average(0, s(0), 0).
average(0, s(s(0)), s(0)).
average(s(X), Y, Z) :- average(X, s(Y), Z).
average(X, s(s(s(Y))), s(Z)) :- average(s(X), Y, Z).
Query: average(g,a,g)
(1) PrologToTRSTransformerProof (SOUND transformation)
Transformed Prolog program to TRS.
(2) Obligation:
Q restricted rewrite system:
The TRS R consists of the following rules:
f2_in(0, 0) → f2_out1(0)
f2_in(0, 0) → f2_out1(s(0))
f2_in(0, s(0)) → f2_out1(s(s(0)))
f2_in(s(T16), T18) → U1(f2_in(T16, T18), s(T16), T18)
U1(f2_out1(s(T19)), s(T16), T18) → f2_out1(T19)
f2_in(T26, s(T28)) → U2(f2_in(s(T26), T28), T26, s(T28))
U2(f2_out1(T29), T26, s(T28)) → f2_out1(s(s(s(T29))))
Q is empty.
(3) QTRSRRRProof (EQUIVALENT transformation)
Used ordering:
Combined order from the following AFS and order.
f2_in(
x1,
x2) =
f2_in(
x1,
x2)
0 =
0
f2_out1(
x1) =
x1
s(
x1) =
s(
x1)
U1(
x1,
x2,
x3) =
U1(
x1,
x2,
x3)
U2(
x1,
x2,
x3) =
U2(
x1,
x2,
x3)
Recursive path order with status [RPO].
Quasi-Precedence:
f2in2 > 0 > s1
f2in2 > U13 > s1
f2in2 > U23 > s1
Status:
f2in2: [2,1]
0: multiset
s1: multiset
U13: [1,2,3]
U23: multiset
With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:
f2_in(0, 0) → f2_out1(0)
f2_in(0, 0) → f2_out1(s(0))
f2_in(0, s(0)) → f2_out1(s(s(0)))
f2_in(s(T16), T18) → U1(f2_in(T16, T18), s(T16), T18)
U1(f2_out1(s(T19)), s(T16), T18) → f2_out1(T19)
f2_in(T26, s(T28)) → U2(f2_in(s(T26), T28), T26, s(T28))
U2(f2_out1(T29), T26, s(T28)) → f2_out1(s(s(s(T29))))
(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