Nuprl Lemma : not-tree-big
∀[T:Type]. ∀[A:(T List) ⟶ ℙ].
  ((∃k:ℕ. T ~ ℕ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: A ~ B
, 
length: ||as||
, 
list: T 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: P 
⇒ Q
, 
and: P ∧ Q
, 
apply: f a
, 
function: x:A ⟶ B[x]
, 
natural_number: $n
, 
int: ℤ
, 
universe: Type
, 
equal: s = t ∈ T
Definitions unfolded in proof : 
uall: ∀[x:A]. B[x]
, 
implies: P 
⇒ 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: b supposing a
, 
not: ¬A
, 
false: False
, 
tree-big: tree-big(T;A;n)
, 
cand: A 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