Package list-last: Definitions and theorems about the list last function

Information

namelist-last
version1.12
descriptionDefinitions and theorems about the list last function
authorJoe Hurd <joe@gilith.com>
licenseMIT
showData.Bool
Data.List

Files

Defined Constant

Theorems

l. ¬(l = []) Set.∈ (last l) (toSet l)

h t. last (h :: t) = if t = [] then h else last t

p q. last (p @ q) = if q = [] then last p else last q

(h. last (h :: []) = h) h k t. last (h :: k :: t) = last (k :: t)

Input Type Operators

Input Constants

Assumptions

T

F p. p

(¬) = λp. p F

() = λP. P ((select) P)

t. (x. t) t

() = λp. p = λx. T

x. x = x T

() = λp q. p q p

t. (t T) (t F)

h t. ¬(h :: t = [])

(¬T F) (¬F T)

() = λp q. (λf. f p q) = λf. f T T

() = λP. q. (x. P x q) q

() = λp q. r. (p r) (q r) r

t1 t2. (if T then t1 else t2) = t1 (if F then t1 else t2) = t2

l m. l @ m = [] l = [] m = []

(t. ¬¬t t) (¬T F) (¬F T)

toSet [] = Set.∅ h t. toSet (h :: t) = Set.insert h (toSet t)

x y s. Set.∈ x (Set.insert y s) x = y Set.∈ x s

P. P [] (a0 a1. P a1 P (a0 :: a1)) x. P x

P c x y. P (if c then x else y) (c P x) (¬c P y)

NIL' CONS'.
    fn. fn [] = NIL' a0 a1. fn (a0 :: a1) = CONS' a0 a1 (fn a1)

(l. [] @ l = l) l h t. (h :: t) @ l = h :: t @ l

t. ((T t) t) ((t T) t) ((F t) ¬t) ((t F) ¬t)

t. (T t t) (t T t) (F t F) (t F F) (t t t)

t. (T t T) (t T T) (F t t) (t F t) (t t t)

t. (T t t) (t T T) (F t T) (t t T) (t F ¬t)