YES

Problem 1:

(VAR vu95NonEmpty x y)
(RULES
a -> d
b -> d
f(x,y) -> g(x) | a ->* d
f(x,y) -> h(x) | b ->* d
g(s(x)) -> x
h(s(x)) -> x
)

Problem 1:

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

Results:


Domains:
S: |N U {-1}

Function Interpretations:
|[a]| = 1
|[b]| = 1
|[d]| = - 1
|[f(x_1_1:S,x_2_1:S)]| = 6 + 2.x_1_1:S + x_2_1:S
|[fSNonEmpty]| = 0
|[g(x_1_1:S)]| = x_1_1:S
|[h(x_1_1:S)]| = x_1_1:S
|[s(x_1_1:S)]| = 2 + x_1_1:S

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

The problem is finite.
3.08user 0.17system 0:03.59elapsed 90%CPU (0avgtext+0avgdata 65040maxresident)k
26064inputs+128outputs (117major+18011minor)pagefaults 0swaps