---

{ [l:IdLnk]. [p:IdLnk List].
    uiff(lpath([l / p]);lpath(p)
     (destination(l) = source(hd(p)))  ((hd(p) = lnk-inv(l))) 
      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||,  uiff: uiff(P;Q),  uimplies: b supposing a,  uall: [x:A]. B[x],  not: A,  and: P  Q,  cons: [car / cdr],  list: type List,  natural_number: $n,  int: ,  equal: s = t
Definitions :  uall: [x:A]. B[x],  uiff: uiff(P;Q),  lpath: lpath(p),  and: P  Q,  uimplies: b supposing a,  not: A,  member: t  T,  implies: P  Q,  false: False,  prop: ,  top: Top,  all: x:A. B[x],  subtype: S  T,  true: True,  iff: P  Q,  squash: T,  rev_implies: P  Q,  hd: hd(l),  select: l[i],  ifthenelse: if b then t else f fi ,  le_int: i z j,  bnot: b,  lt_int: i <z j,  bfalse: ff,  btrue: tt,  length: ||as||,  ycomb: Y,  le: A  B,  int_seg: {i..j},  sq_type: SQType(T),  guard: {T},  lelt: i  j < k,  decidable: Dec(P),  or: P  Q
Lemmas :  IdLnk_wf,  hd_wf,  length_wf1,  non_neg_length,  length_wf_nat,  top_wf,  lnk-inv_wf,  not_wf,  select_wf,  int_seg_wf,  lpath_wf,  Id_wf,  ldst_wf,  lsrc_wf,  subtype_base_sq,  int_subtype_base,  length_cons,  squash_wf,  true_wf,  select_cons_tl,  decidable__equal_int

---

\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: 2011_08_10-AM-07_46_59
Last ObjectModification: 2011_06_18-AM-08_12_27

Home Index