(24steps)
PrintForm
Definitions
Lemmas
mb
automata
4
Sections
GenAutomata
Doc
At:
closed
rel
mng
2
1
2
1.
r:
rel()
2.
rho:
Decl
3.
ds:
Collection(dec())
4.
daa:
Collection(dec())
5.
da1:
Collection(SimpleType)
6.
da2:
Collection(SimpleType)
7.
de:
sig()
8.
s:
{[[ds]] rho}
9.
e:
{[[de]] rho}
10.
a1:
Top
11.
a2:
Top
12.
tr:
trace_env([[daa]] rho)
13.
trace_consistent_rel(rho;daa;tr.proj;r)
14.
tc(r;ds;da1;de)
15.
closed_rel(r)
[[r]] rho ds da1 de e s a1 tr
[[r]] rho ds < > de e s a2 tr
By:
Subst ([[r]] rho ds da1 de e s a1 tr ~ [[r]] rho ds < > de e s a1 tr) 0
Generated subgoals:
1
[[r]] rho ds da1 de e s a1 tr ~ [[r]] rho ds < > de e s a1 tr
2
[[r]] rho ds < > de e s a1 tr
[[r]] rho ds < > de e s a2 tr
About:
(24steps)
PrintForm
Definitions
Lemmas
mb
automata
4
Sections
GenAutomata
Doc