Nuprl Lemma : assert-dlo

Nuprl Lemma : assert-dlo_eq

∀a,b:dl-Obj(). (↑dlo_eq(a;b) ⇐⇒ a = b ∈ dl-Obj())

Proof

Definitions occuring in Statement : dlo_eq: dlo_eq(a;b), dl-Obj: dl-Obj(), assert: ↑b, all: ∀x:A. B[x], iff: P ⇐⇒ Q, equal: s = t ∈ T
Definitions unfolded in proof : uall: ∀[x:A]. B[x], so_lambda: λ₂x.t[x], member: t ∈ T, so_apply: x[s], subtype_rel: A ⊆r B, prop: ℙ, implies: P ⇒ Q, all: ∀x:A. B[x], iff: P ⇐⇒ Q, and: P ∧ Q, rev_implies: P ⇐ Q, nat: ℕ, uimplies: b supposing a, dlo_eq: dlo_eq(a;b), dlo-eq: dlo-eq(), top: Top, so_lambda: so_lambda(x,y,z,w.t[x; y; z; w]), so_apply: x[s1;s2;s3;s4], so_lambda: λ₂x y.t[x; y], so_apply: x[s1;s2], dl-kind: dl-kind(d), mobj-kind: mobj-kind(x), pi1: fst(t), dl-prog-obj: prog(x), eq_atom: x =a y, dl-obj-prog: dl-obj-prog(x), pi2: snd(t), dl-aprog?: dl-aprog?(x), dl-label: dl-label(d), mobj-label: mobj-label(x), prec-label: prec-label(x), mobj-data: mobj-data(x), dl-aprog: atm(x), mk-prec: mk-prec(lbl;x), btrue: tt, dl-aprog-1: dl-aprog-1(x), select-tuple: x.n, ifthenelse: if b then t else f fi , eq_int: (i =_z j), band: p ∧_b q, uiff: uiff(P;Q), ge: i ≥ j , decidable: Dec(P), or: P ∨ Q, not: ¬A, satisfiable_int_formula: satisfiable_int_formula(fmla), exists: ∃x:A. B[x], false: False, rev_uimplies: rev_uimplies(P;Q), squash: ↓T, assert: ↑b, true: True, dl-comp: (x1;x), bfalse: ff, dl-comp?: dl-comp?(x), dl-choose: x1 ⋃ x, dl-choose?: dl-choose?(x), dl-iterate: (x)*, dl-iterate?: dl-iterate?(x), dl-test: (x)?, dl-test?: dl-test?(x), dl-prop-obj: prop(x), dl-aprop: atm(x), l_member: (x ∈ l), select: L[n], cons: [a / b], cand: A c∧ B, less_than: a < b, less_than': less_than'(a;b), subtract: n - m, dl-false: 0, dl-implies: x1 ⇒ x, dl-and: x1 ∧ x, dl-or: x1 ∨ x, dl-box: [x1] x, dl-diamond: <x1> x, dl-comp-1: dl-comp-1(x), dl-comp-2: dl-comp-2(x), sq_type: SQType(T), guard: {T}, dl-choose-1: dl-choose-1(x), dl-choose-2: dl-choose-2(x), dl-iterate-1: dl-iterate-1(x), dl-test-1: dl-test-1(x), dl-obj-prop: dl-obj-prop(x), dl-aprop?: dl-aprop?(x), dl-aprop-1: dl-aprop-1(x), dl-false?: dl-false?(x), dl-implies?: dl-implies?(x), dl-and?: dl-and?(x), dl-or?: dl-or?(x), dl-box?: dl-box?(x), dl-diamond?: dl-diamond?(x), dl-implies-1: dl-implies-1(x), dl-implies-2: dl-implies-2(x), dl-and-1: dl-and-1(x), dl-and-2: dl-and-2(x), dl-or-1: dl-or-1(x), dl-or-2: dl-or-2(x), dl-box-1: dl-box-1(x), dl-box-2: dl-box-2(x), dl-diamond-1: dl-diamond-1(x), dl-diamond-2: dl-diamond-2(x)
Lemmas referenced : dl-induction, all_wf, dl-Obj_wf, iff_wf, assert_wf, dlo_eq_wf, equal_wf, subtype-TYPE, istype-nat, istype-assert, dl-prog-obj_wf, dl-prog_wf, dl-prop-obj_wf, dl-prop_wf, dl-aprog_wf, equal-wf-base-T, set_subtype_base, le_wf, istype-int, int_subtype_base, dl-ind-dl-aprog, istype-void, assert_of_eq_int, nat_properties, decidable__equal_int, full-omega-unsat, intformand_wf, intformnot_wf, intformeq_wf, itermVar_wf, int_formula_prop_and_lemma, int_formula_prop_not_lemma, int_formula_prop_eq_lemma, int_term_value_var_lemma, int_formula_prop_wf, decidable__le, intformle_wf, itermConstant_wf, int_formula_prop_le_lemma, int_term_value_constant_lemma, istype-le, eq_int_wf, dl-obj-prog_wf, squash_wf, equal-wf-base, dl-kind_wf, l_member_wf, cons_wf, nil_wf, istype-atom, atom_subtype_base, dl-aprog-1_wf, dl-aprog?_wf, btrue_wf, dl-comp_wf, dl-comp?_wf, bfalse_wf, btrue_neq_bfalse, dl-choose_wf, dl-choose?_wf, dl-iterate_wf, dl-iterate?_wf, dl-test_wf, dl-test?_wf, length_of_cons_lemma, length_of_nil_lemma, istype-less_than, length_wf, list_subtype_base, assert_of_eq_atom, dl-implies_wf, dl-and_wf, dl-or_wf, dl-box_wf, dl-diamond_wf, dl-ind-dl-comp, bool_cases, subtype_base_sq, bool_wf, bool_subtype_base, eqtt_to_assert, band_wf, assert_of_band, dl-aprop_wf, dl-false_wf, dl-comp-1_wf, dl-comp-2_wf, true_wf, dl-ind-dl-choose, dl-choose-1_wf, dl-choose-2_wf, dl-ind-dl-iterate, dl-iterate-1_wf, dl-ind-dl-test, dl-test-1_wf, dl-obj-prop_wf, dl-ind-dl-aprop, dl-aprop-1_wf, dl-aprop?_wf, dl-false?_wf, dl-implies?_wf, dl-and?_wf, dl-or?_wf, dl-box?_wf, dl-diamond?_wf, dl-ind-dl-false, istype-true, dl-ind-dl-implies, dl-implies-1_wf, dl-implies-2_wf, dl-ind-dl-and, dl-and-1_wf, dl-and-2_wf, dl-ind-dl-or, dl-or-1_wf, dl-or-2_wf, dl-ind-dl-box, dl-box-1_wf, dl-box-2_wf, dl-ind-dl-diamond, dl-diamond-1_wf, dl-diamond-2_wf
Rules used in proof : cut, introduction, extract_by_obid, sqequalHypSubstitution, sqequalSubstitution, sqequalTransitivity, computationStep, sqequalReflexivity, isectElimination, thin, sqequalRule, lambdaEquality_alt, hypothesis, hypothesisEquality, inhabitedIsType, applyEquality, universeIsType, independent_functionElimination, lambdaFormation_alt, dependent_functionElimination, because_Cache, functionIsType, productIsType, equalityIstype, baseApply, closedConclusion, baseClosed, intEquality, natural_numberEquality, independent_isectElimination, isect_memberEquality_alt, voidElimination, independent_pairFormation, setElimination, rename, productElimination, unionElimination, approximateComputation, dependent_pairFormation_alt, int_eqEquality, dependent_set_memberEquality_alt, equalityTransitivity, equalitySymmetry, applyLambdaEquality, imageElimination, atomEquality, tokenEquality, imageMemberEquality, promote_hyp, hyp_replacement, sqequalBase, instantiate, cumulativity

Latex:
\mforall{}a,b:dl-Obj(). (\muparrow{}dlo\_eq(a;b) \mLeftarrow{}{}\mRightarrow{} a = b) Date html generated: 2019_10_15-AM-11_43_02 Last ObjectModification: 2019_04_05-AM-11_35_36 Theory : dynamic!logic Home Index