Nuprl Lemma : not-assert-isname

`∀[L:Cname List]. ∀[z:extd-nameset(L)].  uiff(¬↑isname(z);z ∈ ℕ2)`

Proof

Definitions occuring in Statement :  isname: `isname(z)` extd-nameset: `extd-nameset(L)` coordinate_name: `Cname` list: `T List` int_seg: `{i..j-}` assert: `↑b` uiff: `uiff(P;Q)` uall: `∀[x:A]. B[x]` not: `¬A` member: `t ∈ T` natural_number: `\$n`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` uiff: `uiff(P;Q)` and: `P ∧ Q` uimplies: `b supposing a` member: `t ∈ T` subtype_rel: `A ⊆r B` not: `¬A` implies: `P `` Q` false: `False` extd-nameset: `extd-nameset(L)` b-union: `A ⋃ B` tunion: `⋃x:A.B[x]` bool: `𝔹` unit: `Unit` ifthenelse: `if b then t else f fi ` pi2: `snd(t)` nameset: `nameset(L)` coordinate_name: `Cname` int_upper: `{i...}` isname: `isname(z)` rev_uimplies: `rev_uimplies(P;Q)` all: `∀x:A. B[x]` int_seg: `{i..j-}` decidable: `Dec(P)` or: `P ∨ Q` sq_type: `SQType(T)` guard: `{T}` le_int: `i ≤z j` lt_int: `i <z j` bnot: `¬bb` btrue: `tt` assert: `↑b` bfalse: `ff` lelt: `i ≤ j < k` satisfiable_int_formula: `satisfiable_int_formula(fmla)` exists: `∃x:A. B[x]` top: `Top` prop: `ℙ`
Lemmas referenced :  extd-nameset_subtype_base istype-assert isname_wf istype-void int_seg_wf extd-nameset_wf list_wf coordinate_name_wf assert_of_le_int decidable__equal_int subtype_base_sq int_subtype_base int_seg_properties int_seg_subtype_special int_seg_cases full-omega-unsat intformand_wf intformless_wf itermVar_wf itermConstant_wf intformle_wf istype-int int_formula_prop_and_lemma int_formula_prop_less_lemma int_term_value_var_lemma int_term_value_constant_lemma int_formula_prop_le_lemma int_formula_prop_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation_alt independent_pairFormation introduction cut sqequalRule sqequalHypSubstitution axiomEquality equalityTransitivity hypothesis equalitySymmetry hypothesisEquality applyEquality extract_by_obid isectElimination thin functionIsType lambdaEquality_alt dependent_functionElimination voidElimination functionIsTypeImplies inhabitedIsType because_Cache equalityIsType4 universeIsType natural_numberEquality imageElimination productElimination unionElimination equalityElimination independent_functionElimination setElimination rename independent_isectElimination lambdaFormation_alt equalityIsType1 instantiate cumulativity intEquality hypothesis_subsumption approximateComputation dependent_pairFormation_alt int_eqEquality isect_memberEquality_alt

Latex:
\mforall{}[L:Cname  List].  \mforall{}[z:extd-nameset(L)].    uiff(\mneg{}\muparrow{}isname(z);z  \mmember{}  \mBbbN{}2)

Date html generated: 2019_11_05-PM-00_24_08
Last ObjectModification: 2018_11_08-AM-11_41_06

Theory : cubical!sets

Home Index