Package pair-induct: pair-induct

Information

namepair-induct
version1.0
descriptionpair-induct
authorJoe Hurd <joe@gilith.com>
licenseHOLLight
provenanceHOL Light theory extracted on 2011-02-19
showData.Bool

Files

Theorems

x. Data.Pair., (Data.Pair.fst x) (Data.Pair.snd x) = x

P. (x y. P (Data.Pair., x y)) p. P p

PAIR'. fn. a0 a1. fn (Data.Pair., a0 a1) = PAIR' a0 a1

Input Type Operators

Input Constants

Assumptions

T

t. (x. t) t

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

x. x = x T

() = λp q. p q p

x y. Data.Pair.fst (Data.Pair., x y) = x

x y. Data.Pair.snd (Data.Pair., x y) = y

p. x y. p = Data.Pair., x y

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

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