Termination proof of INVY_15

Termination of the given RelTRS could be proven:

0 RelTRS

↳1 RelTRStoRelADPProof (⇔, 0 ms)

↳2 RelADPP

↳3 RelADPDepGraphProof (⇔, 0 ms)

↳4 RelADPP

↳5 RelADPCleverAfsProof (⇒, 60 ms)

↳6 QDP

↳7 MRRProof (⇔, 0 ms)

↳8 QDP

↳9 PisEmptyProof (⇔, 0 ms)

↳10 YES

(0) Obligation:

Relative term rewrite system:
The relative TRS consists of the following R rules:

g(s(x), y) → g(f(x, y), y)

The relative TRS consists of the following S rules:

f(x, y) → f(x, s(y))
f(x, y) → x

(1) RelTRStoRelADPProof (EQUIVALENT transformation)

We upgrade the RelTRS problem to an equivalent Relative ADP Problem [IJCAR24].

(2) Obligation:

Relative ADP Problem with
absolute ADPs:

g(s(x), y) → G(f(x, y), y)
g(s(x), y) → g(F(x, y), y)

and relative ADPs:

f(x, y) → F(x, s(y))
f(x, y) → x

(3) RelADPDepGraphProof (EQUIVALENT transformation)

We use the relative dependency graph processor [IJCAR24].
The approximation of the Relative Dependency Graph contains:
1 SCC with nodes from P_abs,
0 Lassos,
Result: This relative DT problem is equivalent to 1 subproblem.

(4) Obligation:

Relative ADP Problem with
absolute ADPs:

g(s(x), y) → G(f(x, y), y)

and relative ADPs:

f(x, y) → f(x, s(y))
f(x, y) → x
g(s(x), y) → g(f(x, y), y)

(5) RelADPCleverAfsProof (SOUND transformation)

We use the first derelatifying processor [IJCAR24].
There are no annotations in relative ADPs, so the relative ADP problem can be transformed into a non-relative DP problem.

Furthermore, We use an argument filter [LPAR04].
Filtering:s_1 = G_2 = f_2 = 1 g_2 = 0
Found this filtering by looking at the following order that orders at least one DP strictly:Combined order from the following AFS and order.
G(x1, x2) = G(x1, x2)
s(x1) = s(x1)
f(x1, x2) = f(x1)
g(x1, x2) = x2

Recursive path order with status [RPO].
Quasi-Precedence:

s₁ > f₁ > G₂

Status:

G₂: [2,1]
s₁: [1]
f₁: [1]

(6) Obligation:

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

G0(s0(x), y) → G0(f(x), y)

The TRS R consists of the following rules:

f(x) → f(x)
f(x) → x
g(y) → g(y)

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

(7) MRRProof (EQUIVALENT transformation)

By using the rule removal processor [LPAR04] with the following ordering, at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.
Strictly oriented dependency pairs:

G0(s0(x), y) → G0(f(x), y)

Strictly oriented rules of the TRS R:

f(x) → x

Used ordering: Knuth-Bendix order [KBO] with precedence:

s0₁ > g₁ > G0₂ > f₁

and weight map:

f_1=1
g_1=1
s0_1=1
G0_2=0

The variable weight is 1

(8) Obligation:

Q DP problem:
P is empty.
The TRS R consists of the following rules:

f(x) → f(x)
g(y) → g(y)