Nuprl Definition : infinite-tree
infinite-tree(A) == (∀as,bs:𝔹 List. (as ≤ bs ⇒ (A bs) ⇒ (A as))) ∧ (∀n:ℕ. ∃as:𝔹 List. ((||as|| = n ∈ ℤ) ∧ (A as)))
Definitions occuring in Statement :
iseg: l1 ≤ l2,
length: ||as||,
list: T List,
nat: ℕ,
bool: 𝔹,
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
implies: P ⇒ Q,
and: P ∧ Q,
apply: f a,
int: ℤ,
equal: s = t ∈ T
Definitions occuring in definition :
iseg: l1 ≤ l2,
implies: P ⇒ Q,
all: ∀x:A. B[x],
nat: ℕ,
exists: ∃x:A. B[x],
list: T List,
bool: 𝔹,
and: P ∧ Q,
equal: s = t ∈ T,
int: ℤ,
length: ||as||,
apply: f a
FDL editor aliases :
infinite-tree
Latex:
infinite-tree(A) ==
(\mforall{}as,bs:\mBbbB{} List. (as \mleq{} bs {}\mRightarrow{} (A bs) {}\mRightarrow{} (A as))) \mwedge{} (\mforall{}n:\mBbbN{}. \mexists{}as:\mBbbB{} List. ((||as|| = n) \mwedge{} (A as)))
Date html generated:
2016_05_14-PM-04_12_38
Last ObjectModification:
2015_09_22-PM-06_02_24
Theory : fan-theorem
Home
Index