YES

Problem 1:

(VAR vu95NonEmpty)
(RULES
a -> b
a -> c
b -> c | b ->* c
)

Problem 1:

Well-founded Relation Processor:
-> Rules:
 a -> b
 a -> c
 b -> c | b ->* c
->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 b :  -> S .
op c :  -> 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
a ->R b
a ->R c
b ->R* c => b ->R c
x ->R y => sqsupset(x,y)

Results:


Domains:
S: |N

Function Interpretations:
|[a]| = 2
|[b]| = 1
|[c]| = 0
|[fSNonEmpty]| = 0

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

The problem is finite.
0.15user 0.17system 0:00.61elapsed 54%CPU (0avgtext+0avgdata 118040maxresident)k
25848inputs+48outputs (116major+49863minor)pagefaults 0swaps