name "basic_1_src"

table uri "static/coq/lambdadelta/basic_1/" ext ".txt" {
   class "gray"
   [ { "component" * } {
        [ { "plane" * } {
             [ "files" * ]
          }
        ]
     }
   ]
   class "wine"
   [ { "examples" * } {
        [ { "terms with special features" * } {
             [ @@"levels_ex0" + @@"ty3_ex1" + @@"nf2_ex2" * ]
          }
        ]
     }
   ]
   class "magenta"
   [ { "" * } {
        [ { "" * } {
             [ "" * ]
          }
        ]
     }
   ]
(*   
   [ { "higher order dynamic typing" * } {
        [ { "higher order native type assignment" * } {
             [ "ntas ( ⦃?,?⦄ ⊢ ? :* ? )" "nta_lift" * ]
          }
        ]
     }
   ]
*)
   class "prune"
   [ { "dynamic typing" * } {
        [ { "well-formed contexts" * } {
             [ @@"wf3_defs" @@"wf3_props" * ]
          }
        ]
        [ { "context ref. for native type assignment" * } {
             [ @@"csubt_defs" @@"csubt_props" + @@"csubt_arity_props" * ]
          }
        ]
        [ { "native type assignment" * } {
             [ @@"ty3_defs" @@"ty3_props" + @@"ty3_gen" + @@"ty3_gen_context" + @@"ty3_gen_nf2" + @@"ty3_lift" + @@"ty3_subst0" + @@"ty3_arity_props" + @@"ty3_nf2_gen" + @@"ty3_sred" + @@"ty3_sred_props" + @@"ty3_dec" * ]
          }
        ]
     }
   ]
   class "blue"
   [ { "equivalence" * } {
        [ { "context-sensitive equivalence" * } {
             [ @@"pc3_defs" @@"pc3_props" + @@"pc3_gen" + @@"pc3_gen_context" + @@"pc3_subst0" * ]
          }
        ]
        [ { "context-free equivalence" * } {
             [ @@"pc1_defs" @@"pc1_props" * ]
          }
        ]
     }
   ]
   class "sky"
   [ { "" * } {
        [ { "" * } {
             [ "" * ]
          }
        ]
     }
   ]
   class "cyan"
   [ { "computation" * } {
        [ { "context ref. for reducibility" * } {
             [ @@"csubc_defs" @@"csubc_props" * ]
          }
        ]
        [ { "reducibility" * } {
             [ @@"sc3_defs" @@"sc3_props" + @@"sc3_arity" * ]
          }
        ]
        [ { "strongly normalizing computation" * } {
             [ @@"sn3_defs" @@"sn3_gen" + @@"sn3_props" * ]
          }
        ]
        [ { "context-sensitive computation" * } {
             [ @@"pr3_defs" @@"pr3_props" + @@"pr3_gen" + @@"pr3_gen_context" + @@"pr3_iso" + @@"pr3_subst1" + @@"pr3_confluence" * ]
          }
        ]
        [ { "context-free computation" * } {
             [ @@"pr1_defs" @@"pr1_props" + @@"pr1_confluence" * ]
          }
        ]
     }
   ]
   class "water"
   [ { "reduction" * } {
        [ { "normal forms for context-sensitive reduction" * } {
             [ @@"nf2_defs" @@"nf2_props" + @@"nf2_gen" + @@"nf2_dec" * ]
          }
        ]
        [ { "context-sensitive reduction" * } {
             [ @@"pr2_defs" @@"pr2_gen" + @@"pr2_gen_context" + @@"pr2_lift" + @@"pr2_subst1" + @@"pr2_confluence" * ]
          }
        ]
        [ { "normal forms for context-free reduction" * } {
             [ "" @@"nf0_dec" * ]
          }
        ]
        [ { "context-free reduction" * } {
             [ @@"wcpr0_defs" * ]
             [ @@"pr0_defs" @@"pr0_gen" + @@"pr0_lift" + @@"pr0_subst0" + @@"pr0_subst1" + @@"pr0_confluence" * ]
          }
        ]
     }
   ]
   class "green"
   [ { "unfold" * } {
        [ { "iterated static type assignment" * } {
             [ @@"sty1_defs" @@"sty1_props" * ]
          }
        ]
     }
   ]
   class "grass"
   [ { "static typing" * } {
        [ { "static type assignment" * } {
             [ @@"sty0_defs" @@"sty0_props" * ]
          }
        ]
        [ { "context ref. for binary arity assignment" * } {
             [ @@"csuba_defs" @@"csuba_props" * ]
          }
        ]
        [ { "binary arity assignment" * } {
             [ @@"arity_defs" @@"arity_props" + @@"arity_gen" + @@"arity_subst0" + @@"arity_sred" * ]
          }
        ]
        [ { "binary arity" * } {
             [ @@"levels_defs" + @@"llt_defs" + @@"aprem_defs" * ]
          }
        ]
        [ { "parameters" * } {
             [ @@"parameter_defs" * ]
          }
        ]
        [ { "basic context ref." * } {
             [ @@"csubv_defs" * ]
          }
        ]
     }
   ]
   class "yellow"
   [ { "multiple substitution" * } {
        [ { "iterated context slicing" * } {
             [ @@"drop1_defs" @@"drop1_props" * ]
          }
        ]
        [ { "generic term relocation" * } {
             [ @@"lift1_defs" @@"lift1_props" * ]
          }
        ]
     }
   ]
   class "orange"
   [ { "substitution" * } {
        [ { "ordinary substitution" * } {
             [ @@"subst_defs" @@"subst_props" * ]
             [ @@"csubst1_defs" @@"csubst1_props" * ]
             [ @@"subst1_defs" @@"subst1_gen" + @@"subst1_lift" + @@"subst1_subst1" + @@"subst1_confluence" * ]
          }
        ]
        [ { "normal forms for ordinary strict substitution" * } {
             [ "" @@"dnf_dec" * ]
          }
        ]
        [ { "ordinary strict substitution" * } {
             [ @@"fsubst0_defs" * ]
             [ @@"csubst0_defs" * ]
             [ @@"subst0_defs" @@"subst0_gen" + @@"subst0_tlt" + @@"subst0_lift" + @@"subst0_subst0" + @@"subst0_confluence" * ]
          }
        ]
        [ { "basic local env. slicing" * } {
             [ @@"getl_defs" @@"getl_props" * ]
             [ @@"drop_defs" @@"drop_props" * ]
          }
        ]
        [ { "basic term relocation" * } {
             [ @@"lift_defs" @@"lift_props" + @@"lift_gen" + @@"lift_tlt" * ]
          }
        ]
     }
   ]
   class "red"
   [ { "grammar" * } {
        [ { "closures" * } {
             [ @@"flt_defs" * ]
          }
        ]
        [ { "contexts" * } {
             [ @@"contexts_defs" + @@"clt_defs" + @@"ctail_defs" + @@"app_defs" + @@"cnt_defs" * ]
          }
        ]
        [ { "terms" * } {
             [ @@"tlist_defs" * ]
             [ @@"terms_defs" + @@"tlt_defs" + @@"iso_defs" * ]
          }
        ]
     }
   ]
}

class "top"               { * }

class "capitalize italic" { 0 }

class "italic"            { 1 }