### Nuprl Lemma : not-assert

`∀[b:𝔹]. uiff(¬↑b;b = ff)`

Proof

Definitions occuring in Statement :  assert: `↑b` bfalse: `ff` bool: `𝔹` uiff: `uiff(P;Q)` uall: `∀[x:A]. B[x]` not: `¬A` equal: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` uiff: `uiff(P;Q)` and: `P ∧ Q` uimplies: `b supposing a` assert: `↑b` ifthenelse: `if b then t else f fi ` bfalse: `ff` iff: `P `⇐⇒` Q` implies: `P `` Q` not: `¬A` false: `False` prop: `ℙ` rev_implies: `P `` Q`
Lemmas referenced :  iff_imp_equal_bool bfalse_wf assert_wf false_wf not_wf assert_elim btrue_neq_bfalse equal_wf bool_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut independent_pairFormation lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis independent_isectElimination sqequalRule lambdaFormation independent_functionElimination voidElimination addLevel levelHypothesis equalityTransitivity equalitySymmetry lambdaEquality dependent_functionElimination productElimination independent_pairEquality isect_memberEquality axiomEquality because_Cache

Latex:
\mforall{}[b:\mBbbB{}].  uiff(\mneg{}\muparrow{}b;b  =  ff)

Date html generated: 2016_05_15-PM-03_27_11
Last ObjectModification: 2015_12_27-PM-01_08_13

Theory : general

Home Index