Nuprl Lemma : aa_max_ltree_spec2
t:aa_ltree(
). j:. ((aa_binary_search_tree(t) 
(aa_max_ltree(t) = (inl j ))) 
aa_bst_member_prop(j;t))
Proof
Definitions occuring in Statement :
aa_binary_search_tree: aa_binary_search_tree(t),
aa_bst_member_prop: aa_bst_member_prop(i;t),
aa_max_ltree: aa_max_ltree(t),
aa_ltree: aa_ltree(T),
all: x:A. B[x],
implies: P Q,
and: P Q,
unit: Unit,
inl: inl x ,
union: left + right,
int: ,
equal: s = t
Definitions :
all: x:A. B[x],
aa_ltree: aa_ltree(T),
member: t 
T,
type-monotone: Monotone(T.F[T]),
uall: [x:A]. B[x],
uimplies: b supposing a,
implies: P Q,
and: P Q,
prop: 
,
so_lambda: 
x.t[x],
true: True,
ifthenelse: if b then t else f fi ,
btrue: tt,
isl: isl(x),
assert: 
b,
outl: outl(x),
exists: 
x:A. B[x],
aa_bst_member_prop: aa_bst_member_prop(i;t),
rev_implies: P 
Q,
iff: P Q,
not: 
A,
guard: {T},
or: P 
Q,
so_lambda: so_lambda(x,y,z,w,v.t[x; y; z; w; v]),
so_apply: x[s],
aa_max_ltree: aa_max_ltree(t),
aa_max_w_unit: aa_max_w_unit(u1;u2),
sq_type: SQType(T),
uiff: uiff(P;Q),
bfalse: ff,
imax: imax(a;b),
aa_binary_search_tree: aa_binary_search_tree(t),
bool: 
,
unit: Unit,
so_apply: x[s1;s2;s3;s4;s5],
it: 
Lemmas :
unit_wf2,
subtype_rel_sum,
subtype_rel_simple_product,
aa_ltree-induction,
all_wf,
aa_binary_search_tree_wf,
aa_max_ltree_wf,
aa_bst_member_prop_wf,
aa_ltree_wf,
aa_lt_leaf_wf,
aa_lt_node_wf,
isl_wf,
assert_wf,
outl_wf,
subtype_rel_self,
unit_subtype_base,
int_subtype_base,
union_subtype_base,
subtype_base_sq,
equal_wf,
assert_of_lt_int,
bnot_of_le_int,
assert_functionality_wrt_uiff,
eqff_to_assert,
bnot_wf,
less_than_wf,
lt_int_wf,
assert_of_le_int,
eqtt_to_assert,
le_wf,
uiff_transitivity,
bool_subtype_base,
bool_wf,
le_int_wf,
bool_cases,
and_wf,
imax_wf,
assert_of_bnot,
iff_weakening_uiff,
not_wf,
iff_transitivity,
assert_of_eq_int,
eq_int_wf,
or_wf,
false_wf,
aa_ltree_ind_wf
\mforall{}t:aa\_ltree(\mBbbZ{}). \mforall{}j:\mBbbZ{}.
((aa\_binary\_search\_tree(t) \mwedge{} (aa\_max\_ltree(t) = (inl j ))) {}\mRightarrow{} aa\_bst\_member\_prop(j;t))
Date html generated:
2013_03_20-AM-09_52_58
Last ObjectModification:
2012_11_27-AM-10_32_53
Home
Index