Nuprl Lemma : lifting-strict-decide

[F:Base]. ∀[p,q,r:Top].
    (F[case of inl(x) => A[x] inr(x) => B[x];p;q;r] case of inl(x) => F[A[x];p;q;r] inr(x) => F[B[x];p;q;r]) 
  supposing strict4(λx,y,z,w. F[x;y;z;w])


Definitions occuring in Statement :  strict4: strict4(F) uimplies: supposing a uall: [x:A]. B[x] top: Top so_apply: x[s1;s2;s3;s4] so_apply: x[s] lambda: λx.A[x] decide: case of inl(x) => s[x] inr(y) => t[y] base: Base sqequal: t
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a strict4: strict4(F) and: P ∧ Q cand: c∧ B all: x:A. B[x] implies:  Q has-value: (a)↓ prop: squash: T or: P ∨ Q sq_type: SQType(T) guard: {T} uiff: uiff(P;Q) ifthenelse: if then else fi  btrue: tt bfalse: ff
Lemmas referenced :  top_wf equal_wf injection-eta isl_wf bool_cases subtype_base_sq bool_wf bool_subtype_base eqtt_to_assert has-value_wf_base is-exception_wf eqff_to_assert assert_of_bnot strict4_wf base_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalSqle sqleRule thin divergentSqle sqequalHypSubstitution sqequalRule productElimination hypothesis dependent_functionElimination baseApply closedConclusion baseClosed hypothesisEquality independent_functionElimination callbyvalueDecide equalityTransitivity equalitySymmetry unionEquality extract_by_obid lambdaFormation unionElimination sqleReflexivity isectElimination imageElimination axiomSqleEquality decideExceptionCases exceptionSqequal because_Cache instantiate cumulativity independent_isectElimination sqequalAxiom isect_memberEquality

\mforall{}[F:Base].  \mforall{}[p,q,r:Top].
        (F[case  a  of  inl(x)  =>  A[x]  |  inr(x)  =>  B[x];p;q;r]  \msim{}  case  a
          of  inl(x)  =>
          |  inr(x)  =>
    supposing  strict4(\mlambda{}x,y,z,w.  F[x;y;z;w])

Date html generated: 2017_04_14-AM-07_20_51
Last ObjectModification: 2017_02_27-PM-02_54_23

Theory : computation

Home Index