Nuprl Lemma : rename-one-comp

I:Cname List. ∀z,z1,z2:Cname.
  (rename-one-name(z;z1) rename-one-name(z1;z2)) rename-one-name(z;z2) ∈ name-morph([z I];[z2 I]) 
  supposing (z2 ∈ I)) ∧ (z1 ∈ I)) ∧ (z ∈ I))


Proof




Definitions occuring in Statement :  rename-one-name: rename-one-name(z1;z2) name-comp: (f g) name-morph: name-morph(I;J) coordinate_name: Cname l_member: (x ∈ l) cons: [a b] list: List uimplies: supposing a all: x:A. B[x] not: ¬A and: P ∧ Q equal: t ∈ T
Definitions unfolded in proof :  all: x:A. B[x] uimplies: supposing a and: P ∧ Q uall: [x:A]. B[x] member: t ∈ T cand: c∧ B not: ¬A implies:  Q prop: false: False subtype_rel: A ⊆B name-morph: name-morph(I;J) rename-one-name: rename-one-name(z1;z2) name-comp: (f g) compose: g uext: uext(g) nameset: nameset(L) bool: 𝔹 unit: Unit it: btrue: tt uiff: uiff(P;Q) ifthenelse: if then else fi  bfalse: ff exists: x:A. B[x] or: P ∨ Q sq_type: SQType(T) guard: {T} bnot: ¬bb assert: b rev_implies:  Q coordinate_name: Cname int_upper: {i...} so_lambda: λ2x.t[x] so_apply: x[s] iff: ⇐⇒ Q 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 ≥ 
Lemmas referenced :  name-morphs-equal cons_wf coordinate_name_wf rename-one-name_wf l_member_wf istype-void list_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 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 isname-nameset cons_member nameset_subtype l_subset_right_cons_trivial
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation_alt isect_memberFormation_alt cut sqequalHypSubstitution productElimination thin equalitySymmetry introduction extract_by_obid isectElimination hypothesis hypothesisEquality independent_isectElimination independent_pairFormation sqequalRule productIsType functionIsType universeIsType inhabitedIsType applyEquality because_Cache lambdaEquality_alt setElimination rename equalityTransitivity functionExtensionality unionElimination equalityElimination dependent_pairFormation_alt equalityIstype promote_hyp dependent_functionElimination instantiate cumulativity independent_functionElimination voidElimination intEquality natural_numberEquality dependent_set_memberEquality_alt isect_memberEquality_alt applyLambdaEquality imageMemberEquality baseClosed imageElimination approximateComputation Error :memTop,  pointwiseFunctionality baseApply closedConclusion int_eqEquality sqequalBase

Latex:
\mforall{}I:Cname  List.  \mforall{}z,z1,z2:Cname.
    (rename-one-name(z;z1)  o  rename-one-name(z1;z2))  =  rename-one-name(z;z2) 
    supposing  (\mneg{}(z2  \mmember{}  I))  \mwedge{}  (\mneg{}(z1  \mmember{}  I))  \mwedge{}  (\mneg{}(z  \mmember{}  I))



Date html generated: 2020_05_21-AM-10_49_18
Last ObjectModification: 2019_12_08-PM-07_06_26

Theory : cubical!sets


Home Index