Theory "listRange"

Signature

Definitions

listRangeLHI_def

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

listRangeINC_def

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

Theorems

MEM_listRangeLHI

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

MEM_listRangeINC

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

listRangeLHI_EQ

⊢ [m ..< m] = []

listRangeLHI_EMPTY

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

listRangeLHI_CONS

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

listRangeLHI_ALL_DISTINCT

⊢ ALL_DISTINCT [lo ..< hi]

listRangeINC_SING

⊢ [m .. m] = [m]

listRangeINC_EMPTY

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

listRangeINC_CONS

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

LENGTH_listRangeLHI

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

EL_listRangeLHI

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