Nuprl Definition : l_tree_ind

l_tree_ind(v;
           Leaf(lval)⇒ leaf[lval];
           Node(nval,left_subtree,right_subtree)⇒ rec1,rec2.node[nval; left_subtree; right_subtree; rec1; rec2])  ==
  fix((λl_tree_ind,v. let lbl,lval = v 
                      in if lbl="leaf" then leaf[lval]
                         if lbl="node"
                           then let nval,v2 = lval 
                                in let left_subtree,v3 = v2 
                                   in node[nval; left_subtree; v3; l_tree_ind left_subtree; l_tree_ind v3]
                         else Ax
                         fi )) 
  v


Definitions occuring in Statement :  atom_eq: if a=b then c else d fi ,  apply: f a,  fix: fix(F),  lambda: λx.A[x],  spread: spread def,  token: "$token",  axiom: Ax
Definitions occuring in definition :  fix: fix(F),  lambda: λx.A[x],  atom_eq: if a=b then c else d fi ,  token: "$token",  spread: spread def,  apply: f a,  axiom: Ax
FDL editor aliases :  l_tree_ind
Latex:
l\_tree\_ind(v;
                      Leaf(lval){}\mRightarrow{}  leaf[lval];
                      Node(nval,left$_{subtree}$,right$_{subtree}$){}\mRightarrow{}  r\000Cec1,rec2.node[nval;  left$_{subtree}$;  right$_{subtree}$;
                                                                                                                                rec1;  rec2])    ==
    fix((\mlambda{}l\_tree$_{ind}$,v.  let  lbl,lval  =  v 
                                          in  if  lbl="leaf"  then  leaf[lval]
                                                if  lbl="node"
                                                    then  let  nval,v2  =  lval 
                                                              in  let  left$_{subtree}$,v3  =  v2 
                                                                    in  node[nval;  left$_{subtree}$;  v3;  l\_tree\mbackslash{}ff2\000C4_{ind}$  left$_{subtree}$;  l\_tree$_{ind}$ 
                                                                                                                                                                                v3]
                                                else  Ax
                                                fi  )) 
    v


Date html generated: 2018_05_22-PM-09_39_17
Last ObjectModification: 2018_01_23-PM-00_23_10

Theory : labeled!trees


Home Index