// SPDX-FileCopyrightText: Chris Pressey, the original author of this work, has dedicated it to the public domain.
// For more information, please refer to <https://unlicense.org/>
// SPDX-License-Identifier: Unlicense

module ParityJazz

let even n:nat : bool =
    n % 2 = 0

let odd n:nat : bool =
    n % 2 = 1

//
// It is the case that every natural number is even or odd.
//

let _ = assert (forall (n:nat) . (even n) \/ (odd n))

//
// It is the case that every natural number is not both even and odd.
//

let _ = assert (forall (n:nat) . ~((even n) /\ (odd n)))

//
// It is the case that every natural number is either even or odd, but not both.
//

let _ = assert (forall (n:nat) . ((even n) \/ (odd n)) /\ (~((even n) /\ (odd n))))

let xor a b = (a \/ b) /\ ~(a /\ b)

//
// It is the case that every natural number is either even or odd.
//

let _ = assert (forall (n:nat) . (xor (even n) (odd n)))