Nuprl Lemma : decidable__assert
∀b:𝔹. Dec(↑b)
Proof
Definitions occuring in Statement :
assert: ↑b,
bool: 𝔹,
decidable: Dec(P),
all: ∀x:A. B[x]
Definitions unfolded in proof :
all: ∀x:A. B[x],
member: t ∈ T,
bool: 𝔹,
assert: ↑b,
decidable: Dec(P),
ifthenelse: if b then t else f fi ,
not: ¬A,
or: P ∨ Q,
subtype_rel: A ⊆r B,
unit: Unit,
true: True,
uall: ∀[x:A]. B[x],
prop: ℙ,
implies: P ⇒ Q,
false: False
Lemmas referenced :
subtype_rel_self,
equal-wf-base,
true_wf,
false_wf,
bool_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
lambdaFormation,
introduction,
sqequalHypSubstitution,
unionElimination,
thin,
sqequalRule,
inlEquality,
cut,
hypothesisEquality,
applyEquality,
extract_by_obid,
isectElimination,
intEquality,
baseClosed,
because_Cache,
hypothesis,
functionEquality,
inrEquality,
lambdaEquality,
voidElimination
Latex:
\mforall{}b:\mBbbB{}. Dec(\muparrow{}b)
Date html generated:
2017_04_14-AM-07_14_18
Last ObjectModification:
2017_02_27-PM-02_50_02
Theory : union
Home
Index