Nuprl Definition : rat_term_ind

rat_term_ind(v;
             rtermConstant(const)⇒ Constant[const];
             rtermVar(var)⇒ Var[var];
             rtermAdd(left,right)⇒ rec1,rec2.Add[left; right; rec1; rec2];
             rtermSubtract(left,right)⇒ rec3,rec4.Subtract[left; right; rec3; rec4];
             rtermMultiply(left,right)⇒ rec5,rec6.Multiply[left; right; rec5; rec6];
             rtermDivide(num,denom)⇒ rec7,rec8.Divide[num; denom; rec7; rec8];
             rtermMinus(num)⇒ rec9.Minus[num; rec9])  ==
  fix((λrat_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; rat_term_ind left; rat_term_ind v2]
                           if lbl="Subtract"
                             then let left,v2 = v1 
                                  in Subtract[left; v2; rat_term_ind left; rat_term_ind v2]
                           if lbl="Multiply"
                             then let left,v2 = v1 
                                  in Multiply[left; v2; rat_term_ind left; rat_term_ind v2]
                           if lbl="Divide" then let num,v2 = v1 in Divide[num; v2; rat_term_ind num; rat_term_ind v2]
                           if lbl="Minus" then Minus[v1; rat_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 :  rat_term_ind
Latex:
rat\_term\_ind(v;
                          rtermConstant(const){}\mRightarrow{}  Constant[const];
                          rtermVar(var){}\mRightarrow{}  Var[var];
                          rtermAdd(left,right){}\mRightarrow{}  rec1,rec2.Add[left;  right;  rec1;  rec2];
                          rtermSubtract(left,right){}\mRightarrow{}  rec3,rec4.Subtract[left;  right;  rec3;  rec4];
                          rtermMultiply(left,right){}\mRightarrow{}  rec5,rec6.Multiply[left;  right;  rec5;  rec6];
                          rtermDivide(num,denom){}\mRightarrow{}  rec7,rec8.Divide[num;  denom;  rec7;  rec8];
                          rtermMinus(num){}\mRightarrow{}  rec9.Minus[num;  rec9])    ==
    fix((\mlambda{}rat\_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;  rat\_term$_{ind}$  left;  rat\_ter\000Cm$_{ind}$  v2]
                                                    if  lbl="Subtract"
                                                        then  let  left,v2  =  v1 
                                                                  in  Subtract[left;  v2;  rat\_term$_{ind}$  left;  ra\000Ct\_term$_{ind}$  v2]
                                                    if  lbl="Multiply"
                                                        then  let  left,v2  =  v1 
                                                                  in  Multiply[left;  v2;  rat\_term$_{ind}$  left;  ra\000Ct\_term$_{ind}$  v2]
                                                    if  lbl="Divide"
                                                        then  let  num,v2  =  v1 
                                                                  in  Divide[num;  v2;  rat\_term$_{ind}$  num;  rat\_te\000Crm$_{ind}$  v2]
                                                    if  lbl="Minus"  then  Minus[v1;  rat\_term$_{ind}$  v1]
                                                    else  Ax
                                                    fi  )) 
    v


Date html generated: 2019_10_29-AM-09_30_59
Last ObjectModification: 2019_03_31-PM-05_21_43

Theory : reals


Home Index