{ 
[dd:DeclSet]. [G:Graph(|dd|)]. [T:Type]. [a:Id 
Id Id]. [b:Id].
(add-graph-decls(dd;G;T;a;b) 
DeclSet) }
{ Proof }
Definitions occuring in Statement :
add-graph-decls: add-graph-decls(dd;G;T;a;b),
es-decl-set-domain: |dd|,
es-decl-set: DeclSet,
id-graph: Graph(S),
Id: Id,
uall: [x:A]. B[x],
member: t T,
function: x:A B[x],
universe: Type
Definitions :
uall: [x:A]. B[x],
es-decl-set: DeclSet,
es-decl-set-domain: |dd|,
member: t T,
add-graph-decls: add-graph-decls(dd;G;T;a;b),
pi1: fst(t),
spreadn: spread3,
all: x:A. B[x],
prop: 
,
so_lambda: 
x.t[x],
so_apply: x[s],
uimplies: b supposing a
Lemmas :
l_member_wf,
fpf-join_wf,
Knd_wf,
assert_wf,
hasloc_wf,
fpf-const_wf,
graph-rcvs_wf2,
strong-subtype-deq-subtype,
strong-subtype-set3,
strong-subtype-self,
Id_wf,
fpf_wf,
id-graph_wf,
es-decl-set-domain_wf,
es-decl-set_wf
\mforall{}[dd:DeclSet]. \mforall{}[G:Graph(|dd|)]. \mforall{}[T:Type]. \mforall{}[a:Id {}\mrightarrow{} Id {}\mrightarrow{} Id]. \mforall{}[b:Id].
(add-graph-decls(dd;G;T;a;b) \mmember{} DeclSet)
Date html generated:
2011_08_16-AM-11_02_22
Last ObjectModification:
2011_06_18-AM-09_35_49
Home
Index