Nuprl Lemma : lift-simple-decide-decide1

[X,F,G,M,N:Top].
  (case case of inl(x) => inr F[x]  inr(x) => inl G[x] of inl(a) => M[a] inr(b) => N[b] case X
   of inl(x) =>
   N[F[x]]
   inr(x) =>
   M[G[x]])


Proof




Definitions occuring in Statement :  uall: [x:A]. B[x] top: Top so_apply: x[s] decide: case of inl(x) => s[x] inr(y) => t[y] inr: inr  inl: inl x sqequal: t
Definitions unfolded in proof :  uall: [x:A]. B[x] so_lambda: so_lambda(x,y,z,w.t[x; y; z; w]) member: t ∈ T so_apply: x[s1;s2;s3;s4] so_lambda: λ2x.t[x] top: Top so_apply: x[s] uimplies: supposing a strict4: strict4(F) and: P ∧ Q all: x:A. B[x] implies:  Q has-value: (a)↓ prop: guard: {T} or: P ∨ Q squash: T
Lemmas referenced :  lifting-strict-decide top_wf equal_wf has-value_wf_base base_wf is-exception_wf
Rules used in proof :  sqequalSubstitution sqequalRule cut introduction extract_by_obid sqequalHypSubstitution sqequalTransitivity computationStep sqequalReflexivity isectElimination thin baseClosed isect_memberEquality voidElimination voidEquality independent_isectElimination independent_pairFormation lambdaFormation callbyvalueDecide hypothesis hypothesisEquality equalityTransitivity equalitySymmetry unionEquality unionElimination sqleReflexivity dependent_functionElimination independent_functionElimination baseApply closedConclusion decideExceptionCases inrFormation because_Cache imageMemberEquality imageElimination exceptionSqequal inlFormation isect_memberFormation sqequalAxiom

Latex:
\mforall{}[X,F,G,M,N:Top].
    (case  case  X  of  inl(x)  =>  inr  F[x]    |  inr(x)  =>  inl  G[x]  of  inl(a)  =>  M[a]  |  inr(b)  =>  N[b] 
    \msim{}  case  X  of  inl(x)  =>  N[F[x]]  |  inr(x)  =>  M[G[x]])



Date html generated: 2017_10_01-AM-08_39_33
Last ObjectModification: 2017_07_26-PM-04_27_35

Theory : untyped!computation


Home Index