Nuprl Definition : pnegate

pnegate(x) ==
  formula_ind(x;
              pvar(v)⇒ pnot(pvar(v));
              pnot(A)⇒ nA.A;
              pand(A,B)⇒ nA,nB.por(nA;nB);
              por(A,B)⇒ nA,nB.pand(nA;nB);
              pimp(A,B)⇒ nA,nB.pand(A;nB)) 


Definitions occuring in Statement :  formula_ind: formula_ind,  por: por(left;right),  pand: pand(left;right),  pnot: pnot(sub),  pvar: pvar(name)
Definitions occuring in definition :  formula_ind: formula_ind,  pnot: pnot(sub),  pvar: pvar(name),  por: por(left;right),  pand: pand(left;right)
FDL editor aliases :  pnegate
Latex:
pnegate(x)  ==
    formula\_ind(x;
                            pvar(v){}\mRightarrow{}  pnot(pvar(v));
                            pnot(A){}\mRightarrow{}  nA.A;
                            pand(A,B){}\mRightarrow{}  nA,nB.por(nA;nB);
                            por(A,B){}\mRightarrow{}  nA,nB.pand(nA;nB);
                            pimp(A,B){}\mRightarrow{}  nA,nB.pand(A;nB)) 


Date html generated: 2016_05_15-PM-07_18_23
Last ObjectModification: 2015_09_23-AM-08_14_10

Theory : general


Home Index