Nuprl Lemma : mem_test_inc_max
es:EO'. e1,e2:E. n1,n2:
.
((
n,s:. e:E. ((e1 <loc e) 
e 
loc e2 n 
mem_test_int'base()(e) s mem_test_Maximum()(pred(e)) (s < n)))
(e1 <loc e2)
n1 mem_test_Maximum()(e1)
n2 mem_test_Maximum()(e2)
(n1 < n2))
Proof not projected
Definitions occuring in Statement :
mem_test_Maximum: mem_test_Maximum(),
mem_test_int'base: mem_test_int'base(),
Message: Message,
classrel: v X(e),
event-ordering+: EO+(Info),
es-le: e loc e' ,
es-locl: (e <loc e'),
es-pred: pred(e),
es-E: E,
all: x:A. B[x],
exists: x:A. B[x],
implies: P Q,
and: P Q,
less_than: a < b,
int:
Definitions :
all: x:A. B[x],
implies: P Q,
exists: x:A. B[x],
and: P Q,
mem_test_int'base: mem_test_int'base(),
imax: imax(a;b),
prop: 
,
trans: Trans(T;x,y.E[x; y]),
not: 
A,
member: t T,
so_lambda: 
x.t[x],
cand: A c B,
ifthenelse: if b then t else f fi ,
btrue: tt,
assert: 
b,
bfalse: ff,
name: Name,
mem_test_Maximum: mem_test_Maximum(),
uall: [x:A]. B[x],
so_apply: x[s1;s2],
bool: 
,
unit: Unit,
uimplies: b supposing a,
le: A B,
uiff: uiff(P;Q),
false: False,
guard: {T},
sq_type: SQType(T),
so_apply: x[s],
it: 
,
subtype: S 
T
Lemmas :
State-comb-progress,
Message_wf,
imax_wf,
single-bag_wf,
Id_wf,
mem_test_int'base_wf,
decidable__lt,
less_than_wf,
sq_stable_from_decidable,
le_int_wf,
bool_wf,
uiff_transitivity,
equal_wf,
assert_wf,
le_wf,
eqtt_to_assert,
assert_of_le_int,
lt_int_wf,
bnot_wf,
eqff_to_assert,
assert_functionality_wrt_uiff,
bnot_of_le_int,
assert_of_lt_int,
not_wf,
classrel_wf,
State-comb_wf,
es-pred_wf,
event-ordering+_inc,
subtype_base_sq,
bool_subtype_base,
false_wf,
es-le_wf,
es-locl_wf,
single-valued-classrel-base,
single-valued-bag-single,
exists_wf,
mem_test_Maximum_wf,
es-E_wf,
event-ordering+_wf,
es-locl-first
\mforall{}es:EO'. \mforall{}e1,e2:E. \mforall{}n1,n2:\mBbbZ{}.
((\mexists{}n,s:\mBbbZ{}
\mexists{}e:E
((e1 <loc e)
\mwedge{} e \mleq{}loc e2
\mwedge{} n \mmember{} mem\_test\_int'base()(e)
\mwedge{} s \mmember{} mem\_test\_Maximum()(pred(e))
\mwedge{} (s < n)))
{}\mRightarrow{} (e1 <loc e2)
{}\mRightarrow{} n1 \mmember{} mem\_test\_Maximum()(e1)
{}\mRightarrow{} n2 \mmember{} mem\_test\_Maximum()(e2)
{}\mRightarrow{} (n1 < n2))
Date html generated:
2012_02_20-PM-05_12_11
Last ObjectModification:
2012_02_17-PM-06_29_54
Home
Index