---

Step * of Lemma wellfounded-lex

∀[A:Type]. ∀[<A:A ⟶ A ⟶ ℙ].
  (WellFnd{i}(A;a,b.<A[a;b])
  ⇒ (∀[B:Type]. ∀[<B:B ⟶ B ⟶ ℙ].
        (WellFnd{i}(B;a,b.<B[a;b])
        ⇒ WellFnd{i}(A × B;p,q.<A[fst(p);fst(q)] ∨ (((fst(p)) = (fst(q)) ∈ A) ∧ <B[snd(p);snd(q)])))))
BY
{ (Auto
   THEN All (Unfold `wellfounded`)
   THEN Auto
   THEN Unfold `guard` 0
   THEN Auto
   THEN D -1
   THEN RenameVar `a' (-2)
   THEN RenameVar `b' (-1)
   THEN RepeatFor 2 (MoveToConcl (-1))) }

1
1. [A] : Type
2. [<A] : A ⟶ A ⟶ ℙ
3. ∀[P:A ⟶ ℙ]. ((∀j:A. ((∀k:A. (<A[k;j] ⇒ P[k])) ⇒ P[j])) ⇒ {∀n:A. P[n]})
4. [B] : Type
5. [<B] : B ⟶ B ⟶ ℙ
6. ∀[P:B ⟶ ℙ]. ((∀j:B. ((∀k:B. (<B[k;j] ⇒ P[k])) ⇒ P[j])) ⇒ {∀n:B. P[n]})
7. [P] : (A × B) ⟶ ℙ
8. ∀j:A × B. ((∀k:A × B. ((<A[fst(k);fst(j)] ∨ (((fst(k)) = (fst(j)) ∈ A) ∧ <B[snd(k);snd(j)])) ⇒ P[k])) ⇒ P[j])
⊢ ∀a:A. ∀b:B.  P[<a, b>]

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}[<A:A  {}\mrightarrow{}  A  {}\mrightarrow{}  \mBbbP{}].
    (WellFnd\{i\}(A;a,b.<A[a;b])
    {}\mRightarrow{}  (\mforall{}[B:Type].  \mforall{}[<B:B  {}\mrightarrow{}  B  {}\mrightarrow{}  \mBbbP{}].
                (WellFnd\{i\}(B;a,b.<B[a;b])
                {}\mRightarrow{}  WellFnd\{i\}(A  \mtimes{}  B;p,q.<A[fst(p);fst(q)]  \mvee{}  (((fst(p))  =  (fst(q)))  \mwedge{}  <B[snd(p);snd(q)])))))


By

---

Latex:
(Auto
  THEN  All  (Unfold  `wellfounded`)
  THEN  Auto
  THEN  Unfold  `guard`  0
  THEN  Auto
  THEN  D  -1
  THEN  RenameVar  `a'  (-2)
  THEN  RenameVar  `b'  (-1)
  THEN  RepeatFor  2  (MoveToConcl  (-1)))

---

Home Index