Nuprl Lemma : alpha-rename-binders-disjoint
∀[opr:Type]
∀L:varname() List. ∀t:term(opr). ∀f:{v:varname()| (v ∈ all-vars(t))} ⟶ varname().
((∀x:{v:varname()| (v ∈ all-vars(t))}
((((f x) = nullvar() ∈ varname()) ⇒ (x = nullvar() ∈ varname())) ∧ (¬(f x ∈ L))))
⇒ binders-disjoint(opr;L;alpha-rename(f;t)))
Proof
Definitions occuring in Statement :
alpha-rename: alpha-rename(f;t),
binders-disjoint: binders-disjoint(opr;L;t),
all-vars: all-vars(t),
term: term(opr),
nullvar: nullvar(),
varname: varname(),
l_member: (x ∈ l),
list: T List,
uall: ∀[x:A]. B[x],
all: ∀x:A. B[x],
not: ¬A,
implies: P ⇒ Q,
and: P ∧ Q,
set: {x:A| B[x]} ,
apply: f a,
function: x:A ⟶ B[x],
universe: Type,
equal: s = t ∈ T
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
all: ∀x:A. B[x],
member: t ∈ T,
so_lambda: λ2x.t[x],
prop: ℙ,
implies: P ⇒ Q,
and: P ∧ Q,
guard: {T},
so_apply: x[s],
uimplies: b supposing a,
not: ¬A,
false: False,
alpha-rename-aux: alpha-rename-aux(f;bnds;t),
varterm: varterm(v),
bool: 𝔹,
unit: Unit,
it: ⋅,
btrue: tt,
uiff: uiff(P;Q),
iff: P ⇐⇒ Q,
ifthenelse: if b then t else f fi ,
binders-disjoint: binders-disjoint(opr;L;t),
true: True,
bfalse: ff,
exists: ∃x:A. B[x],
or: P ∨ Q,
sq_type: SQType(T),
bnot: ¬bb,
assert: ↑b,
rev_implies: P ⇐ Q,
mkterm: mkterm(opr;bts),
bound-term: bound-term(opr),
pi2: snd(t),
append: as @ bs,
so_lambda: so_lambda3,
so_apply: x[s1;s2;s3],
alpha-rename: alpha-rename(f;t),
istype: istype(T),
pi1: fst(t),
cand: A c∧ B,
subtype_rel: A ⊆r B,
has-value: (a)↓,
satisfiable_int_formula: satisfiable_int_formula(fmla),
decidable: Dec(P),
squash: ↓T,
less_than: a < b,
le: A ≤ B,
lelt: i ≤ j < k,
int_seg: {i..j-},
l_all: (∀x∈L.P[x]),
l_disjoint: l_disjoint(T;l1;l2)
Lemmas referenced :
term-induction,
all_wf,
list_wf,
varname_wf,
l_member_wf,
append_wf,
all-vars_wf,
equal-wf-T-base,
not_wf,
binders-disjoint_wf,
alpha-rename-aux_wf,
nullvar_wf,
term_wf,
varterm_wf,
deq-member_wf,
var-deq_wf,
eqtt_to_assert,
assert-deq-member,
eqff_to_assert,
bool_cases_sqequal,
subtype_base_sq,
bool_wf,
bool_subtype_base,
assert-bnot,
istype-void,
mkterm_wf,
bound-term_wf,
nil_wf,
list_ind_nil_lemma,
istype-universe,
list-subtype,
subtype_rel_dep_function,
map_wf,
member-all-vars-mkterm,
member_append,
rev-append_wf,
member-rev-append,
eager-map-is-map,
product-value-type,
list-value-type,
value-type-has-value,
int_seg_wf,
select_member,
int_formula_prop_less_lemma,
intformless_wf,
length_wf,
decidable__lt,
int_formula_prop_wf,
int_term_value_var_lemma,
int_term_value_constant_lemma,
int_formula_prop_le_lemma,
int_formula_prop_not_lemma,
int_formula_prop_and_lemma,
istype-int,
itermVar_wf,
itermConstant_wf,
intformle_wf,
intformnot_wf,
intformand_wf,
full-omega-unsat,
decidable__le,
int_seg_properties,
select_wf,
pi2_wf,
pi1_wf,
l_disjoint_wf,
subtype_rel_self,
l_all_map,
subtype_rel_list_set,
member-map,
iff_weakening_equal,
true_wf,
squash_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation_alt,
lambdaFormation_alt,
cut,
introduction,
extract_by_obid,
sqequalHypSubstitution,
isectElimination,
thin,
hypothesisEquality,
sqequalRule,
lambdaEquality_alt,
hypothesis,
functionEquality,
setEquality,
because_Cache,
universeIsType,
setElimination,
rename,
productEquality,
applyEquality,
dependent_set_memberEquality_alt,
dependent_functionElimination,
baseClosed,
setIsType,
independent_isectElimination,
equalityIstype,
functionIsType,
independent_functionElimination,
voidElimination,
inhabitedIsType,
unionElimination,
equalityElimination,
equalityTransitivity,
equalitySymmetry,
productElimination,
natural_numberEquality,
dependent_pairFormation_alt,
promote_hyp,
instantiate,
cumulativity,
productIsType,
Error :memTop,
universeEquality,
independent_pairEquality,
unionIsType,
inlFormation_alt,
independent_pairFormation,
inrFormation_alt,
callbyvalueReduce,
int_eqEquality,
approximateComputation,
imageElimination,
functionExtensionality,
imageMemberEquality,
functionIsTypeImplies,
axiomEquality
Latex:
\mforall{}[opr:Type]
\mforall{}L:varname() List. \mforall{}t:term(opr). \mforall{}f:\{v:varname()| (v \mmember{} all-vars(t))\} {}\mrightarrow{} varname().
((\mforall{}x:\{v:varname()| (v \mmember{} all-vars(t))\}
((((f x) = nullvar()) {}\mRightarrow{} (x = nullvar())) \mwedge{} (\mneg{}(f x \mmember{} L))))
{}\mRightarrow{} binders-disjoint(opr;L;alpha-rename(f;t)))
Date html generated:
2020_05_19-PM-09_57_04
Last ObjectModification:
2020_03_09-PM-04_09_32
Theory : terms
Home
Index