Nuprl Lemma : isinl-implies
∀[t:Base]. (t ~ inl outl(t)) supposing ((↑isinl(t)) and (t)↓)
Proof
Definitions occuring in Statement : 
has-value: (a)↓
, 
outl: outl(x)
, 
assert: ↑b
, 
bfalse: ff
, 
btrue: tt
, 
uimplies: b supposing a
, 
uall: ∀[x:A]. B[x]
, 
isinl: isinl def, 
inl: inl x
, 
base: Base
, 
sqequal: s ~ t
Definitions unfolded in proof : 
uall: ∀[x:A]. B[x]
, 
member: t ∈ T
, 
uimplies: b supposing a
, 
has-value: (a)↓
, 
outl: outl(x)
, 
assert: ↑b
, 
ifthenelse: if b then t else f fi 
, 
btrue: tt
, 
implies: P 
⇒ Q
, 
prop: ℙ
, 
bfalse: ff
, 
false: False
, 
top: Top
Lemmas referenced : 
base_wf, 
bfalse_wf, 
top_wf, 
btrue_wf, 
is-exception_wf, 
has-value_wf_base, 
assert_wf, 
false_wf, 
true_wf
Rules used in proof : 
sqequalSubstitution, 
sqequalTransitivity, 
computationStep, 
sqequalReflexivity, 
isect_memberFormation, 
introduction, 
cut, 
thin, 
isinlCases, 
divergentSqle, 
hypothesis, 
because_Cache, 
sqequalRule, 
lambdaFormation, 
lemma_by_obid, 
sqequalHypSubstitution, 
isectElimination, 
sqequalAxiom, 
isect_memberEquality, 
hypothesisEquality, 
voidElimination, 
independent_functionElimination, 
baseClosed, 
voidEquality, 
equalityTransitivity, 
equalitySymmetry
Latex:
\mforall{}[t:Base].  (t  \msim{}  inl  outl(t))  supposing  ((\muparrow{}isinl(t))  and  (t)\mdownarrow{})
Date html generated:
2016_05_13-PM-03_27_42
Last ObjectModification:
2016_01_14-PM-06_43_34
Theory : call!by!value_1
Home
Index