Nuprl Definition : int_term_ind

int_term_ind(v;
             itermConstant(const)⇒ Constant[const];
             itermVar(var)⇒ Var[var];
             itermAdd(left,right)⇒ rec1,rec2.Add[left; right; rec1; rec2];
             itermSubtract(left,right)⇒ rec3,rec4.Subtract[left; right; rec3; rec4];
             itermMultiply(left,right)⇒ rec5,rec6.Multiply[left; right; rec5; rec6];
             itermMinus(num)⇒ rec7.Minus[num; rec7])  ==
  fix((λint_term_ind,v. let lbl,v1 = v 
                        in if lbl="Constant" then Constant[v1]
                           if lbl="Var" then Var[v1]
                           if lbl="Add" then let left,v2 = v1 in Add[left; v2; int_term_ind left; int_term_ind v2]
                           if lbl="Subtract"
                             then let left,v2 = v1 
                                  in Subtract[left; v2; int_term_ind left; int_term_ind v2]
                           if lbl="Multiply"
                             then let left,v2 = v1 
                                  in Multiply[left; v2; int_term_ind left; int_term_ind v2]
                           if lbl="Minus" then Minus[v1; int_term_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_term_ind
Latex:
int\_term\_ind(v;
                          itermConstant(const){}\mRightarrow{}  Constant[const];
                          itermVar(var){}\mRightarrow{}  Var[var];
                          itermAdd(left,right){}\mRightarrow{}  rec1,rec2.Add[left;  right;  rec1;  rec2];
                          itermSubtract(left,right){}\mRightarrow{}  rec3,rec4.Subtract[left;  right;  rec3;  rec4];
                          itermMultiply(left,right){}\mRightarrow{}  rec5,rec6.Multiply[left;  right;  rec5;  rec6];
                          itermMinus(num){}\mRightarrow{}  rec7.Minus[num;  rec7])    ==
    fix((\mlambda{}int\_term$_{ind}$,v.  let  lbl,v1  =  v 
                                              in  if  lbl="Constant"  then  Constant[v1]
                                                    if  lbl="Var"  then  Var[v1]
                                                    if  lbl="Add"
                                                        then  let  left,v2  =  v1 
                                                                  in  Add[left;  v2;  int\_term$_{ind}$  left;  int\_ter\000Cm$_{ind}$  v2]
                                                    if  lbl="Subtract"
                                                        then  let  left,v2  =  v1 
                                                                  in  Subtract[left;  v2;  int\_term$_{ind}$  left;  in\000Ct\_term$_{ind}$  v2]
                                                    if  lbl="Multiply"
                                                        then  let  left,v2  =  v1 
                                                                  in  Multiply[left;  v2;  int\_term$_{ind}$  left;  in\000Ct\_term$_{ind}$  v2]
                                                    if  lbl="Minus"  then  Minus[v1;  int\_term$_{ind}$  v1]
                                                    else  Ax
                                                    fi  )) 
    v


Date html generated: 2016_05_14-AM-06_59_13
Last ObjectModification: 2015_09_22-PM-05_51_37

Theory : omega


Home Index