Theory "numpair"

Signature

Definitions

invtri_def

⊢ ∀n. tri⁻¹ n = SND (invtri0 n 0)

nfst_def

⊢ ∀n. nfst n = tri (tri⁻¹ n) + tri⁻¹ n − n

npair_def

⊢ ∀m n. m ⊗ n = tri (m + n) + n

nsnd_def

⊢ ∀n. nsnd n = n − tri (tri⁻¹ n)

tri_def

⊢ (tri 0 = 0) ∧ ∀n. tri (SUC n) = SUC n + tri n

Theorems

SND_invtri0

⊢ ∀n a. FST (invtri0 n a) < SUC (SND (invtri0 n a))

invtri0_def

⊢ ∀n a.
    invtri0 n a = if n < a + 1 then (n,a) else invtri0 (n − (a + 1)) (a + 1)

invtri0_ind

⊢ ∀P. (∀n a. (¬(n < a + 1) ⇒ P (n − (a + 1)) (a + 1)) ⇒ P n a) ⇒ ∀v v1. P v v1

invtri0_thm

⊢ ∀n a. tri (SND (invtri0 n a)) + FST (invtri0 n a) = n + tri a

invtri_le

⊢ tri⁻¹ n ≤ n

invtri_linverse

⊢ tri⁻¹ (tri n) = n

invtri_linverse_r

⊢ y ≤ x ⇒ (tri⁻¹ (tri x + y) = x)

invtri_lower

⊢ tri (tri⁻¹ n) ≤ n

invtri_unique

⊢ tri y ≤ n ∧ n < tri (y + 1) ⇒ (tri⁻¹ n = y)

invtri_upper

⊢ n < tri (tri⁻¹ n + 1)

nfst0

⊢ nfst 0 = 0

nfst_le

⊢ nfst n ≤ n

nfst_le_npair

⊢ ∀m n. n ≤ n ⊗ m

nfst_npair

⊢ nfst (x ⊗ y) = x

npair

⊢ ∀n. nfst n ⊗ nsnd n = n

npair00

⊢ 0 ⊗ 0 = 0

npair2_lt

⊢ ∀n n1 n2. n ⊗ n1 < n ⊗ n2 ⇔ n1 < n2

npair2_lt_E

⊢ ∀n n1 n2. n ⊗ n1 < n ⊗ n2 ⇒ n1 < n2

npair2_lt_I

⊢ ∀n n1 n2. n1 < n2 ⇒ n ⊗ n1 < n ⊗ n2

npair_11

⊢ (x1 ⊗ y1 = x2 ⊗ y2) ⇔ (x1 = x2) ∧ (y1 = y2)

npair_EQ_0

⊢ ∀x y. (x ⊗ y = 0) ⇔ (x = 0) ∧ (y = 0)

npair_cases

⊢ ∀n. ∃x y. n = x ⊗ y

npairs_lt_I

⊢ ∀a b c d. a ≤ b ∧ c < d ⇒ a ⊗ c < b ⊗ d

nsnd0

⊢ nsnd 0 = 0

nsnd_le

⊢ nsnd n ≤ n

nsnd_le_npair

⊢ ∀m n. m ≤ n ⊗ m

nsnd_npair

⊢ nsnd (x ⊗ y) = y

tri_11

⊢ ∀m n. (tri m = tri n) ⇔ (m = n)

tri_LE

⊢ ∀m n. tri m ≤ tri n ⇔ m ≤ n

tri_LT

⊢ ∀n m. tri n < tri m ⇔ n < m

tri_LT_I

⊢ ∀n m. n < m ⇒ tri n < tri m

tri_eq_0

⊢ ((tri n = 0) ⇔ (n = 0)) ∧ ((0 = tri n) ⇔ (n = 0))

tri_formula

⊢ tri n = n * (n + 1) DIV 2

tri_le

⊢ n ≤ tri n

twotri_formula

⊢ 2 * tri n = n * (n + 1)