Nuprl Lemma : try-is-exception
∀[t,n,B,m,x:Base].
exception(m; x) ≤ t?n:v.B[v]
supposing ↓((n ∈ Atom2)
∧ (((m ∈ Atom2) ∧ (exception(m; x) ≤ t) ∧ (¬(n = m ∈ Atom2)))
∨ (∃u:Base. ((t ~ exception(n; u)) ∧ (exception(m; x) ≤ B[u])))))
∨ ((t)↓ ∧ (exception(m; x) ≤ n))
Proof
Definitions occuring in Statement :
has-value: (a)↓,
atom: Atom$n,
uimplies: b supposing a,
uall: ∀[x:A]. B[x],
so_apply: x[s],
exists: ∃x:A. B[x],
not: ¬A,
squash: ↓T,
or: P ∨ Q,
and: P ∧ Q,
member: t ∈ T,
base: Base,
sqle: s ≤ t,
sqequal: s ~ t,
equal: s = t ∈ T
Definitions unfolded in proof :
so_apply: x[s],
so_lambda: λ2x.t[x],
prop: ℙ,
exists: ∃x:A. B[x],
and: P ∧ Q,
or: P ∨ Q,
squash: ↓T,
implies: P ⇒ Q,
sq_stable: SqStable(P),
member: t ∈ T,
uimplies: b supposing a,
uall: ∀[x:A]. B[x],
not: ¬A,
false: False,
has-value: (a)↓
Lemmas referenced :
has-value_wf_base,
base_wf,
exists_wf,
not_wf,
sqle_wf_base,
equal-wf-base,
or_wf,
squash_wf,
sq_stable__sqle,
is-exception_wf
Rules used in proof :
sqequalIntensionalEquality,
lambdaEquality,
because_Cache,
atomnEquality,
productEquality,
imageMemberEquality,
productElimination,
unionElimination,
imageElimination,
independent_functionElimination,
hypothesis,
hypothesisEquality,
baseClosed,
closedConclusion,
baseApply,
sqequalRule,
thin,
isectElimination,
sqequalHypSubstitution,
extract_by_obid,
introduction,
cut,
isect_memberFormation,
sqequalReflexivity,
computationStep,
sqequalTransitivity,
sqequalSubstitution,
sqleReflexivity,
sqleRule,
divergentSqle,
atomn_eqReduceFalseSq,
equalitySymmetry,
equalityTransitivity,
atomn_eqReduceTrueSq,
tryReduceValue
Latex:
\mforall{}[t,n,B,m,x:Base].
exception(m; x) \mleq{} t?n:v.B[v]
supposing \mdownarrow{}((n \mmember{} Atom2)
\mwedge{} (((m \mmember{} Atom2) \mwedge{} (exception(m; x) \mleq{} t) \mwedge{} (\mneg{}(n = m)))
\mvee{} (\mexists{}u:Base. ((t \msim{} exception(n; u)) \mwedge{} (exception(m; x) \mleq{} B[u])))))
\mvee{} ((t)\mdownarrow{} \mwedge{} (exception(m; x) \mleq{} n))
Date html generated:
2019_06_20-AM-11_21_52
Last ObjectModification:
2018_10_15-PM-05_09_20
Theory : call!by!value_1
Home
Index