Nuprl Lemma : eqff_assert_2

[b:Decision]. uiff(b ff ∈ Decision;¬↑b)


Proof




Definitions occuring in Statement :  decision: Decision assert: b bfalse: ff uiff: uiff(P;Q) uall: [x:A]. B[x] not: ¬A equal: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T decision: Decision assert: b bfalse: ff ifthenelse: if then else fi  uiff: uiff(P;Q) and: P ∧ Q uimplies: supposing a not: ¬A implies:  Q false: False isl: isl(x) prop: subtype_rel: A ⊆B top: Top true: True
Lemmas referenced :  btrue_wf bfalse_wf and_wf equal_wf top_wf isl_wf btrue_neq_bfalse true_wf it_wf unit_wf2 not_wf false_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalHypSubstitution unionElimination thin sqequalRule independent_pairFormation lambdaFormation lemma_by_obid hypothesis equalitySymmetry dependent_set_memberEquality equalityTransitivity isectElimination unionEquality hypothesisEquality applyEquality lambdaEquality setElimination rename productElimination setEquality independent_functionElimination voidElimination dependent_functionElimination inlEquality inrEquality isect_memberEquality voidEquality natural_numberEquality because_Cache independent_pairEquality axiomEquality

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



Date html generated: 2016_05_15-PM-01_44_24
Last ObjectModification: 2015_12_27-AM-00_10_37

Theory : basic


Home Index