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