Next: FUNCTION Up: The Rules Previous: LIST

# UNION

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

* formation . H >> ext A|B by intro union
* >> 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 >> A|B ext inl(a) by intro at left
* >> A ext a
* >> B in

. H >> inl(a) in A|B by intro at
* >> a in A
* >> B in

. H >> A|B ext inr(b) by intro at right
* >> B ext b
* >> A in

. H >> inr(b) in A|B by intro at
* >> b in B
* >> A in

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

* noncanonical . H,z:A|B, >> T ext decide(z;x.;y.) by elim z [new x,y] x:A,z=inl(x) in A|B >> T[inl(x)/z] ext
* y:B,z=inr(y) in A|B >> T[inr(y)/z] ext

. H >> decide(e;x.;y.) in T[e/z]
* by intro [over z.T] using A|B [new u,v]
* >> e in A|B
* u:A, e=inl(u) in A|B >> [u/x] in T[inl(u)/z]
* v:B, e=inr(v) in A|B >> [v/y] in T[inr(v)/z]

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

* computation

. H >> decide(inl(a);x.;y.) = t in T by reduce 1
* >> [a/x] = t in T

. H >> decide(inr(b);x.;y.) = t in T by reduce 1
* >> [b/y] = t in T

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