Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2006-01-08 21:01:22 -0800 (Sun, 08 Jan 2006)
Revision: 8431
Log message:

      Ok, enough for now.  The basic rules in Pmn_core_terms are proved.
      
      Forward-chaining has the following problem--a forward chaining
      rule might introduce a wf subgoal that would normally be proved
      by forward chaining on a later hyp.  Using forward chaining on
      the wf subgoal will result in a loop.  NOTE: wrt forward chaining,
      this is a major issue.
      
      For the moment, I added precedences to the forward chainer.  This
      is only a temporary fix.
      
      Added a fair number of new rules.  This is ad-hoc at the moment.
      Basically, I just see what isn't proved, and I add the appropriate
      theorems.  I'm not sure if we can make this systematic, but we
      should think about it.
      
      All rules in Pmn_core_terms are proved, but just *look* at the stats!
      500k primitive steps is totally--umm--amazing/terrible etc.
      Time for expand_all ():
         User time 293.000000; System time 2.820000; Real time 340.365773
      
         Refiner status:
            wf_term_TyTop
            is a derived object with a complete grounded proof (1 rule boxes, 3164 primitive steps, 248 dependencies)
         Refiner status:
            wf_term_TyFun
            is a derived object with a complete grounded proof (1 rule boxes, 15765 primitive steps, 249 dependencies)
         Refiner status:
            wf_term_TyAll
            is a derived object with a complete grounded proof (1 rule boxes, 35857 primitive steps, 254 dependencies)
         Refiner status:
            wf_Types
            is a derived object with a complete grounded proof (1 rule boxes, 38 primitive steps, 260 dependencies)
         Refiner status:
            mem_term_TyTop_Types
            is a derived object with a complete grounded proof (1 rule boxes, 101 primitive steps, 264 dependencies)
         Refiner status:
            mem_term_TyFun_Types
            is a derived object with a complete grounded proof (1 rule boxes, 103 primitive steps, 264 dependencies)
         Refiner status:
            mem_term_TyAll_Types
            is a derived object with a complete grounded proof (1 rule boxes, 105 primitive steps, 264 dependencies)
         Refiner status:
            intro_term_TyTop
            is a derived object with a complete grounded proof (1 rule boxes, 14782 primitive steps, 295 dependencies)
         Refiner status:
            intro_term_TyFun
            is a derived object with a complete grounded proof (1 rule boxes, 254485 primitive steps, 295 dependencies)
         Refiner status:
            intro_term_TyAll
            is a derived object with a complete grounded proof (1 rule boxes, 491120 primitive steps, 300 dependencies)