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

notational update in lambdadelta completed

+ minor improvements

partial notational update in ground_2 and basic_2 ....

+ the notation for lists and streams contains a bug

update in models and ground_2

+ model declaration completed
+ compatibility with veq, first results
+ some old files moved in etc for now

initial definition of λδ model

+ intensional and extensional variant
+ denotational equivalence

this is previously uncommitted matter ported to current version of λδ

update in basic_2

+ first results on cpms
+ minor improvements

update in ground_2 and basic_2

+ old and unused definition llstar replaced with new definition ltc to appear in cpms

notational update in ground_2 and basic_2

+ one addition in predefined_virtuals
+ works citing \lambda\delta updated on web site

decentralizing core notation continues ...

+ uparrows and downarrows clash with \lambda\delta
+ improved list of failing files

update in basic_2 and ground_2

+ some notational changes
+ some renaming
+ some dependences updated

anniversary push

+ one more work citing\lambda\delta
+ more predefined virtuals

bug fixed in xoa generator

notations of existentials must differ according to arity of the involved predicates
+ porting to the updated version of xoa
+ one addition in predefined virtuals

decentralizing core notation

centralized core notation (one single file) has two disadvantages:
- when some core notation is added the whole "world" must be recompiled
- unused core notation loaded in the parser gets in the way when defining contrib-specific notation
by defining core notation on a "one notation per file" basis:
+ every contrib file can load just the needed notation
+ sharing is possible as before in that two contrib files can load the same notation file

decentralalization will occur is stages:
this is the first stage meant to solve some issues in
+ lambdadelta (! blocked by fact)
+ certifiedRev (o{} blocked by compose, comprehension, singl, subset)

milestone update in basic_2

+ big tree theorem proved!

update in basic_2

+ lemma csx_fsb proved

update in basic_2

+ last property of fpbs proved

update in basic_2

+ first results on fsb

update in basic_2

+ fpbg completed

update in basic_2

+ advances on fpbg
+ Makefile update

update in basic_2

+ fpbs completed (some lemmas parked)

update in basic_2

+ first results on fpbs
+ minor fixes

update in basic_2

+ advances on fpbq
+ minor updates

update in basic_2

+ advances on fpb completed

update in basic_2

advances on fpb to be continued ...

bugfix update in basic_2

+ bugfix in ffdeq
+ bugfix in fpbq
+ minor fixes

update in basic_2 + web page

+ csx completed
+ notational change to lreq and lfeq to reduce overloading

long awaited update in basic_2

csx_lfsx eventually proved! (major result on lfsx)

update in basic_2

+ yet anothe equivalent of lfsx to be used in lfsx_pair_lpxs

update in basic_2

+ improved version of lfxs_trans_gen, now lfxs_trans_fsle
  based on an improved version of lexs_trans_gen
+ refactoring

update in basic_2

+ new equivalent of lfsx opens the road to lfsx_pair_lpxs
+ minor corrections

update in basic_2

+ new proof of cpx_frees_conf_lexs with fsle
+ refactoring

update in ground_2 and basic_2

+ minor additions
+ refactoring

advances on cpx_lfxs_conf_fle

+ transitivities for fle
+ minor additions

lref case closed in cpx_lfxs_conf_fle

+ premise with h.o equality added to the theorem

integrating the framework with fle ...

+ new ignores

two cases of cpx_lfxs_conf_fle closed

+ advances on fle
+ one inversion lemma missing in lveq
+ one character missing in predefined virtuals

xoa updated

a dependence from matita removed
optional generation of separated objects (this should be the default)

helena: updated prolog exportation to ld3 and ALT-0/PTS

update in basic_2

yet another definition of lveq allows to prove a missing lemma in lfxs_fle

update in ground_2 and basic_2

- new version of lveq completed: allows to prove all six main properties of fle, but lfxs_fle fails :(
- voids parked for now
- more ignores for the web site