### Nuprl Lemma : strict4-decide

`strict4(λx,y,z,w. case x of inl(x) => y[x] | inr(x) => z[x])`

Proof

Definitions occuring in Statement :  strict4: `strict4(F)` so_apply: `x[s]` lambda: `λx.A[x]` decide: `case b of inl(x) => s[x] | inr(y) => t[y]`
Definitions unfolded in proof :  strict4: `strict4(F)` and: `P ∧ Q` all: `∀x:A. B[x]` implies: `P `` Q` has-value: `(a)↓` member: `t ∈ T` uall: `∀[x:A]. B[x]` prop: `ℙ` so_apply: `x[s]` guard: `{T}` or: `P ∨ Q` squash: `↓T`
Lemmas referenced :  top_wf equal_wf has-value_wf_base base_wf is-exception_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity independent_pairFormation lambdaFormation sqequalRule cut callbyvalueDecide sqequalHypSubstitution hypothesis hypothesisEquality equalityTransitivity equalitySymmetry thin unionEquality introduction extract_by_obid unionElimination sqleReflexivity isectElimination dependent_functionElimination independent_functionElimination baseApply closedConclusion baseClosed decideExceptionCases inrFormation because_Cache imageMemberEquality imageElimination exceptionSqequal inlFormation

Latex:
strict4(\mlambda{}x,y,z,w.  case  x  of  inl(x)  =>  y[x]  |  inr(x)  =>  z[x])

Date html generated: 2017_04_14-AM-07_21_50
Last ObjectModification: 2017_02_27-PM-02_55_10

Theory : computation

Home Index