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.(let theta = vs-FormFvs(b) in
(ra theta) ∧ (rb vs-theta)
∨ let phi = vs-FormFvs(a) in
(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_member: (x ∈ l),
null: null(as),
cons: [a / b],
nil: [],
atom-deq: AtomDeq,
assert: ↑b,
let: let,
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],
nil: [],
apply: f a,
null: null(as),
assert: ↑b,
and: P ∧ Q,
atom-deq: AtomDeq,
list-diff: as-bs,
FormFvs: FormFvs(f),
let: let,
or: P ∨ Q,
atom: Atom,
l_member: (x ∈ l),
not: ¬A,
FormVar-name: FormVar-name(v),
equal: s = t ∈ T,
FormVar?: FormVar?(v),
cons: [a / b],
set-equal: set-equal(T;x;y),
exists: ∃x:A. B[x],
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.(let theta = vs-FormFvs(b) in
(ra theta) \mwedge{} (rb vs-theta)
\mvee{} let phi = vs-FormFvs(a) in
(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_24
Last ObjectModification:
2017_10_12-PM-03_33_26
Theory : PZF
Home
Index