fun EvenNat(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)))

fun OddNat(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)))

fun is_even(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))))

fun is_odd(n:Nat) {
  parity(n, false)
}

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