theorem InfModel.Finite.Equation374794_implies_Equation2 (G : Type u_1) [Magma G] [Finite G] (h : Equation374794 G) : Equation2 G

In a finite model Equation374794 implies Equation2, that the model is a subsingleton.

theorem InfModel.Equation374794_not_implies_Equation2 : ∃ (G : Type) (x : Magma G), Equation374794 G ∧ ¬Equation2 G

However, Equation374794 doesn't imply Equation2.

theorem InfModel.Finite.Equation5093_implies_Equation2 (G : Type u_1) [Magma G] [Finite G] (h : Equation5093 G) : Equation2 G

theorem InfModel.Finite.Equation28770_implies_Equation2 (G : Type u_1) [Magma G] [Finite G] (h : Equation28770 G) : Equation2 G

theorem InfModel.Equation28770_not_implies_Equation2 : ∃ (G : Type) (x : Magma G), Equation28770 G ∧ ¬Equation2 G

theorem InfModel.Finite.Equation3994_implies_Equation3588 (G : Type u_1) [Magma G] [Finite G] (h : Equation3994 G) : Equation3588 G

theorem InfModel.Equation3994_not_implies_Equation3588 : ∃ (G : Type) (x : Magma G), Equation3994 G ∧ ¬Equation3588 G

theorem InfModel.Equation3588_not_implies_Equation3994 : ∃ (G : Type) (x : Magma G), Equation3588 G ∧ ¬Equation3994 G

Dual of the above.

theorem InfModel.Finite.Equation206_implies_Equation1648 (G : Type u_1) [Magma G] [Finite G] (h : Equation206 G) : Equation1648 G

noncomputable def InfModel.word_polynomial : FreeMagma (Fin 2) → Polynomial ℤ

Equations

• InfModel.word_polynomial (w1 ⋆ w2) = (1 - Polynomial.X) * InfModel.word_polynomial w1 + Polynomial.X * InfModel.word_polynomial w2
• InfModel.word_polynomial (Lf z) = 1 - ↑↑z

theorem InfModel.zero_lt_degree_word_polynomial (w : FreeMagma (Fin 2)) : FreeMagma.Mem 0 w → w.first = 1 → w.last = 1 → 0 < (word_polynomial w).degree

theorem InfModel.Finite.two_variable_laws {α : Type} [ht : Fintype α] (hc : Fintype.card α = 2) (E : Law.MagmaLaw α) (z : α) : FreeMagma.Mem z E.lhs → FreeMagma.Mem z E.rhs → ∃ (G : Type) (x : Magma G), Finite G ∧ ¬Equation2 G ∧ G ⊧ E