At:
vcs mng wf
1
1.
vs: vc{i:l}()
Prop{i'}
2.
ds: dec()Prop{i}
3.
da: dec()Prop{i}
4.
de: sig()
5.
rho: LabelType{i}
6.
e: {sig_mng{i:l}
(de; rho)}
7.
s: {[[ds]] rho}
8.
tr: trace_env([[da]] rho)
9.
tc_vcs{i}(vs;ds;da;de)
10.
(
v
vs.trace_consistent_vc(rho;da;tr.proj;v))
11.
v: vc{i:l}()
12.
v vs
trace_consistent_vc(rho;da;tr.proj;v)
By:
EasyHypThen Auto
Generated subgoals:
None
About:
