YES

Problem 1:

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

Problem 1:

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

Results:


Domains:
S: |N \ {0}

Function Interpretations:
|[a]| = 1
|[b]| = 1
|[c]| = 1
|[d]| = 1
|[f(x_1_1:S)]| = 19 + 10.x_1_1:S
|[fSNonEmpty]| = 1
|[g(x_1_1:S,x_2_1:S,x_3_1:S)]| = x_1_1:S + x_2_1:S + x_3_1:S
|[h(x_1_1:S,x_2_1:S)]| = 1 + x_1_1:S + x_2_1:S
|[i(x_1_1:S)]| = 1 + x_1_1:S

Predicate Interpretations:
 x_1_1:S ->* x_2_1:S <=> ((x_2_1:S >= 0) /\ (1 + x_1_1:S >= x_2_1:S))
 x_1_1:S -> x_2_1:S <=> (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.
2.89user 0.16system 0:03.32elapsed 91%CPU (0avgtext+0avgdata 100120maxresident)k
25296inputs+160outputs (113major+26114minor)pagefaults 0swaps