Nuprl Lemma : has-value-try-iff
∀[t,n,B:Base].
uiff((t?n:v.B[v])↓;↓((t)↓ ∧ (t?n:v.B[v] ~ t)) ∨ (∃u:Base. ((t ~ exception(n; u)) ∧ (t?n:v.B[v] ~ B[u]) ∧ (B[u])↓)))
Proof
Definitions occuring in Statement :
has-value: (a)↓,
uiff: uiff(P;Q),
uall: ∀[x:A]. B[x],
so_apply: x[s],
exists: ∃x:A. B[x],
squash: ↓T,
or: P ∨ Q,
and: P ∧ Q,
base: Base,
sqequal: s ~ t
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
uiff: uiff(P;Q),
and: P ∧ Q,
uimplies: b supposing a,
so_lambda: λ2x.t[x],
so_apply: x[s],
squash: ↓T,
prop: ℙ,
has-value: (a)↓,
sq_stable: SqStable(P),
implies: P ⇒ Q,
or: P ∨ Q,
exists: ∃x:A. B[x]
Lemmas referenced :
has-value-try,
has-value_wf_base,
squash_wf,
or_wf,
exists_wf,
base_wf,
sq_stable__has-value
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation,
introduction,
cut,
independent_pairFormation,
extract_by_obid,
sqequalHypSubstitution,
isectElimination,
thin,
hypothesisEquality,
sqequalRule,
baseApply,
closedConclusion,
baseClosed,
independent_isectElimination,
hypothesis,
imageElimination,
imageMemberEquality,
axiomSqleEquality,
productEquality,
sqequalIntensionalEquality,
lambdaEquality,
productElimination,
independent_pairEquality,
isect_memberEquality,
because_Cache,
equalityTransitivity,
equalitySymmetry,
independent_functionElimination,
unionElimination
Latex:
\mforall{}[t,n,B:Base].
uiff((t?n:v.B[v])\mdownarrow{};\mdownarrow{}((t)\mdownarrow{} \mwedge{} (t?n:v.B[v] \msim{} t))
\mvee{} (\mexists{}u:Base. ((t \msim{} exception(n; u)) \mwedge{} (t?n:v.B[v] \msim{} B[u]) \mwedge{} (B[u])\mdownarrow{})))
Date html generated:
2017_02_20-AM-10_46_27
Last ObjectModification:
2017_01_25-PM-07_01_20
Theory : call!by!value_1
Home
Index