Nuprl Lemma : ppcc-problem2
∀[es:EO]. ∀[e:E]. (False) supposing ((↑¬bfirst(e)) and (↑first(e)))
Proof
Definitions occuring in Statement :
es-first: first(e),
es-E: E,
event_ordering: EO,
bnot: ¬bb,
assert: ↑b,
uimplies: b supposing a,
uall: ∀[x:A]. B[x],
false: False
Lemmas :
assert_elim,
es-first_wf2,
bfalse_wf,
and_wf,
equal_wf,
bool_wf,
bnot_wf,
btrue_neq_bfalse,
assert_wf,
es-E_wf,
event_ordering_wf
\mforall{}[es:EO]. \mforall{}[e:E]. (False) supposing ((\muparrow{}\mneg{}\msubb{}first(e)) and (\muparrow{}first(e)))
Date html generated:
2015_07_17-AM-08_41_01
Last ObjectModification:
2015_01_27-PM-02_39_39
Home
Index