+ class "yellow"
+ [ { "models" * } {
+ [ { "term model" * } {
+ [ "tm" * ]
+ }
+ ]
+ [ { "denotational equivalence" * } {
+ [ "deq" + "( ? ⊢ ? ≗{?} ? )" "deq_cpr" * ]
+ }
+ ]
+ [ { "local environment interpretation" * } {
+ [ "li" + "( ? ϵ ⟦?⟧{?}[?] )" "li_vpushs" * ]
+ }
+ ]
+ [ { "multiple evaluation push" * } {
+ [ "vpushs" + "( ?⨁{?}[?]? ≘ ? )" "vpush_fold" * ]
+ }
+ ]
+ [ { "evaluation equivalence" * } {
+ [ "veq" + "( ? ≗{?} ? )" "veq_lifts" * ]
+ }
+ ]
+ [ { "model declaration" * } {
+ [ "model" + "( ? ≗{?} ? )" + "( ? @{?} ? )" + "( ⟦?⟧{?}[?,?] )"
+ "model_vpush" + "( ⫯{?}[?←?]? )"
+ "model_props"
+ * ]
+ }
+ ]
+ }
+ ]