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)
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
uimplies: b supposing a,
member: t ∈ T,
all: ∀x:A. B[x],
implies: P ⇒ Q,
prop: ℙ,
so_lambda: λ2x.t[x],
subtype_rel: A ⊆r B,
so_lambda: λ2x y.t[x; y],
so_apply: x[s1;s2],
top: Top,
so_apply: x[s],
es-E-interface: E(X),
guard: {T},
iff: P ⇐⇒ Q,
and: P ∧ Q,
rev_implies: P ⇐ Q,
sq_type: SQType(T),
assert: ↑b,
ifthenelse: if b then t else f fi ,
btrue: tt,
true: True
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:
2016_05_17-AM-06_56_03
Last ObjectModification:
2015_12_29-AM-00_21_40
Theory : event-ordering
Home
Index