(4steps) PrintForm Definitions Lemmas mb automata 4 Sections GenAutomata Doc

At: vc mng wf 1

1. x: imp{i:l}()
2. ds: Collection(dec())
3. da: Collection(dec())
4. de: sig()
5. rho: Decl
6. e: {[[de]] rho}
7. s: {[[ds]] rho}
8. tr: trace_env([[da]] rho)
9. tc_pred(x.hyp;ds; < > ;de) & tc_pred(x.concl;ds; < > ;de)
10. trace_consistent_pred(rho;da;tr.proj;x.hyp)
11. trace_consistent_pred(rho;da;tr.proj;x.concl)

([[x.hyp]] rho ds < > de e s mk_trace_env(nil, tr.proj) [[x.concl]] rho ds < > de e s mk_trace_env(nil, tr.proj)) Prop

By:
Analyze
THEN
Using [`daa',da] (BackThru Thm* 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)
THEN
Try (BackThru Thm* v:Top, rho:Decl. v [[ < > ]] rho)
THEN
Reduce 0


Generated subgoals:

None

About:
nilitmemberpropimpliesand

(4steps) PrintForm Definitions Lemmas mb automata 4 Sections GenAutomata Doc