(65steps) (too big for print form)
Definitions
Lemmas
mb
automata
4
Sections
GenAutomata
Doc
At:
rel
subst
mng
2
iff
3
2
1
2
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.
x:
Label
17.
(x
rel_primed_vars(r))
18.
t:
SimpleType
19.
mk_dec(x, t)
ds
20.
t
term_types(ds;da;de;apply_alist(as;x;x))
21.
g:
Label
22.
term_mentions_guard(g;apply_alist(as;x;x))
23.
apply_alist(as;x;x) = x
subst_mentions_trace(as)
By:
HypSubstSq -1 -2
THEN
Reduce -2
Generated subgoals:
None
About:
(65steps) (too big for print form)
Definitions
Lemmas
mb
automata
4
Sections
GenAutomata
Doc
Term) List
rel_primed_vars(r))
ds
term_types(ds;da;de;apply_alist(as;x;x))
subst_mentions_trace(as)