Nuprl Definition : FormSafe2

FormSafe2(f) ==
  Form_ind(f;
           FormVar(v)⇒ λvs.ff;
           FormConst(c)⇒ λvs.ff;
           FormSet(x,phi)⇒ r.λvs.ff;
           FormEqual(a,b)⇒ ra,rb.λvs.(null(vs)
                                      ∨blet x = hd(vs) in
                                            null(vs-[x])
                                            ∧b ((FormVar?(a) ∧b FormVar-name(a) =a x ∧b (¬bx ∈b FormFvs(b)))
                                               ∨b(FormVar?(b) ∧b FormVar-name(b) =a x ∧b (¬bx ∈b FormFvs(a)))));
           FormMember(a,b)⇒ ra,rb.λvs.(null(vs)
                                       ∨blet x = hd(vs) in
                                             null(vs-[x])
                                             ∧b FormVar?(a)
                                             ∧b FormVar-name(a) =a x
                                             ∧b ((FormVar?(b) ∧b FormVar-name(b) =a x) ∨b(¬bx ∈b FormFvs(b))));
           FormAnd(a,b)⇒ ra,rb.λvs.eval as = FormFvs(a) in
                                    eval bs = FormFvs(b) in
                                      eval theta = vs-bs in
                                      (ra theta) ∧b (rb vs-theta)
                                      ∨beval phi = vs-as in
                                        (ra vs-phi) ∧b (rb phi);
           FormOr(a,b)⇒ ra,rb.λvs.((ra vs) ∧b (rb vs));
           FormNot(a)⇒ ra.λvs.(null(vs) ∧b (ra []));
           FormAll(x,phi)⇒ r.λvs.ff;
           FormExists(x,phi)⇒ r.λvs.((¬bx ∈b vs) ∧b (r [x / vs]))) 


Definitions occuring in Statement :  FormFvs: FormFvs(f),  Form_ind: Form_ind,  FormVar-name: FormVar-name(v),  FormVar?: FormVar?(v),  list-diff: as-bs,  hd: hd(l),  null: null(as),  deq-member: x ∈b L,  cons: [a / b],  nil: [],  atom-deq: AtomDeq,  bor: p ∨bq,  band: p ∧b q,  callbyvalue: callbyvalue,  bnot: ¬bb,  eq_atom: x =a y,  bfalse: ff,  let: let,  apply: f a,  lambda: λx.A[x]
Definitions occuring in definition :  apply: f a,  atom-deq: AtomDeq,  deq-member: x ∈b L,  bnot: ¬bb,  band: p ∧b q,  lambda: λx.A[x],  bfalse: ff,  nil: [],  null: null(as),  list-diff: as-bs,  callbyvalue: callbyvalue,  bor: p ∨bq,  FormFvs: FormFvs(f),  FormVar-name: FormVar-name(v),  eq_atom: x =a y,  FormVar?: FormVar?(v),  cons: [a / b],  hd: hd(l),  let: let,  Form_ind: Form_ind
FDL editor aliases :  FormSafe2 FormSafe2
Latex:
FormSafe2(f)  ==
    Form\_ind(f;
                      FormVar(v){}\mRightarrow{}  \mlambda{}vs.ff;
                      FormConst(c){}\mRightarrow{}  \mlambda{}vs.ff;
                      FormSet(x,phi){}\mRightarrow{}  r.\mlambda{}vs.ff;
                      FormEqual(a,b){}\mRightarrow{}  ra,rb.\mlambda{}vs.(null(vs)
                                                                            \mvee{}\msubb{}let  x  =  hd(vs)  in
                                                                                        null(vs-[x])
                                                                                        \mwedge{}\msubb{}  ((FormVar?(a)
                                                                                              \mwedge{}\msubb{}  FormVar-name(a)  =a  x
                                                                                              \mwedge{}\msubb{}  (\mneg{}\msubb{}x  \mmember{}\msubb{}  FormFvs(b)))
                                                                                              \mvee{}\msubb{}(FormVar?(b)
                                                                                                  \mwedge{}\msubb{}  FormVar-name(b)  =a  x
                                                                                                  \mwedge{}\msubb{}  (\mneg{}\msubb{}x  \mmember{}\msubb{}  FormFvs(a)))));
                      FormMember(a,b){}\mRightarrow{}  ra,rb.\mlambda{}vs.(null(vs)
                                                                              \mvee{}\msubb{}let  x  =  hd(vs)  in
                                                                                          null(vs-[x])
                                                                                          \mwedge{}\msubb{}  FormVar?(a)
                                                                                          \mwedge{}\msubb{}  FormVar-name(a)  =a  x
                                                                                          \mwedge{}\msubb{}  ((FormVar?(b)  \mwedge{}\msubb{}  FormVar-name(b)  =a  x)
                                                                                                \mvee{}\msubb{}(\mneg{}\msubb{}x  \mmember{}\msubb{}  FormFvs(b))));
                      FormAnd(a,b){}\mRightarrow{}  ra,rb.\mlambda{}vs.eval  as  =  FormFvs(a)  in
                                                                        eval  bs  =  FormFvs(b)  in
                                                                            eval  theta  =  vs-bs  in
                                                                            (ra  theta)  \mwedge{}\msubb{}  (rb  vs-theta)
                                                                            \mvee{}\msubb{}eval  phi  =  vs-as  in
                                                                                (ra  vs-phi)  \mwedge{}\msubb{}  (rb  phi);
                      FormOr(a,b){}\mRightarrow{}  ra,rb.\mlambda{}vs.((ra  vs)  \mwedge{}\msubb{}  (rb  vs));
                      FormNot(a){}\mRightarrow{}  ra.\mlambda{}vs.(null(vs)  \mwedge{}\msubb{}  (ra  []));
                      FormAll(x,phi){}\mRightarrow{}  r.\mlambda{}vs.ff;
                      FormExists(x,phi){}\mRightarrow{}  r.\mlambda{}vs.((\mneg{}\msubb{}x  \mmember{}\msubb{}  vs)  \mwedge{}\msubb{}  (r  [x  /  vs]))) 


Date html generated: 2018_05_21-PM-11_30_06
Last ObjectModification: 2017_10_12-PM-03_56_21

Theory : PZF


Home Index