/* OddEvenPrime
 * Author: 
 * Creation date: 02/11/2019
 */
MACHINE
    OddEvenPrime
    
DEFINITIONS // comme des macro 
    divides(nn,dd) == (#kk . (kk : NATURAL & (nn = kk * dd)))
    ; odd(nn) == not divides(nn,2) // ie impair
    ; even(nn) == divides(nn,2) // ie pair
    ; foo(xx, yy) == ( (xx <= yy) or (yy <= xx) )

CONSTANTS  // CONSTANTS+PROPERTIES vont toujours ensemble
    divisible
,   prime
,   pair // pair (even)
,   impair // impair (odd)

PROPERTIES // on y défint les constantes
    divisible : NATURAL * NATURAL --> BOOL
&   !(nn,dd).((nn : NATURAL & dd : NATURAL & dd > 0) => (divisible(nn,dd) = bool(#kk . (kk : NATURAL & (nn = kk * dd)))))

&   prime : NATURAL --> BOOL // a prime number
&   !(nn).((nn : NATURAL) => ((prime(nn) = 
             bool(!di.( (di : NATURAL & (divides (nn,di))) => ( (di = 1) or ((di = nn) & (di /=1 ))) )) ))) 

&   pair : NATURAL --> BOOL 
&  !nn.((nn: NATURAL) => (pair(nn) = bool(#kk . (kk : NATURAL & (nn = kk * 2))))) 
  
&   impair : NATURAL --> BOOL  
&  !nn.((nn: NATURAL) => (impair(nn) = bool(not(#kk . (kk : NATURAL & (nn = kk * 2)))))) 


ASSERTIONS // les assertions doivent etre prouvees
    !nn.((nn : NATURAL) => ( even(nn) or odd(nn) ))  // tout entier est pair ou impair 
;
    ! nn.((nn : NATURAL) => ( even(nn) or odd(nn) ))  // tout entier est pair ou impair
; 
    !(nn,mm).((nn : NATURAL & mm: NATURAL) => foo(nn,mm))

// paire d'une autre façon  
/*    !nn.((nn: NATURAL & (#kk . (kk : NATURAL & (nn = kk * 2)))) => pair(nn) = TRUE)
;
    !nn.((nn: NATURAL) => (pair(nn) = bool(#kk . (kk : NATURAL & (nn = kk * 2))))) 
    ;
    !(nn).(((nn : NATURAL) & 
             (!di.( (di : NATURAL & (divides (nn,di))) => ( (di = 1) or (di = nn)))))  
     => ((prime(nn) = TRUE))) */
END