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.