(65steps) (too big for print form)
Definitions
Lemmas
mb
automata
4
Sections
GenAutomata
Doc
At:
rel
subst
mng
2
iff
3
1
1.
r:
rel()
2.
as:
(Label
Term) List
3.
ds:
Collection(dec())
4.
daa:
Collection(dec())
5.
da:
Collection(SimpleType)
6.
de:
sig()
7.
rho:
Decl
8.
e:
{[[de]] rho}
9.
s:
{[[ds]] rho}
10.
s':
{[[ds]] rho}
11.
k:
Label
12.
a:
[[da]] rho
13.
tr:
trace_env([[daa]] rho)
14.
trace_consistent_rel(rho;daa;tr.proj;r)
15.
tc(r;ds;da;de)
16.
subst_mentions_trace(as)
17.
x:
Label
18.
(x
rel_primed_vars(r))
19.
t:
SimpleType
20.
mk_dec(x, t)
ds
21.
t
term_types(ds;da;de;apply_alist(as;x;x))
1of(e)
{1of([[de]] rho)}
By:
AllHyps (
i.(Analyze i) THEN (All Reduce) THEN Trivial)
Generated subgoals:
None
About:
(65steps) (too big for print form)
Definitions
Lemmas
mb
automata
4
Sections
GenAutomata
Doc
Term) List
subst_mentions_trace(as)
rel_primed_vars(r))
ds
term_types(ds;da;de;apply_alist(as;x;x))
1of(e) {1of([[de]] rho)}
i.(Analyze i) THEN (All Reduce) THEN Trivial)