Nuprl Definition : MultiTree_ind
MultiTree_ind(v;
              MTree_Node(labels,children)
⇒ rec1.Node[labels; children; rec1];
              MTree_Leaf(val)
⇒ Leaf[val])  ==
  fix((λMultiTree_ind,v. let lbl,v1 = v 
                         in if lbl="Node" then let labels,v2 = v1 in Node[labels; v2; λu.(MultiTree_ind (v2 u))]
                            if lbl="Leaf" then Leaf[v1]
                            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)
, 
spread: spread def, 
lambda: λx.A[x]
, 
apply: f a
, 
atom_eq: if a=b then c else d fi 
, 
token: "$token"
, 
axiom: Ax
FDL editor aliases : 
MultiTree_ind
Latex:
MultiTree\_ind(v;
                            MTree\_Node(labels,children){}\mRightarrow{}  rec1.Node[labels;  children;  rec1];
                            MTree\_Leaf(val){}\mRightarrow{}  Leaf[val])    ==
    fix((\mlambda{}MultiTree$_{ind}$,v.  let  lbl,v1  =  v 
                                                in  if  lbl="Node"
                                                          then  let  labels,v2  =  v1 
                                                                    in  Node[labels;  v2;  \mlambda{}u.(MultiTree$_{ind}$  (v2  \000Cu))]
                                                      if  lbl="Leaf"  then  Leaf[v1]
                                                      else  Ax
                                                      fi  )) 
    v
Date html generated:
2016_05_16-AM-08_53_41
Last ObjectModification:
2015_12_14-PM-01_40_40
Theory : C-semantics
Home
Index