updated web site

+ updated change log
+ updated site generation procedure

diff --git a/helm/www/lambdadelta/Makefile b/helm/www/lambdadelta/Makefile
index 391b4e1f883d524907b4b3b469df35ddda1a4736..98fb867c78d89d062e18f7a975205bec50266f94 100644 (file)
--- a/helm/www/lambdadelta/Makefile
+++ b/helm/www/lambdadelta/Makefile
@@ -1,25 +1,26 @@
 SHELL := $(shell which bash)
 H=@
 
 SHELL := $(shell which bash)
 H=@
 

+TAGS = up-html up-html-ix up-home html html-ix home ldw ldw-ix
+

 TAGS = www up-html up-css up-images up-download \
        lint-xml index lddl install-xml \
        test-html html install-html \
        install-jed install-bib install-2 install-1 install-coq \
        install-automath install-v install-matita \
 
 TAGS = www up-html up-css up-images up-download \
        lint-xml index lddl install-xml \
        test-html html install-html \
        install-jed install-bib install-2 install-1 install-coq \
        install-automath install-v install-matita \
 

-# LDURL = http://lambdadelta.info/
-LDURL = http://helm.cs.unibo.it/lambdadelta/
+LDWEBURL = http://helm.cs.unibo.it/lambdadelta/

 
 SITEDIR    = html
 
 SITEDIR    = html

-ETCDIR     = etc
-DOWNDIR    = download
-XSLTDIR    = xslt
-XMLDIR     = xml
+HTMLDIR    = html/lddl

 SRCDIR     = web/home
 LDDLDIR    = web/lddl
 XHTBLDIR   = bin/xhtbl
 INDEXDIR   = bin/index
 SRCDIR     = web/home
 LDDLDIR    = web/lddl
 XHTBLDIR   = bin/xhtbl
 INDEXDIR   = bin/index

-HTMLDIR    = html/lddl
+ETCDIR     = etc
+DOWNDIR    = download
+XSLTDIR    = xslt
+XMLDIR     = xml

 JEDDIR     = $(HOME)/mps/jed
 BIBDIR     = $(HOME)/texmf/bibtex/bib
 CONTRIBDIR = $(ETCDIR)/lambdadelta
 JEDDIR     = $(HOME)/mps/jed
 BIBDIR     = $(HOME)/texmf/bibtex/bib
 CONTRIBDIR = $(ETCDIR)/lambdadelta


@@ -36,10 +37,12 @@ RSTATICDIR = /projects/helm/public_html/lambda-delta/static
 
 HTMLSTAMP   = $(ETCDIR)/html.stamp
 HTMLIXSTAMP = $(ETCDIR)/html_ix.stamp
 
 HTMLSTAMP   = $(ETCDIR)/html.stamp
 HTMLIXSTAMP = $(ETCDIR)/html_ix.stamp

+HOMESTAMP   = $(ETCDIR)/home.stamp

 LDWSTAMP    = $(ETCDIR)/ldw.stamp
 LDWIXSTAMP  = $(ETCDIR)/ldw_ix.stamp
 
 SITEMAP     = $(XSLTDIR)/sitemap.xsl
 LDWSTAMP    = $(ETCDIR)/ldw.stamp
 LDWIXSTAMP  = $(ETCDIR)/ldw_ix.stamp
 
 SITEMAP     = $(XSLTDIR)/sitemap.xsl

+TABLES      = $(XSLTDIR)/xhtbl.xsl

 
 SLS     = helena.sl automath.sl
 BIB     = lambdadelta.bib
 
 SLS     = helena.sl automath.sl
 BIB     = lambdadelta.bib


@@ -80,35 +83,14 @@ ifeq ($(XSLT), xalan)
    XSLT       += -indent 2
 endif
 
    XSLT       += -indent 2
 endif
 

-XSLT += $(XSLT_PARAM) baseurl '"$(LDURL)"' $(XSLT_PARAM) date '"$(shell date -R)"'
-
-define HTML_TEMPLATE
-   HTML_$(2)  = $$(SITEDIR)/$(2).html
-   HTMLS     += $$(HTML_$(2))
-
-   $$(HTML_$(2)): $(1) $$(XSLS) $$(LDWEB:%=$$(XSLTDIR)/%)
-       @echo "  XSLT $$(notdir $$<)"
-       $$(H)$$(XSLT) $$(XSLT_OUT) $$@ $$(XSLT_XSL) $$(XSLTDIR)/ld_web.xsl $$(XSLT_IN) $$<
-endef
-
-ifeq ($(MAKECMDGOALS), home)
-   LDWS  = $(shell find -L $(WEBDIRS) -name "*.ldw.xml")
-   TBLS  = $(shell find -L $(WEBDIRS) -name "*.tbl")
-   XSLS  = $(addprefix $(XSLTDIR)/,xhtbl.xsl $(notdir $(TBLS:%.tbl=%.xsl)))
-
-   $(XSLS): $(TBLS) $(XHTBL)
-       @echo "  XHTBL $(XHTBLOPTS) *.tbl"
-       $(H)$(XHTBL) $(XHTBLOPTS) -b $(LDURL) -O $(XSLTDIR) $(TBLS)
-
-   $(foreach LDW,$(LDWS),$(eval $(call HTML_TEMPLATE,$(LDW),$(notdir $(LDW:%.ldw.xml=%)))))
-endif
+XSLT += $(XSLT_PARAM) baseurl '"$(LDWEBURL)"' $(XSLT_PARAM) date '"$(shell date -R)"'

 
 all:
 
 # UPDATE HTML LDDL ###########################################################
 
 $(ETCDIR)/html_lddl.tar.bz2: $(HTMLSTAMP)
 
 all:
 
 # UPDATE HTML LDDL ###########################################################
 
 $(ETCDIR)/html_lddl.tar.bz2: $(HTMLSTAMP)

-       @echo "  INSTALL html"
+       @echo "  UPDATE $(RHOMEDIR)/$(HTMLDIR)/"

        $(H)tar -cjf $@ $(HTMLDIR)
        $(H)scp $@ $(RHOMEDIR)/$(ETCDIR)
        $(H)ssh $(REMOTE) "cd $(RDIR) && tar -xjf $@"
        $(H)tar -cjf $@ $(HTMLDIR)
        $(H)scp $@ $(RHOMEDIR)/$(ETCDIR)
        $(H)ssh $(REMOTE) "cd $(RDIR) && tar -xjf $@"


@@ -118,7 +100,7 @@ up-html: $(ETCDIR)/html_lddl.tar.bz2
 # UPDATE HTML IX LDDL ########################################################
 
 $(ETCDIR)/html_lddl_ix.tar.bz2: $(HTMLIXSTAMP)
 # UPDATE HTML IX LDDL ########################################################
 
 $(ETCDIR)/html_lddl_ix.tar.bz2: $(HTMLIXSTAMP)

-       @echo "  INSTALL html-ix"
+       @echo "  UPDATE $(RHOMEDIR)/$(HTMLDIR)/*/index.html"

        $(H)tar -cjf $@ `find $(HTMLDIR) -name index.html`
        $(H)scp $@ $(RHOMEDIR)/$(ETCDIR)
        $(H)ssh $(REMOTE) "cd $(RDIR) && tar -xjf $@"
        $(H)tar -cjf $@ `find $(HTMLDIR) -name index.html`
        $(H)scp $@ $(RHOMEDIR)/$(ETCDIR)
        $(H)ssh $(REMOTE) "cd $(RDIR) && tar -xjf $@"


@@ -127,14 +109,16 @@ up-html-ix: $(ETCDIR)/html_lddl_ix.tar.bz2
 
 # UPDATE HTML HOME ###########################################################
 
 
 # UPDATE HTML HOME ###########################################################
 

-up-home:
-       @echo "  UPDATE $(RHOMEDIR)/html/"
-       $(H)scp -q html/*.html $(RHOMEDIR)/html/
+up-home: $(HOMESTAMP)
+       @echo "  UPDATE $(RHOMEDIR)/$(SITEDIR)/"
+       $(H)scp -q html/*.html $(RHOMEDIR)/$(SITEDIR)/

 
 # GENERATE HTML LDDL #########################################################
 
 
 # GENERATE HTML LDDL #########################################################
 

-$(HTMLSTAMP): $(LDWSTAMP) $(SITEMAP)
-       $(H)for LDW in `find $(LDDLDIR) -name *.ldw.xml`; do \
+$(HTMLSTAMP): LDWS = `find $(LDDLDIR) -name *.ldw.xml`
+
+$(HTMLSTAMP): $(LDWSTAMP) $(SITEMAP) $(LDWEB:%=$(XSLTDIR)/%)
+       $(H)for LDW in $(LDWS); do \

        TMP=$${LDW/web/html};HTML=$${TMP/ldw.xml/html}; \
        echo "  XSLT $$LDW"; \
        mkdir -p $${HTML%/*}; \
        TMP=$${LDW/web/html};HTML=$${TMP/ldw.xml/html}; \
        echo "  XSLT $$LDW"; \
        mkdir -p $${HTML%/*}; \


@@ -147,8 +131,10 @@ html: $(HTMLSTAMP)
 
 # GENERATE HTML IX LDDL ######################################################
 
 
 # GENERATE HTML IX LDDL ######################################################
 

-$(HTMLIXSTAMP): $(LDWIXSTAMP) $(SITEMAP)
-       $(H)for LDW in `find $(LDDLDIR) -name index.ldw.xml`; do \
+$(HTMLIXSTAMP): LDWS = `find $(LDDLDIR) -name index.ldw.xml`
+
+$(HTMLIXSTAMP): $(LDWIXSTAMP) $(SITEMAP) $(LDWEB:%=$(XSLTDIR)/%)
+       $(H)for LDW in $(LDWS); do \

        TMP=$${LDW/web/html};HTML=$${TMP/ldw.xml/html}; \
        echo "  XSLT $$LDW"; \
        mkdir -p $${HTML%/*}; \
        TMP=$${LDW/web/html};HTML=$${TMP/ldw.xml/html}; \
        echo "  XSLT $$LDW"; \
        mkdir -p $${HTML%/*}; \


@@ -160,7 +146,25 @@ html-ix: $(HTMLIXSTAMP)
 
 # GENERATE HTML HOME #########################################################
 
 
 # GENERATE HTML HOME #########################################################
 

-home: $(HTMLS) $(TBLS) $(XHTBL)
+$(HOMESTAMP): LDWS = `find -L $(WEBDIRS) -name "*.ldw.xml"`
+
+$(HOMESTAMP): $(LDWS) $(TABLES) $(LDWEB:%=$(XSLTDIR)/%)
+       $(H)for LDW in $(LDWS); do \
+       TMP=$${LDW##*/};HTML=$${TMP/ldw.xml/html}; \
+       echo "  XSLT $$LDW"; \
+       $(XSLT) $(XSLT_OUT) $(SITEDIR)/$$HTML $(XSLT_XSL) $(XSLTDIR)/ld_web.xsl $(XSLT_IN) $$LDW; \
+       done
+       $(H)touch $@
+
+home: $(HOMESTAMP)
+
+# GENERATE XSL ###############################################################
+
+$(TABLES) $(SITEMAP): TBLS = `find -L $(WEBDIRS) -name "*.tbl"`
+
+$(TABLES) $(SITEMAP): $(TBLS) $(XHTBL)
+       @echo "  XHTBL $(XHTBLOPTS) *.tbl"
+       $(H)$(XHTBL) $(XHTBLOPTS) -b $(LDWEBURL) -O $(XSLTDIR) $(TBLS)

 
 # GENERATE LDW LDDL ##########################################################
 
 
 # GENERATE LDW LDDL ##########################################################
 


@@ -253,7 +257,5 @@ up-download:
 #      @echo "  XSLT $@"
 #      $(H)mkdir -p $(LDDLDIR)/$(@D)
 #      $(H)$(XSLT) --novalid $(XSLT_OUT) $(LDDLDIR)/$@.ldw.xml $(XSLT_XSL) $(XSLTDIR)/lddl.xsl $(XSLT_IN) $(XMLDIR)/$@.xml
 #      @echo "  XSLT $@"
 #      $(H)mkdir -p $(LDDLDIR)/$(@D)
 #      $(H)$(XSLT) --novalid $(XSLT_OUT) $(LDDLDIR)/$@.ldw.xml $(XSLT_XSL) $(XSLTDIR)/lddl.xsl $(XSLT_IN) $(XMLDIR)/$@.xml

-#      $(H)mkdir -p $(HTMLDIR)/$(@D)
-#      $(H)$(XSLT) $(XSLT_OUT) $(HTMLDIR)/$@.html $(XSLT_XSL) $(XSLTDIR)/ld_web.xsl $(XSLT_IN) $(LDDLDIR)/$@.ldw.xml

 
 .PHONY: $(TAGS)
 
 .PHONY: $(TAGS)

diff --git a/matita/matita/contribs/lambdadelta/Makefile b/matita/matita/contribs/lambdadelta/Makefile
index ff1ebeeefeca0a4465fefdbc3acb3d4637a64ad7..4438f07b5be99ca54236b68d21ee1510311a8aca 100644 (file)
--- a/matita/matita/contribs/lambdadelta/Makefile
+++ b/matita/matita/contribs/lambdadelta/Makefile
@@ -30,7 +30,7 @@ CONTRIB      := lambdadelta_2B
 WWW          := ../../../../helm/www/lambdadelta
 
 TAGS := all xoa xoa2 orig elim deps top leaf stats tbls odeps trim contrib clean \
 WWW          := ../../../../helm/www/lambdadelta
 
 TAGS := all xoa xoa2 orig elim deps top leaf stats tbls odeps trim contrib clean \

-        www up-html
+        home up-home

 
 PACKAGES  := ground_2 static_2 basic_2 apps_2 alpha_1
 XPACKAGES := ground_2 static_2 basic_2
 
 PACKAGES  := ground_2 static_2 basic_2 apps_2 alpha_1
 XPACKAGES := ground_2 static_2 basic_2


@@ -270,13 +270,13 @@ clean:
 
 # www ######################################################################
 
 
 # www ######################################################################
 

-www:
-       $(H)$(MAKE) --no-print-directory -C $(WWW) www
+home:
+       $(H)$(MAKE) --no-print-directory -C $(WWW) home

 
 # www ######################################################################
 
 
 # www ######################################################################
 

-up-html:
-       $(H)$(MAKE) --no-print-directory -C $(WWW) up-html
+up-home:
+       $(H)$(MAKE) --no-print-directory -C $(WWW) up-home

 
 ##############################################################################
 
 
 ##############################################################################
 

diff --git a/matita/matita/contribs/lambdadelta/web/changes.tbl b/matita/matita/contribs/lambdadelta/web/changes.tbl
index bf985679d8c0459016396b8e3a34e02e00eaebd6..42002da8262679b1554aa8cc9317ca23fbbdb42b 100644 (file)
--- a/matita/matita/contribs/lambdadelta/web/changes.tbl
+++ b/matita/matita/contribs/lambdadelta/web/changes.tbl
@@ -12,23 +12,34 @@ table {
        { "@" "" "@" }
        { "+" "-" "*" }
        { "type assignment (terms)"
        { "@" "" "@" }
        { "+" "-" "*" }
        { "type assignment (terms)"

-         "stratified higher validity (terms) removed"
+         "higher validity (terms) removed"

          "primitive validity (terms)"
        }
      ]
      [ [{ "equivalences" * }]
          "primitive validity (terms)"
        }
      ]
      [ [{ "equivalences" * }]

-       { "" "" "" "" }
-       { "+" "+" "+" "-" }
-       { "equivalence for full rt-reduction (terms)"
-         "equivalence for whd rt-reduction (terms)"
-         "equivalence for full rt-reduction (terms, referred lenvs, closures)"
-         "syntactic equivalence (closures) removed"
+       { "" "" "" "" "" }
+       { "+" "+" "+" "+" "-" }
+       { "equivalence for whd rt-reduction (terms)"
+         "equivalence for full rt-reduction (terms, items, referred lenvs, referred closures)"
+         "equivalence up to exclusion binders (selected lenvs)"
+         "syntactic equivalence (items)"
+         "syntactic equivalence (selected closures) removed"

        }
      ]
      [ [{ "partial orders" * }]
        }
      ]
      [ [{ "partial orders" * }]

+       { "" "" "" "" "" }
+       { "+" "+" "+" "+" "+" }
+       { "properties with inclusion (hereditarily free variables)"
+         "inclusion (hereditarily free variables)"
+         "inclusion (applicability)"
+         "switch in primitive order relations (closures) to enable the exclusion binder"
+         "simple weight (items, genvs)"
+       }
+     ]
+     [ [{ "reducibility" * }]

        { "" }
        { "" }

-       { "+" }
-       { "switch in primitive order relations for closures to enable the exclusion binder"
+       { "*" }
+       { "abatract Tait's candidates with 6 postulates"

        }
      ]
      [ [{ "normal form predicates" * }]
        }
      ]
      [ [{ "normal form predicates" * }]


@@ -47,25 +58,57 @@ table {
        { "zero or more refs (terms) removed"
        }
      ]
        { "zero or more refs (terms) removed"
        }
      ]

-     [ [{ "relocation" * }]
-       { "" "" "" "" }
-       { "-" "*" "-" "*" }
-       { "basic slicing (lenvs) removed"
+     [ [{ "relocation and slicing" * }]
+       { "" "" "" "" "" "" }
+       { "+" "-" "*" "-" "+" "*" }
+       { "properties with abstract relocation (terms/items)"
+         "basic slicing (lenvs) removed"

          "primitive finite slicing (lenvs)"
          "primitive finite slicing (lenvs)"

-         "basic relocation (lists of terms) removed"
+         "basic relocation (terms, lists of terms) removed"
+         "primitive finite relocation (items)" 

          "primitive finite relocation (terms, lists of terms)"
        }
      ]
      [ [{ "free varibles" * }]
          "primitive finite relocation (terms, lists of terms)"
        }
      ]
      [ [{ "free varibles" * }]

-       { "" }
-       { "+" }
-       { "union (referred lenvs) removed"
+       { "" "" }
+       { "+" "-" }
+       { "refinement for hereditarily free variables (lenvs)"
+         "union (referred lenvs) removed"
+       }
+     ]
+     [ [{ "helpers" * }]
+       { "" "" "" }
+       { "+" "+" "+" }
+       { "append (restricted closures) wrong on excluded entries"
+         "length (genvs)"
+         "abstract properties with append (lenvs)"
+       }
+     ]
+     [ [{ "extension" * }]
+       { "" "" "" "" "" }
+       { "+" "+" "+" "+" "+" }
+       { "properties with iterated extension (referred lenvs)"
+         "iterated for 3-relations (referred lenvs)"
+         "abstract properties with extension (selected lenvs)"
+         "for 3-relations (selected lenvs)"
+         "for 2-relations and 3-relations (items)"

        }
      ]
      [ [{ "syntax" * }]
        }
      ]
      [ [{ "syntax" * }]

-       { "@" }
-       { "+" }
-       { "exclusion binder for lenvs"
+       { "@" "" }
+       { "+" "+" }
+       { "exclusion binder (lenvs)"
+         "bonding items (lenvs)"
+       }
+     ]
+     [ [{ "parameters" * }]
+       { "" "" "@" "" "@" }
+       { "+" "+" "+" "+" "*" }
+       { "concrete instances (applicability)"
+         "abstract properties (applicability)"
+         "abstract applicability condition"
+         "sort hierarchy properties including strict monotonicity condition based on non-negative integers"
+         "abstract sort hierarchy without properties"

        }
      ]
      [ [{ "ground" * }]
        }
      ]
      [ [{ "ground" * }]


@@ -96,24 +139,26 @@ table {
        }
      ]
      [ [{ "equivalences" * }]
        }
      ]
      [ [{ "equivalences" * }]

-       { "@" "" "@" "" "" "" }
-       { "+" "+" "-" "-" "-" "+" }
+       { "@" "" "@" "" "" "" "" }
+       { "+" "+" "-" "-" "-" "+" "+" }

        { "primitive decomposed rt-equivalence (terms)"
          "single-step context-sensitive r-eqivalence (terms)"
          "primitive context-sensitive r-eqivalence (terms) removed"
          "context-free r-eqivalence (terms) removed"
          "level equivalence (binary arities) removed"
        { "primitive decomposed rt-equivalence (terms)"
          "single-step context-sensitive r-eqivalence (terms)"
          "primitive context-sensitive r-eqivalence (terms) removed"
          "context-free r-eqivalence (terms) removed"
          "level equivalence (binary arities) removed"

-         "syntactic equivalence (selected lenvs, referred lenvs, selected closures)"
+         "properties with syntactic equivalence (referred lenvs)"
+         "syntactic equivalence (selected lenvs, referred lenvs, referred closures)"

        }
      ]
      [ [{ "partial orders" * }]
        }
      ]
      [ [{ "partial orders" * }]

-       { "" "" "" "" "" "" "" }
-       { "+" "*" "+" "-" "-" "-" "-" }
+       { "" "" "" "" "" "" "" "" }
+       { "+" "*" "+" "-" "-" "-" "-" "-" }

        { "big-tree order relations (closures)"
          "primitive order relations for closures"
          "simple weight (restricted closures)"
        { "big-tree order relations (closures)"
          "primitive order relations for closures"
          "simple weight (restricted closures)"

+         "order relation (lenvs) based on look-up removed"

          "order relation (lists of terms) based on lengths removed"
          "order relation (lists of terms) based on lengths removed"

-         "order relations (binary arities) based on weights removed"
+         "order relations (terms, lenvs, binary arities) based on weights removed"

          "simple weights (binary arities) removed"
          "complex weight (terms) removed"
        }
          "simple weights (binary arities) removed"
          "complex weight (terms) removed"
        }


@@ -136,7 +181,7 @@ table {
        { "+" "+" "+" "+" "+" "-" "+" "+" "+" }
        { "evaluation for full rt-reduction (terms)"
          "normal form for full rt-reduction (terms)"
        { "+" "+" "+" "+" "+" "-" "+" "+" "+" }
        { "evaluation for full rt-reduction (terms)"
          "normal form for full rt-reduction (terms)"

-         "irreducible forms for fulld rt-reduction (terms)"
+         "irreducible forms for full rt-reduction (terms)"

          "reducible forms for full rt-reduction (terms)"
          "evaluation for reduction (terms)"
          "normal form for reduction (lists of terms) removed"
          "reducible forms for full rt-reduction (terms)"
          "evaluation for reduction (terms)"
          "normal form for reduction (lists of terms) removed"


@@ -169,7 +214,7 @@ table {
        }
      ]
      [ [{ "degree" * }]
        }
      ]
      [ [{ "degree" * }]

-       { "@" "" "@" "" }
+       { "" "@" "" "@" }

        { "+" "+" "+" "+" }
        { "refinement for degree (lenvs)"
          "degree assignment (terms)"
        { "+" "+" "+" "+" }
        { "refinement for degree (lenvs)"
          "degree assignment (terms)"


@@ -204,7 +249,7 @@ table {
          "refinement (selected lenvs)"
          "append (lenvs)"
          "left cons (lenvs) removed"
          "refinement (selected lenvs)"
          "append (lenvs)"
          "left cons (lenvs) removed"

-         "flat construction clear (lenvs) removed"
+         "flat entry clear (lenvs) removed"

          "sort extraction (lenvs) removed"
          "context predicate (terms) removed"
          "neutral predicate (terms)"
          "sort extraction (lenvs) removed"
          "context predicate (terms) removed"
          "neutral predicate (terms)"


@@ -232,7 +277,7 @@ table {
      ]
      [ [{ "parameters" * }]
        { "" "" }
      ]
      [ [{ "parameters" * }]
        { "" "" }

-       { "+" "-"}
+       { "+" "-" }

        { "concrete sort hierarchies"
          "iterated next function (sort hierarchy) removed"
        }
        { "concrete sort hierarchies"
          "iterated next function (sort hierarchy) removed"
        }


@@ -270,9 +315,10 @@ table {
        }
      ]
      [ [{ "partial orders" * }]
        }
      ]
      [ [{ "partial orders" * }]

-       { "" "" "" "" }
-       { "+" "+" "+" "+" }
-       { "order relation (specialized lists of terms) based on lengths"
+       { "" "" "" "" "" }
+       { "+" "+" "+" "+" "+" }
+       { "order relation (lenvs) based on look-up"
+         "order relation (specialized lists of terms) based on lengths"

          "order relations (terms, lenvs, closures, binary arities) based on weights"
          "simple weights (terms, lenvs, closures, binary arities)"
          "complex weight (terms)"
          "order relations (terms, lenvs, closures, binary arities) based on weights"
          "simple weights (terms, lenvs, closures, binary arities)"
          "complex weight (terms)"


@@ -293,7 +339,7 @@ table {
      [ [{ "normal form predicates" * }]
        { "" }
        { "+" }
      [ [{ "normal form predicates" * }]
        { "" }
        { "+" }

-       { "normal form for context-sensitive reduction (terms, specialized lists of terms)"
+       { "normal form for reduction (terms, specialized lists of terms)"

        }
      ]
      [ [{ "reduction and type synthesis" * }]
        }
      ]
      [ [{ "reduction and type synthesis" * }]


@@ -316,10 +362,9 @@ table {
        }
      ]
      [ [{ "relocation and slicing" * }]
        }
      ]
      [ [{ "relocation and slicing" * }]

-       { "" "" "" "" "" "" "" "" }
-       { "+" "+" "+" "+" "+" "+" "+" "+" }
-       { "order relation (lenvs) based on look-up"
-         "look-up predicate (lenvs)"
+       { "" "" "" "" "" "" "" }
+       { "+" "+" "+" "+" "+" "+" "+" }
+       { "look-up predicate (lenvs)"

          "finite slicing (lenvs)"
          "basic slicing (lenvs)"
          "finite relocation (terms, specialized lists of terms)"
          "finite slicing (lenvs)"
          "basic slicing (lenvs)"
          "finite relocation (terms, specialized lists of terms)"