Nuprl Lemma : cond-msg-body

{

[hdr:Name].

[T:Type].

[m:Message]. (cond-msg-body(hdr;T;m)

bag(T)) }

{ Proof }

Definitions occuring in Statement : cond-msg-body: cond-msg-body(hdr;typ;m), Message: Message, name: Name, uall:

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

T, universe: Type, bag: bag(T)
Definitions : uall:

[x:A]. B[x], isect:

x:A. B[x], equal: s = t, member: t

T, universe: Type, axiom: Ax, name: Name, Message: Message, cond-msg-body: cond-msg-body(hdr;typ;m), bag: bag(T), list: type List, all:

x:A. B[x], function: x:A

B[x], bool:

, implies: P

Q, union: left + right, unit: Unit, int:

, bnot:

b, assert:

b, band: p

q, name_eq: name_eq(x;y), pi1: fst(t), eq_term: a == b, msg-type: msg-type(msg), bor: p

q, bimplies: p

q, es-ble: e

loc e', es-bless: e <loc e', es-eq-E: e = e', eq_lnk: a = b, eq_id: a = b, not:

A, deq-all-disjoint: deq-all-disjoint(eq;ass;bs), deq-disjoint: deq-disjoint(eq;as;bs), deq-member: deq-member(eq;x;L), q_le: q_le(r;s), q_less: q_less(r;s), qeq: qeq(r;s), eq_atom: eq_atom$n(x;y), eq_type: eq_type(T;T'), bag-null: bag-null(bs), b-exists: (

i<n.P[i])_b, bl-exists: (

x

L.P[x])_b, bl-all: (

x

L.P[x])_b, dcdr-to-bool: [d]

, infix_ap: x f y, apply: f a, grp_blt: a <

b, set_blt: a <

b, null: null(as), eq_atom: x =a y, eq_int: (i =

j), le_int: i

z j, lt_int: i <z j, eq_bool: p =b q, and: P

Q, uiff: uiff(P;Q), product: x:A

B[x], uimplies: b supposing a, btrue: tt, bfalse: ff, or: P

Q, pMsg: pMsg(P.M[P]), mData: mData, void: Void, pair: <a, b>, top: Top, valueall-type: valueall-type(T), subtype_rel: A

r B, subtype: S

T, prop:

, limited-type: LimitedType, less_than: a < b, ge: i

j , le: A

B, strong-subtype: strong-subtype(A;B), fpf: a:A fp-> B[a], eclass: EClass(A[eo; e]), sq_type: SQType(T), guard: {T}, b-union: A

B, tunion:

x:A.B[x], set: {x:A| B[x]} , quotient: x,y:A//B[x; y], rec: rec(x.A[x]), atom: Atom, atom: Atom$n, cand: A c

B, decide: case b of inl(x) => s[x] | inr(y) => t[y], spread: spread def, true: True, false: False, intensional-universe: IType, ifthenelse: if b then t else f fi , decidable: Dec(P), lg-edge: lg-edge(g;a;b), path-goes-thru: x-f*-y thru i, cut-order: a

(X;f) b, collect-event: collect-event(es;X;n;v.num[v];L.P[L];e), same-thread: same-thread(es;p;e;e'), es-r-immediate-pred: es-r-immediate-pred(es;R;e';e), exists:

x:A. B[x], es-fset-loc: i

locs(s), existse-between3:

e

(e1,e2].P[e], existse-between2:

e

[e1,e2].P[e], alle-between2:

e

[e1,e2].P[e], existse-between1:

e

[e1,e2).P[e], alle-between1:

e

[e1,e2).P[e], alle-le:

e

e'.P[e], alle-lt:

e<e'.P[e], existse-le:

e

e'.P[e], existse-before:

e<e'.P[e], es-causle: e c

e', es-le: e

loc e' , es-locl: (e <loc e'), es-causl: (e < e'), cs-precondition: state s may consider v in inning i, cs-archive-blocked: in state s, ws' blocks ws from archiving v in inning i, cs-inning-committable: in state s, inning i could commit v , cs-inning-committed: in state s, inning i has committed v, cs-passed: by state s, a passed inning i without archiving a value, cs-archived: by state s, a archived v in inning i, cs-not-completed: in state s, a has not completed inning i, l_disjoint: l_disjoint(T;l1;l2), fset-closed: (s closed under fs), f-subset: xs

ys, fset-member: a

s, p-outcome: Outcome, i-closed: i-closed(I), i-finite: i-finite(I), sq_exists:

x:{A| B[x]}, q-rel: q-rel(r;x), qless: r < s, qle: r

s, fun-connected: y is f*(x), l_all: (

x

L.P[x]), l_exists: (

x

L. P[x]), squash:

T, prime: prime(a), reducible: reducible(a), inject: Inj(A;B;f), cmp-le: cmp-le(cmp;x;y), l_contains: A

B, l_member: (x

l), grp_lt: a < b, set_lt: a <p b, set_leq: a

b, assoced: a ~ b, divides: b | a, single-bag: {x}, msg-body: msg-body(msg), msg-has-type: msg-has-type(m;T), permutation: permutation(T;L1;L2), inl: inl x , inr: inr x , empty-bag: {}, Unfold: Error :Unfold, CollapseTHEN: Error :CollapseTHEN, MaAuto: Error :MaAuto, sqequal: s ~ t, callbyvalueall: callbyvalueall, natural_number: $n, has-valueall: has-valueall(a), rationals:

, int_nzero:

, es-E-interface: E(X), so_lambda:

x.t[x], Id: Id
Lemmas : Id_wf, Id-has-valueall, tunion_wf, assert-eq_term, rational-has-value, int_nzero_wf, b-union_wf, int-rational, rationals_wf, empty-bag_wf, btrue_wf, bfalse_wf, bor_wf, permutation_wf, bag_wf, msg-has-type_wf, ifthenelse_wf, msg-body_wf, msg-body_wf2, single-bag_wf, decidable__assert, decidable_wf, intensional-universe_wf, unit_wf, false_wf, true_wf, type-valueall-type, bnot_wf, subtype_rel_wf, Message_wf, assert_of_band, and_functionality_wrt_uiff2, eqff_to_assert, assert_functionality_wrt_uiff, bnot_thru_band, assert_of_bor, or_functionality_wrt_uiff, not_wf, not_functionality_wrt_uiff, assert_of_bnot, band_wf, name_eq_wf, eq_term_wf, msg-type_wf, valueall-type_wf, uiff_transitivity, eqtt_to_assert, assert-name_eq, bool_wf, assert_wf, pi1_wf_top, member_wf, name_wf, top_wf

\mforall{}[hdr:Name]. \mforall{}[T:Type]. \mforall{}[m:Message]. (cond-msg-body(hdr;T;m) \mmember{} bag(T)) Date html generated: 2011_08_17-PM-04_00_45 Last ObjectModification: 2011_06_20-PM-01_12_11 Home Index