Nuprl Lemma : callbyvalueall-single-bag-combine3

[F,G,a,b:Top].
  (let x ⟵ [a]
   in let z ⟵ b
      in let y ⟵ ⋃v∈x.G[z;v]
         in F[z;y] let x ⟵ a
                     in let z ⟵ b
                        in let y ⟵ G[z;x] []
                           in F[z;y])


Proof




Definitions occuring in Statement :  bag-combine: x∈bs.f[x] append: as bs cons: [a b] nil: [] callbyvalueall: callbyvalueall uall: [x:A]. B[x] top: Top so_apply: x[s1;s2] sqequal: t
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T nil: [] it: cons: [a b] so_apply: x[s1;s2] bag-combine: x∈bs.f[x] bag-union: bag-union(bbs) concat: concat(ll) bag-map: bag-map(f;bs) so_lambda: λ2x.t[x] so_apply: x[s] callbyvalueall: callbyvalueall evalall: evalall(t) all: x:A. B[x]
Lemmas referenced :  lifting-callbyvalueall-pair map_cons_lemma evalall_nil_lemma reduce_cons_lemma map_nil_lemma reduce_nil_lemma istype-top
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation_alt introduction cut sqequalRule extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality Error :memTop,  hypothesis callbyvalueReduce sqleReflexivity dependent_functionElimination axiomSqEquality inhabitedIsType isect_memberEquality_alt isectIsTypeImplies

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



Date html generated: 2020_05_20-AM-08_03_45
Last ObjectModification: 2020_01_17-AM-07_51_41

Theory : bags


Home Index