### Nuprl Lemma : bsc-body_wf

`∀[T:Type]. ∀[F:(ℕ ⟶ T) ⟶ ℕ]. ∀[M:n:ℕ ⟶ (ℕn ⟶ T) ⟶ (ℕ ⋃ (ℕ × ℕ))]. ∀[f:ℕ ⟶ T].  (bsc-body(F;M;f) ∈ ℙ)`

Proof

Definitions occuring in Statement :  bsc-body: `bsc-body(F;M;f)` int_seg: `{i..j-}` nat: `ℕ` b-union: `A ⋃ B` uall: `∀[x:A]. B[x]` prop: `ℙ` member: `t ∈ T` function: `x:A ⟶ B[x]` product: `x:A × B[x]` natural_number: `\$n` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` bsc-body: `bsc-body(F;M;f)` prop: `ℙ` and: `P ∧ Q` exists: `∃x:A. B[x]` subtype_rel: `A ⊆r B` nat: `ℕ` uimplies: `b supposing a` le: `A ≤ B` less_than': `less_than'(a;b)` false: `False` not: `¬A` implies: `P `` Q` all: `∀x:A. B[x]` b-union: `A ⋃ B` tunion: `⋃x:A.B[x]` bool: `𝔹` unit: `Unit` ifthenelse: `if b then t else f fi ` pi2: `snd(t)` so_lambda: `λ2x.t[x]` so_apply: `x[s]` sq_type: `SQType(T)` guard: `{T}`
Lemmas referenced :  nat_wf subtype_rel_function int_seg_wf int_seg_subtype_nat istype-false subtype_rel_self equal-wf-base set_subtype_base le_wf istype-int int_subtype_base product_subtype_base isect_wf true_wf false_wf equal_wf istype-universe all_wf istype-nat b-union_wf istype-void subtype_base_sq base_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity Error :isect_memberFormation_alt,  introduction cut sqequalRule productEquality extract_by_obid hypothesis applyEquality hypothesisEquality sqequalHypSubstitution isectElimination thin natural_numberEquality setElimination rename because_Cache independent_isectElimination independent_pairFormation Error :lambdaFormation_alt,  Error :inhabitedIsType,  imageElimination productElimination unionElimination equalityElimination intEquality Error :lambdaEquality_alt,  Error :equalityIstype,  equalityTransitivity equalitySymmetry dependent_functionElimination independent_functionElimination functionEquality isintReduceTrue axiomEquality Error :functionIsType,  Error :universeIsType,  Error :isect_memberEquality_alt,  Error :isectIsTypeImplies,  instantiate universeEquality voidElimination cumulativity

Latex:
\mforall{}[T:Type].  \mforall{}[F:(\mBbbN{}  {}\mrightarrow{}  T)  {}\mrightarrow{}  \mBbbN{}].  \mforall{}[M:n:\mBbbN{}  {}\mrightarrow{}  (\mBbbN{}n  {}\mrightarrow{}  T)  {}\mrightarrow{}  (\mBbbN{}  \mcup{}  (\mBbbN{}  \mtimes{}  \mBbbN{}))].  \mforall{}[f:\mBbbN{}  {}\mrightarrow{}  T].
(bsc-body(F;M;f)  \mmember{}  \mBbbP{})

Date html generated: 2019_06_20-PM-02_50_08
Last ObjectModification: 2019_02_11-AM-11_17_31

Theory : continuity

Home Index