Nuprl Lemma : mfact_exists_a
∀g:IAbMonoid
(Cancel(|g|;|g|;*)
⇒ WellFnd{i}(|g|;x,y.x p| y)
⇒ (∀c:|g|. Dec(Reducible(c)))
⇒ (∀c:|g|. Dec(g-unit(c)))
⇒ (∀b:|g|. ∃as:Atom{g} List. (b ~ (Π as))))
Proof
Definitions occuring in Statement :
matom_ty: Atom{g},
mreducible: Reducible(a),
mpdivides: a p| b,
massoc: a ~ b,
munit: g-unit(u),
mon_reduce: mon_reduce,
list: T List,
wellfounded: WellFnd{i}(A;x,y.R[x; y]),
decidable: Dec(P),
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
implies: P ⇒ Q,
iabmonoid: IAbMonoid,
grp_op: *,
grp_car: |g|,
cancel: Cancel(T;S;op)
Definitions unfolded in proof :
all: ∀x:A. B[x],
implies: P ⇒ Q,
member: t ∈ T,
uall: ∀[x:A]. B[x],
iabmonoid: IAbMonoid,
imon: IMonoid,
prop: ℙ,
so_lambda: λ2x.t[x],
so_apply: x[s],
so_lambda: λ2x y.t[x; y],
so_apply: x[s1;s2],
decidable: Dec(P),
or: P ∨ Q,
exists: ∃x:A. B[x],
mon_reduce: mon_reduce,
top: Top,
subtype_rel: A ⊆r B,
uimplies: b supposing a,
matom_ty: Atom{g},
iff: P ⇐⇒ Q,
and: P ∧ Q
Lemmas referenced :
grp_car_wf,
all_wf,
decidable_wf,
munit_wf,
mreducible_wf,
wellfounded_wf,
mpdivides_wf,
cancel_wf,
grp_op_wf,
iabmonoid_wf,
nil_wf,
matom_ty_wf,
reduce_nil_lemma,
massoc_wf,
mon_reduce_wf,
subtype_rel_list,
munit_char,
mfact_exists,
massoc_weakening
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
lambdaFormation,
cut,
lemma_by_obid,
sqequalHypSubstitution,
isectElimination,
thin,
setElimination,
rename,
hypothesisEquality,
hypothesis,
sqequalRule,
lambdaEquality,
dependent_functionElimination,
unionElimination,
dependent_pairFormation,
isect_memberEquality,
voidElimination,
voidEquality,
applyEquality,
independent_isectElimination,
because_Cache,
productElimination,
independent_functionElimination,
equalityTransitivity,
equalitySymmetry
Latex:
\mforall{}g:IAbMonoid
(Cancel(|g|;|g|;*)
{}\mRightarrow{} WellFnd\{i\}(|g|;x,y.x p| y)
{}\mRightarrow{} (\mforall{}c:|g|. Dec(Reducible(c)))
{}\mRightarrow{} (\mforall{}c:|g|. Dec(g-unit(c)))
{}\mRightarrow{} (\mforall{}b:|g|. \mexists{}as:Atom\{g\} List. (b \msim{} (\mPi{} as))))
Date html generated:
2016_05_16-AM-07_44_56
Last ObjectModification:
2015_12_28-PM-05_54_06
Theory : factor_1
Home
Index