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

passive support for global environments completed!

partial commit: "conversion" and "equivalence" components ...

partial commit: "computation" component ...

partial commit: "reduction" component

partial commit: "unfold" component

partial commit: "static" component ....

partial commit: just the components before "static" ...

- the milestone was not reported on the web page!
- we say on the web pages how nodes are counted

milesone in basic_2!

- probe: critical bug fixed (all objects were deleted due to wrong test)
- lambdadelta: lenv refinement for atomic arity assignment updated,
               some renaming and notational change
reaxiomatization of beta-reduction complete! (milestone)

lambdadelta
- we changed the beta-reductum to make reduction a special case of
  extended reduction, the lenv refinement for native validity was
  updated accordingly
- we parked restricted reduction, substitution and lenv refinement for
  static type assignment
- active notations are now one per file and are included by nead: this
  avoids time-wasting recompilations when notations are added, removed,
  or changed
- Makefile: some speed up, uses new version of mac, handles auxiliary
  xoa files that can be included by need to avoid time-wasting
  recompilations when xoa objects are added
mac
- now outputs the pages count
probe
- minor bug fix: exceptions during file removal where not cought

milestone in basic_2

- new extendedd beta-reductum involving native type annotation
- extended strong normalization for simply typed terms (milestone)
- some renaming

partial commit of the components before "conversion"
- some work on extended reduction and computation
- some renaming

update in basic_2

- bug fix il ldrop (interesting), fsup, fsups
- now fsupq is the reflexive closure of fsup, as expected
- some renaming

- partial commit :(
  some work on supclosure and extended reduction ...

update in basic_2

more results on extended reduction

some work on extended reduction ...

update in basic_2

redundant dependence removed

- a comment removed

- induction on supclosure replaces induction on weight for closures everywhere
- bug fix in csn_alt

update in basic_2 and apps_2

- basic_2: induction for preservation results now uses supclosure
relation rather than weight on closures
- app_2: "functional" component updated
- we park delifting substitution for now

iteration.ma

bounded quantifiers and pidgeon_hole

gap.ma

Nuovi files

commit by user andrea

commit by user andrea

commit by user andrea

Error to debug

Improved version

more functions

partial update in basic_2

- some renaming
- finally we issue the "dynamic" component

partial commit of the "dynamic" component

partial update in basic_2 ...

- partial commit: we issue the "conversion" and "equivalence" components
- we park conversion and equivalence on local environments for the moment

partial commit in basic_2

partial commit: finaly we issue the "computation" component ...

- partial commit: refactoring in the components before "computation"

partial update in basic_2

- partial commit (just the components before computation)
- we park head normal forms for the moment
- some refactoring

reverse complexity

Bumped to 0.99.2.

Missing include.

chapter9

tutorial

Old version dropped.

New notation for congruence

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

M    chebyshev/chebyshev_psi.ma
D    chebyshev/chebyshev_B.ma

commit by user ricciott

A few integrations (closed an axiom in finset).

commit by user andrea

commit by user andrea