Step
*
1
1
of Lemma
finite-cantor-decider_wf
.....assertion.....
1. T : Type
2. R : T ⟶ T ⟶ ℙ
3. dcdr : ∀x,y:T. Dec(R[x;y])
4. n : ℕ
5. F : (ℕn ⟶ 𝔹) ⟶ T
⊢ λdcdr,n,F. finite-cantor-decider(dcdr;n;F) ∈ ∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].
((∀x,y:T. Dec(R[x;y]))
⇒ (∀n:ℕ. ∀F:(ℕn ⟶ 𝔹) ⟶ T. Dec(∃f,g:ℕn ⟶ 𝔹. R[F f;F g])))
BY
{ (Subst' λdcdr,n,F. finite-cantor-decider(dcdr;n;F) ~ TERMOF{decidable-finite-cantor-ext:o, \\v:l, i:l} 0 THEN Auto) }
1
.....equality.....
1. T : Type
2. R : T ⟶ T ⟶ ℙ
3. dcdr : ∀x,y:T. Dec(R[x;y])
4. n : ℕ
5. F : (ℕn ⟶ 𝔹) ⟶ T
⊢ λdcdr,n,F. finite-cantor-decider(dcdr;n;F) ~ TERMOF{decidable-finite-cantor-ext:o, \\v:l, i:l}
Latex:
Latex:
.....assertion.....
1. T : Type
2. R : T {}\mrightarrow{} T {}\mrightarrow{} \mBbbP{}
3. dcdr : \mforall{}x,y:T. Dec(R[x;y])
4. n : \mBbbN{}
5. F : (\mBbbN{}n {}\mrightarrow{} \mBbbB{}) {}\mrightarrow{} T
\mvdash{} \mlambda{}dcdr,n,F. finite-cantor-decider(dcdr;n;F) \mmember{} \mforall{}[T:Type]. \mforall{}[R:T {}\mrightarrow{} T {}\mrightarrow{} \mBbbP{}].
((\mforall{}x,y:T. Dec(R[x;y]))
{}\mRightarrow{} (\mforall{}n:\mBbbN{}. \mforall{}F:(\mBbbN{}n {}\mrightarrow{} \mBbbB{}) {}\mrightarrow{} T.
Dec(\mexists{}f,g:\mBbbN{}n {}\mrightarrow{} \mBbbB{}. R[F f;F g])))
By
Latex:
(Subst' \mlambda{}dcdr,n,F. finite-cantor-decider(dcdr;n;F) \msim{} TERMOF\{decidable-finite-cantor-ext:o, \mbackslash{}\mbackslash{}v:l, i:\000Cl\} 0
THEN Auto
)
Home
Index