Table of content


Content



BookManagerEnabled

BookManagerEnabled.

"BookManagerEnabled": default is "yes"


Caption

Caption.
 "Caption": freeform caption for report output.
 


Clear

Clear.

 "Clear":  clear loaded/derived mm data (files/grammar,etc)
          as well as all RunParm values except for
          SystemErrorFile and SystemOutputFile.
 


DeclareWorkVars

DeclareWorkVars command.
  - Optional. May appear anywhere after the "Parse" RunParm
              within an input, and takes effect immediately
              (any existing Work Variables are deleted and
              a new set is created.)
 
  - Default = A default DeclareWorkVars RunParm is executed
              automatically when first need arises (e.g. at
              Proof Assistant start-up), if none have been
              input since the last Clear RunParm or the start
              of the RunParm file.
 
  - Value1 = N/A
 
  - Examples
 
     *       1         2         3         4
     *234567890123456789012345678901234567890
     DeclareWorkVars
 


DefineWorkVarType

DefineWorkVarType command.
 : - Optional. May appear anywhere after the "Parse" RunParm
              within an input RunParm file, and takes effect
              when the next DeclareWorkVars RunParm command is
              processed. If not input prior to first use -- the
              Proof Assistant -- the default settings are
              automatically used.
 
  - Default = One default DefineWorkVarType RunParm is
              generated for each grammatical Type Code.
              specifying a prefix of "&x" where "x" is
              the first character of the grammatical
              type code, converted to lower case if
              necessary; 100 work variables are defined
              by default for each grammatical type code.
 
  - Value1 = Grammatical Type Code (e.g. "wff", "class",
             "set", etc.) Must be a valid grammatical
             Type Code.
 
  - Value2 = Work Variable Prefix for the grammatical
             Type Code. Must generate unique variable and
             variable hypothesis names when concatenated
             with the Work Variable numerical suffix (1,
             2, ..., 11, ..., etc.) Note that Work
             Variable Hypothesis labels are generated
             automatically and are the same as the Work
             Variables. A Work Variable Prefix must
             consist solely of valid Metamath math
             symbol characters (not "$", for example,
             or embedded blanks.)
 
  - Value3 = Number of Work Variables to be declared for the
             grammatical Type Code. Must be greater than 9
             and less than 1000 ("stinginess" is recommended to
             avoid wasted processing and memory allocations...
             but, in the event that the supply of available
             Work Variables is exhausted during processing
             a pop-up GUI error message will be displayed; the
             RunParms will need to be modified and re-input
             in a subsequent run...)
 
      - Examples:
         *       1         2         3         4
         *234567890123456789012345678901234567890
         DefineWorkVarType,wff,&W,100
         DefineWorkVarType,set,&S,100
         DefineWorkVarType,class,&C,100
 


DisableSettings

* DisableSettings

"DisableSettings": no options

Turn off the saving and loading of settings to the SettingsFile on startup and shutdown. Use SettingsFile RunParm to re-enable.


ExtractTheoremToMMTFolder

null

GarbageCollection

GarbageCollection.

"GarbageCollection": frees up unused memory items.



GMFFExportFromFolder

GMFFExportFromFolder command.
 - Optional. Primarily used for testing. Exports Proof Worksheet
             file(s) from a given directory using the current
             parameter settings (export parms, escapes, etc.)
 
             May appear anywhere after the "LoadFile" RunParm,
             but should appear after Work Var allocations, at
             least.
 
  - Default = N/A -- used for batch testing.
 
  - Value1 = directory containing Proof Worksheet files
 
  - Value2 = theorem label or "*" (all). If theorem label
             input then it is the starting point of the
             export process, which will export the Max
             Number of files beginning at that label.
             If "*" input then the export begins at the
             first label. Either way, files are exported
             in lexicographic order -- i.e. alphabetically.
 
  - Value3 = file type of input Proof Worksheet files
             (normally either .mmp or .mmt)
 
  - Value4 = Max Number of proofs to export. Required.
 
  - Value5 = Append File Name. Name of output file minus
             the file type. Optional. If specified must
             not contain any whitespace characters, or '/'
             or '\' or ':' characters (for safety.) All
             exported Proof Worksheets will be appended
             to the named file (written at the end instead
             of the beginning.) Used for regression testing.
 
      - Examples:
         *       1         2         3         4
         *234567890123456789012345678901234567890
         GMFFExportFromFolder,myproofs,syl,.mmp,1
         GMFFExportFromFolder,myproofs,*,.mmt,100
         GMFFExportFromFolder,myproofs,a2i,.mmt,5,Test20110915a
 


GMFFExportParms

GMFFExportParms command.
 
 - Optional. Default values are shown above. Modifications
   to the defaults as well as additional settings for new
   export types are made with this RunParm. Validation is
   deferred until GMFF Initialization except for the number
   of RunParm parameters -- i.e. use of this RunParm does not
   trigger GMFF Initialization.
 
 - May appear anywhere after the "LoadFile" RunParm
   but preferably the GMFF RunParms -- if used at
   all -- appear just prior to starting the Proof
   Assistant. For testing purposes, if input Proof
   Worksheet files are used and they contain Work
   Variables then the GMFF RunParms should appear
   after the WorkVar RunParms.
 
 - Value1     = Export Type (Unicode or .gif)
   - defaults: althtml and html
   - Export Type must be unique. It is the key in the export
     parms (and text escapes) lists built using default
     settings merged with the input RunParms GMFFExportParms
     entries.
   - A second GMFFExportParms RunParm with the same Export
     Type updates the first.
 
 - Value2     = on/off
   - default ON
   - ON or OFF to enable/disable this export type.
   - Note that by default, both html and althtml are ON.
   - Setting all export types OFF disables GMFF exports.
   - If OFF the rest of the input parameters are not validated
     or stored.
 
 - Value3     = Typesetting Definition Keyword in .mm file
               (in the $t typesetting comment) for this export.
   - defaults: althtmldef and htmldef (or latex but latex is
     not supported by the GMFF Model files provided and only
     Model A is coded into the program.)
 
 - Value4     = Export Directory.
   - defaults: gmff\althtml and gmff\html
   - Directory where exports are written. Also, gmff\html
     contains .gif files for symbols.
 
 - Value5     = export File Type
   - default: .html (.html or .htm might be good choices :-)
 
 - Value6     = GMFF Models Directory -- Directory containing
                html fragment files serving as models for exports.
   - defaults: gmff\althtml\models and GMFF\html\models
 
 - Value7     = Model Id. Only "A" is valid now.
   - defaults: Model Id."A"
 
 - Value8     = Charset Encoding name.
   - default: ISO-8859-1
   - Must match the html fragment for the specified Model Id
     which contains the html  keyword...but the program
     does not validate this! Model A specifies ISO-8859-1
     (same as Metamath Proof Explorer).
   - Valid charset encodings on all Java platforms are:
     - US-ASCII
     - ISO-8859-1
     - UTF-8
     - UTF-16BE
     - UTF-16LE
     - UTF-16
 
  - Value9 = OutputFileName 
 
              Name of output file minus the file type. 
              Optional. 
 
              - If not specified the output file name is 
                constructed from the proof theorem's label 
                + the Export File Type. 
 
                - Note! The OutputFileName applies to all 
                  exports, including those via the 
                  GMFFExportTheorem and GMFFExportFromFolder 
                  RunParms in addition to ProofAsstGUI 
                  export requests. To export to individual 
                  theorem-named files you must input a 
                  new GMFEExportTheorems RunParm!!! 
 
              - If specified must not contain any 
                whitespace characters, or '/' or '\' or ':' 
                characters (for safety.) 
 
                - All/any exported Proof Worksheets will be 
                  output to the named file suffixed with the 
                  GMFFExportParms file type -- except that 
                  the GMFFExportTheorem and 
                  GMFFExportFromFolder AppendFileName 
                  parameter overrides the OutputFileName 
                  parameter on the GMFFExportParms RunParm! 
 
 
 - NOTE: There is nothing in the GMFF program code specific
         to html. All html-specific information is external
         to the code, and is specified via the GMFF RunParms,
         the GMFF \models directory files, and the Metamath
         $t typesetting definitions.
 
         - Since mmj2 allows you to input more than one
           LoadFile RunParm, you could create an extra $t
           comment in a second input .mm file and output
           export data in whatever format you desire...
           the only proviso being that the GMFF code knows
           the names of the \models files for Model A. So
           either your extra export type must match the
           pattern of \models files (with regards to the
           parts which are filled in by the code vs. what
           is in the fragments), or another model would
           need to be added to the GMFF code.
 
           - Model A is a "minimalist" version of a webpage
             which typesets only proof step formulas plus the
             theorem label, which is output as text but is
             treated as a variable in the model.)
 
           - The one thing you cannot do with this design is
             export to a language which is based on the formula
             parse trees, for example MathML. Exporting and
             typesetting based on parse trees -- as opposed to
             formulas comprised of sequences of symbols -- would
             require extra code in GMFF.
 
      - Examples (these are the defaults):
         *       1         2         3         4
         *234567890123456789012345678901234567890
         GMFFExportParms,althtml,ON,althtmldef,gmff\althtml,.html,gmff\althtml\models,A,ISO-8859-1,general
         GMFFExportParms,html,ON,htmldef,gmff\html,.html,gmff\html\models,A,ISO-8859-1,general
 


GMFFExportTheorem

GMFFExportTheorem command.
 - Optional. Primarily used for testing. Exports Proof Worksheet
             file(s) from the loaded Metamath database using
             the current parameter settings (export parms, escapes, etc.)
 
             May appear anywhere after the "LoadFile" RunParm,
             but should appear after Proof Assistant parameters
             initialized if the default Proof Assistant settings
             are not used.
 
  - Default = N/A -- used for batch testing.
 
  - Value1 = theorem label or "*" (all). If theorem label
             input then it is the starting point of the
             export process, which will export the Max
             Number of files beginning at that label.
             If "*" input then the export begins at the
             first label. Either way, files are exported
             in MObj.seq number -- i.e. by order of appearance
             in the loaded Metamath database (LogicalSystem.)
 
  - Value2 = Max Number of proofs to export. Required.
 
  - Value3 = Append File Name. Name of output file minus
             the file type. Optional. If specified must
             not contain any whitespace characters, or '/'
             or '\' or ':' characters (for safety.) All
             exported Proof Worksheets will be appended
             to the named file (written at the end instead
             of the beginning.) Used for regression testing.
 
      - Examples:
         *       1         2         3         4
         *234567890123456789012345678901234567890
         GMFFExportTheorem,syl,1
         GMFFExportTheorem,*,100
         GMFFExportTheorem,syl,100,Test20110915a
 


GMFFInitialize

GMFFInitialize command.
 - Optional. Forces initialization or re-initialization
             using whatever GMFF RunParm options, default
             settings and Metamath $t typesetting definitions have
             been input.
        - NOTE: GMFFInitialize prints an audit message showing the final set
        of parms in effect: selected Exporter ExportParms,
        UserTextEscapes and UserExportChoice ... plus
        typeset definition symbol counts by def keyword.
 
  - The audit report is printed only if GMFF initialization is
    successful.
 
  - May appear anywhere after the "LoadFile" RunParm
    but preferably the GMFF RunParms -- if used at
    all -- appear just prior to starting the Proof
    Assistant. For testing purposes, if input Proof
    Worksheet files are used and they contain Work
    Variables then the GMFF RunParms should appear
    after the WorkVar RunParms.
 
 - If GMFFInitialize is not used then initialization
   takes place only if/when the first GMFF export is
   attempted. Reinitialization can occur if one or
   more additional LoadFile commands have executed
   since initialization and new Metamath $t typsetting
   definitions have been input. (And of course, the
   "Clear" RunParms resets all state variables, which
   would force reinitialization if additional LoadFile
   commands and GMFF export processing were to occur.)
 
 - Initialization may result in error messages about
   the contents of the input .mm Metamath file's $t
   typesetting commands, as well as any other start-up
   errors from GMFF.)
 
  - Default = N/A -- GMFF initialization is automatic.
 
 
 - Value1 -  "PrintTypesettingDefinitions" or spaces.
   - Optional
   - Prints the defined symbols and their definitions (replacement
     text.)
 
 
      - Examples:
         *       1         2         3         4
         *234567890123456789012345678901234567890
         GMFFInitialize
         GMFFInitialize,PrintTypesettingDefinitions
 


GMFFParseMetamathTypesetComment

GMFFParseMetamathTypesetComment command.
 - Optional. Primarily used for testing. Executes
             standalone parse of a single Metamath $t comment
             (does not affect the state of GMFF or anything
             else -- except Messages.)
 
             NOTE: the input file should contain only
             the $t comment!
 
             May appear anywhere after the "LoadFile" RunParm.
             (Although it is "standalone" and affects only the
             Messages and GMFFManager objects, the LoadFile
             command creates the LogicalSystem object which holds
             the GMFFManager object.)
 
             A dump of the parse results is generated along with
             statistics. The dump is in the form of a very long
             "info" message.
 
  - Default = N/A -- used for batch testing.
 
  - Value1 = Typesetting Definition Keyword in .mm file
              (in the $t typesetting comment) to be selected
             for parsing.
 
  - Value2 = directory containing MM file
 
  - Value3 = Metamath .mm file containing just a $t comment.
 
 
  - Value4 -  "PRINT" or spaces.
   - Optional
   - Prints the input file as well as the parsed symbols and
     their definitions (replacement text.)
 
      - Examples:
         *       1         2         3         4
         *234567890123456789012345678901234567890
         GMFFParseMetamathTypesetComment,htmldef,mydirectory,mytypesetdefs.mm
         GMFFParseMetamathTypesetComment,htmldef,mydirectory,mytypesetdefs.mm,PRINT
 


GMFFUserExportChoice

GMFFUserExportChoice command.
 - Optional:
   - These "escapes" convert certain output text characters
     to an alternative character sequence that represents
     the escaped text characters in the output language
     (e.g. html).
 
 - Value1 - Export Type (Unicode or .gif).
   - Defaults: althtml and html
   - Must match the Export Type on one of the GMFFExportParms
     RunParms or the default GMFFExportParms
 
      - Examples ("ALL" is the default):
         *       1         2         3         4
         *234567890123456789012345678901234567890
         GMFFUserExportChoice,ALL 
         GMFFUserExportChoice,html 
         GMFFUserExportChoice,althtml
 


GMFFUserTextEscapes

GMFFUserTextEscapes command.
 - Optional:
   - These "escapes" convert certain output text characters
     to an alternative character sequence that represents
     the escaped text characters in the output language
     (e.g. html).
 
     - Escapes are necessary because certain text characters
       which may be used in a Proof Worksheet have special,
       non-text significance in html. Characters such as '&',
     '>', '<', etc. are used in the html language.
 
     - The space character is escaped into " " so that
       Proof Worksheet text spacing is maintained (otherwise
       browsers would collapse or ignore output spaces in
       certain situations.)
 
 - Value1 - Export Type (Unicode or .gif).
   - Defaults: althtml and html
   - Must match the Export Type on one of the GMFFExportParms
     RunParms or the default GMFFExportParms
 
 - ValueN - Decimal number of Metamath ASCII character
            to be "escaped" in the output html file.
 - ValueN+1
          - Character string to replace escaped character.
 
 - Default Escape Pairs (for both html and althtml):
   -  32 (' ') -> " "
   -  34 ('"') -> """
   -  38 ('&') -> "&"
   -  60 ('<') -> "<"
   -  62 ('>') -> ">"
 
 - NOTE: User Text to be "escaped" is whatever text
         in the Proof Worksheet is not "typeset" using
         the Metamath $t typesetting definitions --
         and any mmj2 Proof Worksheet text stored in
         a \models directory (e.g. Proof Worksheet Header
         text contains both "<" and ">", which are stored
         in the \models directory in escaped format
         (so it does not need to be escaped again.)
 
      - Examples (these are the defaults):
         *       1         2         3         4
         *234567890123456789012345678901234567890
         GMFFUserTextEscapes,html,32," ",34,""",38,"&",60,"<",62,">" 
         GMFFUserTextEscapes,althtml,32," ",34,""",38,"&",60,"<",62,">"
 


GrammarAmbiguityEdits

GrammarAmbiguityEdits.
 "GrammarAmbiguityEdits": "basic" (default) or "complete"
 


InitializeGrammar

InitializeGrammar.
 "InitializeGrammar": no option values
 


LoadComments

LoadComments
 "LoadComments": value1 = yes/no (default = yes)
                          load Metamath comments
                          into LogicalSystem as Descriptions for
                          the MObj's. The comment immediately
                          preceding the $p statement is treated
                          as the description (must be the statement
                          immediately prior to the $p statement.)
 
                          Only Theorem descriptions are loaded
                          now -- which is for Proof Assistant --
                          but in principle, the rest could be
                          loaded, except for $c and $v statements
                          which often have the description
                          after the declaration.
 


LoadEndpointStmtLabel

LoadEndpointStmtLabel.
 "LoadEndpointStmtLabel": value1 = stop after loading given
                                 statement label from
                                 input Metamath file(s).
                                 Must not be blank.
 


LoadEndpointStmtNbr

LoadEndpointStmtNbr.
 "LoadEndpointStmtNbr": value1 = stop after loading given
                                 number of statements from
                                 input Metamath file(s).
                                 Must be greater than zero.
 


LoadFile

LoadFile.
 "LoadFile": value1 = qual/unqual filename (varies by OS!)
 


LoadProofs

LoadProofs
 "LoadProofs": value1 = yes/no (default = yes)
                          load Metamath proofs from input .mm
                          file.
 
                          Use "no" to conserve memory and
                          shorten start-up time for the Proof
                          Assistant.
 
                          If set to "no" then RunParm
                          "VerifyProof" will be ignored -- a
                          warning message is produced though.
 


LoadSettings

* LoadSettings

"LoadSettings": file name relative to mmj2 path.

Load settings from the given file if it exists. If no file given, use the file set by 'SettingsFile,xxx' RunParm.


LoadTheoremsFromMMTFolder

null

LogicStmtType

LogicStmtType.

"LogicStmtType": default is "wff"



MacroFolder

* MacroFolder

"MacroFolder": directory name, no "\" at end of name. Must exist.

Optional. Search location for macros. If this RunParm is not provided, the current directory is used instead.


MacroLanguage

MacroLanguage command.
 Set the language for macro scripts. Valid values depend on
 your installation; input an invalid language to see the list
 of possibilities.

  - Value1 = Language name, default 'js', which corresponds to
             'rhino' on JRE7- and 'nashorn' on JDK8+.
 
  - Value2 = Default file extension, attached to macros with
             no specified extensions, default 'js'.
 
      - Examples:
         *       1         2         3         4
         *234567890123456789012345678901234567890
         MacroLanguage,js,js
         MacroLanguage,BeanShell,bsh
         MacroLanguage,jruby,rb
 


MacrosEnabled

* MacrosEnabled

"MacrosEnabled": yes or no.

Set macros on or off, default = yes.


MaxErrorMessages

MaxErrorMessages.
 "MaxErrorMessages": 1 -> 999999999...
 


MaxInfoMessages

MaxInfoMessages.
 "MaxInfoMessages": 1 -> 999999999...
 


MaxStatementPrintCount

MaxStatementPrintCount.
 "MaxStatementPrintCount": 1 -> 9999999999....
 


OutputVerbosity

OutputVerbosity

 "OutputVerbosity": value1 = integer,
 
  Verbosity = 9999 is the default
            =    0 means only print error messages and
                 specifically requested output
 


Parse

Parse.
 "Parse": "*" or Stmt.label
 


PreprocessRequestBatchTest

PreprocessRequestBatchTest

 "PreprocessRequestBatchTest":
 
                value1 = Mandatory: 
                         a file name, either absolute
                         or relative (to the current
                         directory, or if provided
                         the ProofAsstProofFolder,
                         which is input via RunParm
                         and also during use of
                         ProofAsstGUI<.)
 
                value2 = "EraseAndRederiveFormulas" is the only
                         valid option at this time.
 

This RunParm is provided for regression testing.

The Proof Text is printed before and after preprocessing and unification.


PrintBookManagerChapters

PrintBookManagerChapters
 "PrintBookManagerChapters"
 


PrintBookManagerSectionDetails

PrintBookManagerSectionDetails.
 "PrintBookManagerSectionDetails": "*" or Section Number
 


PrintBookManagerSections

PrintBookManagerSections
 "PrintBookManagerSections"
 


PrintStatementDetails

PrintStatementDetails.
 "PrintStatementDetails": "*" or Stmt.label
 


PrintSyntaxDetails

PrintSyntaxDetails.
 "PrintSyntaxDetails": no options
 


ProofAsstAssrtListFreespace

ProofAsstAssrtListFreespace

Sets the amount of freespace in the ArrayLists used in the Proof Assistant.

Optional, default is 5, minimum 0, maximum 1000.


ProofAsstAutocompleteEnabled

ProofAsstAutocompleteEnabled
"ProofAsstAutocompleteEnabled": Yes or No

Optional, default is Yes (enabled).


ProofAsstAutoReformat

ProofAsstAutoReformat

"ProofAsstAutoReformat": yes or no.

Specifies whether or not proof step formulas are automatically reformatted after work variables are resolved.

Optional, default is yes (see mmj.pa.PaConstants.java)


ProofAsstBackgroundColorRGB

ProofAsstBackgroundColorRGB

 "ProofAsstBackgroundColorRGB":
                        "255,255,255" -- white (default)
                        thru
                        "0,0,0" -- black
 
 Optional, default is "255,255,255" (white)
 


ProofAsstBatchTest

ProofAsstBatchTest

 "ProofAsstBatchTest": value1 = selection, either
 
                      "*"    - all theorems
                      label  - a single theorem
                      99999  - a given number of theorems
 
                      value2 = Optional: 
                               a file name, either absolute
                               or relative (to the current
                               directory, or if provided
                               the ProofAsstProofFolder,
                               which is input via RunParm
                               and also during use of
                               ProofAsstGUI<.) If no file
                               name input, skeleton proofs
                               are generated from memory 
                               (the .mm file loaded :)
 
                value3 = un-unified (default) or
                         unified proof format.
 
                value4 = "Correct" (deprecated "NotRandomized",
                         default), "Randomized", "Reverse" and
                         others (see  mmj.verify.HypsOrder).
                         Controls order of exported proof
                         step logical hypotheses (a testing
                         feature).
 
                value5 = Print or NoPrint (default)
                         Print requests copy of Proof 
                         Worksheet to be sent to the
                         SystemOutputFile (or System.out)
                         in addition to the export file.
 
                value6 = "DeriveFormulas" or "NoDeriveFormulas"
                         (default) or "". If "DeriveFormulas"
                         then the exported Proof Worksheets
                         are written with blank formulas to
                         trigger the Derive Formula feature
                         in the Proof Assistant during later
                         import. Note that the theorem's
                         logical hypotheses and "qed" step
                         cannot be derived -- formula is
                         always required for these steps,
                         so "DeriveFormulas" applies only to
                         non-Qed derivation proof steps.
 
                value7 = "CompareDJs" or "NoCompareDJs"
                          (default) or "".
 
                          See mmj2\data\runparm\windows
                          \AnnotatedRunParms.txt for more
                          info.
 
                value8 = "UpdateDJs" or "NoUpdateDJs"
                         (default) or "".
 
                          See mmj2\data\runparm\windows
                          \AnnotatedRunParms.txt for more
                          info.
 

This RunParm is provided for use in high-volume testing.

RunParm option value2 is input to specify an input file containing proofs in the format used on the Proof Assistant GUI screen. This is optional, and if not provided, the program simulates an input file using the currently loaded Metamath data

In "simulation" mode (no input file), the program exports a proof "to memory", just as it would have been created for the ProofAsstExportToFile RunParm (which is why the unified/un-unified and Randomized/ NotRandomized options are provided here also.) The The export-simulated proof is run through the Unification process for testing purposes. RunParm option value1 provides a selection capability, and this capability works with or without an input file. Specify "*" to test unification of all proofs, either in the input file or those loaded into the system. Specifying a number, for example 99, runs the test for the first 99 theorems (database sequence if input file not provided). Finally, specifying a theorem label runs the test for just that one theorem. Note: a relative filename such as "export.mmp" can be input or an "absolute" name such as "c:\my\export.mmp". The "ProofAsstProofFolder", if present, is used with relative filename. And take care to note that if export is performed *after* ProofAsstGUI, the ProofAsstProofFolder may have been changed.



ProofAsstDefaultFileNameSuffix

ProofAsstDefaultFileNameSuffix

"ProofAsstDefaultFileNameSuffix": ".txt", ".TXT", ".mmp" or ".MMP"

Optional. If this RunParm is not provided, the hardcoded default ".txt" is used as the default for Proof Worksheet file names.


ProofAsstDeriveAutocomplete

ProofAsstDeriveAutocomplete
"ProofAsstDeriveAutocomplete": Yes or No

Optional, default is Yes (enabled).


ProofAsstDjVarsSoftErrors

ProofAsstDjVarsSoftErrors
 "ProofAsstDjVarsSoftErrors":
 
     "Ignore" -- Don't check for missing $d statements
     "Report" -- Create missing $d statement error messages.
     "GenerateReplacements"
              -- Generate complete set of $d statements if
                 any omissions are detected
     "GenerateDifferences"
              -- Generate set of $d statements to add to the
                 $d's in the Proof Worksheet and .mm database
                 for the theorem.
 
 Optional, default is "GenerateReplacements"
 
 NOTE: Superfluous $d statements are not detected!
 


ProofAsstDummyVarPrefix

ProofAsstDummyVarPrefix

"ProofAsstDummyVarPrefix": length > 0, no embedded blanks or unprintable characters. Dummy variables used to display un-determined variable substitutions are given a prefix string and a number. For example: $1, $2, etc. Optional, default is "$ (see mmj.pa.PaConstants.java) +



ProofAsstErrorMessageColumns

ProofAsstErrorMessageColumns
 "ProofAsstErrorMessageColumns":
     greater than 39 and
     less than 1000
 
 Provides a clue to the system about how wide to make
 the ProofAsstGUI error message text area window.
 
 Optional, default is 80 (see mmj.pa.PaConstants.java)
 


ProofAsstErrorMessageRows

ProofAsstErrorMessageRows
 "ProofAsstErrorMessageRows":
     greater than 1 and
     less than 100
 
 Provides a clue to the system about how big to make
 the ProofAsstGUI error message text area window.
 
 Optional, default is 4 (see mmj.pa.PaConstants.java)
 


ProofAsstExcludeDiscouraged

* ProofAsstExcludeDiscouraged

"ProofAsstExcludeDiscouraged": yes or no.

Exclude discouraged theorems from unification search, default = yes.


ProofAsstExportToFile

ProofAsstExportToFile

 "ProofAsstExportToFile":
                value1 = filename; absolute or
                         relative (to current
                         directory or if provided
                         the ProofAsstProofFolder,
                         which is input via RunParm
                         and also during use of
                         ProofAsstGUI
 
                value2 = "*"    - all theorems
                         label  - a single theorem
                         99999  - a given number of theorems
 
                value3 = Optional: new (default),
                         or update
 
                value4 = un-unified (default) or
                                   unified.
 
                value5 = "Correct" (deprecated "NotRandomized",
                         default), "Randomized", "Reverse" and
                         others (see  mmj.verify.HypsOrder).
                         Controls order of exported proof
                         step logical hypotheses (a testing
                         feature).
 
                value6 = Print or NoPrint (default)
                         Print requests copy of Proof 
                         Worksheet to be sent to the
                         SystemOutputFile (or System.out)
                         in addition to the export file.
 
               value7 = "DeriveFormulas" or "NoDeriveFormulas"
                         (default) or "". If "DeriveFormulas"
                         then the exported Proof Worksheets
                         are written with blank formulas to
                         trigger the Derive Formula feature
                         in the Proof Assistant during later
                         import. Note that the theorem's
                         logical hypotheses and "qed" step
                         cannot be derived -- formula is
                         always required for these steps,
                         so "DeriveFormulas" applies only to
                         non-Qed derivation proof steps.
 
 This RunParm is provided for use in high-volume testing.
 It exports proofs to a file in the format required
 by the Proof Assistant GUI. To import the proof file and
 test the Unification function, use RunParm
 'ProofAsstBatchTest', specifying the file name.
 
 Option value3 has two variations: un-unified means the
 exported derivation proof steps do not have Ref labels,
 whereas unified means Ref labels are present.
 
 Note: this feature is not a full export of a Metamath
 file as it does not export $d or anything besides theorems
 and their logical hypotheses.
 
 Note: a relative filename such as "export.mmp" can be
 input or an "absolute" name such as "c:\my\export.mmp".
 The "ProofAsstProofFolder", if present, is used with
 relative filename. And take care to note that if export
 is performed *after* ProofAsstGUI, the ProofAsstProofFolder
 may have been changed.
 



ProofAsstFontBold

ProofAsstFontBold
 "ProofAsstFontBold": Yes or No
 
 Optional, default is Yes (bold).
 


ProofAsstFontFamily

ProofAsstFontFamily
 "ProofAsstFontFamily": "Monospaced", (the default),
                        "Serif",
                        "SansSerif",
                        "Monospaced",
                        "Dialog",
                        "DialogInput"...
                        etc.
 One way to view the list of Font Family Names defined
 on a system is to input an invalid Font Family Name
 on the ProofAsstFontFamily command -- a list will be
 displayed as part of a punitively long error message :)
 
 NOTE!!! Fixed-width fonts such as Monospaced or Courier
         are essential for Proof Assistant if you plan
         on using the Text Mode Formula Formatting
         (TMFF) alignment Methods such as AlignColumn.
         TMFF will not align formula symbols properly
         when proportional fonts are used!!!
 
 Optional, default is "Monospaced"
 


ProofAsstFontSize

ProofAsstFontSize
 "ProofAsstFontSize": 8 or 9, 10, 11, 12, 14, 16, 18
                      20, 22, 24, 26, 28, 36, 48, 72
 
 Optional, default is 14 (see mmj.pa.PaConstants.java)
 


ProofAsstForegroundColorRGB

ProofAsstForegroundColorRGB
 "ProofAsstForegroundColorRGB":
                        "0,0,0" -- black (default)
                        thru
                        "255,255,255" -- white
 
 Optional, default is "0,0,0" (black)
 


ProofAsstFormulaLeftCol

ProofAsstFormulaLeftCol
 "ProofAsstFormulaLeftCol":
     greater than 1 and
     less than ProofAsstFormulaRightCol
 
 Controls program formatting, not user-input formulas.
 
 Optional, default is 20 (see mmj.pa.PaConstants.java)
 


ProofAsstFormulaRightCol

ProofAsstFormulaRightCol
 "ProofAsstFormulaRightCol":
     greater than ProofAsstFormulaLeftCol and
     less than 9999
 
 Controls program formatting, not user-input formulas.
 
 Optional, default is 79 (see mmj.pa.PaConstants.java)
 


ProofAsstHighlightingEnabled

ProofAsstHighlightingEnabled
 "ProofAsstHighlightingEnabled": Yes or No
 
 Optional, default is Yes (enabled).
 


ProofAsstHighlightingStyle

ProofAsstHighlightingStyle
 "ProofAsstHighlightingStyle": type, color RGB, bold yes/no, italic yes/no
 
The color RGB should be given as 6 hex digits (i.e. '00FFC0'), and any of the three fields can be set to 'Inherit' to use the global color/bold/italic settings. Style types and defaults are:
 default: inherit,inherit,inherit
 comment: 808080,no,yes
 keyword: 808080,yes,inherit
 error: FF0000,yes,inherit
 proof: 808080,no,inherit
 step: 8A2908,yes,inherit
 hyp: 8A2908,inherit,inherit
 ref: 0044DD,yes,inherit
 localref: 008800,inherit,inherit
 specialstep: B58900,yes,inherit
 class: CC33CC,inherit,inherit
 set: FF0000,inherit,inherit
 wff: 0000FF,inherit,inherit
 workvar: 008800,inherit,inherit
 


ProofAsstIncompleteStepCursor

ProofAsstIncompleteStepCursor
 "ProofAsstIncompleteStepCursor":
     'First', 'Last', or 'AsIs' (not case sensitive).
 
 Pertains to cursor positioning when no unification
 errors found and there is at least one incomplete
 proof step; 'First' means position cursor to the
 first incomplete proof step, etc.
 
 The cursor is positioned to the Ref sub-field within
 a proof step.
 
 Optional, default is 'Last' (see mmj.pa.PaConstants.java)
 


ProofAsstLineSpacing

ProofAsstLineSpacing
 "ProofAsstLineSpacing": float value, default 0
 


ProofAsstLineWrap

ProofAsstLineWrap
 "ProofAsstLineWrap":
     equal to 'on'
     or       'off'
 
 Controls whether or not text displayed in the proof
 window wraps around when the number of columns of
 text exceeds ProofAsstTextColumns.
 
 Optional, default is 'off' (see mmj.pa.PaConstants.java)
 


ProofAsstLookAndFeel

ProofAsstLookAndFeel

"ProofAsstLookAndFeel": choose between any installed looks on your Java installation. Default is Metal, and available options on my computer are Metal, Nimbus, CDE/Motif, Windows, and Windows Classic, although the specific options depend on your installation. Input an invalid option here to get a list of available options in the error message.



ProofAsstMaximized

ProofAsstMaximized
 "ProofAsstMaximized":
     'yes' or 'no' or 'y' or 'n' or 'Y' or 'N'
 
 If 'yes', maximizes the ProofAsstGUI main window on startup.
 
 Optional, default is 'no' (see mmj.pa.PaConstants.java)
 


ProofAsstMaxUnifyAlternates

ProofAsstMaxUnifyAlternates DEPRECATED

ProofAsstMaxUnifyHints

ProofAsstMaxUnifyHints DEPRECATED

ProofAsstOptimizeTheoremSearch

Perform the optimizations for theorem search during "parallel" unification.

ProofAsstOutputCursorInstrumentation

ProofAsstOutputCursorInstrumentation

"ProofAsstOutputCursorInstrumentation": yes or no.

Used to generate "instrumentation" info messages for use in regression testing. OutputCursor state information is generated by ProofAsst.java at the end of main functions, such as "unify".

Optional, default is no (see mmj.pa.PaConstants.java)


ProofAsstProofFolder

* ProofAsstProofFolder

"ProofAsstProofFolder": directory name, no "\" at end of name. Must exist.

Optional. If this RunParm is not provided, the user of ProofAsstGUI is prompted during Save dialogs, and the folder is remembered for the duration of the session.


ProofAsstProofFormat

ProofAsstProofFormat

 "ProofAsstProofFormat":
 
     "Normal" -- Uncompressed RPN proof
     "Packed" -- RPN proof with backreferences
     "Compressed"
              -- Full compression (with all caps encoding)
 
 Optional, default is "Compressed"
 


ProofAsstRPNProofLeftCol

ProofAsstRPNProofLeftCol
 "ProofAsstRPNProofLeftCol":
     greater than 3 and
     less than ProofAsstRPNProofRightCol
 
 Controls program formatting of generated proof statements
 
 Optional, default is 6 (see mmj.pa.PaConstants.java)
 


ProofAsstRPNProofRightCol

ProofAsstRPNProofRightCol
 "ProofAsstRPNProofRightCol":
     greater than ProofAsstRPNProofLeftCol and
     less than 9999
 
 Controls program formatting of generated proof statements
 
 Optional, default is 79 (see mmj.pa.PaConstants.java)
 


ProofAsstStartupProofWorksheet

ProofAsstStartupProofWorksheet

"ProofAsstStartupProofWorksheet": name of Proof Worksheet file to be displayed at ProofAsstGUI startup. Must exist.

Optional. If this RunParm is not provided, a hardcoded Proof Worksheet (String) is displayd.


ProofAsstStore

ProofAsstStore

"ProofAsstStore": define a file for automatic saving and loading of preferences.



ProofAsstTextAtTop

ProofAsstTextAtTop
 "ProofAsstTextAtTop":
     'yes' or 'no' or 'y' or 'n' or 'Y' or 'N'
 
 If 'yes', positions the ProofAsstGUI proof text area
 above the error message text area; otherwise, their
 positions are reversed (error messages at top).
 
 Optional, default is 'yes' (see mmj.pa.PaConstants.java)
 


ProofAsstTextColumns

ProofAsstTextColumns
 "ProofAsstTextColumns":
     greater than 39 and
     less than 1000
 
 Controls program formatting, not user-input formulas.
 Defines the column width of the window, which can
 be greater than or less than the width of the screen
 or the formulas! Primary effect seen with LineWrap ON
 because intra-formula line breaks are done with spaces
 (and because a double newline is needed at end of
 formulas for legibility reasons.)
 
 Optional, default is 80 (see mmj.pa.PaConstants.java)
 


ProofAsstTextRows

ProofAsstTextRows
 "ProofAsstTextRows":
     greater than 1 and
     less than 100
 
 Provides a clue to the system about how big to make
 the ProofAsstGUI proof text area window.
 
 Optional, default is 21 (see mmj.pa.PaConstants.java)
 


ProofAsstUndoRedoEnabled

ProofAsstUndoRedoEnabled RunParm.

Controls whether or not the Proof Assistant GUI provides Undo/Redo support.

Normally this is turned on, but if desired, say for performance reasons, the user can disable Undo/Redo at start-up time via RunParm.

Optional. Default = yes.


ProofAsstUnifyHintsInBatch

ProofAsstUnifyHintsInBatch DEPRECATED

ProofAsstUnifySearchExclude

ProofAsstUnifySearchExclude

"ProofAsstUnifySearchExclude": options = Assrt labels, comma separated (ex: biigb,xxxid)

NOTE: The RunParm validation for these excluded Assrt labels will be very lenient and will just ignore labels that are "invalid" or not in the Statment Table. The reason is that the exclusion list is expected to be very stable and the new RunParm "LoadEndpointStmtNbr" allows loading of just a portion of a Metamath file; if we required perfection in the exclusion list the usability of LoadEndPointStmtNbr would drop dramatically (see also LoadEndpointStmtLabel).

This RunParm instructs ProofUnifier.java to not attempt to unify the specified assertion labels with any proof steps -- unless the user specifically enters them on a proof step.

The Unification process scans the loaded Metamath file assertion (LogicalSystem.stmtTbl) in ascending database sequence and accepts the first match it finds. Generally that works fine, but in a few cases, such as duplicate theorems that are present simply because of an alternate proof, this feature is helpful (though it would possibly be easier to put biigb after bii and avoid the situation in the first place.)

The *problem* of multiple valid unifications for a proof step may affect a small number of theorems. The list of alternatives can be obtained by specifically entering a valid assertion label that does *not* unify -- the program then provides a message detailing the possible choices. (The message with alternatives is also produced if there is a Distinct Variables error on a proof step and there is no unifying assertion that doesn't have a Distinct Variables error.) In set.mm p0ex and snex are appear as alternatives in a few proofs; mulid1 and mulid2 are another example.



ProofAsstUseAutotransformations

Auto-transformation options (it is temporary option and could be changed any moment):

value1 = Yes/No (use or do not use auto-transformations)

value2 = Yes/No (use debug output or do not use it) value3 = Yes/No (support implication prefix)


ProvableLogicStmtType

ProvableLogicStmtType.

"ProvableLogicStmtType": default is "|-"



RecheckProofAsstUsingProofVerifier

RecheckProofAsstUsingProofVerifier

"RecheckProofAsstUsingProofVerifier,yes" or "RecheckProofAsstUsingProofVerifier,no" Optional, default = "no". If equal to "yes", then each derivation proof step's generated Metamath RPN proof is double-checked using the full Metamath Proof Engine, AKA "Proof Verifier". In theory this should be unnecessary since the Proof Assistant should provide valid proofs, but it may be useful if question arise, or if the user has spare CPU cycles and skepticism. *



RunMacro

RunMacro command.
 : - Optional. Run a BeanShell macro in the macro/ directory.
               May appear anywhere in the RunParms list.
 
  - Value1 = File name.  Path name is relative to the macro/             directory.
 
  - ...    = An arbitrary number of additional parameters are
             permitted; they are passed unchanged to the macro.
 
      - Examples:
         *       1         2         3         4
         *234567890123456789012345678901234567890
         RunMacro,echo,Hello World
 


RunMacroInitialization

RunMacroInitialization command.
 Run the given macro for initialization. Will replace the
 existing script context if a macro has already been run.
 Optional, default is 'init.js', which is run immediately
 before a call to RunMacro if this command is not run first.

  - Value1 = File name.  Path name is relative to the macro/
             directory.
 
      - Examples:
         *       1         2         3         4
         *234567890123456789012345678901234567890
         RunMacroInitialization,init
 


RunProofAsstGUI

RunProofAsstGUI

"RunProofAsstGUI": no option values (for now...)



SaveSettings

* SaveSettings

"SaveSettings": file name relative to mmj2 path.

Save settings to the given file. If no file given, use the file set by 'SettingsFile,xxx' RunParm.


SeqAssignerIntervalSize

SeqAssignerIntervalSize.
 "SeqAssignerIntervalSize": default = 100, min = 1,
 max = 10000.
 


SeqAssignerIntervalTblInitialSize

SeqAssignerIntervalTblInitialSize.
 "SeqAssignerIntervalTblInitialSize": default = 100, min = 10,
 max = 10000.
 


SetMMDefinitionsCheckWithExclusions

SetMMDefinitionsCheckWithExclusions

 
 "SetMMDefinitionsCheckWithExclusions":
     options = Assrt labels, comma separated, with * wildcard
 

This option runs a soundness check on all axioms in the database, except those specified in the list. Recommended exclusions are ax-*,df-bi,df-clab,df-cleq,df-clel, which will always fail the check.

This RunParm option is deprecated; its functionality has been replaced by RunMacro,definitionCheck,... with the same arguments.


SetParser

SetParser.
 "SetParser": fully qualified parser implementation class name.
 


SettingsFile

* SettingsFile

"SettingsFile": file name relative to mmj2 path.

Set the file for use by 'LoadSettings' and 'SaveSettings' RunParms. Default value is 'store.json'.


StartInstrumentationTimer

StartInstrumentationTimer

 "StartInstrumentationTimer": value1 = ID String,
 
  ID String = Identifier in output message produced
              by StopInstrumentationTimer RunParm --
              must match that ID String.
 


StatementAmbiguityEdits

StatementAmbiguityEdits.
 "StatementAmbiguityEdits": "basic" (default) or "complete"
 


StatementTableInitialSize

StatementTableInitialSize.
 "StatementTableInitialSize": default = 30000, min = 100
 


StepSelectorBatchTest

StepSelectorBatchTest

 "StepSelectorBatchTest":
 
                value1 = Mandatory: 
                         a file name, either absolute
                         or relative (to the current
                         directory, or if provided
                         the ProofAsstProofFolder,
                         which is input via RunParm
                         and also during use of
                         ProofAsstGUI<.)
 
                value2 = cursor position:
                         char offset position in Proof Worksheet
 
                value3 = selection number
                         zero to 99999999.
 

This RunParm is provided for regression testing.

Specify the cursor position within the Proof Worksheet and the number to be selected from the StepSelectorDialog for the request. The program initiates a StepSelectorSearch and then if there are no errors, selects the chosen item from the StepSelectorResults and invokes unify().

The StepSelectorResults are printed, as well as the ProofWorksheet after unification -- and any messages.


StepSelectorDialogPaneHeight

StepSelectorDialogPaneHeight

Sets the pixel width of the StepSelectorDialog.

Optional, default is 440 (see mmj.pa.PaConstants.java)


StepSelectorDialogPaneWidth

StepSelectorDialogPaneWidth

Sets the pixel width of the StepSelectorDialog.

Optional, default is 720 (see mmj.pa.PaConstants.java)


StepSelectorMaxResults

StepSelectorMaxResults

Limits the number of unifying assertions returned by the StepSelectorSearch.

Optional, default is 50 (see mmj.pa.PaConstants.java)


StepSelectorShowSubstitutions

StepSelectorShowSubstitutions

Determines whether or not unifying assertions are shown as is or with the substitutions required by unification.

Default is true (see mmj.pa.PaConstants.java)


StopInstrumentationTimer

StopInstrumentationTimer

 "StopInstrumentationTimer": value1 = ID String,
 
  ID String = Identifier in StartInstrumentationTimer
              RunParm -- must match.
 


SvcArg

SvcArg

 "SvcArg": Key/Value Pair loaded into Map which is passed
           to SvcCallback.go(). Key/Value pairs are minimally
           validated to ensure that each Key is at least
           one character long and unique. The Key/Value parm
           contents are parsed using the same separator
           and delimter characters used for the rest of
           the RunParms. Multiple SvcArgs can be input.
 
 : - Optional.
 
  - Default = None.
 
  - Value1 = Key. Non-blank string at least one character
             in length. Must not be a duplicate of any
             other SvcArg key.
 
  - Value2 = Value. String zero or more characters in
             length.
 
      - Examples:
         *       1         2         3         4
         *234567890123456789012345678901234567890
         SvcArg,OutFilePrefix,exp
         SvcArg,OutFileSuffix,zip
         SvcArg,ZipOutput,yes
 


SvcCall

SvcCall

 "SvcCall": Command to perform call to SvcCallback.go().
 
      - Examples:
         *       1         2         3         4
         *234567890123456789012345678901234567890
         SvcCall
 


SvcCallbackClass

SvcCallbackClass

 "SvcCallbackClass": Name of class which implements the
              mmj.svc.SvcCallback interface in "callee"
              mode. Must have a default constructor.
 
      NOTE: Do not input this RunParm if you are using
            SvcCallback in "caller" mode because it will
            override the specific instance of your class
            which you pass as an argument to
            BatchMMJ2.generateSvcCallback()
 
 : - Optional. SvcCallback can be provided via a call to
              BatchMMJ2.setSvcCallback().
 
  - Default = None.
 
  - Value1 = SvcCallbackClass class name.
 
      - Examples:
         *       1         2         3         4
         *234567890123456789012345678901234567890
         SvcCallbackClass,c:\MyClass
 


SvcFolder

SvcFolder

 "SvcFolder": directory name, no "\" at end of name.
              Must exist and must be a directory.
 
 : - Optional. Must appear prior to the SvcCall RunParm.
 
  - Default = If not input, output Svc files are directed
              to the current directory.
 
  - Value1 = Directory Name. No "\" or "/" at the end
             of name. Must exist and must be the name of
             a directory. The separator symbol is OS 
             dependent (Windows uses "\", *nix/Max = "/").
 
      - Examples:
         *       1         2         3         4
         *234567890123456789012345678901234567890
         SvcFolder,c:\MyFolder
 


SymbolTableInitialSize

SymbolTableInitialSize.
 "SymbolTableInitialSize": default = 1500, min = 10
 


SystemErrorFile

SystemErrorFile.

 "SystemErrorFile": value1 = filename,
 
                    value2 = new (default) or update.
                      The system will NOT touch an existing
                      file unless given "update",
                      AND if "new" is specified an error is
                      reported, halting processing ASAP if
                      the file already exists. If the file
                      does exist and Update is specified,
                      then it is overwritten (not appended),
                      but no error is reported for Update
                      if the file does not exist.
 
                    value3 = charset. Note: the program
                      will not stop you from appending
                      a different charset to an existing
                      file, thus hopelessly mixing up your
                      data, so have fun but be careful!
 
 info on charsets
 file:///C:/Program%20Files/Java/jdk1.5.0_02/docs/api/java/nio/charset/Charset.html
 
 Valid charset names on all Java Platforms:
     US-ASCII
     ISO-8859-1
     UTF-8
     UTF-16BE
     UTF-16LE
     UTF-16
 


SystemOutputFile

SystemOutputFile.

 "SystemOutputFile": value1 = filename,
 
                     value2 = new (default), or
                        update
 
                     value3 = charset
                        see RUNPARM_SYSERR_FILE comments
                        for info on the above value parms!
 


TheoremLoaderAuditMessages

null

TheoremLoaderDjVarsOption

null

TheoremLoaderMMTFolder

null

TheoremLoaderStoreFormulasAsIs

null

TheoremLoaderStoreMMIndentAmt

null

TheoremLoaderStoreMMRightCol

null

TMFFAltFormat

TMFFAltFormat command.

Specifies the alternate TMFF Format to be used when the ProofAsstGUI Edit/Reformat Proof - Swap Alt menu item is selected.

Parameters:

  1. Format Nbr: 0, 1, 2, 3, etc.


TMFFAltIndent

TMFFAltIndent command.

Specifies the number of columns to indent a proof step formula for each level in the proof tree. Specifies the alternate TMFF Indent Amount to be used when the ProofAsstGUI Edit/Reformat Proof - Swap Alt menu item is selected.

Parameters:

  1. Alt Indent Amount: 0, 1, 2, 3, or 4.


TMFFDefineFormat

TMFFDefineFormat command.

Defines TMFF Formats that may be referenced subsequently in the TMFFUseFormat command (TMFFUseFormat can only refer to a TMFF Scheme that is already defined, which includes the pre-defined, built-in Formats.)

Note: a Format can be re-defined in a subsequent RunParm. This would normally be of use only in a testing situation.

Parameters:

  1. Format Nbr: 1, 2 or 3.
  2. Scheme Name: must be non-blank, unique, not = "Unformatted". Not case sensitive.


TMFFDefineScheme

TMFFDefineScheme command.

Defines TMFF Schemes that may be referenced subsequently in TMFF Formats (TMFFDefineFormat can only refer to a TMFF Scheme that is already defined.)

Note: a Scheme can be re-defined in a subsequent RunParm. This would normally be of use only in a testing situation.

Parameters:

  1. Scheme Name: must be non-blank, unique, not = "Unformatted". Not case sensitive.
  2. Method Name: = "AlignColumn" or "Flat". Not case sensitive.
  3. MaxDepth = subtree depth max before triggering break
  4. ByValue = "Var", "Sym", or "Cnst" (AlignColumn only)
  5. AtNbr = 1, 2, or 3 (AlignColumn only)
  6. AtValue = "Var", "Sym" or "Cnst" (AlignColumn only)


TMFFUseFormat

TMFFUseFormat command.

Specifies which TMFF Format is in use during subsequent processing.

Note: multiple TMFFUseFormat commands can be input, but only one format can be in effect at a single time.

Note: Format '0' = Unformatted, turn TMFF off/disabled.

Parameters:

  1. Format Nbr: 0, 1, 2, 3, etc.


TMFFUseIndent

TMFFUseIndent command.

Specifies the number of columns to indent a proof step formula for each level in the proof tree.

Parameters:

  1. Indent Amount: 0, 1, 2, 3, or 4.


UnifyPlusStoreInLogSysAndMMTFolder

null

UnifyPlusStoreInMMTFolder

null

VerifyParse

VerifyParse.
 "VerifyParse": "*" or Stmt.label
 


VerifyProof

VerifyProof.
 "VerifyProof": "*" or Stmt.label