Step
*
1
of Lemma
unsquashed-monotone-bar-induction8-false
1. ∀Q:n:ℕ ⟶ (ℕn ⟶ ℕ) ⟶ ℙ
((∀n:ℕ. ∀s:ℕn ⟶ ℕ. ((∀m:ℕ. Q[n + 1;s.m@n])
⇒ Q[n;s]))
⇒ (∀f:ℕ ⟶ ℕ. ⇃(∃n:ℕ. ∀m:{n...}. Q[m;f]))
⇒ Q[0;λx.⊥])
2. F : (ℕ ⟶ ℕ) ⟶ ℕ
3. a : ℕ ⟶ ℕ
⊢ ∃n:ℕ. ∀b:ℕ ⟶ ℕ. ((∀i:ℕn. ((a i) = (b i) ∈ ℕ))
⇒ ((F a) = (F b) ∈ ℕ))
BY
{ ((InstHyp [⌜λ2k.λ2f.∃n:{k...}
∀b:ℕ ⟶ ℕ
((∀i:ℕn. ((rep-seq-from(f;k;a) i) = (b i) ∈ ℕ))
⇒ ((F rep-seq-from(f;k;a)) = (F b) ∈ ℕ))⌝
] (-3)⋅
THENA Auto
)
THEN AllReduce
) }
1
1. ∀Q:n:ℕ ⟶ (ℕn ⟶ ℕ) ⟶ ℙ
((∀n:ℕ. ∀s:ℕn ⟶ ℕ. ((∀m:ℕ. Q[n + 1;s.m@n])
⇒ Q[n;s]))
⇒ (∀f:ℕ ⟶ ℕ. ⇃(∃n:ℕ. ∀m:{n...}. Q[m;f]))
⇒ 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. ∀Q:n:ℕ ⟶ (ℕn ⟶ ℕ) ⟶ ℙ
((∀n:ℕ. ∀s:ℕn ⟶ ℕ. ((∀m:ℕ. Q[n + 1;s.m@n])
⇒ Q[n;s]))
⇒ (∀f:ℕ ⟶ ℕ. ⇃(∃n:ℕ. ∀m:{n...}. Q[m;f]))
⇒ Q[0;λx.⊥])
2. F : (ℕ ⟶ ℕ) ⟶ ℕ
3. a : ℕ ⟶ ℕ
4. f : ℕ ⟶ ℕ
⊢ ⇃(∃n:ℕ
∀m:{n...}
∃n:{m...}. ∀b:ℕ ⟶ ℕ. ((∀i:ℕn. ((rep-seq-from(f;m;a) i) = (b i) ∈ ℕ))
⇒ ((F rep-seq-from(f;m;a)) = (F b) ∈ ℕ)))
3
1. ∀Q:n:ℕ ⟶ (ℕn ⟶ ℕ) ⟶ ℙ
((∀n:ℕ. ∀s:ℕn ⟶ ℕ. ((∀m:ℕ. Q[n + 1;s.m@n])
⇒ Q[n;s]))
⇒ (∀f:ℕ ⟶ ℕ. ⇃(∃n:ℕ. ∀m:{n...}. Q[m;f]))
⇒ 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{}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{}. \mforall{}m:\{n...\}. Q[m;f]))
{}\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.\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{}] (-3)\mcdot{}
THENA Auto
)
THEN AllReduce
)
Home
Index