Next: PRODUCT Up: The Rules Previous: UNION

# FUNCTION

rulesubsection23.25ex plus 1ex minus .2ex1.5ex plus .2ex

* formation . H >> ext x:A->B by intro function A new x
* >> A in
* x:A >> ext B

. H >> x:A->B in by intro [new y]
* >> A in
* y:A >> B[y/x] in

. H >> ext A->B by intro function
* >> ext A
* >> ext B

. H >> A->B in by intro
* >> A in
* >> B in

rulesubsection23.25ex plus 1ex minus .2ex1.5ex plus .2ex

* canonical . H >> x:A->B ext y.b by intro at [new y]
* y:A >> B[y/x] ext b
* >> A in

. H >> x.b in y:A->B by intro at [new z]
* z:A >> b[z/x] in B[z/y]
* >> A in

rulesubsection23.25ex plus 1ex minus .2ex1.5ex plus .2ex

* noncanonical . H,f:(x:A->B), >> T ext t[f(a)/y]

by elim f on a [new y] >> a in A
* y:B[a/x] , y=f(a) in B[a/x] >> T ext t

. H,f:(x:A->B), >> T ext t[f(a)/y]

by elim f [new y]
* >> A ext a
* y:B >> T ext t

The first form is used when x occurs free in B, the second when it doesn't.

. H >> f(a) in B[a/x] by intro using x:A->B
* >> f in x:A->B
* >> a in A

rulesubsection23.25ex plus 1ex minus .2ex1.5ex plus .2ex

* equality  . H >> f = g in x:A->B by extensionality [new y]
* y:A >> f(y) = g(y) in B[y/x]
* >> f in x:A->B
* >> g in x:A->B

rulesubsection23.25ex plus 1ex minus .2ex1.5ex plus .2ex

* computation . H >> ( x.b)(a) = t in B by reduce 1
* >> b[a/x] = t in B

Next: PRODUCT Up: The Rules Previous: UNION

Richard Eaton
Thu Sep 14 08:45:18 EDT 1995