Nuprl Lemma : simple-loc-comb-3-concat-es-sv

[Info:Type]. ∀[es:EO+(Info)]. ∀[A,B,C:Type]. ∀[F:Id ─→ A ─→ B ─→ C ─→ bag(Top)]. ∀[X:EClass(A)]. ∀[Y:EClass(B)].
[Z:EClass(C)].
es-sv-class(es;concat-lifting-loc-3(F)|Loc, X, Y, Z|)
supposing (∀i:Id. ∀a:A. ∀b:B. ∀c:C.  (#(F c) ≤ 1)) ∧ es-sv-class(es;X) ∧ es-sv-class(es;Y) ∧ es-sv-class(es;Z)

Proof

Definitions occuring in Statement :  concat-lifting-loc-3: concat-lifting-loc-3(f) simple-loc-comb-3: F|Loc, X, Y, Z| es-sv-class: es-sv-class(es;X) eclass: EClass(A[eo; e]) event-ordering+: EO+(Info) Id: Id uimplies: supposing a uall: [x:A]. B[x] top: Top le: A ≤ B all: x:A. B[x] and: P ∧ Q apply: a function: x:A ─→ B[x] natural_number: \$n universe: Type bag-size: #(bs) bag: bag(T)
Lemmas :  bag-size_wf nat_wf es-E_wf event-ordering+_subtype less_than_wf top_wf simple-loc-comb-3_wf concat-lifting-loc-3_wf eclass_wf event-ordering+_wf all_wf Id_wf le_wf es-sv-class_wf bag_wf bag-size-zero le_weakening bag-combine-empty-left bag_union_empty_lemma bag_size_empty_lemma false_wf single-valued-bag-if-le1 bag-size-one bag-combine-single-left bag-combine_wf single-bag_wf es-loc_wf bag-only_wf2 decidable__lt le_antisymmetry_iff add_functionality_wrt_le add-zero le-add-cancel add-commutes zero-add concat_conv_single_nil_lemma length_of_nil_lemma reduce_cons_lemma reduce_nil_lemma list_ind_cons_lemma list_ind_nil_lemma length_of_cons_lemma

Latex:
\mforall{}[Info:Type].  \mforall{}[es:EO+(Info)].  \mforall{}[A,B,C:Type].  \mforall{}[F:Id  {}\mrightarrow{}  A  {}\mrightarrow{}  B  {}\mrightarrow{}  C  {}\mrightarrow{}  bag(Top)].  \mforall{}[X:EClass(A)].
\mforall{}[Y:EClass(B)].  \mforall{}[Z:EClass(C)].
es-sv-class(es;concat-lifting-loc-3(F)|Loc,  X,  Y,  Z|)
supposing  (\mforall{}i:Id.  \mforall{}a:A.  \mforall{}b:B.  \mforall{}c:C.    (\#(F  i  a  b  c)  \mleq{}  1))
\mwedge{}  es-sv-class(es;X)
\mwedge{}  es-sv-class(es;Y)
\mwedge{}  es-sv-class(es;Z)

Date html generated: 2015_07_22-PM-00_15_49
Last ObjectModification: 2015_01_28-AM-10_47_13

Home Index