Nuprl Lemma : filter-image-interface-accum-equal

∀[Info,A1,B1,A2,B2,C:Type]. ∀[X1:EClass(A1)]. ∀[X2:EClass(A2)]. ∀[b1:B1]. ∀[b2:B2]. ∀[acc1:B1 ─→ A1 ─→ B1].

∀[acc2:B2 ─→ A2 ─→ B2]. ∀[F1:B1 ─→ bag(C)]. ∀[F2:B2 ─→ bag(C)].
  (F1[es-interface-accum(acc1;b1;X1)] = F2[es-interface-accum(acc2;b2;X2)] ∈ EClass(C)) supposing
     ((∀a:B1. ∀b:B2.
         (((F1 a) = (F2 b) ∈ bag(C))
         ⇒ (∀es:EO+(Info). ∀e:E.  ((↑e ∈_b X1) ⇒ (↑e ∈_b X1) ⇒ (F1[acc1 a X1(e)] = F2[acc2 b X2(e)] ∈ bag(C)))))) and
     (F1[b1] = F2[b2] ∈ bag(C)) and
     (∀es:EO+(Info). ∀e:E.  (↑e ∈_b X1 ⇐⇒ ↑e ∈_b X2)))

Proof

Definitions occuring in Statement : es-interface-accum: es-interface-accum(f;x;X), es-filter-image: f[X], eclass-val: X(e), in-eclass: e ∈_b X, eclass: EClass(A[eo; e]), event-ordering+: EO+(Info), es-E: E, assert: ↑b, uimplies: b supposing a, uall: ∀[x:A]. B[x], so_apply: x[s], all: ∀x:A. B[x], iff: P ⇐⇒ Q, implies: P ⇒ Q, apply: f a, function: x:A ─→ B[x], universe: Type, equal: s = t ∈ T, bag: bag(T)
Lemmas : all_wf, bag_wf, es-E_wf, event-ordering+_subtype, assert_wf, in-eclass_wf, es-interface-subtype_rel2, top_wf, eclass-val_wf, es-E-interface-property, equal_wf, iff_wf, eclass_wf, event-ordering+_wf, filter-image_functionality, es-interface-accum_wf, is-interface-accum, es-interface-predecessors-equal, es-interface-accum-val, length_wf_nat, es-E-interface_wf, Id_wf, es-loc_wf, es-interface-predecessors_wf, nat_wf, list_accum_wf, assert_elim, subtype_base_sq, bool_wf, bool_subtype_base, list_accum_equality, es-E-interface_functionality, and_wf

Latex:
\mforall{}[Info,A1,B1,A2,B2,C:Type]. \mforall{}[X1:EClass(A1)]. \mforall{}[X2:EClass(A2)]. \mforall{}[b1:B1]. \mforall{}[b2:B2]. \mforall{}[acc1:B1 {}\mrightarrow{} A1 {}\mrightarrow{} B1]. \mforall{}[acc2:B2 {}\mrightarrow{} A2 {}\mrightarrow{} B2]. \mforall{}[F1:B1 {}\mrightarrow{} bag(C)]. \mforall{}[F2:B2 {}\mrightarrow{} bag(C)]. (F1[es-interface-accum(acc1;b1;X1)] = F2[es-interface-accum(acc2;b2;X2)]) supposing ((\mforall{}a:B1. \mforall{}b:B2. (((F1 a) = (F2 b)) {}\mRightarrow{} (\mforall{}es:EO+(Info). \mforall{}e:E. ((\muparrow{}e \mmember{}\msubb{} X1) {}\mRightarrow{} (\muparrow{}e \mmember{}\msubb{} X1) {}\mRightarrow{} (F1[acc1 a X1(e)] = F2[acc2 b X2(e)]))))) and (F1[b1] = F2[b2]) and (\mforall{}es:EO+(Info). \mforall{}e:E. (\muparrow{}e \mmember{}\msubb{} X1 \mLeftarrow{}{}\mRightarrow{} \muparrow{}e \mmember{}\msubb{} X2))) Date html generated: 2015_07_21-PM-03_34_36 Last ObjectModification: 2015_01_27-PM-06_45_54 Home Index