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

At: ioa mng wf 5
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)

[[ef.smt.term]] 1of(e) s1 value(a) niltrace() [[ef.smt.typ]] rho
By:
Using [`de',de;`st1', < ef.typ > ;`da',A.da] (BackThru Thm* ds,da:Collection(dec()), st1:Collection(SimpleType), de:sig(), rho:Decl, t:Term, s:{[[ds]] rho}, e:{1of([[de]] rho)}, a:SimpleType, v:[[st1]] rho, tr:trace_env([[da]] rho). trace_consistent(rho;da;tr.proj;t) a term_types(ds;st1;de;t) [[t]] e s v tr [[a]] rho)
THEN
AllHyps (i.(Analyze i) THEN (Reduce 0) THEN Trivial)
Generated subgoals:

1 value(a) [[ < ef.typ > ]] rho
2 trace_consistent(rho;A.da;niltrace().proj;ef.smt.term)
3 ef.smt.typ term_types(A.ds; < ef.typ > ;de;ef.smt.term)

About:
equalmemberimpliesandall

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