[kopylov] Allow sequents with non_zero depth._Sat Apr 1 13:07:38 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-04/2006-04-01-13-07-38-421623000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-04/2006-04-01-13-07-38-421623000-PST.html[nogin] Filter_reflection follow_up to Alexei_s previous commit._Sat Apr 1 13:24:51 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-04/2006-04-01-13-24-51-807237000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-04/2006-04-01-13-24-51-807237000-PST.html[kopylov] Fixed some broken proofs._Sat Apr 1 13:35:58 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-04/2006-04-01-13-35-58-872045000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-04/2006-04-01-13-35-58-872045000-PST.html[nogin] Couple of minor optimizations._Sat Apr 1 13:52:17 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-04/2006-04-01-13-52-17-476794000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-04/2006-04-01-13-52-17-476794000-PST.html[nogin] Moved couple of lemmas from itt_list_sloppy to itt_nat._Sat Apr 1 14:28:54 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-04/2006-04-01-14-28-54-434782000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-04/2006-04-01-14-28-54-434782000-PST.html[xiny] Modified the sequent_bterm forward rule._Sat Apr 1 16:20:05 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-04/2006-04-01-16-20-05-143274000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-04/2006-04-01-16-20-05-143274000-PST.html[xiny] Added 2 nth_hyp rules._Sat Apr 1 17:24:28 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-04/2006-04-01-17-24-28-887013000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-04/2006-04-01-17-24-28-887013000-PST.html[kopylov] Now I define Sequent____ Sequent_0_. I did not make it as iform, because it would break a lot of proofs_Sat Apr 1 22:54:08 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-04/2006-04-01-22-54-08-940451000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-04/2006-04-01-22-54-08-940451000-PST.html[xiny] Fully proved the test rule in Pmn_core_terms_test._Sun Apr 2 00:10:32 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-04/2006-04-02-00-10-32-990816000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-04/2006-04-02-00-10-32-990816000-PST.html[kopylov] Fixed a broken proof_Sun Apr 2 00:37:05 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-04/2006-04-02-00-37-05-390101000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-04/2006-04-02-00-37-05-390101000-PST.html[kopylov] Proved two simple theorems_Sun Apr 2 00:47:17 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-04/2006-04-02-00-47-17-663043000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-04/2006-04-02-00-47-17-663043000-PST.html[kopylov] Fixed the last broken proof_Sun Apr 2 00:49:15 PST 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-04/2006-04-02-00-49-15-787897000-PST.html
http://svn.metaprl.org/commitlogs/metaprl/2006-04/2006-04-02-00-49-15-787897000-PST.html[nogin] Minor optimization in autoT._Sun Apr 2 15:35:46 PDT 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-04/2006-04-02-15-35-46-608897000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2006-04/2006-04-02-15-35-46-608897000-PDT.html[nogin] Small optimization of the elim part of autoT._Sun Apr 2 18:08:11 PDT 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-04/2006-04-02-18-08-11-547572000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2006-04/2006-04-02-18-08-11-547572000-PDT.html[nogin] Another _elim in autoT_ optimization._Sun Apr 2 19:41:40 PDT 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-04/2006-04-02-19-41-40-161317000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2006-04/2006-04-02-19-41-40-161317000-PDT.html[nogin] autoT_ split the reduceT step into two_ _rw reduceC 0_ and _reduceHypsT_ and_Sun Apr 2 20:42:01 PDT 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-04/2006-04-02-20-42-01-805423000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2006-04/2006-04-02-20-42-01-805423000-PDT.html[nogin] Added equalityElimination rule _which postulates that any witness for an_Sun Apr 2 21:06:33 PDT 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-04/2006-04-02-21-06-33-908553000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2006-04/2006-04-02-21-06-33-908553000-PDT.html[nogin] Added bterm_neq_var and var_neq_bterm to the elim resource as Xin requested._Sun Apr 2 21:18:11 PDT 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-04/2006-04-02-21-18-11-043173000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2006-04/2006-04-02-21-18-11-043173000-PDT.html[nogin] _ Forward_ allow forward_chaining rules to thin the original hyp._Sun Apr 2 21:51:44 PDT 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-04/2006-04-02-21-51-44-512569000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2006-04/2006-04-02-21-51-44-512569000-PDT.html[nogin] Follow some forward_chaining rules by an appropriate reduceC to simplify the arithmetic in_Mon Apr 3 02:12:24 PDT 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-04/2006-04-03-02-12-24-462755000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2006-04/2006-04-03-02-12-24-462755000-PDT.html[nogin] Wrote another elimination tactic._Mon Apr 3 02:55:30 PDT 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-04/2006-04-03-02-55-30-353384000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2006-04/2006-04-03-02-55-30-353384000-PDT.html[nogin] We no longer need reduceC in the forward_chainer._Mon Apr 3 04:48:23 PDT 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-04/2006-04-03-04-48-23-513210000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2006-04/2006-04-03-04-48-23-513210000-PDT.html[nogin] For rules that already have an nth_hyp annotation, the elim annotation is_Mon Apr 3 16:49:31 PDT 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-04/2006-04-03-16-49-31-642588000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2006-04/2006-04-03-16-49-31-642588000-PDT.html[nogin] Wrote another elimination tactic._Mon Apr 3 19:07:03 PDT 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-04/2006-04-03-19-07-03-934261000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2006-04/2006-04-03-19-07-03-934261000-PDT.html[nogin] Working on elimination tactics, made some progress._Mon Apr 3 20:31:55 PDT 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-04/2006-04-03-20-31-55-643249000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2006-04/2006-04-03-20-31-55-643249000-PDT.html[nogin] I finally figured out why I was getting these weird linking errors with_Mon Apr 3 20:58:49 PDT 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-04/2006-04-03-20-58-49-029391000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2006-04/2006-04-03-20-58-49-029391000-PDT.html[nogin] More progress with the elimination tactic._Mon Apr 3 21:00:37 PDT 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-04/2006-04-03-21-00-37-825467000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2006-04/2006-04-03-21-00-37-825467000-PDT.html[nogin] Fixed the forwardChainT bug that Xin found._Mon Apr 3 21:29:35 PDT 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-04/2006-04-03-21-29-35-370079000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2006-04/2006-04-03-21-29-35-370079000-PDT.html[nogin] Added a proper implementation of the forwardT tactic that only brings in_Tue Apr 4 01:16:34 PDT 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-04/2006-04-04-01-16-34-276195000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2006-04/2006-04-04-01-16-34-276195000-PDT.html[xiny] Updated the proof with Aleksey_s improved forwardT implementation._Tue Apr 4 14:34:54 PDT 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-04/2006-04-04-14-34-54-164038000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2006-04/2006-04-04-14-34-54-164038000-PDT.html[jyh] Some progress on sequent normalization._Tue Apr 4 20:29:17 PDT 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-04/2006-04-04-20-29-17-116200000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2006-04/2006-04-04-20-29-17-116200000-PDT.html[xiny] Mostly proved subtyping is reflexive _Reflect_pmn_core_logic_test.intro_rule_test_ref__ there are only a few well_formedness subgoals left unproven__Tue Apr 4 23:39:45 PDT 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-04/2006-04-04-23-39-45-079808000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2006-04/2006-04-04-23-39-45-079808000-PDT.html[yegor] Display forms added, I also use reduce_resource as unfold_resource. It is ok for S4LP since it does not have a notion of computation._Wed Apr 5 08:12:39 PDT 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-04/2006-04-05-08-12-39-648240000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2006-04/2006-04-05-08-12-39-648240000-PDT.html[nogin] More progress on elimination tactics. They are now mostly complete, except for_Wed Apr 5 14:18:04 PDT 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-04/2006-04-05-14-18-04-780747000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2006-04/2006-04-05-14-18-04-780747000-PDT.html[nogin] Minor optimization._Wed Apr 5 18:07:33 PDT 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-04/2006-04-05-18-07-33-693204000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2006-04/2006-04-05-18-07-33-693204000-PDT.html[xiny] Changed the forward rule for sequent_bterm. It is now more general._Wed Apr 5 18:08:14 PDT 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-04/2006-04-05-18-08-14-186915000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2006-04/2006-04-05-18-08-14-186915000-PDT.html[xiny] Added sequent_bterm_depth back to the reduce resource._Wed Apr 5 20:53:51 PDT 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-04/2006-04-05-20-53-51-479905000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2006-04/2006-04-05-20-53-51-479905000-PDT.html[xiny] _bind_in_bind_ge_ shouldn_t be in the intro resource_ if the term has the form bind_n_ y. bind_n2_ z. e[y_ z]__, then _n can be smaller than _m._Wed Apr 5 23:18:38 PDT 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-04/2006-04-05-23-18-38-499842000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2006-04/2006-04-05-23-18-38-499842000-PDT.html[xiny] Added support for _vsequent_..._ in SequentRelax__ updated the proof in Reflect_pmn_core_logic_test._Wed Apr 5 23:58:13 PDT 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-04/2006-04-05-23-58-13-886288000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2006-04/2006-04-05-23-58-13-886288000-PDT.html[xiny] Recommit this file._Thu Apr 6 12:24:06 PDT 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-04/2006-04-06-12-24-06-449662000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2006-04/2006-04-06-12-24-06-449662000-PDT.html[xiny] Updated the proof for _Pmn_core_terms_test.tyExp_left__Thu Apr 6 13:55:52 PDT 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-04/2006-04-06-13-55-52-776684000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2006-04/2006-04-06-13-55-52-776684000-PDT.html[nogin] When we have a hyp of the form t_number[n] in _int_nat_, dT should try_Thu Apr 6 14:13:36 PDT 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-04/2006-04-06-14-13-36-131183000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2006-04/2006-04-06-14-13-36-131183000-PDT.html[xiny] This one should work. I re_did all the proof and regenerated the file._Thu Apr 6 15:51:25 PDT 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-04/2006-04-06-15-51-25-702393000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2006-04/2006-04-06-15-51-25-702393000-PDT.html[xiny] Use forwardChainT to make the proofs much easier._Fri Apr 7 00:12:17 PDT 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-04/2006-04-07-00-12-17-036817000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2006-04/2006-04-07-00-12-17-036817000-PDT.html[nogin] Prohibit JProver in the automatic reflection proofs _we do not need it and it_Fri Apr 7 16:30:19 PDT 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-04/2006-04-07-16-30-19-779407000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2006-04/2006-04-07-16-30-19-779407000-PDT.html[nogin] Require OMake 0.9.6.9_Mon Apr 10 19:52:54 PDT 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-04/2006-04-10-19-52-54-036170000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2006-04/2006-04-10-19-52-54-036170000-PDT.html[jyh] Updated the magic number to match changes in libmojave._Mon Apr 17 10:09:12 PDT 2006
http://svn.metaprl.org/commitlogs/metaprl/2006-04/2006-04-17-10-09-12-861068000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2006-04/2006-04-17-10-09-12-861068000-PDT.html