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

At: tproj w f2 1 1 1 1 2 1
1. da: Collection(dec())
2. rho: Decl
3. tr: trace_env([[da]] rho)
4. y1: Label
5. 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 > ))))
8. x: {a:([[da]] rho)| tr.proj(y1,kind(a)) } List

x rho(lbl_pr( < Trace, y1 > ))
By: SubsumeC ({a:([[da]] rho)| tr.proj(y1,kind(a)) } List)
Generated subgoals:

None

About:
listassertsetapplymemberimpliesall

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