### Nuprl Lemma : genFAN_wf

`∀[T:ℕ ⟶ Type]`
`  ∀[max:∀i:ℕ. Bounded(T[i])]. ∀[X:n:ℕ ⟶ (i:ℕn ⟶ T[i]) ⟶ ℙ].`
`    ∀[d:∀n:ℕ. ∀s:i:ℕn ⟶ T[i].  Dec(X[n;s])]. (genFAN(max;d) ∈ {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 :  genFAN: `genFAN(max;d)` 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]` so_apply: `x[s]` all: `∀x:A. B[x]` exists: `∃x:A. B[x]` squash: `↓T` member: `t ∈ T` set: `{x:A| B[x]} ` function: `x:A ⟶ B[x]` natural_number: `\$n` universe: `Type`
Definitions unfolded in proof :  lelt: `i ≤ j < k` int_seg: `{i..j-}` sq_exists: `∃x:A [B[x]]` istype: `istype(T)` not: `¬A` false: `False` less_than': `less_than'(a;b)` and: `P ∧ Q` le: `A ≤ B` so_lambda: `λ2x.t[x]` exists: `∃x:A. B[x]` nat: `ℕ` prop: `ℙ` subtype_rel: `A ⊆r B` so_apply: `x[s1;s2]` so_apply: `x[s]` implies: `P `` Q` all: `∀x:A. B[x]` simple_more_general_fan_theorem-ext int_seg_decide: `int_seg_decide(d;i;j)` ifthenelse: `if b then t else f fi ` bar_recursion: bar_recursion genFAN: `genFAN(max;d)` uimplies: `b supposing a` member: `t ∈ T` uall: `∀[x:A]. B[x]`
Lemmas referenced :  istype-universe decidable_wf istype-false int_seg_subtype_nat subtype_rel_dep_function nat_wf squash_wf int_seg_wf bounded-type_wf istype-nat simple_more_general_fan_theorem-ext
Rules used in proof :  isectIsTypeImplies isect_memberEquality_alt axiomEquality instantiate productElimination productIsType setIsType independent_pairFormation independent_isectElimination productEquality universeEquality setElimination natural_numberEquality because_Cache universeIsType extract_by_obid functionIsType isectIsType independent_functionElimination dependent_functionElimination equalityIstype rename sqequalHypSubstitution thin lambdaFormation_alt inhabitedIsType hypothesis equalitySymmetry equalityTransitivity hypothesisEquality isectElimination lambdaEquality_alt applyEquality sqequalRule cut introduction isect_memberFormation_alt sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution

Latex:
\mforall{}[T:\mBbbN{}  {}\mrightarrow{}  Type]
\mforall{}[max:\mforall{}i:\mBbbN{}.  Bounded(T[i])].  \mforall{}[X:n:\mBbbN{}  {}\mrightarrow{}  (i:\mBbbN{}n  {}\mrightarrow{}  T[i])  {}\mrightarrow{}  \mBbbP{}].
\mforall{}[d:\mforall{}n:\mBbbN{}.  \mforall{}s:i:\mBbbN{}n  {}\mrightarrow{}  T[i].    Dec(X[n;s])].  (genFAN(max;d)  \mmember{}  \{k:\mBbbN{}|  \mforall{}f:i:\mBbbN{}  {}\mrightarrow{}  T[i].  \mexists{}n:\mBbbN{}k.  X[n;f]\}  \000C)
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_21
Last ObjectModification: 2019_10_07-PM-04_41_41

Theory : bar-induction

Home Index