PrintForm Definitions mb automata 4 Sections GenAutomata Doc

At: pred mng 2 wf

p:Fmla, ds,daa:Collection(dec()), da:Collection(SimpleType), de:sig(), rho:Decl, e:{[[de]] rho}, s,s':{[[ds]] rho}, a:[[da]] rho, tr:trace_env([[daa]] rho). trace_consistent_pred(rho;daa;tr.proj;p) tc_pred(p;ds;da;de) pred_mng_2(p; rho; ds; da; de; e; s; s'; a; tr) Prop
By:
Unfolds [`trace_consistent_pred`;`pred`;`pred_mng_2`] 0
THEN
Try (Unfold `decl` 0)
THEN
EasyHypThen Auto
THEN
Try (Unfold `pred` 0)
Generated subgoals:

None

About:
memberpropimpliesall

PrintForm Definitions mb automata 4 Sections GenAutomata Doc