Nuprl Lemma : classrel-multi-list-prefix

es:EO'

[n1:

].

[n2:{m:

| m

n1 } ].

[A:{n1..n2

}

'].

[Xs:k:{n1..n2

}

EClass'(A k)].

L1:n:{n1..n2

}

A n

E List

.

L2:(n:{n1..n2

}

A n

E) List.
(classrel-multi-list(es;A;Xs;L1 @ L2;snd(snd(last(L1 @ L2)));n1;n2)

classrel-multi-list(es;A;Xs;L1;snd(snd(last(L1)));n1;n2))

Proof not projected

Definitions occuring in Statement : classrel-multi-list: classrel-multi-list(es;A;Xs;L;e;n1;n2), Message: Message, eclass: EClass(A[eo; e]), event-ordering+: EO+(Info), es-E: E, append: as @ bs, int_seg: {i..j

}, uall:

[x:A]. B[x], pi2: snd(t), ge: i

j , all:

x:A. B[x], implies: P

Q, set: {x:A| B[x]} , apply: f a, function: x:A

B[x], product: x:A

B[x], list: type List, int:

, universe: Type, listp: A List

, last: last(L)
Definitions : all:

x:A. B[x], uall:

[x:A]. B[x], ge: i

j , int_seg: {i..j

}, eclass: EClass(A[eo; e]), implies: P

Q, classrel-multi-list: classrel-multi-list(es;A;Xs;L;e;n1;n2), and: P

Q, iff: P

Q, exists:

x:A. B[x], member: t

T, top: Top, subtype: S

T, so_lambda:

x.t[x], rev_implies: P

Q, prop:

, lelt: i

j < k, pi2: snd(t), pi1: fst(t), so_apply: x[s], squash:

T, true: True, not:

A, es-le: e

loc e' , last: last(L), or: P

Q, assert:

b, le: A

B, nat:

, false: False, ifthenelse: if b then t else f fi , btrue: tt, bfalse: ff, gt: i > j, l_member: (x

l), cand: A c

B, listp: A List

, uimplies: b supposing a, uiff: uiff(P;Q), sorted-by: sorted-by(R;L), sq_type: SQType(T), guard: {T}
Lemmas : no_repeats_witness, map_wf, pi2_wf, pi1_wf_top, es-le_wf, last_wf, classrel_wf, int_seg_wf, le_wf, not_wf, l_member_wf, es-E_wf, event-ordering+_inc, Message_wf, listp_wf, event-ordering+_wf, bag_wf, ge_wf, listp_properties, pos_length2, append_wf, length_wf1, non_neg_length, length_wf_nat, top_wf, length_append, classrel-multi-list_wf, l_all_append, sorted-by-append, es-locl_wf, no_repeats_append_iff, no_repeats_wf, squash_wf, true_wf, map_append, length_zero, append_nil_sq, event_ordering_wf, assert_wf, null_wf3, select_wf, nat_wf, subtype_base_sq, bool_subtype_base, iff_imp_equal_bool, lt_int_wf, btrue_wf, iff_functionality_wrt_iff, iff_weakening_uiff, assert_of_lt_int, bfalse_wf, false_wf, int_subtype_base, es-locl_transitivity1, select_append, map_functionality, map_length, map_select, length-append, nat_properties, es-locl_transitivity2, es-locl_irreflexivity, member_append, length-map

\mforall{}es:EO' \mforall{}[n1:\mBbbZ{}]. \mforall{}[n2:\{m:\mBbbZ{}| m \mgeq{} n1 \} ]. \mforall{}[A:\{n1..n2\msupminus{}\} {}\mrightarrow{} \mBbbU{}']. \mforall{}[Xs:k:\{n1..n2\msupminus{}\} {}\mrightarrow{} EClass'(A k)]. \mforall{}L1:n:\{n1..n2\msupminus{}\} \mtimes{} A n \mtimes{} E List\msupplus{}. \mforall{}L2:(n:\{n1..n2\msupminus{}\} \mtimes{} A n \mtimes{} E) List. (classrel-multi-list(es;A;Xs;L1 @ L2;snd(snd(last(L1 @ L2)));n1;n2) {}\mRightarrow{} classrel-multi-list(es;A;Xs;L1;snd(snd(last(L1)));n1;n2)) Date html generated: 2011_10_20-PM-03_45_38 Last ObjectModification: 2011_08_18-PM-06_16_24 Home Index