YES

Problem 1:

(VAR vu95NonEmpty x z)
(RULES
a -> c
a -> d
f(x) -> z | s(x) ->* t(z)
s(c) -> t(k)
)

Problem 1:

Well-founded Relation Processor:
-> Rules:
 a -> c
 a -> d
 f(x) -> z | s(x) ->* t(z)
 s(c) -> t(k)
->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 s : S -> S .
op c :  -> S .
op d :  -> S .
op fSNonEmpty :  -> S .
op k :  -> S .
op t : S -> 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 => s(x1) ->R s(y1)
x1 ->R y1 => t(x1) ->R t(y1)
a ->R c
a ->R d
s(x) ->R* t(z) => f(x) ->R z
s(c) ->R t(k)
x ->R y => sqsupset(x,y)

Results:


Domains:
S: |N \ {0}

Function Interpretations:
|[a]| = 3
|[c]| = 2
|[d]| = 1
|[f(x_1_1:S)]| = 3.x_1_1:S
|[fSNonEmpty]| = 1
|[k]| = 1
|[s(x_1_1:S)]| = x_1_1:S
|[t(x_1_1:S)]| = 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))
 x_1_1:S -> x_2_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.67user 0.10system 0:01.06elapsed 73%CPU (0avgtext+0avgdata 33032maxresident)k
25304inputs+80outputs (113major+9837minor)pagefaults 0swaps