slight refactoring in the proof of strong normalization

update in basic_2 ...

one more typo ...

bug fix in ththe notation for lists:
disambiguation of nil does not work very well in gcp_cr and gcp_aaa :(

...

...

added an example on lstas showing a difference with previous sta

- contrib update for version 2
- update in basic_2

New chapter on setoids.

chapter12 (coinductive) -> chapter13

milestone in basic_2 :)

commit completed! the new iterated static type assignment is up!

- the PARTIAL COMMIT continues, we issue the "reduction" component

- new stand-alone definition of lstas (sta and old lstas parked in etc)
- PARTIAL COMMIT: we issue just the components "static" and "unfold"

Notes.

A tentative chaptern on coinductive types.

Currently I hitted a major bug somewhere.

- update in basic_2
- minor update to the web site

some renaming and a minor addition

- bugfixed "aacr" allows to remove historical eta-conversions
  in the apparatus for strong normalization
- minor bugfixes in annotations
- xhtbl tables updated for the bugfixed stylesheets

- update in basic_2
- minor updates in the web site, including css bugfix

update in basic_2 ...

- some renaming and minor updates

- update in basic_2 and ground_2
- uodated web site

bugfix in source table :(

- basic_2: reaxiomatized snv with improved cpds and cpes simplifies preservation
- alpha_1: first commit
- ground_2/lib: one addition
- Makefile: improved contrib generation

new files

one property of abstract computation removed

refactoring of the butterflies :)

web site update

the generation of the web site is completed!

- update in ground_2 and basic_2
- the third page of the web site is generated

- irreflexivity of static type assignment iterated at least once
- some traces added for auto

- update in basic_2 and ground_2
- minor update of the web site

some renaming and some typos corrected ...

- xhtbl : support for named anchors (id's) and other improvements
- ld_web: additions for the "documentation" page

now the "news" page is generated

update for CamlP5

red butterfly added for version 1 :)

improved site map and version 2 page

- xhtbl: we added the real concatenation of cells (without added spaces)
- web site: we added a page for each version of \lambda\delta

named anchors replaced by ids as requested by xhtml

- xhtbl: support for relative links added
- web site: now the "forword" page is generated

minor update in basic_2

improved example: Delta must be a family of terms

- now unicode characters are counted :)
- now identifiers are counted as single characters

important update in basic_2: cpr is not antisymmetric

conjecture on antisymmetry of cpr finally closed
cpr is NOT antisymmetric: call-by-value beta-reduction takes two steps exactly

some additions and corrections ...

- we begin the new site based on ld_web
- xhtbl: xml namespaces and absolute atnl links are now supported
- lambdadelta_2 uploaded

- wrong version of drop was used in four places
- bugfixed css class in tables

update in basic_2

- ldrop is now drop as in basic_1
- notation change for tstc and leq

updated slides

pathologic @-typing removed by adding imp-introduction

misspelled filename :(

milestone reported on web site

- we upload communication #8
- update in basic_2 and ground_2

- some pending conjectures closed in basic_2 and ground_2
- bug fix in decidability of lift

milestone in basic_2 !!

milestone connit for preservation:
- for now we remove stratified equivalence for terms
  (it is much more complicated than expected)
- we park in etc a generalization of preservation

minor update in basic_2

- we introduce stratified term equivalence to remove the parameter g from cpx
- unused files removed from etc
- minor updates

update in basic_2 ...

reorganization of the "static" component:
from now on we use the non-stratified version of the static type assignment,
as in basic_1

preservation of stratified vaildity through ordinary reduction and static typing

update in basic_2 ...

advances on append allow to complete the long awaited "big tree" theorem by closing the last comjecure!

mailstone in basic_2 !! "big tree" theorem completed after 15 months

now we use the version of lazy union for local environments in which
the arguments have the same length. it should have better invariants

bug fix in lazy union for local environments

- some work on append
- some corrections and some annotations

update in basic_2 ...

source table bugfixed

- advances on free variables allow to reduce lleq_lpx_trans to llor_total :)
- lazy union of local environments need a depth argument
- Makefile bugfixed

- some refactoring and minor additions

- advances on hereditarily free variables: now "frees" is primitive
- some refactoring in etc

one file was missing :(

new definition of llor gives a long awaited lemma :),
but introduces an axiom :(

update in ground_2 and basic_2 ...

- theory of llor now includes (long awaited) non-recursive alternative definition
- poinwise extensions downgraded (current llor does not need the improved version)
- some refactoring in etc

non-recursive alternative of llpx_sn completed !

update in grond_2 and basic_2 ...

advances on cofrees allows to prove one direction of
non-recursive characterization of llpx_sn (finally!)

update in ground_2 and basic_2 ...

advances on ldrop ....

advances on cofrees

reordering abstract computation properties and saturation conditions

one file was missing ...

- advances in the theory of cofrees
- some notational changes
- some refactoring in etc

- we introduce recursive free variables of a term in a context ...
- some symbols added

update in basic_2 ...

- name changes in the rediction rules
- theory of extended substitution is active again, we hope to use it
to obtain a non-recurisive alternative definition of llpx_sn

update in basic_2 ...

- the relation for pointwise extensions now takes a binder as argument
- explicit alternative definition of lprs and lpxs removed
- changes in the notation for subclosures and refinements

anniversary milestone in basic_2 !!

3rd anniversary milestone
- recursion removed from alernative definition of lpx_sn
- some corrections and updates

- lazy extended reduction parked
- fpns finally removed
- "big tree" computation based again on "full" extended reduction
  but improved with lazy equivalence for local environments
- llor parked for now (something to fix there)

we restored the strong normalization of extended computation for local
environments with some important updates from the "lazy version"

commit completed: one file was missing :(

- some work on extensions:
  the alternative definition of lpx_sn and llpx_sn is useless since it is recursive
  llor seems to contain a bug in the referred components
- some work pointwise extended reduction:
  we restore the "full" version and use it for the normaliztion of extended reduction
  we still use "lazy" version for the "big-tree" theorem