Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2006-02-01 11:51:28 -0800 (Wed, 01 Feb 2006)
Revision: 8626
Log message:

      Addec cs136.
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2006-02-02 14:57:30 -0800 (Thu, 02 Feb 2006)
Revision: 8627
Log message:

      Defined BTerms as the basic terms, instead of defining it based on languages.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2006-02-05 11:35:56 -0800 (Sun, 05 Feb 2006)
Revision: 8629
Log message:

      Preparing to move "append sequents" to obsolete status.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2006-02-05 11:54:18 -0800 (Sun, 05 Feb 2006)
Revision: 8630
Log message:

      Moved append/flat sequents into theories/itt/reflection/obsolete_flat
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-02-06 17:14:11 -0800 (Mon, 06 Feb 2006)
Revision: 8631
Log message:

      Itt_bool does not depend on Itt_set.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-02-06 23:20:24 -0800 (Mon, 06 Feb 2006)
Revision: 8632
Log message:

      Minor optimization.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-02-07 00:00:50 -0800 (Tue, 07 Feb 2006)
Revision: 8633
Log message:

      Minor cleanup.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-02-07 18:30:59 -0800 (Tue, 07 Feb 2006)
Revision: 8640
Log message:

      Made the script a bit more flexible.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-02-07 19:25:53 -0800 (Tue, 07 Feb 2006)
Revision: 8642
Log message:

      Alexei & Aleksey:
      
      - Reformulated the dintersectionSubtype rule (it used to be incorrectly too
        strong) and derived it (it used to be a primitive axiom).
      
      - A little more progress reverifying ITT rules under pairwise functionality.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-02-07 21:23:33 -0800 (Tue, 07 Feb 2006)
Revision: 8643
Log message:

      Alexei & Aleksey:
      
      - Switching ITT core from pointwise to pairwise functionality!
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-02-08 00:56:20 -0800 (Wed, 08 Feb 2006)
Revision: 8644
Log message:

      - Fixed a rewriter bug uncovered by a recent change to let_rule rule.
      - Fixed proofs that were broken by a variable naming change in let_rule.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-02-08 02:05:45 -0800 (Wed, 08 Feb 2006)
Revision: 8645
Log message:

      *** Warning: breaks binary compatibility! ***
      
      Simplified and cleaned up the naming of bound variables when building
      contractum in the rewriter.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-02-08 14:58:34 -0800 (Wed, 08 Feb 2006)
Revision: 8647
Log message:

      Removing an outdated comment.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-02-08 20:20:49 -0800 (Wed, 08 Feb 2006)
Revision: 8649
Log message:

      - Changed the filter to add a "Perv!select_crw" label to all the annotations
        on conditional rewrites.
      
      - Added simpleReduceC that calls reduceC while ignoring the conditional
        rewrites.
      
      TODO:
      - Add the "select_crw" label to manual reduce adds (where approproate)
      
      - Try adding simpleReduceT to autoT with a higher priority than the regular
        reduceT (possibly even to AutoNormal and not just AutoComplete)
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-02-08 20:54:01 -0800 (Wed, 08 Feb 2006)
Revision: 8650
Log message:

      Minor variable naming fix.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-02-08 23:05:17 -0800 (Wed, 08 Feb 2006)
Revision: 8651
Log message:

      Small simplification of definitions.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-02-09 02:34:57 -0800 (Thu, 09 Feb 2006)
Revision: 8652
Log message:

      Minor improvements in reduce resource for the number theory

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-02-09 14:32:05 -0800 (Thu, 09 Feb 2006)
Revision: 8653
Log message:

      The way we had <= and >= defined with reduceT "randomly" turning >= into <=
      was a complete mess! To avoid this mess, I have defined le and le_bool as
      _iforms_ that automatically turn into corresponding ge/ge_bool. Ideally, they
      should be some sort of "soft IO abstractions" so that terms that are entered
      as <= will be displayed as <= (while being idential to >= from the POV of the
      formal rewriter) - see bug 256 and bug 261.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-02-09 14:36:49 -0800 (Thu, 09 Feb 2006)
Revision: 8654
Log message:

      Fixed a proof broken by the previous commit.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-02-09 21:32:41 -0800 (Thu, 09 Feb 2006)
Revision: 8657
Log message:

      Proven much stronger elimination rules for Image and union types.
      
      Note: this does break a few proofs in Itt_hoas_* theories. I will fix those
      over the weekend (and try to clean up them a bit - now that we are using
      pairwise functionality they can be done _much_ simpler).
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-02-09 23:16:10 -0800 (Thu, 09 Feb 2006)
Revision: 8658
Log message:

      - Implemented the splitNatT tactic that does case wplit (0 or not) for a
        natural number.
      
      - Added a missing item (the "not{m = n in nat}" hyp) to the appropriate
        arithT/omegaT resource (ge_elim).
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-02-10 00:44:18 -0800 (Fri, 10 Feb 2006)
Revision: 8659
Log message:

      Derived the itt_list theory!
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-02-10 01:04:26 -0800 (Fri, 10 Feb 2006)
Revision: 8660
Log message:

      Turns out that we do not really need the "weak reverse functionality" axiom
        list{'A} Type --> nil in list{'A} and it sufficient to have
        list{'A} --> nil in list{'A} in nthHypT.
      
      The latter form is actually derivable, so I was able to get rid of the only
      remaining prim rule in itt_list. Now itt_list is truly derived!
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2006-02-10 12:06:23 -0800 (Fri, 10 Feb 2006)
Revision: 8662
Log message:

      Added a missing comma in addsuffix, relevant to win32 only

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2006-02-10 12:10:10 -0800 (Fri, 10 Feb 2006)
Revision: 8663
Log message:

      Tiny typo

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2006-02-12 18:20:44 -0800 (Sun, 12 Feb 2006)
Revision: 8667
Log message:

      Working on .cmoz conversion.
      
      We discussed the following scheme for reflecting files:
      for an original (non-reflected) file foo.cmoz, we
      would generate a reflected file as foo_reflect.cmoz.
      
      However, the method has a problem, because the reflected
      theory includes ML code for resources.
      
      This is a pain.  Some options I see:
      
        1. Do not generate a separate file, but include the reflected
           code in the original foo.cmoz (with corresponding ML code in
           foo.cmo).
      
           Problem: it isn't modular, because you have to plan ahead
           for those files you want to reflect.  Also, you don't want the
           existence of theorems in the .cmoz to depend on how MetaPRL
           is configured.
      
           OTOH, if we _always_ generate reflected code, it is modular,
           with a cost.
      
        2. Provide tools:
      
              # Generates foo_reflect.cmi, foo_reflect.cmiz
              prlc --reflect foo_reflect foo.cmiz
      
              # Generates foo_reflect.cmo, foo_reflect.cmoz
              prlc --reflect foo_reflect foo.cmoz
      
           We would have to hack on omake:
              1. Make sure dependencies on _reflect files can be computed.
              2. Build the _reflect files automatically.
      
      I think option 2 is better _if_ it can be done.  The issue is that
      I'm not sure there is enough information in the .cm?z files to
      generate reflected theories.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2006-02-12 18:59:23 -0800 (Sun, 12 Feb 2006)
Revision: 8668
Log message:

      Fixed filter_bin--its been broken for a long time.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2006-02-12 19:15:43 -0800 (Sun, 12 Feb 2006)
Revision: 8669
Log message:

      Might as well fix the "convert" program too.
      This was the program that we could use externally
      to convert .prlb -> .prla.
      
      Not sure that it works, but we probably still
      want it.  It would be nice to be able to run
      "omake export" rather than trying to remember
      what files were changed.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-02-12 20:13:33 -0800 (Sun, 12 Feb 2006)
Revision: 8670
Log message:

      Reverted revisions 8657, 8659, and 8660. These revisions have made the
      elimination rule for the image type stronger than what is valid under pairwise
      functionality and used those invalid rules to derive the itt_list theory.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-02-12 21:06:24 -0800 (Sun, 12 Feb 2006)
Revision: 8671
Log message:

      Weakened the nilEquality axiom, replacing the 
      "type"{list{'A}} --> nil in list{'A}
      (which is a bit too srtong semantically) with weaker theorems of the form
      list{'A} --> list{'A}
      
      This was first added un rev 8660, but then reverted in rev 8670.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-02-12 22:41:00 -0800 (Sun, 12 Feb 2006)
Revision: 8672
Log message:

      Boolean rules should be producing asserts instead of boolean equalities.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-02-12 23:32:03 -0800 (Sun, 12 Feb 2006)
Revision: 8673
Log message:

      Maked a conditional rewrite in reduce resource.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-02-13 01:02:22 -0800 (Mon, 13 Feb 2006)
Revision: 8674
Log message:

      Using Itt_pairwise, proved stronger elimination rules for the image type (for
      the "reversible" case only - where the "transitive closure" does not add any
      equalities to the image type).
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-02-13 02:06:59 -0800 (Mon, 13 Feb 2006)
Revision: 8675
Log message:

      Derived itt_list from itt_union + itt_nat!
      
      This time it's using the weaker (pairwise-compatible) rules.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-02-13 02:44:17 -0800 (Mon, 13 Feb 2006)
Revision: 8676
Log message:

      "Strong" elimination rules (dprod, prod, disjoint union) should be formulated
      in thinning form; it should be up to the user and/or tactic to copy the hyp if
      it needs to be preserved (which is never the case in existing proofs).
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-02-13 02:45:50 -0800 (Mon, 13 Feb 2006)
Revision: 8677
Log message:

      Getting rid of gt and gt_bool operators - turning them into iforms for lt and
      lt_bool.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-02-13 02:49:22 -0800 (Mon, 13 Feb 2006)
Revision: 8678
Log message:

      Filled in the proofs (do we actually need this module?)

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-02-13 12:58:15 -0800 (Mon, 13 Feb 2006)
Revision: 8679
Log message:

      Annotated some manual adds to reduce as conditional rewrites.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-02-13 15:37:16 -0800 (Mon, 13 Feb 2006)
Revision: 8680
Log message:

      Getting rid of the Itt_hoas_lang theory (moving it to obsolete), deriving the
      BTerm type directly instead (this is 99.9% based on Xin's Itt_hoas_bterm1).
      
      Itt_hoas_bterm TODO:
       - the theory is in need of a major clean-up.
       - it needs to be well-commented.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-02-13 16:57:51 -0800 (Mon, 13 Feb 2006)
Revision: 8681
Log message:

      The previos commit broke a few proofs, fixing.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-02-13 17:43:09 -0800 (Mon, 13 Feb 2006)
Revision: 8683
Log message:

      Adding reduce_vsubst_dummy_null to reduce.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-02-13 19:16:59 -0800 (Mon, 13 Feb 2006)
Revision: 8686
Log message:

      Simplified the Itt_vec_sequent_term theory a bit.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-02-13 21:19:31 -0800 (Mon, 13 Feb 2006)
Revision: 8687
Log message:

      Another small simplification (trying to make sure that rewrites do not have
      unnecessary redices on the LHS as it can make it harder to apply them).
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-02-13 21:45:53 -0800 (Mon, 13 Feb 2006)
Revision: 8688
Log message:

      - Removing a duplicate rule: Itt_vec_sequent_term.reduce_nth_of_list_of_fun was
      the exact same thing as Itt_list2.nth_map_list_of_fun.
      
      - The name of this theorem in Itt_list2 was very weird (which is probaly the
      reason why Jason have missed it). Renamed it into nth_of_list_of_fun.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-02-13 22:06:34 -0800 (Mon, 13 Feb 2006)
Revision: 8689
Log message:

      Adding hyps_length_null to reduce

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-02-13 22:29:46 -0800 (Mon, 13 Feb 2006)
Revision: 8690
Log message:

      Swapped reduce_hyps_flatten_bind_nil1 and reduce_hyps_flatten_bind_nil2
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-02-14 02:20:49 -0800 (Tue, 14 Feb 2006)
Revision: 8691
Log message:

      - Added nth_hyp annotations to _lots_ of rules (especially in the algerba
        theory).
      
      - Made the nthHypT a bit safer (it used to be the case that something like
        'l in list{'A} --> 'l in list{top} may loop nth_hyp).
      
      - Made nthHypT and Itt_struct.nthAssumT more efficient (by making sure they do
        not create unnecessary ruleboxes).
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-02-14 13:31:09 -0800 (Tue, 14 Feb 2006)
Revision: 8692
Log message:

      Removed Itt_hoas_lang from the list of the printed theories.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-02-14 13:31:46 -0800 (Tue, 14 Feb 2006)
Revision: 8693
Log message:

      Slightly more efficient nthHypT and Itt_struct.nthAssumT

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-02-14 15:13:21 -0800 (Tue, 14 Feb 2006)
Revision: 8694
Log message:

      Term_match_table: use options instead if Not_found exceptions to communicate
      whether the lookup was successful. This is more efficient, safer (as it makes
      it impossible to forget to test for Not_found), and the code is sligtly
      simpler.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-02-14 16:03:53 -0800 (Tue, 14 Feb 2006)
Revision: 8696
Log message:

      Removing a duplicate rule.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-02-14 18:11:39 -0800 (Tue, 14 Feb 2006)
Revision: 8697
Log message:

      Minor intro resource annotation change

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2006-02-14 18:49:24 -0800 (Tue, 14 Feb 2006)
Revision: 8699
Log message:

      Added the template for reflecting theories from the .cmoz file.
      The only thing handled at the moment are the "extends" directives.
      
      The reflected theory for a theory Foo is named Reflect_foo.
      
      Whew, this wasn't easy.
      
         - Filter_cache_fun has an issue with loading "summarized"
           modules.  A "summarized" module is formed when a module
           is loaded.  If another "extends" for that theory is
           encountered, then the module is loaded from the
           summary.  In other words, the file is cached.
      
           Unfortunately, this is very damaged.  The only thing
           included from a cached file is the opnames.
           The other stuff, like resources and grammars, are ignored.
      
           This should be fixed.  In the meantime, I added a
           "reset_hack" function that resets the cache.  This is
           expensive, and should be removed asap.
      
         - For the moment, I'm hand-coding the dependencies for
           reflected files.
      
           Unfortunately, this is broken.  If you add an explicit
           dependency to theories/foo/OMakefile.  For example,
           the following dependency seems like it should work.
      
               reflect_x.cmoz: x.cmoz
      
           However reflect_x.cmoz will be compiled _without_
           OCAMLINCLUDES being defined to include THEORY_DEPS.
           In fact, it won't even include meta/base:(
      
           Again, this should be fixed.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-02-14 19:04:05 -0800 (Tue, 14 Feb 2006)
Revision: 8700
Log message:

      Small resource update.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2006-02-14 19:17:10 -0800 (Tue, 14 Feb 2006)
Revision: 8701
Log message:

      Doh,
      
      In the middle of all the other files, I saw
      
         D filter_reflect.ml
      
      but this should be A, not D!
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-02-14 19:55:29 -0800 (Tue, 14 Feb 2006)
Revision: 8702
Log message:

      Adding a temporary hack to account for the fact that reflected theories have
      no scanner.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-02-14 20:32:58 -0800 (Tue, 14 Feb 2006)
Revision: 8703
Log message:

      MLZFILES should be symlinked before scanning for dependencies.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-02-14 21:46:35 -0800 (Tue, 14 Feb 2006)
Revision: 8704
Log message:

      All the reflected theories depend on itt_hoas_theory.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-02-14 22:59:08 -0800 (Tue, 14 Feb 2006)
Revision: 8705
Log message:

      - Filter_reflection: module names should not be capitalized.
      
      - OMakefile_theories: rules for generating .p4 and .p4i for the reflected
        theories (these are pretty-printed versions of the generated OCaml code;
        useful for debugging the filter).
      
      - OMakefile_theories: in rev 8704 I've ordered the new dependencies for the
        reflect_% files incorrectly (the theory .SUBDIRS did not have them in
        scope); fixed.
      
      - Filter_prog: generate the show_loading debugging call at the beginning and
        end of every theory.
      
      - A _huge_ number of theory files: removed the manual "show_loading" calls as
        they will now be automatically generated.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-02-15 00:23:38 -0800 (Wed, 15 Feb 2006)
Revision: 8706
Log message:

      Fixing a typo.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-02-15 01:01:48 -0800 (Wed, 15 Feb 2006)
Revision: 8707
Log message:

      Making the nth_hyp resource a bit more precise.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-02-15 02:01:30 -0800 (Wed, 15 Feb 2006)
Revision: 8708
Log message:

      Adding conjunction elimination to the nth_hyp resource.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-02-15 03:25:50 -0800 (Wed, 15 Feb 2006)
Revision: 8709
Log message:

      Making the nth_hyp annotation processor slightly more precise

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-02-15 05:16:18 -0800 (Wed, 15 Feb 2006)
Revision: 8710
Log message:

      Exposing the "in_auto" function in the interface.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-02-15 06:26:48 -0800 (Wed, 15 Feb 2006)
Revision: 8711
Log message:

      Added a few nth_hyp annotations

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-02-15 12:48:45 -0800 (Wed, 15 Feb 2006)
Revision: 8712
Log message:

      We do not need this OMakefile (it duplicates a part of the code that I've
      added to the root OMakefile_theories).
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-02-15 13:38:54 -0800 (Wed, 15 Feb 2006)
Revision: 8713
Log message:

      Keep the pnm_core_logic in the default build for now.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-02-15 16:34:26 -0800 (Wed, 15 Feb 2006)
Revision: 8714
Log message:

      Adding squash{compatible_shapes{...}} to the elim resource.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-02-15 18:37:19 -0800 (Wed, 15 Feb 2006)
Revision: 8715
Log message:

      Better usage of bySubtypeT.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-02-15 21:54:18 -0800 (Wed, 15 Feb 2006)
Revision: 8716
Log message:

      Negation is squash-stable (when well-typed).
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-02-15 23:04:08 -0800 (Wed, 15 Feb 2006)
Revision: 8717
Log message:

      - Added an AutoOK option to elim rule annotations. The rules marked with
        AutoOK will now be used by AutoNormal phase of autoT. The default for the
        elimination rules, as before, is to only use then in the AutoComplete phase.
      
      - Marked select elimination rules with AutoOK. In particular, the rules like
        and_elim and exists_elim are now marked with AutoOK, which eliminated the
        need to have a separate auto_logicT in autoT, which was a completely ad-hoc
        non-modular non-compositional way of decomposing certain hyps during the
        AutoNormal phase of autoT.
      
      - Improved the "relation" of the squash/unsuqash tactics and autoT. In
        particular, the unsquashing of the squash-stable conclusions will now happen
        during the AutoNormal phase (when the conclusion is _not_ squash-stable, it
        will only happen in the AutoComplete phase).
      
      This significantly speeds up status_all ( > 15%) and reduced the size of the
      PNM proofs (>20%).
        
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-02-15 21:54:18 -0800 (Wed, 15 Feb 2006)
Revision: 8716
Log message:

      Negation is squash-stable (when well-typed).
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-02-15 23:04:08 -0800 (Wed, 15 Feb 2006)
Revision: 8717
Log message:

      - Added an AutoOK option to elim rule annotations. The rules marked with
        AutoOK will now be used by AutoNormal phase of autoT. The default for the
        elimination rules, as before, is to only use then in the AutoComplete phase.
      
      - Marked select elimination rules with AutoOK. In particular, the rules like
        and_elim and exists_elim are now marked with AutoOK, which eliminated the
        need to have a separate auto_logicT in autoT, which was a completely ad-hoc
        non-modular non-compositional way of decomposing certain hyps during the
        AutoNormal phase of autoT.
      
      - Improved the "relation" of the squash/unsuqash tactics and autoT. In
        particular, the unsquashing of the squash-stable conclusions will now happen
        during the AutoNormal phase (when the conclusion is _not_ squash-stable, it
        will only happen in the AutoComplete phase).
      
      This significantly speeds up status_all ( > 15%) and reduced the size of the
      PNM proofs (>20%).
        
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-02-16 17:14:24 -0800 (Thu, 16 Feb 2006)
Revision: 8718
Log message:

      Now that > and <= are iforms, we should not have a separate omegaT entries for
      them in the intro resource.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2006-02-16 18:12:12 -0800 (Thu, 16 Feb 2006)
Revision: 8719
Log message:

      Temporarily removed Aleksey's reflection dependency code.
      It doesn't hold for reflect_base_theory.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-02-17 01:31:53 -0800 (Fri, 17 Feb 2006)
Revision: 8720
Log message:

      Symlinks for .mlz should not a part of the repository.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2006-02-17 12:16:46 -0800 (Fri, 17 Feb 2006)
Revision: 8722
Log message:

      Working on dependencies and despagettification of ocamldep.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-02-17 12:18:09 -0800 (Fri, 17 Feb 2006)
Revision: 8723
Log message:

      Ignore the reflect_base_theory.{ml,mli} symlinks.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-02-17 12:45:52 -0800 (Fri, 17 Feb 2006)
Revision: 8724
Log message:

      Fixing a typo.
      

Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2006-02-17 15:18:29 -0800 (Fri, 17 Feb 2006)
Revision: 8725
Log message:

      Defined set and squash types using image type.
      
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-02-17 15:47:58 -0800 (Fri, 17 Feb 2006)
Revision: 8726
Log message:

      Now that the squash is a defined operator and not a postulated one, I am a bit
      uncomfortable using it in the esquash axioms. The problem is that definitions
      tend to change once in a while and it's better not to have to rely on a them
      not changing in a way that would invalidate the seemingly unrelated axioms.
      
      This changes the equash axioms slightly, so that they do not refer to squash
      operator and the rules squash-related rule are now all derived.
      
      Alexei Kopylov have reviewed the changes to esquash axioms.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-02-17 16:07:14 -0800 (Fri, 17 Feb 2006)
Revision: 8727
Log message:

      The squash resource should not rely on dT 0.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-02-17 17:49:50 -0800 (Fri, 17 Feb 2006)
Revision: 8730
Log message:

      Reducing constant inequalities in intro and elim was implemented a bit badly. For
      example, if we had a hyp of the form "1 >= 0", elim would reduce it to
      "assert{bnot{bfalse}}" and a subsequent elim would then eliminate the bnot,
      potentially replacing a provable conclusion with an unprovable
      "assert{bfalse}" (Oops!).
      

Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2006-02-17 18:08:41 -0800 (Fri, 17 Feb 2006)
Revision: 8731
Log message:

      1. Added a new tactic
         splitHypT i j
      that "splits" i'th hypothesis and put a new copy to the j'th place.
      It similar to copyHypT, but afrer splitT all hypotethes after the new copy will depend on the new copy instead of the old one.
      
      2. Change elimination rule for image to match one in the paper.
      
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-02-17 18:29:06 -0800 (Fri, 17 Feb 2006)
Revision: 8733
Log message:

      Added ' 'a='b in nat --> 'a in int ' and ' 'a='b in nat --> 'b in int ' to
      nth_hyp.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-02-18 20:12:12 -0800 (Sat, 18 Feb 2006)
Revision: 8734
Log message:

      Removing a redundant rule (should have been removed when gt became an iform
      for lt).
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-02-18 20:24:01 -0800 (Sat, 18 Feb 2006)
Revision: 8735
Log message:

      Adding ' n in nat >- n >= 0' to the nth_hyp resource.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2006-02-19 13:27:32 -0800 (Sun, 19 Feb 2006)
Revision: 8736
Log message:

      Finished despaghettification of ocamldep.mll.
      Also added dependencies for reflection files.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-02-19 16:12:41 -0800 (Sun, 19 Feb 2006)
Revision: 8738
Log message:

      Use simpleReduceT instead of "rw reduceC 0" before omegaT in intro.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2006-02-19 16:58:48 -0800 (Sun, 19 Feb 2006)
Revision: 8739
Log message:

      Added reflection conversion for term declarations.
      
      TODO:
         1. Convert rules
         2. Add the postprocessing (the part that adds
            the elimination rule, etc).
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2006-02-19 18:58:17 -0800 (Sun, 19 Feb 2006)
Revision: 8740
Log message:

      Add the other reflected theorems, including the elimination rule.
      
      Dependency analysis seems to be failing.  I'll see...
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2006-02-19 20:30:25 -0800 (Sun, 19 Feb 2006)
Revision: 8741
Log message:

      Boo, I have no idea why the dependencies for reflected files
      are not accurate.  The dependencies look good, the order of
      compilation looks good, but OCaml reports a dependency error...
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-02-19 23:00:23 -0800 (Sun, 19 Feb 2006)
Revision: 8742
Log message:

      A few nth_hyp annotations in reflected theories.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2006-02-20 11:41:01 -0800 (Mon, 20 Feb 2006)
Revision: 8743
Log message:

      Doh, the dependency problem was because OCaml uses the filename to
      determine the module name.
      
      So, instead of generating reflect_%.cmi in one step from %.cmiz, generate
      reflect_%.ppi first, then compile it to get the reflect_%.cmi.  This will
      make sure OCaml sees the right filename.
      
      Also, use :squash: %.ml in the original implicit rules to avoid forced
      recompiles when the %.ml file changes.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2006-02-20 11:49:42 -0800 (Mon, 20 Feb 2006)
Revision: 8744
Log message:

      Minor cleanup.  Remove ReflectC from mk/prlcomp.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2006-02-20 13:01:58 -0800 (Mon, 20 Feb 2006)
Revision: 8745
Log message:

      Oops, it looks like target_is_buildable does not
      work with :squash: dependencies.
      
      Resurrecting %.ml as normal dependencies for the moment.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-02-20 16:08:50 -0800 (Mon, 20 Feb 2006)
Revision: 8746
Log message:

      - Changed bneq_int into an iform.
      - Added fold_neq_int to reduce.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-02-20 18:44:20 -0800 (Mon, 20 Feb 2006)
Revision: 8747
Log message:

      - Added an elimination rule for the neq_int proposition.
      - Cleaned up some of the proof error messages caused by my previous commit.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2006-02-20 20:07:46 -0800 (Mon, 20 Feb 2006)
Revision: 8749
Log message:

      Squash the .ml dependencies
         %.cmo: %.ppo :squash: %.ml
      
      This is conditional on omake 0.9.6.8.1
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-02-20 20:28:52 -0800 (Mon, 20 Feb 2006)
Revision: 8750
Log message:

      No-op API change - added "wrap_elim_auto_ok".
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2006-02-20 21:26:14 -0800 (Mon, 20 Feb 2006)
Revision: 8751
Log message:

      Added var_elim3 for special case, noticed by Aleksey Nogin

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2006-02-20 21:40:19 -0800 (Mon, 20 Feb 2006)
Revision: 8752
Log message:

      I've been trying to prove a better elimination rule. I think provable_elim1
      better resembles what we need in pmn_core_terms. However, no matter how I tried,
      I always came across a well-formedness assumption (w: ty; ... => C[w] Type).
      
      So is the rule statement wrong? Or is this really what we need?
      
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-02-20 21:46:14 -0800 (Mon, 20 Feb 2006)
Revision: 8753
Log message:

      For hypothesis of the form "x: int", "x: nat", "x: BTerm", etc, where "x" does
      not occur anywhere, dT should simply thin out such a hypothesis, instead of
      trying to preform meaningless induction. This thinning should happen in
      AutoNormal.
      
      I've added a new option to elim annotations - annotating a rule with 
      "elim [ThinFirst thinT]" would cause dT to first try thinning out any matching
      hypothesis, and only apply the annotated rule when the corresponding variable
      is actually used somewhere.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-02-20 22:13:23 -0800 (Mon, 20 Feb 2006)
Revision: 8754
Log message:

      Increasing the priority of a few elim resource entries
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-02-20 22:28:47 -0800 (Mon, 20 Feb 2006)
Revision: 8755
Log message:

      Expose d_elim_prec.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-02-20 23:02:40 -0800 (Mon, 20 Feb 2006)
Revision: 8756
Log message:

      Proved the Itt_hoas_proof_ind.provable_elim1. I've used pairwise functionality
      here to simplify the proof slightly, but this is not necessary as list{BTerm}
      is a sqsimple type.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-02-21 00:12:28 -0800 (Tue, 21 Feb 2006)
Revision: 8758
Log message:

      The unit elimination rule should thin.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-02-21 00:36:03 -0800 (Tue, 21 Feb 2006)
Revision: 8759
Log message:

      Added " a = b in nat --> b = a in int " to the nth_hyp resource.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-02-21 00:55:58 -0800 (Tue, 21 Feb 2006)
Revision: 8760
Log message:

      Small optimization (a follow-up to my previous commit).
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-02-21 01:12:08 -0800 (Tue, 21 Feb 2006)
Revision: 8761
Log message:

      Thin out useless BTerm{'i}, BSequentCore and BSequentCore{'i} hypotheses.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-02-21 01:41:56 -0800 (Tue, 21 Feb 2006)
Revision: 8762
Log message:

      Another nth_hyp improvement.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2006-02-21 11:12:37 -0800 (Tue, 21 Feb 2006)
Revision: 8763
Log message:

      The rule generation code should use second-order variables for the logic.
      
      Added a dummy file Itt_hoas_sequent_elim.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2006-02-21 11:25:23 -0800 (Tue, 21 Feb 2006)
Revision: 8764
Log message:

      Intermediate commit while I rename the files.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2006-02-21 11:32:16 -0800 (Tue, 21 Feb 2006)
Revision: 8765
Log message:

      Use new method of generating reflected theories.
      
      NOTE: I'll probably delete the reflection code in Filter_parse soon.
      Let me know if you still want it.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-02-21 11:45:31 -0800 (Tue, 21 Feb 2006)
Revision: 8766
Log message:

      This adds the simpleReduceT tactic to autoT on AutoNormal level.
      
      This noticeably speeds up the "status_all" and significantly reduces the size
      of reflection proofs:
      
        Expanding `intro_term_Apply':
        -Status: /pmn_core_terms/intro_term_Apply is a derived object with a complete proof (1 rule boxes, 16071 primitive steps)
        +Status: /pmn_core_terms/intro_term_Apply is a derived object with a complete proof (1 rule boxes, 9430 primitive steps)
        Expanding `intro_term_Lambda':
        -Status: /pmn_core_terms/intro_term_Lambda is a derived object with a complete proof (1 rule boxes, 37250 primitive steps)
        +Status: /pmn_core_terms/intro_term_Lambda is a derived object with a complete proof (1 rule boxes, 23894 primitive steps)
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2006-02-21 14:22:44 -0800 (Tue, 21 Feb 2006)
Revision: 8767
Log message:

      For reflect_ theories, allow dependencies for reflect_theory.suffix
      to be computed based on the presence of file theory.suffix.
      
      A comment:
       * XXX: JYH: this is bogus, because the reflect_* theories do not
       * need to be placed in the same directory as the original files.
       * However, it is difficult to decide what to do otherwise, and
       * this will work in all the cases we are currently considering.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2006-02-21 15:20:50 -0800 (Tue, 21 Feb 2006)
Revision: 8768
Log message:

      Minor efficiency cleanup.
      

Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2006-02-21 19:09:50 -0800 (Tue, 21 Feb 2006)
Revision: 8769
Log message:

      1. Defined singleton using the Image type.
      2. Added complete_if_member which is dual to complete_unless_member
      
      

Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2006-02-21 19:45:24 -0800 (Tue, 21 Feb 2006)
Revision: 8770
Log message:

      Fixed some source display forms

Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2006-02-21 19:54:18 -0800 (Tue, 21 Feb 2006)
Revision: 8771
Log message:

      Updated some documentation
      
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2006-02-21 20:05:06 -0800 (Tue, 21 Feb 2006)
Revision: 8772
Log message:

      This version, rather than having Reflect_foo extend Foo,
      just copies the terms from Foo into Reflect_foo verbatim.
      
      Otherwise, there is no logical relation between the
      theories.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-02-22 00:34:05 -0800 (Wed, 22 Feb 2006)
Revision: 8773
Log message:

      Tiny progress towards the elimination tactic.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2006-02-22 10:32:21 -0800 (Wed, 22 Feb 2006)
Revision: 8774
Log message:

      Simplify the elimination rule by omitting dependencies on the proof
      itself.
      
         <H>; v: 'ty; x: ProvableSequent{'logic; 'A['v]}; <J['v; 'x]> >- 'C['v]
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2006-02-22 15:36:17 -0800 (Wed, 22 Feb 2006)
Revision: 8775
Log message:

      exists_list_elim shouldn't have 'i as one of the arguments.
      

Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2006-02-22 16:02:23 -0800 (Wed, 22 Feb 2006)
Revision: 8776
Log message:

      Fixed proofs broken by my last commit

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-02-22 18:00:39 -0800 (Wed, 22 Feb 2006)
Revision: 8777
Log message:

      Minor improvements to rule statements generated by filter_reflection:
      
      - Use C<|J; H|> in place of C<|H; J|> as this would cause the display
        mechanism to hide these contexts in more cases.
      
      - Add labels on some of the rule assumptions:
        - MemLogic rules: 
           - "wf" on "logic in Logic" assumption
        - Intro rules:
           - "aux" on "logic in Logic" and "SubLogic{rule; logic}" assumptions
           - "wf" on type-checking assumptions
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-02-22 18:38:37 -0800 (Wed, 22 Feb 2006)
Revision: 8778
Log message:

      Adding the missing wf assumption to the elimination rule.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2006-02-22 18:48:23 -0800 (Wed, 22 Feb 2006)
Revision: 8779
Log message:

      Removed the reflection code from Filter_parse.
      
      Did not remove Filter_reflection from the camlp4* processors.
      It is nice to be able to define quotations that call into
      Filter_reflection.
      
      Did not remove poplmark/naive_old.  I'll delete it soon, but I still
      need to copy some code from it.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-02-23 13:09:19 -0800 (Thu, 23 Feb 2006)
Revision: 8780
Log message:

      Small proofRuleAuxWFT optimization,
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2006-02-23 19:01:26 -0800 (Thu, 23 Feb 2006)
Revision: 8781
Log message:

      Copy display forms to reflected theories.  The display forms
      clearly need some work, but they will do for now.
      
         - quote the redex
         - wrap the contractum in reflect_df{'def} for mk_term,
           and reflect_df{'d; 'def} for mk_bterm.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2006-02-23 19:05:57 -0800 (Thu, 23 Feb 2006)
Revision: 8782
Log message:

      Add display forms for judgments too.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2006-02-23 20:27:09 -0800 (Thu, 23 Feb 2006)
Revision: 8783
Log message:

      Working on reflecting more stuff.
      
      It isn't clear whether grammars should be included in a reflected theory.
      In any case, we can postpone for now.
      
      However, at least the original theory should be able to define a grammar.
      Then we get weird stuff in the original theory like:
      
         declare tok_foo : Terminal
         define iform succ{'x} <--> 'x +@ 1
      
      From the point of view of the reflected logic, we want to ignore this
      junk.
      
      I think the only thing that can't be easily filtered out is the "declare
      tok_foo : Terminal".  I don't like filtering based on the semantic info--
      I prefer filtering based on syntactic info...
      
      Would we be willing to define a new shapeclass, and define tokens in
      the following way (rather than the way we do now)?
      
         declare token tok_foo
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-02-24 15:54:39 -0800 (Fri, 24 Feb 2006)
Revision: 8784
Log message:

      Added assert(bnot(a >=@ b)) to the ge_elim resource.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-02-24 18:49:31 -0800 (Fri, 24 Feb 2006)
Revision: 8785
Log message:

      Some helper lemmas for the elimination proof. Unfortunately the
      step_union_logic_elim rule is not provable as is - we either need a bunch of
      extra wf conditions (which would be unfortunate), or we need to strengthen the
      SimpleStep definition to include those wf conditions (which is my current
      plan).
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-02-26 12:22:49 -0800 (Sun, 26 Feb 2006)
Revision: 8786
Log message:

      - Allow nth_hyp annotations on forward-chaining rules that do not have wf
        subgoals.
      
      - Added nth_hyp annotations on bunch of forward-chaining rules in HOAS theory
      
      - Proved several rules like "t in BSequent --> t in BTerm" and added them to
        nth_hyp.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-02-26 12:56:33 -0800 (Sun, 26 Feb 2006)
Revision: 8787
Log message:

      - Changed the definition of the SimpleStep predicate to include the wf
        conditions for the subterms.
      
      - Proved the Itt_hoas_proof_ind.step_union_logic_elim rule.
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2006-02-27 13:54:38 -0800 (Mon, 27 Feb 2006)
Revision: 8792
Log message:

      The main subgoal of omegaT is completed by omegaT itself (it used to be deligated to autoT).
      it still uses simpleReduceC, Aleksey, do you want me to replace it with specific rewrites? 

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-02-27 16:31:15 -0800 (Mon, 27 Feb 2006)
Revision: 8793
Log message:

      Perv.bind should be polymorphic.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-02-27 18:23:10 -0800 (Mon, 27 Feb 2006)
Revision: 8794
Log message:

      Removing a theorem that is not too useful.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-02-27 20:30:35 -0800 (Mon, 27 Feb 2006)
Revision: 8795
Log message:

      Wrote a tactic that would apply hypC (or revHypC) to the whole goal sequent,
      as appropriate and added it to the elim resource.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-02-27 21:31:55 -0800 (Mon, 27 Feb 2006)
Revision: 8796
Log message:

      - Defined a new suffic "ta" that stands for "thenT autoT"
      - Replaced "thenT autoT", "thenWT autoT", "thenAT autoT" with "ta", "twa",
        "taa" respectively in all the *.prla and *.ml in theories.