An Inconsistent Proof Step Enumeration
Below is a fragment of a proof that uses an inconsistent numbering scheme for proof steps.

 We show that R is preserved by all operations in . We use 1. quantifier elimination, 2. case analysis, 3. implication elimination, 4. conjunction elimination, 5. lemma introduction, and 6. reduction to show that ( I1,I2,N : Nat, A1,A2 : Arr)         (I1 || A1) R (I2 || A2)   implies                 pop(I1 || A1)  R   pop(I2 || A2)   and                 push(N, I1 || A1)  R  push(N, I2 || A2) . This involves the following steps:     1.  introduce new constants i1, i2, n of sort Nat, and a1, a2 of sort Arr ;     2. 3. 4. 6.  in case that i1 = 0 ;                     assume i2 = 0, then show                             pop(0 || a1)  R  top(i2 || a2) = true and                             push(n, 0 || a1)  R  push(n, i2 || a2) = true,                     separately by reduction.     2. 3. 4. 5. 6.  in case that i1 = s i for some i of sort Nat ;                         assume                                 s i = i2,                                 a1[i] = a2[i], and                                 (i || a1) R (i || a2),                         then show                                 pop(s i || a1)  R  pop(i2 || a2) = true                         by reduction, and introduce the lemma ( I, I1, I2: Nat, A : Arr) I1 <= I2         implies   I1 || put(I, I2, A) = I1 || A .                         to show                                 push(n, s i || a1)  R   push(n, i2 || a2) = true,                         by reduction.

To UCSZ homepage.
To Tatami project homepage.
To UCSD Meaning and Computation Lab homepage.
To my homepage.
10 January 1998; version of 24 January 2000.