Nuprl Definition : PFan
PFan{i:l}() ==
∀n:ℕ. ∀ss:((𝔹 × 𝔹) List) ⟶ ℙ.
((∀bc:(𝔹 × 𝔹) List. Dec(ss bc))
⇒ (∀bc,bc':(𝔹 × 𝔹) List. (bc ≤ bc' ⇒ (ss bc) ⇒ (ss bc')))
⇒ (∀gh:ℕ ⟶ (𝔹 × 𝔹)
((¬(map(λi.(fst((gh i)));upto(n)) = map(λi.(snd((gh i)));upto(n)) ∈ (𝔹 List)))
⇒ (∃m:ℕ. (ss map(gh;upto(m))))))
⇒ (∃k:ℕ
∀gh:ℕ ⟶ (𝔹 × 𝔹)
((¬(map(λi.(fst((gh i)));upto(n)) = map(λi.(snd((gh i)));upto(n)) ∈ (𝔹 List))) ⇒ (ss map(gh;upto(k))))))
Definitions occuring in Statement :
upto: upto(n),
iseg: l1 ≤ l2,
map: map(f;as),
list: T List,
nat: ℕ,
bool: 𝔹,
decidable: Dec(P),
prop: ℙ,
pi1: fst(t),
pi2: snd(t),
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
not: ¬A,
implies: P ⇒ Q,
apply: f a,
lambda: λx.A[x],
function: x:A ⟶ B[x],
product: x:A × B[x],
equal: s = t ∈ T
Definitions occuring in definition :
prop: ℙ,
decidable: Dec(P),
iseg: l1 ≤ l2,
exists: ∃x:A. B[x],
all: ∀x:A. B[x],
function: x:A ⟶ B[x],
nat: ℕ,
product: x:A × B[x],
implies: P ⇒ Q,
not: ¬A,
equal: s = t ∈ T,
list: T List,
bool: 𝔹,
pi1: fst(t),
lambda: λx.A[x],
pi2: snd(t),
apply: f a,
map: map(f;as),
upto: upto(n)
FDL editor aliases :
PFan
Latex:
PFan\{i:l\}() ==
\mforall{}n:\mBbbN{}. \mforall{}ss:((\mBbbB{} \mtimes{} \mBbbB{}) List) {}\mrightarrow{} \mBbbP{}.
((\mforall{}bc:(\mBbbB{} \mtimes{} \mBbbB{}) List. Dec(ss bc))
{}\mRightarrow{} (\mforall{}bc,bc':(\mBbbB{} \mtimes{} \mBbbB{}) List. (bc \mleq{} bc' {}\mRightarrow{} (ss bc) {}\mRightarrow{} (ss bc')))
{}\mRightarrow{} (\mforall{}gh:\mBbbN{} {}\mrightarrow{} (\mBbbB{} \mtimes{} \mBbbB{})
((\mneg{}(map(\mlambda{}i.(fst((gh i)));upto(n)) = map(\mlambda{}i.(snd((gh i)));upto(n))))
{}\mRightarrow{} (\mexists{}m:\mBbbN{}. (ss map(gh;upto(m))))))
{}\mRightarrow{} (\mexists{}k:\mBbbN{}
\mforall{}gh:\mBbbN{} {}\mrightarrow{} (\mBbbB{} \mtimes{} \mBbbB{})
((\mneg{}(map(\mlambda{}i.(fst((gh i)));upto(n)) = map(\mlambda{}i.(snd((gh i)));upto(n))))
{}\mRightarrow{} (ss map(gh;upto(k))))))
Date html generated:
2016_05_14-PM-04_13_02
Last ObjectModification:
2015_09_22-PM-06_02_26
Theory : fan-theorem
Home
Index