### Nuprl Definition : int_formula_prop

`int_formula_prop(f;fmla) ==`
`  int_formula_ind(fmla;`
`                  a,b.int_term_value(f;a) < int_term_value(f;b);`
`                  a,b.int_term_value(f;a) ≤ int_term_value(f;b);`
`                  a,b.int_term_value(f;a) = int_term_value(f;b) ∈ ℤ;`
`                  X,Y,PX,PY.PX ∧ PY;`
`                  X,Y,PX,PY.PX ∨ PY;`
`                  X,Y,PX,PY.PX `` PY;`
`                  X,PX.¬PX)`

Definitions occuring in Statement :  int_formula_ind: int_formula_ind int_term_value: `int_term_value(f;t)` less_than: `a < b` le: `A ≤ B` not: `¬A` implies: `P `` Q` or: `P ∨ Q` and: `P ∧ Q` int: `ℤ` equal: `s = t ∈ T`
Definitions occuring in definition :  int_formula_ind: int_formula_ind less_than: `a < b` le: `A ≤ B` equal: `s = t ∈ T` int: `ℤ` int_term_value: `int_term_value(f;t)` and: `P ∧ Q` or: `P ∨ Q` implies: `P `` Q` not: `¬A`
FDL editor aliases :  int_formula_prop

Latex:
int\_formula\_prop(f;fmla)  ==
int\_formula\_ind(fmla;
a,b.int\_term\_value(f;a)  <  int\_term\_value(f;b);
a,b.int\_term\_value(f;a)  \mleq{}  int\_term\_value(f;b);
a,b.int\_term\_value(f;a)  =  int\_term\_value(f;b);
X,Y,PX,PY.PX  \mwedge{}  PY;
X,Y,PX,PY.PX  \mvee{}  PY;
X,Y,PX,PY.PX  {}\mRightarrow{}  PY;
X,PX.\mneg{}PX)

Date html generated: 2016_05_14-AM-07_07_15
Last ObjectModification: 2015_09_22-PM-05_52_46

Theory : omega

Home Index