Nuprl Lemma : dl-program-eq-equiv

∀a,b:Prog. equiv-props([(a ⇐⇒ b); (a ⇐⇒a b); (a ⇐⇒w b); a ≡ b])

Proof

Definitions occuring in Statement : dl-logical-eq: (a ⇐⇒ b), dl-logical-eq-atomic: (a ⇐⇒a b), dl-logical-eq-weak: (a ⇐⇒w b), dl-sem-eq: a ≡ b, dl-prog: Prog, equiv-props: equiv-props(L), cons: [a / b], nil: [], all: ∀x:A. B[x]
Definitions unfolded in proof : all: ∀x:A. B[x], member: t ∈ T, uall: ∀[x:A]. B[x], prop: ℙ, implies: P ⇒ Q, top: Top, subtract: n - m, int_seg: {i..j^-}, lelt: i ≤ j < k, and: P ∧ Q, le: A ≤ B, decidable: Dec(P), or: P ∨ Q, uimplies: b supposing a, sq_type: SQType(T), guard: {T}, select: L[n], cons: [a / b], dl-logical-eq: (a ⇐⇒ b), dl-logical-eq-atomic: (a ⇐⇒a b), dl-logical-eq-weak: (a ⇐⇒w b), dl-sem-eq: a ≡ b, not: ¬A, satisfiable_int_formula: satisfiable_int_formula(fmla), exists: ∃x:A. B[x], false: False, last: last(L), cand: A c∧ B, iff: P ⇐⇒ Q, rev_implies: P ⇐ Q, so_lambda: λ₂x.t[x], nat: ℕ, dl-valid: |= phi, so_apply: x[s], subtype_rel: A ⊆r B, dl-prop-sem: [|phi|], dl-sem: dl-sem(K;n.R[n];m.P[m]), 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-prog-sem: [|alpha|], bool: 𝔹, unit: Unit, it: ⋅, btrue: tt, uiff: uiff(P;Q), ifthenelse: if b then t else f fi , bfalse: ff, bnot: ¬_bb, assert: ↑b, nequal: a ≠ b ∈ T , ge: i ≥ j , squash: ↓T, true: True
Lemmas referenced : implies-equiv-props, cons-listp, cons_wf, dl-logical-eq-atomic_wf, dl-logical-eq-weak_wf, dl-sem-eq_wf, nil_wf, dl-logical-eq_wf, length_of_cons_lemma, istype-void, length_of_nil_lemma, 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, int_seg_wf, reduce_hd_cons_lemma, dl-prog_wf, dl-aprop_wf, istype-nat, fresh-nat-exists2, append_wf, nat_wf, dl-prop-atoms_wf, dl-prog-obj_wf, l_member_wf, member_append, dl-valid_wf, dl-implies_wf, dl-diamond_wf, ifthenelse_wf, eq_int_wf, equal_wf, dl-prog-sem_wf, subtype_rel_self, istype-universe, dl-ind-dl-implies, dl-ind-dl-diamond, dl-ind-dl-aprop, eqtt_to_assert, assert_of_eq_int, eqff_to_assert, bool_cases_sqequal, bool_wf, bool_subtype_base, assert-bnot, neg_assert_of_eq_int, nat_properties, intformnot_wf, intformeq_wf, int_formula_prop_not_lemma, int_formula_prop_eq_lemma, dl-prog-sem_functionality, l_all_iff, iff_wf, decidable__le, istype-le, equal-wf-base, set_subtype_base, le_wf, assert_wf, bnot_wf, not_wf, istype-assert, uiff_transitivity, iff_transitivity, iff_weakening_uiff, assert_of_bnot, bool_cases, squash_wf, true_wf, eq_int_eq_true, btrue_wf, iff_weakening_equal, bfalse_wf, assert_elim, btrue_neq_bfalse, dl-prop-sem_wf, dl-prop_wf
Rules used in proof : sqequalSubstitution, sqequalTransitivity, computationStep, sqequalReflexivity, lambdaFormation_alt, cut, thin, instantiate, introduction, extract_by_obid, sqequalHypSubstitution, dependent_functionElimination, isectElimination, universeEquality, hypothesisEquality, hypothesis, independent_functionElimination, sqequalRule, isect_memberEquality_alt, voidElimination, setElimination, rename, productElimination, unionElimination, cumulativity, intEquality, independent_isectElimination, because_Cache, equalityTransitivity, equalitySymmetry, natural_numberEquality, universeIsType, hypothesis_subsumption, approximateComputation, dependent_pairFormation_alt, lambdaEquality_alt, int_eqEquality, independent_pairFormation, inhabitedIsType, applyEquality, productIsType, functionIsType, inlFormation_alt, inrFormation_alt, equalityElimination, equalityIstype, promote_hyp, functionEquality, dependent_set_memberEquality_alt, setIsType, baseApply, closedConclusion, baseClosed, sqequalBase, imageElimination, imageMemberEquality, applyLambdaEquality, hyp_replacement

Latex:
\mforall{}a,b:Prog. equiv-props([(a \mLeftarrow{}{}\mRightarrow{} b); (a \mLeftarrow{}{}\mRightarrow{}a b); (a \mLeftarrow{}{}\mRightarrow{}w b); a \mequiv{} b]) Date html generated: 2019_10_15-AM-11_46_30 Last ObjectModification: 2019_03_26-PM-11_42_55 Theory : dynamic!logic Home Index