YES

Problem 1:

(VAR vu95NonEmpty x)
(RULES
even(num0) -> ftrue
even(s(x)) -> ffalse | odd(x) ->* ffalse
even(s(x)) -> ftrue | odd(x) ->* ftrue
odd(num0) -> ffalse
odd(s(x)) -> ffalse | even(x) ->* ffalse
odd(s(x)) -> ftrue | even(x) ->* ftrue
)

Problem 1:

Well-founded Relation Processor:
-> Rules:
 even(num0) -> ftrue
 even(s(x)) -> ffalse | odd(x) ->* ffalse
 even(s(x)) -> ftrue | odd(x) ->* ftrue
 odd(num0) -> ffalse
 odd(s(x)) -> ffalse | even(x) ->* ffalse
 odd(s(x)) -> ftrue | even(x) ->* ftrue
->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 even : S -> S .
op odd : S -> S .
op num0 :  -> S .
op fSNonEmpty :  -> S .
op ffalse :  -> S .
op s : S -> S .
op ftrue :  -> 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 => even(x1) ->R even(y1)
x1 ->R y1 => odd(x1) ->R odd(y1)
x1 ->R y1 => s(x1) ->R s(y1)
even(num0) ->R ftrue
odd(x) ->R* ffalse => even(s(x)) ->R ffalse
odd(x) ->R* ftrue => even(s(x)) ->R ftrue
odd(num0) ->R ffalse
even(x) ->R* ffalse => odd(s(x)) ->R ffalse
even(x) ->R* ftrue => odd(s(x)) ->R ftrue
x ->R y => sqsupset(x,y)

Results:


Domains:
S: -|N

Function Interpretations:
|[even(x_1_1:S)]| = - 1 + x_1_1:S
|[fSNonEmpty]| = 0
|[ffalse]| = - 1
|[ftrue]| = 0
|[num0]| = - 2
|[odd(x_1_1:S)]| = x_1_1:S
|[s(x_1_1:S)]| = - 11 + 3.x_1_1:S

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

The problem is finite.
1.62user 0.15system 0:02.07elapsed 85%CPU (0avgtext+0avgdata 48656maxresident)k
26064inputs+88outputs (117major+13464minor)pagefaults 0swaps