### Nuprl Lemma : consistent-seq_wf

`∀[T:Type]. ∀[R:n:ℕ ⟶ (ℕn ⟶ T) ⟶ T ⟶ ℙ]. ∀[n:ℕ].  (R-consistent-seq(n) ∈ Type)`

Proof

Definitions occuring in Statement :  consistent-seq: `R-consistent-seq(n)` int_seg: `{i..j-}` nat: `ℕ` uall: `∀[x:A]. B[x]` prop: `ℙ` member: `t ∈ T` function: `x:A ⟶ B[x]` natural_number: `\$n` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` consistent-seq: `R-consistent-seq(n)` nat: `ℕ` so_lambda: `λ2x.t[x]` subtype_rel: `A ⊆r B` uimplies: `b supposing a` le: `A ≤ B` and: `P ∧ Q` less_than': `less_than'(a;b)` false: `False` not: `¬A` implies: `P `` Q` prop: `ℙ` so_apply: `x[s]` int_seg: `{i..j-}` lelt: `i ≤ j < k` all: `∀x:A. B[x]` guard: `{T}`
Lemmas referenced :  int_seg_wf all_wf int_seg_subtype_nat false_wf subtype_rel_dep_function subtype_rel_sets and_wf le_wf less_than_wf less_than_transitivity2 le_weakening2 nat_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule setEquality functionEquality lemma_by_obid sqequalHypSubstitution isectElimination thin natural_numberEquality setElimination rename hypothesisEquality hypothesis cumulativity because_Cache lambdaEquality applyEquality independent_isectElimination independent_pairFormation lambdaFormation intEquality productElimination dependent_functionElimination axiomEquality equalityTransitivity equalitySymmetry isect_memberEquality universeEquality

Latex:
\mforall{}[T:Type].  \mforall{}[R:n:\mBbbN{}  {}\mrightarrow{}  (\mBbbN{}n  {}\mrightarrow{}  T)  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[n:\mBbbN{}].    (R-consistent-seq(n)  \mmember{}  Type)

Date html generated: 2016_05_13-PM-03_48_45
Last ObjectModification: 2015_12_26-AM-10_18_09

Theory : bar-induction

Home Index