Nuprl Lemma : int_add_grp_wf2

<ℤ+> ∈ OGrp


Proof




Definitions occuring in Statement :  int_add_grp: <ℤ+> ocgrp: OGrp member: t ∈ T
Definitions unfolded in proof :  member: t ∈ T ocgrp: OGrp uall: [x:A]. B[x] ocmon: OCMon abmonoid: AbMon mon: Mon prop: and: P ∧ Q so_lambda: λ2y.t[x; y] so_apply: x[s1;s2] infix_ap: y all: x:A. B[x] implies:  Q bool: 𝔹 unit: Unit it: btrue: tt band: p ∧b q ifthenelse: if then else fi  uiff: uiff(P;Q) uimplies: supposing a bfalse: ff so_lambda: λ2x.t[x] so_apply: x[s] subtype_rel: A ⊆B abgrp: AbGrp grp: Group{i} int_add_grp: <ℤ+> grp_car: |g| pi1: fst(t) grp_le: b pi2: snd(t) grp_eq: =b grp_op: * le: A ≤ B not: ¬A false: False iff: ⇐⇒ Q rev_implies:  Q monot: monot(T;x,y.R[x; y];f) ulinorder: UniformLinorder(T;x,y.R[x; y]) uorder: UniformOrder(T;x,y.R[x; y]) urefl: UniformlyRefl(T;x,y.E[x; y]) decidable: Dec(P) or: P ∨ Q satisfiable_int_formula: satisfiable_int_formula(fmla) exists: x:A. B[x] top: Top utrans: UniformlyTrans(T;x,y.E[x; y]) uanti_sym: UniformlyAntiSym(T;x,y.R[x; y]) connex: Connex(T;x,y.R[x; y]) cancel: Cancel(T;S;op) inverse: Inverse(T;op;id;inv) grp_inv: ~ grp_id: e cand: c∧ B
Lemmas referenced :  inverse_wf grp_car_wf grp_op_wf grp_id_wf grp_inv_wf ulinorder_wf assert_wf infix_ap_wf bool_wf grp_le_wf equal_wf grp_eq_wf eqtt_to_assert cancel_wf uall_wf monot_wf int_add_grp_wf subtype_rel_sets mon_wf comm_wf set_wf ulinorder_functionality_wrt_iff le_int_wf le_wf assert_of_le_int less_than'_wf assert_witness monot_functionality iff_weakening_uiff decidable__le satisfiable-full-omega-tt intformnot_wf intformle_wf itermVar_wf int_formula_prop_not_lemma int_formula_prop_le_lemma int_term_value_var_lemma int_formula_prop_wf intformand_wf int_formula_prop_and_lemma decidable__equal_int intformeq_wf int_formula_prop_eq_lemma decidable__or intformor_wf int_formula_prop_or_lemma iff_imp_equal_bool eq_int_wf band_wf equal-wf-base int_subtype_base assert_of_eq_int iff_transitivity assert_of_band iff_wf itermAdd_wf int_term_value_add_lemma itermMinus_wf itermConstant_wf int_term_value_minus_lemma int_term_value_constant_lemma
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity dependent_set_memberEquality cut introduction extract_by_obid sqequalHypSubstitution isectElimination thin setElimination rename hypothesisEquality hypothesis because_Cache productEquality sqequalRule lambdaEquality functionEquality lambdaFormation unionElimination equalityElimination productElimination independent_isectElimination equalityTransitivity equalitySymmetry dependent_functionElimination independent_functionElimination applyEquality instantiate setEquality cumulativity independent_pairFormation intEquality isect_memberFormation independent_pairEquality isect_memberEquality axiomEquality voidElimination addEquality natural_numberEquality dependent_pairFormation int_eqEquality voidEquality computeAll functionExtensionality addLevel impliesFunctionality baseApply closedConclusion baseClosed

Latex:
<\mBbbZ{}+>  \mmember{}  OGrp



Date html generated: 2017_10_01-AM-08_16_56
Last ObjectModification: 2017_02_28-PM-02_02_34

Theory : groups_1


Home Index