define EvenNat : (fn Nat -> bool) = fun n:Nat {
      some m:Nat. n = suc(suc(zero)) * m
    }

Even_not_Odd: (all n:Nat. (EvenNat(n) ⇔ (not OddNat(n))))

Even_or_Odd: (all n:Nat. (EvenNat(n) or OddNat(n)))

define OddNat : (fn Nat -> bool) = fun n:Nat {
      some m:Nat. n = suc(suc(suc(zero)) * m)
    }

addition_of_evens: (all x:Nat, y:Nat. (if (EvenNat(x) and EvenNat(y)) then EvenNat(x + y)))

even_or_odd: (all n:Nat. (is_even(n) or is_odd(n)))

define is_even : (fn Nat -> bool) = fun n:Nat {
      parity(n, true)
    }

is_even_odd: (all n:Nat. ((if is_even(n) then EvenNat(n)) and (if is_odd(n) then OddNat(n))))

define is_odd : (fn Nat -> bool) = fun n:Nat {
      parity(n, false)
    }

recursive parity(Nat,bool) -> bool{
  parity(zero, b) = b
  parity(suc(n'), b) = parity(n', not b)
}