Nuprl Lemma : ifthenelse-wf
∀[b:𝔹]. ∀[A:Type]. ∀[p:⋂v:↑b. A]. ∀[q:⋂v:¬↑b. A]. (if b then p else q fi ∈ A)
Proof
Definitions occuring in Statement :
assert: ↑b,
ifthenelse: if b then t else f fi ,
bool: 𝔹,
uall: ∀[x:A]. B[x],
not: ¬A,
member: t ∈ T,
isect: ⋂x:A. B[x],
universe: Type
Definitions unfolded in proof :
member: t ∈ T,
uall: ∀[x:A]. B[x],
prop: ℙ,
bool: 𝔹,
ifthenelse: if b then t else f fi ,
assert: ↑b,
true: True,
implies: P ⇒ Q,
not: ¬A
Lemmas referenced :
not_wf,
assert_wf,
bool_wf,
false_wf
Rules used in proof :
Error :isectIsType,
Error :universeIsType,
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
cut,
introduction,
extract_by_obid,
sqequalHypSubstitution,
isectElimination,
thin,
hypothesisEquality,
hypothesis,
isectEquality,
because_Cache,
universeEquality,
Error :isect_memberFormation_alt,
sqequalRule,
axiomEquality,
equalityTransitivity,
equalitySymmetry,
isect_memberEquality,
unionElimination,
natural_numberEquality,
lemma_by_obid,
lambdaEquality
Latex:
\mforall{}[b:\mBbbB{}]. \mforall{}[A:Type]. \mforall{}[p:\mcap{}v:\muparrow{}b. A]. \mforall{}[q:\mcap{}v:\mneg{}\muparrow{}b. A]. (if b then p else q fi \mmember{} A)
Date html generated:
2019_06_20-AM-11_30_58
Last ObjectModification:
2018_09_26-AM-11_29_27
Theory : bool_1
Home
Index