### Nuprl Lemma : posint_reduc_dec

`∀a:|<ℤ+,*>|. Dec(Reducible(a))`

Proof

Definitions occuring in Statement :  posint_mul_mon: `<ℤ+,*>` mreducible: `Reducible(a)` decidable: `Dec(P)` all: `∀x:A. B[x]` grp_car: `|g|`
Definitions unfolded in proof :  all: `∀x:A. B[x]` uall: `∀[x:A]. B[x]` member: `t ∈ T` subtype_rel: `A ⊆r B` guard: `{T}` uimplies: `b supposing a` so_lambda: `λ2x.t[x]` prop: `ℙ` and: `P ∧ Q` so_apply: `x[s]` implies: `P `` Q` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` mpdivides: `a p| b` mdivides: `b | a` posint_mul_mon: `<ℤ+,*>` grp_car: `|g|` pi1: `fst(t)` grp_op: `*` pi2: `snd(t)` infix_ap: `x f y` exists: `∃x:A. B[x]` nat_plus: `ℕ+` not: `¬A` int_seg: `{i..j-}` lelt: `i ≤ j < k` decidable: `Dec(P)` or: `P ∨ Q` satisfiable_int_formula: `satisfiable_int_formula(fmla)` false: `False` top: `Top` uiff: `uiff(P;Q)` le: `A ≤ B` less_than': `less_than'(a;b)` true: `True` cand: `A c∧ B`
Lemmas referenced :  decidable_functionality mreducible_wf posint_mul_mon_wf mon_subtype_grp_sig abmonoid_subtype_mon subtype_rel_transitivity abmonoid_wf mon_wf grp_sig_wf exists_wf grp_car_wf not_wf munit_wf mpdivides_wf mreducible_elim abmonoid_subtype_iabmonoid posint_cancel nat_plus_wf equal_wf mul_nat_plus equal-wf-T-base divides_wf posint_munit_elim istype-int set_subtype_base less_than_wf int_subtype_base divides_nchar pdivisor_bound nat_plus_subtype_nat nat_plus_properties decidable__le full-omega-unsat intformand_wf intformnot_wf intformle_wf itermConstant_wf itermVar_wf intformeq_wf intformless_wf int_formula_prop_and_lemma istype-void int_formula_prop_not_lemma int_formula_prop_le_lemma int_term_value_constant_lemma int_term_value_var_lemma int_formula_prop_eq_lemma int_formula_prop_less_lemma int_formula_prop_wf le_wf equal-wf-base decidable__lt istype-false not-lt-2 add_functionality_wrt_le add-commutes zero-add le-add-cancel int_seg_properties lelt_wf int_seg_wf decidable__exists_int_seg decidable__divides_ext
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation_alt cut introduction extract_by_obid sqequalHypSubstitution isectElimination thin dependent_functionElimination hypothesis applyEquality instantiate independent_isectElimination sqequalRule hypothesisEquality because_Cache lambdaEquality_alt productEquality inhabitedIsType independent_functionElimination productElimination universeIsType setElimination rename independent_pairFormation dependent_pairFormation_alt equalityIsType4 baseApply closedConclusion baseClosed intEquality natural_numberEquality promote_hyp productIsType equalityIsType3 multiplyEquality dependent_set_memberEquality_alt unionElimination approximateComputation int_eqEquality isect_memberEquality_alt voidElimination

Latex:
\mforall{}a:|<\mBbbZ{}\msupplus{},*>|.  Dec(Reducible(a))

Date html generated: 2019_10_16-PM-01_06_08
Last ObjectModification: 2018_10_08-PM-00_18_42

Theory : factor_1

Home Index