---

Step * 1 2 1 1 1 1 1 2 of Lemma wellfounded-llex


1. [A] : Type
2. [<] : A ⟶ A ⟶ ℙ
3. ∀a,b:A.  SqStable(<[a;b])
4. ∀[P:A ⟶ ℙ]. ((∀j:A. ((∀k:A. (<[k;j] ⇒ P[k])) ⇒ P[j])) ⇒ (∀n:A. P[n]))
5. [P] : Des(A;a,b.<[a;b]) ⟶ ℙ
6. ∀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])
7. ∀[a:A]. ∀[m,k:Des(A;a,b.<[a;b])].  (descending(a,b.<[a;b];m @ [a / k]) ∈ ℙ)
8. ∀[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)
9. j : A
10. ∀k:A
      (<[k;j]
      ⇒ (∀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@0:{k@0:Des(A;a,b.<[a;b])| descending(a,b.<[a;b];m @ [k / k@0])} . P[m @ [k / k@0]]))))
11. m : Des(A;a,b.<[a;b])
12. ∀L:Des(A;a,b.<[a;b]). ((L llex(A;a,b.<[a;b]) m) ⇒ P[L])
13. k : {k:Des(A;a,b.<[a;b])| descending(a,b.<[a;b];m @ [j / k])} 
14. P[m]
15. l : Des(A;a,b.<[a;b])
16. l llex(A;a,b.<[a;b]) (m @ [j])
17. (l llex(A;a,b.<[a;b]) m) ∨ (∃k:Des(A;a,b.<[a;b]). ((l = (m @ k) ∈ (A List)) ∧ (0 < ||k|| ⇒ <[hd(k);j])))
⊢ P[l]
BY
{ D (-1) }

1
1. [A] : Type
2. [<] : A ⟶ A ⟶ ℙ
3. ∀a,b:A.  SqStable(<[a;b])
4. ∀[P:A ⟶ ℙ]. ((∀j:A. ((∀k:A. (<[k;j] ⇒ P[k])) ⇒ P[j])) ⇒ (∀n:A. P[n]))
5. [P] : Des(A;a,b.<[a;b]) ⟶ ℙ
6. ∀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])
7. ∀[a:A]. ∀[m,k:Des(A;a,b.<[a;b])].  (descending(a,b.<[a;b];m @ [a / k]) ∈ ℙ)
8. ∀[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)
9. j : A
10. ∀k:A
      (<[k;j]
      ⇒ (∀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@0:{k@0:Des(A;a,b.<[a;b])| descending(a,b.<[a;b];m @ [k / k@0])} . P[m @ [k / k@0]]))))
11. m : Des(A;a,b.<[a;b])
12. ∀L:Des(A;a,b.<[a;b]). ((L llex(A;a,b.<[a;b]) m) ⇒ P[L])
13. k : {k:Des(A;a,b.<[a;b])| descending(a,b.<[a;b];m @ [j / k])} 
14. P[m]
15. l : Des(A;a,b.<[a;b])
16. l llex(A;a,b.<[a;b]) (m @ [j])
17. l llex(A;a,b.<[a;b]) m
⊢ P[l]

2
1. [A] : Type
2. [<] : A ⟶ A ⟶ ℙ
3. ∀a,b:A.  SqStable(<[a;b])
4. ∀[P:A ⟶ ℙ]. ((∀j:A. ((∀k:A. (<[k;j] ⇒ P[k])) ⇒ P[j])) ⇒ (∀n:A. P[n]))
5. [P] : Des(A;a,b.<[a;b]) ⟶ ℙ
6. ∀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])
7. ∀[a:A]. ∀[m,k:Des(A;a,b.<[a;b])].  (descending(a,b.<[a;b];m @ [a / k]) ∈ ℙ)
8. ∀[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)
9. j : A
10. ∀k:A
      (<[k;j]
      ⇒ (∀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@0:{k@0:Des(A;a,b.<[a;b])| descending(a,b.<[a;b];m @ [k / k@0])} . P[m @ [k / k@0]]))))
11. m : Des(A;a,b.<[a;b])
12. ∀L:Des(A;a,b.<[a;b]). ((L llex(A;a,b.<[a;b]) m) ⇒ P[L])
13. k : {k:Des(A;a,b.<[a;b])| descending(a,b.<[a;b];m @ [j / k])} 
14. P[m]
15. l : Des(A;a,b.<[a;b])
16. l llex(A;a,b.<[a;b]) (m @ [j])
17. ∃k:Des(A;a,b.<[a;b]). ((l = (m @ k) ∈ (A List)) ∧ (0 < ||k|| ⇒ <[hd(k);j]))
⊢ P[l]

---

Latex:

---

Latex:

1.  [A]  :  Type
2.  [<]  :  A  {}\mrightarrow{}  A  {}\mrightarrow{}  \mBbbP{}
3.  \mforall{}a,b:A.    SqStable(<[a;b])
4.  \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]))
5.  [P]  :  Des(A;a,b.<[a;b])  {}\mrightarrow{}  \mBbbP{}
6.  \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])
7.  \mforall{}[a:A].  \mforall{}[m,k:Des(A;a,b.<[a;b])].    (descending(a,b.<[a;b];m  @  [a  /  k])  \mmember{}  \mBbbP{})
8.  \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)
9.  j  :  A
10.  \mforall{}k:A
            (<[k;j]
            {}\mRightarrow{}  (\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@0:\{k@0:Des(A;a,b.<[a;b])|  descending(a,b.<[a;b];m  @  [k  /  k@0])\} 
                                    P[m  @  [k  /  k@0]]))))
11.  m  :  Des(A;a,b.<[a;b])
12.  \mforall{}L:Des(A;a,b.<[a;b]).  ((L  llex(A;a,b.<[a;b])  m)  {}\mRightarrow{}  P[L])
13.  k  :  \{k:Des(A;a,b.<[a;b])|  descending(a,b.<[a;b];m  @  [j  /  k])\} 
14.  P[m]
15.  l  :  Des(A;a,b.<[a;b])
16.  l  llex(A;a,b.<[a;b])  (m  @  [j])
17.  (l  llex(A;a,b.<[a;b])  m)  \mvee{}  (\mexists{}k:Des(A;a,b.<[a;b]).  ((l  =  (m  @  k))  \mwedge{}  (0  <  ||k||  {}\mRightarrow{}  <[hd(k);j])))
\mvdash{}  P[l]


By

---

Latex:
D  (-1)

---

Home Index