---

Step * of Lemma llex-irreflexive

∀[A:Type]. ∀[<:A ⟶ A ⟶ ℙ].  ((∀a:A. (¬<[a;a])) ⇒ (∀[L:A List]. (¬(L llex(A;a,b.<[a;b]) L))))
BY
{ (RepUR ``llex`` 0 THEN Auto THEN (D 0 THENM D -1) THEN Auto) }

1
1. A : Type
2. < : A ⟶ A ⟶ ℙ
3. ∀a:A. (¬<[a;a])@i
4. L : A List
5. ∃i:ℕ. (i < ||L|| ∧ i < ||L|| ∧ (∀j:ℕi. (L[j] = L[j] ∈ A)) ∧ <[L[i];L[i]])@i
⊢ False

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}[<:A  {}\mrightarrow{}  A  {}\mrightarrow{}  \mBbbP{}].    ((\mforall{}a:A.  (\mneg{}<[a;a]))  {}\mRightarrow{}  (\mforall{}[L:A  List].  (\mneg{}(L  llex(A;a,b.<[a;b])  L))))


By

---

Latex:
(RepUR  ``llex``  0  THEN  Auto  THEN  (D  0  THENM  D  -1)  THEN  Auto)

---

Home Index