(8steps) PrintForm Definitions Lemmas mb automata 3 Sections GenAutomata Doc

At: tproj w f2 1 1 1 1
1. da: Collection(dec())
2. rho: Decl
3. tr: trace_env([[da]] rho)
4. y1: Label
5. trace_consistent(rho;da;tr.proj;trace(y1))
6. tr.y1 {a:([[da]] rho)| tr.proj(y1,kind(a)) } List

({a:([[da]] rho)| tr.proj(y1,kind(a)) } List) (rho(lbl_pr( < Trace, y1 > )))
By: AllHyps (h.(Unfold `trace_consistent` h) THEN (Reduce h) THEN (InstHyp [y1] h))
Generated subgoals:

15. g:Label. y1 = g subtype_rel(({a:([[da]] rho)| tr.proj(g,kind(a)) } List); (rho(lbl_pr( < Trace, g > ))))
6. tr.y1 {a:([[da]] rho)| tr.proj(y1,kind(a)) } List
y1 = y1
25. g:Label. y1 = g subtype_rel(({a:([[da]] rho)| tr.proj(g,kind(a)) } List); (rho(lbl_pr( < Trace, g > ))))
6. tr.y1 {a:([[da]] rho)| tr.proj(y1,kind(a)) } List
7. subtype_rel(({a:([[da]] rho)| tr.proj(y1,kind(a)) } List); (rho(lbl_pr( < Trace, y1 > ))))
({a:([[da]] rho)| tr.proj(y1,kind(a)) } List) (rho(lbl_pr( < Trace, y1 > )))

About:
listassertsetapplymembersubtype

(8steps) PrintForm Definitions Lemmas mb automata 3 Sections GenAutomata Doc