Nuprl Lemma : cu-filler-cases

I:Cname List. ∀J:nameset(I) List. ∀K:Cname List. ∀x:nameset(I). ∀f:name-morph(I-[x];K). ∀i:ℕ2.
box:open_box(c𝕌;I;J;x;i).
  ((J ∈ nameset(J) List)
  ∧ (nameset(J) ⊆nameset(I-[x]))
  ∧ ((∃y:nameset(J) [((y ∈ J) ∧ (↑¬bisname(f y)) ∧ (l-first(y.¬bisname(f y);J) inl y))])
    ∨ (((∀y∈J.¬↑¬bisname(f y)) ∧ (↑isr(l-first(y.¬bisname(f y);J))))
      ∧ (f[x:=fresh-cname(K)] ∈ name-morph(I;[fresh-cname(K) K]))
      ∧ (nameset([x J]) ⊆nameset(I))
      ∧ (∀z:nameset([x J]). (↑isname(f[x:=fresh-cname(K)] z)))
      ∧ (f[x:=fresh-cname(K)] ∈ nameset([x J]) ⟶ nameset([fresh-cname(K) K]))
      ∧ (x ∈ nameset([x J]))
      ∧ (nameset([x J]) ⊆name-morph-domain(f[x:=fresh-cname(K)];I)))))


Proof




Definitions occuring in Statement :  cubical-universe: c𝕌 open_box: open_box(X;I;J;x;i) name-morph-domain: name-morph-domain(f;I) extend-name-morph: f[z1:=z2] name-morph: name-morph(I;J) isname: isname(z) fresh-cname: fresh-cname(I) nameset: nameset(L) cname_deq: CnameDeq coordinate_name: Cname list-diff: as-bs l-first: l-first(x.f[x];L) l_all: (∀x∈L.P[x]) l_member: (x ∈ l) cons: [a b] nil: [] list: List int_seg: {i..j-} bnot: ¬bb assert: b isr: isr(x) subtype_rel: A ⊆B all: x:A. B[x] sq_exists: x:A [B[x]] not: ¬A or: P ∨ Q and: P ∧ Q member: t ∈ T apply: a function: x:A ⟶ B[x] inl: inl x natural_number: $n sqequal: t
Definitions unfolded in proof :  all: x:A. B[x] and: P ∧ Q cand: c∧ B member: t ∈ T uall: [x:A]. B[x] subtype_rel: A ⊆B uimplies: supposing a nameset: nameset(L) guard: {T} prop: so_apply: x[s] so_lambda: λ2x.t[x] int_upper: {i...} coordinate_name: Cname not: ¬A implies:  Q rev_implies:  Q iff: ⇐⇒ Q open_box: open_box(X;I;J;x;i) l_subset: l_subset(T;as;bs) false: False name-morph: name-morph(I;J) or: P ∨ Q sq_exists: x:A [B[x]] istype: istype(T) respects-equality: respects-equality(S;T) uiff: uiff(P;Q) true: True btrue: tt ifthenelse: if then else fi  assert: b isr: isr(x) sq_type: SQType(T) bnot: ¬bb exists: x:A. B[x] bfalse: ff it: unit: Unit bool: 𝔹 extend-name-morph: f[z1:=z2] l_member: (x ∈ l) top: Top satisfiable_int_formula: satisfiable_int_formula(fmla) decidable: Dec(P) ge: i ≥  lelt: i ≤ j < k int_seg: {i..j-} sq_stable: SqStable(P) squash: T nat: l_all: (∀x∈L.P[x]) rev_uimplies: rev_uimplies(P;Q) ext-eq: A ≡ B
Lemmas referenced :  open_box_wf cubical-universe_wf subtype_rel_list nameset_wf coordinate_name_wf int_seg_wf name-morph_wf list-diff_wf cname_deq_wf cons_wf nil_wf list_wf list-subtype l_member_wf member_singleton int_subtype_base istype-int le_wf set_subtype_base member-list-diff l-first_wf bnot_wf isname_wf nameset_subtype_base istype-sqequal istype-assert l_all_wf2 not_wf assert_wf isr_wf sq_exists_wf and_wf istype-void fresh-cname_wf extend-name-morph_wf fresh-cname-not-member2 respects-equality-set extd-nameset_wf all_wf equal_wf subtype-respects-equality subtype_rel_set subtype_rel_dep_function nameset_subtype_cons_diff subtype_rel_wf respects-equality-set-trivial2 assert-isname name-morph-domain_wf cons_member subtype_base_sq list-diff-subset nameset_subtype iff_weakening_uiff assert-bnot bool_wf bool_cases_sqequal bool_subtype_base eqff_to_assert assert-eq-cname eqtt_to_assert eq-cname_wf isname-name 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 itermVar_wf itermConstant_wf intformle_wf intformnot_wf intformand_wf full-omega-unsat decidable__le decidable__equal-coordinate_name sq_stable__l_member int_seg_properties nat_properties sq_stable__le select_wf istype-le int_formula_prop_eq_lemma intformeq_wf decidable__assert length_wf istype-less_than assert_of_bnot name-morph-domain_subtype istype-inr-sqeq-inl
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation_alt cut independent_pairFormation hypothesis universeIsType thin instantiate introduction extract_by_obid sqequalHypSubstitution isectElimination hypothesisEquality applyEquality independent_isectElimination lambdaEquality_alt setElimination rename inhabitedIsType sqequalRule natural_numberEquality equalitySymmetry equalityTransitivity closedConclusion intEquality equalityIsType2 independent_functionElimination productElimination because_Cache dependent_functionElimination dependent_set_memberEquality_alt hyp_replacement productIsType equalityIsType4 baseApply baseClosed applyLambdaEquality voidElimination equalityIstype unionElimination inlFormation_alt dependent_set_memberFormation_alt setIsType voidEquality inlEquality_alt functionEquality functionIsType functionExtensionality inrFormation_alt cumulativity equalityIsType1 promote_hyp equalityIsType3 dependent_pairFormation_alt equalityElimination isect_memberEquality_alt int_eqEquality approximateComputation imageElimination imageMemberEquality

Latex:
\mforall{}I:Cname  List.  \mforall{}J:nameset(I)  List.  \mforall{}K:Cname  List.  \mforall{}x:nameset(I).  \mforall{}f:name-morph(I-[x];K).  \mforall{}i:\mBbbN{}2.
\mforall{}box:open\_box(c\mBbbU{};I;J;x;i).
    ((J  \mmember{}  nameset(J)  List)
    \mwedge{}  (nameset(J)  \msubseteq{}r  nameset(I-[x]))
    \mwedge{}  ((\mexists{}y:nameset(J)  [((y  \mmember{}  J)  \mwedge{}  (\muparrow{}\mneg{}\msubb{}isname(f  y))  \mwedge{}  (l-first(y.\mneg{}\msubb{}isname(f  y);J)  \msim{}  inl  y))])
        \mvee{}  (((\mforall{}y\mmember{}J.\mneg{}\muparrow{}\mneg{}\msubb{}isname(f  y))  \mwedge{}  (\muparrow{}isr(l-first(y.\mneg{}\msubb{}isname(f  y);J))))
            \mwedge{}  (f[x:=fresh-cname(K)]  \mmember{}  name-morph(I;[fresh-cname(K)  /  K]))
            \mwedge{}  (nameset([x  /  J])  \msubseteq{}r  nameset(I))
            \mwedge{}  (\mforall{}z:nameset([x  /  J]).  (\muparrow{}isname(f[x:=fresh-cname(K)]  z)))
            \mwedge{}  (f[x:=fresh-cname(K)]  \mmember{}  nameset([x  /  J])  {}\mrightarrow{}  nameset([fresh-cname(K)  /  K]))
            \mwedge{}  (x  \mmember{}  nameset([x  /  J]))
            \mwedge{}  (nameset([x  /  J])  \msubseteq{}r  name-morph-domain(f[x:=fresh-cname(K)];I)))))



Date html generated: 2019_11_06-PM-00_54_27
Last ObjectModification: 2018_12_10-PM-03_15_12

Theory : cubical!sets


Home Index