---

Step * 1 of Lemma decidable__llex-le


1. [A] : Type
2. [<] : A ⟶ A ⟶ ℙ
3. ∀a,b:A.  (Dec(<[a;b]) ∧ Dec(a = b ∈ A))
4. L1 : A List
5. L2 : A List
6. Dec(L1 llex(A;a,b.<[a;b]) L2)
⊢ Dec(L1 llex-le(A;a,b.<[a;b]) L2)
BY
{ (RepUR ``llex-le`` 0 THEN D -1 THEN Auto) }

---

Latex:

---

Latex:

1.  [A]  :  Type
2.  [<]  :  A  {}\mrightarrow{}  A  {}\mrightarrow{}  \mBbbP{}
3.  \mforall{}a,b:A.    (Dec(<[a;b])  \mwedge{}  Dec(a  =  b))
4.  L1  :  A  List
5.  L2  :  A  List
6.  Dec(L1  llex(A;a,b.<[a;b])  L2)
\mvdash{}  Dec(L1  llex-le(A;a,b.<[a;b])  L2)


By

---

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

---

Home Index