Nuprl Lemma : lg-remove_wf_dag
∀[T:Type]. ∀[g:LabeledDAG(T)]. ∀[x:ℕ]. (lg-remove(g;x) ∈ LabeledDAG(T))
Proof
Definitions occuring in Statement :
ldag: LabeledDAG(T),
lg-remove: lg-remove(g;n),
nat: ℕ,
uall: ∀[x:A]. B[x],
member: t ∈ T,
universe: Type
Lemmas :
decidable__lt,
lg-size_wf,
nat_wf,
is-dag_wf,
ldag_wf,
lelt_wf,
is-dag-remove,
lg-remove-noop,
labeled-graph_wf,
true_wf,
squash_wf
Latex:
\mforall{}[T:Type]. \mforall{}[g:LabeledDAG(T)]. \mforall{}[x:\mBbbN{}]. (lg-remove(g;x) \mmember{} LabeledDAG(T))
Date html generated:
2015_07_23-AM-11_03_15
Last ObjectModification:
2015_07_16-AM-09_38_58
Home
Index