Notation and Prerequisites

This paper was created as an object in the Nuprl library. All the lemmas and theorems quoted in this paper, in fact, everything that appears in typewriter font is the display form of a Nuprl term. The careful reader will notice that some of our definitions use parameters that are not shown in their display form. In such cases, we have chosen a display form for the term that suppresses a parameter because we think the parameter will be clear from context. In a session with the Nuprl system, a user can always use an alternate display form that shows all the parameters, but for this printed document we have chosen the forms that seem most readable without loss of information. We have actually left more parameters exposed than necessary; many of the definitions that we will present have a parameter E that is an event structure and is displayed as a subscript. In all of our theorems, there is only one relevant event structure E, so we could have supressed the parameter E in the display of terms that mention it.

Our logical notation is standard, so only one comment on logical notation is called for. When stating the theorem that propositions A,B, and C imply proposition D, we write

rather than

We do this because, in constructive logic, every theorem has an extract and the extract of the first form is a Curried function while the extract of the second form is uncurried. Our tactics work best on the Curried form. In the proofs given in this paper (which are English summaries of the Nuprl proofs), we will refer to D as ``the conclusion'' and to B as ``the second hypothesis''.

The type theory prerequisites are minimal. We will mention only that Nuprl type theory includes intersection types and void types, and this lets us define the type Top by:

The only thing we need to know about this type is that every type T is a subtype of Top. In our treatment of structures, we use the dependent product type

We will also remind readers that in constructive type theory, propositions are types, not booleans , and that we have P (P) only for decidable propositions. For this paper, we can mostly ignore this distinction because whenever we need to know that a proposition is decidable, Nuprl's Auto-tactic can prove it for us.

We will use a number of operations on lists and will use facts about them without proof. The real Nuprl proofs come from an extensive list-theory library. Here, we will merely show the notations we use for list operations. In a list type T List, we have nil and cons constructors, [] and [a / L], and lists built by cons-ing to nil will display like [x; y; z]. The length and append functions are ||L|| and L$_{1}$ @ L$_{2}$. The type ||L|| of natural numbers less than the length of L is the domain of the selection function L[i]. The prefix, or initial-segment, relation is written L$_{1}$ L$_{2}$. The filter operation forms lists like <xL | P x>, the list obtained by swapping the elements of L at indices i and j is swap(L;i;j) and we define the swap adjacent relation on lists by:

Notice that, as in the lefthand side of this definition, we like to use infix notation for the application of a relation.