Def tc_vc(v;ds;da;de) == Case(v) Case vc_imp(hc) = > tc_pred(hc.hyp;ds; < > ;de) & tc_pred(hc.concl;ds; < > ;de) Case vc_qimp(qhc) = > tc_pred(qhc.hyp;ds;dec_lookup(da;qhc.lbl);de) & tc_pred(qhc.concl;ds;dec_lookup(da;qhc.lbl);de) Default = > False
is mentioned
In prior sections:
mb automata 4
