### Nuprl Lemma : simple_general_fan_theorem-ext

`∀[T:Type]`
`  (Bounded(T)`
`  `` (∀[X:n:ℕ ⟶ (ℕn ⟶ T) ⟶ ℙ]`
`        (∀n:ℕ. ∀s:ℕn ⟶ T.  Dec(X[n;s])) `` (∃k:ℕ [(∀f:ℕ ⟶ T. ∃n:ℕk. X[n;f])]) supposing ∀f:ℕ ⟶ T. (↓∃n:ℕ. X[n;f])))`

Proof

Definitions occuring in Statement :  bounded-type: `Bounded(T)` int_seg: `{i..j-}` nat: `ℕ` decidable: `Dec(P)` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` prop: `ℙ` so_apply: `x[s1;s2]` all: `∀x:A. B[x]` sq_exists: `∃x:A [B[x]]` exists: `∃x:A. B[x]` squash: `↓T` implies: `P `` Q` function: `x:A ⟶ B[x]` natural_number: `\$n` universe: `Type`
Definitions unfolded in proof :  basic_bar_induction simple_general_fan_theorem prop: `ℙ` rev_implies: `P `` Q` iff: `P `⇐⇒` Q` assert: `↑b` ifthenelse: `if b then t else f fi ` bnot: `¬bb` guard: `{T}` sq_type: `SQType(T)` or: `P ∨ Q` exists: `∃x:A. B[x]` bfalse: `ff` squash: `↓T` true: `True` top: `Top` less_than': `less_than'(a;b)` less_than: `a < b` uimplies: `b supposing a` uiff: `uiff(P;Q)` btrue: `tt` it: `⋅` unit: `Unit` bool: `𝔹` all: `∀x:A. B[x]` and: `P ∧ Q` uall: `∀[x:A]. B[x]` false: `False` implies: `P `` Q` not: `¬A` has-value: `(a)↓` seq-normalize: `seq-normalize(n;s)` bottom: `⊥` member: `t ∈ T`
Lemmas referenced :  int-value-type value-type-has-value exception-not-value istype-assert istype-less_than assert_of_bnot iff_weakening_uiff less_than_wf not_wf bnot_wf assert_wf iff_transitivity bool_subtype_base bool_wf subtype_base_sq bool_cases_sqequal eqff_to_assert bottom-sqle strictness-apply istype-void istype-top assert_of_lt_int eqtt_to_assert lt_int_wf is-exception_wf has-value_wf_base exception-not-bottom bottom_diverge simple_general_fan_theorem basic_bar_induction
Rules used in proof :  intEquality lessExceptionCases universeIsType functionIsType cumulativity dependent_functionElimination promote_hyp equalityIstype dependent_pairFormation_alt imageElimination imageMemberEquality natural_numberEquality independent_pairFormation isectIsTypeImplies isect_memberEquality_alt axiomSqEquality isect_memberFormation_alt lessCases independent_isectElimination equalityElimination unionElimination lambdaFormation_alt inhabitedIsType productElimination callbyvalueLess because_Cache isectElimination hypothesisEquality baseClosed closedConclusion baseApply sqleReflexivity exceptionSqequal axiomSqleEquality callbyvalueExceptionCases voidElimination independent_functionElimination callbyvalueReduce callbyvalueCallbyvalue divergentSqle sqequalSqle equalitySymmetry equalityTransitivity sqequalHypSubstitution thin sqequalRule hypothesis extract_by_obid instantiate cut sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution introduction

Latex:
\mforall{}[T:Type]
(Bounded(T)
{}\mRightarrow{}  (\mforall{}[X:n:\mBbbN{}  {}\mrightarrow{}  (\mBbbN{}n  {}\mrightarrow{}  T)  {}\mrightarrow{}  \mBbbP{}]
(\mforall{}n:\mBbbN{}.  \mforall{}s:\mBbbN{}n  {}\mrightarrow{}  T.    Dec(X[n;s]))  {}\mRightarrow{}  (\mexists{}k:\mBbbN{}  [(\mforall{}f:\mBbbN{}  {}\mrightarrow{}  T.  \mexists{}n:\mBbbN{}k.  X[n;f])])
supposing  \mforall{}f:\mBbbN{}  {}\mrightarrow{}  T.  (\mdownarrow{}\mexists{}n:\mBbbN{}.  X[n;f])))

Date html generated: 2019_10_15-AM-10_20_25
Last ObjectModification: 2019_10_07-PM-04_47_50

Theory : bar-induction

Home Index