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