---

Step * of Lemma l_before-sorted-by

∀[T:Type]
  ∀L:T List. ∀[R:{x:T| (x ∈ L)}  ⟶ {x:T| (x ∈ L)}  ⟶ ℙ]. (sorted-by(R;L) ⇒ (∀x,y:T.  (x before y ∈ L ⇒ (R x y))))
BY
{ (Auto
   THEN (D (-1))
   THEN Auto
   THEN All Reduce
   THEN ((InstHyp [⌜0⌝] (-1))⋅ THENA Auto)
   THEN (Reduce (-1))
   THEN ((InstHyp [⌜1⌝] (-2))⋅ THENA Auto)
   THEN (Reduce (-1))
   THEN skip{((InstLemma `list-subtype` [⌜T⌝; ⌜L⌝])⋅ THEN Auto)}) }

1
1. [T] : Type
2. L : T List
3. [R] : {x:T| (x ∈ L)}  ⟶ {x:T| (x ∈ L)}  ⟶ ℙ
4. sorted-by(R;L)
5. x : T
6. y : T
7. f : ℕ2 ⟶ ℕ||L||
8. increasing(f;2)
9. ∀j:ℕ2. ([x; y][j] = L[f j] ∈ T)
10. x = L[f 0] ∈ T
11. y = L[f 1] ∈ T
⊢ R x y

---

Latex:

---

Latex:
\mforall{}[T:Type]
    \mforall{}L:T  List
        \mforall{}[R:\{x:T|  (x  \mmember{}  L)\}    {}\mrightarrow{}  \{x:T|  (x  \mmember{}  L)\}    {}\mrightarrow{}  \mBbbP{}]
            (sorted-by(R;L)  {}\mRightarrow{}  (\mforall{}x,y:T.    (x  before  y  \mmember{}  L  {}\mRightarrow{}  (R  x  y))))


By

---

Latex:
(Auto
  THEN  (D  (-1))
  THEN  Auto
  THEN  All  Reduce
  THEN  ((InstHyp  [\mkleeneopen{}0\mkleeneclose{}]  (-1))\mcdot{}  THENA  Auto)
  THEN  (Reduce  (-1))
  THEN  ((InstHyp  [\mkleeneopen{}1\mkleeneclose{}]  (-2))\mcdot{}  THENA  Auto)
  THEN  (Reduce  (-1))
  THEN  skip\{((InstLemma  `list-subtype`  [\mkleeneopen{}T\mkleeneclose{};  \mkleeneopen{}L\mkleeneclose{}])\mcdot{}  THEN  Auto)\})

---

Home Index