Nuprl Lemma : aa_bst_member_prop_wf
[t:aa_ltree(
)]. [i:]. (aa_bst_member_prop(i;t) 
)
Proof
Definitions occuring in Statement :
aa_bst_member_prop: aa_bst_member_prop(i;t),
aa_ltree: aa_ltree(T),
uall: [x:A]. B[x],
prop: ,
member: t T,
int:
Definitions :
so_lambda: so_lambda(x,y,z,w,v.t[x; y; z; w; v]),
and: P 
Q,
aa_bst_member_prop: aa_bst_member_prop(i;t),
prop: ,
member: t T,
uall: [x:A]. B[x],
so_apply: x[s1;s2;s3;s4;s5]
Lemmas :
aa_ltree_wf,
equal_wf,
or_wf,
false_wf,
aa_ltree_ind_wf
\mforall{}[t:aa\_ltree(\mBbbZ{})]. \mforall{}[i:\mBbbZ{}]. (aa\_bst\_member\_prop(i;t) \mmember{} \mBbbP{})
Date html generated:
2013_03_20-AM-09_52_37
Last ObjectModification:
2012_11_27-AM-10_32_49
Home
Index