Nuprl Lemma : ifthenelse-as-band-bnot

[b:𝔹]. ∀[x:Top].  (if then ff else fi  bb) ∧b x)


Proof




Definitions occuring in Statement :  band: p ∧b q bnot: ¬bb ifthenelse: if then else fi  bfalse: ff bool: 𝔹 uall: [x:A]. B[x] top: Top sqequal: t
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T all: x:A. B[x] implies:  Q bool: 𝔹 unit: Unit it: btrue: tt uiff: uiff(P;Q) and: P ∧ Q uimplies: supposing a ifthenelse: if then else fi  bnot: ¬bb bfalse: ff band: p ∧b q exists: x:A. B[x] prop: or: P ∨ Q sq_type: SQType(T) guard: {T} assert: b false: False
Lemmas referenced :  bool_wf eqtt_to_assert top_wf eqff_to_assert equal_wf bool_cases_sqequal subtype_base_sq bool_subtype_base assert-bnot
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut hypothesisEquality thin extract_by_obid hypothesis lambdaFormation sqequalHypSubstitution unionElimination equalityElimination isectElimination productElimination independent_isectElimination sqequalRule sqequalAxiom dependent_pairFormation promote_hyp dependent_functionElimination instantiate cumulativity equalityTransitivity equalitySymmetry independent_functionElimination because_Cache voidElimination isect_memberEquality

Latex:
\mforall{}[b:\mBbbB{}].  \mforall{}[x:Top].    (if  b  then  ff  else  x  fi    \msim{}  (\mneg{}\msubb{}b)  \mwedge{}\msubb{}  x)



Date html generated: 2017_10_01-AM-09_11_53
Last ObjectModification: 2017_07_26-PM-04_47_45

Theory : general


Home Index