---

{ [T:Type]
    dT:EqDecider(T). L:T List. x,y:T.
      ((x  L)
       (y  L)
       x before y  L  (x = y) 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],  le: A  B,  all: x:A. B[x],  implies: P  Q,  or: P  Q,  list: type List,  universe: Type,  equal: s = t,  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,  le: A  B,  or: P  Q,  member: t  T,  not: A,  false: False,  prop: ,  guard: {T},  squash: T,  and: P  Q,  true: True,  top: Top,  subtype: S  T,  iff: P  Q,  rev_implies: P  Q,  int_seg: {i..j},  decidable: Dec(P)
Lemmas :  l_index_wf,  int_seg_wf,  length_wf1,  decidable__lt,  l_before_wf,  le_wf,  l_member_wf,  deq_wf,  l_before_l_index,  select_wf,  squash_wf,  non_neg_length,  length_wf_nat,  top_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  \mvee{}  (x  =  y)  supposing  index(L;x)  \mleq{}  index(L;y))


Date html generated: 2011_08_10-AM-07_51_18
Last ObjectModification: 2011_06_18-AM-08_13_59

Home Index