---

Step * of Lemma llex-append1

No Annotations
∀[A:Type]. ∀[<:A ⟶ A ⟶ ℙ].
  ∀L1,L2:A List. ∀a:A.
    ((L1 llex(A;a,b.<[a;b]) (L2 @ [a]))
    ⇒ ((L1 llex(A;a,b.<[a;b]) L2) ∨ (∃L3:A List. ((L1 = (L2 @ L3) ∈ (A List)) ∧ <[hd(L3);a] supposing 0 < ||L3||))))
BY
{ (Auto THEN RepUR ``llex`` (-1)⋅ THEN D -1) }

1
1. [A] : Type
2. [<] : A ⟶ A ⟶ ℙ
3. L1 : A List
4. L2 : A List
5. a : A
6. ||L1|| < ||L2 @ [a]|| ∧ (∀i:ℕ||L1||. (L1[i] = L2 @ [a][i] ∈ A))
⊢ (L1 llex(A;a,b.<[a;b]) L2) ∨ (∃L3:A List. ((L1 = (L2 @ L3) ∈ (A List)) ∧ <[hd(L3);a] supposing 0 < ||L3||))

2
1. [A] : Type
2. [<] : A ⟶ A ⟶ ℙ
3. L1 : A List
4. L2 : A List
5. a : A
6. ∃i:ℕ. (i < ||L1|| ∧ i < ||L2 @ [a]|| ∧ (∀j:ℕi. (L1[j] = L2 @ [a][j] ∈ A)) ∧ <[L1[i];L2 @ [a][i]])
⊢ (L1 llex(A;a,b.<[a;b]) L2) ∨ (∃L3:A List. ((L1 = (L2 @ L3) ∈ (A List)) ∧ <[hd(L3);a] supposing 0 < ||L3||))

---

Latex:

---

Latex:
No  Annotations
\mforall{}[A:Type].  \mforall{}[<:A  {}\mrightarrow{}  A  {}\mrightarrow{}  \mBbbP{}].
    \mforall{}L1,L2:A  List.  \mforall{}a:A.
        ((L1  llex(A;a,b.<[a;b])  (L2  @  [a]))
        {}\mRightarrow{}  ((L1  llex(A;a,b.<[a;b])  L2)
              \mvee{}  (\mexists{}L3:A  List.  ((L1  =  (L2  @  L3))  \mwedge{}  <[hd(L3);a]  supposing  0  <  ||L3||))))


By

---

Latex:
(Auto  THEN  RepUR  ``llex``  (-1)\mcdot{}  THEN  D  -1)

---

Home Index