Nuprl Definition : int_formula_ind

int_formula_ind(v;
                intformless(left,right)⇒ less[left; right];
                intformle(left,right)⇒ le[left; right];
                intformeq(left,right)⇒ eq[left; right];
                intformand(left,right)⇒ rec1,rec2.and[left; right; rec1; rec2];
                intformor(left,right)⇒ rec3,rec4.or[left; right; rec3; rec4];
                intformimplies(left,right)⇒ rec5,rec6.implies[left; right; rec5; rec6];
                intformnot(form)⇒ rec7.not[form; rec7])  ==
  fix((λint_formula_ind,v. let lbl,v1 = v 
                           in if lbl="less" then let left,v2 = v1 in less[left; v2]
                              if lbl="le" then let left,v2 = v1 in le[left; v2]
                              if lbl="eq" then let left,v2 = v1 in eq[left; v2]
                              if lbl="and"
                                then let left,v2 = v1 
                                     in and[left; v2; int_formula_ind left; int_formula_ind v2]
                              if lbl="or"
                                then let left,v2 = v1 
                                     in or[left; v2; int_formula_ind left; int_formula_ind v2]
                              if lbl="implies"
                                then let left,v2 = v1 
                                     in implies[left; v2; int_formula_ind left; int_formula_ind v2]
                              if lbl="not" then not[v1; int_formula_ind 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),  lambda: λx.A[x],  spread: spread def,  atom_eq: if a=b then c else d fi ,  token: "$token",  apply: f a,  axiom: Ax
FDL editor aliases :  int_formula_ind
Latex:
int\_formula\_ind(v;
                                intformless(left,right){}\mRightarrow{}  less[left;  right];
                                intformle(left,right){}\mRightarrow{}  le[left;  right];
                                intformeq(left,right){}\mRightarrow{}  eq[left;  right];
                                intformand(left,right){}\mRightarrow{}  rec1,rec2.and[left;  right;  rec1;  rec2];
                                intformor(left,right){}\mRightarrow{}  rec3,rec4.or[left;  right;  rec3;  rec4];
                                intformimplies(left,right){}\mRightarrow{}  rec5,rec6.implies[left;  right;  rec5;  rec6];
                                intformnot(form){}\mRightarrow{}  rec7.not[form;  rec7])    ==
    fix((\mlambda{}int\_formula$_{ind}$,v.  let  lbl,v1  =  v 
                                                    in  if  lbl="less"  then  let  left,v2  =  v1  in  less[left;  v2]
                                                          if  lbl="le"  then  let  left,v2  =  v1  in  le[left;  v2]
                                                          if  lbl="eq"  then  let  left,v2  =  v1  in  eq[left;  v2]
                                                          if  lbl="and"
                                                              then  let  left,v2  =  v1 
                                                                        in  and[left;  v2;  int\_formula$_{ind}$  left;  i\000Cnt\_formula$_{ind}$  v2]
                                                          if  lbl="or"
                                                              then  let  left,v2  =  v1 
                                                                        in  or[left;  v2;  int\_formula$_{ind}$  left;  in\000Ct\_formula$_{ind}$  v2]
                                                          if  lbl="implies"
                                                              then  let  left,v2  =  v1 
                                                                        in  implies[left;  v2;  int\_formula$_{ind}$  lef\000Ct;  int\_formula$_{ind}$  v2]
                                                          if  lbl="not"  then  not[v1;  int\_formula$_{ind}$  v1]
                                                          else  Ax
                                                          fi  )) 
    v


Date html generated: 2016_05_14-AM-07_07_05
Last ObjectModification: 2015_09_22-PM-05_52_45

Theory : omega


Home Index