### Nuprl Lemma : lifting-strict-int_eq

`∀[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]` int_eq: `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)` 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` false: `False` iff: `P `⇐⇒` Q` not: `¬A` rev_implies: `P `` Q` prop: `ℙ` squash: `↓T` so_apply: `x[s1;s2;s3;s4]`
Lemmas referenced :  eq_int_wf eqtt_to_assert assert_of_eq_int 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 equal-wf-base 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 callbyvalueIntEq extract_by_obid isectElimination Error :inhabitedIsType,  Error :lambdaFormation_alt,  unionElimination equalityElimination because_Cache independent_isectElimination equalityTransitivity equalitySymmetry int_eqReduceTrueSq sqleReflexivity Error :dependent_pairFormation_alt,  Error :equalityIsType2,  promote_hyp instantiate cumulativity voidElimination intEquality independent_pairFormation Error :equalityIsType4,  Error :universeIsType,  int_eqReduceFalseSq Error :equalityIsType1,  imageElimination axiomSqleEquality int_eqExceptionCases exceptionSqequal axiomSqEquality Error :isect_memberEquality_alt,  exceptionInteq

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_11
Last ObjectModification: 2018_09_28-PM-03_30_36

Theory : computation

Home Index