Nuprl Lemma : ping-ilf
[locs:bag(Id)]. [p:Id]. [es:EO']. [e:E]. [i:Id]. [m:Message].
{<i, m> 
ping_main(locs;p)(e)
((loc(e) = p)
(
e':{e':E| e' 
loc e }
z:Id
(z Base([start];Id)(e')
(z1:Id
(((((i = z1) (m = make-Msg([ping];Id;loc(e)))) (e = e'))
(((i = z) (m = make-Msg([out];Id;z1))) z1 Base([pong];Id)(e)))
z1 locs)))))
(loc(e) locs (m = make-Msg([pong];Id;loc(e))) i Base([ping];Id)(e))}
Proof not projected
Definitions occuring in Statement :
ping_main: ping_main(locs;p),
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-le: e loc e' ,
es-loc: loc(e),
es-E: E,
Id: Id,
sq_or: a b,
uall: [x:A]. B[x],
guard: {T},
exists: x:A. B[x],
iff: P Q,
squash: T,
and: P Q,
set: {x:A| B[x]} ,
pair: <a, b>,
product: x:A 
B[x],
cons: [car / cdr],
nil: [],
token: "$token",
equal: s = t,
bag-member: x bs,
bag: bag(T)
Definitions :
uall: [x:A]. B[x],
guard: {T},
iff: P Q,
classrel: v X(e),
sq_or: a b,
and: P Q,
squash: T,
exists: x:A. B[x],
bag-member: x bs,
member: t T,
implies: P Q,
rev_implies: P Q,
prop: 
,
name: Name,
true: True,
so_lambda: 
x.t[x],
top: Top,
Id: Id,
ping_main: ping_main(locs;p),
ping_P: ping_P(locs),
ping_Reply: ping_Reply(),
ping_Subs: ping_Subs(locs),
ping_Handler: ping_Handler(),
ping_pong: ping_pong(),
ping_Ping: ping_Ping(),
uiff: uiff(P;Q),
all: x:A. B[x],
ping_Start: ping_Start(),
ping_ping: ping_ping(),
ping_cout: ping_cout(),
ping_Pong: ping_Pong(),
subtype: S 
T,
ifthenelse: if b then t else f fi ,
ping_out: ping_out(),
false: False,
btrue: tt,
bfalse: ff,
cand: A c B,
so_apply: x[s],
uimplies: b supposing a,
pi1: fst(t),
pi2: snd(t),
sq_type: SQType(T),
sq_stable: SqStable(P),
bool: 
,
unit: Unit,
not: 
A,
deq: EqDecider(T),
it: 
Lemmas :
classrel_wf,
Message_wf,
Id_wf,
ping_main_wf,
sq_or_wf,
es-loc_wf,
event-ordering+_inc,
squash_wf,
es-E_wf,
es-le_wf,
base-headers-msg-val_wf,
make-Msg_wf,
Id-valueall-type,
valueall-type_wf,
bag-member_wf,
event-ordering+_wf,
bag_wf,
parallel-class_wf,
class-at_wf,
ping_P_wf,
single-bag_wf,
ping_Reply_wf,
bind-class_wf,
ping_Subs_wf,
ping_Handler_wf,
simple-loc-comb-1_wf,
concat-lifting-loc-1_wf,
ping_pong_wf,
ping_Ping_wf,
false_wf,
iff_transitivity,
parallel-classrel-weak,
sq_or_functionality_wrt_iff,
classrel-at,
and_functionality_wrt_iff,
bag-member-single-weak,
bind-class-rel-weak,
simple-loc-comb-1-concat-classrel-weak,
and_functionality_wrt_uiff3,
squash_functionality_wrt_uiff,
exists_functionality_wrt_iff,
pi1_wf_top,
Error :pi2_wf,
iff_weakening_uiff,
bag-member-map,
send-once-loc-classrel,
squash_and,
and_functionality_wrt_uiff,
sq_or_squash3,
squash_equal,
subtype_base_sq,
atom2_subtype_base,
eo-forward-first2,
squash-classrel,
eo-forward_wf,
member-eo-forward-E,
sq_stable_from_decidable,
decidable__es-le,
eo-forward-base-classrel,
bag-member-ifthenelse,
eo-forward-loc,
ifthenelse_functionality_wrt_iff,
bag-member-empty-weak,
bool_wf,
uiff_transitivity,
assert_wf,
eqtt_to_assert,
assert-deq,
id-deq_wf,
ping_out_wf,
bnot_wf,
not_wf,
eqff_to_assert,
assert_of_bnot,
not_functionality_wrt_uiff,
and_functionality_wrt_uiff2,
squash_squash,
squash-bag-member,
bag-map_wf,
ping_Start_wf,
send-once-loc-class_wf,
ping_ping_wf,
ping_cout_wf,
ping_Pong_wf,
es-first_wf,
ifthenelse_wf,
deq_wf,
empty-bag_wf
\mforall{}[locs:bag(Id)]. \mforall{}[p:Id]. \mforall{}[es:EO']. \mforall{}[e:E]. \mforall{}[i:Id]. \mforall{}[m:Message].
\{<i, m> \mmember{} ping\_main(locs;p)(e)
\mLeftarrow{}{}\mRightarrow{} ((loc(e) = p)
\mwedge{} (\mdownarrow{}\mexists{}e':\{e':E| e' \mleq{}loc e \}
\mexists{}z:Id
(z \mmember{} Base([start];Id)(e')
\mwedge{} (\mexists{}z1:Id
(((((i = z1) \mwedge{} (m = make-Msg([ping];Id;loc(e)))) \mwedge{} (e = e'))
\mdownarrow{}\mvee{} (((i = z) \mwedge{} (m = make-Msg([out];Id;z1))) \mwedge{} z1 \mmember{} Base([pong];Id)(e)))
\mwedge{} z1 \mdownarrow{}\mmember{} locs)))))
\mdownarrow{}\mvee{} (loc(e) \mdownarrow{}\mmember{} locs \mwedge{} (m = make-Msg([pong];Id;loc(e))) \mwedge{} i \mmember{} Base([ping];Id)(e))\}
Date html generated:
2012_02_20-PM-06_21_29
Last ObjectModification:
2012_02_02-PM-02_46_49
Home
Index