`∀[f,c,d,L:Top].`
`  (map(f;reduce(λx,a. let y,z = x in let u,v = z in case d[y;u;v] of inl(x1) => a | inr(y1) => [c[y;u;v] / a];[];L)) `
`  ~ reduce(λx,a. let y,z = x in let u,v = z in if d[y;u;v] then a else [f c[y;u;v] / a] fi ;[];L))`

Proof

Definitions occuring in Statement :  map: `map(f;as)` reduce: `reduce(f;k;as)` cons: `[a / b]` nil: `[]` ifthenelse: `if b then t else f fi ` uall: `∀[x:A]. B[x]` top: `Top` so_apply: `x[s1;s2;s3]` apply: `f a` lambda: `λx.A[x]` spread: spread def decide: `case b of inl(x) => s[x] | inr(y) => t[y]` sqequal: `s ~ t`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` reduce: `reduce(f;k;as)` so_lambda: `λ2x.t[x]` so_apply: `x[s]` uimplies: `b supposing a` strict1: `strict1(F)` and: `P ∧ Q` all: `∀x:A. B[x]` implies: `P `` Q` map: `map(f;as)` list_ind: list_ind has-value: `(a)↓` prop: `ℙ` or: `P ∨ Q` squash: `↓T` guard: `{T}` so_lambda: `so_lambda(x,y,z.t[x; y; z])` so_apply: `x[s1;s2;s3]` so_lambda: `so_lambda(x,y,z,w.t[x; y; z; w])` so_apply: `x[s1;s2;s3;s4]` top: `Top` strict4: `strict4(F)` so_lambda: `λ2x y.t[x; y]` so_apply: `x[s1;s2]` ifthenelse: `if b then t else f fi ` cons: `[a / b]`
Lemmas referenced :  top_wf map_nil_lemma sqle_wf_base lifting-strict-decide lifting-strict-spread is-exception_wf base_wf has-value_wf_base sqequal-list_ind
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule thin lemma_by_obid sqequalHypSubstitution isectElimination baseApply closedConclusion baseClosed hypothesisEquality independent_isectElimination independent_pairFormation lambdaFormation callbyvalueCallbyvalue hypothesis callbyvalueReduce callbyvalueExceptionCases inlFormation imageMemberEquality imageElimination exceptionSqequal inrFormation isect_memberEquality voidElimination voidEquality sqleRule sqleReflexivity because_Cache dependent_functionElimination sqequalAxiom

Latex:
\mforall{}[f,c,d,L:Top].
(map(f;reduce(\mlambda{}x,a.  let  y,z  =  x
in  let  u,v  =  z
in  case  d[y;u;v]  of  inl(x1)  =>  a  |  inr(y1)  =>  [c[y;u;v]  /  a];[];L))
\msim{}  reduce(\mlambda{}x,a.  let  y,z  =  x  in  let  u,v  =  z  in  if  d[y;u;v]  then  a  else  [f  c[y;u;v]  /  a]  fi  ;[];L))

Date html generated: 2016_05_15-PM-02_08_24
Last ObjectModification: 2016_01_15-PM-10_23_56

Theory : untyped!computation

Home Index