Step
*
1
1
of Lemma
WCP_wf
.....equality.....
1. F : (ℕ+ ⟶ ℤ) ⟶ 𝔹
2. f : ℕ+ ⟶ ℤ
3. G : n:ℕ+ ⟶ {g:ℕ+ ⟶ ℤ| f = g ∈ (ℕ+n ⟶ ℤ)}
4. TERMOF{weak-continuity-principle-nat+-int-bool-ext:o, 1:l} ∈ ∀F:(ℕ+ ⟶ ℤ) ⟶ 𝔹. ∀f:ℕ+ ⟶ ℤ. ∀G:n:ℕ+ ⟶ {g:ℕ+ ⟶ ℤ|
f
= g
∈ (ℕ+n
⟶ ℤ)} .
∃n:ℕ+. F f = F (G n)
⊢ WCP(F;f;G) ~ fst((TERMOF{weak-continuity-principle-nat+-int-bool-ext:o, 1:l} F f G))
BY
{ RW (AddrC [2] (TagC (mk_tag_term 6))) 0 }
1
1. F : (ℕ+ ⟶ ℤ) ⟶ 𝔹
2. f : ℕ+ ⟶ ℤ
3. G : n:ℕ+ ⟶ {g:ℕ+ ⟶ ℤ| f = g ∈ (ℕ+n ⟶ ℤ)}
4. TERMOF{weak-continuity-principle-nat+-int-bool-ext:o, 1:l} ∈ ∀F:(ℕ+ ⟶ ℤ) ⟶ 𝔹. ∀f:ℕ+ ⟶ ℤ. ∀G:n:ℕ+ ⟶ {g:ℕ+ ⟶ ℤ|
f
= g
∈ (ℕ+n
⟶ ℤ)} .
∃n:ℕ+. F f = F (G n)
⊢ WCP(F;f;G) ~ mu(λn.F f =b F (G (n + 1))) + 1
Latex:
Latex:
.....equality.....
1. F : (\mBbbN{}\msupplus{} {}\mrightarrow{} \mBbbZ{}) {}\mrightarrow{} \mBbbB{}
2. f : \mBbbN{}\msupplus{} {}\mrightarrow{} \mBbbZ{}
3. G : n:\mBbbN{}\msupplus{} {}\mrightarrow{} \{g:\mBbbN{}\msupplus{} {}\mrightarrow{} \mBbbZ{}| f = g\}
4. TERMOF\{weak-continuity-principle-nat+-int-bool-ext:o, 1:l\}
\mmember{} \mforall{}F:(\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)
\mvdash{} WCP(F;f;G) \msim{} fst((TERMOF\{weak-continuity-principle-nat+-int-bool-ext:o, 1:l\} F f G))
By
Latex:
RW (AddrC [2] (TagC (mk\_tag\_term 6))) 0
Home
Index