]> matita.cs.unibo.it Git - helm.git/log
helm.git
7 years agoupdated colors for summary tables in the web site
Ferruccio Guidi [Thu, 26 Oct 2017 20:38:49 +0000 (20:38 +0000)]
updated colors for summary tables in the web site

7 years ago- cpxs completed
Ferruccio Guidi [Thu, 26 Oct 2017 18:21:59 +0000 (18:21 +0000)]
- cpxs completed
- changed colors in sunnary tables for web site

7 years agoupdate in basic_2
Ferruccio Guidi [Wed, 25 Oct 2017 19:44:59 +0000 (19:44 +0000)]
update in basic_2

7 years ago- exclusion binder in local environments
Ferruccio Guidi [Wed, 25 Oct 2017 19:44:02 +0000 (19:44 +0000)]
- exclusion binder in local environments
  portions updated of: cpxs, lfpxs

7 years agoupdate in basic_2 and apps_2
Ferruccio Guidi [Wed, 25 Oct 2017 14:56:38 +0000 (14:56 +0000)]
update in basic_2 and apps_2

7 years ago- exclusion binder in local environments
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

7 years agoupdate in basic_2
Ferruccio Guidi [Wed, 25 Oct 2017 13:23:57 +0000 (13:23 +0000)]
update in basic_2

7 years ago- exclusion binder in local environments
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

7 years ago- update in basic_2
Ferruccio Guidi [Mon, 23 Oct 2017 17:20:25 +0000 (17:20 +0000)]
- update in basic_2
- "versions" table fixed in the web site

7 years agoone file missing in previous commit :(
Ferruccio Guidi [Mon, 23 Oct 2017 17:16:58 +0000 (17:16 +0000)]
one file missing in previous commit :(

7 years ago- exclusion binder in local environments:
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

7 years ago- one conjecture closed on lsubf
Ferruccio Guidi [Sat, 21 Oct 2017 18:25:40 +0000 (18:25 +0000)]
- one conjecture closed on lsubf
- some renaming in rtmap_sor

7 years agoupdate in basic_2
Ferruccio Guidi [Tue, 17 Oct 2017 18:35:17 +0000 (18:35 +0000)]
update in basic_2

7 years ago- exclusion binder in local environments
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

7 years agopost milestone in basic_2
Ferruccio Guidi [Tue, 17 Oct 2017 15:27:32 +0000 (15:27 +0000)]
post milestone in basic_2

7 years ago- exclusion binder in local environments
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)

7 years ago- milestone in basic_2
Ferruccio Guidi [Mon, 16 Oct 2017 21:38:21 +0000 (21:38 +0000)]
- milestone in basic_2
- update in ground_2

7 years ago- exclusion binder added in local environments
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

7 years agoupdate in basic_2
Ferruccio Guidi [Tue, 10 Oct 2017 20:45:38 +0000 (20:45 +0000)]
update in basic_2

7 years agoupdate in basic_2 due to previous update in grond_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

7 years ago- web site update
Ferruccio Guidi [Tue, 10 Oct 2017 17:16:31 +0000 (17:16 +0000)]
- web site update
- update in ground_2

7 years ago- more results on relocation
Ferruccio Guidi [Tue, 10 Oct 2017 17:05:35 +0000 (17:05 +0000)]
- more results on relocation
- refactoring

7 years agonotation bug due to previous refactoring
Ferruccio Guidi [Sun, 10 Sep 2017 15:07:18 +0000 (15:07 +0000)]
notation bug due to previous refactoring

7 years agoxoa notation refactoring and minor additions
Ferruccio Guidi [Sun, 10 Sep 2017 14:23:34 +0000 (14:23 +0000)]
xoa notation refactoring and minor additions

7 years agoone file was missing :(
Ferruccio Guidi [Fri, 2 Jun 2017 20:18:37 +0000 (20:18 +0000)]
one file was missing :(

7 years agomore results on binders ...
Ferruccio Guidi [Fri, 2 Jun 2017 19:35:13 +0000 (19:35 +0000)]
more results on binders ...

7 years agoextension of a relation to binders
Ferruccio Guidi [Thu, 25 May 2017 10:30:15 +0000 (10:30 +0000)]
extension of a relation to binders

7 years agocomponent utf8_macros fully renamed
Ferruccio Guidi [Wed, 17 May 2017 13:45:29 +0000 (13:45 +0000)]
component utf8_macros fully renamed

7 years agocomponent syntax_extensions was not declared
Ferruccio Guidi [Wed, 17 May 2017 13:23:46 +0000 (13:23 +0000)]
component syntax_extensions was not declared

7 years agomore notation for s-steps
Ferruccio Guidi [Wed, 3 May 2017 10:12:43 +0000 (10:12 +0000)]
more notation for s-steps

7 years agonotation for clear
Ferruccio Guidi [Wed, 3 May 2017 10:03:36 +0000 (10:03 +0000)]
notation for clear

7 years agonotational change for lexs
Ferruccio Guidi [Wed, 3 May 2017 09:56:08 +0000 (09:56 +0000)]
notational change for lexs

7 years agoone file was missing :(
Ferruccio Guidi [Fri, 28 Apr 2017 14:35:53 +0000 (14:35 +0000)]
one file was missing :(

7 years ago- more background for the exclusion binder
Ferruccio Guidi [Fri, 28 Apr 2017 14:33:54 +0000 (14:33 +0000)]
- more background for the exclusion binder
- some corrections

7 years agorefactoring completed
Ferruccio Guidi [Fri, 28 Apr 2017 10:52:19 +0000 (10:52 +0000)]
refactoring completed

7 years agorefactoring ...
Ferruccio Guidi [Thu, 27 Apr 2017 18:20:12 +0000 (18:20 +0000)]
refactoring ...

7 years agosome improvements before setting up the exclusion binder
Ferruccio Guidi [Mon, 24 Apr 2017 15:07:30 +0000 (15:07 +0000)]
some improvements before setting up the exclusion binder

7 years ago- notation for the exclusion binder in local envirinments
Ferruccio Guidi [Thu, 20 Apr 2017 15:19:53 +0000 (15:19 +0000)]
- notation for the exclusion binder in local envirinments
- advances on lfsx

7 years ago- advances on lfpxs ...
Ferruccio Guidi [Mon, 17 Apr 2017 19:40:28 +0000 (19:40 +0000)]
- advances on lfpxs ...
- some instances of Conf3 discovered
- some refactoring

7 years agomilestone in basic_2
Ferruccio Guidi [Sun, 16 Apr 2017 13:43:19 +0000 (13:43 +0000)]
milestone in basic_2

7 years ago- strong normalization for rt-comutation
Ferruccio Guidi [Sun, 16 Apr 2017 13:42:16 +0000 (13:42 +0000)]
- strong normalization for rt-comutation
- advances on lfpxs ...

7 years agolfsx_lfpxs completed!
Ferruccio Guidi [Sat, 15 Apr 2017 17:49:29 +0000 (17:49 +0000)]
lfsx_lfpxs completed!

7 years ago- lfpxs based on tc_lfxs
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

7 years agoadvances on lfsx ...
Ferruccio Guidi [Thu, 6 Apr 2017 10:51:28 +0000 (10:51 +0000)]
advances on lfsx ...

7 years agoupdate in basic_2 ...
Ferruccio Guidi [Wed, 5 Apr 2017 16:05:49 +0000 (16:05 +0000)]
update in basic_2 ...

7 years ago- first prroperties on lfsx proved
Ferruccio Guidi [Wed, 5 Apr 2017 16:02:22 +0000 (16:02 +0000)]
- first prroperties on lfsx proved
- component "conversion" completed
- some typos fixed

7 years agoadvances non lfsx ...
Ferruccio Guidi [Tue, 4 Apr 2017 17:14:20 +0000 (17:14 +0000)]
advances non lfsx ...

7 years ago- lfsx started ...
Ferruccio Guidi [Mon, 3 Apr 2017 21:31:19 +0000 (21:31 +0000)]
- lfsx started ...
- advances to complete csx_aaa

7 years agoupdate in basic_2
Ferruccio Guidi [Sat, 1 Apr 2017 14:51:15 +0000 (14:51 +0000)]
update in basic_2

7 years ago- strongly normalizing terms form a candidate of reducibility
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

7 years agowe always update OCAMLPATH rather than leaving it unchanged if defined
Ferruccio Guidi [Fri, 31 Mar 2017 12:34:49 +0000 (12:34 +0000)]
we always update OCAMLPATH rather than leaving it unchanged if defined

7 years agoremoved unused timeout flag
Ferruccio Guidi [Fri, 31 Mar 2017 12:11:23 +0000 (12:11 +0000)]
removed unused timeout flag

7 years agoremoving extra spaces
Ferruccio Guidi [Fri, 31 Mar 2017 11:57:31 +0000 (11:57 +0000)]
removing extra spaces

7 years ago- csx_cnx_vector.ma completed
Ferruccio Guidi [Thu, 30 Mar 2017 11:30:39 +0000 (11:30 +0000)]
- csx_cnx_vector.ma completed
- refactoring

7 years agocsx_lfpx.ma completed!
Ferruccio Guidi [Wed, 29 Mar 2017 16:00:24 +0000 (16:00 +0000)]
csx_lfpx.ma completed!

7 years ago- advances towards strong normalization
Ferruccio Guidi [Wed, 29 Mar 2017 10:24:25 +0000 (10:24 +0000)]
- advances towards strong normalization
- refactoring of properties with relocation

7 years agowe finally understood what tsts is, :)
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

7 years agoadvances on csx towards strong normalization of rt-computation ,,,
Ferruccio Guidi [Fri, 17 Mar 2017 18:54:16 +0000 (18:54 +0000)]
advances on csx towards strong normalization of rt-computation ,,,

7 years agonilestone in basic_2 !
Ferruccio Guidi [Thu, 16 Mar 2017 20:00:23 +0000 (20:00 +0000)]
nilestone in basic_2 !

7 years agocomponent rt_transition completed!
Ferruccio Guidi [Thu, 16 Mar 2017 19:59:05 +0000 (19:59 +0000)]
component rt_transition completed!

7 years agoupdate in basic_2
Ferruccio Guidi [Thu, 16 Mar 2017 16:23:05 +0000 (16:23 +0000)]
update in basic_2

7 years ago- more commutations with superclosure: fpb_lfdeq
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

7 years ago- fpbq
Ferruccio Guidi [Tue, 14 Mar 2017 19:18:09 +0000 (19:18 +0000)]
- fpbq
- advances on lfdeq towards lfdeq_lfpx_conf

7 years ago- cpxs_tsts_vector completed
Ferruccio Guidi [Tue, 14 Mar 2017 14:22:00 +0000 (14:22 +0000)]
- cpxs_tsts_vector completed
- refactoring in etc

7 years agocpx_tsts completed
Ferruccio Guidi [Mon, 13 Mar 2017 19:29:33 +0000 (19:29 +0000)]
cpx_tsts completed

7 years ago- tdeq must imply tsts
Ferruccio Guidi [Mon, 13 Mar 2017 17:04:14 +0000 (17:04 +0000)]
- tdeq must imply tsts
- notational change for tsts
- refactoring

7 years agoupdate in basic_2
Ferruccio Guidi [Sat, 11 Mar 2017 18:32:41 +0000 (18:32 +0000)]
update in basic_2

7 years agomain part of lfpxs_cpxs ...
Ferruccio Guidi [Sat, 11 Mar 2017 18:29:51 +0000 (18:29 +0000)]
main part of lfpxs_cpxs ...

7 years agoupdate in basic_2
Ferruccio Guidi [Thu, 9 Mar 2017 12:46:29 +0000 (12:46 +0000)]
update in basic_2

7 years agocpxs_drops completed
Ferruccio Guidi [Thu, 9 Mar 2017 11:54:10 +0000 (11:54 +0000)]
cpxs_drops completed

7 years agoupdate in basic_2
Ferruccio Guidi [Wed, 8 Mar 2017 21:36:52 +0000 (21:36 +0000)]
update in basic_2

7 years agocpxs_lfpx completed
Ferruccio Guidi [Wed, 8 Mar 2017 21:17:06 +0000 (21:17 +0000)]
cpxs_lfpx completed

7 years agoupdate in basic_2 and apps_2
Ferruccio Guidi [Mon, 6 Mar 2017 22:23:40 +0000 (22:23 +0000)]
update in basic_2 and apps_2

7 years ago- advances on lfxs for lfpxs
Ferruccio Guidi [Mon, 6 Mar 2017 22:20:11 +0000 (22:20 +0000)]
- advances on lfxs for lfpxs
- ex_cpr_omega (2-steps loop)

7 years agoupdate in basic_2
Ferruccio Guidi [Sun, 5 Mar 2017 17:10:08 +0000 (17:10 +0000)]
update in basic_2

7 years agoadvances on cpxs and cnx (cnxa removed) ,,,
Ferruccio Guidi [Sun, 5 Mar 2017 17:08:20 +0000 (17:08 +0000)]
advances on cpxs and cnx (cnxa removed) ,,,

7 years agoupdate in basic_2
Ferruccio Guidi [Thu, 2 Mar 2017 16:02:14 +0000 (16:02 +0000)]
update in basic_2

7 years ago- advances on csx
Ferruccio Guidi [Thu, 2 Mar 2017 16:00:48 +0000 (16:00 +0000)]
- advances on csx
- corrections in the web page

7 years ago- initial support for sigma-types
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

7 years agocsx on the way ...
Ferruccio Guidi [Mon, 20 Feb 2017 21:16:13 +0000 (21:16 +0000)]
csx on the way ...

7 years agoupdate in basic_2
Ferruccio Guidi [Sun, 19 Feb 2017 18:57:39 +0000 (18:57 +0000)]
update in basic_2

7 years ago- advances on cnx
Ferruccio Guidi [Sun, 19 Feb 2017 18:56:35 +0000 (18:56 +0000)]
- advances on cnx
- generic reducibility moved to the "static" component

7 years ago- one annotation added
Ferruccio Guidi [Sun, 19 Feb 2017 15:55:59 +0000 (15:55 +0000)]
- one annotation added
- web page updated

7 years agomilestone in basic_2
Ferruccio Guidi [Sun, 19 Feb 2017 15:53:33 +0000 (15:53 +0000)]
milestone in basic_2

7 years agosupport for generic reducibility ...
Ferruccio Guidi [Sun, 19 Feb 2017 15:32:41 +0000 (15:32 +0000)]
support for generic reducibility ...

7 years agoupdate in basic_2
Ferruccio Guidi [Sun, 19 Feb 2017 15:26:15 +0000 (15:26 +0000)]
update in basic_2

7 years agoupdate in basic_2 ...
Ferruccio Guidi [Thu, 16 Feb 2017 11:24:32 +0000 (11:24 +0000)]
update in basic_2 ...

7 years ago- cprs and cnx on the way
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

7 years agoupdate in basic_2 ...
Ferruccio Guidi [Wed, 1 Feb 2017 19:55:11 +0000 (19:55 +0000)]
update in basic_2 ...

7 years ago- advances in rt_transition
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

7 years ago- comparative table of the core objects started ...
Ferruccio Guidi [Mon, 30 Jan 2017 18:25:25 +0000 (18:25 +0000)]
- comparative table of the core objects started ...
- some bugs fixed

7 years agoupdate in basic_2 ...
Ferruccio Guidi [Thu, 26 Jan 2017 21:16:37 +0000 (21:16 +0000)]
update in basic_2 ...

7 years ago- some commutations between the rt-steps and the s-steps proved
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

7 years agoupdate in basic_2
Ferruccio Guidi [Tue, 24 Jan 2017 17:22:44 +0000 (17:22 +0000)]
update in basic_2

7 years ago- updated equivalence on referred entries: it nust be degree-based
Ferruccio Guidi [Tue, 24 Jan 2017 17:21:08 +0000 (17:21 +0000)]
- updated equivalence on referred entries: it nust be degree-based
- refactoring

7 years ago- degree-based equivalene for terms
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

7 years agoupdate in basic_2 ...
Ferruccio Guidi [Sun, 22 Jan 2017 19:48:37 +0000 (19:48 +0000)]
update in basic_2 ...

7 years agoupdate in basic_2 and ground_2 ...
Ferruccio Guidi [Sat, 21 Jan 2017 14:36:03 +0000 (14:36 +0000)]
update in basic_2 and ground_2 ...

7 years ago- improved fqu allows to prove fqu_cpx_trans and its derivatives
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

7 years agoupdate in basic_2 ...
Ferruccio Guidi [Thu, 19 Jan 2017 18:23:04 +0000 (18:23 +0000)]
update in basic_2 ...