Nuprl Lemma : no-limited-omniscience
¬LPO
Proof
Definitions occuring in Statement :
limited-omniscience: LPO,
not: ¬A
Definitions unfolded in proof :
exists: ∃x:A. B[x],
so_apply: x[s],
so_lambda: λ2x.t[x],
uall: ∀[x:A]. B[x],
decidable: Dec(P),
prop: ℙ,
false: False,
or: P ∨ Q,
all: ∀x:A. B[x],
limited-omniscience: LPO,
member: t ∈ T,
implies: P ⇒ Q,
not: ¬A
Lemmas referenced :
btrue_neq_bfalse,
equal-wf-T-base,
all_wf,
not_wf,
limited-omniscience_wf,
bool_wf,
nat_wf,
no-weak-limited-omniscience
Rules used in proof :
equalitySymmetry,
equalityTransitivity,
productElimination,
inrFormation,
baseClosed,
applyEquality,
lambdaEquality,
sqequalRule,
isectElimination,
inlFormation,
voidElimination,
functionEquality,
unionElimination,
hypothesisEquality,
dependent_functionElimination,
hypothesis,
thin,
independent_functionElimination,
sqequalHypSubstitution,
lambdaFormation,
sqequalReflexivity,
computationStep,
sqequalTransitivity,
sqequalSubstitution,
extract_by_obid,
introduction,
cut
Latex:
\mneg{}LPO
Date html generated:
2018_07_29-AM-09_29_11
Last ObjectModification:
2018_07_27-PM-04_27_18
Theory : basic
Home
Index