Nuprl Lemma : Accum-loc-class-single-val

[A,B:

'].

[es:EO'].

X:EClass'(A)

[init:Id

bag(B)].

[f:Id

A

B

B].
(single-valued-classrel(es;X;A)

(

l:Id. (bag-size(init l)

1))

single-valued-classrel(es;Accum-loc-class(f;init;X);B))

Proof not projected

Definitions occuring in Statement : Accum-loc-class: Accum-loc-class(f;init;X), Message: Message, single-valued-classrel: single-valued-classrel(es;X;T), eclass: EClass(A[eo; e]), event-ordering+: EO+(Info), Id: Id, uall:

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

B, all:

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

Q, apply: f a, function: x:A

B[x], natural_number: $n, universe: Type, bag-size: bag-size(bs), bag: bag(T)
Definitions : eclass: EClass(A[eo; e]), single-valued-classrel: single-valued-classrel(es;X;T), all:

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

Q, member: t

T, prop:

, le: A

B, subtype: S

T, top: Top, so_lambda:

x y.t[x; y], not:

A, false: False, uimplies: b supposing a, squash:

T, exists:

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

Q, uiff: uiff(P;Q), uall:

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

, so_apply: x[s1;s2], or: P

Q
Lemmas : Accum-loc-classrel, classrel_wf, Accum-loc-class_wf, es-E_wf, event-ordering+_inc, Id_wf, le_wf, bag-size_wf, nat_wf, single-valued-classrel_wf, Message_wf, bag_wf, event-ordering+_wf, list_accum_wf, es-loc_wf, map_wf, pi1_wf_top, bag-size-zero, bag-member-empty-iff, bag-size-one, bag-member-single, bag-only_wf, prior-classrel-list-unique, length_wf_nat, top_wf, member_wf

\mforall{}[A,B:\mBbbU{}']. \mforall{}[es:EO']. \mforall{}X:EClass'(A) \mforall{}[init:Id {}\mrightarrow{} bag(B)]. \mforall{}[f:Id {}\mrightarrow{} A {}\mrightarrow{} B {}\mrightarrow{} B]. (single-valued-classrel(es;X;A) {}\mRightarrow{} (\mforall{}l:Id. (bag-size(init l) \mleq{} 1)) {}\mRightarrow{} single-valued-classrel(es;Accum-loc-class(f;init;X);B)) Date html generated: 2012_01_23-PM-01_20_21 Last ObjectModification: 2011_10_23-PM-04_23_52 Home Index