Nuprl Lemma : no-uniform-xmiddle

¬(∀[P:ℙ]. (P ∨ P)))


Proof




Definitions occuring in Statement :  uall: [x:A]. B[x] prop: not: ¬A or: P ∨ Q
Definitions unfolded in proof :  not: ¬A implies:  Q member: t ∈ T prop: uall: [x:A]. B[x] so_lambda: λ2x.t[x] or: P ∨ Q so_apply: x[s] subtype_rel: A ⊆B all: x:A. B[x] isl: isl(x) assert: b ifthenelse: if then else fi  btrue: tt false: False bfalse: ff true: True
Lemmas referenced :  uall_wf or_wf not_wf false_wf equal_wf true_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut instantiate lemma_by_obid sqequalHypSubstitution isectElimination thin universeEquality sqequalRule lambdaEquality cumulativity hypothesisEquality hypothesis rename applyEquality equalityTransitivity equalitySymmetry isectEquality unionElimination voidElimination dependent_functionElimination independent_functionElimination natural_numberEquality

Latex:
\mneg{}(\mforall{}[P:\mBbbP{}].  (P  \mvee{}  (\mneg{}P)))



Date html generated: 2016_05_15-PM-03_19_09
Last ObjectModification: 2015_12_27-PM-01_03_35

Theory : general


Home Index