### Nuprl Lemma : rename-one-extend-name-morph

`∀I,K:Cname List. ∀f:name-morph(I;K). ∀x,y,z:Cname.`
`  ((¬(x ∈ I)) `` (¬(z ∈ K)) `` (¬(y ∈ K)) `` ((f[x:=y] o rename-one-name(y;z)) = f[x:=z] ∈ name-morph([x / I];[z / K])))`

Proof

Definitions occuring in Statement :  rename-one-name: `rename-one-name(z1;z2)` name-comp: `(f o g)` extend-name-morph: `f[z1:=z2]` name-morph: `name-morph(I;J)` coordinate_name: `Cname` l_member: `(x ∈ l)` cons: `[a / b]` list: `T List` all: `∀x:A. B[x]` not: `¬A` implies: `P `` Q` equal: `s = t ∈ T`
Definitions unfolded in proof :  all: `∀x:A. B[x]` implies: `P `` Q` uall: `∀[x:A]. B[x]` member: `t ∈ T` uimplies: `b supposing a` and: `P ∧ Q` cand: `A c∧ B` subtype_rel: `A ⊆r B` name-morph: `name-morph(I;J)` extend-name-morph: `f[z1:=z2]` rename-one-name: `rename-one-name(z1;z2)` name-comp: `(f o g)` compose: `f o g` uext: `uext(g)` nameset: `nameset(L)` bool: `𝔹` unit: `Unit` it: `⋅` btrue: `tt` uiff: `uiff(P;Q)` ifthenelse: `if b then t else f fi ` bfalse: `ff` exists: `∃x:A. B[x]` or: `P ∨ Q` sq_type: `SQType(T)` guard: `{T}` bnot: `¬bb` assert: `↑b` false: `False` not: `¬A` rev_implies: `P `` Q` coordinate_name: `Cname` int_upper: `{i...}` so_lambda: `λ2x.t[x]` so_apply: `x[s]` iff: `P `⇐⇒` Q` prop: `ℙ` isname: `isname(z)` true: `True` l_member: `(x ∈ l)` nat: `ℕ` le: `A ≤ B` less_than': `less_than'(a;b)` top: `Top` select: `L[n]` cons: `[a / b]` nat_plus: `ℕ+` squash: `↓T` decidable: `Dec(P)` satisfiable_int_formula: `satisfiable_int_formula(fmla)` sq_stable: `SqStable(P)` ge: `i ≥ j ` respects-equality: `respects-equality(S;T)`
Lemmas referenced :  name-morphs-equal cons_wf coordinate_name_wf name-comp_wf extend-name-morph_wf rename-one-name_wf eq-cname_wf eqtt_to_assert assert-eq-cname eqff_to_assert bool_cases_sqequal subtype_base_sq bool_wf bool_subtype_base assert-bnot iff_weakening_uiff assert_wf equal-wf-T-base set_subtype_base le_wf istype-int int_subtype_base nameset_wf l_member_wf istype-void name-morph_wf list_wf iff_imp_equal_bool le_int_wf btrue_wf iff_functionality_wrt_iff true_wf assert_of_le_int iff_weakening_equal istype-true equal-wf-base istype-le length_of_cons_lemma add_nat_plus length_wf_nat decidable__lt full-omega-unsat intformnot_wf intformless_wf itermConstant_wf int_formula_prop_not_lemma int_formula_prop_less_lemma int_term_value_constant_lemma int_formula_prop_wf istype-less_than nat_plus_properties add-is-int-iff intformand_wf itermVar_wf itermAdd_wf intformeq_wf int_formula_prop_and_lemma int_term_value_var_lemma int_term_value_add_lemma int_formula_prop_eq_lemma false_wf length_wf select_wf nat_properties sq_stable__le sq_stable__l_member decidable__equal-coordinate_name decidable__le intformle_wf int_formula_prop_le_lemma nameset_subtype_extd-nameset cons_member isname_wf assert-isname respects-equality-set-trivial2 extd-nameset_subtype l_subset_right_cons_trivial
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation_alt cut introduction extract_by_obid sqequalHypSubstitution isectElimination thin hypothesis hypothesisEquality because_Cache independent_isectElimination independent_pairFormation applyEquality lambdaEquality_alt setElimination rename inhabitedIsType equalityTransitivity equalitySymmetry sqequalRule functionExtensionality unionElimination equalityElimination productElimination dependent_pairFormation_alt equalityIstype promote_hyp dependent_functionElimination instantiate cumulativity independent_functionElimination voidElimination intEquality natural_numberEquality functionIsType universeIsType dependent_set_memberEquality_alt isect_memberEquality_alt applyLambdaEquality imageMemberEquality baseClosed imageElimination approximateComputation Error :memTop,  pointwiseFunctionality baseApply closedConclusion int_eqEquality productIsType sqequalBase

Latex:
\mforall{}I,K:Cname  List.  \mforall{}f:name-morph(I;K).  \mforall{}x,y,z:Cname.
((\mneg{}(x  \mmember{}  I))  {}\mRightarrow{}  (\mneg{}(z  \mmember{}  K))  {}\mRightarrow{}  (\mneg{}(y  \mmember{}  K))  {}\mRightarrow{}  ((f[x:=y]  o  rename-one-name(y;z))  =  f[x:=z]))

Date html generated: 2020_05_21-AM-10_49_50
Last ObjectModification: 2019_12_08-PM-07_06_16

Theory : cubical!sets

Home Index