Nuprl Definition : Wqo
Wqo(T;x,y.R[x; y]) ==
(∀f:ℕ ⟶ T. (↓∃i,j:ℕ. (i < j ∧ R[f i; f j]))) ∧ (∀x:T. R[x; x]) ∧ (∀x,y,z:T. (R[x; y] ⇒ R[y; z] ⇒ R[x; z]))
Definitions occuring in Statement :
nat: ℕ,
less_than: a < b,
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
squash: ↓T,
implies: P ⇒ Q,
and: P ∧ Q,
apply: f a,
function: x:A ⟶ B[x]
Definitions occuring in definition :
function: x:A ⟶ B[x],
squash: ↓T,
exists: ∃x:A. B[x],
nat: ℕ,
less_than: a < b,
apply: f a,
and: P ∧ Q,
all: ∀x:A. B[x],
implies: P ⇒ Q
FDL editor aliases :
Wqo
Latex:
Wqo(T;x,y.R[x; y]) ==
(\mforall{}f:\mBbbN{} {}\mrightarrow{} T. (\mdownarrow{}\mexists{}i,j:\mBbbN{}. (i < j \mwedge{} R[f i; f j])))
\mwedge{} (\mforall{}x:T. R[x; x])
\mwedge{} (\mforall{}x,y,z:T. (R[x; y] {}\mRightarrow{} R[y; z] {}\mRightarrow{} R[x; z]))
Date html generated:
2016_05_13-PM-03_53_06
Last ObjectModification:
2015_09_22-PM-05_45_28
Theory : bar-induction
Home
Index