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

\lambda\delta web site update for git

helena: warning removed and modifications for λΥP exportation

update in helena

- new system of attributes for terms
- exportation to λΥP λProlog engine
- now based on ocamlbuild

jet a change in dependences

work in progress with voids and lveq (was: the most recent voids)

update in ground_2 + \lambda\delta-related ignores

matita.basedir used consistently

more files to ignore

updated depend files

beginning of minimalist foundation from a student of Milly

Horrible workaround

Compiled with recent OCaml, Matita now fails removing
a notation when it starts. The patch avoids the assert
false. I have not investigated what's going on.

.depend{.opt} files changed

Patch to make it compile with recent OCaml

added .gitignore

OCaml special files ignored

patch to make it compile with recent OCaml versions

strange bug-fix to allow compilation on recent ocaml+camlp5o

Stupid fix to avoid new camlp5 bug with int64 literals

Patch to make it work with new versions of lablgtk2

- work in progress proceeds for the new definition of voids ...
- arith.ma: some additions and reordering

an addition for \lambda\delta

work in progress on a new definition of voids ...

the previous commit was incomplete :(

work in progress with fle ...

work in progress ...

- free variables innclusion (fle) encapsulates some complexity
  in the proof of a generalization of frees_lfxs_conf
- a refactoring solves a bug in dependences

update in basic_2

- equivalence between lfpxs and lpxs + lfeq proved
- more descriptions in basic_2_src.tbl

- lpx and lpxs restored to prove equivalene between lfpxs and lpxs + lfeq
- Makefile: number of objects and intrinsic loss factor added in summary for web page
- basic_2_src.tbl: more descriptions

update in basic_2 and in the corresponding web page