Nuprl Lemma : sq_or_simp
∀[a:ℙ]. ({uiff(a ↓∨ False;↓a)} ∧ {uiff(False ↓∨ a;↓a)} ∧ {uiff(a ↓∨ True;True)} ∧ {uiff(True ↓∨ a;True)})
Proof
Error : references
Latex:
\mforall{}[a:\mBbbP{}]
(\{uiff(a \mdownarrow{}\mvee{} False;\mdownarrow{}a)\} \mwedge{} \{uiff(False \mdownarrow{}\mvee{} a;\mdownarrow{}a)\} \mwedge{} \{uiff(a \mdownarrow{}\mvee{} True;True)\} \mwedge{} \{uiff(True \mdownarrow{}\mvee{} a;True)\})
Date html generated:
2020_05_19-PM-09_35_02
Last ObjectModification:
2017_07_26-PM-01_21_17
Theory : core_2
Home
Index