Nuprl Lemma : lifting-strict-isaxiom

[F:Base]. ∀[p,q,r:Top].
  ∀[a,b,c:Top].  (F[if Ax then otherwise c;p;q;r] if Ax then F[b;p;q;r] otherwise F[c;p;q;r]) 
  supposing strict4(λx,y,z,w. F[x;y;z;w])


Proof




Definitions occuring in Statement :  strict4: strict4(F) uimplies: supposing a uall: [x:A]. B[x] top: Top so_apply: x[s1;s2;s3;s4] isaxiom: if Ax then otherwise b lambda: λx.A[x] 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)↓ or: P ∨ Q top: Top squash: T prop:
Lemmas referenced :  base_wf strict4_wf top_wf is-exception_wf has-value_wf_base has-value-implies-dec-isaxiom-2
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 callbyvalueIsaxiom lemma_by_obid unionElimination sqleReflexivity lambdaFormation because_Cache isect_memberEquality voidElimination voidEquality imageElimination axiomSqleEquality isaxiomExceptionCases exceptionSqequal isectElimination sqequalAxiom equalityTransitivity equalitySymmetry

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



Date html generated: 2016_05_13-PM-03_41_35
Last ObjectModification: 2016_01_14-PM-07_08_59

Theory : computation


Home Index