update in delayed_updating

+ lift: additions and refactoring
+ reduction: WIP

update in ground and delayed_updating

+ main theorem about dfr proved!
+ ground: duplicated lemma removed
+ some refactoring

update in delayed_updating

+ crux of the main proof completed
+ notation for path_reverse fixed

update in delayed_updating

+ unwind completed with an important result on lift

update in ground

+ additions to lifts

update in ground

+ new notation for application of a relocation

update in delayed_updating

+ generic unwind meeds to be  even more generic

update in delayed_updating

+ generic unwind for path
+ some old files parked

update in delayed_updating

+ main function to locate the referred binder
+ update function for unfold

update in delayed_updating

+ notation for reversed path

update in delayed_updating

+ conflicts solved

update in delayed_updating

+ closed paths
+ updated notation for height
+ some parked files added

update in delayed_updating

+ some notation updated
+ some unused files removed

update in delayed_updating

+ alternative definition of unwind based on lift

update in delayed updating

updated notation

update in delayed updating

+ new version of lift
+ corrected and updated notation

update in ground

+ some addittions and corrections

update un delayed updating

+ some parked files

WIP in delayed_updating

+ we re focusing on a special case of the main theorem

update in delayed updating

+ additions to lift

update in ground

+ some additions and corrections

update in delayed_updating

+ lift
+ two versions of unwind
+ some renaming, additions and corrections

update in delayed_updating

+ some additions and corrections

update in ground

+ some additions

partial update in delayed_updating

+ WIP

update in ground

+ minor corrections and additions

update in delayed_updating

+ important additionsand corrections

update in ground

+ some additions and corrections

update in delayed_updating

+ update count for paths
+ minor additions and corrections

update in ground

+ additions to tr_compose

update in delayed_updating

+ WIP on dfr_lift_bi
+ minor corrections

update in ground

+ main commutation of tr_compose and tr_uni

update in delayed_updating

+ relationship between grafted trees and updating clarified in the case of interest so far

update in delayed_updating

+ WIP on updating grafted trees

update in delayed-updating

+ relationship between updating an grafted terms clarified
+ progress with dfr-lift_bi

update in delayed updating

+ additions to lift
+ bugs fixed in dtr and itr

update in ground

+ additions to subsets

update in delayed_updating

+ additions to lift
+ bugs fixed in ifr

update in ground

+ additions to tr_compose

update in ground

+ additions to tr_compose

update in delayed_updating

+ bugs fixed in depth, dfr, ifr
+ WIP on dfr_lift_bi

update un delayed_updating

+ bugs fixed in dfr and ifr

update in ground

+ additions on tr_pap

update in delayed_updating

+ bugs fixed id dfr and ifr

update in ground

+ additions on tr_id

update in delayed_updating

+ mark label added
+ bugs fixed in depth and reduction
+ two notations changed

update in delayed_updating

+ a premise removed from lift_fsubst_sn
+ dfr and ifr restated to take equiprovability into account
+ notatation update for preterms

update in ground

+ advanced eliminators on lists

update in delayed_updating

+ commutation of lift and fsubst
+ preterms renamed as prototerms

update in grafite parser

+ parameter notation in record fields

update in ground

+ WIP on subsets

update in delayed_updating

+ proper condition for path
+ relation between lift and append proved

update in delayed updating

+ notation for "proper element"
+ bug fixed ub the notation of predicates

update in lib

+ notation for card decentralized

update in ground and delayed updating

+ notation at level 75 moved at level 70
+ dfr, ifr: path depth was not considered

update in delayed_updating

+ improved lift

update in delayed_updating

+ immediate reduction defined
+ some lemmas with lift simplified

update in delayed updating

+ some properties of lift

update in ground, static_2 and apps_2

+ updated notation for extensional equality

update in delayed_updating

+ updated notation for lists
+ WIP on lift

update in ground, basic_2A and apps_2

+ notation for lists: fixed and updated

update in ground

+ uniform total relocations

update in delayed updating

+ delayed focalized reduction

update in ground

+ composition for total relocation maps

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

update in ground

+ positive application for total relocation maps completed

update in delayed_updating

+ terms are defined modulo logical equivalence

update in ground

+ basic support for subsets as predicates

update in delayed updating

+ WIP on dephi
+ some renaming
+ subset notation improved

update in delayed_updating

+ wip on predicate for bdd terms
+ updated notation
+ additions to lists

update in ground

+ updated notation and terminology for lists

update in ground

+ additions and corrections on lists

update in ground

+ advances on total redlocation

contribution on delayed updating begins

we place it here for convenience

update in ground

+ total relocation begins

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

λδ web site update

+ updated bibliography

update in ground static_2 basic_2 apps_2

+ two sets of bold parentheses were used. now just one

update in ground

+ total relocation restarted

partial update in static_2

+ propagation of ground library in static_2/relocation begins
+ additions in ground

partial update in static_2

+ ground library propagated in static/syntax
+ additions in ground

partial update in static_2

+ propagating the ground library
+ one addition in ground

update in ground

+ minor bug fixed in a notation

partial commit in static_2

propagating the new ground library to static_2 begins

update in ground

+ one lemma was missing

update in ground

+ bug fixed in the notation of exp
+ minor bugs fixed

update in ground

+ some renaming

update in ground

+ new notation for head and tail

update in ground and static_2

+ notation update for tail function
+ predefined virtuals: one symbol added

update in alpha_1

+ type of terms redefined
+ Makefile added to lambdadelta/bin
+ a correction static_2/syntax/term.ma

λδ site update

+ one citation added to home page
+ one bug fixed in xhtbl.ml
+ ome comment added in gcp_cr.ma

update in ground

+ comments restyled

λδ site update

+ ground and documentation

probe

+ improved error handling

nCicLibrary

+ config flag added to emove old objects before storing new ones
  I don't even rememberwhy thisisnot done by default

update in ground

+ some renaming

cic notation parser

syntax of constructors updated to match syntax of definitions

milestone update in ground

+ generic relocation maps are now streams of booleans
+ some renaming and restyling
+ operator precedence more uniform
+ recomm updated for relocation

grafite parser updated

+ syntax for parameters added to constructors
  as it was done with definitions some time ago

propagating the arithmetics library, partial commit

+ relocation updated and ported (de Bruijn indexes now start at 1)
+ recomm updated to generate substitution files
+ results on positive integers added to arith
+ some corrections