Nuprl Lemma : subst-term_functionality
∀[opr:Type]
∀t1,t2:term(opr). ∀s1,s2:(varname() × term(opr)) List.
(alpha-eq-terms(opr;t1;t2) ⇒ equiv-substs(opr;s1;s2) ⇒ alpha-eq-terms(opr;subst-term(s1;t1);subst-term(s2;t2)))
Proof
Definitions occuring in Statement :
subst-term: subst-term(s;t),
equiv-substs: equiv-substs(opr;s1;s2),
alpha-eq-terms: alpha-eq-terms(opr;a;b),
term: term(opr),
varname: varname(),
list: T List,
uall: ∀[x:A]. B[x],
all: ∀x:A. B[x],
implies: P ⇒ Q,
product: x:A × B[x],
universe: Type
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
all: ∀x:A. B[x],
implies: P ⇒ Q,
subst-term: subst-term(s;t),
member: t ∈ T,
guard: {T},
so_lambda: λ2x.t[x],
prop: ℙ,
subtype_rel: A ⊆r B,
so_apply: x[s],
uimplies: b supposing a,
not: ¬A,
false: False,
alpha-aux: alpha-aux(opr;vs;ws;a;b),
varterm: varterm(v),
mkterm: mkterm(opr;bts),
bound-term: bound-term(opr),
pi2: snd(t),
alpha-eq-terms: alpha-eq-terms(opr;a;b),
replace-vars: replace-vars(s;t),
vars-of-subst: vars-of-subst(s),
iff: P ⇐⇒ Q,
and: P ∧ Q,
rev_implies: P ⇐ Q,
exists: ∃x:A. B[x],
cand: A c∧ B,
bool: 𝔹,
unit: Unit,
it: ⋅,
btrue: tt,
uiff: uiff(P;Q),
ifthenelse: if b then t else f fi ,
bfalse: ff,
or: P ∨ Q,
sq_type: SQType(T),
bnot: ¬bb,
assert: ↑b,
l_disjoint: l_disjoint(T;l1;l2),
squash: ↓T,
true: True,
sq_stable: SqStable(P),
equiv-substs: equiv-substs(opr;s1;s2),
isl: isl(x),
outl: outl(x),
free-vars: free-vars(t),
append: as @ bs,
list_ind: list_ind,
nil: [],
so_lambda: so_lambda3,
so_apply: x[s1;s2;s3],
nat: ℕ,
free-vars-aux: free-vars-aux(bnds;t),
l_member: (x ∈ l),
le: A ≤ B,
less_than': less_than'(a;b),
select: L[n],
cons: [a / b],
less_than: a < b,
ge: i ≥ j ,
decidable: Dec(P),
satisfiable_int_formula: satisfiable_int_formula(fmla),
colength: colength(L),
so_lambda: λ2x y.t[x; y],
so_apply: x[s1;s2],
same-binding: same-binding(vs;ws;v;w),
rev_uimplies: rev_uimplies(P;Q),
band: p ∧b q,
int_seg: {i..j-},
lelt: i ≤ j < k,
pi1: fst(t),
reverse: rev(as),
respects-equality: respects-equality(S;T),
has-value: (a)↓,
binders-disjoint: binders-disjoint(opr;L;t)
Lemmas referenced :
subst-frame-alpha,
alpha-eq-terms_inversion,
subst-frame_wf,
alpha-eq-terms_transitivity,
subst-frame-binders-disjoint,
term-induction,
term_wf,
list_wf,
varname_wf,
l_disjoint_wf,
vars-of-subst_wf,
alpha-aux_wf,
binders-disjoint_wf,
replace-vars_wf,
varterm_wf,
subtype_rel_list,
not_wf,
equal-wf-T-base,
nullvar_wf,
mkterm_wf,
bound-term_wf,
l_member_wf,
istype-void,
nil_wf,
l_disjoint_nil,
alpha-eq-terms_wf,
equiv-substs_wf,
istype-universe,
apply-alist_wf,
var-deq_wf,
apply-alist-inl,
member-l-union-list,
map_wf,
ifthenelse_wf,
eq_var_wf,
free-vars_wf,
insert_wf,
eqtt_to_assert,
assert-eq_var,
eqff_to_assert,
bool_cases_sqequal,
subtype_base_sq,
bool_wf,
bool_subtype_base,
assert-bnot,
iff_weakening_uiff,
assert_wf,
member-map,
same-binding-not-bound,
member-insert,
squash_wf,
true_wf,
equal_wf,
unit_wf2,
deq_wf,
iff_weakening_equal,
inl-one-one,
not-0-eq-1,
inr-one-one,
sq_stable__not,
subtype_rel_self,
btrue_wf,
bfalse_wf,
outl_wf,
isl_wf,
btrue_neq_bfalse,
length_wf,
list_ind_nil_lemma,
append_back_nil,
equal-wf-base,
length_wf_nat,
set_subtype_base,
le_wf,
istype-int,
int_subtype_base,
append_wf,
free-vars-aux_wf,
deq-member_wf,
assert-deq-member,
istype-le,
length_of_cons_lemma,
length_of_nil_lemma,
cons_wf,
istype-less_than,
select_wf,
nat_properties,
decidable__le,
full-omega-unsat,
intformand_wf,
intformnot_wf,
intformle_wf,
itermConstant_wf,
itermVar_wf,
int_formula_prop_and_lemma,
int_formula_prop_not_lemma,
int_formula_prop_le_lemma,
int_term_value_constant_lemma,
int_term_value_var_lemma,
int_formula_prop_wf,
intformless_wf,
int_formula_prop_less_lemma,
ge_wf,
assert_witness,
intformeq_wf,
int_formula_prop_eq_lemma,
list-cases,
product_subtype_list,
colength-cons-not-zero,
same-binding_wf,
subtract-1-ge-0,
spread_cons_lemma,
list_ind_cons_lemma,
non_neg_length,
itermAdd_wf,
int_term_value_add_lemma,
colength_wf_list,
decidable__equal_int,
subtract_wf,
itermSubtract_wf,
int_term_value_subtract_lemma,
istype-nat,
istype-assert,
member-implies-null-eq-bfalse,
null_nil_lemma,
cons_member,
add-is-int-iff,
false_wf,
alpha-aux-mkterm,
rev-append-as-reverse,
append_assoc,
int_seg_wf,
int_seg_properties,
decidable__lt,
select_member,
reverse_wf,
length-append,
length-reverse,
rev-append-property,
rev-append_wf,
respects-equality-list,
respects-equality-set-trivial2,
same-binding-symm,
product-value-type,
value-type-has-value,
list-value-type,
select-map,
top_wf,
eager-map-is-map,
map-length,
int_seg_subtype_nat,
istype-false,
l_disjoint_append2,
l_all_iff,
member-reverse
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation_alt,
lambdaFormation_alt,
cut,
introduction,
extract_by_obid,
sqequalHypSubstitution,
isectElimination,
thin,
hypothesisEquality,
dependent_functionElimination,
hypothesis,
independent_functionElimination,
inhabitedIsType,
sqequalRule,
lambdaEquality_alt,
functionEquality,
applyEquality,
because_Cache,
universeIsType,
setElimination,
rename,
independent_isectElimination,
voidElimination,
setEquality,
baseClosed,
equalityTransitivity,
equalitySymmetry,
equalityIstype,
functionIsType,
productElimination,
setIsType,
productEquality,
instantiate,
universeEquality,
unionElimination,
spreadEquality,
productIsType,
dependent_pairFormation_alt,
independent_pairEquality,
independent_pairFormation,
equalityElimination,
promote_hyp,
cumulativity,
inlFormation_alt,
imageElimination,
unionEquality,
natural_numberEquality,
imageMemberEquality,
applyLambdaEquality,
dependent_set_memberEquality_alt,
unionIsType,
sqequalBase,
inrFormation_alt,
voidEquality,
Error :memTop,
intEquality,
approximateComputation,
int_eqEquality,
intWeakElimination,
functionIsTypeImplies,
hypothesis_subsumption,
addEquality,
baseApply,
closedConclusion,
hyp_replacement,
pointwiseFunctionality,
callbyvalueReduce
Latex:
\mforall{}[opr:Type]
\mforall{}t1,t2:term(opr). \mforall{}s1,s2:(varname() \mtimes{} term(opr)) List.
(alpha-eq-terms(opr;t1;t2)
{}\mRightarrow{} equiv-substs(opr;s1;s2)
{}\mRightarrow{} alpha-eq-terms(opr;subst-term(s1;t1);subst-term(s2;t2)))
Date html generated:
2020_05_19-PM-09_58_06
Last ObjectModification:
2020_03_09-PM-04_10_09
Theory : terms
Home
Index