Theory "listRange"

Signature

Definitions

listRangeINC_def

⊢ ∀m n. [m .. n] = GENLIST (λi. m + i) (n + 1 − m)

listRangeLHI_def

⊢ ∀m n. [m ..< n] = GENLIST (λi. m + i) (n − m)

Theorems

listRangeINC_SING

⊢ [m .. m] = [m]

MEM_listRangeINC

⊢ MEM x [m .. n] ⇔ m ≤ x ∧ x ≤ n

listRangeINC_CONS

⊢ m ≤ n ⇒ [m .. n] = m::[m + 1 .. n]

listRangeINC_EMPTY

⊢ n < m ⇒ [m .. n] = []

listRangeLHI_EQ

⊢ [m ..< m] = []

MEM_listRangeLHI

⊢ MEM x [m ..< n] ⇔ m ≤ x ∧ x < n

listRangeLHI_EMPTY

⊢ hi ≤ lo ⇒ [lo ..< hi] = []

listRangeLHI_CONS

⊢ lo < hi ⇒ [lo ..< hi] = lo::[lo + 1 ..< hi]

listRangeLHI_ALL_DISTINCT

⊢ ALL_DISTINCT [lo ..< hi]

LENGTH_listRangeLHI

⊢ LENGTH [lo ..< hi] = hi − lo

EL_listRangeLHI

⊢ lo + i < hi ⇒ EL i [lo ..< hi] = lo + i