YES

Problem 1:

(VAR vu95NonEmpty x y)
(RULES
pin(a) -> pout(b)
pin(b) -> pout(c)
tc(x) -> x
tc(x) -> y | pin(x) ->* pout(z), tc(z) ->* y
)

Problem 1:

Well-founded Relation Processor:
-> Rules:
 pin(a) -> pout(b)
 pin(b) -> pout(c)
 tc(x) -> x
 tc(x) -> y | pin(x) ->* pout(z), tc(z) ->* y
->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 tc : S -> S .
op a :  -> S .
op b :  -> S .
op c :  -> S .
op fSNonEmpty :  -> S .
op pout : S -> S .
op z :  -> 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 => tc(x1) ->R tc(y1)
x1 ->R y1 => pout(x1) ->R pout(y1)
pin(a) ->R pout(b)
pin(b) ->R pout(c)
tc(x) ->R x
pin(x) ->R* pout(z) /\ tc(z) ->R* y => tc(x) ->R y
x ->R y => sqsupset(x,y)

Results:


Domains:
S: |N

Function Interpretations:
|[a]| = 4
|[b]| = 2
|[c]| = 0
|[fSNonEmpty]| = 0
|[pin(x_1_1:S)]| = x_1_1:S
|[pout(x_1_1:S)]| = 1 + x_1_1:S
|[tc(x_1_1:S)]| = 1 + x_1_1:S
|[z]| = 1

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

The problem is finite.
0.48user 0.06system 0:00.87elapsed 62%CPU (0avgtext+0avgdata 31196maxresident)k
25304inputs+80outputs (113major+9398minor)pagefaults 0swaps