### Nuprl Lemma : not_over_and

`∀[A,B:ℙ].  (Dec(A) `` (¬(A ∧ B) `⇐⇒` (¬A) ∨ (¬B)))`

Proof

Definitions occuring in Statement :  decidable: `Dec(P)` uall: `∀[x:A]. B[x]` prop: `ℙ` iff: `P `⇐⇒` Q` not: `¬A` implies: `P `` Q` or: `P ∨ Q` and: `P ∧ Q`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` implies: `P `` Q` iff: `P `⇐⇒` Q` and: `P ∧ Q` decidable: `Dec(P)` or: `P ∨ Q` guard: `{T}` not: `¬A` false: `False` cand: `A c∧ B` member: `t ∈ T` prop: `ℙ` rev_implies: `P `` Q` uimplies: `b supposing a`
Lemmas referenced :  not_wf or_wf decidable_wf not_over_and_b
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity Error :isect_memberFormation_alt,  lambdaFormation independent_pairFormation cut hypothesis sqequalHypSubstitution unionElimination thin sqequalRule inrFormation independent_functionElimination hypothesisEquality introduction extract_by_obid isectElimination inlFormation productEquality cumulativity voidElimination Error :inhabitedIsType,  Error :universeIsType,  universeEquality independent_isectElimination

Latex:
\mforall{}[A,B:\mBbbP{}].    (Dec(A)  {}\mRightarrow{}  (\mneg{}(A  \mwedge{}  B)  \mLeftarrow{}{}\mRightarrow{}  (\mneg{}A)  \mvee{}  (\mneg{}B)))

Date html generated: 2019_06_20-AM-11_16_09
Last ObjectModification: 2018_09_26-AM-10_24_00

Theory : core_2

Home Index