YES

Problem 1:

(VAR vu95NonEmpty x)
(RULES
a -> c
a -> d
b -> c
b -> d
c -> e
c -> l
d -> m
f(x) -> x | x ->* e
g(d,x,x) -> A
h(x,x) -> g(x,x,f(k))
k -> l
k -> m
)

Problem 1:

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

Results:


Domains:
S: |N U {-1}

Function Interpretations:
|[A]| = - 1
|[a]| = 3
|[b]| = 3
|[c]| = 2
|[d]| = 1
|[e]| = 1
|[f(x_1_1:S)]| = 9 + x_1_1:S
|[fSNonEmpty]| = - 1
|[g(x_1_1:S,x_2_1:S,x_3_1:S)]| = 11 + 7.x_1_1:S + 2.x_2_1:S + x_3_1:S
|[h(x_1_1:S,x_2_1:S)]| = 22 + 5.x_1_1:S + 4.x_2_1:S
|[k]| = 1
|[l]| = - 1
|[m]| = 0

Predicate Interpretations:
 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) <=> (2.x_1_1:S >= 1 + 2.x_2_1:S)

The problem is finite.
8.78user 0.23system 0:09.32elapsed 96%CPU (0avgtext+0avgdata 163396maxresident)k
26064inputs+208outputs (117major+42777minor)pagefaults 0swaps