---

Step * 1 3 1 2 of Lemma wellfounded-llex


1. [A] : Type
2. [<] : A ⟶ A ⟶ ℙ
3. ∀[P:A ⟶ ℙ]. ((∀j:A. ((∀k:A. (<[k;j] ⇒ P[k])) ⇒ P[j])) ⇒ (∀n:A. P[n]))
4. [P] : Des(A;a,b.<[a;b]) ⟶ ℙ
5. ∀j:Des(A;a,b.<[a;b]). ((∀k:Des(A;a,b.<[a;b]). ((k llex(A;a,b.<[a;b]) j) ⇒ P[k])) ⇒ P[j])
6. ∀[a:A]. ∀[m,k:Des(A;a,b.<[a;b])].  (descending(a,b.<[a;b];m @ [a / k]) ∈ ℙ)
7. ∀[a:A]. ∀[m:Des(A;a,b.<[a;b])].  ({k:Des(A;a,b.<[a;b])| descending(a,b.<[a;b];m @ [a / k])}  ∈ Type)
8. [%8] : descending(a,b.<[a;b];[])
9. ∀n:A. ∀m:Des(A;a,b.<[a;b]).
     ((∀L:Des(A;a,b.<[a;b]). ((L llex(A;a,b.<[a;b]) m) ⇒ P[L]))
     ⇒ (∀k:{k:Des(A;a,b.<[a;b])| descending(a,b.<[a;b];m @ [n / k])} . P[m @ [n / k]]))
⊢ ∀k:Des(A;a,b.<[a;b]). ((k llex(A;a,b.<[a;b]) []) ⇒ P[k])
BY
{ (RepeatFor 2 ((D 0 THENA Auto)) THEN RepUR ``llex`` -1 THEN D -1) }

1
1. [A] : Type
2. [<] : A ⟶ A ⟶ ℙ
3. ∀[P:A ⟶ ℙ]. ((∀j:A. ((∀k:A. (<[k;j] ⇒ P[k])) ⇒ P[j])) ⇒ (∀n:A. P[n]))
4. [P] : Des(A;a,b.<[a;b]) ⟶ ℙ
5. ∀j:Des(A;a,b.<[a;b]). ((∀k:Des(A;a,b.<[a;b]). ((k llex(A;a,b.<[a;b]) j) ⇒ P[k])) ⇒ P[j])
6. ∀[a:A]. ∀[m,k:Des(A;a,b.<[a;b])].  (descending(a,b.<[a;b];m @ [a / k]) ∈ ℙ)
7. ∀[a:A]. ∀[m:Des(A;a,b.<[a;b])].  ({k:Des(A;a,b.<[a;b])| descending(a,b.<[a;b];m @ [a / k])}  ∈ Type)
8. [%8] : descending(a,b.<[a;b];[])
9. ∀n:A. ∀m:Des(A;a,b.<[a;b]).
     ((∀L:Des(A;a,b.<[a;b]). ((L llex(A;a,b.<[a;b]) m) ⇒ P[L]))
     ⇒ (∀k:{k:Des(A;a,b.<[a;b])| descending(a,b.<[a;b];m @ [n / k])} . P[m @ [n / k]]))
10. k : Des(A;a,b.<[a;b])
11. ||k|| < 0 ∧ (∀i:ℕ||k||. (k[i] = ⊥ ∈ A))
⊢ P[k]

2
1. [A] : Type
2. [<] : A ⟶ A ⟶ ℙ
3. ∀[P:A ⟶ ℙ]. ((∀j:A. ((∀k:A. (<[k;j] ⇒ P[k])) ⇒ P[j])) ⇒ (∀n:A. P[n]))
4. [P] : Des(A;a,b.<[a;b]) ⟶ ℙ
5. ∀j:Des(A;a,b.<[a;b]). ((∀k:Des(A;a,b.<[a;b]). ((k llex(A;a,b.<[a;b]) j) ⇒ P[k])) ⇒ P[j])
6. ∀[a:A]. ∀[m,k:Des(A;a,b.<[a;b])].  (descending(a,b.<[a;b];m @ [a / k]) ∈ ℙ)
7. ∀[a:A]. ∀[m:Des(A;a,b.<[a;b])].  ({k:Des(A;a,b.<[a;b])| descending(a,b.<[a;b];m @ [a / k])}  ∈ Type)
8. [%8] : descending(a,b.<[a;b];[])
9. ∀n:A. ∀m:Des(A;a,b.<[a;b]).
     ((∀L:Des(A;a,b.<[a;b]). ((L llex(A;a,b.<[a;b]) m) ⇒ P[L]))
     ⇒ (∀k:{k:Des(A;a,b.<[a;b])| descending(a,b.<[a;b];m @ [n / k])} . P[m @ [n / k]]))
10. k : Des(A;a,b.<[a;b])
11. ∃i:ℕ. (i < ||k|| ∧ i < 0 ∧ (∀j:ℕi. (k[j] = ⊥ ∈ A)) ∧ <[k[i];⊥])
⊢ P[k]

---

Latex:

---

Latex:

1.  [A]  :  Type
2.  [<]  :  A  {}\mrightarrow{}  A  {}\mrightarrow{}  \mBbbP{}
3.  \mforall{}[P:A  {}\mrightarrow{}  \mBbbP{}].  ((\mforall{}j:A.  ((\mforall{}k:A.  (<[k;j]  {}\mRightarrow{}  P[k]))  {}\mRightarrow{}  P[j]))  {}\mRightarrow{}  (\mforall{}n:A.  P[n]))
4.  [P]  :  Des(A;a,b.<[a;b])  {}\mrightarrow{}  \mBbbP{}
5.  \mforall{}j:Des(A;a,b.<[a;b]).  ((\mforall{}k:Des(A;a,b.<[a;b]).  ((k  llex(A;a,b.<[a;b])  j)  {}\mRightarrow{}  P[k]))  {}\mRightarrow{}  P[j])
6.  \mforall{}[a:A].  \mforall{}[m,k:Des(A;a,b.<[a;b])].    (descending(a,b.<[a;b];m  @  [a  /  k])  \mmember{}  \mBbbP{})
7.  \mforall{}[a:A].  \mforall{}[m:Des(A;a,b.<[a;b])].
          (\{k:Des(A;a,b.<[a;b])|  descending(a,b.<[a;b];m  @  [a  /  k])\}    \mmember{}  Type)
8.  [\%8]  :  descending(a,b.<[a;b];[])
9.  \mforall{}n:A.  \mforall{}m:Des(A;a,b.<[a;b]).
          ((\mforall{}L:Des(A;a,b.<[a;b]).  ((L  llex(A;a,b.<[a;b])  m)  {}\mRightarrow{}  P[L]))
          {}\mRightarrow{}  (\mforall{}k:\{k:Des(A;a,b.<[a;b])|  descending(a,b.<[a;b];m  @  [n  /  k])\}  .  P[m  @  [n  /  k]]))
\mvdash{}  \mforall{}k:Des(A;a,b.<[a;b]).  ((k  llex(A;a,b.<[a;b])  [])  {}\mRightarrow{}  P[k])


By

---

Latex:
(RepeatFor  2  ((D  0  THENA  Auto))  THEN  RepUR  ``llex``  -1  THEN  D  -1)

---

Home Index