Nuprl Lemma : C_TYPE_subtype

Nuprl Lemma : C_TYPE_subtype_base

C_TYPE() ⊆r Base

Proof

Definitions occuring in Statement : C_TYPE: C_TYPE(), subtype_rel: A ⊆r B, base: Base
Definitions unfolded in proof : subtype_rel: A ⊆r B, member: t ∈ T, uall: ∀[x:A]. B[x], all: ∀x:A. B[x], nat: ℕ, implies: P ⇒ Q, false: False, ge: i ≥ j , uimplies: b supposing a, satisfiable_int_formula: satisfiable_int_formula(fmla), exists: ∃x:A. B[x], not: ¬A, top: Top, and: P ∧ Q, prop: ℙ, guard: {T}, int_seg: {i..j^-}, lelt: i ≤ j < k, decidable: Dec(P), or: P ∨ Q, le: A ≤ B, less_than': less_than'(a;b), ext-eq: A ≡ B, bool: 𝔹, unit: Unit, it: ⋅, btrue: tt, uiff: uiff(P;Q), sq_type: SQType(T), eq_atom: x =a y, ifthenelse: if b then t else f fi , C_Void: C_Void(), C_TYPE_size: C_TYPE_size(p), select: L[n], so_lambda: λ₂x y.t[x; y], so_apply: x[s1;s2], cand: A c∧ B, bfalse: ff, bnot: ¬_bb, assert: ↑b, C_Int: C_Int(), C_Struct: C_Struct(fields), so_lambda: λ₂x.t[x], less_than: a < b, squash: ↓T, so_apply: x[s], C_Array: C_Array(length;elems), pi2: snd(t), C_Pointer: C_Pointer(to), true: True, b-union: A ⋃ B, cons: [a / b], colength: colength(L), nil: [], subtract: n - m, iff: P ⇐⇒ Q, rev_implies: P ⇐ Q
Lemmas referenced : iff_weakening_equal, pair-eta, subtype_rel_product, pi1_wf_top, equal_functionality_wrt_subtype_rel2, subtype_rel_list, add-subtract-cancel, assert_of_bnot, iff_weakening_uiff, iff_transitivity, assert_of_le_int, bool_cases, select-cons, not_wf, bnot_wf, assert_wf, le_int_wf, add-member-int_seg2, add-is-int-iff, tl_wf, subtype_rel_self, product_subtype_base, reduce_tl_cons_lemma, reduce_tl_nil_lemma, non_neg_length, length_of_cons_lemma, spread_cons_lemma, product_subtype_list, length_of_nil_lemma, list-cases, colength_wf_list, top_wf, equal-wf-base, less_than_irreflexivity, less_than_transitivity1, equal-wf-T-base, subtype_rel_wf, and_wf, ext-eq_weakening, subtype_rel_weakening, subtype_rel-equal, ifthenelse_wf, tunion_subtype_base, list_wf, true_wf, squash_wf, all_wf, nat_wf, int_subtype_base, set_subtype_base, sum-nat-less, int_term_value_add_lemma, itermAdd_wf, pi2_wf, decidable__lt, length_wf, select_wf, length_wf_nat, sum-nat, neg_assert_of_eq_atom, assert-bnot, bool_subtype_base, bool_cases_sqequal, equal_wf, eqff_to_assert, member_wf, base_wf, stuck-spread, it_wf, unit_subtype_base, atom_subtype_base, subtype_base_sq, assert_of_eq_atom, eqtt_to_assert, bool_wf, eq_atom_wf, C_TYPE-ext, int_formula_prop_eq_lemma, intformeq_wf, lelt_wf, false_wf, int_seg_subtype, decidable__equal_int, int_term_value_subtract_lemma, int_formula_prop_not_lemma, itermSubtract_wf, intformnot_wf, subtract_wf, decidable__le, int_seg_properties, int_seg_wf, C_TYPE_wf, C_TYPE_size_wf, le_wf, less_than_wf, ge_wf, int_formula_prop_wf, int_formula_prop_less_lemma, int_term_value_var_lemma, int_term_value_constant_lemma, int_formula_prop_le_lemma, int_formula_prop_and_lemma, intformless_wf, itermVar_wf, itermConstant_wf, intformle_wf, intformand_wf, satisfiable-full-omega-tt, nat_properties
Rules used in proof : sqequalSubstitution, sqequalTransitivity, computationStep, sqequalReflexivity, lambdaEquality, cut, thin, isect_memberFormation, introduction, lambdaFormation, lemma_by_obid, sqequalHypSubstitution, isectElimination, hypothesisEquality, hypothesis, setElimination, rename, sqequalRule, intWeakElimination, natural_numberEquality, independent_isectElimination, dependent_pairFormation, int_eqEquality, intEquality, dependent_functionElimination, isect_memberEquality, voidElimination, voidEquality, independent_pairFormation, computeAll, independent_functionElimination, productElimination, independent_pairEquality, axiomEquality, equalityTransitivity, equalitySymmetry, applyEquality, because_Cache, unionElimination, setEquality, hypothesis_subsumption, dependent_set_memberEquality, promote_hyp, tokenEquality, equalityElimination, instantiate, cumulativity, atomEquality, baseClosed, productEquality, imageElimination, equalityEquality, baseApply, closedConclusion, addEquality, addLevel, pointwiseFunctionality wrename, functionUniverseElim, universeEquality, imageMemberEquality, equalityUniverseElim, substitution, sqequalAxiom, levelHypothesis, pointwiseFunctionality, impliesFunctionality

Latex:
C\_TYPE() \msubseteq{}r Base Date html generated: 2016_05_16-AM-08_45_41 Last ObjectModification: 2016_01_17-AM-09_44_57 Theory : C-semantics Home Index