Nuprl Definition : aa_ltree_ind

aa_ltree_ind(x;leaf;val,left_subtree,right_subtree,rec1,rec2.node[val; left_subtree; right_subtree; rec1; rec2]) ==
  fix((aa_ltree_ind,x. case x
                       of inl(x) =>
                        leaf
                        | inr(x) =>
                        node[fst(x); fst(snd(x)); snd(snd(x)); aa_ltree_ind (fst(snd(x))); aa_ltree_ind (snd(snd(x)))]))\000C 
  x


Definitions occuring in Statement :  pi1: fst(t),  pi2: snd(t),  apply: f a,  lambda: x.A[x],  decide: case b of inl(x) => s[x] | inr(y) => t[y]
FDL editor aliases :  aa_ltree_ind
aa\_ltree\_ind(x;leaf;val,left$_{subtree}$,right$_{subtree}$,r\000Cec1,rec2.node[val;  left$_{subtree}$;  right$_{subtree}$;
                                                                                                                                rec1;  rec2])  ==
    fix((\mlambda{}aa\_ltree$_{ind}$,x.  case  x
                                            of  inl(x)  =>
                                              leaf
                                              |  inr(x)  =>
                                              node[fst(x);  fst(snd(x));  snd(snd(x));  aa\_ltree$_{ind}$  (\000Cfst(snd(x)));
                                                        aa\_ltree$_{ind}$  (snd(snd(x)))])) 
    x


Date html generated: 2013_03_20-AM-10_57_43
Last ObjectModification: 2012_11_27-AM-10_32_22

Home Index