Step
*
1
of Lemma
gen-bar-rec
1. P : n:ℕ ⟶ (ℕn ⟶ ℕ) ⟶ ℙ@i'
2. ind : ∀n:ℕ. ∀s:ℕn ⟶ ℕ. ((∀m:ℕ. P[n + 1;s.m@n]) ⇒ P[n;s])@i
3. bar : ∀f:ℕ ⟶ ℕ. ⇃(∃n:ℕ. ∀m:{n...}. P[m;f])@i
4. M : n:ℕ ⟶ s:(ℕn ⟶ ℕ) ⟶ (k:ℕn × (∀m:{k...}. P[m;ext2Baire(n;s;0)])?)@i
5. ∀f:ℕ ⟶ ℕ
∃n:ℕ
∃k:ℕn
∃p:∀m:{k...}. P[m;ext2Baire(n;f;0)]
(((M n f) = (inl <k, p>) ∈ (k:ℕn × (∀m:{k...}. P[m;ext2Baire(n;f;0)])?)) ∧ (∀m:ℕ. ((↑isl(M m f)) ⇒ (m = n ∈ ℕ))\000C))
⊢ P[0;λx.⊥]
BY
{ ((Subst' ⌜(λx.⊥) = seq-normalize(0;⊥) ∈ (ℕ0 ⟶ ℕ)⌝ 0⋅ THENA Auto)
THEN UseWitness ⌜spector-bar-rec(λn,s. if M n s then 0 else n + 1 fi ;λn,s. case M n s
of inl(x) =>
let k,F = x
in F n
| inr(x) =>
⊥;ind;0;seq-normalize(0;⊥))⌝⋅
THEN (Assert ⌜↓spector-bar-rec(λn,s. if M n s then 0 else n + 1 fi ;λn,s. case M n s
of inl(x) =>
let k,F = x
in F n
| inr(x) =>
⊥;ind;0;seq-normalize(0;⊥))
∈ P[0;seq-normalize(0;⊥)]⌝⋅
THENM Unsquash
)
THEN (Subst ⌜spector-bar-rec(λn,s. if M n s then 0 else n + 1 fi ;λn,s. case M n s
of inl(x) =>
let k,F = x
in F n
| inr(x) =>
⊥;ind;0;seq-normalize(0;⊥))
∈ P[0;seq-normalize(0;⊥)] ~ (λn,s. (spector-bar-rec(λn,s. if M n s then 0 else n + 1 fi ;λn,s. case M n \000Cs
of inl(x) =>
let k,F = x
in F n
| inr(x) =>
⊥;ind;n;s)
∈ P[n;s]))
0
seq-normalize(0;⊥)⌝ 0⋅
THENA (Reduce 0 THEN Auto)
)) }
1
1. P : n:ℕ ⟶ (ℕn ⟶ ℕ) ⟶ ℙ@i'
2. ind : ∀n:ℕ. ∀s:ℕn ⟶ ℕ. ((∀m:ℕ. P[n + 1;s.m@n]) ⇒ P[n;s])@i
3. bar : ∀f:ℕ ⟶ ℕ. ⇃(∃n:ℕ. ∀m:{n...}. P[m;f])@i
4. M : n:ℕ ⟶ s:(ℕn ⟶ ℕ) ⟶ (k:ℕn × (∀m:{k...}. P[m;ext2Baire(n;s;0)])?)@i
5. ∀f:ℕ ⟶ ℕ
∃n:ℕ
∃k:ℕn
∃p:∀m:{k...}. P[m;ext2Baire(n;f;0)]
(((M n f) = (inl <k, p>) ∈ (k:ℕn × (∀m:{k...}. P[m;ext2Baire(n;f;0)])?)) ∧ (∀m:ℕ. ((↑isl(M m f)) ⇒ (m = n ∈ ℕ))\000C))
⊢ ↓(λn,s. (spector-bar-rec(λn,s. if M n s then 0 else n + 1 fi ;λn,s. case M n s
of inl(x) =>
let k,F = x
in F n
| inr(x) =>
⊥;ind;n;s) ∈ P[n;s]))
0
seq-normalize(0;⊥)
Latex:
Latex:
1. P : n:\mBbbN{} {}\mrightarrow{} (\mBbbN{}n {}\mrightarrow{} \mBbbN{}) {}\mrightarrow{} \mBbbP{}@i'
2. ind : \mforall{}n:\mBbbN{}. \mforall{}s:\mBbbN{}n {}\mrightarrow{} \mBbbN{}. ((\mforall{}m:\mBbbN{}. P[n + 1;s.m@n]) {}\mRightarrow{} P[n;s])@i
3. bar : \mforall{}f:\mBbbN{} {}\mrightarrow{} \mBbbN{}. \00D9(\mexists{}n:\mBbbN{}. \mforall{}m:\{n...\}. P[m;f])@i
4. M : n:\mBbbN{} {}\mrightarrow{} s:(\mBbbN{}n {}\mrightarrow{} \mBbbN{}) {}\mrightarrow{} (k:\mBbbN{}n \mtimes{} (\mforall{}m:\{k...\}. P[m;ext2Baire(n;s;0)])?)@i
5. \mforall{}f:\mBbbN{} {}\mrightarrow{} \mBbbN{}
\mexists{}n:\mBbbN{}
\mexists{}k:\mBbbN{}n
\mexists{}p:\mforall{}m:\{k...\}. P[m;ext2Baire(n;f;0)]
(((M n f) = (inl <k, p>)) \mwedge{} (\mforall{}m:\mBbbN{}. ((\muparrow{}isl(M m f)) {}\mRightarrow{} (m = n))))
\mvdash{} P[0;\mlambda{}x.\mbot{}]
By
Latex:
((Subst' \mkleeneopen{}(\mlambda{}x.\mbot{}) = seq-normalize(0;\mbot{})\mkleeneclose{} 0\mcdot{} THENA Auto)
THEN UseWitness \mkleeneopen{}spector-bar-rec(\mlambda{}n,s. if M n s then 0 else n + 1 fi ;\mlambda{}n,s. case M n s
of inl(x) =>
let k,F = x
in F n
| inr(x) =>
\mbot{};ind;0;seq-normalize(0;\mbot{}))\000C\mkleeneclose{}\mcdot{}
THEN (Assert \mkleeneopen{}\mdownarrow{}spector-bar-rec(\mlambda{}n,s. if M n s then 0 else n + 1 fi ;\mlambda{}n,s. case M n s
of inl(x) =>
let k,F = x
in F n
| inr(x) =>
\mbot{};ind;0;seq-normalize(0;\mbot{}))
\mmember{} P[0;seq-normalize(0;\mbot{})]\mkleeneclose{}\mcdot{}
THENM Unsquash
)
THEN (Subst \mkleeneopen{}spector-bar-rec(\mlambda{}n,s. if M n s then 0 else n + 1 fi ;\mlambda{}n,s. case M n s
of inl(x) =>
let k,F = x
in F n
| inr(x) =>
\mbot{};ind;0;seq-normalize(0;\mbot{}))
\mmember{} P[0;seq-normalize(0;\mbot{})] \msim{} (\mlambda{}n,s. (spector-bar-rec(\mlambda{}n,s. if M n s
then 0
else n + 1
fi ;\mlambda{}n,s. case M n s
of inl(x) =>
let k,F = x
in F n
| inr(x) =>
\mbot{};ind;n;s) \mmember{} P[n;s]))
0
seq-normalize(0;\mbot{})\mkleeneclose{} 0\mcdot{}
THENA (Reduce 0 THEN Auto)
))
Home
Index