Nuprl Lemma : not-member-mFOL-sequent-freevars
∀s:mFOL-sequent(). ∀v:ℤ.
(¬(v ∈ mFOL-sequent-freevars(s)) ⇐⇒ (¬(v ∈ mFOL-freevars(snd(s)))) ∧ (∀h∈fst(s).¬(v ∈ mFOL-freevars(h))))
Proof
Definitions occuring in Statement :
mFOL-sequent-freevars: mFOL-sequent-freevars(s),
mFOL-sequent: mFOL-sequent(),
mFOL-freevars: mFOL-freevars(fmla),
l_all: (∀x∈L.P[x]),
l_member: (x ∈ l),
pi1: fst(t),
pi2: snd(t),
all: ∀x:A. B[x],
iff: P ⇐⇒ Q,
not: ¬A,
and: P ∧ Q,
int: ℤ
Definitions unfolded in proof :
all: ∀x:A. B[x],
mFOL-sequent: mFOL-sequent(),
mFOL-sequent-freevars: mFOL-sequent-freevars(s),
pi2: snd(t),
pi1: fst(t),
member: t ∈ T,
uall: ∀[x:A]. B[x],
implies: P ⇒ Q,
so_lambda: λ2x.t[x],
prop: ℙ,
and: P ∧ Q,
so_apply: x[s],
top: Top,
iff: P ⇐⇒ Q,
uiff: uiff(P;Q),
uimplies: b supposing a,
rev_implies: P ⇐ Q,
subtype_rel: A ⊆r B,
not: ¬A,
or: P ∨ Q,
true: True,
false: False,
l_all: (∀x∈L.P[x]),
guard: {T},
cand: A c∧ B
Lemmas referenced :
mFOL-freevars_wf,
list_wf,
list_induction,
mFOL_wf,
all_wf,
iff_wf,
not_wf,
l_member_wf,
reduce_wf,
l-union_wf,
int-deq_wf,
l_all_wf2,
reduce_nil_lemma,
l_all_nil_iff,
nil_wf,
subtype_rel_set,
true_wf,
reduce_cons_lemma,
member-union,
or_wf,
l_all_cons,
cons_wf,
equal_wf,
mFOL-sequent_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
lambdaFormation,
sqequalHypSubstitution,
productElimination,
thin,
sqequalRule,
cut,
introduction,
extract_by_obid,
isectElimination,
hypothesisEquality,
hypothesis,
intEquality,
lambdaEquality,
because_Cache,
productEquality,
setElimination,
rename,
setEquality,
independent_functionElimination,
dependent_functionElimination,
isect_memberEquality,
voidElimination,
voidEquality,
addLevel,
allFunctionality,
independent_pairFormation,
impliesFunctionality,
independent_isectElimination,
andLevelFunctionality,
applyEquality,
functionExtensionality,
impliesLevelFunctionality,
equalityTransitivity,
equalitySymmetry,
natural_numberEquality,
inrFormation,
inlFormation,
unionElimination
Latex:
\mforall{}s:mFOL-sequent(). \mforall{}v:\mBbbZ{}.
(\mneg{}(v \mmember{} mFOL-sequent-freevars(s))
\mLeftarrow{}{}\mRightarrow{} (\mneg{}(v \mmember{} mFOL-freevars(snd(s)))) \mwedge{} (\mforall{}h\mmember{}fst(s).\mneg{}(v \mmember{} mFOL-freevars(h))))
Date html generated:
2018_05_21-PM-10_29_30
Last ObjectModification:
2017_07_26-PM-06_41_38
Theory : minimal-first-order-logic
Home
Index