update in delayed_updating

+ new operator on update functions

update in ground

+ some additions
+ some renaming

update in delayed_updating

+ some renaming

update in delayed_updating

+ more complex example in which discarding num labels in b solves unwind

update in delayed_updating

+ couterexample to dbfr_ibfr when inner labels in b are not bound in b

update in delayed_updating

+ excess added to closure condition for path
+ height for path restored

update in ground

+ some renaming

update in delayed_updating

+ guard condition removed from reduction

update in ground

+ minor addition to relocation

update in delayed_updating

+ bug fixed in the "crux of the proof" allows to certify more reductions
+ restricted form of closed path not used anymore

update in ground

+ head-tail decomposition of a relocation map
+ injectivity of pnpred

wip in delayed_updating

guard condition

update in delayed_updating

+ example of unprotected balanced reduction continued and simplified

update in delayed_updating

+ example of unprotected balanced reduction continued

update in delayed_updating

+ example of unprotected balanced β-reduction started
+ some corrections and additions

update in ground

+ positive integer two

update in ground

+ additions to subset extensionality

update in delayed_updating

+ core reduction parked
+ paths of one repeated label resumed

update in delayed_updating

commutations of balanced reduction completed

update in predefined_virtuals

+ two arrows added

update in delayed_updating

+ balanced reduction with main theorem proved
+ notation change for lift

update in delayed_updating and ground

+ single specification for protected and unprotected closed path
+ some parked files removed

update in delayed_updating

+ reference by depth with offset parked for now

partial update in delayed_updating

+ we add reference by depth with offset
+ component "syntax" updated
+ some improvements
+ height parked for now

update in ground and delayed_updating

+ example of unprotected balanced segment
+ balanced reduction parked for now
+ additions and renaming

update in delayd_updating

+ introduction of path_closed complete

update in ground

+ some renaming and some refactoring

update in static_2

+ notation update from ground

update in ground

+ notation update and renaming

addition to predefined virtuals

+ one character added

partial update in delayed_updating

+ syntax and substitution components updated
+ path_head parked and replaced by path_closed
+ balanced reductions introduced and main theorem proved
+ minor corrections to notation

update in delayed_updating

+ focused reduction takes just one focus
+ changed minor premise of ifr_unwind_bi
+ some renaming

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

commit in delayed_updating

+ reversing paths completed updating component "reduction"

update in ground

+ additions to nap and xap

update in delayed_updating

+ three old lemmas restored
+ some parked lemmas removed
+ minor renaming

partial commit in delayed_updating

+ reversing paths in component "unwind"

partial commit in delayed_updating

+ reversing paths in component "substitution"
+ lift reformulated in terms of simpler functions

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

partial commit in delayed_updating

+ reversing paths in component "syntax"
+ some renaming

update in ground

+ one more lemma with list_append

partial commit in delayed_updating

+ parchin reverse operator for paths

update in delayed_updating

+ bind condition simplified for ifr and dfr

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

update in delayed updating

+ two lemmas on path_head
+ invocation added to first file

update in delayed_updating

+ some additions
+ minor improvements

update in delayed_updating

+ ifr_lift proved
+ ifr corrected
+ minor corrections

update in delayed_updating

+ unwind2_path_after_lift
+ prelift
+ refactoring for lift

update in ground

+ minor corrections

update in delayed updating

+ dfr_lift_bi proved

update in delayed_updating

+ WIP on lift
+ notation changed for delayed updating (term constructor)
+ minor corrections

update in delayed_updating

+ additions for lift
+ advances in dfr_lift_bi
+ some corrections
+ some parked files removed

update in delayed_updating

+ final definition of lift
+ WIP on dfr_lift_bi
+ updates and corrections
+ old definition of lift parked

update in delayed_updating

+ bug fixed in ifr allows to prove ifr_unwind_bi

update in delayed_updating

+ lift changed to lift after unwind in ifr
+ notion of lift swapped again
+ some additions to prove a side condition of ifr_unwind_bi

update in ground

* subset overlap

update  in lib

+ notation for overlap decentralized

update in delayed_updating

+ some files parked

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