YES

Problem 1:

(VAR vu95NonEmpty x)
(RULES
e(num0) -> ftrue
e(s(x)) -> ffalse | e(x) ->* ftrue
e(s(x)) -> ftrue | o(x) ->* ftrue
o(num0) -> ftrue
o(s(x)) -> ffalse | o(x) ->* ftrue
o(s(x)) -> ftrue | e(x) ->* ftrue
)

Problem 1:

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

Results:


Domains:
S: |N

Function Interpretations:
|[e(x_1_1:S)]| = x_1_1:S
|[fSNonEmpty]| = 1
|[ffalse]| = 1
|[ftrue]| = 0
|[num0]| = 1
|[o(x_1_1:S)]| = 1 + x_1_1:S
|[s(x_1_1:S)]| = 7 + 3.x_1_1:S

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 <=> ((1 + x_2_1:S >= 0) /\ (x_1_1:S >= 1 + x_2_1:S))
sqsupset(x_1_1:S,x_2_1:S) <=> (2.x_1_1:S >= 1 + 2.x_2_1:S)

The problem is finite.
0.44user 0.14system 0:00.86elapsed 68%CPU (0avgtext+0avgdata 33420maxresident)k
25840inputs+88outputs (116major+10232minor)pagefaults 0swaps