---

Step * of Lemma decidable__llex

∀[A:Type]. ∀[<:A ⟶ A ⟶ ℙ].
  ((∀a,b:A.  (Dec(<[a;b]) ∧ Dec(a = b ∈ A))) ⇒ (∀L1,L2:A List.  Dec(L1 llex(A;a,b.<[a;b]) L2)))
BY
{ (Auto THEN RepUR ``llex`` 0 THEN BLemma `decidable__or` THEN Try (Complete (Auto))) }

1
1. [A] : Type
2. [<] : A ⟶ A ⟶ ℙ
3. ∀a,b:A.  (Dec(<[a;b]) ∧ Dec(a = b ∈ A))@i
4. L1 : A List@i
5. L2 : A List@i
⊢ Dec(||L1|| < ||L2|| ∧ (∀i:ℕ||L1||. (L1[i] = L2[i] ∈ A)))

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

---

Latex:

---

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


By

---

Latex:
(Auto  THEN  RepUR  ``llex``  0  THEN  BLemma  `decidable\_\_or`  THEN  Try  (Complete  (Auto)))

---

Home Index