YES Termination w.r.t. Q proof of SK90_2.40.ari

(0) Obligation:

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

or(true, y) → true
or(x, true) → true
or(false, false) → false
mem(x, nil) → false
mem(x, set(y)) → =(x, y)
mem(x, union(y, z)) → or(mem(x, y), mem(x, z))

Q is empty.

(1) QTRSRRRProof (EQUIVALENT transformation)

Used ordering:
Combined order from the following AFS and order.
or(x1, x2)  =  or(x1, x2)
true  =  true
false  =  false
mem(x1, x2)  =  mem(x1, x2)
nil  =  nil
set(x1)  =  x1
=(x1, x2)  =  =(x1, x2)
union(x1, x2)  =  union(x1, x2)

Recursive path order with status [RPO].
Quasi-Precedence:
mem2 > or2
mem2 > [false, nil]
mem2 > =2

Status:
or2: multiset
true: multiset
false: multiset
mem2: multiset
nil: multiset
=2: multiset
union2: multiset

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

or(true, y) → true
or(x, true) → true
or(false, false) → false
mem(x, nil) → false
mem(x, set(y)) → =(x, y)
mem(x, union(y, z)) → or(mem(x, y), mem(x, z))


(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