Nuprl Lemma : aa_binary_search_tree_wf
t:aa_ltree(
). (aa_binary_search_tree(t) 
)
Proof
Definitions occuring in Statement :
aa_binary_search_tree: aa_binary_search_tree(t),
aa_ltree: aa_ltree(T),
prop: ,
all: x:A. B[x],
member: t T,
int:
Definitions :
all: x:A. B[x],
member: t T,
prop: ,
aa_binary_search_tree: aa_binary_search_tree(t),
so_lambda: so_lambda(x,y,z,w,v.t[x; y; z; w; v]),
uall: [x:A]. B[x],
so_apply: x[s1;s2;s3;s4;s5]
Lemmas :
aa_ltree_ind_wf,
le_wf,
and_wf,
aa_max_ltree_wf,
less_than_wf,
aa_min_ltree_wf,
aa_ltree_wf
\mforall{}t:aa\_ltree(\mBbbZ{}). (aa\_binary\_search\_tree(t) \mmember{} \mBbbP{})
Date html generated:
2013_03_20-AM-09_52_44
Last ObjectModification:
2012_11_27-AM-10_32_51
Home
Index