Go backward to Example
Go up to Top
Go forward to Example
Recursive predicate definition
with termination function t(x) := x.
iseven subset N iseven(x) : <=> if x = 0 then T else ~iseven(x-1)
iseven(3) = ~iseven(2) = ~~iseven(1) = ~~~iseven(0) = ~~~T = ~~F = ~T = F.
Termination after a finite number of unfoldings.