Nuprl Lemma : test-rewrite-dcdr
∀[P:ℙ]. ∀d:Dec(P). ((↑[d]b) ∨ (¬↑[d]b))
Proof
Definitions occuring in Statement :
dcdr-to-bool: [d]b,
assert: ↑b,
decidable: Dec(P),
uall: ∀[x:A]. B[x],
prop: ℙ,
all: ∀x:A. B[x],
not: ¬A,
or: P ∨ Q
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
all: ∀x:A. B[x],
decidable: Dec(P),
or: P ∨ Q,
member: t ∈ T,
prop: ℙ,
guard: {T},
iff: P ⇐⇒ Q,
and: P ∧ Q,
rev_implies: P ⇐ Q,
implies: P ⇒ Q,
not: ¬A,
subtype_rel: A ⊆r B,
so_lambda: λ2x.t[x],
so_apply: x[s]
Lemmas referenced :
not_wf,
decidable_wf,
dcdr-to-bool-equivalence,
assert_wf,
dcdr-to-bool_wf,
uall_wf,
all_wf,
or_wf
Rules used in proof :
cut,
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation,
lambdaFormation,
hypothesis,
sqequalHypSubstitution,
unionElimination,
thin,
inlFormation,
lemma_by_obid,
isectElimination,
hypothesisEquality,
sqequalRule,
inrFormation,
universeEquality,
addLevel,
uallFunctionality,
allFunctionality,
orFunctionality,
dependent_functionElimination,
productElimination,
independent_functionElimination,
impliesFunctionality,
instantiate,
equalityTransitivity,
equalitySymmetry,
applyEquality,
lambdaEquality,
cumulativity,
impliesLevelFunctionality,
because_Cache
Latex:
\mforall{}[P:\mBbbP{}]. \mforall{}d:Dec(P). ((\muparrow{}[d]\msubb{}) \mvee{} (\mneg{}\muparrow{}[d]\msubb{}))
Date html generated:
2016_05_15-PM-03_27_42
Last ObjectModification:
2015_12_27-PM-01_08_38
Theory : general
Home
Index