RAP Examples - Prime Numbers

```{***********************************************************************}
{* TEST OF A NUMBER TO BE PRIME                                        *}
{***********************************************************************}

type DIV
basedon NAT, BOOL
func divides : (Nat,Nat)Bool
axioms all (a, n : Nat)
{1} n = 0  =>  divides(a,n) -> true,
{2} lt(0,n) = true & lt(n,a) = true  =>  divides(a,n) -> false,
{3} le(a,n) = true =>  divides(a,n) -> divides(a,sub(n,a))
endoftype

type ISPRIM
basedon DIV, NAT, BOOL
func isp : (Nat)Bool,
aux : (Nat,Nat)Bool
axioms all (x, a : Nat)
{3} isp(x) -> and(ge(x,2),aux(x,2)),
{4} le(x,a) = true  =>
aux(x,a) -> true,
{5} lt(a,x) = true  =>
aux(x,a) -> and(not(divides(a,x)),aux(x,succ(a)))
endoftype

{***********************************************************************}
{***********************************************************************}

basedon DIV, NAT, BOOL
unknown x : Nat
goals   divides(x,20) = true

basedon ISPRIM, NAT, BOOL
unknown x : Nat
goals   isp(x) = false

basedon ISPRIM, NAT, BOOL
unknown x : Nat
goals   isp(x) = true