update in basuc_2

+ cpce_drops completed
+ WIP on cpce

WIP on cpce ...

backport of WIP on \lambda\delta to matita 0.99.3

auto tactic of matita 0.99.4 is broken
for now WIP on \lambda\delta continues on this branch

update in ground_2 and basic_2

+ initial support for t-transition (the core of inferred type assignment)

update in static_2

+ notation change for lifts and drops

update in basic_2

+ iterated type assignment completed
+ minor additions to the arith library

update in basic_2

+ main result on acle proved

update in static_2

+ preorder on applicability domains
+ minor bug fixes

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