---

Step * of Lemma weak-continuity-principle-nat+-int-bool-double

∀F,H:(ℕ+ ⟶ ℤ) ⟶ 𝔹. ∀f:ℕ+ ⟶ ℤ. ∀G:n:ℕ+ ⟶ {g:ℕ+ ⟶ ℤ| f = g ∈ (ℕ+n ⟶ ℤ)} .  ∃n:ℕ+. (F f = F (G n) ∧ H f = H (G n))
BY
{ ((Auto
    THEN (InstLemma `weak-continuity-nat-int` 
          [⌜λf.if F (λn.(f (n - 1))) then 1 else 0 fi ⌝;λn.(f (n + 1))]⋅
          THENA Auto
          )
    )
   THEN Reduce -1
   THEN (InstLemma `weak-continuity-nat-int`  [⌜λf.if H (λn.(f (n - 1))) then 1 else 0 fi ⌝;λn.(f (n + 1))]⋅ THENA Auto)
   THEN Reduce -1
   THEN Assert ⌜↓∃n:ℕ. (F f = F (G (n + 1)) ∧ H f = H (G (n + 1)))⌝⋅) }

1
.....assertion..... 
1. F : (ℕ+ ⟶ ℤ) ⟶ 𝔹
2. H : (ℕ+ ⟶ ℤ) ⟶ 𝔹
3. f : ℕ+ ⟶ ℤ
4. G : n:ℕ+ ⟶ {g:ℕ+ ⟶ ℤ| f = g ∈ (ℕ+n ⟶ ℤ)} 
5. ⇃(∃n:ℕ
      ∀g:ℕ ⟶ ℤ
        (((λn.(f (n + 1))) = g ∈ (ℕn ⟶ ℤ))
        ⇒ (if F (λn.(f ((n - 1) + 1))) then 1 else 0 fi  = if F (λn.(g (n - 1))) then 1 else 0 fi  ∈ ℕ)))
6. ⇃(∃n:ℕ
      ∀g:ℕ ⟶ ℤ
        (((λn.(f (n + 1))) = g ∈ (ℕn ⟶ ℤ))
        ⇒ (if H (λn.(f ((n - 1) + 1))) then 1 else 0 fi  = if H (λn.(g (n - 1))) then 1 else 0 fi  ∈ ℕ)))
⊢ ↓∃n:ℕ. (F f = F (G (n + 1)) ∧ H f = H (G (n + 1)))

2
1. F : (ℕ+ ⟶ ℤ) ⟶ 𝔹
2. H : (ℕ+ ⟶ ℤ) ⟶ 𝔹
3. f : ℕ+ ⟶ ℤ
4. G : n:ℕ+ ⟶ {g:ℕ+ ⟶ ℤ| f = g ∈ (ℕ+n ⟶ ℤ)} 
5. ⇃(∃n:ℕ
      ∀g:ℕ ⟶ ℤ
        (((λn.(f (n + 1))) = g ∈ (ℕn ⟶ ℤ))
        ⇒ (if F (λn.(f ((n - 1) + 1))) then 1 else 0 fi  = if F (λn.(g (n - 1))) then 1 else 0 fi  ∈ ℕ)))
6. ⇃(∃n:ℕ
      ∀g:ℕ ⟶ ℤ
        (((λn.(f (n + 1))) = g ∈ (ℕn ⟶ ℤ))
        ⇒ (if H (λn.(f ((n - 1) + 1))) then 1 else 0 fi  = if H (λn.(g (n - 1))) then 1 else 0 fi  ∈ ℕ)))
7. ↓∃n:ℕ. (F f = F (G (n + 1)) ∧ H f = H (G (n + 1)))
⊢ ∃n:ℕ+. (F f = F (G n) ∧ H f = H (G n))

---

Latex:

---

Latex:
\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))


By

---

Latex:
((Auto
    THEN  (InstLemma  `weak-continuity-nat-int` 
                [\mkleeneopen{}\mlambda{}f.if  F  (\mlambda{}n.(f  (n  -  1)))  then  1  else  0  fi  \mkleeneclose{};\mlambda{}n.(f  (n  +  1))]\mcdot{}
                THENA  Auto
                )
    )
  THEN  Reduce  -1
  THEN  (InstLemma  `weak-continuity-nat-int` 
              [\mkleeneopen{}\mlambda{}f.if  H  (\mlambda{}n.(f  (n  -  1)))  then  1  else  0  fi  \mkleeneclose{};\mlambda{}n.(f  (n  +  1))]\mcdot{}
              THENA  Auto
              )
  THEN  Reduce  -1
  THEN  Assert  \mkleeneopen{}\mdownarrow{}\mexists{}n:\mBbbN{}.  (F  f  =  F  (G  (n  +  1))  \mwedge{}  H  f  =  H  (G  (n  +  1)))\mkleeneclose{}\mcdot{})

---

Home Index