Proof Verification Steps
( Adapted from metamath.pdf and output of mmverify.py at www.metamath.org)
  1. A proof is scanned in order of its label sequence.
  2. If the label refers to an active hypothesis, the expression in the hypothesis is pushed onto a stack called the "Proof Work Stack. In the table diagrams below the Proof Work Stack is represented with the most recently added stack item at the bottom and the oldest item at the top (the terminology "push onto a stack" is unfortunate in some ways because programmers most frequently store stack upside down and ADD to the bottom -- this is so that the existing stack items do not need to be shifted down to make room on the "top").
  3. If the label refers to an assertion that has no hypotheses, the assertion is pushed onto the Proof Work Stack. (For example, see "con0 $a class On $." in set.mm, which is an assertion with no hypotheses -- essentially it gives the constant 'On' a type = 'class').
  4. If the label refers to an assertion with hypotheses, a (unique) substitution must exist that, when made to the mandatory hypotheses of the referenced assertion, causes them to match the most recent entries of the Proof Work Stack. Note: "mandatory" refers to floating hypotheses for variables referenced by the assertion as well as Essential hypotheses, if any.) Assume the referenced assertion has 'n' mandatory hypotheses: these 'n' hypotheses are matched, in order of their appearance in the database, with the 'n' most recent Proof Work Stack entries in order of their position in the stack. If the Type symbol of any hypothesis does not match the Type symbol of the stack item in the corresponding position, a proof verification error is reported ('Type' refers to the 1st symbol of the assertion.) Then, if each hypothesis has a Type matching its corresponding item on the Proof Work Stack, the unique substitutions are derived to make the mandatory hypotheses match the corresponding stack entries. This is very simple derivation: for each Variable Hypothesis of the referenced assertion, the substitution is simply the corresponding Proof Work Stack item! After deriving substitutions for all of the referenced assertion's Variable Hypotheses, apply the substitutions to the referenced assertion's Logical Hypotheses, simultaneously, and verify that each resulting expression matches the corresponding stack item! If not, a proof verification error is reported.
  5. As many stack entries as there are mandatory hypotheses are then popped from the Proof Work Stack.
  6.  The same substitutions are made to the referenced assertion, and the result is pushed onto the Proof Work Stack.
  7. After the last label in the proof is processed, the stack must have a single entry that matches the expression in the $p statement containing the proof.
  8. A proof may contain a ? in place of a label to indicate an unknown step (A proof verifier may ignore any proof containing ? but should warn the user that the proof is incomplete.  )


Another Explanation

Another way of explaining this is to compare the proof verification process to a robot assembling a product. In this case the "product" is the assertion that is being proved, and the robot's job is to replicate the assertion exactly, symbol for symbol, using the tools and sub-components in the inventory. The proof is, to the robot, a set of step by step computer instructions on how to assemble the product -- and remember, the robot knows nothing about logic or mathematics! Each proof step is a construction step that pulls out of inventory either a sub-component (hypothesis) or an assertion (tool) -- an assertion with its own hypotheses might be considered a "kit", containing both sub-components and the specific tool needed for customization to the job at hand.

Now, continuing the analogy, the Proof Work Stack is like a conveyor belt that the robot uses to temporarily store sub-components that have already been customized and assembled but are not needed until later, when they will be combined into larger components, and so on. For example, imagine that the final product (provable assertion) has three sub-components. As each sub-component is customized and assembled, it is placed on the conveyor belt, which is then shifted one position to make room for the next sub-component. Then, when it is time for final assembly, the direction of the conveyor belt is reversed and the sub-components are removed, one at a time, customized some more, and then installed in the finished product (this is why the order of items on the conveyor belt is critically important, just as it is for the Proof Work Stack -- when you need a wheel and the next item on the conveyor belt is a radiator, the finished product either cannot be built or doesn't work!)

The key to all of this is customizing the generic sub-components in the inventory so that they fit into the finished product according to the product specifications. In Metamath Proof Verification, customization is achieved by substituting already assembed expressions into the new variables at each step of the process  --  and then storing the result on the stack/conveyor belt for later use.

I hope that helps more than it hinders...

Example: a1i



Notes Regarding Proof Demonstration Table Below:

1) I used "show statement xxx / full" to see details of mandatory hypotheses and referenced formulas for the labels referenced in the proof.

2) Metamath displays the stack in "RPN" order, which means Reversed, "Last-In, First Out" (LIFO) Order. This is done for convenience in programming with arrays (reversing the stack eliminates the need to move entries in memory when adding or removing an entry from the stack). Thus, in MetaMath.pdf, "topmost" should be interpreted as the bottom-most entry of a reversed stack...


3) The table below demonstrates Proof Verification without any Distinct Variable Restrictions.



4) The 3rd column, "Type" refers to "H" for Hypothesis and "A" for Assertion (may be Axiomatic or Provable Assertion)



5)  The 6th column, "Unique Substitution", contains the variable substitutions necessary to make the 5th Column, "Assertion's Mandatory Hypotheses", match the 4rd column, "Proof Work Stack". [In other words, this is the legendary process of Unification at work! A small example...but nonetheless, a great achievement for mankind!]


  ${
    $( Premise for ~ a1i . $)
    a1i.1 $e |- ph $.
    $( Inference derived from axiom ~ ax-1 .  See ~ a1d for an explanation of
       our informal use of the terms "inference" and "deduction". $)
    a1i $p |- ( ps -> ph ) $=
      wph wps wph wi a1i.1 wph wps ax-1 ax-mp $.
      $([5-Aug-93]$)
  $}

Label



======
 T
y
p
e
=
 Referenced
Expression

=====================		 Proof Work Stack
(After step
processed!)
In RPN Order
=====================
 Assertion's
Mandatory
Hypotheses
In RPN Order
================
 Unique
Substitution


===============
1
 
wph
 
H
 
wff ph
 wff ph

2
 wps
 
H
 wff ps wff ph
wff ps

3
 wph
 H 
wff ph
 wff ph
wff ps
wff ph

4
 wi
 A
 
wff ( ph -> ps )
 wff ph
wff ( ps -> ph )
 wff ph
wff ps
 'ps' for
'ph',

'ph' for
'ps'
5
 a1i..1
 H
 
|- ph
 
wff ph
wff ( ps -> ph )
|- ph

6
 wph
 H 
wff ph
 
wff ph
wff ( ps -> ph )
|- ph
wff ph

7
 wps
 H 
wff ps
 
wff ph
wff ( ps -> ph )
|- ph
wff ph
wff ps

8
 ax-1
 A
 
|- ( ph -> ( ps -> ph ) )
 
wff ph
wff ( ps -> ph )
|- ph
|- ( ph -> ( ps -> ph ) )
 wff ph
wff ps
 'ph' for
'ph',

'ps' for
'ps'
9
 ax-mp
 A
 
|- ps
 
|- ( ps -> ph )
 wff ph
wff ps
|- ph
|- ( ph -> ps )
 'ph' for
'ph',

'( ps -> ph )' for 'ps'


Voila! The contents of the Proof Work Stack after Step 9 match the $p expression! QED!!!


Example: elong


  ${
    $d x A $.  $( ` x ` is dummy. $)
    $( An ordinal number is an ordinal set. $)
    elong $p |- ( A e. B -> ( A e. On <-> Ord A ) ) $=
      vx cv word cA word vx cA con0 cB vx cv cA ordeq vx df-on elab2g $.
      $( [5-Jun-94] $)
  $}



 Label



=====
 T
y
p
e
=
 Referenced
Expression


=========================		 Proof Work Stack
(After step
processed!)
In RPN Order
=========================
 Assertion's
Mandatory
Hypotheses
In RPN Order
=================
 Unique
Substitution


======
1 vx
 		H set x set x

2
 cv A class x class x
 set x
 'x' for 'x'
3
 word A
 wff Ord A
 		wff Ord x
 class A
 'x' for 'A'
4
 cA H
 class A
 		wff Ord x
class A

5
 word A
 wff Ord A wff Ord x
wff Ord A
 class A
 'A' for 'A'
6
 vx H set x
 		wff Ord x
wff Ord A
set x

7
 cA H class A wff Ord x
wff Ord A
set x
class A

8
 con0 A
 class On
 		wff Ord x
wff Ord A
set x
class A
class On

9
 cB H
 class B
 wff Ord x
wff Ord A
set x
class A
class On
class B

10 vx H
 set x
 wff Ord x
wff Ord A
set x
class A
class On
class B
set x

11 cv A
 class x
 wff Ord x
wff Ord A
set x
class A
class On
class B
class x		 set x
 'x' for 'x'
12 cA H
 class A wff Ord x
wff Ord A
set x
class A
class On
class B
class x
class A

13 ordeq A
 |- ( A = B ->
   ( Ord A <-> Ord B ) )
 wff Ord x
wff Ord A
set x
class A
class On
class B
|- ( x = A ->
  ( Ord x <-> Ord A ) )		 class A
class B
 'x' for 'A'
'A' for 'B'
14 vx H
 set x
 wff Ord x
wff Ord A
set x
class A
class On
class B
|- ( x = A ->
  ( Ord x <-> Ord A ) )
set x

15 df-on A
 |- On = { x | Ord x }
 wff Ord x
wff Ord A
set x
class A
class On
class B
|- ( x = A ->
  ( Ord x <-> Ord A ) )
|- On = { x | Ord x }
 set x
 'x' for 'x'
16 elab2g A
 |- ( A e. C ->
( A e. B <-> ps ) )
 |- ( A e. B ->
( A e. On <-> Ord A ) )		 wff ph
wff ps
set x
class A
class B
class C
|- ( x = A ->
 ( ph <-> ps ) )
|- B = { x | ph }

'Ord x' for
        'ph'
'Ord A' for
        'ps'
'x' for 'x'
'A' for 'A'
'On' for 'B'
'B' for 'C'

Voila! The contents of the Proof Work Stack after Step 16 match the $p expression! QED!!!
  ${
    $d x A $.  $( ` x ` is dummy. $)
    $( An ordinal number is an ordinal set. $)
    elong $p |- ( A e. B -> ( A e. On <-> Ord A ) ) $=
      vx cv word cA word vx cA con0 cB vx cv cA ordeq vx df-on elab2g $.
      $( [5-Jun-94] $)
  $}