(11steps)
PrintForm
Definitions
Lemmas
mb
automata
4
Sections
GenAutomata
Doc
At:
closed
pred
mng
1
1
1.
p:
Fmla
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_pred(rho;daa;tr.proj;p)
14.
tc_pred(p;ds;da1;de)
15.
closed_pred(p)
(
r:rel(). r
p
[[r]] rho ds da1 de e s a1 tr)
Prop
By:
RepeatFor 2 (Analyze THEN (Try (Complete (Auto THEN (Fold `pred` 0)))))
Generated subgoal:
1
16.
r:
rel()
17.
r
p
[[r]] rho ds da1 de e s a1 tr
Prop
About:
(11steps)
PrintForm
Definitions
Lemmas
mb
automata
4
Sections
GenAutomata
Doc
p
[[r]] rho ds da1 de e s a1 tr Prop
(
r:rel(). r p 
[[r]] rho ds da1 de e s a1 tr) Prop
p [[r]] rho ds da1 de e s a1 tr Prop
