At:
pred mng 2 wf closed
1
2
2
1
3
1
1
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.
r:rel(). r 
p 
tc(r;ds;da;de)
13.
closed_pred(p)
14.
r: rel()
15.
r p
16.
tc(r;ds;da;de)
tc(r;ds; < > ;de)
By:
Using [`da1',da]
(BackThru
Thm* r:rel(), ds:Collection(dec()), da1,da2:Collection(SimpleType), de:sig(). closed_rel(r) tc(r;ds;da1;de) tc(r;ds;da2;de))
Generated subgoal:
| 1 | closed_rel(r) |
About:
