Nuprl Lemma : wkl!-iff-nwkl!
WKL! ⇐⇒ nWKL!
Proof
Definitions occuring in Statement :
nwkl!: nWKL!,
wkl!: WKL!,
iff: P ⇐⇒ Q
Definitions unfolded in proof :
iff: P ⇐⇒ Q,
and: P ∧ Q,
implies: P ⇒ Q,
member: t ∈ T,
prop: ℙ,
rev_implies: P ⇐ Q,
uall: ∀[x:A]. B[x]
Lemmas referenced :
fan_wf,
fan-iff-wkl!,
fan-iff-nwkl!,
wkl!_wf,
nwkl!_wf,
iff_wf
Rules used in proof :
cut,
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
independent_pairFormation,
lambdaFormation,
hypothesis,
lemma_by_obid,
because_Cache,
addLevel,
sqequalHypSubstitution,
productElimination,
thin,
impliesFunctionality,
independent_functionElimination,
instantiate,
isectElimination
Latex:
WKL! \mLeftarrow{}{}\mRightarrow{} nWKL!
Date html generated:
2016_05_14-PM-04_14_50
Last ObjectModification:
2015_12_26-PM-07_53_48
Theory : fan-theorem
Home
Index