---

{ [T:Type]
    dT:EqDecider(T). L:T List. x,y:T.
      ((x  L)  (y  L)  x before y  L supposing index(L;x) < index(L;y)) }

{ Proof }

---

Definitions occuring in Statement :  l_index: index(L;x),  uimplies: b supposing a,  uall: [x:A]. B[x],  all: x:A. B[x],  implies: P  Q,  less_than: a < b,  list: type List,  universe: Type,  l_before: x before y  l,  l_member: (x  l),  deq: EqDecider(T)
Definitions :  uall: [x:A]. B[x],  all: x:A. B[x],  implies: P  Q,  uimplies: b supposing a,  member: t  T,  prop: ,  squash: T,  true: True,  rev_implies: P  Q,  iff: P  Q,  and: P  Q,  int_seg: {i..j}
Lemmas :  l_index_wf,  int_seg_wf,  length_wf1,  l_member_wf,  deq_wf,  l_before_select,  l_before_wf,  squash_wf,  true_wf,  select_l_index

---

\mforall{}[T:Type]
    \mforall{}dT:EqDecider(T).  \mforall{}L:T  List.  \mforall{}x,y:T.
        ((x  \mmember{}  L)  {}\mRightarrow{}  (y  \mmember{}  L)  {}\mRightarrow{}  x  before  y  \mmember{}  L  supposing  index(L;x)  <  index(L;y))


Date html generated: 2011_08_10-AM-07_51_14
Last ObjectModification: 2011_06_18-AM-08_13_57

Home Index