---

Step * of Lemma wellfounded-llex

∀[A:Type]. ∀[<:A ⟶ A ⟶ ℙ].
  ((∀a,b:A.  SqStable(<[a;b]))
  ⇒ WellFnd{i}(A;a,b.<[a;b])
  ⇒ WellFnd{i}(Des(A;a,b.<[a;b]);L1,L2.L1 llex(A;a,b.<[a;b]) L2))
BY
{ TACTIC:((Auto THEN ParallelLast)
          THEN Auto
          THEN (Assert ∀[a:A]. ∀[m,k:Des(A;a,b.<[a;b])].  (descending(a,b.<[a;b];m @ [a / k]) ∈ ℙ) BY
                      (Auto THEN D -2 THEN D -1 THEN Auto))
          THEN (Assert ∀[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) BY
                      (Auto THEN BackThruSomeHyp))) }

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)
⊢ {∀n:Des(A;a,b.<[a;b]). P[n]}

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}[<:A  {}\mrightarrow{}  A  {}\mrightarrow{}  \mBbbP{}].
    ((\mforall{}a,b:A.    SqStable(<[a;b]))
    {}\mRightarrow{}  WellFnd\{i\}(A;a,b.<[a;b])
    {}\mRightarrow{}  WellFnd\{i\}(Des(A;a,b.<[a;b]);L1,L2.L1  llex(A;a,b.<[a;b])  L2))


By

---

Latex:
TACTIC:((Auto  THEN  ParallelLast)
                THEN  Auto
                THEN  (Assert  \mforall{}[a:A].  \mforall{}[m,k:Des(A;a,b.<[a;b])].    (descending(a,b.<[a;b];m  @  [a  /  k])  \mmember{}  \mBbbP{})  BY
                                        (Auto  THEN  D  -2  THEN  D  -1  THEN  Auto))
                THEN  (Assert  \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)  BY
                                        (Auto  THEN  BackThruSomeHyp)))

---

Home Index