progress in unistep_aux

unistep_aux

more unistep

unistep_aux

copy finished

- a few more lemmas ...
- some renaming

copy.ma

match.ma completed

match termination completed, still a small case ignored in wsem_match

wsem_match finished

advancement in match

Closed some daemons

nth_current_chars

standardization: equivalence between paths and left residuals started

match almost finished

more porting to machines that can move without writing

parmove based on end of the tape

porting to machine that can move without writing

dependences update

refactoring ...

Ported permutation.ma and fermat_little_theorem.ma

refactoring

Refactoring

Chebishev ported

lambda: some refactoring + support for subsets of subterms started
core_notation: some "term 19" added
predefined_virtuals: an addition

- probe: new application to compute some data on the proof objects of
a development, such as their net size (aka intrinsinc complexity)
- lambdadelta: Makefile now asks "probe" fore some data

update in basic_2

commit completed! some bugs fixed and some instances of auto resized

xoa: change in naming convenctions for existential quantifies
     to cope with ex2 in lib
lib: some additions
lambdadelta: partial commit in basic_2: just grammar, substitution,
unfold, static

- lambda_delta: programmed renaming to lambdadelta
- nat: general weight-based eliminator added for lambdadelta

- we introduced the pointer_step rc in the perspective of proving
results on head normal forms
- some renaming

some renaming ...

one file was missing .... :(

Many changes

mem/append lemmas

bertrand OK.

- nat.ma: cut removed from f_ind :)
- lanbda: some refactoring

reordering and corrections

bertrand!
-tThis line, and those below, will be ignored--

A    chebyshev/bertrand256.ma
A    chebyshev/bertrand.ma

we simplified our proof of standardization
by removing Kashima's "hap" computation

sqrt.ma

- star.ma: strip lemma and confluence of star
- lambda: confluence of labelled sequential reduction completed!

addenda

changes

chebyshev_teta

- lambda: some parts commented out, some refactoring
  and some notational changes
- lib: some additions from the preamble of "lambda"
- predefined_virtuals: some additions

This line, and those below, will be ignored--

D    arithmetics/big_pi.ma

splitted chebyshev in two parts

restructuring

backup copy rm

Still porting chebyshev

- we added delimiters to the URL in lambdadelta1

- bib refactoring
- date correction for lambdadelta5

lambdadelta1 is now dated with release date of \lambda\delta version 1

- pointer structure simplified
- new properties on poiner orders
- last lemma in Kashima's article proved

- lambda: - normalization theorem completed!
          - binary trees on pointer sequences set up to serve as labels for "st" computations
- lstar: right-oriened eliminator added

Porting chebyshev

Porting chebyshev

- lambda: first half of the standardization theorem is proved!

- list.ma: improved notation for constant lists (a "term 19" was missing)
- lambda: more properties on pointers, extra xoa quantifier removed,
bugfix in notations and names

- new pointes can point to any subterm
- new star_ind_l-like eliminator for lstar now in use

lstar removed from list.ma and placed in its own file

- "re": a part of reb.ma commented out since it cannot compile

- pts_dummy/pts_dummy_new: non compiling parts commented out
- tutorial: some comments added

- untranslated sections of "formal_topology" commented to make it compile
- "tutorial" now compiles

match termination

- we enabled a notation for ex2
- we improved star_ind_l that now behaves as if starl were defined
with a "left parameter" occurring on the right. this makes star_ind_l
symmetric with respect to star_ind
- we commented the non-more-compiling sections of "turing"
- some progress in "lambda"

Cleared unused variables in wsem_match (they were also sharing names with
other variables).

Bug fixed: %n was badly failing (with Failure "nth") when n was
not a valid constructor. Now fail is raised (to be captured by
try, etc.)

Fixes a bug in NCicElim.pp (term -> ast conversion used when building
projections) that was swapping arguments in a let-in, causing projection
generation to fail for any record field containing a let-in expression.

Concludes match (weak) semantics. Yay!

we started Kashima's proof of standardization

match nearing completion

match wsem almost done

- nat.ma: we added a general induction principle
- lambda: we have the diamond property of parallel reduction
          notation bugfixes in term and muktiplicity

- bugfix in stylesheets
- lddl data set released

bugfix in uri's: missing "/" added to baseuri's where necessary

- dehypenation involves helena as well
- now we compile helena against the latest version of matita components

the dehyphenation update continues ...

some corrections to the prose of the web site

web site update

old lambdadelta home page is dismissed

nug fix in the location of images

- lambda: parallel reduction to obtain diamond property
- list:   local "norm" notation removed in favour of "card" core notation

planned dehyphenation of lambdadelta eventually took place!

- bug fix in notation precedences
- bug fix in the Makefile

- labelled sequential reduction started ...
- bug fix in precedence relation on redex pointers

match

- relations.ma:
  we introduced the reflexive closure (RC) for use in lambda and lambda_delta
- lambda:
  we introduced pointers to redexes
  notation bug fix in delifting_substitution.ma

match_step

bug fix in notation precedences

- the theory of delifting substitution is done
- the theory of multiplicity is done

par_test.ma

ennesima versione

splitting files

splitting files

we started the theory of delifting substitution ...

test null, match

- lambda: the theory of lift is complete!
- predefined_virtuals: symbol for lift added

working on match