Nuprl Lemma : max1-ilf
(
[es:EO']. [e:E].
v:
. {v 
max_exch_Input()(e) 
v Base([int];)(e) 
(
a:Id. <a, v> Base(``max_exch exchange``;Id 
)(e))})
([A,B:Id]. [es:EO']. [e:E]. [i:Id]. [m:Message].
{<i, m> max_exch_main(A;B)(e)
((loc(e) = A) (loc(e) = B))
(b1:
(b1 Memory-class(
x,state.imax(x;state);loc.{0};max_exch_Input())(e)
(m = make-Msg(``max_exch exchange``;Id ;<loc(e), b1>))))
(b:. <i, b> Base(``max_exch exchange``;Id )(e))})
Proof not projected
Definitions occuring in Statement :
max_exch_main: max_exch_main(A;B),
max_exch_Input: max_exch_Input(),
Memory-class: Memory-class(f;init;X),
make-Msg: make-Msg(hdr;typ;val),
base-headers-msg-val: Base(hdr;typ),
Message: Message,
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,
squash: T,
and: P Q,
lambda: x.A[x],
pair: <a, b>,
product: x:A B[x],
cons: [car / cdr],
nil: [],
natural_number: $n,
int: ,
token: "$token",
equal: s = t,
single-bag: {x}
Definitions :
and: P Q,
uall: [x:A]. B[x],
all: x:A. B[x],
guard: {T},
iff: P Q,
classrel: v X(e),
sq_or: a b,
exists: x:A. B[x],
member: t T,
squash: T,
or: P Q,
prop: 
,
name: Name,
cand: A c B,
implies: P Q,
rev_implies: P Q,
true: True,
so_lambda: 
x.t[x],
bag-member: x bs,
max_exch_int'base: max_exch_int'base(),
max_exch_exchange'base: max_exch_exchange'base(),
max_exch_Input: max_exch_Input(),
let: let,
subtype: S 
T,
top: Top,
label: ...$L... t,
suptype: suptype(S; T),
max_exch_exchange'send: max_exch_exchange'send(),
max_exch_Maximum: max_exch_Maximum(),
max_exch_Exchange: max_exch_Exchange(),
max_exch_main: max_exch_main(A;B),
so_apply: x[s],
rev_uimplies: rev_uimplies(P;Q),
uiff: uiff(P;Q),
uimplies: b supposing a,
pi1: fst(t),
pi2: snd(t)
Lemmas :
classrel_wf,
Message_wf,
base-headers-msg-val_wf,
exists_wf,
Id_wf,
true_wf,
false_wf,
or_wf,
squash_wf,
sq_or_wf,
bag-member_wf,
single-bag_wf,
parallel-class_wf,
max_exch_int'base_wf,
simple-loc-comb-1_wf,
concat-lifting-loc-1_wf,
max_exch_exchange'base_wf,
max_exch_Input_wf,
es-E_wf,
event-ordering+_inc,
event-ordering+_wf,
and_true_l,
exists-elim,
trivial-eq,
sq_or_squash3,
bag-member-single-weak,
parallel-classrel-weak,
simple-loc-comb-1-concat-classrel-weak,
exists-product1,
equal_wf,
es-loc_wf,
product-valueall-type,
Id-valueall-type,
int-valueall-type,
valueall-type_wf,
Memory-class_wf,
imax_wf,
make-Msg_wf,
max_exch_exchange'send_wf,
simple-loc-comb-2_wf,
concat-lifting-loc-2_wf,
max_exch_Maximum_wf,
let_wf,
top_wf,
bag_wf,
eclass_wf2,
class-at_wf,
max_exch_Exchange_wf,
cons-bag_wf,
max_exch_main_wf,
squash_and,
squash_true,
pi1_wf_top,
pi2_wf,
simple-loc-comb-2-concat-classrel-weak,
classrel-at,
bag-member-cons
(\mforall{}[es:EO']. \mforall{}[e:E].
\mforall{}v:\mBbbZ{}
\{v \mmember{} max\_exch\_Input()(e)
\mLeftarrow{}{}\mRightarrow{} v \mmember{} Base([int];\mBbbZ{})(e) \mdownarrow{}\mvee{} (\mexists{}a:Id. <a, v> \mmember{} Base(``max\_exch exchange``;Id \mtimes{} \mBbbZ{})(e))\})
\mwedge{} (\mforall{}[A,B:Id]. \mforall{}[es:EO']. \mforall{}[e:E]. \mforall{}[i:Id]. \mforall{}[m:Message].
\{<i, m> \mmember{} max\_exch\_main(A;B)(e)
\mLeftarrow{}{}\mRightarrow{} ((loc(e) = A) \mdownarrow{}\mvee{} (loc(e) = B))
\mwedge{} (\mdownarrow{}\mexists{}b1:\mBbbZ{}
(b1 \mmember{} Memory-class(\mlambda{}x,state.imax(x;state);\mlambda{}loc.\{0\};max\_exch\_Input())(e)
\mwedge{} (m = make-Msg(``max\_exch exchange``;Id \mtimes{} \mBbbZ{};<loc(e), b1>))))
\mwedge{} (\mdownarrow{}\mexists{}b:\mBbbZ{}. <i, b> \mmember{} Base(``max\_exch exchange``;Id \mtimes{} \mBbbZ{})(e))\})
Date html generated:
2012_02_20-PM-05_18_26
Last ObjectModification:
2012_02_17-PM-03_41_01
Home
Index