Nuprl Definition : int_formula

Nuprl Definition : int_formula_dnf

int_formula_dnf(fmla) ==
  int_formula_ind(fmla;
                  a,b.[<[], [int_term_to_ipoly(b "-" a "+" "1")]>];
                  a,b.[<[], [int_term_to_ipoly(b "-" a)]>];
                  a,b.[<[int_term_to_ipoly(b "-" a)], []>];
                  X,Y,nfX,nfY.and-poly-constraints(nfX;nfY);
                  X,Y,nfX,nfY.nfX @ nfY;
                  X,Y,nfX,nfY.negate-poly-constraints(nfX) @ nfY;
                  X,nfX.negate-poly-constraints(nfX))

Definitions occuring in Statement : negate-poly-constraints: negate-poly-constraints(Xs), and-poly-constraints: and-poly-constraints(Xs;Ys), int_formula_ind: int_formula_ind, int_term_to_ipoly: int_term_to_ipoly(t), itermSubtract: left "-" right, itermAdd: left "+" right, itermConstant: "const", append: as @ bs, cons: [a / b], nil: [], pair: <a, b>, natural_number: $n
Definitions occuring in definition : int_formula_ind: int_formula_ind, itermAdd: left "+" right, itermConstant: "const", natural_number: $n, pair: <a, b>, cons: [a / b], int_term_to_ipoly: int_term_to_ipoly(t), itermSubtract: left "-" right, nil: [], and-poly-constraints: and-poly-constraints(Xs;Ys), append: as @ bs, negate-poly-constraints: negate-poly-constraints(Xs)
FDL editor aliases : int_formula_dnf

Latex:
int\_formula\_dnf(fmla) == int\_formula\_ind(fmla; a,b.[<[], [int\_term\_to\_ipoly(b "-" a "+" "1")]>]; a,b.[<[], [int\_term\_to\_ipoly(b "-" a)]>]; a,b.[<[int\_term\_to\_ipoly(b "-" a)], []>]; X,Y,nfX,nfY.and-poly-constraints(nfX;nfY); X,Y,nfX,nfY.nfX @ nfY; X,Y,nfX,nfY.negate-poly-constraints(nfX) @ nfY; X,nfX.negate-poly-constraints(nfX)) Date html generated: 2016_05_14-AM-07_09_32 Last ObjectModification: 2015_09_22-PM-05_53_01 Theory : omega Home Index