# The Book

*Implementing Mathematics with The Nuprl Proof Development System*

- Semantics

- The Type System in Detail

- The Rules
- The Form of a Rule
- Organization of the Rules
- Specifying a Rule
- Optional Parameters and Defaults
- Hidden Assumptions
- Shortcuts in the Presentation

- ATOM
- VOID
- INT
- LESS
- LIST
- UNION
- FUNCTION
- PRODUCT
- QUOTIENT
- SET
- EQUALITY
- UNIVERSE
- MISCELLANEOUS
- ML Constructors
- ATOM
- VOID
- INT
- LESS
- LIST
- UNION
- FUNCTION
- PRODUCT
- QUOTIENT
- SET
- EQUALITY
- UNIVERSE
- MISCELLANEOUS

# The Rules

#

Semantics

The Nuprl semantics is a variation on that given by Martin-Löf for
his type theory [Martin-Löf 82]. There are three stages in the semantic specification:
the
*computation system*,
the *type system* and
the so-called *judgement forms*. Here
is how we shall proceed.
We shall specify a computation system consisting of *terms*,
divided
into *canonical* and
*noncanonical*, and a procedure for
*evaluating*
terms which for a given term returns at most one canonical term,
called the *value* of .
In Nuprl
whether a term is canonical depends only on the
outermost form of the term, and there are terms which
have no value.
We shall write
to mean that has value .

Next we shall specify a system of types. A *type* is a term (of the
computation system) with which is associated a transitive, symmetric
relation, , which respects evaluation in and ;
that is, if is a type and
and
, then if and only if .
We shall sometimes say `` type'' to mean that is a type.
We say is a *member* of , or , if .
Note that is an equivalence relation (in and )
when restricted to members of .^{8.1}Actually, is a three-place relation on terms which respects evaluation
in all three places. We also use a transitive, symmetric relation on
terms, , called *type equality*,
which respects in ; that is,
if then if and only if .
The relation respects evaluation in and ,
and is a type if and only if .
The restriction of to types is an equivalence relation.

For our purposes, then, a type system for a given computation system consists of a two-place relation and a three-place relation on terms such that

is transitive and symmetric;We define `` type'' and ``'' by

if and only if & ;

is transitive and symmetric in and ;

if and only if & ;

if ;

if & .

type if and only if ;

if and only if .

Finally, so-called judgements will be explained. This requires
consideration of terms with free variables
because substitution of closed
terms for free variables is central to judgements as presented
here.
In the description of semantics given so far
``term'' has meant a closed term, i.e., a term with no free variables.
There is only one form of judgement in Nuprl,
`:,,: » [ext ]`,
which in the case that is means .
The explanation of the cases in which is not must wait.

## Substitution

For the purposes of giving the procedure for evaluation and explaining the semantics of judgements, we would only need to consider substitution of closed terms for free variables and hence would not need to consider simultaneous substitution or capture. However, for the purpose of specifying inference rules later we shall want to have simultaneous substitution of terms with free variables for free variables. The result of such a substitution is indicated thus:where , are variables (not necessarily distinct) and are terms. It is handy to permit multiple occurrences of the same variable among the targets for replacements, all but the last of which are ignored. is the result of replacing each free occurrence of in by for , where is with the greatest such that is .

## The Computation System

Figure 8.1 shows the terms of Nuprl. Variables are terms, although since they are not closed they are not executable. Variables are written as identifiers, with distinct identifiers indicating distinct variables.^{8.2}Nonnegative integers are written in standard decimal notation. There is no way to write a negative integer in Nuprl; the best one can do is to write a noncanonical term, such as

`-5`, which evaluates to a negative integer. Atom constants are written as character strings enclosed in double quotes, with distinct strings indicating distinct atom constants.

The free occurrences of a variable
in a term are the occurrences
of which either *are* or are free in the immediate subterms of ,
excepting those occurrences of which become *bound*
in . In figure 8.1
the variables written below the terms indicate which variable
occurrences become bound; some examples are explained below.

- In
`:#`the in front of the colon becomes bound and any free occurrences of in become bound. The free occurrences of variables in`:#`are all the free occurrences of variables in and all the free occurrences of variables in except for . - In
`<,>`no variable occurrences become bound; hence, the free occurrences of variables in`<,>`are those of and those of . - In
`spread(;,.)`the and in front of the dot and any free occurrences of or in become bound.

Parentheses may be used freely around terms and often must be used to resolve ambiguous notations correctly. Figure 8.2 gives the relative precedences and associativities of Nuprl operators.

The closed terms above the dotted line in figure 8.1 are the
canonical terms, while the closed terms below it
are the noncanonical terms. Note that
carets appear below most of the noncanonical forms; these indicate the
*principal argument places* of those
terms. This notion is used in the
evaluation procedure below. Certain terms are
designated as *redices*, and each redex has a
unique *contractum*.
Figure 8.3 shows all redices and their contracta.

The evaluation procedure is as follows. Given a (closed) term ,

- If is canonical then the procedure terminates with result .
- Otherwise, execute the evaluation procedure on each principal argument of , and if each has a value, replace the principal arguments of by their respective values; call this term .
- If is a redex then the procedure for evaluating is continued by evaluating the contractum of .
- If is not a redex then the procedure is terminated without result; has no value.

## The Type System

For convenience we shall extend the relation to possibly open terms. If or contain free variables then does not hold; otherwise, it is true if and only if has value . Also, define to mean that and .
Recall that the members of a type are its canonical members and the
terms which have those members as values. The integers
are the canonical members of
the type `int`. The denumerably
many atom constants are the canonical members of the type `atom`.
The type `void` is empty. The type `|` is like a disjoint
union of types and .
The terms `inl()` and `inr()` are canonical members so long as
and ; and need not be canonical.
(The operator names `inl`
and `inr`
are mnemonic for ``inject left'' and
``inject right''.) The canonical
members of `:#` are the terms `<,>` with and ,
and not necessarily canonical. Note that the type from which the
second component is selected may depend on the value of the first
component.
The canonical members of the type ` list` represent lists of members of .
The empty list is represented by `nil`. A
nonempty list with head is
represented by `.`, where evaluates to a member of the type ` list`
and represents the tail.

A term of the form `()` is called an
*application* of to ,
and is called its *argument*.
The members of `:->` are called *functions*,
and each
canonical member is a *lambda term*,
`\`

`.`,
whose application to any is a member of .
It is required that applications to equal members of type
be equal.
Clearly, `()` if `:->` and .

The significance of some constructors derives from the representation
of propositions as types.
A proposition represented by a type is true if and only if the type
is inhabited. The type `<` is inhabited
if and only if the value of is less than the value of .
The type `(= in )` is inhabited if and only if .
Obviously, the type `(= in )` is inhabited if and only if ,
so ``` in `'' has been adopted as a notation for this type.
The members of `{:|}` are the
members of such that is inhabited.
Types of the form `{:|}` are called
*set types*.
The set constructor provides a device for specifying subtypes;
for example, `{x:int|0<x}` has just the positive integers
as canonical members.

The members of `,://` are the members of .
The difference between this type and is equality.
`,://` if and only if and are members
of and is inhabited.
Types of this form are called *quotient types*.
The relation
is an equivalence relation
over in and ;
this is built into the criteria for `,://` being a type.

Now consider equality on the other types already discussed.
(Recall that
terms are equal in a given type if and only if they evaluate to canonical
terms equal in that type.
Recall also that is an equivalence relation
in and when restricted to members of .)
Members of `int` are equal
(in `int`) if and only if they have the same value.
The same goes for type `atom`.
Canonical members of `|` (`:#`, ` list`) are
equal if and only if they have the same outermost operator and their
corresponding immediate subterms are equal (in the corresponding types).
Members of `:->` are equal if and only if their applications
to any member of are equal in .
We say equality on `:->` is *extensional*.
The types `<` and `(= in )` have
at most one canonical member, `axiom`.
Equality in `{:|}` is just the
restriction of equality in to `{:|}`.

We must now consider the notion of *functionality*.
A term is *type-functional in* if and only if
is a type and
for any and such that .
A term is *-functional in* if and only if
is type-functional in and
for any and such that
.
There are restrictions on type formation involving type-functionality.
These can be seen in the type formation clauses
of section 8.2 for `:#`,
`:->`, and `{:|}`.
In each of these must be type-functional in :.^{8.3}We may now say that the members of `:->` are the lambda terms
` \.` such that is -functional in .
In the type

`,://`, that must be type-functional in both ,: follows from the fact that

`:->:->->`must be a type. There are also constraints on the typehood of

`,://`which guarantee that the relation is an equivalence relation on members of and respects equality in . It should be noted that if is empty then every term is type-functional in its free variables over . Hence,

`:void#3`is a type (with no members) even though

`3`is not a type.

Equal types have the same membership and equality, but not conversely.
Type equality in
Nuprl is not extensional;
that is, it is not enough for type equality that two types should have
the same membership and equality. In Nuprl equal canonical types always
have the same outermost type constructor.^{8.4}The relations that must hold between the
respective immediate subterms are seen easily enough in the definition of type
equality given in section 8.2 on page .
It should be noted that in contrast to equality between types of the form
`:#` or `:->`,
much less is required for
`{:|}``{:|}` than type-functional
equality of and in :. All that is required is the existence
of functions which for each evaluate to functions
mapping back and forth between and .
Equality between quotient types is defined similarly.
If does not occur free in
then `#``:#`,
`->``:->`,
and `{|}``{:|}`;
if and do not occur free in then
`//``,://`.
As a result there is no need for clauses in the type system description
giving the criteria for `#` and the others explicitly.

Now consider the so-called *universes*,
( positive).
The members of are types. The universes are
cumulative; that is,
if is less than then membership and equality in are just
restrictions of membership and equality in .
Universe is closed
under all the type-forming operations except formation
of for greater than or equal to .
Equality (hence membership) in is similar to
type equality as defined previously
except that equality (membership) *in * is
required wherever type equality (typehood) was formerly required,
and although all universes are types, only those `U` such that is less
than are in . Equality in is the restriction
of type equality to members of .

So far the only noncanonical form explicitly
mentioned in
connection with the type system is application. We shall elaborate
here on a couple of forms, and it should then be easy to
see how to treat the others. The `spread` form is
used for computational
analysis of pairs. The pair of components is *spread* apart
so that the components can be used separately.

`spread(;,.)` if

& is type functional in :(`:#`)

&
`<``,``>`

if and

Since
then for some and
where , and .
Hence
and
have the same value, so it is enough
that
But from our hypotheses it follows that
so it is enough that
Now
since `:#` and equality respects evaluation;
therefore
in light of
's functionality in :`(:#)`.^{8.5}

The list induction form allows one to perform
inductive
analysis of lists.
`list_ind(;;,.)` is a function (in ) which
halts on all members of ` list`. It is the function (in ) defined by primitive
recursion,
where is the result for the base case of `nil` (in ` list`) and
shows how to build the value for `.` (in ` list`) from , and the value
of the function being defined on , this value being passed through during
evaluation.

if

` list`

& is type functional in :(` list`)

& `nil`

&

if &
&

Let us prove this by induction on the length of the list
represented by , all other variables universally quantified.
Suppose
. By definition we know that
`list_ind(;;,,.)`
and
have the same value,
so it is enough for the base case that ;
this is true since is functional in ` list`,
, and
.
Now suppose that for some and , `.`
, , and
.
Now

and

have the same value, so it is enough that the substitution into is in . and represents a shorter list than ; therefore, by inductive hypothesis

It follows that the substitution into is in , so it is enough that ; this holds because of 's functionality and the equality of

`.`and (in

`list`).

The `decide` form is used to discern a left from a right injection, and
to permit computation on the injected term. The `ind` form is used
to define functions recursively on integers.^{8.6}The reader is referred to chapter 2 or to the exposition of the rules for further
elaboration of the use of noncanonical forms.

## Judgements

The significance of the so-called judgements lies in the fact that they constitute the claims of a Nuprl proof. They are the units of assertion; they are the objects of inference. The judgements of Nuprl have the formwhere are distinct variables and are terms ( may be ), every free variable of is one of , and every free variable of or of is one of . The list is called the

*hypothesis list*or

*assumption list*, each

`:`is called a

*declaration*(of ), each is called a

*hypothesis*or

*assumption*, is called the

*consequent*or

*conclusion*, the

*extract term*(the reason will be seen later), and the whole thing is called a

*sequent*.

Before explaining the conditions which make a Nuprl sequent true
we shall define a relation , where is a hypothesis list and
is a list of terms,
and we shall define what it is for a sequent to be *true at*
a list of terms.

`:,,:` if and only if

&

if

We can also express this relation by saying that
every is a member of

and every is type-functional in , where means the set type

The sequent

is true at if and only if

(

&

)

if

`:,,:`

&

Equivalently, we can say that is -functional in if

:,,: . The sequent

is true if and only if

is true at

The connection between functionality and the truth of sequents lies in the fact that is type-functional (or is -functional) in if and only if is a type and for each member of , is type-functional ( is -functional) in

`{:| = in }`. Therefore, is -functional in if and only if is a type and the sequent

`: » [ext ]`is true.

^{8.7}

It is not always necessary to declare a variable with every hypothesis in a hypothesis list. If a declared variable does not occur free in the conclusion, extract term or any hypothesis, then the variable (and the colon following it) may be omitted.

In Nuprl it is not possible for the user to enter a complete
sequent directly; the extract term must be omitted.
In fact, a sequent is never displayed with its extract term.
The system has been designed so that upon completion of a proof,
the system automatically provides, or *extracts*, the extract term.
This is because in what is anticipated to be the standard mode of use,
the user tries to prove that a certain type is inhabited without
regard to the identity of any member.
One expects that in this mode the user thinks of the type
(that is to be shown inhabited) as a proposition, and that it
is merely the truth of this proposition that the user wants to show.
When one does wish to show explicitly that or that ,
one instead shows the type `( = in )` or the type
`( in )` to be inhabited.^{8.8}

Also, the system can often extract a term from an incomplete proof when the extraction is independent of
the extract terms of any unproven claims within the proof body.
Of course, such unproven claims may still
contribute to the truth of the proof's main claim.
For example, it is possible to provide an incomplete proof of
the untrue sequent `» 1<1 [ext axiom]`, the extract term `axiom`
being provided automatically.

Although the term extracted from a proof of a sequent is not displayed in the sequent, the term is accessible by other means through the name assigned to the proof in the user's library. It should be noted that in the current system proofs named in the user's library cannot be proofs of sequents with hypotheses.

# The Type System in Detail

This section may be skipped on the first reading, as the informal description of the type system given in section 8.1 should meet the needs of most readers.This section consists of two parts. First, we give the formal definition of Nuprl's type system by means of a recursive definition of the necessary predicates. Then, for ease of understanding and reference, from the definition we extract criteria for typehood and membership. Those who do read this section may benefit by reading the latter part first.

##

Formal Definition of Equality

What follows is a recursive definition of four predicates--
type, , and --on possibly
open terms.
When restricted to closed terms these are just the
predicates which constitute the Nuprl type system.^{8.9}In the clauses below,

range over possibly open terms,

range over variables;

range over positive integers;

range over integers;

ranges over atom constants.

type iff

iff

iff `void`
or `atom`
or `int`

or
`(= in )`
& `(= in )`

& & &

or
`(<)`
& `(<)`
& `int` & `int`

or
` list`
& ` list`
&

or
`|`
& `|`
& &

or
( `:#`
or `#`
)

& ( `:#`
or `#`
)

& &
if

or
( `:->`
or `->`
)

& ( `:->`
or `->`
)

& &
if

or

( `{:|}`
or `{|}`
)

& ( `{:|}`
or `{|}`
)

& & occurs in neither nor

& `:->->`

& `:->->`

or

( `,://`
or `//`
)

& ( `,://`
or `//`
)

&

& are distinct and occur in neither nor

& `:->:->->`

& `:->:->->`

& `:->`

& `:->:->->`

& `:->:->:->->->
`

or

`U`

if &

not

`void`

`atom`iff

`int`iff

`(= in )`iff

`axiom`&

`<`iff

`axiom`& & & is less than

`list`iff

`list`type

&

`nil`or

`(.)`&

`(.)`

& &

`list`

`|`iff

`|`type

& (

`inl()`&

`inl()`& )

or

`inr()`&

`inr()`&

`:#`iff

`:#`type

&

`<,>`&

`<,>`

& &

`:->`iff

`:->`type

&

`\`

`.`&

`\`

`.`

&

if

`{:|}`iff

`{:|}`type & &

`,://`iff

`,://`type & &

&

`U`iff

`void`or

`atom`or

`int`

or

`(= in )`&

`(= in )`

&

`U`& &

or

`(<)`&

`(<)`

&

`int`&

`int`

or

`list`&

`list`&

`U`

or

`|`&

`|`

&

`U`&

`U`

or (

`:#`or

`#`)

& (

`:#`or

`#`)

&

`U`

&

`U`if

or (

`:->`or

`->`)

& (

`:->`or

`->`)

&

`U`

&

`U`if

or

(

`{:|}`or

`{|}`)

& (

`{:|}`or

`{|}`)

&

`U`

&

`U`if

&

`U`if

& occurs in neither nor

&

`:->->`

&

`:->->`

or

(

`,://`or

`//`)

& (

`,://`or

`//`)

&

`U`

&

`U`if &

&

`U`if &

& are distinct and occur in neither nor

&

`:->:->->`

&

`:->:->->`

&

`:->`

&

`:->:->->`

&

`:->:->:->->->`

or

`U`& is less than

## Typehood and Membership

What follows is*not*a definition but a body of facts easily derived from the definition above.

type iff

`void`or

`atom`or

`int`

or

`(= in )`& &

or

`(<)`&

`int`&

`int`

or

`list`& type

or

`|`& type & type

or (

`:#`or

`#`)

& type & if

or (

`:->`or

`->`)

& type & if

or (

`{:|}`or

`{|}`)

& type & if

or

(

`,://`or

`//`)

& type

& are distinct and don't occur in

&

`:->`

&

`:->:->->`

&

`:->:->:->->->`

or

`U`

if &

not

`void`

`atom`iff

`int`iff

`(= in )`iff

`axiom`&

`<`iff

`axiom`& & & is less than

`list`iff

`list`type

&

`nil`or

`(.)`& &

`list`

`|`iff

`|`type

& (

`inl()`& ) or

`inr()`&

`:#`iff

`:#`type &

`<,>`& &

`:->`iff

`:->`type

&

`\`

`.`

&

if

`{:|}`iff

`{:|}`type & &

`,://`iff

`,://`type &

`U`iff

`void`or

`atom`or

`int`

or

`(= in )`&

`U`& &

or

`(<)`&

`int`&

`int`

or

`list`&

`U`

or

`|`&

`U`&

`U`

or (

`:#`or

`#`)

&

`U`&

`U`if

or (

`:->`or

`->`)

&

`U`&

`U`if

or (

`{:|}`or

`{|}`)

&

`U`&

`U`if

or

(

`,://`or

`//`)

&

`U`

&

`U`

if &

& are distinct and don't occur in

&

`:->`

&

`:->:->->`

&

`:->:->:->->->`

or

`U`& is less than

# The Rules

The
Nuprl system has been designed to accommodate the
top-down construction of proofs by
refinement.
In this style one proves a judgement (i.e., a *goal*) by applying
a *refinement rule*, thereby obtaining a set of
judgements called *subgoals*,
and then proving each of the subgoals.
The mechanics of using the proof-editing system were discussed in
chapter 7.
In this section we will describe the refinement rules themselves.
First we give some general comments regarding the rules and then proceed to
give a description of each rule.

## The Form of a Rule

To accommodate the top-down style of the Nuprl system the rules of the logic are presented in the following*refinement*style.

`» ext by`

» ext

» ext

» ext

» ext

The goal is shown at the top, and each subgoal is shown indented underneath. The rules are defined so that if every subgoal is true then one can show the truth of the goal, where the truth of a judgement is to be understood as defined in section 8.1. If there are no subgoals () then the truth of the goal is axiomatic.

One of the features of the proof editor is that
the extraction terms are not
displayed and indeed are not immediately available.
The idea is that one can judge a term to be a type and to be
inhabited without explicitly presenting the inhabiting object.
When one is viewing as a proposition this is convenient, as a
proposition is true if it is inhabited.
If is being viewed as a specification this allows one to
implicitly
build a program which is guaranteed to be correct for the specification.
The extraction term for a goal is built as a function of the extraction
terms of the subgoals and thus in general cannot be built until each of
the subgoals have been proved.
If one has a specific term, , in mind as the inhabiting object and wants
it displayed, one can use the explicit intro rule and then show that the
type ` in ` is inhabited.
The rules have the property that each subgoal can be constructed from the
information in the rule and from the goal, exclusive of the extraction term.
As a result some of the more complicated rules require certain terms as
parameters.

Implicit in showing a judgement to be true is showing that the conclusion of
the judgement is in fact a type.
We cannot directly judge a term to be a type; rather, we show that it
inhabits a universe.
An examination of the semantic definition will reveal that this is
sufficient for our purposes.
Due to the rich type structure of the system it is not possible in general
to decide algorithmically if a given term denotes an element of a universe,
so this is something which will require proof.
The logic has been arranged so the proof that the conclusion of a goal
is a type can be conducted simultaneously with the proof that the type is
inhabited.
In many cases this causes no great overhead,
but some rules have subgoals whose only purpose is to establish that the
goal is a type, that is, that it is *well-formed*.
These subgoals all have the form ` » in ` and are referred
to as *well-formedness* subgoals.

## Organization of the Rules

The rules for reasoning about each type and objects of the type will be presented in separate sections. Recall from above that for each judgement of the form`» ext`where the inhabiting object is left implicit, there is a corresponding explicit judgement

`» in ext axiom`. As the content of these judgements is essentially the same, the rules for reasoning about them will be presented together. In the preceding chapters, the rules have been classified mainly as introduction or elimination rules, where the introduction rules break down the form of the conclusion of a goal, and the elimination rules use a hypothesis. This is too coarse a classification for the purposes of this section, as the large majority of the rules are introduction rules. Here we will use different criteria for classifying the rules which will hopefully be more illuminating. For each type we will have the following categories of rules:

*Formation*

These rules give the conditions under which a canonical type may be judged to inhabit a universe, thus verifying that it is indeed a type.*Canonical*

These rules give the conditions under which a canonical object (implicitly or explicitly presented) may be judged to inhabit a canonical type. Note that the formation rules are all actually canonical rules, but it is convenient to separate them.*Noncanonical*

These rules give the conditions under which a noncanonical object may be judged to inhabit a type. The elimination rules all fall in this category, as the extract term for an elimination rule is a noncanonical term.*Equality*

These rules give the conditions under which objects having the same outer form may be judged to be equal. Recall that the rules are being presented in implicit/explicit pairs,`» ext`and`» in`. The explicit judgement`» in`is simply the reflexive instance of the general equality judgement`» = in`, and in most cases the rule for the general form is an obvious generalization of the rule for the reflexive form, and thus will be omitted. As the rules for the reflexive judgement are given in one of the other categories, there will be no equality rules presented for some types.*Computation*

These rules allow one to make judgements of equalities resulting from computation.

Rules such as the *sequence*, *hypothesis* and *lemma* rules
which are not associated with one particular type are grouped together under
the heading "miscellaneous".

## Specifying a Rule

In the context of a particular goal a rule is specified by giving a name and, possibly, certain parameters. As there are a large number of rules it would be unfortunate to have to remember a unique name for each one. Instead, there are small number of generic names, and the proof editor infers the specific rule desired from the form of the goal. In fact, for the rules dealing with specific types or objects of specific types, there are only the names*intro*,

*elim*and

*reduce*. The

*intro*rules are those which break down the conclusion of the goal, and the

*elim*rules are those which use a hypothesis. Accordingly, the first parameter of any elim rule is the declared variable or number of the hypothesis to be used. The

*reduce*rules are the computation rules. The first parameter of a reduce rule is a number that specifies which term of the equality is to be reduced. Among the parameters of some rules are keyword parameters which have the following form:

`new`

This parameter is used to give new names for hypotheses in the subgoals. In most cases the defaults, which are derived from subterms of the conclusion of the goal, suffice. For technical reasons the same variable can be declared at most once in a hypothesis list, so if a default name is already declared a new name will have to be given. Whenever this parameter is used it must be the case that the names given are all distinct and do not occur in the hypothesis list of the goal.`using`,`over`

These parameters are used when judging the equality of noncanonical forms in types dependent on the principal argument of the noncanonical form. The`using`parameter specifies the type of the principal argument of the noncanonical form. The value should be a canonical type which is appropriate for the particular noncanonical form. The`over`parameter specifies the dependence of the type over which the equality is being judged on the principal argument of the form. Each occurrence of in indicates such a dependency. The proof editor always checks that the term obtained by substituting the principal argument for in is -convertible to the type of the equality judgement.`at`

The value of this parameter is the universe level at which any type judgements in the subgoals are to be made. The default is .

## Optional Parameters and Defaults

Each rule will be presented in its most general form. However, some of the parameters of a rule may be optional, in which case they will be enclosed by square brackets (`[]`). If a new hypothesis in a subgoal depends on an optional parameter, and in a particular instance of the rule the optional parameter is not given, that new hypothesis will not be added. Such a dependence is usually in the form of a hypothesis specifically referring to an optional

`new`name. The

`over`parameter discussed above is almost always optional. If it is not given, it is assumed that the type of the equality has no dependence on the principal argument of the noncanonical form.

The issue of default values for variable names arises when the main term of a goal's conclusion contains binding variables. In general, the default values are taken to be those binding variables. For example, the rule for explicitly showing a product to be in a universe is

` » :# in by intro [new y]
» in
: » in `

The rule is presented as if a new name is given, but the default is to use . All the dependent types follow this general pattern.

For judging the equality of terms containing binding variables the binding variables of the first term are in general the default values for the ``appropriate'' new hypotheses. Consider the rule for showing that a spread term is in a type:

` » spread(;) in [/]
by intro [over ] using :# [new ]
» in :#
,:,:[/] »
[/] in [<,>/]`

Here the new variables default to . If no new names are given and and don't appear in , then the second subgoal will be

` ,:,: » in [<,>/]`

Again this is the general pattern for rules of this type.

## Hidden Assumptions

For certain rules, we need to be able to control the free variables occuring in the extract term. The mechanism used to achieve this is that of*hidden*hypotheses. A hypothesis is hidden when it is displayed enclosed in square brackets. At the moment the only place where such hypotheses are added is in a subgoal of the set elim rule. The intended meaning of a hypothesis being hidden is that the name of the hypothesis cannot appear free in the extracted term; that is, that it cannot be used computationally. Accordingly, a hidden hypothesis cannot be the object of an

`elim`or

`hyp`rule. For the rules for which the extract term is the trivial term

`axiom`, the extract term contains no free variable references and so all restrictions on the use of hidden hypotheses can be removed. The editor will remove the brackets from any hidden hypotheses in displaying a goal of this form.

## Shortcuts in the Presentation

With the exception of one of the direct computation rules, each of the rules has the property that the list of hypotheses in a subgoal is an extension of the hypothesis list of the goal. To highlight the new hypotheses and to save space, we will show only the new hypotheses in the subgoals. Also, we will not explicitly display trivial extraction terms, that is, extraction terms which are just`axiom`.

# ATOM

## formation

1.` » ext atom by intro atom
`

2.` » atom in by intro
`

## canonical

3.`» atom ext`

`"`

`"`

by intro `"`

`"`

4.` » "" in atom by intro
`

`
`5.

`» atom_eq(;;;) in by intro`

» in atom

» in atom

= in atom » in

(= in atom)->void » in

» in atom

» in atom

= in atom » in

(= in atom)->void » in

## computation

6a.`» atom_eq(;;;)= in by reduce 1`

» = inwhere is a canonical token term.

» = in

6b.` » atom_eq(;;;)= in by reduce 1
» = in
`

where and are different canonical token terms.

# VOID

## formation

1.`» ext void by intro void`

2.` » void in by intro
`

## noncanonical

3.`,:void » ext any() by elim`

4.` » any() in by intro
» in void
`

# INT

## formation

1.`» ext int by intro int`

2.` » int in by intro
`

## canonical

3.`» int ext by intro`

4.` » in int by intro
`

`where must be an integer constant.`

## noncanonical

5.`» - in int`

» in int

» in int

6.` » int ext by intro
» int ext
» int ext
`

`7. » in int by intro
`

» in int

» in int

`where must be one of`

`+,-,*,/,`or`mod`.
8.`,:int, »
ext ind(;.;;.)
by elim new [,]
:int,<0,:[+1/]
» [/] ext
» [0/] ext
:int,0<,:[-1/]
» [/] ext
`

`The optional`

`new`name must be given if occurs free in .
9.` » ind(;,.;;,.) in
by intro [over .] [new ,]
» in int
:int,<0,:
» in
» in
:int,0<,:
» in
`

10.` » int_eq(;;;) in by intro
» in int
» in int
= in int » in
(= in int)->void » in
`

`
11. » less(;;;) in by intro
`

» in int

» in int

< » in

(<)->void » in

## computation

12a.`» ind(;,.;;,.) = in by reduce 1 down`

» [,(ind(+1;,.;;,.))/,] = in

» <0

» [,(ind(+1;,.;;,.))/,] = in

» <0

`12b. » ind(;,./;;,.) = in
by reduce 1 base
`

» = in

» = 0 in int

`
12c. » ind(;,.;;,.) = in
by reduce 1 up
`

» [,(ind(-1;,.;;,.))/,] = in

» 0<

`
13a. » int_eq(;;;) = in by reduce 1
`

» = in

`
13b. » int_eq(;;;) = in by reduce 1
`

» = in

`
where and are canonical int terms, and .
`

14a.` » less(;;;) = in by reduce 1
» = in
`

where and are canonical `int` terms such that .

14b.` » less(;;;) = in by reduce 1
» = in
`

where and are canonical `int` terms such that .

# LESS

## formation

1.`» ext < by intro less`

» int ext

» int ext

» int ext

» int ext

2.` » < in by intro
» in int
» in int
`

## equality

3.`» axiom in <`

» <

» <

# LIST

## formation

1.`» ext list by intro list`

» ext

» ext

2.` » list in by intro
» in
`

## canonical

3.`» list ext nil by intro nil at`

» in

» in

4.` » nil in list by intro at
» in
`

5.` » list ext . by intro .
» ext
» list ext
`

6.` » in list by intro
» in
» in list
`

## noncanonical

7.`,: list, » T ext list_ind(;;.)`

by elim new ,[,]

» [nil/] ext

:,: list,:[/] » [/] ext

by elim new ,[,]

» [nil/] ext

:,: list,:[/] » [/] ext

8.` » list_ind(;;) in [/]
by intro [over ] using list [new u,v,w]
» in list
» in [nil/]
:,: list,:[/]
» [/] in
[./]
`

## computation

9a.`» list_ind(nil;;) = in by reduce 1`

» = in

» = in

9b.` » list_ind(;;) = in by reduce 1
» [list_ind(;;)/]
= in
`

# UNION

## formation

1.`» ext | by intro union`

» ext

» ext

» ext

» ext

2.` » | in by intro
» in
» in
`

## canonical

3.`» | ext inl() by intro at left`

» ext

» in

» ext

» in

4.` » inl() in | by intro at
» in
» in
`

5.` » | ext inr() by intro at right
» ext
» in
`

6.` » inr() in | by intro at
» in
» in
`

## noncanonical

7.`,:|, » ext decide(;.;.) by elim [new ,] :,=inl() in | » [inl()/] ext`

:,=inr() in | » [inr()/] ext

:,=inr() in | » [inr()/] ext

8.` » decide(;.;.) in [/]
by intro [over .] using | [new u,v]
» in |
:, =inl() in | »
[/] in [inl()/]
:, =inr() in | »
[/] in [inr()/]
`

## computation

9a.`» decide(inl();.;.) = in by reduce 1`

» [/] = in

» [/] = in

9b.` » decide(inr();.;.) = in by reduce 1
» [/] = in
`

# FUNCTION

## formation

1.`» ext :-> by intro function new`

» in

: » ext

» in

: » ext

2.` » :-> in by intro [new ]
» in
: » [/] in
`

3.` » ext -> by intro function
» ext
» ext
`

4.` » -> in by intro
» in
» in
`

## canonical

5.`» :-> ext . by intro at [new ]`

: » [/] ext

» in

: » [/] ext

» in

6.` » . in :-> by intro at [new ]
: » [/] in [/]
» in
`

## noncanonical

7.`,:(:->), » ext [()/] by elim on [new ] » in`

:[/], =() in [/] » ext

:[/], =() in [/] » ext

8.`,:(:->), » ext [()/]
by elim [new ]
» ext
: » ext
`

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

9.` » () in [/] by intro using :->
» in :->
» in
`

## equality

10.`» = in :-> by extensionality [new ]`

: » () = () in [/]

» in :->

» in :->

: » () = () in [/]

» in :->

» in :->

## computation

11.`» (.)() = in by reduce 1`

» [/] = in

» [/] = in

# PRODUCT

## formation

1.`» ext :# by intro product new`

» in

: » ext

» in

: » ext

2.` » :# in by intro [new ]
» in
: » [/] in
`

3.` » ext # by intro product
» ext
» ext
`

4.` » # in by intro
» in
» in
`

## canonical

5.`» :# ext <,> by intro at [new ]`

» in

» [/] ext

: » [/] in

» in

» [/] ext

: » [/] in

6.` » <,> in :# by intro at [new ]
» in
» in [/]
: » [/] in
`

7.` » # ext <,> by intro
» ext
» ext
`

8.` » <,> in # by intro
» in
» in
`

## noncanonical

9.`,:(:#), » ext spread(;.) by elim new`

:,:[/],=<,> in :# » [<,>/] ext

:,:[/],=<,> in :# » [<,>/] ext

10.` » spread(;) in [/]
by intro [over ] using :# [new ]
» in :#
:,:[/],=<,> in :# »
[/] in [<,>/]
`

## computation

11.`» spread(<,>;) = in by reduce 1`

» [/] = in

» [/] = in

# QUOTIENT

## formation

1.`» ext (,):// by intro quotient , new ,,`

» in

:,: » in

: » [/]

:,:,[/] » [/]

:,:,:,[/], [/] » [/]

» in

:,: » in

: » [/]

:,:,[/] » [/]

:,:,:,[/], [/] » [/]

2.` » ():// in by intro new ,,
» in
:,: » [/] in
: » [/]
:,:,[/]
» [/]
:,:,:,[/], [/] » [/]
`

## canonical

3.`» ():// ext by intro at`

» ():// in

» ext

» ():// in

» ext

4.` » in ():// by intro at
» ():// in
» in
`

## noncanonical

5.`,:()://, » = in by elim at [new ]`

:,: » [/] in

» in

:,:,[/] »

[/] = [/] in [/]

:,: » [/] in

» in

:,:,[/] »

[/] = [/] in [/]

## equality

6.`» ():// = ():// in by intro [new ]`

» ():// in

» ():// in

» = in

= in ,:,: » [/] -> [/]

= in ,:,: » [/] -> [/]

» ():// in

» ():// in

» = in

= in ,:,: » [/] -> [/]

= in ,:,: » [/] -> [/]

7.` » = in ():// by intro at
» ():// in
» in
» in
» [/]
`

# SET

## formation

< 1.`» ext :| by intro set new`

» in

: » ext

» in

: » ext

2.` » :| in by intro [new y]
» in
: » [/] in
`

3.` » ext | by intro set
» ext
» ext
`

4.` » | in by intro
» in
» in
`

## canonical

5.`» :| ext by intro at [new ]`

» in

» [/] ext

: » [/] in

» in

» [/] ext

: » [/] in

All hidden hypothesis in become unhidden in the second subgoal.

6.` » in :| by intro at [new ]
» in
» [/]
: » [/] in
`

7.` » | ext by intro
» ext
» ext
`

8.` » in | by intro
» in
» ext
`

## noncanonical

9.`,::|, » ext (.)() by elim at [new ]`

: » [/] in

:,[[/]],= in » [/] ext

: » [/] in

:,[[/]],= in » [/] ext

Note that the second new hypotheses of the second subgoal is hidden.

## equality

10.`» :| = :| in by intro [new ]`

» = in

: » [/] -> [/]

: » [/] -> [/]

» = in

: » [/] -> [/]

: » [/] -> [/]

# EQUALITY

## formation

1.`» ext == in by intro equality`

» in

» ext

» ext

» in

» ext

» ext

The default for is 1.

2.` » (== in ) in by intro
» in
» in
» in
`

## canonical

3.`» axiom in ( in ) by intro`

» in

» in

4.`,:, » in by intro
`

This rule doesn't work when T is a set or quotient term,
since intro will invoke the equality rule for the set or quotient type,
respectively.
In any case, the `equality` rule can be used.

# UNIVERSE

## canonical

1.`» ext by intro universe`

2.` » in by intro
`

`where . Note that all the formation rules are intro rules for a universe type.`

## noncanonical

Currently there are no rules in the system for analyzing universes. At some later date such rules may be added.

# MISCELLANEOUS

## hypothesis

1.`,:, » ext by hyp`

where is -convertible to

## sequence

2.`» ext (.(.)()))()`

by seq [new ]

» ext

: » ext

:,,: » ext

by seq [new ]

» ext

: » ext

:,,: » ext

## lemma

3.`» ext [term_of()/] by lemma [new ]`

: » ext

: » ext

where is the conclusion of the complete theorem .

## def

4.`» ext by def [new ]`

:term_of() = - in » ext

:term_of() = - in » ext

where is the conclusion of the complete theorem, ,
and - is the term extracted from that theorem.
^{8.10}`
`

`
`

`explicit intro`

`5.`

`» ext by explicit intro`

» in» in

## cumulativity

6.`» in by cumulativity at`

» in

» in

where

## substitution

7.`» [/] ext by subst at = in over`

» = in

» [/] ext

: » in

» = in

» [/] ext

: » in

## direct computation

8.`» ext by compute using`

» ext

» ext

9.`, :, »
ext
by compute hyp i using
, :, » ext
`

where `:` is the hypothesis, where is
obtained from by ``tagging'' some of its subterms, and
where is generated by the system by performing some
computation steps on subterms of , as indicated by the
tags. A subterm is tagged by replacing it by
`[[*;]]` or `[[;]]`, where is a positive
integer constant. The latter tag causes to be computed
for steps, and the former causes computation to proceed
as far as possible. There are some somewhat complicated
restrictions on what subterms of may be tagged, but most
users will likely find it sufficient to know that any subterm
of may be tagged that does not occur within the scope of
a binding variable occurrence in . An application of
one of these
rules will fail if the tagging is illegal, or if removing the
tags from does not yield a term equal to . For a more
complete description of this rule, see appendix C.
Note that many of the computation rules, such as the one for product,
are instances of direct computation.

## equality

10.`» = in by equality`

where the equality of and can be deduced from assumptions that are equalities over (or equalities over where is deducible using only reflexivity, commutativity and transitivity) .

## arith

11.`» by arith at`

The `arith` rule is used to justify conclusions which follow from
hypotheses by
a restricted form of arithmetic reasoning. Roughly speaking, `arith` knows
about the ring axioms for integer multiplication and addition, the total
order axioms of , the reflexivity, symmetry and transitivity of equality, and
a limited form of substitutivity of equality. We will describe the class
of problems decidable by `arith` by giving an informal account of the
procedure which `arith` uses to decide whether or not follows from .

The terms that `arith` understands are those denoting arithmetic relations,
namely terms of the form `<`, `= in int`
or the negation of a term of this form.
As the only equalities `arith` concerns itself with are those of the form
`= in int`, we will drop the `in int` and write only
`=` in the rest of this description.
For `arith` the negation of an `arith`metic relation where
is one of or is of the form
`()->void`, which we will write as
.
As integer equality and less-than are decidable relations,
and
denote the same relation and will be treated identically by `arith`.

The `arith` rule may be used to justify goals of the form

`, , » | | `,

where each and is a term denoting an arithmetic relation.
If `arith` can justify the goal it will produce subgoals requiring the user
to show that the left- and right-hand sides of each denote integer
terms.
As a convenience `arith` will attempt to prove goals in which not all of the
are arithmetic relations; it simply ignores such disjuncts. If it is
successful on such a goal, it will produce subgoals
requiring the user to prove that each such disjunct is a type
at the level given in the invocation of the rule.

`Arith` begins by normalizing the relevant formulas of the goal according to
the following conventions:

- Rewrite each relation of the form
`as the equivalent``|`. A conclusion follows from such an assumption if it follows from either or ; hence`arith`tries both cases. Henceforth, we assume that all negations of equalities have been eliminated from consideration. - Replace all occurrences of terms which are not addition, subtraction
or multiplication by a new variable.
Multiple occurrences of the same term are replaced by the same variable.
`Arith`uses only facts about addition, subtraction and multiplication, so it treats all other terms as atomic. At this point all terms are built from integer constants and integer variables using , and . - Rewrite all terms as polynomials in canonical form. The exact nature of the canonical form is irrelevant (the reader may think of it as the form used in high school algebra texts) but has the important property that any two equal terms are identical. Each term now has the form , where and are nonconstant polynomials in canonical form, and are constants, and is one of , or ( is equivalent to ).
- Replace each nonconstant polynomial by a new variable,
with each occurrence of being replaced by the same variable.
This amounts to treating each nonconstant polynomial as an atom.
Now each formula is of the form
.
`Arith`now decides whether or not the conclusion follows from the hypotheses by using the total order axioms of , the reflexivity, symmetry, transitivity and substitutivity of , and the following so-called*trivial monotonicity*axioms ( and are constants).

For a detailed account of the `arith` rule and a proof of its correctness, see
the article by Tat-hung Chan in [Constable, Johnson, & Eichenlaub 82].

# ML Constructors

One of the features of the Nuprl system is that it comes with its own formal metalanguage, implemented in ML. Accordingly, ML needs access to the rules of the system. Following is a list of the ML rule constructors. The constructors are categorized and numbered in the same manner as the rules. For example, the constructor numbered 4 in the`atom`section corresponds to the rule numbered 4 in the

`atom`section. Each constructor is presented in the form

`constructor_name(parameter names): type`. The parameter names are never actually used but appear here solely for documentation purposes. Following are some conventions regarding the parameter names which we give with their types:

`hyp:int`is used to indicate a hypothesis.`where:int`is used to indicate which equand of an equality should be reduced in a computation rule.`level:int`is used to give a universe level.`using:term`is used to indicate a using term.`over_id:tok, over:term`are used to indicate an over term. If the`over_id`is the token``nil``, the over term is ignored.

``nil``.

Unlike the rules, each constructor needs a unique name.
The general form of the names is *base-type*_*kind*_*qualifier*, where *base-type* is a prl type and *kind* is one of
`intro`, `elim`, `equality`, `formation` or `computation`.
So, for example, `list_equality_nil` is the name of the constructor for
the rule which specifies how to show two `nil` terms are the same in a
`list` type, and `int_elim` is the name of the constructor for the elim
rule for integers.
There are some exceptions to this general pattern, the main one being that
the name of the constructor for the rule for showing two canonical type
terms to be equal in some universe is *type*`_equality` rather than
`universe_equality_`*type*.

# ATOM

## formation universe_intro_atom: rule.

atom_equality: rule.

## canonical

atom_intro(token): term rule.

atom_equality_token: rule.

## quality

atom_eq_equality: rule.

## computation

atom_eq_computation(where): int rule.# VOID

## formation

universe_intro_void: rule.void_equality: rule.

## noncanonical

void_elim(hyp): int rule.void_equality_any: rule.

# INT

## formation

universe_intro_integer: rule.int_equality: rule.

## canonical

integer_intro_integer(c): int rule.integer_equality_natural_number: rule.

## noncanonical

integer_equality_minus: rule.

integer_intro_addition: rule.

integer_intro_subtraction: rule.

integer_intro_multiplication: rule.

integer_intro_division: rule.

integer_intro_modulo: rule.

integer_equality_addition: rule.

integer_equality_subtraction: rule.

integer_equality_multiplication: rule.

integer_equality_division: rule.

integer_equality_modulo: rule.

integer_elim(hyp y z): int tok tok rule.

integer_equality_induction(over_id over u v): tok term tok tok rule.

## equality

int_eq_equality: rule.int_less_equality: rule.

## computation

integer_computation(kind where): tok int rule.where kind should be one of `UP`, `BASE` or `DOWN`.int_eq_computation(where): int rule.

int_less_computation(where): int rule.

# LESS

## formation

universe_intro_less: rule.less_equality: rule.

## equality

axiom_equality_less: rule.# LIST

## formation

universe_intro_list: rule.list_equality(level): int rule.

## canonical

list_intro_nil(level): int rule.list_equality_nil(level): int rule.

list_intro_cons: rule.

list_equality_cons: rule.

## noncanonical

list_elim (hyp u v w): int tok tok tok rule.list_equality_induction (over_id over using u v w): tok term term tok tok tok rule.

## computation

list_computation(where): int rule.# UNION

## formation

universe_intro_union: rule.union_equality: rule.

## canonical

union_intro_left(level): int rule.union_equality_inl(level): int rule.

union_intro_right(level): int rule.

union_equality_inr(level): int rule.

## noncanonical

union_elim(hyp x y): int tok tok rule.union_equality_decide(over_id over using u v): tok term term tok tok rule.

## computation

union_computation(where): int rule.# FUNCTION

## formation

universe_intro_function(x term): tok term rule.function_equality(y): tok rule.

universe_intro_function_independent: rule.

function_equality_independent: rule.

## canonical

function_intro(level y): int tok rule.function_equality_lambda(level z): int tok rule.

## noncanonical

function_elim(hyp on y): int term tok rule.function_elim_independent(hyp y): int tok rule.

function_equality_apply(using): term rule.

## equality

extensionality(y): tok rule.

## computation

function_computation(where): int rule.# PRODUCT

## formation

universe_intro_product(x left_term): tok term rule.product_equality(y): tok rule.

universe_intro_product_independent: rule.

product_equality_independent: rule.

## canonical

product_intro_dependent(left_term level y): term int tok rule.product_equality_pair(level y): int tok rule.

product_intro: rule.

product_equality_pair_independent: rule.

## noncanonical

product_elim(hyp u v): int tok tok rule.product_equality_spread(over_id over using u v): tok term term tok tok rule.

## computation

product_computation(where): int rule.# QUOTIENT

## formation

universe_intro_quotient(A E x y z): term term tok tok tok rule.quotient_formation(x y z): tok tok tok rule.

## canonical

quotient_intro(level): int rule.quotient_equality_element(level): int rule.

## noncanonical

quotient_elim (hyp level v w): int int tok tok rule.

## equality

quotient_equality(r s): tok tok rule.quotient_equality_element(level): int rule.

# SET

## formation

universe_intro_set(x type): tok term rule.set_formation(y): tok rule.

universe_intro_set_independent: rule.

set_formation_independent: rule.

## 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.

## noncanonical

set_elim(hyp level y): int int tok rule.

## equality

set_equality(z): tok rule.# EQUALITY

## formation

universe_intro_equality(type number_terms): term int rule.equal_equality: rule.

## canonical

axiom_equality_equal: rule.equal_equality_variable: rule.

# UNIVERSE

## canonical

universe_intro_universe (level): int rule.universe_equality: rule.

# MISCELLANEOUS

## hypothesis

hyp(hyp): int rule.

## sequence

seq(term_list id_list): (term list) (tok list) rule.where the length of the token list should match the length of the term list.

## lemma

lemma(lemma_name x): tok tok rule.

## def

def(theorem x): tok tok rule.

## explicit intro

explicit_intro(term): term rule.

## cumulativity

cumulativity(level): int rule.

## substitution

substitution(level equality_term over_id over): int term tok term rule.

## direct computation

direct_computation(tagged_term): term rule.direct_computation_hyp(hyp tagged_term): int term rule.

## equality

equality: rule.

## arith

arith(level): int rule.#### Footnotes

- ....
^{8.1} - There is a similarity between a type
and Bishop's notion of
*set*. Bishop [Bishop 67] says that to give a set, one gives a way to construct its members and gives an equivalence relation, called the*equality*on that set, on the members. - ... variables.
^{8.2} -
An identifier is any string of letters, digits, underscores or
at-signs that starts with a letter.
The only identifiers which cannot be used for variables are
`term_of`and those which serve as operator names, such as`int`or`spread`. - ....
^{8.3} - In the formation of these as members of , must be -functional in :.
- ... constructor.
^{8.4} - modulo the difference between
`#`and`:#`, etc. `... CLASS="MATH">)`.^{8.5}- If the reader finds this a bit difficult to follow, perhaps it would help to consider first the case in which is not free in and is not free in and then the more general cases afterward.
- ... integers.
^{8.6} -
This is defined by primitive recursion with
`0`as the base case and an induction step for each direction out (positive and negative). Of course, in a higher-order system such as Nuprl, where functions can take functions as arguments and have functions as values, one can define by primitive recursion functions in`int->int`which are not primitive recursive. - ... true.
^{8.7} - If we were to give a similar semantic account of the judgements of [Martin-Löf 82], the plainest difference between the truth conditions for those judgements and Nuprl judgements would be that the truth of the former requires type-functionality of each assumption in all its variables.
- ... inhabited.
^{8.8} -
Recall that the term
`( = in )`is a type whenever and and is inhabited just when . As a special case, the term`( in )`is a type and is inhabited just when . - ... system.
^{8.9} - It turns out that these predicates will hold only for closed terms.
- ... theorem.
^{8.10} - This rule introduces very strong interproof dependencies. A proof using this rule depends not only on but also on the way is proved.