Nuprl Definition : formula_ind

formula_ind(v;
            pvar(name)⇒ var[name];
            pnot(sub)⇒ rec1.not[sub; rec1];
            pand(left,right)⇒ rec2,rec3.and[left; right; rec2; rec3];
            por(left,right)⇒ rec4,rec5.or[left; right; rec4; rec5];
            pimp(left,right)⇒ rec6,rec7.imp[left; right; rec6; rec7])  ==
  fix((λformula_ind,v. let lbl,v1 = v 
                       in if lbl="var" then var[v1]
                          if lbl="not" then not[v1; formula_ind v1]
                          if lbl="and" then let left,v2 = v1 in and[left; v2; formula_ind left; formula_ind v2]
                          if lbl="or" then let left,v2 = v1 in or[left; v2; formula_ind left; formula_ind v2]
                          if lbl="imp" then let left,v2 = v1 in imp[left; v2; formula_ind left; formula_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 :  formula_ind formula_ind
Latex:
formula\_ind(v;
                        pvar(name){}\mRightarrow{}  var[name];
                        pnot(sub){}\mRightarrow{}  rec1.not[sub;  rec1];
                        pand(left,right){}\mRightarrow{}  rec2,rec3.and[left;  right;  rec2;  rec3];
                        por(left,right){}\mRightarrow{}  rec4,rec5.or[left;  right;  rec4;  rec5];
                        pimp(left,right){}\mRightarrow{}  rec6,rec7.imp[left;  right;  rec6;  rec7])    ==
    fix((\mlambda{}formula$_{ind}$,v.  let  lbl,v1  =  v 
                                            in  if  lbl="var"  then  var[v1]
                                                  if  lbl="not"  then  not[v1;  formula$_{ind}$  v1]
                                                  if  lbl="and"
                                                      then  let  left,v2  =  v1 
                                                                in  and[left;  v2;  formula$_{ind}$  left;  formula\mbackslash{}f\000Cf24_{ind}$  v2]
                                                  if  lbl="or"
                                                      then  let  left,v2  =  v1 
                                                                in  or[left;  v2;  formula$_{ind}$  left;  formula\mbackslash{}ff\000C24_{ind}$  v2]
                                                  if  lbl="imp"
                                                      then  let  left,v2  =  v1 
                                                                in  imp[left;  v2;  formula$_{ind}$  left;  formula\mbackslash{}f\000Cf24_{ind}$  v2]
                                                  else  Ax
                                                  fi  )) 
    v


Date html generated: 2016_05_15-PM-07_11_55
Last ObjectModification: 2015_11_30-PM-09_11_24

Theory : general


Home Index