{ 
[T:Type]. [eo:EO']. [e:E]. [e':E]. [v:T]. [hdrs:Name].
uiff(v 
Base(hdrs;T)(e');v Base(hdrs;T)(e')) }
{ Proof }
Definitions occuring in Statement :
base-headers-msg-val: Base(hdr;typ),
Message: Message,
classrel: v X(e),
eo-forward: eo.e,
event-ordering+: EO+(Info),
es-E: E,
name: Name,
uiff: uiff(P;Q),
uall: [x:A]. B[x],
universe: Type
Lemmas :
eo-forward-info,
assert-eq_term,
mData_wf,
rational-has-value,
int_nzero_wf,
b-union_wf,
rationals_wf,
int-rational,
btrue_wf,
bfalse_wf,
tunion_wf,
Id-has-valueall,
Id_wf,
base-headers-msg-val_wf,
classrel_wf,
Message_wf,
eo-forward_wf,
uiff_wf,
event-ordering+_wf,
event-ordering+_inc,
es-E_wf,
name_wf,
member_wf,
subtype_rel_wf,
l_member_wf,
bag_wf,
true_wf,
bag_qinc,
eclass_wf,
es-interface-top,
intensional-universe_wf,
eo-forward-E-subtype,
sq_stable__classrel,
bool_cases,
bool_wf,
subtype_base_sq,
bool_subtype_base,
assert_wf,
uiff_transitivity,
eqtt_to_assert,
assert_of_band,
and_functionality_wrt_uiff2,
assert-name_eq,
not_wf,
eqff_to_assert,
assert_functionality_wrt_uiff,
bnot_thru_band,
assert_of_bor,
or_functionality_wrt_uiff,
assert_of_bnot,
not_functionality_wrt_uiff,
band_wf,
name_eq_wf,
pi1_wf_top,
top_wf,
es-info_wf,
eq_term_wf,
msg-type_wf,
es-base-E_wf,
subtype_rel_self,
valueall-type_wf,
event_ordering_wf,
subtype_rel_record+,
subtype_rel_function,
type-valueall-type,
decidable_wf,
decidable__assert,
bor_wf,
bnot_wf,
bag-member-single,
msg-body_wf2,
false_wf,
ifthenelse_wf,
msg-has-type_wf,
bag-member-empty-iff
\mforall{}[T:Type]. \mforall{}[eo:EO']. \mforall{}[e:E]. \mforall{}[e':E]. \mforall{}[v:T]. \mforall{}[hdrs:Name].
uiff(v \mmember{} Base(hdrs;T)(e');v \mmember{} Base(hdrs;T)(e'))
Date html generated:
2011_08_17-PM-04_02_26
Last ObjectModification:
2011_07_27-AM-11_12_15
Home
Index