### 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];
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]
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