### Nuprl Lemma : extend-name-morph-comp

`∀I,J,K:Cname List. ∀f:name-morph(I;J). ∀g:name-morph(J;K). ∀z,v,v1:Cname.`
`  ((¬(z ∈ I)) `` (¬(v ∈ K)) `` (¬(v1 ∈ J)) `` ((f o g)[z:=v] = (f[z:=v1] o g[v1:=v]) ∈ name-morph([z / I];[v / K])))`

Proof

Definitions occuring in Statement :  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` subtype_rel: `A ⊆r B` name-morph: `name-morph(I;J)` extend-name-morph: `f[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)` and: `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]` cand: `A c∧ 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 extend-name-morph_wf name-comp_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 not-assert-isname nsub2_subtype_extd-nameset
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation_alt cut introduction extract_by_obid sqequalHypSubstitution isectElimination thin hypothesis hypothesisEquality independent_isectElimination 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 because_Cache voidElimination intEquality natural_numberEquality functionIsType universeIsType independent_pairFormation dependent_set_memberEquality_alt isect_memberEquality_alt applyLambdaEquality imageMemberEquality baseClosed imageElimination approximateComputation Error :memTop,  pointwiseFunctionality baseApply closedConclusion int_eqEquality productIsType sqequalBase

Latex:
\mforall{}I,J,K:Cname  List.  \mforall{}f:name-morph(I;J).  \mforall{}g:name-morph(J;K).  \mforall{}z,v,v1:Cname.
((\mneg{}(z  \mmember{}  I))  {}\mRightarrow{}  (\mneg{}(v  \mmember{}  K))  {}\mRightarrow{}  (\mneg{}(v1  \mmember{}  J))  {}\mRightarrow{}  ((f  o  g)[z:=v]  =  (f[z:=v1]  o  g[v1:=v])))

Date html generated: 2020_05_21-AM-10_49_56
Last ObjectModification: 2019_12_08-PM-07_06_12

Theory : cubical!sets

Home Index