---

Step * 1 1 of Lemma product_well_fnd


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])
9. j : A@i
10. ∀k:A. (Ra[k;j] ⇒ (∀b:B. P[<k, b>]))
11. b : B@i
⊢ P[<j, b>]
BY
{ (InstHyp [⌜λ2b.P[<j, b>]⌝] 6⋅ THENA 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])
9. j : A@i
10. ∀k:A. (Ra[k;j] ⇒ (∀b:B. P[<k, b>]))
11. b : B@i
12. j@0 : B@i
13. ∀k:B. (Rb[k;j@0] ⇒ P[<j, k>])
⊢ P[<j, j@0>]

2
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])
9. j : A@i
10. ∀k:A. (Ra[k;j] ⇒ (∀b:B. P[<k, b>]))
11. b : B@i
12. ∀n:B. P[<j, n>]
⊢ P[<j, b>]

---

Latex:

---

Latex:

1.  [A]  :  Type
2.  [B]  :  Type
3.  [Ra]  :  A  {}\mrightarrow{}  A  {}\mrightarrow{}  \mBbbP{}
4.  [Rb]  :  B  {}\mrightarrow{}  B  {}\mrightarrow{}  \mBbbP{}
5.  \mforall{}[P:A  {}\mrightarrow{}  \mBbbP{}].  ((\mforall{}j:A.  ((\mforall{}k:A.  (Ra[k;j]  {}\mRightarrow{}  P[k]))  {}\mRightarrow{}  P[j]))  {}\mRightarrow{}  \{\mforall{}n:A.  P[n]\})
6.  \mforall{}[P:B  {}\mrightarrow{}  \mBbbP{}].  ((\mforall{}j:B.  ((\mforall{}k:B.  (Rb[k;j]  {}\mRightarrow{}  P[k]))  {}\mRightarrow{}  P[j]))  {}\mRightarrow{}  \{\mforall{}n:B.  P[n]\})
7.  [P]  :  (A  \mtimes{}  B)  {}\mrightarrow{}  \mBbbP{}
8.  \mforall{}j:A  \mtimes{}  B
          ((\mforall{}k:A  \mtimes{}  B.  (let  a1,b1  =  k  in  let  a2,b2  =  j  in  Ra[a1;a2]  \mvee{}  ((a1  =  a2)  \mwedge{}  Rb[b1;b2])  {}\mRightarrow{}  P[k]))
          {}\mRightarrow{}  P[j])
9.  j  :  A@i
10.  \mforall{}k:A.  (Ra[k;j]  {}\mRightarrow{}  (\mforall{}b:B.  P[<k,  b>]))
11.  b  :  B@i
\mvdash{}  P[<j,  b>]


By

---

Latex:
(InstHyp  [\mkleeneopen{}\mlambda{}\msubtwo{}b.P[<j,  b>]\mkleeneclose{}]  6\mcdot{}  THENA  Auto)\mcdot{}

---

Home Index