(0) Obligation:
Q restricted rewrite system:
The TRS R consists of the following rules:
f_0(x) → a
f_1(x) → g_1(x, x)
g_1(s(x), y) → b(f_0(y), g_1(x, y))
f_2(x) → g_2(x, x)
g_2(s(x), y) → b(f_1(y), g_2(x, y))
f_3(x) → g_3(x, x)
g_3(s(x), y) → b(f_2(y), g_3(x, y))
f_4(x) → g_4(x, x)
g_4(s(x), y) → b(f_3(y), g_4(x, y))
f_5(x) → g_5(x, x)
g_5(s(x), y) → b(f_4(y), g_5(x, y))
f_6(x) → g_6(x, x)
g_6(s(x), y) → b(f_5(y), g_6(x, y))
f_7(x) → g_7(x, x)
g_7(s(x), y) → b(f_6(y), g_7(x, y))
f_8(x) → g_8(x, x)
g_8(s(x), y) → b(f_7(y), g_8(x, y))
f_9(x) → g_9(x, x)
g_9(s(x), y) → b(f_8(y), g_9(x, y))
f_10(x) → g_10(x, x)
g_10(s(x), y) → b(f_9(y), g_10(x, y))
Q is empty.
(1) QTRSRRRProof (EQUIVALENT transformation)
Used ordering:
Recursive path order with status [RPO].
Quasi-Precedence:
f101 > [f91, g102] > [f81, g92] > [s1, f71, g82] > g72 > f61 > [f51, g62] > [f41, g52] > g42 > f31 > [f21, g32] > [f11, g22] > g12 > [f01, a, b2]
Status:
f01: multiset
a: multiset
f11: [1]
g12: [2,1]
s1: [1]
b2: [2,1]
f21: multiset
g22: [2,1]
f31: multiset
g32: multiset
f41: multiset
g42: [1,2]
f51: multiset
g52: multiset
f61: [1]
g62: multiset
f71: [1]
g72: [2,1]
f81: multiset
g82: [2,1]
f91: multiset
g92: multiset
f101: multiset
g102: multiset
With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:
f_0(x) → a
f_1(x) → g_1(x, x)
g_1(s(x), y) → b(f_0(y), g_1(x, y))
f_2(x) → g_2(x, x)
g_2(s(x), y) → b(f_1(y), g_2(x, y))
f_3(x) → g_3(x, x)
g_3(s(x), y) → b(f_2(y), g_3(x, y))
f_4(x) → g_4(x, x)
g_4(s(x), y) → b(f_3(y), g_4(x, y))
f_5(x) → g_5(x, x)
g_5(s(x), y) → b(f_4(y), g_5(x, y))
f_6(x) → g_6(x, x)
g_6(s(x), y) → b(f_5(y), g_6(x, y))
f_7(x) → g_7(x, x)
g_7(s(x), y) → b(f_6(y), g_7(x, y))
f_8(x) → g_8(x, x)
g_8(s(x), y) → b(f_7(y), g_8(x, y))
f_9(x) → g_9(x, x)
g_9(s(x), y) → b(f_8(y), g_9(x, y))
f_10(x) → g_10(x, x)
g_10(s(x), y) → b(f_9(y), g_10(x, y))
(2) Obligation:
Q restricted rewrite system:
R is empty.
Q is empty.
(3) RisEmptyProof (EQUIVALENT transformation)
The TRS R is empty. Hence, termination is trivially proven.
(4) YES