### 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