is mentioned by
Thm* as:(LabelT) List, p:(LabelT), l:Label, d:T. apply_alist([p / as];l;d) ~ if 1of(p) = l 2of(p) else apply_alist(as;l;d) fi | [apply_alist_cons] |
Thm* as:(LabelT) List, d:T, x:Label. (apply_alist(as;x;d) 2of(unzip(as))) apply_alist(as;x;d) = d | [apply_alist_property] |
Def apply_alist(as;l;d) == 2of((first p as s.t. 1of(p) = l else < l,d > )) | [apply_alist] |
Def t.proj == 2of(t) | [trace_env_proj] |
Def t.frame == 2of(2of(2of(2of(2of(t))))) | [ioa_frame] |
Def t.eff == 1of(2of(2of(2of(2of(t))))) | [ioa_eff] |
Def t.pre == 1of(2of(2of(2of(t)))) | [ioa_pre] |
Def t.init == 1of(2of(2of(t))) | [ioa_init] |
Def t.da == 1of(2of(t)) | [ioa_da] |
Def t.rel == 2of(2of(t)) | [pre_rel] |
Def t.acts == 2of(2of(t)) | [frame_acts] |
Def t.typ == 1of(2of(t)) | [frame_typ] |
Def t.smt == 2of(2of(2of(t))) | [eff_smt] |
Def t.typ == 1of(2of(2of(t))) | [eff_typ] |
Def t.args == 2of(t) | [rel_args] |
Def t.typ == 2of(2of(t)) | [smt_typ] |
Def t.term == 1of(2of(t)) | [smt_term] |
Def t.typ == 2of(t) | [dec_typ] |
Def t.rel == 2of(t) | [sig_rel] |
In prior sections: core mb list 1 prog 1 mb record
Try larger context: GenAutomata