Nuprl Lemma : callbyvalueall-single-bag-combine1

[F,a,as:Top].  (let x ⟵ [a] in let y ⟵ ⋃z∈x.map(z;as) in F[y] let x ⟵ in let y ⟵ map(x;as) in F[y])


Proof




Definitions occuring in Statement :  bag-combine: x∈bs.f[x] map: map(f;as) cons: [a b] nil: [] callbyvalueall: callbyvalueall uall: [x:A]. B[x] top: Top so_apply: x[s] sqequal: t
Definitions unfolded in proof :  uall: [x:A]. B[x] so_lambda: λ2x.t[x] member: t ∈ T top: Top so_apply: x[s] empty-bag: {} bag-append: as bs callbyvalueall: callbyvalueall uimplies: supposing a has-valueall: has-valueall(a) implies:  Q has-value: (a)↓ prop:
Lemmas referenced :  has-valueall_wf_base evalall-sqequal cbv_sqequal top_wf map-append-empty bag-combine-unit-left-top callbyvalueall-single
Rules used in proof :  sqequalSubstitution sqequalRule sqequalReflexivity cut lemma_by_obid sqequalHypSubstitution sqequalTransitivity computationStep isectElimination thin isect_memberEquality voidElimination voidEquality hypothesis because_Cache isect_memberFormation introduction sqequalAxiom hypothesisEquality baseApply closedConclusion baseClosed independent_isectElimination lambdaFormation

Latex:
\mforall{}[F,a,as:Top].
    (let  x  \mleftarrow{}{}  [a]
      in  let  y  \mleftarrow{}{}  \mcup{}z\mmember{}x.map(z;as)
            in  F[y]  \msim{}  let  x  \mleftarrow{}{}  a
                                in  let  y  \mleftarrow{}{}  map(x;as)
                                      in  F[y])



Date html generated: 2016_05_15-PM-03_09_23
Last ObjectModification: 2016_01_16-AM-08_33_43

Theory : bags


Home Index