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

At: pred mng 2 wf closed 1 2 2
1. p: Fmla
2. ds: Collection(dec())
3. daa: Collection(dec())
4. da: Collection(SimpleType)
5. de: sig()
6. rho: Decl
7. e: {[[de]] rho}
8. s: {[[ds]] rho}
9. s': {[[ds]] rho}
10. tr: trace_env([[daa]] rho)
11. trace_consistent_pred(rho;daa;tr.proj;p)
12. tc_pred(p;ds;da;de)
13. closed_pred(p)
14. r: rel()
15. r p

rel_mng_2(r; rho; ds; da; de; e; s; s'; ; tr) Prop
By: Assert (rel_mng_2(r; rho; ds; < > ; de; e; s; s'; ; tr) Prop)
Generated subgoals:

1 rel_mng_2(r; rho; ds; < > ; de; e; s; s'; ; tr) Prop
216. rel_mng_2(r; rho; ds; < > ; de; e; s; s'; ; tr) Prop
rel_mng_2(r; rho; ds; da; de; e; s; s'; ; tr) Prop

About:
itmemberprop

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