Nuprl Lemma : add-graph-decls_wf
∀[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
Lemmas :
l_member_wf,
Id_wf,
fpf-join_wf,
Knd_wf,
assert_wf,
hasloc_wf,
fpf-const_wf,
graph-rcvs_wf2,
Kind-deq_wf,
subtype_rel-deq,
assert_elim,
subtype_base_sq,
bool_wf,
bool_subtype_base,
equal_wf,
set_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:
2015_07_17-PM-00_00_04
Last ObjectModification:
2015_01_28-AM-00_36_02
Home
Index