Nuprl Definition : FormFvs

FormFvs(f) ==
  Form_ind(f;
           FormVar(v)⇒ [v];
           FormConst(c)⇒ [];
           FormSet(x,phi)⇒ fvsphi.filter(λv.(¬bv =a x);fvsphi);
           FormEqual(t1,t2)⇒ fvs1,fvs2.fvs1 ⋃ fvs2;
           FormMember(t1,t2)⇒ fvs1,fvs2.fvs1 ⋃ fvs2;
           FormAnd(a,b)⇒ fvsa,fvsb.fvsa ⋃ fvsb;
           FormOr(a,b)⇒ fvsa,fvsb.fvsa ⋃ fvsb;
           FormNot(a)⇒ fvsa.fvsa;
           FormAll(x,phi)⇒ fvsphi.filter(λv.(¬bv =a x);fvsphi);
           FormExists(x,phi)⇒ fvsphi.filter(λv.(¬bv =a x);fvsphi)) 


Definitions occuring in Statement :  Form_ind: Form_ind,  l-union: as ⋃ bs,  filter: filter(P;l),  cons: [a / b],  nil: [],  atom-deq: AtomDeq,  bnot: ¬bb,  eq_atom: x =a y,  lambda: λx.A[x]
Definitions occuring in definition :  Form_ind: Form_ind,  cons: [a / b],  nil: [],  l-union: as ⋃ bs,  atom-deq: AtomDeq,  filter: filter(P;l),  lambda: λx.A[x],  bnot: ¬bb,  eq_atom: x =a y
FDL editor aliases :  FormFvs FormFvs
Latex:
FormFvs(f)  ==
    Form\_ind(f;
                      FormVar(v){}\mRightarrow{}  [v];
                      FormConst(c){}\mRightarrow{}  [];
                      FormSet(x,phi){}\mRightarrow{}  fvsphi.filter(\mlambda{}v.(\mneg{}\msubb{}v  =a  x);fvsphi);
                      FormEqual(t1,t2){}\mRightarrow{}  fvs1,fvs2.fvs1  \mcup{}  fvs2;
                      FormMember(t1,t2){}\mRightarrow{}  fvs1,fvs2.fvs1  \mcup{}  fvs2;
                      FormAnd(a,b){}\mRightarrow{}  fvsa,fvsb.fvsa  \mcup{}  fvsb;
                      FormOr(a,b){}\mRightarrow{}  fvsa,fvsb.fvsa  \mcup{}  fvsb;
                      FormNot(a){}\mRightarrow{}  fvsa.fvsa;
                      FormAll(x,phi){}\mRightarrow{}  fvsphi.filter(\mlambda{}v.(\mneg{}\msubb{}v  =a  x);fvsphi);
                      FormExists(x,phi){}\mRightarrow{}  fvsphi.filter(\mlambda{}v.(\mneg{}\msubb{}v  =a  x);fvsphi)) 


Date html generated: 2018_05_21-PM-11_27_02
Last ObjectModification: 2017_10_11-AM-11_21_10

Theory : PZF


Home Index