checker.doc.txt - comment block extracted from check4.ax (5-22-25 version)
  - overview documentation of the SAL proof checker

!/
  The check predicate has an original set of axioms and then "check steps"
  that prove valid clauses from those axioms and define new equivalent axiom
  subsets for the original axiom subsets.  Proofs are "inference proofs"
  that prove new valid clauses from previously-proved clauses or they are
  "induction proofs" that define a valid clause from a set of axioms.
  [(semi-formal) grammar notation:
     <item>  - an entity (from some category) in the proof expr to be checked
        - any symbol or atom w/o angle brackets is a keyword 
     ..<item>..  - string of zero or more occurences of <item>
     ..item..  - term w/o angle brackets denotes a string of symbols
     <item1> | ... | <itemk>  - one of these items occurs here
  ]

    (check
      (.. (<lblax> <ax>) | (<lblaxss> ..(<lblax> <ax>)..) ..)
         - initial labeled axioms and axiom subsets in original axiom set
           (axiom labels <lblax> and axiom subset labels <lblaxss> are unique
            for the axiom set)
         - axioms are encoded SAL clauses
           (the axioms are the initial valid clauses)
      (..<chk_step>..)          - sequence of "check steps"
         - each check step proves a valid clause or proves an alternate subset
      (.. (<lblax> | (`alt ..(<lblaxss> ..<lblax>..)..) ..)
         - final axiom set labels with possibly-added alternate equivalent
           axiom subsets
      (..(<lblc> <vcP>)..)  - final set of labeled valid clauses w PAL encoding 
         - the ax set axiom labels are indicies into this list
           (labels <lblc> for valid clauses are unique)
    )  - the ax set labels and proved valid clauses are output exprs
    <lblax>/<lblc> - [ax/]clause label symbol, starting w non-uppercase-letter
    <ax> = <cl> - an SAL encoded clause (<conc_expr> ..<cond_expr>..)
    <vcP> - a valid (axiom or proved) clause in PAL encoding
    <lblaxss> - ax subset label symbol, 1st char uppercase ltr, rest non-ucltr  
    <chk_step> =
      (<lblc> <cl> <lblvc> ..infer..)   - inference proof that clause is valid
          - <lblvc> initializes the "current valid clause" for inference proof
        ..infer.. =   - from a valid clause infer another valid clause
          c# <lblvch> ..infer..  - unfold current vc cond c# with another vc
                (or w induction hypothesis if proving an `ind unfold result)
        | <perm/add> ..infer..  - permute and optionally add vc conditions
          <perm/add> = sequence with permutation of cond #s with optional _'s
                       inserted for added conditions
        | <null>  - at end of inference proof, <cl> to be proved must be
                    instance of the current valid clause
      )
    | (<lblc> <cl> `ind <c#> <axsdef>  - induction unfold of cond wrt ax set
        [later!:  *** `hyp  -- hypothesized clauses can go here!? ***]
        ..(<lblc_lblax> <unfcl> ..proof..)..  - unfolded clauses & their proofs
           - ..proof.. can be an inference proof or a nested induction proof
           - Label of an (expected) unfolded clause is of the form prefix_lblax
             where lblax is label of axiom which yielded this clause.
             (Prefix makes the complete label unique for nested induction
              -- usually it's the label of the clause to be proved.)
      )
        c#  - decimal number 1.. of condition to be unfolded
        <axsdef> - symbol defining axiom set: _ or _..<lblaxss>..
           - underscore w/o any alt ax subset labels gets original subsets;
             if named ax subsets are given, those are used instead
           - Note that no matter what alternate axiom subsets are chosen,
             the set of generated valid exprs (and set of valid clauses)
             remains the same. 
        <unfcl> - encoded SAL representation of unfold result clause
    | (`axss             - def of an equivalent, alternate axiom subset
         - axioms of new subset have already been proved valid wrt orig subset
         <lbloaxss>      - name of old alt ax subset to be proved valid wrt new
         (<lblnaxss>     - name of new ax subset (not used elsewhere)
          ..<lblnax>..)  - labels of already-proved new axioms in new subset
             - each of these appears in list of labeled, proved valid clauses
         (.. <chk_step> ..)  - check steps to prove old ax valid wrt new subset
             - additional valid clauses needed for proofs can be proved here
      )  - at end of `axss block, the new ax subset will be appended to the
           list of alterntive subsets containing the old ax subset
         - Thus, the new ax subset will be equivalent to the old subset
           (when combined with all the other axioms of the complete ax set)

  Input clauses <ax>, <cl>, <unfcl> are textual encoded SAL.
  Valid clauses <vcP> are encoded PAL (with symbolic vars).  Later we convert
  <vcP>s to <vcPn>s with natural number 'varn's for convenient var renaming.
!\

overview of check predicate:
! check - check proofs of valid clauses derived from a set of axioms
! (check <axs>  - labeled axioms with labeled subsets (encoded SAL)
!        <chk_steps>  - check clause proof and equiv subset steps
!        <axsl>  - final ax set clause and subset labels
!        <lvcP>  - final labeled (axiom & proved) valid clauses (encoded PAL)
! )