At:
closed rel mng 2
1
2
2
2
1
1
1
2
1
1.
r: rel()
2.
rho: Decl
3.
ds: Collection(dec())
4.
daa: Collection(dec())
5.
da1: Collection(SimpleType)
6.
da2: Collection(SimpleType)
7.
de: sig()
8.
s: {[[ds]] rho}
9.
e: {[[de]] rho}
10.
a1: Top
11.
a2: Top
12.
tr: trace_env([[daa]] rho)
13.
trace_consistent_rel(rho;daa;tr.proj;r)
14.
tc(r;ds;da1;de)
15.
tc(r;ds; < > ;de) & a1 
[[ < > ]] rho & a2 [[ < > ]] rho
16.
aa: Term List
17.
u: Term
18.
v: Term List
19.
xx:Top.
reduce(
t,vs. term_free_vars(t) @ vs;nil;v) = nil
(list_accum(x,t.x([[t]] 1of(e) s a2 tr);xx;v) ~ list_accum(x,t.x([[t]] 1of(e) s a1 tr);xx;v))
20.
xx: Top
21.
(term_free_vars(u) @ reduce(t,vs. term_free_vars(t) @ vs;nil;v)) = nil
reduce(t,vs. term_free_vars(t) @ vs;nil;v) = nil
By:
Inst
Thm* l1,l2:T List. (l1 @ l2) = nil 
l1 = nil & l2 = nil
[Label;term_free_vars(u);reduce(t,vs. term_free_vars(t) @ vs;nil;v)]
THEN
ThinTrivial
Generated subgoals:
None
About:
