Nuprl Definition : wfFormAux

wfFormAux(f) ==
  Form_ind(f;
           FormVar(v)⇒ λisterm.isterm;
           FormConst(c)⇒ λisterm.isterm;
           FormSet(x,phi)⇒ r.λisterm.(isterm ∧b (r ff));
           FormEqual(l,r)⇒ r1,r2.λisterm.((¬bisterm) ∧b (r1 tt) ∧b (r2 tt));
           FormMember(e,s)⇒ r1,r2.λisterm.((¬bisterm) ∧b (r1 tt) ∧b (r2 tt));
           FormAnd(l,r)⇒ r1,r2.λisterm.((¬bisterm) ∧b (r1 ff) ∧b (r2 ff));
           FormOr(l,r)⇒ r1,r2.λisterm.((¬bisterm) ∧b (r1 ff) ∧b (r2 ff));
           FormNot(b)⇒ r1.λisterm.((¬bisterm) ∧b (r1 ff));
           FormAll(x,b)⇒ r1.λisterm.((¬bisterm) ∧b (r1 ff));
           FormExists(x,b)⇒ r1.λisterm.((¬bisterm) ∧b (r1 ff))) 


Definitions occuring in Statement :  Form_ind: Form_ind,  band: p ∧b q,  bnot: ¬bb,  bfalse: ff,  btrue: tt,  apply: f a,  lambda: λx.A[x]
Definitions occuring in definition :  Form_ind: Form_ind,  btrue: tt,  lambda: λx.A[x],  band: p ∧b q,  bnot: ¬bb,  apply: f a,  bfalse: ff
FDL editor aliases :  wfFormAux wfFormAux
Latex:
wfFormAux(f)  ==
    Form\_ind(f;
                      FormVar(v){}\mRightarrow{}  \mlambda{}isterm.isterm;
                      FormConst(c){}\mRightarrow{}  \mlambda{}isterm.isterm;
                      FormSet(x,phi){}\mRightarrow{}  r.\mlambda{}isterm.(isterm  \mwedge{}\msubb{}  (r  ff));
                      FormEqual(l,r){}\mRightarrow{}  r1,r2.\mlambda{}isterm.((\mneg{}\msubb{}isterm)  \mwedge{}\msubb{}  (r1  tt)  \mwedge{}\msubb{}  (r2  tt));
                      FormMember(e,s){}\mRightarrow{}  r1,r2.\mlambda{}isterm.((\mneg{}\msubb{}isterm)  \mwedge{}\msubb{}  (r1  tt)  \mwedge{}\msubb{}  (r2  tt));
                      FormAnd(l,r){}\mRightarrow{}  r1,r2.\mlambda{}isterm.((\mneg{}\msubb{}isterm)  \mwedge{}\msubb{}  (r1  ff)  \mwedge{}\msubb{}  (r2  ff));
                      FormOr(l,r){}\mRightarrow{}  r1,r2.\mlambda{}isterm.((\mneg{}\msubb{}isterm)  \mwedge{}\msubb{}  (r1  ff)  \mwedge{}\msubb{}  (r2  ff));
                      FormNot(b){}\mRightarrow{}  r1.\mlambda{}isterm.((\mneg{}\msubb{}isterm)  \mwedge{}\msubb{}  (r1  ff));
                      FormAll(x,b){}\mRightarrow{}  r1.\mlambda{}isterm.((\mneg{}\msubb{}isterm)  \mwedge{}\msubb{}  (r1  ff));
                      FormExists(x,b){}\mRightarrow{}  r1.\mlambda{}isterm.((\mneg{}\msubb{}isterm)  \mwedge{}\msubb{}  (r1  ff))) 


Date html generated: 2018_05_21-PM-11_26_39
Last ObjectModification: 2017_10_10-PM-04_59_20

Theory : PZF


Home Index