---

Step * 1 1 of Lemma wellfounded-llex

.....wf..... 
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. n : Des(A;a,b.<[a;b])
⊢ λ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 @ [a / k])} . P[m @ [a / k]])) ∈ A ⟶ ℙ
BY
{ TACTIC:(RepeatFor 4 ((At ⌜Type⌝ (MemCD)⋅ THEN Try (Complete ((Auto THEN BackThruSomeHyp)))))⋅
          THEN D (-1)
          THEN Auto
          THEN MemTypeCD
          THEN Auto)⋅ }

---

Latex:

---

Latex:
.....wf..... 
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.  n  :  Des(A;a,b.<[a;b])
\mvdash{}  \mlambda{}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  @  [a  /  k])\}  .  P[m  @  [a  /  k]]))  \mmember{}  A  {}\mrightarrow{}  \mBbbP{}


By

---

Latex:
TACTIC:(RepeatFor  4  ((At  \mkleeneopen{}Type\mkleeneclose{}  (MemCD)\mcdot{}  THEN  Try  (Complete  ((Auto  THEN  BackThruSomeHyp)))))\mcdot{}
                THEN  D  (-1)
                THEN  Auto
                THEN  MemTypeCD
                THEN  Auto)\mcdot{}

---

Home Index