Nuprl Lemma : aa_max_ltree_spec3
t:aa_ltree(
). (((aa_binary_search_tree(t) 
(
i:. aa_bst_member_prop(i;t))) (aa_max_ltree(t) = (inr 
))) 
False)
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),
it: ,
all: x:A. B[x],
exists: x:A. B[x],
implies: P Q,
and: P Q,
false: False,
unit: Unit,
inr: inr x ,
union: left + right,
int: ,
equal: s = t
Definitions :
so_lambda: 
x.t[x],
prop: 
,
member: t 
T,
false: False,
exists: x:A. B[x],
and: P Q,
implies: P Q,
all: x:A. B[x],
so_lambda: so_lambda(x,y,z,w,v.t[x; y; z; w; v]),
subtype: S 
T,
top: Top,
aa_ltree: aa_ltree(T),
so_apply: x[s],
uall: [x:A]. B[x],
so_apply: x[s1;s2;s3;s4;s5],
aa_ltree_ind: aa_ltree_ind(x;leaf;val,left_subtree,right_subtree,rec1,rec2.node[val; left_subtree; right_subtree; rec1; rec2]),
aa_max_ltree: aa_max_ltree(t),
aa_bst_member_prop: aa_bst_member_prop(i;t),
guard: {T}
Lemmas :
aa_ltree_wf,
it_wf,
aa_max_ltree_wf,
unit_wf2,
aa_bst_member_prop_wf,
exists_wf,
aa_binary_search_tree_wf,
pi2_wf,
aa_ltree_ind_wf,
pi1_wf_top,
aa_max_w_unit_wf,
subtype_rel_self,
equal_wf,
or_wf,
false_wf,
aa_max_w_unit_prop1
\mforall{}t:aa\_ltree(\mBbbZ{})
(((aa\_binary\_search\_tree(t) \mwedge{} (\mexists{}i:\mBbbZ{}. aa\_bst\_member\_prop(i;t))) \mwedge{} (aa\_max\_ltree(t) = (inr \mcdot{} )))
{}\mRightarrow{} False)
Date html generated:
2013_03_20-AM-09_53_54
Last ObjectModification:
2012_11_27-AM-10_32_57
Home
Index