mk_trace_env(nil, tr.proj) 
[[hc.concl]] rho ds < > de e s mk_trace_env(nil, tr.proj) Case vc_qimp(qhc) = > 
v:[[dec_lookup(da;qhc.lbl)]] rho. [[qhc.hyp]] rho ds dec_lookup(da;qhc.lbl) de e s v tr [[qhc.concl]] rho ds dec_lookup(da;qhc.lbl) de e s v tappend(tr; < qhc.lbl,v > ) Default = > False
is mentioned
In prior sections: mb automata 4