At:
pred mng functionality
1
2
4
1
1.
p1: Collection(rel())
2.
p2: Collection(rel())
3.
ds1: Collection(dec())
4.
ds2: Collection(dec())
5.
daa: Collection(dec())
6.
da1: Collection(SimpleType)
7.
da2: Collection(SimpleType)
8.
de: sig()
9.
rho: Decl
10.
e: {[[de]] rho}
11.
s: {[[ds1]] rho}
12.
a: [[da1]] rho
13.
tr: trace_env([[daa]] rho)
14.
(
r
p1.trace_consistent_rel(rho;daa;tr.proj;r))
15.
r:rel(). r p1 
tc(r;ds1;da1;de)
16.
p1 = p2
17.
ds1 = ds2
18.
da1 = da2
19.
s {[[ds2]] rho}
20.
r: rel()
21.
r p2
a [[da2]] rho
By:
Using [`sts1',da1]
(BackThru
Thm* sts1,sts2:Collection(SimpleType), rho:Decl, v:[[sts1]] rho. sts1 = sts2 v [[sts2]] rho)
Generated subgoals:
None
About:
