Nuprl Lemma : decidable__bool

Dec(𝔹)


Proof




Definitions occuring in Statement :  bool: 𝔹 decidable: Dec(P)
Definitions unfolded in proof :  decidable: Dec(P) or: P ∨ Q member: t ∈ T prop: uall: [x:A]. B[x]
Lemmas referenced :  btrue_wf not_wf bool_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity inlFormation introduction cut lemma_by_obid hypothesis sqequalHypSubstitution isectElimination thin

Latex:
Dec(\mBbbB{})



Date html generated: 2016_05_14-PM-09_38_30
Last ObjectModification: 2015_12_26-PM-09_49_20

Theory : continuity


Home Index