### Nuprl Lemma : isr-not-isl

`∀x:Top + Top. ((↑isr(x)) `` (isl(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: `P `` Q` union: `left + right` sqequal: `s ~ t`
Definitions unfolded in proof :  all: `∀x:A. B[x]` implies: `P `` Q` uall: `∀[x:A]. B[x]` member: `t ∈ T` uimplies: `b supposing a` isr: `isr(x)` assert: `↑b` ifthenelse: `if b then t else f fi ` bfalse: `ff` isl: `isl(x)` false: `False` btrue: `tt` sq_type: `SQType(T)` guard: `{T}` prop: `ℙ`
Lemmas referenced :  subtype_base_sq bool_subtype_base bfalse_wf assert_wf isr_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{}isr(x))  {}\mRightarrow{}  (isl(x)  \msim{}  ff))

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

Theory : union

Home Index