YES Termination proof of INVY_15_quicktest_sum.ari

Termination of the given RelTRS could be proven:

0 RelTRS
↳1 RelTRStoRelADPProof (⇔, 0 ms)
↳2 RelADPP
↳3 RelADPDepGraphProof (⇔, 0 ms)
↳4 AND
    ↳5 RelADPP
        ↳6 RelADPCleverAfsProof (⇒, 24 ms)
        ↳7 QDP
        ↳8 MRRProof (⇔, 4 ms)
        ↳9 QDP
        ↳10 MRRProof (⇔, 0 ms)
        ↳11 QDP
        ↳12 MRRProof (⇔, 0 ms)
        ↳13 QDP
        ↳14 MRRProof (⇔, 3 ms)
        ↳15 QDP
        ↳16 QDPBoundsTAProof (⇔, 0 ms)
        ↳17 QDP
        ↳18 PisEmptyProof (⇔, 0 ms)
        ↳19 YES
    ↳20 RelADPP
        ↳21 RelADPDerelatifyingProof (⇔, 0 ms)
        ↳22 QDP
        ↳23 MRRProof (⇔, 0 ms)
        ↳24 QDP
        ↳25 PisEmptyProof (⇔, 0 ms)
        ↳26 YES
    ↳27 RelADPP
        ↳28 RelADPCleverAfsProof (⇒, 23 ms)
        ↳29 QDP
        ↳30 MRRProof (⇔, 3 ms)
        ↳31 QDP
        ↳32 PisEmptyProof (⇔, 0 ms)
        ↳33 YES
    ↳34 RelADPP
        ↳35 RelADPDerelatifyingProof (⇔, 0 ms)
        ↳36 QDP
        ↳37 MRRProof (⇔, 0 ms)
        ↳38 QDP
        ↳39 MRRProof (⇔, 0 ms)
        ↳40 QDP
        ↳41 MRRProof (⇔, 0 ms)
        ↳42 QDP
        ↳43 MRRProof (⇔, 0 ms)
        ↳44 QDP
        ↳45 MRRProof (⇔, 0 ms)
        ↳46 QDP
        ↳47 TransformationProof (⇔, 0 ms)
        ↳48 QDP
        ↳49 TransformationProof (⇔, 0 ms)
        ↳50 QDP
        ↳51 QDPBoundsTAProof (⇔, 0 ms)
        ↳52 QDP
        ↳53 PisEmptyProof (⇔, 0 ms)
        ↳54 YES

(0) Obligation:

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

+(0, y) → y
+(s(x), y) → s(+(x, y))
sum1(nil) → 0
sum1(cons(x, y)) → +(x, sum1(y))
sum2(nil, z) → z
sum2(cons(x, y), z) → sum2(y, +(x, z))
tests(0) → true
tests(s(x)) → and(test(rands(rand(0), nil)), x)
test(done(y)) → eq(f(y), g(y))
eq(x, x) → true
rands(0, y) → done(y)
rands(s(x), y) → rands(x, ::(rand(0), y))

The relative TRS consists of the following S rules:

rand(x) → rand(s(x))
rand(x) → 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:

+(0, y) → y
+(s(x), y) → s(+1(x, y))
sum1(nil) → 0
sum1(cons(x, y)) → +1(x, sum1(y))
sum1(cons(x, y)) → +(x, SUM1(y))
sum2(nil, z) → z
sum2(cons(x, y), z) → SUM2(y, +(x, z))
sum2(cons(x, y), z) → sum2(y, +1(x, z))
tests(0) → true
tests(s(x)) → and(TEST(rands(rand(0), nil)), x)
tests(s(x)) → and(test(RANDS(rand(0), nil)), x)
tests(s(x)) → and(test(rands(RAND(0), nil)), x)
test(done(y)) → EQ(f(y), g(y))
eq(x, x) → true
rands(0, y) → done(y)
rands(s(x), y) → RANDS(x, ::(rand(0), y))
rands(s(x), y) → rands(x, ::(RAND(0), y))

and relative ADPs:

rand(x) → RAND(s(x))
rand(x) → x

(3) RelADPDepGraphProof (EQUIVALENT transformation)

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

(4) Complex Obligation (AND)

(5) Obligation:

Relative ADP Problem with
absolute ADPs:

+(s(x), y) → s(+1(x, y))

and relative ADPs:

rands(0, y) → done(y)
rands(s(x), y) → rands(x, ::(rand(0), y))
sum1(nil) → 0
tests(0) → true
sum2(cons(x, y), z) → sum2(y, +(x, z))
rand(x) → rand(s(x))
eq(x, x) → true
sum1(cons(x, y)) → +(x, sum1(y))
sum2(nil, z) → z
tests(s(x)) → and(test(rands(rand(0), nil)), x)
test(done(y)) → eq(f(y), g(y))
+(0, y) → y
rand(x) → x

(6) 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:rands_2 = true = done_1 = 0 sum1_1 = and_2 = rand_1 = g_1 = nil = s_1 = eq_2 = 0, 1 +_2 = ::_2 = tests_1 = f_1 = 0 = +^1_2 = cons_2 = test_1 = 0 sum2_2 =
Found this filtering by looking at the following order that orders at least one DP strictly:Combined order from the following AFS and order.
+1(x1, x2)  =  +1(x1, x2)
s(x1)  =  s(x1)
test(x1)  =  test
done(x1)  =  done
eq(x1, x2)  =  eq
f(x1)  =  f(x1)
g(x1)  =  g(x1)
true  =  true

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

s1 > +^12
test > [eq, true]
test > f1
test > g1

Status:
+^12: multiset
s1: multiset
test: multiset
done: multiset
eq: []
f1: multiset
g1: multiset
true: multiset

(7) Obligation:

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

+10(s0(x), y) → +10(x, y)

The TRS R consists of the following rules:

rands0(00, y) → done
rands0(s0(x), y) → rands0(x, ::0(rand0(00), y))
sum10(nil0) → 00
tests0(00) → true0
sum20(cons0(x, y), z) → sum20(y, +0(x, z))
rand0(x) → rand0(s0(x))
eq → true0
sum10(cons0(x, y)) → +0(x, sum10(y))
sum20(nil0, z) → z
tests0(s0(x)) → and0(test, x)
+0(s0(x), y) → s0(+0(x, y))
test → eq
+0(00, y) → y
rand0(x) → x

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

(8) 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 rules of the TRS R:

rands0(00, y) → done
tests0(00) → true0
sum20(cons0(x, y), z) → sum20(y, +0(x, z))
sum10(cons0(x, y)) → +0(x, sum10(y))
sum20(nil0, z) → z
tests0(s0(x)) → and0(test, x)

Used ordering: Polynomial interpretation [POLO]:

POL(+0(x1, x2)) = x1 + x2   
POL(+10(x1, x2)) = x1 + x2   
POL(00) = 0   
POL(::0(x1, x2)) = x1 + x2   
POL(and0(x1, x2)) = x1 + x2   
POL(cons0(x1, x2)) = 1 + x1 + x2   
POL(done) = 0   
POL(eq) = 0   
POL(nil0) = 0   
POL(rand0(x1)) = x1   
POL(rands0(x1, x2)) = 2 + x1 + 2·x2   
POL(s0(x1)) = x1   
POL(sum10(x1)) = x1   
POL(sum20(x1, x2)) = 2 + 2·x1 + x2   
POL(test) = 0   
POL(tests0(x1)) = 2 + 2·x1   
POL(true0) = 0   

(9) Obligation:

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

+10(s0(x), y) → +10(x, y)

The TRS R consists of the following rules:

rands0(s0(x), y) → rands0(x, ::0(rand0(00), y))
sum10(nil0) → 00
rand0(x) → rand0(s0(x))
eq → true0
+0(s0(x), y) → s0(+0(x, y))
test → eq
+0(00, y) → y
rand0(x) → x

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

(10) 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 rules of the TRS R:

sum10(nil0) → 00
eq → true0

Used ordering: Polynomial interpretation [POLO]:

POL(+0(x1, x2)) = x1 + x2   
POL(+10(x1, x2)) = x1 + x2   
POL(00) = 0   
POL(::0(x1, x2)) = x1 + x2   
POL(eq) = 2   
POL(nil0) = 0   
POL(rand0(x1)) = x1   
POL(rands0(x1, x2)) = x1 + 2·x2   
POL(s0(x1)) = x1   
POL(sum10(x1)) = 2 + 2·x1   
POL(test) = 2   
POL(true0) = 0   

(11) Obligation:

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

+10(s0(x), y) → +10(x, y)

The TRS R consists of the following rules:

rands0(s0(x), y) → rands0(x, ::0(rand0(00), y))
rand0(x) → rand0(s0(x))
+0(s0(x), y) → s0(+0(x, y))
test → eq
+0(00, y) → y
rand0(x) → x

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

(12) 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 rules of the TRS R:

test → eq

Used ordering: Polynomial interpretation [POLO]:

POL(+0(x1, x2)) = x1 + x2   
POL(+10(x1, x2)) = 2·x1 + x2   
POL(00) = 0   
POL(::0(x1, x2)) = x1 + x2   
POL(eq) = 1   
POL(rand0(x1)) = x1   
POL(rands0(x1, x2)) = x1 + 2·x2   
POL(s0(x1)) = x1   
POL(test) = 2   

(13) Obligation:

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

+10(s0(x), y) → +10(x, y)

The TRS R consists of the following rules:

rands0(s0(x), y) → rands0(x, ::0(rand0(00), y))
rand0(x) → rand0(s0(x))
+0(s0(x), y) → s0(+0(x, y))
+0(00, y) → y
rand0(x) → x

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

(14) 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 rules of the TRS R:

+0(00, y) → y

Used ordering: Polynomial interpretation [POLO]:

POL(+0(x1, x2)) = 2 + x1 + x2   
POL(+10(x1, x2)) = x1 + x2   
POL(00) = 0   
POL(::0(x1, x2)) = x1 + x2   
POL(rand0(x1)) = x1   
POL(rands0(x1, x2)) = x1 + 2·x2   
POL(s0(x1)) = x1   

(15) Obligation:

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

+10(s0(x), y) → +10(x, y)

The TRS R consists of the following rules:

rands0(s0(x), y) → rands0(x, ::0(rand0(00), y))
rand0(x) → rand0(s0(x))
+0(s0(x), y) → s0(+0(x, y))
rand0(x) → x

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

(16) QDPBoundsTAProof (EQUIVALENT transformation)

The DP-Problem (P, R) could be shown to be Match-DP-Bounded [TAB_NONLEFTLINEAR] by 0 for the Rule:

+10(s0(x), y) → +10(x, y)
by considering the usable rules:
none

The compatible tree automaton used to show the Match-DP-Boundedness is represented by:
final states : [0]
transitions:
#0() → 1
#0() → 2
+^100(1, 2) → 0

(17) Obligation:

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

rands0(s0(x), y) → rands0(x, ::0(rand0(00), y))
rand0(x) → rand0(s0(x))
+0(s0(x), y) → s0(+0(x, y))
rand0(x) → x

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

(18) PisEmptyProof (EQUIVALENT transformation)

The TRS P is empty. Hence, there is no (P,Q,R) chain.

(19) YES

(20) Obligation:

Relative ADP Problem with
absolute ADPs:

sum2(cons(x, y), z) → SUM2(y, +(x, z))

and relative ADPs:

rands(0, y) → done(y)
rands(s(x), y) → rands(x, ::(rand(0), y))
sum1(nil) → 0
tests(0) → true
sum2(cons(x, y), z) → sum2(y, +(x, z))
rand(x) → rand(s(x))
eq(x, x) → true
sum1(cons(x, y)) → +(x, sum1(y))
sum2(nil, z) → z
tests(s(x)) → and(test(rands(rand(0), nil)), x)
+(s(x), y) → s(+(x, y))
test(done(y)) → eq(f(y), g(y))
+(0, y) → y
rand(x) → x

(21) RelADPDerelatifyingProof (EQUIVALENT 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.

(22) Obligation:

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

SUM2(cons(x, y), z) → SUM2(y, +(x, z))

The TRS R consists of the following rules:

rands(0, y) → done(y)
rands(s(x), y) → rands(x, ::(rand(0), y))
sum1(nil) → 0
tests(0) → true
sum2(cons(x, y), z) → sum2(y, +(x, z))
rand(x) → rand(s(x))
eq(x, x) → true
sum1(cons(x, y)) → +(x, sum1(y))
sum2(nil, z) → z
tests(s(x)) → and(test(rands(rand(0), nil)), x)
+(s(x), y) → s(+(x, y))
test(done(y)) → eq(f(y), g(y))
+(0, y) → y
rand(x) → x

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

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

SUM2(cons(x, y), z) → SUM2(y, +(x, z))

Strictly oriented rules of the TRS R:

tests(0) → true
sum2(cons(x, y), z) → sum2(y, +(x, z))
sum1(cons(x, y)) → +(x, sum1(y))
sum2(nil, z) → z
tests(s(x)) → and(test(rands(rand(0), nil)), x)

Used ordering: Polynomial interpretation [POLO]:

POL(+(x1, x2)) = x1 + x2   
POL(0) = 0   
POL(::(x1, x2)) = x1 + x2   
POL(SUM2(x1, x2)) = 2·x1 + 2·x2   
POL(and(x1, x2)) = x1 + x2   
POL(cons(x1, x2)) = 1 + 2·x1 + x2   
POL(done(x1)) = x1   
POL(eq(x1, x2)) = x1 + x2   
POL(f(x1)) = x1   
POL(g(x1)) = x1   
POL(nil) = 0   
POL(rand(x1)) = x1   
POL(rands(x1, x2)) = x1 + 2·x2   
POL(s(x1)) = x1   
POL(sum1(x1)) = x1   
POL(sum2(x1, x2)) = 2 + 2·x1 + 2·x2   
POL(test(x1)) = 2·x1   
POL(tests(x1)) = 2 + 2·x1   
POL(true) = 0   

(24) Obligation:

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

rands(0, y) → done(y)
rands(s(x), y) → rands(x, ::(rand(0), y))
sum1(nil) → 0
rand(x) → rand(s(x))
eq(x, x) → true
+(s(x), y) → s(+(x, y))
test(done(y)) → eq(f(y), g(y))
+(0, y) → y
rand(x) → x

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

(25) PisEmptyProof (EQUIVALENT transformation)

The TRS P is empty. Hence, there is no (P,Q,R) chain.

(26) YES

(27) Obligation:

Relative ADP Problem with
absolute ADPs:

sum1(cons(x, y)) → +(x, SUM1(y))

and relative ADPs:

rands(0, y) → done(y)
rands(s(x), y) → rands(x, ::(rand(0), y))
sum1(nil) → 0
tests(0) → true
sum2(cons(x, y), z) → sum2(y, +(x, z))
rand(x) → rand(s(x))
eq(x, x) → true
sum1(cons(x, y)) → +(x, sum1(y))
sum2(nil, z) → z
tests(s(x)) → and(test(rands(rand(0), nil)), x)
+(s(x), y) → s(+(x, y))
test(done(y)) → eq(f(y), g(y))
+(0, y) → y
rand(x) → x

(28) 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:rands_2 = true = done_1 = 0 sum1_1 = SUM1_1 = and_2 = rand_1 = g_1 = nil = s_1 = eq_2 = 0, 1 +_2 = ::_2 = tests_1 = f_1 = 0 = cons_2 = test_1 = 0 sum2_2 =
Found this filtering by looking at the following order that orders at least one DP strictly:Combined order from the following AFS and order.
SUM1(x1)  =  x1
cons(x1, x2)  =  cons(x1, x2)
test(x1)  =  test
done(x1)  =  done
eq(x1, x2)  =  eq
f(x1)  =  f(x1)
g(x1)  =  g(x1)
true  =  true

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

test > [eq, true]
test > f1
test > g1

Status:
cons2: multiset
test: multiset
done: []
eq: []
f1: multiset
g1: multiset
true: multiset

(29) Obligation:

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

SUM10(cons0(x, y)) → SUM10(y)

The TRS R consists of the following rules:

rands0(00, y) → done
rands0(s0(x), y) → rands0(x, ::0(rand0(00), y))
sum10(nil0) → 00
tests0(00) → true0
sum20(cons0(x, y), z) → sum20(y, +0(x, z))
rand0(x) → rand0(s0(x))
eq → true0
sum10(cons0(x, y)) → +0(x, sum10(y))
sum20(nil0, z) → z
tests0(s0(x)) → and0(test, x)
+0(s0(x), y) → s0(+0(x, y))
test → eq
+0(00, y) → y
rand0(x) → x

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

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

SUM10(cons0(x, y)) → SUM10(y)

Strictly oriented rules of the TRS R:

rands0(00, y) → done
tests0(00) → true0
sum20(cons0(x, y), z) → sum20(y, +0(x, z))
sum10(cons0(x, y)) → +0(x, sum10(y))
sum20(nil0, z) → z
tests0(s0(x)) → and0(test, x)

Used ordering: Polynomial interpretation [POLO]:

POL(+0(x1, x2)) = x1 + x2   
POL(00) = 0   
POL(::0(x1, x2)) = x1 + x2   
POL(SUM10(x1)) = x1   
POL(and0(x1, x2)) = x1 + x2   
POL(cons0(x1, x2)) = 1 + x1 + x2   
POL(done) = 0   
POL(eq) = 0   
POL(nil0) = 0   
POL(rand0(x1)) = x1   
POL(rands0(x1, x2)) = 2 + x1 + 2·x2   
POL(s0(x1)) = x1   
POL(sum10(x1)) = x1   
POL(sum20(x1, x2)) = 2 + 2·x1 + x2   
POL(test) = 0   
POL(tests0(x1)) = 2 + 2·x1   
POL(true0) = 0   

(31) Obligation:

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

rands0(s0(x), y) → rands0(x, ::0(rand0(00), y))
sum10(nil0) → 00
rand0(x) → rand0(s0(x))
eq → true0
+0(s0(x), y) → s0(+0(x, y))
test → eq
+0(00, y) → y
rand0(x) → x

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

(32) PisEmptyProof (EQUIVALENT transformation)

The TRS P is empty. Hence, there is no (P,Q,R) chain.

(33) YES

(34) Obligation:

Relative ADP Problem with
absolute ADPs:

rands(s(x), y) → RANDS(x, ::(rand(0), y))

and relative ADPs:

rands(0, y) → done(y)
rands(s(x), y) → rands(x, ::(rand(0), y))
sum1(nil) → 0
tests(0) → true
sum2(cons(x, y), z) → sum2(y, +(x, z))
rand(x) → rand(s(x))
eq(x, x) → true
sum1(cons(x, y)) → +(x, sum1(y))
sum2(nil, z) → z
tests(s(x)) → and(test(rands(rand(0), nil)), x)
+(s(x), y) → s(+(x, y))
test(done(y)) → eq(f(y), g(y))
+(0, y) → y
rand(x) → x

(35) RelADPDerelatifyingProof (EQUIVALENT 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.

(36) Obligation:

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

RANDS(s(x), y) → RANDS(x, ::(rand(0), y))

The TRS R consists of the following rules:

rands(0, y) → done(y)
rands(s(x), y) → rands(x, ::(rand(0), y))
sum1(nil) → 0
tests(0) → true
sum2(cons(x, y), z) → sum2(y, +(x, z))
rand(x) → rand(s(x))
eq(x, x) → true
sum1(cons(x, y)) → +(x, sum1(y))
sum2(nil, z) → z
tests(s(x)) → and(test(rands(rand(0), nil)), x)
+(s(x), y) → s(+(x, y))
test(done(y)) → eq(f(y), g(y))
+(0, y) → y
rand(x) → x

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

(37) 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 rules of the TRS R:

sum2(cons(x, y), z) → sum2(y, +(x, z))
sum1(cons(x, y)) → +(x, sum1(y))
sum2(nil, z) → z

Used ordering: Polynomial interpretation [POLO]:

POL(+(x1, x2)) = x1 + x2   
POL(0) = 0   
POL(::(x1, x2)) = x1 + x2   
POL(RANDS(x1, x2)) = x1 + x2   
POL(and(x1, x2)) = x1 + x2   
POL(cons(x1, x2)) = 1 + x1 + x2   
POL(done(x1)) = 2·x1   
POL(eq(x1, x2)) = x1 + x2   
POL(f(x1)) = x1   
POL(g(x1)) = x1   
POL(nil) = 0   
POL(rand(x1)) = x1   
POL(rands(x1, x2)) = x1 + 2·x2   
POL(s(x1)) = x1   
POL(sum1(x1)) = x1   
POL(sum2(x1, x2)) = 2 + 2·x1 + x2   
POL(test(x1)) = 2·x1   
POL(tests(x1)) = 2·x1   
POL(true) = 0   

(38) Obligation:

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

RANDS(s(x), y) → RANDS(x, ::(rand(0), y))

The TRS R consists of the following rules:

rands(0, y) → done(y)
rands(s(x), y) → rands(x, ::(rand(0), y))
sum1(nil) → 0
tests(0) → true
rand(x) → rand(s(x))
eq(x, x) → true
tests(s(x)) → and(test(rands(rand(0), nil)), x)
+(s(x), y) → s(+(x, y))
test(done(y)) → eq(f(y), g(y))
+(0, y) → y
rand(x) → x

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

(39) 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 rules of the TRS R:

sum1(nil) → 0
tests(0) → true
tests(s(x)) → and(test(rands(rand(0), nil)), x)

Used ordering: Polynomial interpretation [POLO]:

POL(+(x1, x2)) = x1 + x2   
POL(0) = 0   
POL(::(x1, x2)) = x1 + x2   
POL(RANDS(x1, x2)) = x1 + x2   
POL(and(x1, x2)) = x1 + x2   
POL(done(x1)) = 2·x1   
POL(eq(x1, x2)) = x1 + x2   
POL(f(x1)) = x1   
POL(g(x1)) = x1   
POL(nil) = 0   
POL(rand(x1)) = x1   
POL(rands(x1, x2)) = x1 + 2·x2   
POL(s(x1)) = x1   
POL(sum1(x1)) = 2 + x1   
POL(test(x1)) = 2·x1   
POL(tests(x1)) = 2 + 2·x1   
POL(true) = 0   

(40) Obligation:

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

RANDS(s(x), y) → RANDS(x, ::(rand(0), y))

The TRS R consists of the following rules:

rands(0, y) → done(y)
rands(s(x), y) → rands(x, ::(rand(0), y))
rand(x) → rand(s(x))
eq(x, x) → true
+(s(x), y) → s(+(x, y))
test(done(y)) → eq(f(y), g(y))
+(0, y) → y
rand(x) → x

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

(41) 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 rules of the TRS R:

+(0, y) → y

Used ordering: Polynomial interpretation [POLO]:

POL(+(x1, x2)) = 2 + x1 + x2   
POL(0) = 0   
POL(::(x1, x2)) = x1 + x2   
POL(RANDS(x1, x2)) = x1 + x2   
POL(done(x1)) = 2·x1   
POL(eq(x1, x2)) = x1 + x2   
POL(f(x1)) = x1   
POL(g(x1)) = x1   
POL(rand(x1)) = x1   
POL(rands(x1, x2)) = x1 + 2·x2   
POL(s(x1)) = x1   
POL(test(x1)) = 2·x1   
POL(true) = 0   

(42) Obligation:

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

RANDS(s(x), y) → RANDS(x, ::(rand(0), y))

The TRS R consists of the following rules:

rands(0, y) → done(y)
rands(s(x), y) → rands(x, ::(rand(0), y))
rand(x) → rand(s(x))
eq(x, x) → true
+(s(x), y) → s(+(x, y))
test(done(y)) → eq(f(y), g(y))
rand(x) → x

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

(43) 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 rules of the TRS R:

test(done(y)) → eq(f(y), g(y))

Used ordering: Polynomial interpretation [POLO]:

POL(+(x1, x2)) = x1 + x2   
POL(0) = 0   
POL(::(x1, x2)) = x1 + x2   
POL(RANDS(x1, x2)) = x1 + x2   
POL(done(x1)) = 2 + 2·x1   
POL(eq(x1, x2)) = x1 + x2   
POL(f(x1)) = x1   
POL(g(x1)) = x1   
POL(rand(x1)) = x1   
POL(rands(x1, x2)) = 2 + x1 + 2·x2   
POL(s(x1)) = x1   
POL(test(x1)) = 2 + 2·x1   
POL(true) = 0   

(44) Obligation:

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

RANDS(s(x), y) → RANDS(x, ::(rand(0), y))

The TRS R consists of the following rules:

rands(0, y) → done(y)
rands(s(x), y) → rands(x, ::(rand(0), y))
rand(x) → rand(s(x))
eq(x, x) → true
+(s(x), y) → s(+(x, y))
rand(x) → x

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

(45) 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 rules of the TRS R:

rands(0, y) → done(y)
eq(x, x) → true

Used ordering: Polynomial interpretation [POLO]:

POL(+(x1, x2)) = x1 + x2   
POL(0) = 0   
POL(::(x1, x2)) = x1 + x2   
POL(RANDS(x1, x2)) = x1 + x2   
POL(done(x1)) = x1   
POL(eq(x1, x2)) = 2 + x1 + x2   
POL(rand(x1)) = x1   
POL(rands(x1, x2)) = 1 + x1 + 2·x2   
POL(s(x1)) = x1   
POL(true) = 1   

(46) Obligation:

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

RANDS(s(x), y) → RANDS(x, ::(rand(0), y))

The TRS R consists of the following rules:

rands(s(x), y) → rands(x, ::(rand(0), y))
rand(x) → rand(s(x))
+(s(x), y) → s(+(x, y))
rand(x) → x

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

(47) TransformationProof (EQUIVALENT transformation)

By instantiating [LPAR04] the rule RANDS(s(x), y) → RANDS(x, ::(rand(0), y)) we obtained the following new rules [LPAR04]:

RANDS(s(x0), ::(y_1, y_2)) → RANDS(x0, ::(rand(0), ::(y_1, y_2))) → RANDS(s(x0), ::(y_1, y_2)) → RANDS(x0, ::(rand(0), ::(y_1, y_2)))

(48) Obligation:

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

RANDS(s(x0), ::(y_1, y_2)) → RANDS(x0, ::(rand(0), ::(y_1, y_2)))

The TRS R consists of the following rules:

rands(s(x), y) → rands(x, ::(rand(0), y))
rand(x) → rand(s(x))
+(s(x), y) → s(+(x, y))
rand(x) → x

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

(49) TransformationProof (EQUIVALENT transformation)

By instantiating [LPAR04] the rule RANDS(s(x0), ::(y_1, y_2)) → RANDS(x0, ::(rand(0), ::(y_1, y_2))) we obtained the following new rules [LPAR04]:

RANDS(s(x0), ::(y_1, ::(y_2, y_3))) → RANDS(x0, ::(rand(0), ::(y_1, ::(y_2, y_3)))) → RANDS(s(x0), ::(y_1, ::(y_2, y_3))) → RANDS(x0, ::(rand(0), ::(y_1, ::(y_2, y_3))))

(50) Obligation:

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

RANDS(s(x0), ::(y_1, ::(y_2, y_3))) → RANDS(x0, ::(rand(0), ::(y_1, ::(y_2, y_3))))

The TRS R consists of the following rules:

rands(s(x), y) → rands(x, ::(rand(0), y))
rand(x) → rand(s(x))
+(s(x), y) → s(+(x, y))
rand(x) → x

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

(51) QDPBoundsTAProof (EQUIVALENT transformation)

The DP-Problem (P, R) could be shown to be Match-DP-Bounded [TAB_NONLEFTLINEAR] by 0 for the Rule:

RANDS(s(x0), ::(y_1, ::(y_2, y_3))) → RANDS(x0, ::(rand(0), ::(y_1, ::(y_2, y_3))))
by considering the usable rules:

rand(x) → rand(s(x))
rand(x) → x

The compatible tree automaton used to show the Match-DP-Boundedness is represented by:
final states : [0]
transitions:
#0() → 1
01() → 4
rand0(4) → 3
#0() → 6
#0() → 8
::0(6, 8) → 7
::0(6, 7) → 5
::0(3, 5) → 2
RANDS0(1, 2) → 0
s0(4) → 9
rand0(9) → 3
::0(6, 7) → 11
::0(3, 11) → 10
::0(3, 10) → 2
s0(9) → 9
::0(3, 11) → 11
::0(4, 11) → 11
::0(4, 11) → 10
4 → 3
9 → 3

(52) Obligation:

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

rands(s(x), y) → rands(x, ::(rand(0), y))
rand(x) → rand(s(x))
+(s(x), y) → s(+(x, y))
rand(x) → x

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

(53) PisEmptyProof (EQUIVALENT transformation)

The TRS P is empty. Hence, there is no (P,Q,R) chain.

(54) YES