(65steps) (too big for print form) Definitions Lemmas mb automata 4 Sections GenAutomata Doc

At: rel subst mng 2 iff 3
1. r: rel()
2. as: (LabelTerm) List
3. ds: Collection(dec())
4. daa: Collection(dec())
5. da: Collection(SimpleType)
6. de: sig()
7. rho: Decl
8. e: {[[de]] rho}
9. s: {[[ds]] rho}
10. s': {[[ds]] rho}
11. k: Label
12. a: [[da]] rho
13. tr: trace_env([[daa]] rho)
14. trace_consistent_rel(rho;daa;tr.proj;r)
15. tc(r;ds;da;de)
16. subst_mentions_trace(as)
17. x: Label
18. (x rel_primed_vars(r))
19. t: SimpleType
20. mk_dec(x, t) ds
21. t term_types(ds;da;de;apply_alist(as;x;x))

[[apply_alist(as;x;x)]] 1of(e) s a tr [[t]] rho
By: Using [`ds',ds;`da',daa;`de',de] (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)
Generated subgoals:

1 1of(e) {1of([[de]] rho)}
2 trace_consistent(rho;daa;tr.proj;apply_alist(as;x;x))

About:
productlistassertmember

(65steps) (too big for print form) Definitions Lemmas mb automata 4 Sections GenAutomata Doc