Step
*
1
1
of Lemma
fan-realizer_test
.....assertion.....
1. fan-realizer β β[X:(πΉ List) βΆ β]. (tbar(πΉ;X)
β Decidable(X)
β (βk:β. βf:β βΆ πΉ. βn:βk. (X map(f;upto(n)))))
β’ β[X:(πΉ List) βΆ β]. (tbar(πΉ;X)
β Decidable(X)
β (βk:β. βf:β βΆ πΉ. βn:βk. (X map(f;upto(n)))))
BY
{ (UseWitness βfan-realizerβ β
THEN Trivial) }
Latex:
Latex:
.....assertion.....
1. fan-realizer \mmember{} \mforall{}[X:(\mBbbB{} List) {}\mrightarrow{} \mBbbP{}]
(tbar(\mBbbB{};X) {}\mRightarrow{} Decidable(X) {}\mRightarrow{} (\mexists{}k:\mBbbN{}. \mforall{}f:\mBbbN{} {}\mrightarrow{} \mBbbB{}. \mexists{}n:\mBbbN{}k. (X map(f;upto(n)))))
\mvdash{} \mforall{}[X:(\mBbbB{} List) {}\mrightarrow{} \mBbbP{}]. (tbar(\mBbbB{};X) {}\mRightarrow{} Decidable(X) {}\mRightarrow{} (\mexists{}k:\mBbbN{}. \mforall{}f:\mBbbN{} {}\mrightarrow{} \mBbbB{}. \mexists{}n:\mBbbN{}k. (X map(f;upto(n)))))
By
Latex:
(UseWitness \mkleeneopen{}fan-realizer\mkleeneclose{} \mcdot{} THEN Trivial)
Home
Index