Nuprl Lemma : lconnects_wf
∀[p:IdLnk List]. ∀[i,j:Id]. (lconnects(p;i;j) ∈ ℙ)
Proof
Definitions occuring in Statement :
lconnects: lconnects(p;i;j),
IdLnk: IdLnk,
Id: Id,
list: T List,
uall: ∀[x:A]. B[x],
prop: ℙ,
member: t ∈ T
Lemmas :
lpath_wf,
equal-wf-T-base,
length_wf,
IdLnk_wf,
Id_wf,
not_wf,
lsrc_wf,
hd_wf,
non_neg_length,
length_wf_nat,
ldst_wf,
last_wf,
list-cases,
null_nil_lemma,
length_of_nil_lemma,
product_subtype_list,
null_cons_lemma,
false_wf,
list_wf
\mforall{}[p:IdLnk List]. \mforall{}[i,j:Id]. (lconnects(p;i;j) \mmember{} \mBbbP{})
Date html generated:
2015_07_17-AM-09_12_35
Last ObjectModification:
2015_01_28-AM-07_56_20
Home
Index