---

Definition: mdivides
b | a ==  ∃c:|g|. (a = (b * c) ∈ |g|)

Lemma: mdivides_wf
∀g:GrpSig. ∀a,b:|g|.  (a | b ∈ ℙ)

Lemma: comb_for_mdivides_wf
λg,a,b,z. (a | b) ∈ g:GrpSig ⟶ a:|g| ⟶ b:|g| ⟶ (↓True) ⟶ ℙ

Definition: rev_mdivides
a |by b in g ==  b | a

Lemma: rev_mdivides_wf
∀g:GrpSig. ∀a,b:|g|.  (a |by b in g ∈ ℙ)

Lemma: mdivides_id
∀g:IAbMonoid. ∀a:|g|.  (e | a)

Lemma: mdivides_refl
∀g:IAbMonoid. ∀a:|g|.  (a | a)

Lemma: mdivides_trans
∀g:IAbMonoid. ∀a,b,c:|g|.  ((a | b) ⇒ (b | c) ⇒ (a | c))

Lemma: mdivides_preorder
∀g:IAbMonoid. Preorder(|g|;x,y.x | y)

Lemma: mdivides_cancel
∀g:IAbMonoid. (Cancel(|g|;|g|;*) ⇒ (∀a,b,c:|g|.  (((a * b) | (a * c)) ⇒ (b | c))))

Definition: munit
g-unit(u) ==  u | e

Lemma: munit_wf
∀g:GrpSig. ∀a:|g|.  (g-unit(a) ∈ ℙ)

Definition: massoc
a ~ b ==  Symmetrize(x,y.x | y;a;b)

Lemma: massoc_wf
∀g:GrpSig. ∀a,b:|g|.  (a ~ b ∈ ℙ)

Lemma: munit_char
∀g:IAbMonoid. ∀a:|g|.  (g-unit(a) ⇐⇒ a ~ e)

Lemma: munit_of_op
∀g:IAbMonoid. ∀a,b:|g|.  ((g-unit(a * b)) ⇒ ((g-unit(a)) ∧ (g-unit(b))))

Definition: mpdivides
a p| b ==  (a | b) ∧ (¬(b | a))

Lemma: mpdivides_wf
∀g:GrpSig. ∀a,b:|g|.  (a p| b ∈ ℙ)

Lemma: non_munit_diff_imp_mpdivides
∀g:IAbMonoid. (Cancel(|g|;|g|;*) ⇒ (∀a,b,c:|g|.  ((¬(g-unit(b))) ⇒ ((a * b) = c ∈ |g|) ⇒ (a p| c))))

Lemma: comb_for_massoc_wf
λg,a,b,z. (a ~ b) ∈ g:GrpSig ⟶ a:|g| ⟶ b:|g| ⟶ (↓True) ⟶ ℙ

Lemma: mdivides_weakening
∀g:IAbMonoid. ∀a,b:|g|.  ((a ~ b) ⇒ (a | b))

Lemma: massoc_equiv_rel
∀g:IAbMonoid. EquivRel(|g|;x,y.x ~ y)

Lemma: massoc_weakening
∀g:IAbMonoid. ∀a,b:|g|.  ((a = b ∈ |g|) ⇒ (a ~ b))

Lemma: massoc_inversion
∀g:IAbMonoid. ∀a,b:|g|.  ((a ~ b) ⇒ (b ~ a))

Lemma: massoc_transitivity
∀g:IAbMonoid. ∀a,b,c:|g|.  ((a ~ b) ⇒ (b ~ c) ⇒ (a ~ c))

Lemma: grp_op_ap2_functionality_wrt_mdivides
∀g:IAbMonoid. ∀a,a',b,b':|g|.  ((a | b) ⇒ (a' | b') ⇒ ((a * a') | (b * b')))

Lemma: grp_op_ap2_functionality_wrt_massoc
∀g:IAbMonoid. ∀a,a',b,b':|g|.  ((a ~ b) ⇒ (a' ~ b') ⇒ ((a * a') ~ (b * b')))

Lemma: grp_op_functionality_wrt_massoc
∀g:IAbMonoid. ∀a,a',b,b':|g|.  ((a ~ b) ⇒ (a' ~ b') ⇒ ((a * a') ~ (b * b')))

Lemma: massoc_functionality_wrt_massoc
∀g:IAbMonoid. ∀a,a',b,b':|g|.  ((a ~ b) ⇒ (a' ~ b') ⇒ (a ~ a' ⇐⇒ b ~ b'))

Lemma: massoc_cancel
∀g:IAbMonoid. (Cancel(|g|;|g|;*) ⇒ (∀a,b,c:|g|.  (((a * b) ~ (a * c)) ⇒ (b ~ c))))

Lemma: massoc_imp_unit_diff
∀g:IAbMonoid. (Cancel(|g|;|g|;*) ⇒ (∀a,b:|g|.  ((a ~ b) ⇒ (∃u:|g|. ((g-unit(u)) c∧ (a = (u * b) ∈ |g|))))))

Definition: mprime
IsPrime(a) ==  (¬(g-unit(a))) ∧ (∀b,c:|g|.  ((a | (b * c)) ⇒ ((a | b) ∨ (a | c))))

Lemma: mprime_wf
∀g:GrpSig. ∀a:|g|.  (IsPrime(a) ∈ ℙ)

Definition: mprime_ty
Prime(g) ==  {x:|g|| IsPrime(x)} 

Lemma: mprime_ty_wf
∀g:GrpSig. (Prime(g) ∈ Type)

Lemma: sq_stable__mprime
∀g:GrpSig. ((∀a,b:|g|.  Dec(a | b)) ⇒ (∀c:|g|. SqStable(IsPrime(c))))

Lemma: mproper_div_cond
∀g:IAbMonoid. (Cancel(|g|;|g|;*) ⇒ (∀a,b:|g|.  (((a * b) | a) ⇒ (g-unit(b)))))

Definition: mreducible
Reducible(a) ==  ∃b,c:|g|. ((¬(g-unit(b))) ∧ (¬(g-unit(c))) ∧ (a = (b * c) ∈ |g|))

Lemma: mreducible_wf
∀g:GrpSig. ∀a:|g|.  (Reducible(a) ∈ ℙ)

Lemma: mreducible_elim
∀g:IAbMonoid. (Cancel(|g|;|g|;*) ⇒ (∀a:|g|. (Reducible(a) ⇐⇒ ∃b:|g|. ((¬(g-unit(b))) ∧ (b p| a)))))

Definition: matomic
Atomic(a) ==  (¬(g-unit(a))) ∧ (¬Reducible(a))

Lemma: matomic_wf
∀g:GrpSig. ∀a:|g|.  (Atomic(a) ∈ ℙ)

Lemma: mdivisor_of_atom_is_assoc2
∀g:IAbMonoid. ((∀a,b:|g|.  Stable{a | b}) ⇒ (∀a,b:|g|.  ((¬(g-unit(a))) ⇒ Atomic(b) ⇒ (a | b) ⇒ (a ~ b))))

Definition: matom_ty
Atom{g} ==  {a:|g|| Atomic(a)} 

Lemma: matom_ty_wf
∀g:GrpSig. (Atom{g} ∈ Type)

Lemma: matom_ty_properties
∀g:GrpSig. ∀a:Atom{g}.  Atomic(a)

Lemma: mcomp_imp_not_unit
∀g:IAbMonoid. ∀a:|g|.  (Reducible(a) ⇒ (¬(g-unit(a))))

Lemma: mprime_imp_matomic
∀g:IAbMonoid. (Cancel(|g|;|g|;*) ⇒ (∀a:|g|. (IsPrime(a) ⇒ Atomic(a))))

Lemma: mprime_divs_list_el
∀g:IAbMonoid. ∀p:|g|.  (IsPrime(p) ⇒ (∀as:|g| List. ((p | (Π as)) ⇒ (∃i:ℕ||as||. (p | as[i])))))

Definition: permr_massoc
as ≡ bs upto ~ ==  as ≡ bs upto x,y.x ~ y 

Lemma: permr_massoc_wf
∀g:GrpSig. ∀as,bs:|g| List.  (as ≡ bs upto ~ ∈ ℙ)

Lemma: permr_massoc_weakening
∀g:IAbMonoid. ∀as,bs:|g| List.  ((as ≡(|g|) bs) ⇒ as ≡ bs upto ~)

Lemma: permr_massoc_functionality
∀g:IAbMonoid. ∀as,as',bs,bs':|g| List.  (as ≡ bs upto ~ ⇒ as' ≡ bs' upto ~ ⇒ (as ≡ as' upto ~ ⇐⇒ bs ≡ bs' upto ~))

Lemma: cons_functionality_wrt_permr_massoc
∀g:IAbMonoid. ∀a,b:|g|. ∀as,bs:|g| List.  ((a ~ b) ⇒ as ≡ bs upto ~ ⇒ [a / as] ≡ [b / bs] upto ~)

Lemma: mfact_exists
∀g:IAbMonoid
  (Cancel(|g|;|g|;*)
  ⇒ WellFnd{i}(|g|;x,y.x p| y)
  ⇒ (∀c:|g|. Dec(Reducible(c)))
  ⇒ (∀b:|g|. ((¬(g-unit(b))) ⇒ (∃as:Atom{g} List. (b = (Π as) ∈ |g|)))))

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))))

Lemma: unique_mfact
∀g:IAbMonoid
  (Cancel(|g|;|g|;*) ⇒ (∀a,b:|g|.  Dec(a | b)) ⇒ (∀ps,qs:Prime(g) List.  (((Π ps) ~ (Π qs)) ⇒ ps ≡ qs upto ~)))

Definition: uni_sat_upto
a r !x:T. Q[x]  ==  Q[a] ∧ (∀a':T. (Q[a'] ⇒ (a' [r] a)))

Lemma: uni_sat_upto_wf
∀T:Type. ∀r:T ⟶ T ⟶ ℙ. ∀a:T. ∀Q:T ⟶ ℙ.  (a r !x:T. Q[x]  ∈ ℙ)

Definition: exists_uni_upto
(r)∃!x:T. Q[x] ==  ∃a:T. a r !x:T. Q[x] 

Lemma: exists_uni_upto_char
∀T:Type. ∀r:T ⟶ T ⟶ ℙ. ∀Q:T ⟶ ℙ.  ((∃x:T. Q[x]) ⇒ (∀x,y:T.  (Q[x] ⇒ Q[y] ⇒ (x [r] y))) ⇒ (r)∃!x:T. Q[x])

Lemma: exists_uni_upto_wf
∀T:Type. ∀r:T ⟶ T ⟶ ℙ. ∀Q:T ⟶ ℙ.  ((r)∃!x:T. Q[x] ∈ ℙ)

Definition: permr_massoc_rel
≡~ ==  as,bs:|g| List. as ≡ bs upto ~

Lemma: permr_massoc_rel_wf
∀g:GrpSig. (≡~ ∈ (|g| List) ⟶ (|g| List) ⟶ ℙ)

Definition: is_ufm
IsUFM(g) ==  ∀b:|g|. ((¬(g-unit(b))) ⇒ (≡~)∃!as:Atom{g} List. (b = (Π as) ∈ |g|))

Lemma: is_ufm_wf
∀g:IMonoid. (IsUFM(g) ∈ ℙ)

Lemma: ufm_char
∀g:IAbMonoid
  (Cancel(|g|;|g|;*)
  ⇒ WellFnd{i}(|g|;x,y.x p| y)
  ⇒ (∀a:Atom{g}. IsPrime(a))
  ⇒ (∀a:|g|. Dec(Reducible(a)))
  ⇒ (∀a,b:|g|.  Dec(a | b))
  ⇒ IsUFM(g))

Definition: posint_mul_mon
<ℤ+,*> ==  <ℕ+, λx,y. (x =z y), λx,y. x ≤z y, λx,y. (x * y), 1, λx.x>

Lemma: posint_mul_mon_wf
<ℤ+,*> ∈ AbMon

Lemma: posint_cancel
Cancel(|<ℤ+,*>|;|<ℤ+,*>|;*)

Lemma: posint_munit_elim
∀a:|<ℤ+,*>|. (<ℤ+,*>-unit(a) ⇐⇒ a = 1 ∈ ℤ)

Lemma: posint_well_fnd
WellFnd{i}(|<ℤ+,*>|;x,y.x p| y)

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

Lemma: posint_unit_dec
∀a:|<ℤ+,*>|. Dec(<ℤ+,*>-unit(a))

Lemma: posint_div_dec
∀a,b:|<ℤ+,*>|.  Dec(a | b)

Lemma: posint_atom_imp_prime
∀a:Atom{<ℤ+,*>}. IsPrime(a)

Lemma: posint_fact_exists
∀i:ℕ+. (∃ps:{j:ℕ+| prime(j)}  List [(i = (Π ps) ∈ ℤ)])

Lemma: posint_is_ufm
IsUFM(<ℤ+,*>)



Home Index