---

Step * of Lemma product_well_fnd

∀[A,B:Type]. ∀[Ra:A ⟶ A ⟶ ℙ]. ∀[Rb:B ⟶ B ⟶ ℙ].
  (WellFnd{i}(A;a1,a2.Ra[a1;a2])
  ⇒ WellFnd{i}(B;b1,b2.Rb[b1;b2])
  ⇒ WellFnd{i}(A × B;p1,p2.let a1,b1 = p1 
                            in let a2,b2 = p2 
                               in Ra[a1;a2] ∨ ((a1 = a2 ∈ A) ∧ Rb[b1;b2])))
BY
{ (Auto THEN All (Unfold `wellfounded`)⋅ THEN Auto) }

1
1. [A] : Type
2. [B] : Type
3. [Ra] : A ⟶ A ⟶ ℙ
4. [Rb] : B ⟶ B ⟶ ℙ
5. ∀[P:A ⟶ ℙ]. ((∀j:A. ((∀k:A. (Ra[k;j] ⇒ P[k])) ⇒ P[j])) ⇒ {∀n:A. P[n]})
6. ∀[P:B ⟶ ℙ]. ((∀j:B. ((∀k:B. (Rb[k;j] ⇒ P[k])) ⇒ P[j])) ⇒ {∀n:B. P[n]})
7. [P] : (A × B) ⟶ ℙ
8. ∀j:A × B. ((∀k:A × B. (let a1,b1 = k in let a2,b2 = j in Ra[a1;a2] ∨ ((a1 = a2 ∈ A) ∧ Rb[b1;b2]) ⇒ P[k])) ⇒ P[j])
⊢ {∀n:A × B. P[n]}

---

Latex:

---

Latex:
\mforall{}[A,B:Type].  \mforall{}[Ra:A  {}\mrightarrow{}  A  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[Rb:B  {}\mrightarrow{}  B  {}\mrightarrow{}  \mBbbP{}].
    (WellFnd\{i\}(A;a1,a2.Ra[a1;a2])
    {}\mRightarrow{}  WellFnd\{i\}(B;b1,b2.Rb[b1;b2])
    {}\mRightarrow{}  WellFnd\{i\}(A  \mtimes{}  B;p1,p2.let  a1,b1  =  p1 
                                                        in  let  a2,b2  =  p2 
                                                              in  Ra[a1;a2]  \mvee{}  ((a1  =  a2)  \mwedge{}  Rb[b1;b2])))


By

---

Latex:
(Auto  THEN  All  (Unfold  `wellfounded`)\mcdot{}  THEN  Auto)

---

Home Index