YES

Problem 1:

(VAR vu95NonEmpty x)
(RULES
f(x) -> e | d ->* l
h(x,x) -> A
)

Problem 1:

Well-founded Relation Processor:
-> Rules:
 f(x) -> e | d ->* l
 h(x,x) -> A
->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 f : S -> S .
op h : S S -> S .
op A :  -> S .
op d :  -> S .
op e :  -> S .
op fSNonEmpty :  -> S .
op l :  -> 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 => h(x1,x2) ->R h(y1,x2)
x2 ->R y2 => h(x1,x2) ->R h(x1,y2)
d ->R* l => f(x) ->R e
h(x,x) ->R A
x ->R y => sqsupset(x,y)

Results:


Domains:
S: -|N \ {0}

Function Interpretations:
|[A]| = - 2
|[d]| = - 1
|[e]| = - 1
|[f(x_1_1:S)]| = 7.x_1_1:S
|[fSNonEmpty]| = - 1
|[h(x_1_1:S,x_2_1:S)]| = x_1_1:S + 2.x_2_1:S
|[l]| = - 1

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

The problem is finite.
1.19user 0.05system 0:01.53elapsed 81%CPU (0avgtext+0avgdata 34480maxresident)k
26056inputs+80outputs (117major+10231minor)pagefaults 0swaps