Nuprl Lemma : mFOL-rename-bound-to-avoid_wf
∀fmla:mFOL(). ∀L:ℤ List.
(mFOL-rename-bound-to-avoid(fmla;L) ∈ {fmla':mFOL()|
(mFOL-freevars(fmla') = mFOL-freevars(fmla) ∈ (ℤ List))
∧ (mFOL-abstract(fmla')
= mFOL-abstract(fmla)
∈ AbstractFOFormula(mFOL-freevars(fmla)))
∧ l_disjoint(ℤ;L;mFOL-boundvars(fmla'))} )
Proof
Definitions occuring in Statement :
mFOL-rename-bound-to-avoid: mFOL-rename-bound-to-avoid(fmla;L),
mFOL-abstract: mFOL-abstract(fmla),
mFOL-boundvars: mFOL-boundvars(fmla),
mFOL-freevars: mFOL-freevars(fmla),
mFOL: mFOL(),
AbstractFOFormula: AbstractFOFormula(vs),
l_disjoint: l_disjoint(T;l1;l2),
list: T List,
all: ∀x:A. B[x],
and: P ∧ Q,
member: t ∈ T,
set: {x:A| B[x]} ,
int: ℤ,
equal: s = t ∈ T
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
mFOL-rename-bound-to-avoid: mFOL-rename-bound-to-avoid(fmla;L),
member: t ∈ T,
all: ∀x:A. B[x],
mFOL-bound-rename,
mFOL-induction,
uniform-comp-nat-induction,
mFOL-ext,
eq_atom: x =a y,
any: any x,
decidable__l_member,
list_induction,
decidable_functionality,
iff_preserves_decidability,
nil_member,
so_lambda: so_lambda4,
so_apply: x[s1;s2;s3;s4],
uimplies: b supposing a,
so_lambda: λ2x y.t[x; y],
so_apply: x[s1;s2],
cons_member,
decidable__or,
ifthenelse: if b then t else f fi ,
null: null(as),
implies: P ⇒ Q,
subtype_rel: A ⊆r B,
sq_exists: ∃x:A [B[x]],
so_apply: x[s],
so_lambda: λ2x.t[x],
and: P ∧ Q,
prop: ℙ
Lemmas referenced :
list_wf,
lifting-strict-spread,
strict4-apply,
mFOL-bound-rename,
sq_exists_subtype_rel,
mFOL-boundvars_wf,
l_disjoint_wf,
mFOL-abstract_wf,
AbstractFOFormula_wf,
equal_wf,
length_wf,
int_subtype_base,
list_subtype_base,
mFOL-freevars_wf,
equal-wf-base,
mFOL_wf,
mFOL-induction,
uniform-comp-nat-induction,
mFOL-ext,
decidable__l_member,
list_induction,
decidable_functionality,
iff_preserves_decidability,
nil_member,
cons_member,
decidable__or
Rules used in proof :
because_Cache,
intEquality,
thin,
isectElimination,
extract_by_obid,
introduction,
universeIsType,
hypothesis,
sqequalHypSubstitution,
sqequalRule,
cut,
lambdaFormation_alt,
sqequalReflexivity,
computationStep,
sqequalTransitivity,
sqequalSubstitution,
baseClosed,
Error :memTop,
independent_isectElimination,
independent_functionElimination,
dependent_functionElimination,
equalitySymmetry,
equalityTransitivity,
hypothesisEquality,
equalityIstype,
inhabitedIsType,
instantiate,
applyEquality,
sqequalBase,
productIsType,
closedConclusion,
applyLambdaEquality,
productEquality,
lambdaEquality_alt,
cumulativity
Latex:
\mforall{}fmla:mFOL(). \mforall{}L:\mBbbZ{} List.
(mFOL-rename-bound-to-avoid(fmla;L) \mmember{} \{fmla':mFOL()|
(mFOL-freevars(fmla') = mFOL-freevars(fmla))
\mwedge{} (mFOL-abstract(fmla') = mFOL-abstract(fmla))
\mwedge{} l\_disjoint(\mBbbZ{};L;mFOL-boundvars(fmla'))\} )
Date html generated:
2020_05_20-AM-09_08_36
Last ObjectModification:
2020_01_17-AM-09_42_27
Theory : minimal-first-order-logic
Home
Index