YES

Problem 1:

(VAR vu95NonEmpty x)
(RULES
A -> B
f(x) -> x | x ->* a
g(x) -> C | A ->* B
)

Problem 1:

Well-founded Relation Processor:
-> Rules:
 A -> B
 f(x) -> x | x ->* a
 g(x) -> C | A ->* B
->AGES Output:

Model Results

System:
mod InTheory is
sort S .
sort Bool .


op _->*_ : S S -> Bool [m = 2] .
op _->_ : S S -> Bool [m = 2] .
op A :  -> S .
op f : S -> S .
op g : S -> S .
op B :  -> S .
op C :  -> S .
op a :  -> S .
op fSNonEmpty :  -> S .
op sqsupset : S S -> Bool [wellfounded m = 1] .

endm


Property:
x ->R* x
x ->R y /\ y ->R* z => x ->R* z
x1 ->R y1 => f(x1) ->R f(y1)
x1 ->R y1 => g(x1) ->R g(y1)
A ->R B
x ->R* a => f(x) ->R x
A ->R* B => g(x) ->R C
x ->R y => sqsupset(x,y)

Results:


Domains:
S: -|N

Function Interpretations:
|[A]| = - 1
|[B]| = 0
|[C]| = 0
|[a]| = 0
|[f(x_1_1:S)]| = - 1 + 2.x_1_1:S
|[fSNonEmpty]| = 0
|[g(x_1_1:S)]| = - 3 + 2.x_1_1:S

Predicate Interpretations:
 x_1_1:S ->* x_2_1:S <=> (1 >= x_1_1:S + x_2_1:S)
 x_1_1:S -> x_2_1:S <=> (x_2_1:S >= 1 + x_1_1:S)
sqsupset(x_1_1:S,x_2_1:S) <=> (x_2_1:S >= 1 + x_1_1:S)

The problem is finite.
0.36user 0.15system 0:00.78elapsed 65%CPU (0avgtext+0avgdata 25364maxresident)k
25848inputs+64outputs (116major+7943minor)pagefaults 0swaps