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