Nuprl Definition : mFO-equal

mFO-equal(x) ==
  mFOL_ind(x;
           mFOatomic(R,vars)⇒ λy.let R',vars' = dest-atomic(y) in
                                  R =a R' ∧b (list-deq(IntDeq) vars vars');
           mFOconnect(knd,a,b)⇒ eqa,eqb.λy.let a',b' = dest-knd(y) in
                                            (eqa a') ∧b (eqb b');
           mFOquant(isall,v,b)⇒ eqb.λy.let w,b' = dest-if isall then all else exists(y); in
                                         (v =z w) ∧b (eqb b')) 


Definitions occuring in Statement :  mFO-dest-quantifier: mFO-dest-quantifier,  mFO-dest-connective: mFO-dest-connective,  mFO-dest-atomic: mFO-dest-atomic,  mFOL_ind: mFOL_ind,  list-deq: list-deq(eq),  int-deq: IntDeq,  band: p ∧b q,  eq_atom: x =a y,  eq_int: (i =z j),  apply: f a,  lambda: λx.A[x]
FDL editor aliases :  mFO-equal
mFO-equal(x)  ==
    mFOL\_ind(x;
                      mFOatomic(R,vars){}\mRightarrow{}  \mlambda{}y.let  R',vars'  =  dest-atomic(y)  in
                                                                    R  =a  R'  \mwedge{}\msubb{}  (list-deq(IntDeq)  vars  vars');
                      mFOconnect(knd,a,b){}\mRightarrow{}  eqa,eqb.\mlambda{}y.let  a',b'  =  dest-knd(y)  in
                                                                                        (eqa  a')  \mwedge{}\msubb{}  (eqb  b');
                      mFOquant(isall,v,b){}\mRightarrow{}  eqb.\mlambda{}y.let  w,b'  =  dest-if  isall  then  all  else  exists(y);  in
                                                                                  (v  =\msubz{}  w)  \mwedge{}\msubb{}  (eqb  b')) 


Date html generated: 2015_07_17-AM-07_54_04
Last ObjectModification: 2012_12_07-PM-00_14_39

Home Index