Nuprl - Pf pred mng wf

PrintForm Definitions mb automata 4 Sections GenAutomata Doc

p:Fmla, ds,daa:Collection(dec()), da:Collection(SimpleType), de:sig(), rho:Decl, e:{[[de]] rho}, 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) [[p]] rho ds da de e s a tr Prop

By: Unfolds [`trace_consistent_pred`;`pred`;`pred_mng`] 0 THEN Try (Unfold `decl` 0) THEN Try ((AllHyps (Unfold `tc_pred`)) THEN BackThruSomeHyp) THEN Try (Unfold `pred` 0) THEN AllHyps (h.(Unfold `col_all` h) THEN (BackThru h))

Generated subgoals:

None

About:

PrintForm Definitions mb automata 4 Sections GenAutomata Doc