Nuprl Lemma : fan-iff-nwkl!
Fan ⇐⇒ nWKL!
Proof
Definitions occuring in Statement :
nwkl!: nWKL!,
fan: Fan,
iff: P ⇐⇒ Q
Definitions unfolded in proof :
iff: P ⇐⇒ Q,
and: P ∧ Q,
implies: P ⇒ Q,
member: t ∈ T,
prop: ℙ,
rev_implies: P ⇐ Q
Lemmas referenced :
fan-implies-nwkl!-using-PFan,
fan_wf,
nwkl!-implies-fan,
nwkl!_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
independent_pairFormation,
lambdaFormation,
cut,
lemma_by_obid,
sqequalHypSubstitution,
independent_functionElimination,
thin,
hypothesis
Latex:
Fan \mLeftarrow{}{}\mRightarrow{} nWKL!
Date html generated:
2016_05_14-PM-04_14_49
Last ObjectModification:
2015_12_26-PM-07_53_46
Theory : fan-theorem
Home
Index