new web site page

change log for λδ begins

update in static_2 and basic_2

+ advances on ntas for the article
+ minor corrections
+ notation update for: ac, cnv, lsubv, nta, ntas
+ bold digits in predefined virtuals

milestone in basic_2

We parametrize applicability condition with a generic subset of numbers.

update in static_2 and basic_2

+ a weaker version of tueq reintroduced
+ some renaming
+ one conjecture to prove

update in ground_2 static_2 basic_2

+ the applicability parameter is now a predicate
+ tueq removed in favor of theq
+ two conjectures to prove ...

still more additions and corrections for the article

+ one theorem was missing
+ some renaming

still more additions and corrections for the article

+ new proof of csx_rsx
+ more results on jsx
+ extra parameter removed from jsx
+ minor corrections on lsubr
+ some renaming

more additions and corrections for the article

+ fqu_clear excluded from (fqu true)
+ some renaming and changes of notation (esp. lsubsx)
+ more comments and additions to etc
+ matitadep: -b show the recursive backward dependences of a file

additions and corrections for the article on λδ-2B

+ candidates: condition S4 removed
+ arity assignment: decidability proved
+ minor additions

updating the structures for sorts

+ strict monotonicity is now an optional property
+ new optional properties: acyclicity and decidability
+ "next" now has a specific notation
+ refactored sort degree is now based on acyclicity and decidability

some restyling ...

+ fixing some notations
+ fixing some spaces

milestone in basic_2

+ Parametrized applicability condition allows λδ-2B to generalize both λδ-1A and λδ-1B.
+ ground_2: minor additions

update in basic_2

one file was missing in last commit :(

update in basic_2

+ totality for fixed cpce
+ Makefile: bug fixed

decentralizing core notation continues ...

+ apart, napart decentralized

update in basic_2

+ decidability of type inference
+ decidability of type checking

milestone in basic_2 with additions in static_2

+ validity is decidable
+ some renaming
+ batch compilation handles each specification separately
  otherwise matitac opens too many files

update in basic_2

+ decidability of cpes
+ some renaming

update in ground_2 static_2 basic_2

structures for decidability of the validity predicate

+ cpes, cnr, cpre resumed
+ minor corrections

milestone in basic_2

preservation of validity for rt-computation does not need the sort degree parameter (i.e. no induction on the degree).

update in ground_2 static_2 basic_2

+ whd normal forms for terms with arity
+ positive abbreviations are not whd normal forms
+ minor additions

first steps towards decidability of the validity predicate

+ tentative definition of cwhx

minor corrections and updates

intensional and extensional equivalence on lists coincide

the decentralization of core notation continues ...

subseteq notation decentralized

xoa utility updated

+ two missing cases implemented
+ dependences fixed in Makefile

list of failing files updated

+ one file added

web site update

one css stylesheet improved

web site update

+ one css file improved

web site update

additions in a css file

supplementary files for web site

+ css file name corrected

Merge branch 'master' of ssh://matita.cs.unibo.it:/srv/git/helm

some supplementary items for web site

one icon and on css file

presentation upload

A newborn in the λδ family: introducing λδ-2B

update in basic_2 and in web site

+ updates on cpce an related concepts
+ "versions" table updated for web site

update in bsasic_2

+ cnv_cpce_trans_lpce started

update in basic_2

+ lpce

update in basic_2, static_2, web site

+ bug fix and first results on cpce
+ crux favicon for web site is now 32x32
+ some auxiliary files for web site committed/rearranged

update in basic_2

+ more properties on types from λδ-1A including:
  type preservation by valid r-equivalence

milestone uupdate in basic_2

extended and restricted type rules justified

update in basic_2

the restricted type rules are justified

auxiliary update in basic_2

- work in progress to justify the type rules for application

update in basic_2

+ nta_drops completed

update in basic_2 and apps_2

+ more results on typing
+ first results on iterated typing
+ minor corrections

update in basic_2 and static_2

+ first results on type assignment
+ more notation for validity
+ eta-conversion defined (for use in linking the notions of validity)

milestone in basic_2, λδ-2A reconstructed

+ confluence of rt-computation (not proved in λδ-2A)
+ preservation of validity for rt-computation

update in ground_2, static_2, basic_2

+ confluence for restricted rt_transition under hyps
+ positive terms wrt the system of reference parked

update in static_2 and basic_2

+ restricted rt-computation;
  more results towards preservation

dependences for ocaml version 4.05.0

update in ground_2, static_2, basic_2

+ minor additioms

update in static_2 and basic_2

+ cnv_cpms_conf_aux proved
  for positive terms wrt the system of reference
+ unused files parked or removed

update in basic_2 and ground_2

+ more results on restricted transition
+ minor additions to the arith library

severe bug found in parallel zeta

+ final commit: component "examples" corrected
+ ex_cpr_omega improved: Ω ➡ Ω in exactly three steps (long awaited property)

severe bug found in parallel zeta

+ partial commit: component "dynamic" corrected
+ some additions towards preservation

severe bug found in parallel zeta

+ partial commit: component "rt_computation" corrected
+ minor additions

severe bug found in parallel zeta

the transition was not parallel, now it is.

+ partial commit: component "rt_transition" corrected and minor bugs ficed
+ some additions in static_2 to support the correction

commit in ground_2, static_2, basic_2, apps_2

+ first steps towards cnv_cpms_conf_aux
+ examples reconstructed
+ additions in the relocation library
+ addition in the arith library

parameter sintax added to axiom statement

the syntax is already present in the other statements

update in ground_2 and basic_2

+ cnv_cpm_conf_lpr_aux (rt-validity implies diamond property)
+ one addition in the arithmetics library

update in ground_2 and basic_2

+ modification in cnv allows to improve cnv_cpm_trans_lpr_aux
+ modification in lsubv allows to prove its transitivity
+ one lemma added to the arithmetic library

update in basic_2

+ refinement for native validity (lsubv)
  allows to prove cnv_cpm_trans_lpr_aux (rt-confluence implies validity)

update in basic_2 and ground_2

+ auxiliary lemmas for preservation begin
+ one addition in the arith library
+ some typos in names fixed

update in apps_2

+ the model is now aware of polarized abbreviation
+ the term model is on its way

update in functional

+ support for multiple filling

update in ground_2

+ basic relocation swap
+ one name fixed
+ bugs emerging in cpr fixed

updated xoa and predefined virtuals

+ xoa: existing decentralized files are not overwritten by default
+ predefined virtuals: an addition for use in λδ

update in static_2 and app_2

+ term model started
+ functional relocation reactivated
+ some renaming

update in static_2 and app_2

+ advances on the support for models
+ tentative definition of shift (incomplete because unary binders are missing in terms)
+ minor updates and corrections

syntactic components detached from basic_2 become static_2

+ web site updated accordingly

renaming in basic_2

+ a notation problem solved

renaming

+ the predicate in elimination principles in now Q uniformly

renaming in basic_2

nv is now cnv

Merge branch 'master' of ssh://matita.cs.unibo.it:/srv/git/helm

# Conflicts:
# matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl

bug fix in basic_2

+ cpcs_aaa_mono marked as lemma 1500
+ fix in basic_2 web page

bug fix in basic_2

+ cpcs_aaa_mono marked as lemma 1500
+ fix in basic_2 web page

update in basic_2

+ advances on nv ...

update in basic_2

+ component rt_equivalence completed!

milestone update in basic_2

componemt rt_computation cpmpleted!

update in basic_2

+ cprs completed

update in ground_2 and basic_2

+ advances on cpms, cprs, lprs
+ support for decentralized xoa

update in ground_2 and basic_2

+ more results on cpm, and cpms

update in basic_2

+ lprs started ...

commit completed in basic_2

+ fpbs, fpbg, fsb reconstructed

partial commit in basic_2

+ rdsx (was lsx) reconstructed: replaces lfsx

partial update update in basic_2

+ lpxs reconstructed

update in ground_2 and basic_2 (partial commit)

+ preferring lpx and lpr over lfpx and lfpr since lpx seems unavoidable
+ rt_computation will be updated by the next commit

update in basic_2

+ advances on native validity

update in ground_2 and basic_2

+ more results on cpms

update in basic_2

+ moreresults on cpms and cprs

update in basic_2

+ first file on r-equivalence
+ renaming

update in basic_2

definition of native validity

update in basic_2

+ cprs.ma completely ported

update in basic_2

+ first results on cpms and cprs

update in ground_2

set up for equality insertion lemmas

update in basic_2

+ weight of a global environment
+ renaming

update in groud_2 and models

+ denotation is preserved by r-transition
+ minor additions

update in grond_2 and models

+ denotation is preserved by lifts in extensional models

update in apps_2

+ update to web site

update in basic_2

+ list length is now in a separate file

update in ground_2 and basic_2

+ updated notation for lists
+ updated structure for global environments

update in ground_2 and models

+ bug fixed in local environment interpretation
  extensional equality of evaluations allows to prove a lemma