Nuprl Lemma : limited-omniscience_wf

LPO ∈ ℙ


Proof




Definitions occuring in Statement :  limited-omniscience: LPO prop: member: t ∈ T
Definitions unfolded in proof :  limited-omniscience: LPO member: t ∈ T uall: [x:A]. B[x] so_lambda: λ2x.t[x] so_apply: x[s]
Lemmas referenced :  all_wf nat_wf bool_wf or_wf equal_wf bfalse_wf exists_wf btrue_wf
Rules used in proof :  sqequalSubstitution sqequalRule sqequalReflexivity sqequalTransitivity computationStep cut lemma_by_obid sqequalHypSubstitution isectElimination thin functionEquality hypothesis lambdaEquality applyEquality hypothesisEquality

Latex:
LPO  \mmember{}  \mBbbP{}



Date html generated: 2016_05_15-PM-01_44_35
Last ObjectModification: 2015_12_27-AM-00_10_23

Theory : basic


Home Index