Nuprl Definition : aa_max_ltree
aa_max_ltree(t) == aa_ltree_ind(t;inr 
;v,ltr,rtr,ltrm,rtrm.aa_max_w_unit(inl v ;rtrm))
Definitions occuring in Statement :
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_w_unit: aa_max_w_unit(u1;u2),
it: ,
inr: inr x ,
inl: inl x
FDL editor aliases :
aa_max_ltree
aa\_max\_ltree(t) == aa\_ltree\_ind(t;inr \mcdot{} ;v,ltr,rtr,ltrm,rtrm.aa\_max\_w\_unit(inl v ;rtrm))
Date html generated:
2013_03_20-AM-09_52_24
Last ObjectModification:
2012_11_27-AM-10_32_44
Home
Index