Nuprl Lemma : lpath_cons
∀[l:IdLnk]. ∀[p:IdLnk List].
uiff(lpath([l / p]);lpath(p)
∧ (destination(l) = source(hd(p)) ∈ Id) ∧ (¬(hd(p) = lnk-inv(l) ∈ IdLnk)) supposing ¬(||p|| = 0 ∈ ℤ))
Proof
Definitions occuring in Statement :
lpath: lpath(p),
ldst: destination(l),
lsrc: source(l),
lnk-inv: lnk-inv(l),
IdLnk: IdLnk,
Id: Id,
hd: hd(l),
length: ||as||,
cons: [a / b],
list: T List,
uiff: uiff(P;Q),
uimplies: b supposing a,
uall: ∀[x:A]. B[x],
not: ¬A,
and: P ∧ Q,
natural_number: $n,
int: ℤ,
equal: s = t ∈ T
Lemmas :
equal_wf,
IdLnk_wf,
hd_wf,
length_wf,
non_neg_length,
length_wf_nat,
lnk-inv_wf,
not_wf,
equal-wf-T-base,
select_wf,
int_seg_wf,
subtract_wf,
lpath_wf,
cons_wf,
Id_wf,
ldst_wf,
lsrc_wf,
list_wf,
trivial-int-eq1,
length_of_cons_lemma,
squash_wf,
true_wf,
select_cons_tl,
iff_weakening_equal,
select0,
list-cases,
product_subtype_list,
length_of_nil_lemma,
less_than_transitivity1,
less_than_irreflexivity,
length_cons,
reduce_hd_cons_lemma,
general_arith_equation1,
decidable__equal_int,
subtype_base_sq,
int_subtype_base
\mforall{}[l:IdLnk]. \mforall{}[p:IdLnk List].
uiff(lpath([l / p]);lpath(p)
\mwedge{} (destination(l) = source(hd(p))) \mwedge{} (\mneg{}(hd(p) = lnk-inv(l))) supposing \mneg{}(||p|| = 0))
Date html generated:
2015_07_17-AM-09_12_33
Last ObjectModification:
2015_02_04-PM-05_07_59
Home
Index