Page505.mmp

$( <MM> <PROOF_ASST> THEOREM=nngt1ne1REDO  LOC_AFTER=nnge1
*                                                          Page505.mmp

* Mmj2 has two kinds of search mechanisms for finding assertions,
  "step search mode" and "general search mode".

  You've already seen step search mode.  To enter Step Search mode,
  simply double-click a derivation proof step on the proof assistant
  GUI window, or position the cursor to a step and select
  'Search/ Step Search' or the right-mouse button popup window.
  In step search mode there's an implicit requirement that every
  search result must be unifiable with the selected step.

  'General Search mode' is the other mmj2 search mechanism.
  It is not tied to a particular proof step or theorem.
  General Search allows you to search the whole database for assertions,
  for example, if you are still trying to develop a strategy for your proof.

  To enter General Search mode, select 'Search/ General Search'.
  This presents the search form, which has many options.
  The top row has general search commands; in most cases you just
  fill in the sections below it and press "Search" on the top left.
  One of the other commands is "Help".

  There are many ways to control search, but first examine the
  "MaxTime" option on the middle right. This shows the maximum time,
  in seconds, that a search will run. Make sure you give enough time!

  A key part of the search form is the SEARCH_DATA
  (what you are searching for) in up to four
  search data lines. A blank "ForWhat" is ignored.
  Searching is done line by line, top to bottom, with the "AND" and "OR"
  evaluated on its right hand side, and is halted as soon as
  truth or falsity can be determined.

  "InWhat" lets you specify which assertion types and
  associated Metamath statements will be searched
  using the criteria given on the Search Data line.
  The default is "$ap", which searches axioms (the 'a') and proven theorems
  (the 'p'). That doesn't include their hypotheses (which would be 'e').
  "Part" lets you search formulas, comments, or labels.

  "Format" is the search term format.
  There are five different search term formats:
  'Metamath', 'RegExpr', 'CharStr', 'ParseExpr', and 'ParseStmt'.
  Each of the four search lines can be any of those formats
  (e.g., they can all be the same format if you want).
  The last two Formats, 'ParseExpr' and 'ParseStmt', are advanced mechanisms
  that operate on syntactic parse trees; we'll ignore them here.

  The formats 'Metamath', 'RegExpr' and 'CharStr' operate
  on 'normalized' string versions of the underlying Metamath objects --
  formulas, comments, labels and RPN proof label lists. The 'normalized'
  string consists of the non-whitespace math, label and (lower-cased)
  Comment tokens are separated by single space characters (' ') and converted
  to lower case. Let's look at each one in reverse order:

* CharStr : an exact match at least one occurrence of the
  search term within the normalized character string version of the Metamath
  object. Comment searches are not case sensitive.

* RegExpr : uses the Java-defined version of regular expressions as defined at
  https://docs.oracle.com/javase/tutorial/essential/regex/index.html .
  Thus, "." means any character, "*" means 0 or more of the previous
  expression, "+" means 1 or more of the previous expression,
  parentheses group expressions, and "\." matches the period character.

* Metamath : very similar to the RegExpr format except that the Metamath
  Format uses the '$?' and '$*' wildcards instead of '.?' and '.*' --
  signifying 1 character of anything, and 0 or more characters or tokens of any
  value, respectively. When searching labels, '$?' and '$*' can be abbreviated
  to just '?' and '*'.
  
  You can use the FromChap, FromSec, ThruChap, and ThruSec
  to select only specific chapters and their sections to search.

  You can also select "ResetData" to reset a search (to start something new).

  So for example, after setting MaxTime to some reasonble time like 10,
  you could go to the first search data line and select Format "CharStr"
  and ForWhat "1 e. RR".  Then press Search, and you'll find some matching
  assertions.  You can close the search results window when you're done.

qed:: |- ( ph -> ph )

* Please go on to Page901.mmp.

$)