---

Step * of Lemma sq_stable__sorted-by

∀[T:Type]
  ∀L:T List
    ∀[R:{x:T| (x ∈ L)}  ⟶ {x:T| (x ∈ L)}  ⟶ ℙ]. ((∀x,y:{x:T| (x ∈ L)} .  SqStable(R x y)) ⇒ SqStable(sorted-by(R;L)))
BY
{ (xxxAutoxxx THEN (GenConcl ⌜L = Z ∈ ({x:T| (x ∈ L)}  List)⌝⋅ THENA Auto)) }

1
1. [T] : Type
2. L : T List
3. [R] : {x:T| (x ∈ L)}  ⟶ {x:T| (x ∈ L)}  ⟶ ℙ
4. ∀x,y:{x:T| (x ∈ L)} .  SqStable(R x y)
5. Z : {x:T| (x ∈ L)}  List
6. L = Z ∈ ({x:T| (x ∈ L)}  List)
⊢ SqStable(sorted-by(R;Z))

---

Latex:

---

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


By

---

Latex:
(xxxAutoxxx  THEN  (GenConcl  \mkleeneopen{}L  =  Z\mkleeneclose{}\mcdot{}  THENA  Auto))

---

Home Index