Nuprl Lemma : add-graph-decls-declares-tag
∀dd:DeclSet. ∀G:Graph(|dd|). ∀T:Type. ∀a:Id ─→ Id ─→ Id. ∀b:Id.
(es-decl-set-declares-tag{i:l}(dd;b;T) ⇒ es-decl-set-declares-tag{i:l}(add-graph-decls(dd;G;T;a;b);b;T))
Proof
Definitions occuring in Statement :
add-graph-decls: add-graph-decls(dd;G;T;a;b),
es-decl-set-declares-tag: es-decl-set-declares-tag{i:l}(dd;b;T),
es-decl-set-domain: |dd|,
es-decl-set: DeclSet,
id-graph: Graph(S),
Id: Id,
all: ∀x:A. B[x],
implies: P ⇒ Q,
function: x:A ─→ B[x],
universe: Type
Lemmas :
fpf-join-ap-sq,
Knd_wf,
Kind-deq_wf,
fpf-const_wf,
top_wf,
graph-rcvs_wf,
l_member_wf,
Id_wf,
equal_wf,
tagof_wf,
assert_wf,
isrcv_wf,
fpf-domain_wf,
fpf-join_wf,
subtype-fpf3,
hasloc_wf,
strong-subtype-set2,
subtype_top,
set_wf,
fpf-const-dom,
fpf-dom_wf,
bool_wf,
eqtt_to_assert,
iff_wf,
true_wf,
eqff_to_assert,
bool_cases_sqequal,
subtype_base_sq,
bool_subtype_base,
assert-bnot,
fpf-domain-join
\mforall{}dd:DeclSet. \mforall{}G:Graph(|dd|). \mforall{}T:Type. \mforall{}a:Id {}\mrightarrow{} Id {}\mrightarrow{} Id. \mforall{}b:Id.
(es-decl-set-declares-tag\{i:l\}(dd;b;T)
{}\mRightarrow{} es-decl-set-declares-tag\{i:l\}(add-graph-decls(dd;G;T;a;b);b;T))
Date html generated:
2015_07_17-PM-00_00_11
Last ObjectModification:
2015_02_04-PM-05_40_23
Home
Index