Nuprl Definition : bs_tree_ind

case(v)
null=>null
leaf(value)=>leaf[value]
node(left,value,right)=>rec1,rec2.node[left; value; right; rec1; rec2] ==
  fix((λbs_tree_ind,v. let lbl,v1 = v 
                       in if lbl="null" then null
                          if lbl="leaf" then leaf[v1]
                          if lbl="node"
                            then let left,v2 = v1 
                                 in let value,v3 = v2 
                                    in node[left; value; v3; bs_tree_ind left; bs_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 :  bs_tree_ind bs_tree_ind
Latex:
case(v)
null=>null
leaf(value)=>leaf[value]
node(left,value,right)=>rec1,rec2.node[left;  value;  right;  rec1;  rec2]  ==
    fix((\mlambda{}bs\_tree$_{ind}$,v.  let  lbl,v1  =  v 
                                            in  if  lbl="null"  then  null
                                                  if  lbl="leaf"  then  leaf[v1]
                                                  if  lbl="node"
                                                      then  let  left,v2  =  v1 
                                                                in  let  value,v3  =  v2 
                                                                      in  node[left;  value;  v3;  bs\_tree$_{ind}$  left\000C;  bs\_tree$_{ind}$  v3]
                                                  else  Ax
                                                  fi  )) 
    v


Date html generated: 2016_05_15-PM-01_50_59
Last ObjectModification: 2016_04_07-PM-02_26_30

Theory : tree_1


Home Index