At:
rel mng 2 iff
1
1
2
1
1
2
1
2
1
1
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:. i < ||v||+1 [[[u / v][i]]] e1 s1 a tr = [[[u1 / v1][i]]] e1 s1 s2 a tr [[[u2 / v2][i]]] rho
31.
i:. i < ||v|| [[v[i]]] e1 s1 a tr = [[v1[i]]] e1 s1 s2 a tr [[v2[i]]] rho
32.
i:. i < ||v1|| v2[i] term_types(ds;da;de;v1[i])
33.
i:. i < ||v|| v2[i] term_types(ds;da;de;v[i])
34.
||v2||+1 = ||v1||+1 & (i:. i < ||v1||+1 [u2 / v2][i] term_types(ds;da;de;[u1 / v1][i]))
35.
||v2||+1 = ||v||+1 & (i:. i < ||v||+1 [u2 / v2][i] term_types(ds;da;de;[u / v][i]))
36.
f:reduce(s,m. [[s]] rhom;Prop;v2).
(i:||v||. trace_consistent(rho;daa;tr.proj;v[i]))
(i:||v1||. trace_consistent(rho;daa;tr.proj;v1[i]))
||v2|| = ||v|| & (i:. i < ||v|| v2[i] term_types(ds;da;de;v[i]))
||v2|| = ||v1|| & (i:. i < ||v1|| v2[i] term_types(ds;da;de;v1[i]))
(i:. i < ||v|| [[v[i]]] e1 s1 a tr = [[v1[i]]] e1 s1 s2 a tr [[v2[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;v1))
37.
[[u]] e1 s1 a tr = [[u1]] e1 s1 s2 a tr [[u2]] rho
38.
z: [[u2]] rho
39.
i: ||v||
trace_consistent(rho;daa;tr.proj;v[i])
By:
AllHyps
(h.
(InstHyp [i+1] h) THEN (Subst ([u / v][(i+1)] ~ v[i]) -1)
THEN
(Try
(BackThru
Thm* x:T, l:T List, i:||l||. [x / l][(i+1)] ~ l[i]))
THEN
Trivial)
Generated subgoals:
None
About:
