Nuprl Definition : SafeForm

SafeForm(f) ==
  Form_ind(f;
           FormVar(v)⇒ tt;
           FormConst(c)⇒ tt;
           FormSet(x,phi)⇒ r.r ∧b PZF_safe(phi;[x]);
           FormEqual(l,r)⇒ r1,r2.r1 ∧b r2;
           FormMember(e,s)⇒ r1,r2.r1 ∧b r2;
           FormAnd(l,r)⇒ r1,r2.r1 ∧b r2;
           FormOr(l,r)⇒ r1,r2.r1 ∧b r2;
           FormNot(b)⇒ r1.r1;
           FormAll(x,b)⇒ r1.r1;
           FormExists(x,b)⇒ r1.r1) 


Definitions occuring in Statement :  PZF_safe: PZF_safe(phi;vs),  Form_ind: Form_ind,  cons: [a / b],  nil: [],  band: p ∧b q,  btrue: tt
Definitions occuring in definition :  Form_ind: Form_ind,  btrue: tt,  PZF_safe: PZF_safe(phi;vs),  cons: [a / b],  nil: [],  band: p ∧b q
FDL editor aliases :  SafeForm SafeForm
Latex:
SafeForm(f)  ==
    Form\_ind(f;
                      FormVar(v){}\mRightarrow{}  tt;
                      FormConst(c){}\mRightarrow{}  tt;
                      FormSet(x,phi){}\mRightarrow{}  r.r  \mwedge{}\msubb{}  PZF\_safe(phi;[x]);
                      FormEqual(l,r){}\mRightarrow{}  r1,r2.r1  \mwedge{}\msubb{}  r2;
                      FormMember(e,s){}\mRightarrow{}  r1,r2.r1  \mwedge{}\msubb{}  r2;
                      FormAnd(l,r){}\mRightarrow{}  r1,r2.r1  \mwedge{}\msubb{}  r2;
                      FormOr(l,r){}\mRightarrow{}  r1,r2.r1  \mwedge{}\msubb{}  r2;
                      FormNot(b){}\mRightarrow{}  r1.r1;
                      FormAll(x,b){}\mRightarrow{}  r1.r1;
                      FormExists(x,b){}\mRightarrow{}  r1.r1) 


Date html generated: 2018_05_21-PM-11_36_17
Last ObjectModification: 2017_10_12-PM-02_53_37

Theory : PZF


Home Index