.mm Metamath File

(back to Start.html)
mmj2 does not update Metamath .mm database files. As a result, after completing a proof on the Proof Assistant GUI screen you either need to manually copy the generated RPN-format proof of your theorem into the .mm file (using a text editor), or use the Metamath eimm.exe program to "import" your Proof Worksheet (.mmp) file. For new theorems you cannot use eimm.exe, and to see the effect of any additions or updates to the input Metamath .mm database file you need to exit the mmj2 Proof Assistant and start it again.

Here is an example of a Metamath .mm database file: Example.mm
$( Example.mm cloned from Metamath's set.mm $)

          $c (                                       $. 
          $c )                                       $.
          $c ->                                      $.
          $c wff                                     $.
          $c |-                                      $.
 
          $v ph                                      $.
          $v ps                                      $.
          $v ch                                      $.

  wph     $f wff ph                                  $.
  wps     $f wff ps                                  $.
  wch     $f wff ch                                  $.

  wi      $a wff ( ph -> ps )                        $.

  ax-1    $a |-  ( ph -> ( ps -> ph ) )              $.

  ${
    min   $e |-  ph                                  $.
    maj   $e |-  ( ph -> ps )                        $.
    ax-mp $a |-  ps                                  $.
  $}

  ${
    a1i.1 $e |-  ph                                  $.
    a1i   $p |-  ( ps -> ph )
          $= wph wps wph wi a1i.1 wph wps ax-1 ax-mp $.
  $}


Note: mmj2 uses slightly different names than Metamath:
Metamath
 mmj2
Constant ($c)
 Constant ("Cnst" or "Type Code")
Variable ($v)
 Variable ("Var")
Floating Hypothesis ($f)
 Variable Hypothesis ("VarHyp")
Essential Hypothesis ($e)
 Logical Hypothesis ("LogHyp")
Axiomatic Assertion ($a)
 Syntax Axiom ("Axiom")
 "         "
 Logical Axiom (also "Axiom")
Provable Assertion ($p)
 Theorem ("Theorem")
 "        "
 Syntax Proof (rare...)

(More information -- technically oriented -- about mmj2's nomenclature can be found at "MetamathERNotes.html".)

 
(back to Start.html)