Nuprl - Pf vc mng wf 2

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

1. y: qimp{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(y.hyp;ds;dec_lookup(da;y.lbl);de) & tc_pred(y.concl;ds;dec_lookup(da;y.lbl);de)
10. trace_consistent_pred(rho;da;tr.proj;y.hyp)
11. trace_consistent_pred(rho;da;tr.proj;y.concl)

(v:[[dec_lookup(da;y.lbl)]] rho. [[y.hyp]] rho ds dec_lookup(da;y.lbl) de e s v tr [[y.concl]] rho ds dec_lookup(da;y.lbl) de e s v tappend(tr; < y.lbl,v > )) Prop

By: Analyze THENL [Auto;Analyze] THEN 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 (Unfold `tappend` 0) THEN Reduce 0 THEN Try Trivial

Generated subgoal:

1 9. tc_pred(y.hyp;ds;dec_lookup(da;y.lbl);de)
10. tc_pred(y.concl;ds;dec_lookup(da;y.lbl);de)
11. trace_consistent_pred(rho;da;tr.proj;y.hyp)
12. trace_consistent_pred(rho;da;tr.proj;y.concl)
13. v: [[dec_lookup(da;y.lbl)]] rho
14. [[y.hyp]] rho ds dec_lookup(da;y.lbl) de e s v tr
< y.lbl,v > ([[da]] rho)

About:

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