Nuprl Lemma : strict4-decide

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


Definitions occuring in Statement :  strict4: strict4(F) so_apply: x[s] lambda: λx.A[x] decide: case 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:  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

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