Nuprl Definition : aa_ltree_ind_aa_lt_node_compseq_tag_def
aa_ltree_ind_aa_lt_node{aa_ltree_ind_aa_lt_node_compseq_tag_def:o}(v11,v12,v13,v14,v15.node[v11; v12; v13; v14; v15];
leaf;
right_subtree;
left_subtree;
val) ==
compseq
(aa_ltree_ind(aa_lt_node(val;left_subtree;right_subtree);leaf;val,left_subtree,right_subtree,rec1,rec2.node[val;
...;
...;
rec1;
rec2]);
node[val; left_subtree; right_subtree;
aa_ltree_ind(left_subtree;leaf;val,left_subtree,right_subtree,rec1,rec2.node[val; left_subtree; right_subtree;
rec1; rec2]);
aa_ltree_ind(right_subtree;leaf;val,left_subtree,right_subtree,rec1,rec2.node[val; left_subtree;
right_subtree; rec1; rec2])])
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_lt_node: aa_lt_node(val;left_subtree;right_subtree)
aa\_ltree\_ind\_aa\_lt\_node\{aa\_ltree\_ind\_aa\_lt\_node\_compseq\_tag\_def:o\}
(v11,v12,v13,v14,v15.node[v11; v12; v13; v14; v15]; leaf; right$_{subtree}$; l\000Ceft$_{subtree}$; val) ==
compseq
(aa\_ltree\_ind(aa\_lt\_node(val;left$_{subtree}$;...);leaf;val,left$_\mbackslash{}f\000Cf7bsubtree}$,right$_{subtree}$,rec1,rec2....);
node[val; left$_{subtree}$; right$_{subtree}$;
aa\_ltree\_ind(left$_{subtree}$;leaf;val,left$_{subtree}\000C$,right$_{subtree}$,rec1,rec2.node[val;
left$_\mbackslash{}f\000Cf7bsubtree}$;
right$_\mbackslash{}\000Cff7bsubtree}$;
rec1; rec2]);
aa\_ltree\_ind(right$_{subtree}$;leaf;val,left$_{subtree\mbackslash{}ff7\000Cd$,right$_{subtree}$,rec1,rec2.node[val;
left$_\mbackslash{}\000Cff7bsubtree}$;
right$_\000C{subtree}$;
rec1; rec2])])
Date html generated:
2013_03_20-AM-10_57_53
Last ObjectModification:
2012_11_27-AM-10_32_27
Home
Index