### Nuprl Lemma : lifting-strict-less

`∀[F:Base]. ∀[p,q,r:Top].`
`  ∀[a,b,c,d:Top].  (F[if (a) < (b)  then c  else d;p;q;r] ~ if (a) < (b)  then F[c;p;q;r]  else F[d;p;q;r]) `
`  supposing strict4(λx,y,z,w. F[x;y;z;w])`

Proof

Definitions occuring in Statement :  strict4: `strict4(F)` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` top: `Top` so_apply: `x[s1;s2;s3;s4]` less: `if (a) < (b)  then c  else d` lambda: `λx.A[x]` base: `Base` sqequal: `s ~ t`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` uimplies: `b supposing a` strict4: `strict4(F)` and: `P ∧ Q` cand: `A c∧ B` all: `∀x:A. B[x]` implies: `P `` Q` has-value: `(a)↓` bool: `𝔹` unit: `Unit` it: `⋅` btrue: `tt` uiff: `uiff(P;Q)` less_than: `a < b` less_than': `less_than'(a;b)` top: `Top` true: `True` squash: `↓T` not: `¬A` false: `False` bfalse: `ff` exists: `∃x:A. B[x]` or: `P ∨ Q` sq_type: `SQType(T)` guard: `{T}` bnot: `¬bb` ifthenelse: `if b then t else f fi ` assert: `↑b` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` prop: `ℙ` so_apply: `x[s1;s2;s3;s4]`
Lemmas referenced :  lt_int_wf eqtt_to_assert assert_of_lt_int istype-void has-value_wf_base is-exception_wf eqff_to_assert bool_cases_sqequal subtype_base_sq bool_wf bool_subtype_base iff_transitivity assert_wf bnot_wf not_wf less_than_wf iff_weakening_uiff assert_of_bnot strict4_wf top_wf base_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity Error :isect_memberFormation_alt,  introduction cut sqequalSqle sqleRule thin divergentSqle sqequalHypSubstitution sqequalRule productElimination hypothesis dependent_functionElimination baseApply closedConclusion baseClosed hypothesisEquality independent_functionElimination callbyvalueLess extract_by_obid isectElimination Error :inhabitedIsType,  Error :lambdaFormation_alt,  unionElimination equalityElimination because_Cache independent_isectElimination equalityTransitivity equalitySymmetry lessCases axiomSqEquality Error :isect_memberEquality_alt,  Error :universeIsType,  independent_pairFormation voidElimination natural_numberEquality imageMemberEquality imageElimination sqleReflexivity Error :dependent_pairFormation_alt,  Error :equalityIsType2,  promote_hyp instantiate cumulativity Error :equalityIsType1,  axiomSqleEquality lessExceptionCases exceptionSqequal exceptionLess

Latex:
\mforall{}[F:Base].  \mforall{}[p,q,r:Top].
\mforall{}[a,b,c,d:Top].
(F[if  (a)  <  (b)    then  c    else  d;p;q;r]  \msim{}  if  (a)  <  (b)    then  F[c;p;q;r]    else  F[d;p;q;r])
supposing  strict4(\mlambda{}x,y,z,w.  F[x;y;z;w])

Date html generated: 2019_06_20-AM-11_27_10
Last ObjectModification: 2018_09_28-PM-03_23_48

Theory : computation

Home Index