Nuprl Definition : FormSafe1

FormSafe1(f) ==
  Form_ind(f;
           FormVar(v)⇒ λvs.False;
           FormConst(c)⇒ λvs.False;
           FormSet(x,phi)⇒ r.λvs.False;
           FormEqual(a,b)⇒ ra,rb.λvs.((↑null(vs))
                                      ∨ (∃x:Atom
                                          (set-equal(Atom;vs;[x])
                                          ∧ (((↑FormVar?(a)) ∧ (FormVar-name(a) = x ∈ Atom) ∧ (¬(x ∈ FormFvs(b))))
                                            ∨ ((↑FormVar?(b)) ∧ (FormVar-name(b) = x ∈ Atom) ∧ (¬(x ∈ FormFvs(a))))))));
           FormMember(a,b)⇒ ra,rb.λvs.((↑null(vs))
                                       ∨ (∃x:Atom
                                           (set-equal(Atom;vs;[x])
                                           ∧ (↑FormVar?(a))
                                           ∧ (FormVar-name(a) = x ∈ Atom)
                                           ∧ (((↑FormVar?(b)) ∧ (FormVar-name(b) = x ∈ Atom)) ∨ (¬(x ∈ FormFvs(b)))))));
           FormAnd(a,b)⇒ ra,rb.λvs.∃as,bs:Atom List
                                     (set-equal(Atom;vs;as @ bs)
                                     ∧ (ra as)
                                     ∧ (rb bs)
                                     ∧ (l_disjoint(Atom;as;FormFvs(b)) ∨ l_disjoint(Atom;bs;FormFvs(a))));
           FormOr(a,b)⇒ ra,rb.λvs.((ra vs) ∧ (rb vs));
           FormNot(a)⇒ ra.λvs.((↑null(vs)) ∧ (ra []));
           FormAll(x,phi)⇒ r.λvs.False;
           FormExists(x,phi)⇒ r.λvs.((¬(x ∈ vs)) ∧ (r [x / vs]))) 


Definitions occuring in Statement :  FormFvs: FormFvs(f),  Form_ind: Form_ind,  FormVar-name: FormVar-name(v),  FormVar?: FormVar?(v),  set-equal: set-equal(T;x;y),  l_disjoint: l_disjoint(T;l1;l2),  l_member: (x ∈ l),  null: null(as),  append: as @ bs,  cons: [a / b],  nil: [],  list: T List,  assert: ↑b,  exists: ∃x:A. B[x],  not: ¬A,  or: P ∨ Q,  and: P ∧ Q,  false: False,  apply: f a,  lambda: λx.A[x],  atom: Atom,  equal: s = t ∈ T
Definitions occuring in definition :  apply: f a,  null: null(as),  assert: ↑b,  and: P ∧ Q,  lambda: λx.A[x],  FormFvs: FormFvs(f),  atom: Atom,  l_disjoint: l_disjoint(T;l1;l2),  or: P ∨ Q,  append: as @ bs,  set-equal: set-equal(T;x;y),  list: T List,  exists: ∃x:A. B[x],  l_member: (x ∈ l),  not: ¬A,  FormVar-name: FormVar-name(v),  equal: s = t ∈ T,  FormVar?: FormVar?(v),  nil: [],  cons: [a / b],  false: False,  Form_ind: Form_ind
FDL editor aliases :  FormSafe1 FormSafe1
Latex:
FormSafe1(f)  ==
    Form\_ind(f;
                      FormVar(v){}\mRightarrow{}  \mlambda{}vs.False;
                      FormConst(c){}\mRightarrow{}  \mlambda{}vs.False;
                      FormSet(x,phi){}\mRightarrow{}  r.\mlambda{}vs.False;
                      FormEqual(a,b){}\mRightarrow{}  ra,rb.\mlambda{}vs.((\muparrow{}null(vs))
                                                                            \mvee{}  (\mexists{}x:Atom
                                                                                    (set-equal(Atom;vs;[x])
                                                                                    \mwedge{}  (((\muparrow{}FormVar?(a))
                                                                                        \mwedge{}  (FormVar-name(a)  =  x)
                                                                                        \mwedge{}  (\mneg{}(x  \mmember{}  FormFvs(b))))
                                                                                        \mvee{}  ((\muparrow{}FormVar?(b))
                                                                                            \mwedge{}  (FormVar-name(b)  =  x)
                                                                                            \mwedge{}  (\mneg{}(x  \mmember{}  FormFvs(a))))))));
                      FormMember(a,b){}\mRightarrow{}  ra,rb.\mlambda{}vs.((\muparrow{}null(vs))
                                                                              \mvee{}  (\mexists{}x:Atom
                                                                                      (set-equal(Atom;vs;[x])
                                                                                      \mwedge{}  (\muparrow{}FormVar?(a))
                                                                                      \mwedge{}  (FormVar-name(a)  =  x)
                                                                                      \mwedge{}  (((\muparrow{}FormVar?(b))  \mwedge{}  (FormVar-name(b)  =  x))
                                                                                          \mvee{}  (\mneg{}(x  \mmember{}  FormFvs(b)))))));
                      FormAnd(a,b){}\mRightarrow{}  ra,rb.\mlambda{}vs.\mexists{}as,bs:Atom  List
                                                                          (set-equal(Atom;vs;as  @  bs)
                                                                          \mwedge{}  (ra  as)
                                                                          \mwedge{}  (rb  bs)
                                                                          \mwedge{}  (l\_disjoint(Atom;as;FormFvs(b))
                                                                              \mvee{}  l\_disjoint(Atom;bs;FormFvs(a))));
                      FormOr(a,b){}\mRightarrow{}  ra,rb.\mlambda{}vs.((ra  vs)  \mwedge{}  (rb  vs));
                      FormNot(a){}\mRightarrow{}  ra.\mlambda{}vs.((\muparrow{}null(vs))  \mwedge{}  (ra  []));
                      FormAll(x,phi){}\mRightarrow{}  r.\mlambda{}vs.False;
                      FormExists(x,phi){}\mRightarrow{}  r.\mlambda{}vs.((\mneg{}(x  \mmember{}  vs))  \mwedge{}  (r  [x  /  vs]))) 


Date html generated: 2018_05_21-PM-11_27_08
Last ObjectModification: 2017_10_11-PM-09_21_55

Theory : PZF


Home Index