YES

Problem 1:

(VAR vu95NonEmpty x)
(RULES
not(x) -> ffalse | x ->* ftrue
not(x) -> ftrue | x ->* ffalse
)

Problem 1:

Well-founded Relation Processor:
-> Rules:
 not(x) -> ffalse | x ->* ftrue
 not(x) -> ftrue | x ->* ffalse
->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 not : S -> S .
op fSNonEmpty :  -> S .
op ffalse :  -> S .
op ftrue :  -> 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 => not(x1) ->R not(y1)
x ->R* ftrue => not(x) ->R ffalse
x ->R* ffalse => not(x) ->R ftrue
x ->R y => sqsupset(x,y)

Results:


Domains:
S: |N \ {0}

Function Interpretations:
|[fSNonEmpty]| = 1
|[ffalse]| = 1
|[ftrue]| = 1
|[not(x_1_1:S)]| = 3.x_1_1:S

Predicate Interpretations:
 x_1_1:S ->* x_2_1:S <=> (x_1_1:S >= x_2_1:S)
 x_1_1:S -> x_2_1:S <=> (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.92user 0.11system 0:01.47elapsed 70%CPU (0avgtext+0avgdata 22476maxresident)k
26064inputs+56outputs (117major+7007minor)pagefaults 0swaps