{ 
A:
'. X:EClass'(A). es:EO'. L1:A 
E List
. L2:(A E) List.
(classrel-list(es;A;X;L1 @ L2;snd(last(L1 @ L2)))
classrel-list(es;A;X;L1;snd(last(L1)))) }
{ Proof }
Definitions occuring in Statement :
classrel-list: classrel-list(es;A;X;L;e),
Message: Message,
eclass: EClass(A[eo; e]),
event-ordering+: EO+(Info),
es-E: E,
append: as @ bs,
pi2: snd(t),
all: x:A. B[x],
implies: P Q,
product: x:A B[x],
list: type List,
universe: Type,
listp: A List,
last: last(L)
Lemmas :
member_append,
length-map,
es-locl_transitivity2,
es-locl_irreflexivity,
length-append,
nat_properties,
map_length,
map_select,
map_functionality,
le_wf,
select_wf,
select_append,
lt_int_wf,
bool_wf,
bool_subtype_base,
btrue_wf,
iff_imp_equal_bool,
iff_functionality_wrt_iff,
iff_weakening_uiff,
assert_of_lt_int,
bfalse_wf,
int_subtype_base,
es-causl_wf,
Id_wf,
es-locl_transitivity1,
es-causl_weakening,
null_wf3,
event_ordering_wf,
length_zero,
subtype_base_sq,
list_subtype_base,
product_subtype_base,
set_subtype_base,
append_nil_sq,
gt_wf,
true_wf,
squash_wf,
rev_implies_wf,
iff_wf,
no_repeats_append_iff,
map_append,
sorted-by-append,
l_all_append,
pi1_wf_top,
pos_length2,
es-E_wf,
append_wf,
assert_wf,
false_wf,
not_wf,
last_wf,
Message_wf,
event-ordering+_inc,
pi2_wf,
classrel-list_wf,
listp_properties,
es-base-E_wf,
subtype_rel_self,
listp_wf,
event-ordering+_wf,
eclass_wf,
intensional-universe_wf,
member_wf,
subtype_rel_wf,
length_wf_nat,
non_neg_length,
length_append,
length_wf1,
top_wf,
eclass_wf3,
eclass_wf2,
bag_wf,
classrel_wf,
es-le_wf,
l_member_wf,
l_all_wf,
es-locl_wf,
sorted-by_wf,
int_seg_wf,
no_repeats_wf,
nat_wf,
uall_wf,
map_wf
\mforall{}A:\mBbbU{}'. \mforall{}X:EClass'(A). \mforall{}es:EO'. \mforall{}L1:A \mtimes{} E List\msupplus{}. \mforall{}L2:(A \mtimes{} E) List.
(classrel-list(es;A;X;L1 @ L2;snd(last(L1 @ L2))) {}\mRightarrow{} classrel-list(es;A;X;L1;snd(last(L1))))
Date html generated:
2011_08_17-PM-06_25_44
Last ObjectModification:
2011_07_26-PM-04_22_09
Home
Index