Nuprl Lemma : consensus-accum-state

{

[V:Type].

[A:Id List].

[L:consensus-event(V;A) List].
(consensus-accum-state(A;L)

j:

fp-> V

b:Id fp->

(

V + Top)) }

{ Proof }

Definitions occuring in Statement : consensus-accum-state: consensus-accum-state(A;L), consensus-event: consensus-event(V;A), fpf: a:A fp-> B[a], Id: Id, uall:

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

T, product: x:A

B[x], union: left + right, list: type List, int:

, universe: Type
Definitions : uall:

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

T, top: Top, consensus-accum-state: consensus-accum-state(A;L), bfalse: ff, so_lambda:

x.t[x], so_lambda:

x y.t[x; y], so_apply: x[s1;s2], so_apply: x[s], prop:

Lemmas : list_accum_wf, fpf_wf, top_wf, fpf-empty_wf, mk_fpf_wf, l_member_wf, consensus-accum_wf, consensus-event_wf, Id_wf

\mforall{}[V:Type]. \mforall{}[A:Id List]. \mforall{}[L:consensus-event(V;A) List]. (consensus-accum-state(A;L) \mmember{} \mBbbZ{} \mtimes{} j:\mBbbZ{} fp-> V \mtimes{} b:Id fp-> \mBbbZ{} \mtimes{} (\mBbbZ{} \mtimes{} V + Top)) Date html generated: 2011_08_16-AM-10_09_32 Last ObjectModification: 2011_06_18-AM-09_02_51 Home Index