Nuprl - Pf ioa mng wf 5 2 1

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

1. A: ioa{i:l}()
2. de: sig()
3. rho: Decl
4. e: {[[de]] rho}
5. tc_pred(A.init;A.ds; < > ;de)
6. p:pre(). p A.pre tc(p.rel;A.ds;dec_lookup(A.da;p.kind);de)
7. ef:eff(). ef A.eff mk_dec(ef.kind, ef.typ) A.da & tc_eff(ef;A.ds;de)
8. f:frame(). f A.frame mk_dec(f.var, f.typ) A.ds
9. ioa_mentions_trace(A)
10. niltrace() trace_env([[A.da]] rho)
11. s1: {[[A.ds]] rho}
12. a: ([[A.da]] rho)
13. s2: {[[A.ds]] rho}
14. ef: eff()
15. ef A.eff
16. ef.kind = kind(a)

mentions_trace(ef.smt.term)

By: AllHyps (h.(Unfold `ioa_mentions_trace` h) THEN (ParallelOp h))

Generated subgoal:

1 9. niltrace() trace_env([[A.da]] rho)
10. s1: {[[A.ds]] rho}
11. a: ([[A.da]] rho)
12. s2: {[[A.ds]] rho}
13. ef: eff()
14. ef A.eff
15. ef.kind = kind(a)
16. mentions_trace(ef.smt.term)
(e:eff(). e A.eff & mentions_trace(e.smt.term)) (p:pre(). p A.pre & rel_mentions_trace(p.rel)) (r:rel(). r A.init & rel_mentions_trace(r))

About:

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