Package list-last-thm: list-last-thm

Information

namelist-last-thm
version1.0
descriptionlist-last-thm
authorJoe Hurd <joe@gilith.com>
licenseHOLLight
provenanceHOL Light theory extracted on 2011-03-15
showData.Bool

Files

Theorems

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

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

Input Type Operators

Input Constants

Assumptions

T

F p. p

(¬) = λp. p F

t. (x. t) t

() = λP. P = λx. T

x. x = x T

() = λp q. p q p

t. (t T) (t F)

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

(¬T F) (¬F T)

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

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

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

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

l m.
    Data.List.@ l m = Data.List.[] l = Data.List.[] m = Data.List.[]

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

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

(l. Data.List.@ Data.List.[] l = l)
  h t l.
    Data.List.@ (Data.List.:: h t) l = Data.List.:: h (Data.List.@ 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)