At:
pred mng functionality12123
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.
(rp1.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(). r p1 [[r]] rho ds1 da1 de e s a tr
21.
r: rel()
22.
r p2
23.
[[r]] rho ds1 da1 de e s a tr
24.
[[r]] rho ds1 da1 de e s a tr [[r]] rho ds2 da2 de e s a tr
25.
[[r]] rho ds1 da1 de e s a tr [[r]] rho ds2 da2 de e s a tr
[[r]] rho ds2 da2 de e s a tr
By:
ThinTrivial
THEN
Trivial
Generated subgoals:
r
p1.trace_consistent_rel(rho;daa;tr.proj;r))
tc(r;ds1;da1;de)
[[r]] rho ds2 da2 de e s a tr