]>
matita.cs.unibo.it Git - helm.git/log
Ferruccio Guidi [Thu, 26 Oct 2017 20:38:49 +0000 (20:38 +0000)]
updated colors for summary tables in the web site
Ferruccio Guidi [Thu, 26 Oct 2017 18:21:59 +0000 (18:21 +0000)]
- cpxs completed
- changed colors in sunnary tables for web site
Ferruccio Guidi [Wed, 25 Oct 2017 19:44:59 +0000 (19:44 +0000)]
update in basic_2
Ferruccio Guidi [Wed, 25 Oct 2017 19:44:02 +0000 (19:44 +0000)]
- exclusion binder in local environments
portions updated of: cpxs, lfpxs
Ferruccio Guidi [Wed, 25 Oct 2017 14:56:38 +0000 (14:56 +0000)]
update in basic_2 and apps_2
Ferruccio Guidi [Wed, 25 Oct 2017 14:55:12 +0000 (14:55 +0000)]
- exclusion binder in local environments
component "rt_transition" completed by updating: fpb, fpbq
- one example file now works
Ferruccio Guidi [Wed, 25 Oct 2017 13:23:57 +0000 (13:23 +0000)]
update in basic_2
Ferruccio Guidi [Wed, 25 Oct 2017 13:22:29 +0000 (13:22 +0000)]
- exclusion binder in local environments
updated: cpm, cpr, lfpr, cpc
- some refactoeing and minor corrections
Ferruccio Guidi [Mon, 23 Oct 2017 17:20:25 +0000 (17:20 +0000)]
- update in basic_2
- "versions" table fixed in the web site
Ferruccio Guidi [Mon, 23 Oct 2017 17:16:58 +0000 (17:16 +0000)]
one file missing in previous commit :(
Ferruccio Guidi [Mon, 23 Oct 2017 17:15:29 +0000 (17:15 +0000)]
- exclusion binder in local environments:
cpg, cpx, lfpx updated
- notation for lazyeq: fixes and additions
Ferruccio Guidi [Sat, 21 Oct 2017 18:25:40 +0000 (18:25 +0000)]
- one conjecture closed on lsubf
- some renaming in rtmap_sor
Ferruccio Guidi [Tue, 17 Oct 2017 18:35:17 +0000 (18:35 +0000)]
update in basic_2
Ferruccio Guidi [Tue, 17 Oct 2017 18:31:39 +0000 (18:31 +0000)]
- exclusion binder in local environments
updating of component rt_transition started
cpg completed
Ferruccio Guidi [Tue, 17 Oct 2017 15:27:32 +0000 (15:27 +0000)]
post milestone in basic_2
Ferruccio Guidi [Tue, 17 Oct 2017 15:24:43 +0000 (15:24 +0000)]
- exclusion binder in local environments
component i_static updated
(this is part of last milestone)
Ferruccio Guidi [Mon, 16 Oct 2017 21:38:21 +0000 (21:38 +0000)]
- milestone in basic_2
- update in ground_2
Ferruccio Guidi [Mon, 16 Oct 2017 21:34:59 +0000 (21:34 +0000)]
- exclusion binder added in local environments
working components: syntax, relocation, s_transition, s_computation, static
- improved lsubf of which we hope to prove transitivity
- improvements in rtmap
Ferruccio Guidi [Tue, 10 Oct 2017 20:45:38 +0000 (20:45 +0000)]
update in basic_2
Ferruccio Guidi [Tue, 10 Oct 2017 20:43:56 +0000 (20:43 +0000)]
update in basic_2 due to previous update in grond_2
Ferruccio Guidi [Tue, 10 Oct 2017 17:16:31 +0000 (17:16 +0000)]
- web site update
- update in ground_2
Ferruccio Guidi [Tue, 10 Oct 2017 17:05:35 +0000 (17:05 +0000)]
- more results on relocation
- refactoring
Ferruccio Guidi [Sun, 10 Sep 2017 15:07:18 +0000 (15:07 +0000)]
notation bug due to previous refactoring
Ferruccio Guidi [Sun, 10 Sep 2017 14:23:34 +0000 (14:23 +0000)]
xoa notation refactoring and minor additions
Ferruccio Guidi [Fri, 2 Jun 2017 20:18:37 +0000 (20:18 +0000)]
one file was missing :(
Ferruccio Guidi [Fri, 2 Jun 2017 19:35:13 +0000 (19:35 +0000)]
more results on binders ...
Ferruccio Guidi [Thu, 25 May 2017 10:30:15 +0000 (10:30 +0000)]
extension of a relation to binders
Ferruccio Guidi [Wed, 17 May 2017 13:45:29 +0000 (13:45 +0000)]
component utf8_macros fully renamed
Ferruccio Guidi [Wed, 17 May 2017 13:23:46 +0000 (13:23 +0000)]
component syntax_extensions was not declared
Ferruccio Guidi [Wed, 3 May 2017 10:12:43 +0000 (10:12 +0000)]
more notation for s-steps
Ferruccio Guidi [Wed, 3 May 2017 10:03:36 +0000 (10:03 +0000)]
notation for clear
Ferruccio Guidi [Wed, 3 May 2017 09:56:08 +0000 (09:56 +0000)]
notational change for lexs
Ferruccio Guidi [Fri, 28 Apr 2017 14:35:53 +0000 (14:35 +0000)]
one file was missing :(
Ferruccio Guidi [Fri, 28 Apr 2017 14:33:54 +0000 (14:33 +0000)]
- more background for the exclusion binder
- some corrections
Ferruccio Guidi [Fri, 28 Apr 2017 10:52:19 +0000 (10:52 +0000)]
refactoring completed
Ferruccio Guidi [Thu, 27 Apr 2017 18:20:12 +0000 (18:20 +0000)]
refactoring ...
Ferruccio Guidi [Mon, 24 Apr 2017 15:07:30 +0000 (15:07 +0000)]
some improvements before setting up the exclusion binder
Ferruccio Guidi [Thu, 20 Apr 2017 15:19:53 +0000 (15:19 +0000)]
- notation for the exclusion binder in local envirinments
- advances on lfsx
Ferruccio Guidi [Mon, 17 Apr 2017 19:40:28 +0000 (19:40 +0000)]
- advances on lfpxs ...
- some instances of Conf3 discovered
- some refactoring
Ferruccio Guidi [Sun, 16 Apr 2017 13:43:19 +0000 (13:43 +0000)]
milestone in basic_2
Ferruccio Guidi [Sun, 16 Apr 2017 13:42:16 +0000 (13:42 +0000)]
- strong normalization for rt-comutation
- advances on lfpxs ...
Ferruccio Guidi [Sat, 15 Apr 2017 17:49:29 +0000 (17:49 +0000)]
lfsx_lfpxs completed!
Ferruccio Guidi [Fri, 14 Apr 2017 17:01:44 +0000 (17:01 +0000)]
- lfpxs based on tc_lfxs
- documentation improved with the attribute "uses"
- cpre and cpxe parked for now
Ferruccio Guidi [Thu, 6 Apr 2017 10:51:28 +0000 (10:51 +0000)]
advances on lfsx ...
Ferruccio Guidi [Wed, 5 Apr 2017 16:05:49 +0000 (16:05 +0000)]
update in basic_2 ...
Ferruccio Guidi [Wed, 5 Apr 2017 16:02:22 +0000 (16:02 +0000)]
- first prroperties on lfsx proved
- component "conversion" completed
- some typos fixed
Ferruccio Guidi [Tue, 4 Apr 2017 17:14:20 +0000 (17:14 +0000)]
advances non lfsx ...
Ferruccio Guidi [Mon, 3 Apr 2017 21:31:19 +0000 (21:31 +0000)]
- lfsx started ...
- advances to complete csx_aaa
Ferruccio Guidi [Sat, 1 Apr 2017 14:51:15 +0000 (14:51 +0000)]
update in basic_2
Ferruccio Guidi [Sat, 1 Apr 2017 13:03:45 +0000 (13:03 +0000)]
- strongly normalizing terms form a candidate of reducibility
- one application of auto is unnecessarily slow,
a longly awaited improvement of auto is needed to solve the issue
Ferruccio Guidi [Fri, 31 Mar 2017 12:34:49 +0000 (12:34 +0000)]
we always update OCAMLPATH rather than leaving it unchanged if defined
Ferruccio Guidi [Fri, 31 Mar 2017 12:11:23 +0000 (12:11 +0000)]
removed unused timeout flag
Ferruccio Guidi [Fri, 31 Mar 2017 11:57:31 +0000 (11:57 +0000)]
removing extra spaces
Ferruccio Guidi [Thu, 30 Mar 2017 11:30:39 +0000 (11:30 +0000)]
- csx_cnx_vector.ma completed
- refactoring
Ferruccio Guidi [Wed, 29 Mar 2017 16:00:24 +0000 (16:00 +0000)]
csx_lfpx.ma completed!
Ferruccio Guidi [Wed, 29 Mar 2017 10:24:25 +0000 (10:24 +0000)]
- advances towards strong normalization
- refactoring of properties with relocation
Ferruccio Guidi [Tue, 21 Mar 2017 15:17:27 +0000 (15:17 +0000)]
we finally understood what tsts is, :)
so we renamed it as theq
Ferruccio Guidi [Fri, 17 Mar 2017 18:54:16 +0000 (18:54 +0000)]
advances on csx towards strong normalization of rt-computation ,,,
Ferruccio Guidi [Thu, 16 Mar 2017 20:00:23 +0000 (20:00 +0000)]
nilestone in basic_2 !
Ferruccio Guidi [Thu, 16 Mar 2017 19:59:05 +0000 (19:59 +0000)]
component rt_transition completed!
Ferruccio Guidi [Thu, 16 Mar 2017 16:23:05 +0000 (16:23 +0000)]
update in basic_2
Ferruccio Guidi [Thu, 16 Mar 2017 16:19:05 +0000 (16:19 +0000)]
- more commutations with superclosure: fpb_lfdeq
- lfpx_lfdeq_conf, whose proof is much simplified w.r.t. basic_2A1
Ferruccio Guidi [Tue, 14 Mar 2017 19:18:09 +0000 (19:18 +0000)]
- fpbq
- advances on lfdeq towards lfdeq_lfpx_conf
Ferruccio Guidi [Tue, 14 Mar 2017 14:22:00 +0000 (14:22 +0000)]
- cpxs_tsts_vector completed
- refactoring in etc
Ferruccio Guidi [Mon, 13 Mar 2017 19:29:33 +0000 (19:29 +0000)]
cpx_tsts completed
Ferruccio Guidi [Mon, 13 Mar 2017 17:04:14 +0000 (17:04 +0000)]
- tdeq must imply tsts
- notational change for tsts
- refactoring
Ferruccio Guidi [Sat, 11 Mar 2017 18:32:41 +0000 (18:32 +0000)]
update in basic_2
Ferruccio Guidi [Sat, 11 Mar 2017 18:29:51 +0000 (18:29 +0000)]
main part of lfpxs_cpxs ...
Ferruccio Guidi [Thu, 9 Mar 2017 12:46:29 +0000 (12:46 +0000)]
update in basic_2
Ferruccio Guidi [Thu, 9 Mar 2017 11:54:10 +0000 (11:54 +0000)]
cpxs_drops completed
Ferruccio Guidi [Wed, 8 Mar 2017 21:36:52 +0000 (21:36 +0000)]
update in basic_2
Ferruccio Guidi [Wed, 8 Mar 2017 21:17:06 +0000 (21:17 +0000)]
cpxs_lfpx completed
Ferruccio Guidi [Mon, 6 Mar 2017 22:23:40 +0000 (22:23 +0000)]
update in basic_2 and apps_2
Ferruccio Guidi [Mon, 6 Mar 2017 22:20:11 +0000 (22:20 +0000)]
- advances on lfxs for lfpxs
- ex_cpr_omega (2-steps loop)
Ferruccio Guidi [Sun, 5 Mar 2017 17:10:08 +0000 (17:10 +0000)]
update in basic_2
Ferruccio Guidi [Sun, 5 Mar 2017 17:08:20 +0000 (17:08 +0000)]
advances on cpxs and cnx (cnxa removed) ,,,
Ferruccio Guidi [Thu, 2 Mar 2017 16:02:14 +0000 (16:02 +0000)]
update in basic_2
Ferruccio Guidi [Thu, 2 Mar 2017 16:00:48 +0000 (16:00 +0000)]
- advances on csx
- corrections in the web page
Ferruccio Guidi [Mon, 27 Feb 2017 16:35:21 +0000 (16:35 +0000)]
- initial support for sigma-types
- matex.sty: some style improvements
- test.tex: red boxes arround hyperlinks removed
Ferruccio Guidi [Mon, 20 Feb 2017 21:16:13 +0000 (21:16 +0000)]
csx on the way ...
Ferruccio Guidi [Sun, 19 Feb 2017 18:57:39 +0000 (18:57 +0000)]
update in basic_2
Ferruccio Guidi [Sun, 19 Feb 2017 18:56:35 +0000 (18:56 +0000)]
- advances on cnx
- generic reducibility moved to the "static" component
Ferruccio Guidi [Sun, 19 Feb 2017 15:55:59 +0000 (15:55 +0000)]
- one annotation added
- web page updated
Ferruccio Guidi [Sun, 19 Feb 2017 15:53:33 +0000 (15:53 +0000)]
milestone in basic_2
Ferruccio Guidi [Sun, 19 Feb 2017 15:32:41 +0000 (15:32 +0000)]
support for generic reducibility ...
Ferruccio Guidi [Sun, 19 Feb 2017 15:26:15 +0000 (15:26 +0000)]
update in basic_2
Ferruccio Guidi [Thu, 16 Feb 2017 11:24:32 +0000 (11:24 +0000)]
update in basic_2 ...
Ferruccio Guidi [Thu, 16 Feb 2017 11:22:04 +0000 (11:22 +0000)]
- cprs and cnx on the way
- breaks repositioning in notation
- corrections in NF and SN
- refactoring
Ferruccio Guidi [Wed, 1 Feb 2017 19:55:11 +0000 (19:55 +0000)]
update in basic_2 ...
Ferruccio Guidi [Wed, 1 Feb 2017 19:52:07 +0000 (19:52 +0000)]
- advances in rt_transition
- bugs fixed and refactoring of some parked files
Ferruccio Guidi [Mon, 30 Jan 2017 18:25:25 +0000 (18:25 +0000)]
- comparative table of the core objects started ...
- some bugs fixed
Ferruccio Guidi [Thu, 26 Jan 2017 21:16:37 +0000 (21:16 +0000)]
update in basic_2 ...
Ferruccio Guidi [Thu, 26 Jan 2017 21:13:39 +0000 (21:13 +0000)]
- some commutations between the rt-steps and the s-steps proved
- some bugs fixed
Ferruccio Guidi [Tue, 24 Jan 2017 17:22:44 +0000 (17:22 +0000)]
update in basic_2
Ferruccio Guidi [Tue, 24 Jan 2017 17:21:08 +0000 (17:21 +0000)]
- updated equivalence on referred entries: it nust be degree-based
- refactoring
Ferruccio Guidi [Sun, 22 Jan 2017 19:56:34 +0000 (19:56 +0000)]
- degree-based equivalene for terms
- improved matitadep allows to find more top files in the reference graph
- refactoring and bug fix
Ferruccio Guidi [Sun, 22 Jan 2017 19:48:37 +0000 (19:48 +0000)]
update in basic_2 ...
Ferruccio Guidi [Sat, 21 Jan 2017 14:36:03 +0000 (14:36 +0000)]
update in basic_2 and ground_2 ...
Ferruccio Guidi [Sat, 21 Jan 2017 14:34:59 +0000 (14:34 +0000)]
- improved fqu allows to prove fqu_cpx_trans and its derivatives
- parked frees_fqus_drops that does not hold anymore
Ferruccio Guidi [Thu, 19 Jan 2017 18:23:04 +0000 (18:23 +0000)]
update in basic_2 ...