Nuprl Lemma : not-tree-big

[T:Type]. ∀[A:(T List) ⟶ ℙ].
  ((∃k:ℕ~ ℕk)
   Decidable(A)
   (∀n:ℕ((¬tree-big(T;upwd-closure(T;A);n))  (∃as:T List. ((||as|| n ∈ ℤ) ∧ (upwd-closure(T;A) as)))))))


Proof




Definitions occuring in Statement :  tree-big: tree-big(T;A;n) upwd-closure: upwd-closure(T;A) dec-predicate: Decidable(X) equipollent: B length: ||as|| list: List int_seg: {i..j-} nat: uall: [x:A]. B[x] prop: all: x:A. B[x] exists: x:A. B[x] not: ¬A implies:  Q and: P ∧ Q apply: a function: x:A ⟶ B[x] natural_number: $n int: universe: Type equal: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] implies:  Q all: x:A. B[x] member: t ∈ T prop: so_lambda: λ2x.t[x] nat: so_apply: x[s] decidable: Dec(P) or: P ∨ Q uiff: uiff(P;Q) and: P ∧ Q uimplies: supposing a not: ¬A false: False tree-big: tree-big(T;A;n) cand: c∧ B
Lemmas referenced :  not_wf tree-big_wf upwd-closure_wf nat_wf dec-predicate_wf list_wf exists_wf equipollent_wf int_seg_wf decidable__exists_length decidable__not decidable__upwd-closure not_over_exists and_wf equal_wf length_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation lambdaFormation cut lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis sqequalRule lambdaEquality natural_numberEquality setElimination rename functionEquality cumulativity universeEquality applyEquality independent_functionElimination because_Cache dependent_functionElimination unionElimination intEquality productElimination independent_isectElimination voidElimination independent_pairFormation

Latex:
\mforall{}[T:Type].  \mforall{}[A:(T  List)  {}\mrightarrow{}  \mBbbP{}].
    ((\mexists{}k:\mBbbN{}.  T  \msim{}  \mBbbN{}k)
    {}\mRightarrow{}  Decidable(A)
    {}\mRightarrow{}  (\mforall{}n:\mBbbN{}
                ((\mneg{}tree-big(T;upwd-closure(T;A);n))
                {}\mRightarrow{}  (\mexists{}as:T  List.  ((||as||  =  n)  \mwedge{}  (\mneg{}(upwd-closure(T;A)  as)))))))



Date html generated: 2016_05_14-PM-04_10_19
Last ObjectModification: 2015_12_26-PM-07_54_21

Theory : fan-theorem


Home Index