At:
rel mng 2 iff
1
1
2
1
4
1.
y: Label
2.
ds: Collection(dec())
3.
daa: Collection(dec())
4.
da: Collection(SimpleType)
5.
de: sig()
6.
rho: Decl
7.
e1: {1of([[de]] rho)}
8.
e2: l:Label
reduce(
s,m. [[s]] rhom;Prop;de.rel(l))
9.
s1: {[[ds]] rho}
10.
s2: {[[ds]] rho}
11.
a: [[da]] rho
12.
tr: trace_env([[daa]] rho)
13.
l1: Term List
14.
u: Term
15.
v: Term List
16.
l2:Term List.
||v|| = ||l2|| 
(ls:SimpleType List.
||ls|| = ||v|| 
(f:reduce(s,m. [[s]] rhom;Prop;ls).
(i:||v||. trace_consistent(rho;daa;tr.proj;v[i]))
(i:||l2||. trace_consistent(rho;daa;tr.proj;l2[i]))
||ls|| = ||v|| & (i:. i < ||v|| ls[i] term_types(ds;da;de;v[i]))
||ls|| = ||l2|| & (i:. i < ||l2|| ls[i] term_types(ds;da;de;l2[i]))
(i:. i < ||v|| [[v[i]]] e1 s1 a tr = [[l2[i]]] e1 s1 s2 a tr [[ls[i]]] rho)
(list_accum(x,t.x([[t]] e1 s1 a tr);f;v) 
list_accum(x,t.x([[t]] e1 s1 s2 a tr);f;l2))))
17.
l2: Term List
18.
u1: Term
19.
v1: Term List
20.
||v||+1 = ||v1||+1
21.
ls: SimpleType List
22.
u2: SimpleType
23.
v2: SimpleType List
24.
||v2||+1 = ||v||+1
25.
f: [[u2]] rhoreduce(s,m. [[s]] rhom;Prop;v2)
26.
i:(||v||+1). trace_consistent(rho;daa;tr.proj;[u / v][i])
27.
i:(||v1||+1). trace_consistent(rho;daa;tr.proj;[u1 / v1][i])
28.
||v2||+1 = ||v||+1 & (i:. i < ||v||+1 [u2 / v2][i] term_types(ds;da;de;[u / v][i]))
29.
||v2||+1 = ||v1||+1 & (i:. i < ||v1||+1 [u2 / v2][i] term_types(ds;da;de;[u1 / v1][i]))
30.
i:
31.
i < ||v||+1
[[[u1 / v1][i]]] e1 s1 s2 a tr [[[u2 / v2][i]]] rho
By:
ExRepD
THEN
Using [`de',de]
(BackThru
Thm* ds,daa:Collection(dec()), da:Collection(SimpleType), de:sig(), rho:Decl, t:Term, s,s':{[[ds]] rho}, e:{1of([[de]] rho)}, a:SimpleType, v:[[da]] rho, tr:trace_env([[daa]] rho). trace_consistent(rho;daa;tr.proj;t) a term_types(ds;da;de;t) [[t]] e s s' v tr [[a]] rho)
THEN
Try (Reduce 0)
THEN
EasyHyp
Generated subgoals:
None
About:
