YES

Problem 1:

(VAR vu95NonEmpty x)
(RULES
p(s(x)) -> x
pos(p(x)) -> ffalse | pos(x) ->* ffalse
pos(s(num0)) -> ftrue
pos(s(x)) -> ftrue | pos(x) ->* ftrue
pos(num0) -> ffalse
s(p(x)) -> x
)

Problem 1:

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

Results:


Domains:
S: |N \ {0}

Function Interpretations:
|[fSNonEmpty]| = 1
|[ffalse]| = 1
|[ftrue]| = 1
|[num0]| = 1
|[p(x_1_1:S)]| = x_1_1:S
|[pos(x_1_1:S)]| = 1 + x_1_1:S
|[s(x_1_1:S)]| = 1 + x_1_1:S

Predicate Interpretations:
 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 -> 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.70user 0.10system 0:01.12elapsed 72%CPU (0avgtext+0avgdata 35408maxresident)k
25856inputs+88outputs (116major+10712minor)pagefaults 0swaps