class "yellow"
[ { "models" * } {
[ { "term model" * } {
- [ "tm" + "( ⇡[?]? )" + "( ⇡[?←?]? )"
- "tm_exteq"
- * ]
+ [ "tm" * ]
}
]
[ { "denotational equivalence" * } {
*)
class "orange"
[ { "functional" * } {
-(*
- [ { "reduction and type machine" * } {
- [ "rtm" "rtm_step ( ? ⇨ ? )" * ]
+ [ { "multiple filling" * } {
+ [ "mf" + "( ●[?,?]? )" "mf_exeq" "mf_lifts" "mf_cpr" *]
+ [ "mf_vpush" + "( ⇡[?←?]? )" "mf_vpush_exteq" "mf_vpush_vlift" * ]
+ [ "mf_vlift" + "( ⇡[?]? )" "mf_vlift_exteq" * ]
+ [ "mf_v" * ]
}
]
-*)
[ { "relocation" * } {
- [ "flifts" + "( ↑*[?]? )" + "( ↑[?]? )"
- "flifts_basic" + "( ↑[?,?]? )"
- * ]
+ [ "flifts_basic" + "( ↑[?,?]? )" "flifts_flifts_basic" * ]
+ [ "flifts" + "( ↑*[?]? )" + "( ↑[?]? )" "flifts_flifts" * ]
}
]
}
[ "vdrop" + "( ⫰{?}? )" + "( ⫰{?}[?]? )" "vdrop_vlift" * ]
}
]
+ [ { "reduction and type machine" * } {
+ [ "rtm" "rtm_step ( ? ⇨ ? )" * ]
+ }
+ ]
*)