Next: EQUALITY Up: The Rules Previous: QUOTIENT

SET

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

* formation universe_intro_set(x type): tok

term

rule.

set_formation(y): tok rule.

universe_intro_set_independent: rule.

set_formation_independent: rule.

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

* canonical set_intro(level left_term y): int

term

tok

rule.

set_equality_element(level y): int tok rule.

set_intro_independent: rule.

set_equality_element: rule.

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

* noncanonical set_elim(hyp level y): int

int

tok

rule.

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

* equality set_equality(z): tok

rule.

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