Nuprl Lemma : cWObar_wf

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


Proof




Definitions occuring in Statement :  cWObar: cWObar() cWO-rel: cWO-rel(R) consistent-seq: R-consistent-seq(n) nat: uall: [x:A]. B[x] prop: unit: Unit member: t ∈ T function: x:A ⟶ B[x] union: left right universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T cWObar: cWObar() prop: and: P ∧ Q nat: consistent-seq: R-consistent-seq(n) int_seg: {i..j-} lelt: i ≤ j < k all: x:A. B[x] decidable: Dec(P) or: P ∨ Q iff: ⇐⇒ Q not: ¬A rev_implies:  Q implies:  Q false: False uiff: uiff(P;Q) uimplies: supposing a subtract: m subtype_rel: A ⊆B top: Top le: A ≤ B less_than': less_than'(a;b) true: True
Lemmas referenced :  less_than_wf assert_wf isr_wf unit_wf2 subtract_wf decidable__le false_wf not-le-2 less-iff-le condition-implies-le minus-one-mul zero-add minus-one-mul-top nat_wf minus-add minus-minus add-associates add-swap add-commutes add_functionality_wrt_le add-zero le-add-cancel decidable__lt not-lt-2 add-mul-special zero-mul le-add-cancel-alt and_wf le_wf consistent-seq_wf cWO-rel_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule lambdaEquality productEquality lemma_by_obid sqequalHypSubstitution isectElimination thin natural_numberEquality setElimination rename hypothesisEquality hypothesis cumulativity applyEquality dependent_set_memberEquality independent_pairFormation dependent_functionElimination unionElimination lambdaFormation voidElimination productElimination independent_functionElimination independent_isectElimination addEquality isect_memberEquality voidEquality minusEquality intEquality because_Cache unionEquality axiomEquality equalityTransitivity equalitySymmetry functionEquality universeEquality

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



Date html generated: 2016_05_13-PM-03_52_13
Last ObjectModification: 2015_12_26-AM-10_16_57

Theory : bar-induction


Home Index