At:
rel mng 2 iff
1
1
1
1
1
1
1
2
1.
x: SimpleType
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.
l2: Term List
15.
||l1|| = ||l2|| 
16.
i:||l1||. trace_consistent(rho;daa;tr.proj;l1[i])
17.
i:||l2||. trace_consistent(rho;daa;tr.proj;l2[i])
18.
||l1|| = 2 
19.
x term_types(ds;da;de;l1[0])
20.
x term_types(ds;da;de;l1[1])
21.
||l2|| = 2
22.
x term_types(ds;da;de;l2[0])
23.
x term_types(ds;da;de;l2[1])
24.
i:.
i < ||l1|| 
[[l1[i]]] e1 s1 a tr = [[l2[i]]] e1 s1 s2 a tr [[rel_arg_typ(relname_eq(x);i;de)]] rho
([[l1[0]]] e1 s1 a tr = [[l1[1]]] e1 s1 a tr [[x]] rho) Prop
By:
Auto
THEN
BackThru
Thm* ds,da:Collection(dec()), st1:Collection(SimpleType), de:sig(), rho:Decl, t:Term, s:{[[ds]] rho}, e:{1of([[de]] rho)}, a:SimpleType, v:[[st1]] rho, tr:trace_env([[da]] rho). trace_consistent(rho;da;tr.proj;t) a term_types(ds;st1;de;t) [[t]] e s v tr [[a]] rho
THEN
EasyHyp
Generated subgoals:
None
About:
