Nuprl Lemma : ler2_nbr-ilf
[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))))))}
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),
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,
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,
apply: f a,
pair: <a, b>,
product: x:A B[x],
cons: [car / cdr],
nil: [],
list: type List,
natural_number: $n,
int: ,
token: "$token",
equal: s = t
Definitions :
and: P Q
Lemmas :
ler2-ilf
\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))))))\}
Date html generated:
2012_02_20-PM-06_16_04
Last ObjectModification:
2012_02_02-PM-02_43_41
Home
Index