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)