---

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


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))
BY
{ ((Assert mu(λn.(F f =b F (G (n + 1)) ∧b H f =b H (G (n + 1)))) ∈ ℕ BY
          (SqExRepD
           THEN InstLemma `mu_wf` [⌜λn.(F f =b F (G (n + 1)) ∧b H f =b H (G (n + 1)))⌝]⋅
           THEN All Reduce
           THEN Auto))
   THEN D 0 With ⌜mu(λn.(F f =b F (G (n + 1)) ∧b H f =b H (G (n + 1)))) + 1⌝ 
   THEN Auto
   THEN InstLemma `mu-property` [⌜λn.(F f =b F (G (n + 1)) ∧b H f =b H (G (n + 1)))⌝]⋅
   THEN All Reduce
   THEN Auto) }

1
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)))
8. mu(λn.(F f =b F (G (n + 1)) ∧b H f =b H (G (n + 1)))) ∈ ℕ
9. ↑(F f =b F (G (mu(λn.(F f =b F (G (n + 1)) ∧b H f =b H (G (n + 1)))) + 1))
∧b H f =b H (G (mu(λn.(F f =b F (G (n + 1)) ∧b H f =b H (G (n + 1)))) + 1)))
10. ∀[i:ℕ]
      ¬↑(F f =b F (G (i + 1)) ∧b H f =b H (G (i + 1))) 
      supposing i < mu(λn.(F f =b F (G (n + 1)) ∧b H f =b H (G (n + 1))))
⊢ F f = F (G (mu(λn.(F f =b F (G (n + 1)) ∧b H f =b H (G (n + 1)))) + 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)))
8. mu(λn.(F f =b F (G (n + 1)) ∧b H f =b H (G (n + 1)))) ∈ ℕ
9. F f = F (G (mu(λn.(F f =b F (G (n + 1)) ∧b H f =b H (G (n + 1)))) + 1))
10. ↑(F f =b F (G (mu(λn.(F f =b F (G (n + 1)) ∧b H f =b H (G (n + 1)))) + 1))
∧b H f =b H (G (mu(λn.(F f =b F (G (n + 1)) ∧b H f =b H (G (n + 1)))) + 1)))
11. ∀[i:ℕ]
      ¬↑(F f =b F (G (i + 1)) ∧b H f =b H (G (i + 1))) 
      supposing i < mu(λn.(F f =b F (G (n + 1)) ∧b H f =b H (G (n + 1))))
⊢ H f = H (G (mu(λn.(F f =b F (G (n + 1)) ∧b H f =b H (G (n + 1)))) + 1))

---

Latex:

---

Latex:

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.  \00D9(\mexists{}n:\mBbbN{}
            \mforall{}g:\mBbbN{}  {}\mrightarrow{}  \mBbbZ{}
                (((\mlambda{}n.(f  (n  +  1)))  =  g)
                {}\mRightarrow{}  (if  F  (\mlambda{}n.(f  ((n  -  1)  +  1)))  then  1  else  0  fi 
                      =  if  F  (\mlambda{}n.(g  (n  -  1)))  then  1  else  0  fi  )))
6.  \00D9(\mexists{}n:\mBbbN{}
            \mforall{}g:\mBbbN{}  {}\mrightarrow{}  \mBbbZ{}
                (((\mlambda{}n.(f  (n  +  1)))  =  g)
                {}\mRightarrow{}  (if  H  (\mlambda{}n.(f  ((n  -  1)  +  1)))  then  1  else  0  fi 
                      =  if  H  (\mlambda{}n.(g  (n  -  1)))  then  1  else  0  fi  )))
7.  \mdownarrow{}\mexists{}n:\mBbbN{}.  (F  f  =  F  (G  (n  +  1))  \mwedge{}  H  f  =  H  (G  (n  +  1)))
\mvdash{}  \mexists{}n:\mBbbN{}\msupplus{}.  (F  f  =  F  (G  n)  \mwedge{}  H  f  =  H  (G  n))


By

---

Latex:
((Assert  mu(\mlambda{}n.(F  f  =b  F  (G  (n  +  1))  \mwedge{}\msubb{}  H  f  =b  H  (G  (n  +  1))))  \mmember{}  \mBbbN{}  BY
                (SqExRepD
                  THEN  InstLemma  `mu\_wf`  [\mkleeneopen{}\mlambda{}n.(F  f  =b  F  (G  (n  +  1))  \mwedge{}\msubb{}  H  f  =b  H  (G  (n  +  1)))\mkleeneclose{}]\mcdot{}
                  THEN  All  Reduce
                  THEN  Auto))
  THEN  D  0  With  \mkleeneopen{}mu(\mlambda{}n.(F  f  =b  F  (G  (n  +  1))  \mwedge{}\msubb{}  H  f  =b  H  (G  (n  +  1))))  +  1\mkleeneclose{} 
  THEN  Auto
  THEN  InstLemma  `mu-property`  [\mkleeneopen{}\mlambda{}n.(F  f  =b  F  (G  (n  +  1))  \mwedge{}\msubb{}  H  f  =b  H  (G  (n  +  1)))\mkleeneclose{}]\mcdot{}
  THEN  All  Reduce
  THEN  Auto)

---

Home Index