---

Step * of Lemma llex-linear

∀[A:Type]. ∀[<:A ⟶ A ⟶ ℙ].
  ((∀a,b:A.  (<[a;b] ∨ (a = b ∈ A) ∨ <[b;a]))
  ⇒ (∀L1,L2:A List.  ((L1 llex(A;a,b.<[a;b]) L2) ∨ (L1 = L2 ∈ (A List)) ∨ (L2 llex(A;a,b.<[a;b]) L1))))
BY
{ xxxInductionOnListxxx }

1
1. [A] : Type
2. [<] : A ⟶ A ⟶ ℙ
3. ∀a,b:A.  (<[a;b] ∨ (a = b ∈ A) ∨ <[b;a])
⊢ ∀L2:A List. (([] llex(A;a,b.<[a;b]) L2) ∨ ([] = L2 ∈ (A List)) ∨ (L2 llex(A;a,b.<[a;b]) []))

2
1. [A] : Type
2. [<] : A ⟶ A ⟶ ℙ
3. ∀a,b:A.  (<[a;b] ∨ (a = b ∈ A) ∨ <[b;a])
4. u : A
5. v : A List
6. ∀L2:A List. ((v llex(A;a,b.<[a;b]) L2) ∨ (v = L2 ∈ (A List)) ∨ (L2 llex(A;a,b.<[a;b]) v))
⊢ ∀L2:A List. (([u / v] llex(A;a,b.<[a;b]) L2) ∨ ([u / v] = L2 ∈ (A List)) ∨ (L2 llex(A;a,b.<[a;b]) [u / v]))

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}[<:A  {}\mrightarrow{}  A  {}\mrightarrow{}  \mBbbP{}].
    ((\mforall{}a,b:A.    (<[a;b]  \mvee{}  (a  =  b)  \mvee{}  <[b;a]))
    {}\mRightarrow{}  (\mforall{}L1,L2:A  List.    ((L1  llex(A;a,b.<[a;b])  L2)  \mvee{}  (L1  =  L2)  \mvee{}  (L2  llex(A;a,b.<[a;b])  L1))))


By

---

Latex:
xxxInductionOnListxxx

---

Home Index