Nuprl Lemma : unsquashed-weak-continuity-base-false

Nuprl Lemma : unsquashed-weak-continuity-base-false

¬base-CP()

Proof

Definitions occuring in Statement : base-CP: base-CP(), not: ¬A
Definitions unfolded in proof : not: ¬A, implies: P ⇒ Q, base-CP: base-CP(), exists: ∃x:A. B[x], member: t ∈ T, prop: ℙ, uall: ∀[x:A]. B[x], all: ∀x:A. B[x], subtype_rel: A ⊆r B, nat: ℕ, int_seg: {i..j^-}, so_lambda: λ₂x.t[x], so_apply: x[s], uimplies: b supposing a, pi1: fst(t), false: False, less_than': less_than'(a;b), le: A ≤ B, bfalse: ff, ifthenelse: if b then t else f fi , btrue: tt, it: ⋅, unit: Unit, bool: 𝔹, isect2: T1 ⋂ T2, cand: A c∧ B, and: P ∧ Q, top: Top, satisfiable_int_formula: satisfiable_int_formula(fmla), ge: i ≥ j , guard: {T}, sq_type: SQType(T), or: P ∨ Q, decidable: Dec(P), lelt: i ≤ j < k, true: True, assert: ↑b, bnot: ¬_bb, uiff: uiff(P;Q), iff: P ⇐⇒ Q, rev_implies: P ⇐ Q
Lemmas referenced : base-CP_wf, isect2_wf, nat_wf, base_wf, int_seg_wf, istype-nat, set_subtype_base, lelt_wf, istype-int, int_subtype_base, isect2_subtype_rel2, false_wf, bool_wf, equal-wf-base, int_seg_subtype_nat, isect2_decomp, equal_wf, all_wf, le_wf, isect2_subtype_rel, istype-false, istype-le, int_formula_prop_wf, int_formula_prop_le_lemma, int_formula_prop_eq_lemma, int_term_value_var_lemma, int_term_value_constant_lemma, int_formula_prop_less_lemma, int_formula_prop_not_lemma, int_formula_prop_and_lemma, intformle_wf, intformeq_wf, itermVar_wf, itermConstant_wf, intformless_wf, intformnot_wf, intformand_wf, satisfiable-full-omega-tt, decidable__lt, nat_properties, subtype_base_sq, decidable__equal_int, int_seg_properties, less_than_wf, assert-bnot, bool_subtype_base, bool_cases_sqequal, eqff_to_assert, assert_of_lt_int, eqtt_to_assert, lt_int_wf, not_wf, bnot_wf, assert_wf, bool_cases, iff_transitivity, iff_weakening_uiff, assert_of_bnot, ifthenelse_wf
Rules used in proof : sqequalSubstitution, sqequalTransitivity, computationStep, sqequalReflexivity, Error :lambdaFormation_alt, sqequalHypSubstitution, cut, hypothesis, promote_hyp, thin, productElimination, Error :universeIsType, introduction, extract_by_obid, isectElimination, functionEquality, because_Cache, sqequalRule, Error :functionIsType, natural_numberEquality, applyEquality, hypothesisEquality, Error :lambdaEquality_alt, setElimination, rename, Error :equalityIsType4, baseApply, closedConclusion, baseClosed, intEquality, independent_isectElimination, Error :dependent_pairFormation_alt, functionExtensionality, Error :inhabitedIsType, Error :equalityIsType1, equalityTransitivity, equalitySymmetry, dependent_functionElimination, independent_functionElimination, pointwiseFunctionality, productEquality, lambdaFormation, independent_pairFormation, dependent_set_memberEquality, equalityElimination, unionElimination, isect_memberEquality, lambdaEquality, dependent_pairFormation, Error :dependent_set_memberEquality_alt, Error :productIsType, computeAll, voidEquality, voidElimination, int_eqEquality, cumulativity, instantiate, applyLambdaEquality, impliesFunctionality

Latex:
\mneg{}base-CP() Date html generated: 2019_06_20-PM-02_49_30 Last ObjectModification: 2018_10_29-PM-00_52_31 Theory : fan-theorem Home Index