Proof of Nuprl Lemma : unsquashed-BIM-implies-unsquashed-weak-continuity

Step * 1 of Lemma unsquashed-BIM-implies-unsquashed-weak-continuity

1. ∀B,Q:n:ℕ ⟶ (ℕn ⟶ ℕ) ⟶ ℙ.
     ((∀n:ℕ. ∀s:ℕn ⟶ ℕ.  ((∀m:ℕ. Q[n + 1;s.m@n]) ⇒ Q[n;s]))
     ⇒ (∀f:ℕ ⟶ ℕ. ⇃(∃n:ℕ. B[n;f]))
     ⇒ (∀n:ℕ. ∀s:ℕn ⟶ ℕ. ∀m:ℕ.  (B[n;s] ⇒ B[n + 1;s.m@n]))
     ⇒ (∀n:ℕ. ∀s:ℕn ⟶ ℕ.  (B[n;s] ⇒ Q[n;s]))
     ⇒ Q[0;λx.⊥])
2. F : (ℕ ⟶ ℕ) ⟶ ℕ
3. a : ℕ ⟶ ℕ
⊢ ∃n:ℕ. ∀b:ℕ ⟶ ℕ. ((∀i:ℕn. ((a i) = (b i) ∈ ℕ)) ⇒ ((F a) = (F b) ∈ ℕ))
BY
{ ((InstHyp [⌜λ₂k.λ₂f.∀b:ℕ ⟶ ℕ
                        ((∀i:ℕk. ((rep-seq-from(f;k;a) i) = (b i) ∈ ℕ)) ⇒ ((F rep-seq-from(f;k;a)) = (F b) ∈ ℕ))⌝;
    ⌜λ₂k.λ₂f.∃n:{k...}
              ∀b:ℕ ⟶ ℕ. ((∀i:ℕn. ((rep-seq-from(f;k;a) i) = (b i) ∈ ℕ)) ⇒ ((F rep-seq-from(f;k;a)) = (F b) ∈ ℕ))⌝] 1⋅
    THENA Auto
    )
   THEN AllReduce
   ) }

1
1. ∀B,Q:n:ℕ ⟶ (ℕn ⟶ ℕ) ⟶ ℙ.
     ((∀n:ℕ. ∀s:ℕn ⟶ ℕ.  ((∀m:ℕ. Q[n + 1;s.m@n]) ⇒ Q[n;s]))
     ⇒ (∀f:ℕ ⟶ ℕ. ⇃(∃n:ℕ. B[n;f]))
     ⇒ (∀n:ℕ. ∀s:ℕn ⟶ ℕ. ∀m:ℕ.  (B[n;s] ⇒ B[n + 1;s.m@n]))
     ⇒ (∀n:ℕ. ∀s:ℕn ⟶ ℕ.  (B[n;s] ⇒ Q[n;s]))
     ⇒ Q[0;λx.⊥])
2. F : (ℕ ⟶ ℕ) ⟶ ℕ
3. a : ℕ ⟶ ℕ
4. n : ℕ
5. s : ℕn ⟶ ℕ
6. ∀m:ℕ
     ∃n@0:{n + 1...}
      ∀b:ℕ ⟶ ℕ
        ((∀i:ℕn@0. ((rep-seq-from(s.m@n;n + 1;a) i) = (b i) ∈ ℕ)) ⇒ ((F rep-seq-from(s.m@n;n + 1;a)) = (F b) ∈ ℕ))
⊢ ∃n@0:{n...}. ∀b:ℕ ⟶ ℕ. ((∀i:ℕn@0. ((rep-seq-from(s;n;a) i) = (b i) ∈ ℕ)) ⇒ ((F rep-seq-from(s;n;a)) = (F b) ∈ ℕ))

2
1. ∀B,Q:n:ℕ ⟶ (ℕn ⟶ ℕ) ⟶ ℙ.
     ((∀n:ℕ. ∀s:ℕn ⟶ ℕ.  ((∀m:ℕ. Q[n + 1;s.m@n]) ⇒ Q[n;s]))
     ⇒ (∀f:ℕ ⟶ ℕ. ⇃(∃n:ℕ. B[n;f]))
     ⇒ (∀n:ℕ. ∀s:ℕn ⟶ ℕ. ∀m:ℕ.  (B[n;s] ⇒ B[n + 1;s.m@n]))
     ⇒ (∀n:ℕ. ∀s:ℕn ⟶ ℕ.  (B[n;s] ⇒ Q[n;s]))
     ⇒ Q[0;λx.⊥])
2. F : (ℕ ⟶ ℕ) ⟶ ℕ
3. a : ℕ ⟶ ℕ
4. f : ℕ ⟶ ℕ
⊢ ⇃(∃n:ℕ. ∀b:ℕ ⟶ ℕ. ((∀i:ℕn. ((rep-seq-from(f;n;a) i) = (b i) ∈ ℕ)) ⇒ ((F rep-seq-from(f;n;a)) = (F b) ∈ ℕ)))

3
1. ∀B,Q:n:ℕ ⟶ (ℕn ⟶ ℕ) ⟶ ℙ.
     ((∀n:ℕ. ∀s:ℕn ⟶ ℕ.  ((∀m:ℕ. Q[n + 1;s.m@n]) ⇒ Q[n;s]))
     ⇒ (∀f:ℕ ⟶ ℕ. ⇃(∃n:ℕ. B[n;f]))
     ⇒ (∀n:ℕ. ∀s:ℕn ⟶ ℕ. ∀m:ℕ.  (B[n;s] ⇒ B[n + 1;s.m@n]))
     ⇒ (∀n:ℕ. ∀s:ℕn ⟶ ℕ.  (B[n;s] ⇒ Q[n;s]))
     ⇒ Q[0;λx.⊥])
2. F : (ℕ ⟶ ℕ) ⟶ ℕ
3. a : ℕ ⟶ ℕ
4. n : ℕ
5. s : ℕn ⟶ ℕ
6. m : ℕ
7. ∀b:ℕ ⟶ ℕ. ((∀i:ℕn. ((rep-seq-from(s;n;a) i) = (b i) ∈ ℕ)) ⇒ ((F rep-seq-from(s;n;a)) = (F b) ∈ ℕ))
⊢ ∀b:ℕ ⟶ ℕ
    ((∀i:ℕn + 1. ((rep-seq-from(s.m@n;n + 1;a) i) = (b i) ∈ ℕ)) ⇒ ((F rep-seq-from(s.m@n;n + 1;a)) = (F b) ∈ ℕ))

4
1. ∀B,Q:n:ℕ ⟶ (ℕn ⟶ ℕ) ⟶ ℙ.
     ((∀n:ℕ. ∀s:ℕn ⟶ ℕ.  ((∀m:ℕ. Q[n + 1;s.m@n]) ⇒ Q[n;s]))
     ⇒ (∀f:ℕ ⟶ ℕ. ⇃(∃n:ℕ. B[n;f]))
     ⇒ (∀n:ℕ. ∀s:ℕn ⟶ ℕ. ∀m:ℕ.  (B[n;s] ⇒ B[n + 1;s.m@n]))
     ⇒ (∀n:ℕ. ∀s:ℕn ⟶ ℕ.  (B[n;s] ⇒ Q[n;s]))
     ⇒ Q[0;λx.⊥])
2. F : (ℕ ⟶ ℕ) ⟶ ℕ
3. a : ℕ ⟶ ℕ
4. n : ℕ
5. s : ℕn ⟶ ℕ
6. ∀b:ℕ ⟶ ℕ. ((∀i:ℕn. ((rep-seq-from(s;n;a) i) = (b i) ∈ ℕ)) ⇒ ((F rep-seq-from(s;n;a)) = (F b) ∈ ℕ))
⊢ ∃n@0:{n...}. ∀b:ℕ ⟶ ℕ. ((∀i:ℕn@0. ((rep-seq-from(s;n;a) i) = (b i) ∈ ℕ)) ⇒ ((F rep-seq-from(s;n;a)) = (F b) ∈ ℕ))

5
1. ∀B,Q:n:ℕ ⟶ (ℕn ⟶ ℕ) ⟶ ℙ.
     ((∀n:ℕ. ∀s:ℕn ⟶ ℕ.  ((∀m:ℕ. Q[n + 1;s.m@n]) ⇒ Q[n;s]))
     ⇒ (∀f:ℕ ⟶ ℕ. ⇃(∃n:ℕ. B[n;f]))
     ⇒ (∀n:ℕ. ∀s:ℕn ⟶ ℕ. ∀m:ℕ.  (B[n;s] ⇒ B[n + 1;s.m@n]))
     ⇒ (∀n:ℕ. ∀s:ℕn ⟶ ℕ.  (B[n;s] ⇒ Q[n;s]))
     ⇒ Q[0;λx.⊥])
2. F : (ℕ ⟶ ℕ) ⟶ ℕ
3. a : ℕ ⟶ ℕ
4. ∃n:{0...}. ∀b:ℕ ⟶ ℕ. ((∀i:ℕn. ((rep-seq-from(λx.⊥;0;a) i) = (b i) ∈ ℕ)) ⇒ ((F rep-seq-from(λx.⊥;0;a)) = (F b) ∈ ℕ))
⊢ ∃n:ℕ. ∀b:ℕ ⟶ ℕ. ((∀i:ℕn. ((a i) = (b i) ∈ ℕ)) ⇒ ((F a) = (F b) ∈ ℕ))

Latex:

Latex:
1. \mforall{}B,Q:n:\mBbbN{} {}\mrightarrow{} (\mBbbN{}n {}\mrightarrow{} \mBbbN{}) {}\mrightarrow{} \mBbbP{}. ((\mforall{}n:\mBbbN{}. \mforall{}s:\mBbbN{}n {}\mrightarrow{} \mBbbN{}. ((\mforall{}m:\mBbbN{}. Q[n + 1;s.m@n]) {}\mRightarrow{} Q[n;s])) {}\mRightarrow{} (\mforall{}f:\mBbbN{} {}\mrightarrow{} \mBbbN{}. \00D9(\mexists{}n:\mBbbN{}. B[n;f])) {}\mRightarrow{} (\mforall{}n:\mBbbN{}. \mforall{}s:\mBbbN{}n {}\mrightarrow{} \mBbbN{}. \mforall{}m:\mBbbN{}. (B[n;s] {}\mRightarrow{} B[n + 1;s.m@n])) {}\mRightarrow{} (\mforall{}n:\mBbbN{}. \mforall{}s:\mBbbN{}n {}\mrightarrow{} \mBbbN{}. (B[n;s] {}\mRightarrow{} Q[n;s])) {}\mRightarrow{} Q[0;\mlambda{}x.\mbot{}]) 2. F : (\mBbbN{} {}\mrightarrow{} \mBbbN{}) {}\mrightarrow{} \mBbbN{} 3. a : \mBbbN{} {}\mrightarrow{} \mBbbN{} \mvdash{} \mexists{}n:\mBbbN{}. \mforall{}b:\mBbbN{} {}\mrightarrow{} \mBbbN{}. ((\mforall{}i:\mBbbN{}n. ((a i) = (b i))) {}\mRightarrow{} ((F a) = (F b))) By Latex: ((InstHyp [\mkleeneopen{}\mlambda{}\msubtwo{}k.\mlambda{}\msubtwo{}f.\mforall{}b:\mBbbN{} {}\mrightarrow{} \mBbbN{} ((\mforall{}i:\mBbbN{}k. ((rep-seq-from(f;k;a) i) = (b i))) {}\mRightarrow{} ((F rep-seq-from(f;k;a)) = (F b)))\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}k.\mlambda{}\msubtwo{}f.\mexists{}n:\{k...\} \mforall{}b:\mBbbN{} {}\mrightarrow{} \mBbbN{} ((\mforall{}i:\mBbbN{}n ((rep-seq-from(f;k;a) i) = (b i))) {}\mRightarrow{} ((F rep-seq-from(f;k;a)) = (F b)))\mkleeneclose{}] 1\mcdot{} THENA Auto ) THEN AllReduce ) Home Index