Theory cv

⊢ b2c T = cv$Num (SUC 0) ∧ b2c F = cv$Num 0

⊢ ∀x. cv$c2b x ⇔ ∃k. x = cv$Num (SUC k)

⊢ (∀n nmf prf. cv_CASE (cv$Num n) nmf prf = nmf n) ∧
  ∀c d nmf prf. cv_CASE (cv$Pair c d) nmf prf = prf c d

⊢ ∀c d. cv_eq c d = b2c (c = d)

⊢ ∀m n. cv_exp m n = cv$Num (cv$c2n m ** cv$c2n n)

⊢ (∀p q. cv_fst (cv$Pair p q) = p) ∧ ∀m. cv_fst (cv$Num m) = cv$Num 0

⊢ ∀p q r. cv_if p q r = if cv$c2b p then q else r

⊢ (∀p q. cv_ispair (cv$Pair p q) = cv$Num (SUC 0)) ∧
  ∀m. cv_ispair (cv$Num m) = cv$Num 0

⊢ (∀m c.
     cv_lt (cv$Num m) c =
     case c of cv$Num n => b2c (m < n) | cv$Pair v4 v5 => cv$Num 0) ∧
  ∀c d e. cv_lt (cv$Pair c d) e = cv$Num 0

⊢ (∀n. cv_size (cv$Num n) = n) ∧
  ∀c d. cv_size (cv$Pair c d) = 1 + (cv_size c + cv_size d)

⊢ (∀p q. cv_snd (cv$Pair p q) = q) ∧ ∀m. cv_snd (cv$Num m) = cv$Num 0

⊢ (cv$Pair p q = cv$Pair r s ⇔ if p = r then q = s else F) ∧
  (cv$Pair p q = cv$Num n ⇔ F) ∧ (cv$Num m = cv$Num n ⇔ m = n)

⊢ m DIV n = if n = 0 then 0 else if m < n then 0 else SUC ((m − n) DIV n)

⊢ EVEN n ⇔ ¬cv$c2b (cv_mod (cv$Num n) (cv$Num 2))

⊢ (m < 0 ⇔ F) ∧ (m < SUC n ⇔ if m = n then T else m < n)

⊢ m MOD n = if n = 0 then m else if m < n then m else (m − n) MOD n

⊢ cv$Num m = cv$Num n ⇔ m = n

⊢ ODD n ⇔ cv$c2b (cv_mod (cv$Num n) (cv$Num 2))

⊢ cv$Pair c d = cv$Pair e f ⇔ c = e ∧ d = f

⊢ (SUC m = 0 ⇔ F) ∧ (SUC m = SUC n ⇔ m = n)

⊢ m + n = cv$c2n (cv_add (cv$Num m) (cv$Num n))

⊢ (b2c x = cv$Num 1 ⇔ x) ∧ (b2c x = cv$Num (SUC 0) ⇔ x)

⊢ b2c g = if g then cv$Num (SUC 0) else cv$Num 0

⊢ (cv$c2b (cv$Num (SUC n)) ⇔ T) ∧ (cv$c2b (cv$Num 1) ⇔ T) ∧
  (cv$c2b (cv$Num 0) ⇔ F) ∧ (cv$c2b (cv$Num 0) ⇔ F) ∧
  (cv$c2b (cv$Pair x y) ⇔ F)

⊢ cv$c2n (cv_add v1 v2) = cv$c2n v1 + cv$c2n v2

⊢ cv$c2n (cv_mul v1 v2) = cv$c2n v1 * cv$c2n v2

⊢ (∀n. cv$c2n (cv$Num n) = n) ∧ ∀c d. cv$c2n (cv$Pair c d) = 0

⊢ ∀f g. ∃h.
    (∀n. h (cv$Num n) = f n) ∧ ∀c d. h (cv$Pair c d) = g c d (h c) (h d)

⊢ cv_add (cv$Num m) (cv$Num n) = cv$Num (m + n) ∧
  cv_add (cv$Num m) (cv$Pair p q) = cv$Num m ∧
  cv_add (cv$Pair p q) (cv$Num n) = cv$Num n ∧
  cv_add (cv$Pair p q) (cv$Pair r s) = cv$Num 0

⊢ cv$Num n ≠ cv$Pair c d

⊢ cv_div (cv$Num m) (cv$Num n) = cv$Num (m DIV n) ∧
  cv_div (cv$Num m) (cv$Pair p q) = cv$Num 0 ∧
  cv_div (cv$Pair p q) (cv$Num n) = cv$Num 0 ∧
  cv_div (cv$Pair p q) (cv$Pair r s) = cv$Num 0

⊢ cv_eq (cv$Pair x y) (cv$Pair x' y') = b2c (x = x' ∧ y = y') ∧
  cv_eq (cv$Num m) (cv$Num n) = b2c (m = n) ∧
  cv_eq (cv$Pair x y) (cv$Num n) = b2c F ∧
  cv_eq (cv$Num n) (cv$Pair x y) = b2c F

⊢ cv_eq p q = cv$Num (if p = q then SUC 0 else 0)

⊢ cv_exp b e =
  cv_if e
    (cv_if (cv_mod e (cv$Num 2))
       (cv_mul b (cv_exp b (cv_sub e (cv$Num 1))))
       (let x = cv_exp b (cv_div e (cv$Num 2)) in cv_mul x x)) (cv$Num 1)

⊢ cv_lt v (cv$Pair x y) = cv$Num 0 ∧ cv_lt (cv$Pair x y) v = cv$Num 0 ∧
  cv_add (cv$Pair x y) v =
  (case v of cv$Num v4 => v | cv$Pair a b => cv$Num 0) ∧
  cv_add v (cv$Pair x y) =
  (case v of cv$Num v4 => v | cv$Pair a b => cv$Num 0) ∧
  cv_sub (cv$Pair x y) v = cv$Num 0 ∧
  cv_sub v (cv$Pair x y) =
  (case v of cv$Num v4 => v | cv$Pair a b => cv$Num 0) ∧
  cv_mul (cv$Pair x y) v = cv$Num 0 ∧ cv_mul v (cv$Pair x y) = cv$Num 0 ∧
  cv_div (cv$Pair x y) v = cv$Num 0 ∧ cv_div v (cv$Pair x y) = cv$Num 0 ∧
  cv_mod (cv$Pair x y) v = cv$Num 0 ∧
  cv_mod v (cv$Pair x y) =
  case v of cv$Num v4 => v | cv$Pair a b => cv$Num 0

⊢ cv_if x y z = if cv$c2b x then y else z

⊢ (cv$c2b P ⇔ cv$c2b Q) ∧ (cv$c2b Q ⇒ x = x') ∧ (¬cv$c2b Q ⇒ y = y') ⇒
  cv_if P x y = cv_if Q x' y'

⊢ cv_if (cv$Num (SUC m)) p q = p ∧ cv_if (cv$Num 0) p q = q ∧
  cv_if (cv$Pair r s) p q = q

⊢ ∀P. (∀m. P (cv$Num m)) ∧ (∀g g'. P g ∧ P g' ⇒ P (cv$Pair g g')) ⇒ ∀g. P g

⊢ cv_ispair (cv_add x y) = cv$Num 0

⊢ cv$c2b (cv_lt (cv$Num 0) x) ⇔ ∃n. x = cv$Num (SUC n)

⊢ cv_lt (cv$Num m) (cv$Num n) = cv$Num (if m < n then SUC 0 else 0) ∧
  cv_lt (cv$Num m) (cv$Pair p q) = cv$Num 0 ∧
  cv_lt (cv$Pair p q) (cv$Num n) = cv$Num 0 ∧
  cv_lt (cv$Pair p q) (cv$Pair r s) = cv$Num 0

⊢ cv_mod (cv$Num m) (cv$Num n) = cv$Num (m MOD n) ∧
  cv_mod (cv$Num m) (cv$Pair p q) = cv$Num m ∧
  cv_mod (cv$Pair p q) (cv$Num n) = cv$Num 0 ∧
  cv_mod (cv$Pair p q) (cv$Pair r s) = cv$Num 0

⊢ cv_mul (cv$Num m) (cv$Num n) = cv$Num (m * n) ∧
  cv_mul (cv$Num m) (cv$Pair p q) = cv$Num 0 ∧
  cv_mul (cv$Pair p q) (cv$Num n) = cv$Num 0 ∧
  cv_mul (cv$Pair p q) (cv$Pair r s) = cv$Num 0

⊢ cv_sub (cv$Num m) (cv$Num n) = cv$Num (m − n) ∧
  cv_sub (cv$Num m) (cv$Pair p q) = cv$Num m ∧
  cv_sub (cv$Pair p q) (cv$Num n) = cv$Num 0 ∧
  cv_sub (cv$Pair p q) (cv$Pair r s) = cv$Num 0

⊢ m DIV n = cv$c2n (cv_div (cv$Num m) (cv$Num n))

⊢ m ** n = cv$c2n (cv_exp (cv$Num m) (cv$Num n))

⊢ n ≥ m ⇔ ¬cv$c2b (cv_lt (cv$Num n) (cv$Num m))

⊢ m > n ⇔ cv$c2b (cv_lt (cv$Num n) (cv$Num m))

⊢ ∀a0. isnseq a0 ⇔ a0 = cv$Num 0 ∨ ∃n c. a0 = cv$Pair n c ∧ isnseq c

⊢ ∀n c. isnseq c ⇒ isnseq (cv$Pair n c)

⊢ ∀isnseq'.
    isnseq' (cv$Num 0) ∧ (∀n c. isnseq' c ⇒ isnseq' (cv$Pair n c)) ⇒
    ∀a0. isnseq a0 ⇒ isnseq' a0

⊢ isnseq (cv$Num 0)

⊢ isnseq (cv$Num 0) ∧ ∀n c. isnseq c ⇒ isnseq (cv$Pair n c)

⊢ ∀isnseq'.
    isnseq' (cv$Num 0) ∧
    (∀n c. isnseq c ∧ isnseq' c ⇒ isnseq' (cv$Pair n c)) ⇒
    ∀a0. isnseq a0 ⇒ isnseq' a0

⊢ m ≤ n ⇔ ¬cv$c2b (cv_lt (cv$Num n) (cv$Num m))

⊢ m < n ⇔ cv$c2b (cv_lt (cv$Num m) (cv$Num n))

⊢ m MOD n = cv$c2n (cv_mod (cv$Num m) (cv$Num n))

⊢ m * n = cv$c2n (cv_mul (cv$Num m) (cv$Num n))

⊢ ∀m n. m = n ⇔ cv$c2b (cv_eq (cv$Num m) (cv$Num n))

⊢ PRE m = cv$c2n (cv_sub (cv$Num m) (cv$Num 1))

⊢ m − n = cv$c2n (cv_sub (cv$Num m) (cv$Num n))

⊢ SUC m = cv$c2n (cv_add (cv$Num m) (cv$Num 1))