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: 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: 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)↓ 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 then else fi  assert: b iff: ⇐⇒ Q rev_implies:  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