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

At: rel mng 2 wf


r:rel(), ds,da:Collection(dec()), de:sig(), rho:Decl, st1:Collection(SimpleType), e:{[[de]] rho}, s,s':{[[ds]] rho}, a:[[st1]] rho, tr:trace_env([[da]] rho). trace_consistent_rel(rho;da;tr.proj;r) tc(r;ds;st1;de) rel_mng_2(r; rho; ds; st1; de; e; s; s'; a; tr) Prop

By:
Unfold `rel_mng_2` 0
THEN
UnivCD
THEN
MoveToConcl -1


Generated subgoals:

11. r: rel()
2. ds: Collection(dec())
3. da: Collection(dec())
4. de: sig()
5. rho: Decl
6. st1: Collection(SimpleType)
7. e: {[[de]] rho}
8. s: {[[ds]] rho}
9. s': {[[ds]] rho}
10. a: [[st1]] rho
11. tr: trace_env([[da]] rho)
12. trace_consistent_rel(rho;da;tr.proj;r)
tc(r;ds;st1;de) list_accum(x,t.x([[t]] 1of(e) s s' a tr);[[r.name]] rho 2of(e) ;r.args) Prop
21. r: rel()
2. ds: Collection{i}(dec())
3. da: Collection{i}(dec())
4. de: sig()
5. rho: Decl{i}
6. st1: Collection{i}(SimpleType)
7. sig_mng{i:l}(de; rho) = sig_mng{i:l}(de; rho)
8. zzz: Decl{i}Decl{i'}
Decl{i} Decl{i'}

About:
applymembersubtypepropimpliesall

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