Nuprl Definition : mFOL_ind

mFOL_ind(v;
         mFOatomic(name,vars)⇒ atomic[name; vars];
         mFOconnect(knd,left,right)⇒ rec1,rec2.connect[knd; left; right; rec1; rec2];
         mFOquant(isall,var,body)⇒ rec3.quant[isall; var; body; rec3])  ==
  fix((λmFOL_ind,v. let lbl,v1 = v 
                    in if lbl="atomic" then let name,v2 = v1 in atomic[name; v2]
                       if lbl="connect"
                         then let knd,v2 = v1 
                              in let left,v3 = v2 
                                 in connect[knd; left; v3; mFOL_ind left; mFOL_ind v3]
                       if lbl="quant" then let isall,v2 = v1 in let var,v3 = v2 in quant[isall; var; v3; mFOL_ind v3]
                       else ⊥
                       fi )) 
  v


Definitions occuring in Statement :  bottom: ⊥,  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"
FDL editor aliases :  mFOL_ind mFOL_ind
mFOL\_ind(v;
                  mFOatomic(name,vars){}\mRightarrow{}  atomic[name;  vars];
                  mFOconnect(knd,left,right){}\mRightarrow{}  rec1,rec2.connect[knd;  left;  right;  rec1;  rec2];
                  mFOquant(isall,var,body){}\mRightarrow{}  rec3.quant[isall;  var;  body;  rec3])    ==
    fix((\mlambda{}mFOL$_{ind}$,v.  let  lbl,v1  =  v 
                                      in  if  lbl="atomic"  then  let  name,v2  =  v1  in  atomic[name;  v2]
                                            if  lbl="connect"
                                                then  let  knd,v2  =  v1 
                                                          in  let  left,v3  =  v2 
                                                                in  connect[knd;  left;  v3;  mFOL$_{ind}$  left;  mFO\000CL$_{ind}$  v3]
                                            if  lbl="quant"
                                                then  let  isall,v2  =  v1 
                                                          in  let  var,v3  =  v2 
                                                                in  quant[isall;  var;  v3;  mFOL$_{ind}$  v3]
                                            else  \mbot{}
                                            fi  )) 
    v


Date html generated: 2015_07_17-AM-07_53_51
Last ObjectModification: 2014_04_30-PM-01_17_41

Home Index