---

Step * of Lemma member-iseg-sorted-by

No Annotations
∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].
  ∀sa,sb:T List.
    (sa ≤ sb
       ⇒ sorted-by(R;sb)
       ⇒ (∀x:T. ((x ∈ sa) ⇐⇒ (¬↑null(sa)) ∧ (x ∈ sb) ∧ ((x = last(sa) ∈ T) ∨ (R x last(sa)))))) supposing 
       (AntiSym(T;x,y.R x y) and 
       Irrefl(T;x,y.R x y))
BY
{ Auto }

1
1. [T] : Type
2. [R] : T ⟶ T ⟶ ℙ
3. sa : T List
4. sb : T List
5. Irrefl(T;x,y.R x y)
6. AntiSym(T;x,y.R x y)
7. sa ≤ sb
8. sorted-by(R;sb)
9. x : T
10. (x ∈ sa)
⊢ (x = last(sa) ∈ T) ∨ (R x last(sa))

2
1. [T] : Type
2. [R] : T ⟶ T ⟶ ℙ
3. sa : T List
4. sb : T List
5. Irrefl(T;x,y.R x y)
6. AntiSym(T;x,y.R x y)
7. sa ≤ sb
8. sorted-by(R;sb)
9. x : T
10. ¬↑null(sa)
11. (x ∈ sb)
12. (x = last(sa) ∈ T) ∨ (R x last(sa))
⊢ (x ∈ sa)

---

Latex:

---

Latex:
No  Annotations
\mforall{}[T:Type].  \mforall{}[R:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].
    \mforall{}sa,sb:T  List.
        (sa  \mleq{}  sb
              {}\mRightarrow{}  sorted-by(R;sb)
              {}\mRightarrow{}  (\mforall{}x:T
                          ((x  \mmember{}  sa)  \mLeftarrow{}{}\mRightarrow{}  (\mneg{}\muparrow{}null(sa))  \mwedge{}  (x  \mmember{}  sb)  \mwedge{}  ((x  =  last(sa))  \mvee{}  (R  x  last(sa))))))  supposing 
              (AntiSym(T;x,y.R  x  y)  and 
              Irrefl(T;x,y.R  x  y))


By

---

Latex:
Auto

---

Home Index