Nuprl Definition : tree_ind

tree_ind(v;
         tree_leaf(value)⇒ leaf[value];
         tree_node(left,right)⇒ rec1,rec2.node[left; right; rec1; rec2])  ==
  fix((λtree_ind,v. let lbl,v1 = v 
                    in if lbl="leaf" then leaf[v1]
                       if lbl="node" then let left,v2 = v1 in node[left; v2; tree_ind left; tree_ind v2]
                       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 :  tree_ind
Latex:
tree\_ind(v;
                  tree\_leaf(value){}\mRightarrow{}  leaf[value];
                  tree\_node(left,right){}\mRightarrow{}  rec1,rec2.node[left;  right;  rec1;  rec2])    ==
    fix((\mlambda{}tree$_{ind}$,v.  let  lbl,v1  =  v 
                                      in  if  lbl="leaf"  then  leaf[v1]
                                            if  lbl="node"
                                                then  let  left,v2  =  v1 
                                                          in  node[left;  v2;  tree$_{ind}$  left;  tree$_\000C{ind}$  v2]
                                            else  Ax
                                            fi  )) 
    v


Date html generated: 2016_05_15-PM-01_49_53
Last ObjectModification: 2015_11_30-PM-09_26_49

Theory : tree_1


Home Index