more notation for s-steps

notation for clear

notational change for lexs

one file was missing :(

- more background for the exclusion binder
- some corrections

refactoring completed

refactoring ...

some improvements before setting up the exclusion binder

- notation for the exclusion binder in local envirinments
- advances on lfsx

- advances on lfpxs ...
- some instances of Conf3 discovered
- some refactoring

milestone in basic_2

- strong normalization for rt-comutation
- advances on lfpxs ...

lfsx_lfpxs completed!

- lfpxs based on tc_lfxs
- documentation improved with the attribute "uses"
- cpre and cpxe parked for now

advances on lfsx ...

update in basic_2 ...

- first prroperties on lfsx proved
- component "conversion" completed
- some typos fixed

advances non lfsx ...

- lfsx started ...
- advances to complete csx_aaa

update in basic_2

- 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

we always update OCAMLPATH rather than leaving it unchanged if defined

removed unused timeout flag

removing extra spaces

- csx_cnx_vector.ma completed
- refactoring

csx_lfpx.ma completed!

- advances towards strong normalization
- refactoring of properties with relocation

we finally understood what tsts is, :)
so we renamed it as theq

advances on csx towards strong normalization of rt-computation ,,,

nilestone in basic_2 !

component rt_transition completed!

update in basic_2

- more commutations with superclosure: fpb_lfdeq
- lfpx_lfdeq_conf, whose proof is much simplified w.r.t. basic_2A1

- fpbq
- advances on lfdeq towards lfdeq_lfpx_conf

- cpxs_tsts_vector completed
- refactoring in etc

cpx_tsts completed

- tdeq must imply tsts
- notational change for tsts
- refactoring

update in basic_2

main part of lfpxs_cpxs ...

update in basic_2

cpxs_drops completed

update in basic_2

cpxs_lfpx completed

update in basic_2 and apps_2

- advances on lfxs for lfpxs
- ex_cpr_omega (2-steps loop)

update in basic_2

advances on cpxs and cnx (cnxa removed) ,,,

update in basic_2

- advances on csx
- corrections in the web page

- initial support for sigma-types
- matex.sty: some style improvements
- test.tex: red boxes arround hyperlinks removed

csx on the way ...

update in basic_2

- advances on cnx
- generic reducibility moved to the "static" component

- one annotation added
- web page updated

milestone in basic_2

support for generic reducibility ...

update in basic_2

update in basic_2 ...

- cprs and cnx on the way
- breaks repositioning in notation
- corrections in NF and SN
- refactoring

update in basic_2 ...

- advances in rt_transition
- bugs fixed and refactoring of some parked files

- comparative table of the core objects started ...
- some bugs fixed

update in basic_2 ...

- some commutations between the rt-steps and the s-steps proved
- some bugs fixed

update in basic_2

- updated equivalence on referred entries: it nust be degree-based
- refactoring

- degree-based equivalene for terms
- improved matitadep allows to find more top files in the reference graph
- refactoring and bug fix

update in basic_2 ...

update in basic_2 and ground_2 ...

- improved fqu allows to prove fqu_cpx_trans and its derivatives
- parked frees_fqus_drops that does not hold anymore

update in basic_2 ...

- preservation of arity assignment
- hls orders files by extension and then by name

update in basic_2 ...

- improved lfpr_lfpr
- improved make stats (it was still invoking mac)
- hls.ml to list .ma files highligting the ones updated to basic_2A2

milestone in basic_2!

lfpx_frees and confluence of lfpr!

previous lemma proved ...

improved lsubf allowes to prove lsubf_frees_trans.

update in ground_2 and basic_2 ...

advances towards confluence of reduction in local environments ...

lexer updated with the new reference syntax +
linearized references updated in scripts

a linearized reference was still present ...

1) hard coded linearized references removed

2) new concrete syntax for linearized references
   more compliant with URI generic syntax and ELPI

   '#' not allowed in path and name

   Decl                   cic:/path/name#dec
   Def                    cic:/path/name#def:i
   Fix of int * int       cic:/path/name#fix:i:j:h
   CoFix of int           cic:/path/name#cfx:i
   Ind of int             cic:/path/name#ind:b:i:l
   Con of int * int       cic:/path/name#con:i:j:l

   run matitaclean all after this update,
   as stored aliases depend on linearized references

- basic_2 : restricted refinement for free variables (lsubf): first results
- ground_2: additions and corrections to sor

more on lfpx_frees.ma ...

- reconstruction of lfpx_frees.ma begins ...
- minor improvements

improved lexs_conf, now holds under weaker hypotheses ...

update in ground_2 and basic_2 ...

basic_2: stronger supclosure allows better inversion lemmas
ground_2: more results on sle and sor (rtmap)

some improvements towards the confluence of lfpr ...

milestone in basic_2!

one file was missing :(

diamond property of reduction!

first results on lfpr as a base for the diamond property ...

update in basic_2 ...

more results on cpm ...

one more paper citing \lambda\delta

update in ground_2 and basic_2

bug fix in the context reduction rule for cast (cpm)

we count rt parallel steps in a different way:
we use the maximum, that is idempotent, rather than the sum