Nuprl Lemma : lifting-strict-atom_eq2

[F:Base]. ∀[p,q,r:Top].
  ∀[a,b,c,d:Top].  (F[if a=2 then else d;p;q;r] if a=2 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) atom_eq: atomeqn def uimplies: supposing a uall: [x:A]. B[x] top: Top so_apply: x[s1;s2;s3;s4] 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) 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 false: False iff: ⇐⇒ Q not: ¬A rev_implies:  Q prop: squash: T so_apply: x[s1;s2;s3;s4]
Lemmas referenced :  eq_atom_wf2 eqtt_to_assert assert_of_eq_atom2 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 callbyvalueAtomnEq extract_by_obid isectElimination Error :inhabitedIsType,  Error :lambdaFormation_alt,  unionElimination equalityElimination because_Cache independent_isectElimination equalityTransitivity equalitySymmetry atomn_eqReduceTrueSq sqleReflexivity Error :dependent_pairFormation_alt,  Error :equalityIsType2,  promote_hyp instantiate cumulativity voidElimination atomnEquality independent_pairFormation Error :equalityIsType4,  Error :universeIsType,  atomn_eqReduceFalseSq Error :equalityIsType1,  imageElimination axiomSqleEquality atom2_eqExceptionCases exceptionSqequal axiomSqEquality Error :isect_memberEquality_alt,  exceptionAtomeq2

Latex:
\mforall{}[F:Base].  \mforall{}[p,q,r:Top].
    \mforall{}[a,b,c,d:Top].    (F[if  a=2  b  then  c  else  d;p;q;r]  \msim{}  if  a=2  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_14
Last ObjectModification: 2018_09_28-PM-03_31_09

Theory : computation


Home Index