### Nuprl Lemma : simple_more_general_fan_theorem-ext

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

Proof

Definitions occuring in Statement :  bounded-type: Bounded(T) int_seg: {i..j-} nat: decidable: Dec(P) uimplies: supposing a uall: [x:A]. B[x] prop: so_apply: x[s1;s2] so_apply: x[s] all: x:A. B[x] sq_exists: x:A [B[x]] exists: x:A. B[x] squash: T implies:  Q function: x:A ⟶ B[x] natural_number: \$n universe: Type
Definitions unfolded in proof :  so_apply: x[s] so_lambda: λ2x.t[x] so_apply: x[s1;s2;s3;s4] so_lambda: so_lambda(x,y,z,w.t[x; y; z; w]) decidable__false decidable__implies decidable__not decidable__exists_int_seg any: any x decidable__int_equal decidable__all_int_seg basic_bar_induction simple_more_general_fan_theorem prop: rev_implies:  Q iff: ⇐⇒ Q assert: b 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: 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:  Q not: ¬A has-value: (a)↓ genFAN: genFAN(max;d) ifthenelse: if then else fi  seq-normalize: seq-normalize(n;s) bottom: pi2: snd(t) project-seq: project-seq(s) member: t ∈ T
Lemmas referenced :  lifting-strict-int_eq lifting-strict-callbyvalue strict4-decide lifting-strict-decide 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_more_general_fan_theorem decidable__false decidable__implies decidable__not decidable__exists_int_seg decidable__int_equal decidable__all_int_seg 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:\mBbbN{}  {}\mrightarrow{}  Type]
(\mforall{}i:\mBbbN{}.  Bounded(T[i]))
{}\mRightarrow{}  (\mforall{}[X:n:\mBbbN{}  {}\mrightarrow{}  (i:\mBbbN{}n  {}\mrightarrow{}  T[i])  {}\mrightarrow{}  \mBbbP{}]
(\mforall{}n:\mBbbN{}.  \mforall{}s:i:\mBbbN{}n  {}\mrightarrow{}  T[i].    Dec(X[n;s]))  {}\mRightarrow{}  (\mexists{}k:\mBbbN{}  [(\mforall{}f:i:\mBbbN{}  {}\mrightarrow{}  T[i].  \mexists{}n:\mBbbN{}k.  X[n;f])])
supposing  \mforall{}f:i:\mBbbN{}  {}\mrightarrow{}  T[i].  (\mdownarrow{}\mexists{}n:\mBbbN{}.  X[n;f]))
supposing  \mforall{}i:\mBbbN{}.  T[i]

Date html generated: 2019_10_15-AM-10_20_19
Last ObjectModification: 2019_10_07-PM-04_40_56

Theory : bar-induction

Home Index