eliminators of arited terms based on "big tree" proper computation

update in basic_2 completed

one file was still missing

update in basic_2

commit is now complete :)

- "big tree" theorem is now proved up to some conjectures involving
just computation
- redefined "big tree" proper computation now replaces its restricted
form and is transitive
- improved definition of "big tree" proper reduction involves lazy
extended computation for local enviroments

- first results on strongly normalizing local environments
- some updates

partial commit ...
- fleq removed and replaced by fpns
- improved proper "big tree" reduction
- some missing lemmas

update in basic_2

third commutation property on lazy equivalence for
local environments proved, multistep version

New approach: we use "iterator" steps in place of pointers.

update in basic_2

first and second commutation property on lazy equivalence for
local environments proved (lleq_fqup_trans, lleq_cpxs_trans) multistep
version

1. more bugs fixed
2. correctness proof completed

update in basic_2

- last patrtial commit of the "reduction" and "computation" components
- we generalized a lemma

More progress.

Some progress in the correctness proof and a bug fixed.

initial commit of the "rduction" component

update in ground_2

commit of the "substitution" component and of some auxiliary files ...

- improved arithmetics for natural numbers with infinity
- some properties of equivalence for local environments
- improved lazy equivalence for local environments
- we commit just the "relocation" component

A first example that uses a status monad where the status is a tree.
It should be possible to implement it imperatively and efficiently.

addition for natural numbers with infinity

update in ground_2, web page for ground_2

definition of equivalence for local environments,
based on natural numbers with infinity

web page for ground_2 and bugfixed statistics generation in the Makefile

strict order relation for natural numbers with inifinity

- natural numbers with infinity for lambdadelta

update in ground_2 ...

- xoa: the definitions file now includes the notations file
- probe: improved "list" algorithm, and bugfixed "remove" algorithm
- lib/lambda: updated and bugfixed dependences to cope with new xoa
- lambdadelta/ground_2: decentralized and bugfixed notation, now copes
with new xoa, some refactoring

Final version of the binary machine (all proofs completed).

Closes many daemons.

Full rework of the semantics of the binary machine (now completely working
up to arithmetical proofs)

Almost finished...

Major bugfix/reorganization/improvement of the partial proofs: full semantics
of the binary machine should now be easy.

update in basic_2

second and third commutation property on lazy equivalence for
local environments proved (lleq_cpx_trans, lleq_lpx_trans)

update in basic_2 (bugfix)
probe was not run so statistic data were outdated

update in basic_2

- lambdadelta: first commutation property on lazy equivalence for
local environments proved (lleq_fqu_trans)
- matitadep: now three input syntaxes from grep are understood

lazy equivalence for local environments is now defined
its reflexivity reveals a bug in ldrop :(

Splitted star

update in basic_2

- lambdadelta: tentative definition of lazy equivalence for closures +
Makefile update/bugfix to support matitadep update
- matitadep: bug fix in redundancy check + new option shows leaf
nodes

update in basic_2

- bug fix in the connection between global and restricted big-tree
proper computation
- one file was not committed :(

update in basic_2

- bug fix in the induction for the closure property
- some renaming

full.ma

some additions needed for lambda_delta

update in basic_2 ...

- "small step" version of "big tree" theorem proved
- some renaming

step (almost) done

The step machine (draft)

many changes

Completes all the phases of the binary machine (modulo axioms).
Final semantic result still missing.

more results towards the "big-tree" theorem ...

Slowly porting to an enriched tape alphabet

The moves (almost)

added sem_seq_app for the mono case

renaming files

strongly normalizing terms for big-tree reduction are now defined ...

almost there

Completed phases 0, 1, and 3.

update in basic_2

some renaming ...

Still a problem to be fixed: after reaching the border we must always add
blank.

shift a trace from an extremity

splitting files

Moved multi_to_mono.ma inside multi_to_mono

Added a new directory for multi to mono

update in basic_2

bug fix in supclosure allows alternative definition of fpbs !

progress in the semantics of binary machines

bugfix in possible alternative definition of fpbs

some improvements towards an alternative definition of fpbs ...

Starting proof about semantics of binary machines.

Completes the  definition of binaryTM.

progress in the deifinition of the semantics of the shift move.
--

update in basic_2

bug fix in big-tree reduction

update in basic_2

- big-tree reduction is now based on extended reduction
- some renaming

final na,e for big-tree rediction and computation

update in basic_2

lenv refinement for native validity removed from big tree reduction

update in basic_2

- degree assignment, static type assignment, iterated static type
assignment and lenv refinement for native validity reaxiomatized to
move lsubsv_snv_trans out of the mutual induction for preservation
- minor stylistic improvements and Makefile bugfix

Adds transformation of generic monotape machines into machines using a binary
alphabet (first commit, doesn't typecheck)

a vector of finsets is a finset (in progress)

previous commit continued :)

support for nat-labeled reflexive and transitive closure added to lambdadelta

- test.ma on the disambiguation bug moved to ONAG (just out of the way)
- lambdadelta: updated interpretation descriptions fix the disambiguation bug

- the example is now minimal so the bug is understood.
  two interpretations of the same notation with the same description
  override eachother, so the description is not just informative :)
- more keywords added for highlighting

- the example is smaller and really self-contained ...
- two keywords added for highlighting

riduced example showing disambiguation bug ...

- matitadep: new option -t to list the unreferenced sources
- lambdadelta: Makefile update to use matitadep -t
               redundant dependecy removed in cl_weight
       test.ma: shows a bug in the disambiguation mechanism

- we added nat-labeled reflexive and transitive closure (for use in lambdadelta)
- stylistic improvements in list-labeled reflexive and transitive closure

milestone in basic_2