Nuprl Definition : aa_min_ltree
aa_min_ltree(t) ==  aa_ltree_ind(t;inr  v,ltr,rtr,ltrm,rtrm.aa_min_w_unit(inl v ltrm))
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_min_w_unit: aa_min_w_unit(u1;u2), 
it: , 
inr: inr x , 
inl: inl x 
FDL editor aliases : 
aa_min_ltree
aa\_min\_ltree(t)  ==    aa\_ltree\_ind(t;inr  \mcdot{}  ;v,ltr,rtr,ltrm,rtrm.aa\_min\_w\_unit(inl  v  ;ltrm))
Date html generated:
2013_03_20-AM-09_52_26
Last ObjectModification:
2012_11_27-AM-10_32_45
Home
Index