YES

Problem 1:

(VAR vu95NonEmpty x y)
(RULES
pin(x) -> pout(f(y)) | pin(x) ->* pout(g(y))
pin(x) -> pout(g(x))
)

Problem 1:

Well-founded Relation Processor:
-> Rules:
 pin(x) -> pout(f(y)) | pin(x) ->* pout(g(y))
 pin(x) -> pout(g(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 pin : S -> S .
op f : S -> S .
op fSNonEmpty :  -> S .
op g : S -> S .
op pout : 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 => pin(x1) ->R pin(y1)
x1 ->R y1 => f(x1) ->R f(y1)
x1 ->R y1 => g(x1) ->R g(y1)
x1 ->R y1 => pout(x1) ->R pout(y1)
pin(x) ->R* pout(g(y)) => pin(x) ->R pout(f(y))
pin(x) ->R pout(g(x))
x ->R y => sqsupset(x,y)

Results:


Domains:
S: |N \ {0}

Function Interpretations:
|[f(x_1_1:S)]| = 2 + x_1_1:S
|[fSNonEmpty]| = 1
|[g(x_1_1:S)]| = 5 + 3.x_1_1:S
|[pin(x_1_1:S)]| = 6 + 5.x_1_1:S
|[pout(x_1_1:S)]| = 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 <=> ((1 + x_2_1:S >= 0) /\ (x_1_1:S >= 1 + x_2_1:S))
sqsupset(x_1_1:S,x_2_1:S) <=> (2.x_1_1:S >= 2 + 2.x_2_1:S)

The problem is finite.
0.74user 0.14system 0:01.29elapsed 69%CPU (0avgtext+0avgdata 38160maxresident)k
25080inputs+72outputs (112major+11057minor)pagefaults 0swaps