### Nuprl Lemma : strict1-strict4

`∀F:Base. (strict1(F) `` strict4(λx,y,z,w. F[x]))`

Proof

Definitions occuring in Statement :  strict4: `strict4(F)` strict1: `strict1(F)` so_apply: `x[s]` all: `∀x:A. B[x]` implies: `P `` Q` lambda: `λx.A[x]` base: `Base`
Definitions unfolded in proof :  all: `∀x:A. B[x]` implies: `P `` Q` strict1: `strict1(F)` and: `P ∧ Q` strict4: `strict4(F)` cand: `A c∧ B` member: `t ∈ T` so_apply: `x[s]` prop: `ℙ` uall: `∀[x:A]. B[x]` squash: `↓T` or: `P ∨ Q` guard: `{T}`
Lemmas referenced :  is-exception_wf strict1_wf base_wf has-value_wf_base
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation sqequalHypSubstitution productElimination thin independent_pairFormation sqequalRule cut hypothesis dependent_functionElimination hypothesisEquality independent_functionElimination lemma_by_obid isectElimination baseApply closedConclusion baseClosed because_Cache introduction imageElimination imageMemberEquality unionElimination inrFormation inlFormation

Latex:
\mforall{}F:Base.  (strict1(F)  {}\mRightarrow{}  strict4(\mlambda{}x,y,z,w.  F[x]))

Date html generated: 2016_05_13-PM-03_23_49
Last ObjectModification: 2016_01_14-PM-06_45_38

Theory : call!by!value_1

Home Index