Nuprl Lemma : ler2_propose-ilf
[client:Id]. [nodes:bag(Id)]. [uid:Id 
]. [es:EO']. [e:E]. [i:Id]. [k,k1:].
(<i, make-Msg(``ler2 propose``; 
;<k, k1>)> 
ler2_main(client;nodes;uid)(e)
loc(e) 
nodes
<k, i> Prior(ler2_Nbr())?
l.{<0, l>}(e)
((
b1:
((<k, b1> Base(``ler2 propose``; )(e) (
(b1 = (uid loc(e) k)))) (k1 = imax(b1;uid loc(e) k))))
(k Base([choose];)(e) (k1 = (uid loc(e) k)))))
Proof not projected
Definitions occuring in Statement :
ler2_Nbr: ler2_Nbr(),
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),
uall: [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: [],
natural_number: $n,
int: ,
token: "$token",
equal: s = t,
bag-member: x bs,
single-bag: {x},
bag: bag(T)
Definitions :
Id: Id,
not: A,
subtype: S 
T,
top: Top,
bfalse: ff,
eq_atom: x =a y,
atom-deq: AtomDeq,
band: p 
q,
list-deq: list-deq(eq),
name-deq: NameDeq,
ifthenelse: if b then t else f fi ,
uiff: uiff(P;Q),
name_eq: name_eq(x;y),
assert: 
b,
false: False,
guard: {T},
sq_or: a b,
name: Name,
cand: A c B,
so_lambda: 
x.t[x],
all: x:A. B[x],
prop: 
,
true: True,
rev_implies: P Q,
implies: P Q,
member: t T,
exists: x:A. B[x],
or: P Q,
squash: T,
bag-member: x bs,
and: P Q,
classrel: v X(e),
iff: P Q,
uall: [x:A]. B[x],
sq_type: SQType(T),
pi2: snd(t),
pi1: fst(t),
uimplies: b supposing a,
so_apply: x[s]
Lemmas :
atom2_subtype_base,
int_subtype_base,
subtype_base_sq,
pi2_wf,
pi1_wf_top,
assert-name_eq,
Id-valueall-type,
false_wf,
true_wf,
make-Msg-equal,
and_wf,
ler2-ilf,
bag_wf,
event-ordering+_wf,
es-E_wf,
imax_wf,
equal_wf,
not_wf,
base-headers-msg-val_wf,
exists_wf,
or_wf,
squash_wf,
Error :ler2_Nbr_wf,
single-bag_wf,
primed-class-opt_wf,
event-ordering+_inc,
es-loc_wf,
bag-member_wf,
valueall-type_wf,
int-valueall-type,
product-valueall-type,
make-Msg_wf,
Error :ler2_main_wf,
Id_wf,
Message_wf,
classrel_wf
\mforall{}[client:Id]. \mforall{}[nodes:bag(Id)]. \mforall{}[uid:Id {}\mrightarrow{} \mBbbZ{} {}\mrightarrow{} \mBbbZ{}]. \mforall{}[es:EO']. \mforall{}[e:E]. \mforall{}[i:Id]. \mforall{}[k,k1:\mBbbZ{}].
(<i, make-Msg(``ler2 propose``;\mBbbZ{} \mtimes{} \mBbbZ{};<k, k1>)> \mmember{} ler2\_main(client;nodes;uid)(e)
\mLeftarrow{}{}\mRightarrow{} loc(e) \mdownarrow{}\mmember{} nodes
\mwedge{} <k, i> \mmember{} Prior(ler2\_Nbr())?\mlambda{}l.\{ɘ, l>\}(e)
\mwedge{} (\mdownarrow{}(\mexists{}b1:\mBbbZ{}
((<k, b1> \mmember{} Base(``ler2 propose``;\mBbbZ{} \mtimes{} \mBbbZ{})(e) \mwedge{} (\mneg{}(b1 = (uid loc(e) k))))
\mwedge{} (k1 = imax(b1;uid loc(e) k))))
\mvee{} (k \mmember{} Base([choose];\mBbbZ{})(e) \mwedge{} (k1 = (uid loc(e) k)))))
Date html generated:
2012_02_20-PM-06_15_46
Last ObjectModification:
2012_02_02-PM-02_43_35
Home
Index