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.((∃theta:Atom List
                                       (l_subset(Atom;theta;vs-FormFvs(b)) ∧ (ra theta) ∧ (rb vs-theta)))
                                    ∨ (∃phi:Atom List. (l_subset(Atom;phi;vs-FormFvs(a)) ∧ (ra vs-phi) ∧ (rb phi))));
           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),  list-diff: as-bs,  set-equal: set-equal(T;x;y),  l_subset: l_subset(T;as;bs),  l_member: (x ∈ l),  null: null(as),  cons: [a / b],  nil: [],  list: T List,  atom-deq: AtomDeq,  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 :  lambda: λx.A[x],  apply: f a,  atom-deq: AtomDeq,  list-diff: as-bs,  and: P ∧ Q,  FormFvs: FormFvs(f),  atom: Atom,  l_subset: l_subset(T;as;bs),  list: T List,  exists: ∃x:A. B[x],  or: P ∨ Q,  l_member: (x ∈ l),  not: ¬A,  FormVar-name: FormVar-name(v),  equal: s = t ∈ T,  FormVar?: FormVar?(v),  assert: ↑b,  nil: [],  cons: [a / b],  set-equal: set-equal(T;x;y),  null: null(as),  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{}theta:Atom  List
                                                                              (l\_subset(Atom;theta;vs-FormFvs(b))
                                                                              \mwedge{}  (ra  theta)
                                                                              \mwedge{}  (rb  vs-theta)))
                                                                        \mvee{}  (\mexists{}phi:Atom  List
                                                                                (l\_subset(Atom;phi;vs-FormFvs(a))
                                                                                \mwedge{}  (ra  vs-phi)
                                                                                \mwedge{}  (rb  phi))));
                      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_29_05
Last ObjectModification: 2017_10_12-AM-00_15_15

Theory : PZF


Home Index