Nuprl Lemma : isl-not-isr

x:Top Top. ((↑isl(x))  (isr(x) ff))


Proof




Definitions occuring in Statement :  assert: b isr: isr(x) isl: isl(x) bfalse: ff top: Top all: x:A. B[x] implies:  Q union: left right sqequal: t
Definitions unfolded in proof :  all: x:A. B[x] implies:  Q uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a isl: isl(x) assert: b ifthenelse: if then else fi  btrue: tt isr: isr(x) bfalse: ff false: False sq_type: SQType(T) guard: {T} prop:
Lemmas referenced :  subtype_base_sq bool_subtype_base bfalse_wf assert_wf isl_wf top_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut thin instantiate lemma_by_obid sqequalHypSubstitution isectElimination because_Cache independent_isectElimination hypothesis unionElimination sqequalRule voidElimination dependent_functionElimination equalityTransitivity equalitySymmetry independent_functionElimination hypothesisEquality unionEquality

Latex:
\mforall{}x:Top  +  Top.  ((\muparrow{}isl(x))  {}\mRightarrow{}  (isr(x)  \msim{}  ff))



Date html generated: 2016_05_13-PM-03_20_25
Last ObjectModification: 2015_12_26-AM-09_10_53

Theory : union


Home Index