---

Step * 1 of Lemma WCPD_wf

.....equality..... 
1. F : (ℕ+ ⟶ ℤ) ⟶ 𝔹
2. H : (ℕ+ ⟶ ℤ) ⟶ 𝔹
3. f : ℕ+ ⟶ ℤ
4. G : n:ℕ+ ⟶ {g:ℕ+ ⟶ ℤ| f = g ∈ (ℕ+n ⟶ ℤ)} 
5. TERMOF{weak-continuity-principle-nat+-int-bool-double-ext:o, 1:l}
   ∈ ∀F,H:(ℕ+ ⟶ ℤ) ⟶ 𝔹. ∀f:ℕ+ ⟶ ℤ. ∀G:n:ℕ+ ⟶ {g:ℕ+ ⟶ ℤ| f = g ∈ (ℕ+n ⟶ ℤ)} .
       ∃n:ℕ+. (F f = F (G n) ∧ H f = H (G n))
⊢ WCPD(F;H;f;G) ~ fst((TERMOF{weak-continuity-principle-nat+-int-bool-double-ext:o, 1:l} F H f G))
BY
{ (RW (AddrC [2] (TagC (mk_tag_term 7))) 0 THEN Fold `WCPD` 0 THEN Auto) }

---

Latex:

---

Latex:
.....equality..... 
1.  F  :  (\mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{})  {}\mrightarrow{}  \mBbbB{}
2.  H  :  (\mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{})  {}\mrightarrow{}  \mBbbB{}
3.  f  :  \mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{}
4.  G  :  n:\mBbbN{}\msupplus{}  {}\mrightarrow{}  \{g:\mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{}|  f  =  g\} 
5.  TERMOF\{weak-continuity-principle-nat+-int-bool-double-ext:o,  1:l\}
      \mmember{}  \mforall{}F,H:(\mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{})  {}\mrightarrow{}  \mBbbB{}.  \mforall{}f:\mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{}.  \mforall{}G:n:\mBbbN{}\msupplus{}  {}\mrightarrow{}  \{g:\mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{}|  f  =  g\}  .
              \mexists{}n:\mBbbN{}\msupplus{}.  (F  f  =  F  (G  n)  \mwedge{}  H  f  =  H  (G  n))
\mvdash{}  WCPD(F;H;f;G)  \msim{}  fst((TERMOF\{weak-continuity-principle-nat+-int-bool-double-ext:o,  1:l\}  F  H  f  G))


By

---

Latex:
(RW  (AddrC  [2]  (TagC  (mk\_tag\_term  7)))  0  THEN  Fold  `WCPD`  0  THEN  Auto)

---

Home Index