Nuprl Lemma : ler2-ilf
(
[es:EO']. [e:E]. v:
Id. {v 
ler2_config'base()(e) 
v Base([config]; Id)(e)})
([es:EO']. [e:E].
v: Id
{v ler2_Nbr()(e)
L:( Id E) List
(prior-classrel-list(es; Id;ler2_config'base();L;e)
(a:
a1:Id
(<a, a1> Base([config]; Id)(e)
(v
= (ler2_new_conf() <a, a1> es-history-accum(es; Id; Id;<0, loc(e)>;ler2_new_conf();L))))))})
([client:Id]. [nodes:bag(Id)]. [uid:Id 
]. [es:EO']. [e:E]. [i:Id]. [m:Message].
{<i, m> ler2_main(client;nodes;uid)(e)
loc(e) nodes
((a:
a1:Id
(<a, a1> Prior(ler2_Nbr())?
l.{<0, l>}(e)
(b1:
(<a, b1> Base(``ler2 propose``; )(e)
(((b1 = (uid loc(e) a)) (i = client) (m = make-Msg([leader]; Id;<a, loc(e)>)))
((
(b1 = (uid loc(e) a)))
(i = a1)
(m = make-Msg(``ler2 propose``; ;<a, imax(b1;uid loc(e) a)>))))))))
(a:
(a Base([choose];)(e)
(m = make-Msg(``ler2 propose``; ;<a, uid loc(e) a>))
<a, i> Prior(ler2_Nbr())?l.{<0, l>}(e))))})
Proof not projected
Definitions occuring in Statement :
ler2_Nbr: ler2_Nbr(),
ler2_config'base: ler2_config'base(),
es-history-accum: es-history-accum(es;A;B;x;f;L),
prior-classrel-list: prior-classrel-list(es;A;X;L;e),
make-Msg: make-Msg(hdr;typ;val),
base-headers-msg-val: Base(hdr;typ),
Message: Message,
primed-class-opt: Prior(X)?b,
classrel: v X(e),
event-ordering+: EO+(Info),
es-loc: loc(e),
es-E: E,
Id: Id,
imax: imax(a;b),
sq_or: a b,
uall: [x:A]. B[x],
guard: {T},
all: x:A. B[x],
exists: x:A. B[x],
iff: P Q,
not: A,
squash: T,
or: P Q,
and: P Q,
apply: f a,
lambda: x.A[x],
function: x:A B[x],
pair: <a, b>,
product: x:A B[x],
cons: [car / cdr],
nil: [],
list: type List,
natural_number: $n,
int: ,
token: "$token",
equal: s = t,
bag-member: x bs,
single-bag: {x},
bag: bag(T)
Definitions :
not: A,
cand: A c B,
bfalse: ff,
btrue: tt,
false: False,
ler2_choose'base: Error :ler2_choose'base,
ler2_propose'base: Error :ler2_propose'base,
ler2_PrNbr: Error :ler2_PrNbr,
ler2_propose'send: Error :ler2_propose'send,
ler2_leader'send: Error :ler2_leader'send,
ifthenelse: if b then t else f fi ,
let: let,
ler2_ChooseReply: Error :ler2_ChooseReply,
ler2_ProposeReply: Error :ler2_ProposeReply,
ler2_main: Error :ler2_main,
or: P Q,
sq_or: a b,
subtype: S 
T,
top: Top,
pi2: snd(t),
pi1: fst(t),
label: ...$L... t,
ler2_Nbr: Error :ler2_Nbr,
Id: Id,
so_lambda: 
x.t[x],
prop: 
,
exists: x:A. B[x],
ler2_config'base: Error :ler2_config'base,
true: True,
squash: T,
bag-member: x bs,
name: Name,
rev_implies: P Q,
implies: P Q,
member: t T,
classrel: v X(e),
iff: P Q,
guard: {T},
all: x:A. B[x],
uall: [x:A]. B[x],
and: P Q,
unit: Unit,
bool: 
,
uiff: uiff(P;Q),
sq_type: SQType(T),
uimplies: b supposing a,
so_apply: x[s],
it: 
Lemmas :
or_functionality_wrt_iff,
not_functionality_wrt_uiff,
assert_of_bnot,
eqff_to_assert,
bnot_wf,
assert_of_eq_int,
eqtt_to_assert,
assert_wf,
bool_wf,
bag-member-empty-weak,
ifthenelse_functionality_wrt_iff,
bag-member-ifthenelse,
and_functionality_wrt_uiff2,
sq_or_squash,
and_functionality_wrt_uiff3,
simple-loc-comb-2-concat-classrel-weak,
sq_or_functionality_wrt_iff,
parallel-classrel-weak,
classrel-at,
false_wf,
Error :ler2_choose'base_wf,
Error :ler2_propose'base_wf,
Error :ler2_PrNbr_wf,
empty-bag_wf,
Error :ler2_propose'send_wf,
Error :ler2_leader'send_wf,
eq_int_wf,
ifthenelse_wf,
concat-lifting-loc-2_wf,
simple-loc-comb-2_wf,
Error :ler2_ChooseReply_wf,
Error :ler2_ProposeReply_wf,
parallel-class_wf,
class-at_wf,
bag_wf,
imax_wf,
not_wf,
valueall-type_wf,
Id-valueall-type,
int-valueall-type,
product-valueall-type,
make-Msg_wf,
or_wf,
primed-class-opt_wf,
sq_or_wf,
Error :ler2_main_wf,
pi2_wf,
pi1_wf_top,
atom2_subtype_base,
int_subtype_base,
subtype_base_sq,
bag-member-single-weak,
and_functionality_wrt_iff,
exists_functionality_wrt_iff,
squash_functionality_wrt_uiff,
uiff_transitivity,
iff_weakening_uiff,
Accum-classrel-weak,
iff_transitivity,
equal_wf,
bag-member_wf,
single-bag_wf,
Accum-class_wf,
es-loc_wf,
es-history-accum_wf,
Error :ler2_new_conf_wf,
prior-classrel-list_wf,
and_wf,
exists_wf,
squash_wf,
Error :ler2_Nbr_wf,
event-ordering+_wf,
event-ordering+_inc,
es-E_wf,
base-headers-msg-val_wf,
Error :ler2_config'base_wf,
Id_wf,
Message_wf,
classrel_wf
(\mforall{}[es:EO']. \mforall{}[e:E]. \mforall{}v:\mBbbZ{} \mtimes{} Id. \{v \mmember{} ler2\_config'base()(e) \mLeftarrow{}{}\mRightarrow{} v \mmember{} Base([config];\mBbbZ{} \mtimes{} Id)(e)\})
\mwedge{} (\mforall{}[es:EO']. \mforall{}[e:E].
\mforall{}v:\mBbbZ{} \mtimes{} Id
\{v \mmember{} ler2\_Nbr()(e)
\mLeftarrow{}{}\mRightarrow{} \mdownarrow{}\mexists{}L:(\mBbbZ{} \mtimes{} Id \mtimes{} E) List
(prior-classrel-list(es;\mBbbZ{} \mtimes{} Id;ler2\_config'base();L;e)
\mwedge{} (\mexists{}a:\mBbbZ{}
\mexists{}a1:Id
(<a, a1> \mmember{} Base([config];\mBbbZ{} \mtimes{} Id)(e)
\mwedge{} (v
= (ler2\_new\_conf() <a, a1>
es-history-accum(es;\mBbbZ{} \mtimes{} Id;\mBbbZ{} \mtimes{} Id;ɘ, loc(e)>ler2\_new\_conf();L))))))\})
\mwedge{} (\mforall{}[client:Id]. \mforall{}[nodes:bag(Id)]. \mforall{}[uid:Id {}\mrightarrow{} \mBbbZ{} {}\mrightarrow{} \mBbbZ{}]. \mforall{}[es:EO']. \mforall{}[e:E]. \mforall{}[i:Id]. \mforall{}[m:Message].
\{<i, m> \mmember{} ler2\_main(client;nodes;uid)(e)
\mLeftarrow{}{}\mRightarrow{} loc(e) \mdownarrow{}\mmember{} nodes
\mwedge{} ((\mexists{}a:\mBbbZ{}
\mexists{}a1:Id
(<a, a1> \mmember{} Prior(ler2\_Nbr())?\mlambda{}l.\{ɘ, l>\}(e)
\mwedge{} (\mexists{}b1:\mBbbZ{}
(<a, b1> \mmember{} Base(``ler2 propose``;\mBbbZ{} \mtimes{} \mBbbZ{})(e)
\mwedge{} (((b1 = (uid loc(e) a))
\mwedge{} (i = client)
\mwedge{} (m = make-Msg([leader];\mBbbZ{} \mtimes{} Id;<a, loc(e)>)))
\mvee{} ((\mneg{}(b1 = (uid loc(e) a)))
\mwedge{} (i = a1)
\mwedge{} (m = make-Msg(``ler2 propose``;\mBbbZ{} \mtimes{} \mBbbZ{};<a, imax(b1;uid loc(e) a)>))))))))
\mdownarrow{}\mvee{} (\mexists{}a:\mBbbZ{}
(a \mmember{} Base([choose];\mBbbZ{})(e)
\mwedge{} (m = make-Msg(``ler2 propose``;\mBbbZ{} \mtimes{} \mBbbZ{};<a, uid loc(e) a>))
\mwedge{} <a, i> \mmember{} Prior(ler2\_Nbr())?\mlambda{}l.\{ɘ, l>\}(e))))\})
Date html generated:
2012_02_20-PM-06_15_24
Last ObjectModification:
2012_02_02-PM-02_43_24
Home
Index