theorem Subgraph.Equation1_true (G : Type u_1) [Magma G] : Equation1 G

theorem Subgraph.Equation2_implies_Equation3 (G : Type u_1) [Magma G] (h : Equation2 G) : Equation3 G

theorem Subgraph.Equation2_implies_Equation4 (G : Type u_1) [Magma G] (h : Equation2 G) : Equation4 G

theorem Subgraph.Equation2_implies_Equation5 (G : Type u_1) [Magma G] (h : Equation2 G) : Equation5 G

theorem Subgraph.Equation2_implies_Equation6 (G : Type u_1) [Magma G] (h : Equation2 G) : Equation6 G

theorem Subgraph.Equation2_implies_Equation7 (G : Type u_1) [Magma G] (h : Equation2 G) : Equation7 G

theorem Subgraph.Equation2_implies_Equation8 (G : Type u_1) [Magma G] (h : Equation2 G) : Equation8 G

theorem Subgraph.Equation2_implies_Equation23 (G : Type u_1) [Magma G] (h : Equation2 G) : Equation23 G

theorem Subgraph.Equation2_implies_Equation38 (G : Type u_1) [Magma G] (h : Equation2 G) : Equation38 G

theorem Subgraph.Equation2_implies_Equation39 (G : Type u_1) [Magma G] (h : Equation2 G) : Equation39 G

theorem Subgraph.Equation2_implies_Equation40 (G : Type u_1) [Magma G] (h : Equation2 G) : Equation40 G

theorem Subgraph.Equation2_implies_Equation41 (G : Type u_1) [Magma G] (h : Equation2 G) : Equation41 G

theorem Subgraph.Equation2_implies_Equation42 (G : Type u_1) [Magma G] (h : Equation2 G) : Equation42 G

theorem Subgraph.Equation2_implies_Equation43 (G : Type u_1) [Magma G] (h : Equation2 G) : Equation43 G

theorem Subgraph.Equation2_implies_Equation46 (G : Type u_1) [Magma G] (h : Equation2 G) : Equation46 G

theorem Subgraph.Equation2_implies_Equation168 (G : Type u_1) [Magma G] (h : Equation2 G) : Equation168 G

theorem Subgraph.Equation2_implies_Equation387 (G : Type u_1) [Magma G] (h : Equation2 G) : Equation387 G

theorem Subgraph.Equation2_implies_Equation1689 (G : Type u_1) [Magma G] (h : Equation2 G) : Equation1689 G

theorem Subgraph.Equation2_implies_Equation4512 (G : Type u_1) [Magma G] (h : Equation2 G) : Equation4512 G

theorem Subgraph.Equation2_implies_Equation4513 (G : Type u_1) [Magma G] (h : Equation2 G) : Equation4513 G

theorem Subgraph.Equation2_implies_Equation4522 (G : Type u_1) [Magma G] (h : Equation2 G) : Equation4522 G

theorem Subgraph.Equation2_implies_Equation4582 (G : Type u_1) [Magma G] (h : Equation2 G) : Equation4582 G

theorem Subgraph.Equation3_implies_Equation8 (G : Type u_1) [Magma G] (h : Equation3 G) : Equation8 G

theorem Subgraph.Equation3_implies_Equation23 (G : Type u_1) [Magma G] (h : Equation3 G) : Equation23 G

theorem Subgraph.Equation4_implies_Equation3 (G : Type u_1) [Magma G] (h : Equation4 G) : Equation3 G

theorem Subgraph.Equation4_implies_Equation8 (G : Type u_1) [Magma G] (h : Equation4 G) : Equation8 G

theorem Subgraph.Equation4_implies_Equation23 (G : Type u_1) [Magma G] (h : Equation4 G) : Equation23 G

theorem Subgraph.Equation4_implies_Equation42 (G : Type u_1) [Magma G] (h : Equation4 G) : Equation42 G

theorem Subgraph.Equation4_implies_Equation4522 (G : Type u_1) [Magma G] (h : Equation4 G) : Equation4522 G

theorem Subgraph.Equation5_implies_Equation3 (G : Type u_1) [Magma G] (h : Equation5 G) : Equation3 G

theorem Subgraph.Equation5_implies_Equation8 (G : Type u_1) [Magma G] (h : Equation5 G) : Equation8 G

theorem Subgraph.Equation5_implies_Equation23 (G : Type u_1) [Magma G] (h : Equation5 G) : Equation23 G

theorem Subgraph.Equation5_implies_Equation39 (G : Type u_1) [Magma G] (h : Equation5 G) : Equation39 G

theorem Subgraph.Equation5_implies_Equation4512 (G : Type u_1) [Magma G] (h : Equation5 G) : Equation4512 G

theorem Subgraph.Equation6_implies_Equation2 (G : Type u_1) [Magma G] (h : Equation6 G) : Equation2 G

theorem Subgraph.Equation6_implies_Equation3 (G : Type u_1) [Magma G] (h : Equation6 G) : Equation3 G

theorem Subgraph.Equation7_implies_Equation2 (G : Type u_1) [Magma G] (h : Equation7 G) : Equation2 G

theorem Subgraph.Equation7_implies_Equation3 (G : Type u_1) [Magma G] (h : Equation7 G) : Equation3 G

theorem Subgraph.Equation7_implies_Equation41 (G : Type u_1) [Magma G] (h : Equation7 G) : Equation41 G

theorem Subgraph.Equation14_implies_Equation29 (G : Type u_1) [Magma G] (h : Equation14 G) : Equation29 G

Dual to Problem A1 from Putnam 2001

theorem Subgraph.Equation29_implies_Equation14 (G : Type u_1) [Magma G] (h : Equation29 G) : Equation14 G

This implication is Problem A1 from Putnam 2001

theorem Subgraph.Equation38_implies_Equation42 (G : Type u_1) [Magma G] (h : Equation38 G) : Equation42 G

theorem Subgraph.Equation39_implies_Equation45 (G : Type u_1) [Magma G] (h : Equation39 G) : Equation45 G

theorem Subgraph.Equation41_implies_Equation39 (G : Type u_1) [Magma G] (h : Equation41 G) : Equation39 G

theorem Subgraph.Equation41_implies_Equation40 (G : Type u_1) [Magma G] (h : Equation41 G) : Equation40 G

theorem Subgraph.Equation41_implies_Equation46 (G : Type u_1) [Magma G] (h : Equation41 G) : Equation46 G

theorem Subgraph.Equation42_implies_Equation38 (G : Type u_1) [Magma G] (h : Equation42 G) : Equation38 G

theorem Subgraph.Equation45_implies_Equation39 (G : Type u_1) [Magma G] (h : Equation45 G) : Equation39 G

theorem Subgraph.Equation46_implies_Equation39 (G : Type u_1) [Magma G] (h : Equation46 G) : Equation39 G

theorem Subgraph.Equation46_implies_Equation40 (G : Type u_1) [Magma G] (h : Equation46 G) : Equation40 G

theorem Subgraph.Equation46_implies_Equation41 (G : Type u_1) [Magma G] (h : Equation46 G) : Equation41 G

theorem Subgraph.Equation46_implies_Equation42 (G : Type u_1) [Magma G] (h : Equation46 G) : Equation42 G

theorem Subgraph.Equation46_implies_Equation387 (G : Type u_1) [Magma G] (h : Equation46 G) : Equation387 G

theorem Subgraph.Equation46_implies_Equation4582 (G : Type u_1) [Magma G] (h : Equation46 G) : Equation4582 G

theorem Subgraph.Equation387_implies_Equation43 (G : Type u_1) [Magma G] (h : Equation387 G) : Equation43 G

This proof is from https://mathoverflow.net/a/450905/766

theorem Subgraph.Equation1571_implies_Equation2662 (G : Type u_1) [Magma G] (h : Equation1571 G) : Equation2662 G

The below results for Equation1571 are out of order because early ones are lemmas for later ones

theorem Subgraph.Equation1571_implies_Equation40 (G : Type u_1) [Magma G] (h : Equation1571 G) : Equation40 G

theorem Subgraph.Equation1571_implies_Equation23 (G : Type u_1) [Magma G] (h : Equation1571 G) : Equation23 G

theorem Subgraph.Equation1571_implies_Equation8 (G : Type u_1) [Magma G] (h : Equation1571 G) : Equation8 G

theorem Subgraph.Equation1571_implies_Equation16 (G : Type u_1) [Magma G] (h : Equation1571 G) : Equation16 G

theorem Subgraph.Equation1571_implies_Equation43 (G : Type u_1) [Magma G] (h : Equation1571 G) : Equation43 G

theorem Subgraph.Equation1571_implies_Equation4512 (G : Type u_1) [Magma G] (h : Equation1571 G) : Equation4512 G

theorem Subgraph.ProveEquation1571Consequence {n : ℕ} {G : Type u_1} [Magma G] (eq1571 : Equation1571 G) (law : Law.MagmaLaw (Fin (n + 1))) (eq : equation1571Reducer law.lhs = equation1571Reducer law.rhs) : G ⊧ law

theorem Subgraph.Equation1571_implies_Equation3167 {G : Type} [Magma G] (h : Equation1571 G) : Equation3167 G

theorem Subgraph.Equation1571_implies_Equation4656 {G : Type} [Magma G] (h : Equation1571 G) : Equation4656 G

@[reducible, inline]

abbrev Subgraph.Eq1689.pow3 {G : Type u_1} [Magma G] (a : G) : G

Equations

• Subgraph.Eq1689.pow3 a = (a ◇ a) ◇ a

@[reducible, inline]

abbrev Subgraph.Eq1689.pow5 {G : Type u_1} [Magma G] (a : G) : G

Equations

• Subgraph.Eq1689.pow5 a = (Subgraph.Eq1689.pow3 a ◇ a) ◇ a

@[reducible, inline]

abbrev Subgraph.Eq1689.f {G : Type u_1} [Magma G] (a b : G) : G

Equations

• Subgraph.Eq1689.f a b = (a ◇ b) ◇ b

@[reducible, inline]

abbrev Subgraph.Eq1689.g {G : Type u_1} [Magma G] (a b : G) : G

Equations

• Subgraph.Eq1689.g a b = a ◇ ((a ◇ b) ◇ b)

theorem Subgraph.Eq1689.lem_fixf_implies_eq2 {G : Type u_1} [Magma G] (h : Equation1689 G) (hfixf : ∀ (b : G), ∃ (c : G), f b c = b) : Equation2 G

theorem Subgraph.Eq1689.lem_1 {G : Type u_1} [Magma G] (h : Equation1689 G) (a b c : G) : a ◇ f (f a b) c = f a b

theorem Subgraph.Eq1689.lem_2 {G : Type u_1} [Magma G] (h : Equation1689 G) (a b c : G) : a ◇ g b c = f a b

theorem Subgraph.Eq1689.lem_fixf {G : Type u_1} [Magma G] (h : Equation1689 G) (a : G) : ∃ (b : G), f a b = a

theorem Subgraph.Equation1689_implies_Equation2 (G : Type u_1) [Magma G] (h : Equation1689 G) : Equation2 G

This result was first obtained by Kisielewicz in 1997 via computer assistance.

theorem Subgraph.Equation3744_implies_Equation381 (G : Type u_1) [Magma G] (h : Equation3744 G) : Equation381 G

Putnam 1978, problem A4, part (b)

theorem Subgraph.Equation3744_implies_Equation3722 (G : Type u_1) [Magma G] (h : Equation3744 G) : Equation3722 G

Putnam 1978, problem A4, part (a)

theorem Subgraph.Equation4513_implies_Equation4512 (G : Type u_1) [Magma G] (h : Equation4513 G) : Equation4512 G

theorem Subgraph.Equation4522_implies_Equation4513 (G : Type u_1) [Magma G] (h : Equation4522 G) : Equation4513 G

theorem Subgraph.Equation4582_implies_Equation4522 (G : Type u_1) [Magma G] (h : Equation4582 G) : Equation4522 G

theorem Subgraph.Equation4582_implies_Equation4564 (G : Type u_1) [Magma G] (h : Equation4582 G) : Equation4564 G

theorem Subgraph.Equation4582_implies_Equation4579 (G : Type u_1) [Magma G] (h : Equation4582 G) : Equation4579 G

theorem Subgraph.Equation953_implies_Equation2 (G : Type u_1) [Magma G] (h : Equation953 G) : Equation2 G

theorem Subgraph.Equation14_implies_Equation23 (G : Type u_1) [Magma G] (h : Equation14 G) : Equation23 G

theorem Subgraph.Equation14_implies_Equation8 (G : Type u_1) [Magma G] (h : Equation14 G) : Equation8 G

theorem Subgraph.Equation2_implies_Equation14 (G : Type u_1) [Magma G] (h : Equation2 G) : Equation14 G

theorem Subgraph.Equation2_implies_Equation381 (G : Type u_1) [Magma G] (h : Equation2 G) : Equation381 G

theorem Subgraph.Equation2_implies_Equation3722 (G : Type u_1) [Magma G] (h : Equation2 G) : Equation3722 G

theorem Subgraph.Equation2_implies_Equation3744 (G : Type u_1) [Magma G] (h : Equation2 G) : Equation3744 G

theorem Subgraph.Equation2_implies_Equation5093 (G : Type u_1) [Magma G] (h : Equation2 G) : Equation5093 G

theorem Subgraph.Equation2_implies_Equation374794 (G : Type u_1) [Magma G] (h : Equation2 G) : Equation374794 G

theorem Subgraph.Equation3_implies_Equation3722 (G : Type u_1) [Magma G] (h : Equation3 G) : Equation3722 G

theorem Subgraph.Equation4_implies_Equation381 (G : Type u_1) [Magma G] (h : Equation4 G) : Equation381 G

theorem Subgraph.Equation4_implies_Equation3722 (G : Type u_1) [Magma G] (h : Equation4 G) : Equation3722 G

theorem Subgraph.Equation4_implies_Equation3744 (G : Type u_1) [Magma G] (h : Equation4 G) : Equation3744 G

theorem Subgraph.Equation5_implies_Equation381 (G : Type u_1) [Magma G] (h : Equation5 G) : Equation381 G

theorem Subgraph.Equation5_implies_Equation3722 (G : Type u_1) [Magma G] (h : Equation5 G) : Equation3722 G

theorem Subgraph.Equation5_implies_Equation3744 (G : Type u_1) [Magma G] (h : Equation5 G) : Equation3744 G

theorem Subgraph.Equation5_implies_Equation4564 (G : Type u_1) [Magma G] (h : Equation5 G) : Equation4564 G

theorem Subgraph.Equation5_implies_Equation4579 (G : Type u_1) [Magma G] (h : Equation5 G) : Equation4579 G

theorem Subgraph.Equation39_implies_Equation381 (G : Type u_1) [Magma G] (h : Equation39 G) : Equation381 G

theorem Subgraph.Equation41_implies_Equation381 (G : Type u_1) [Magma G] (h : Equation41 G) : Equation381 G

theorem Subgraph.Equation41_implies_Equation3722 (G : Type u_1) [Magma G] (h : Equation41 G) : Equation3722 G

theorem Subgraph.Equation41_implies_Equation3744 (G : Type u_1) [Magma G] (h : Equation41 G) : Equation3744 G

theorem Subgraph.Equation45_implies_Equation381 (G : Type u_1) [Magma G] (h : Equation45 G) : Equation381 G

theorem Subgraph.Equation46_implies_Equation381 (G : Type u_1) [Magma G] (h : Equation46 G) : Equation381 G

theorem Subgraph.Equation46_implies_Equation3722 (G : Type u_1) [Magma G] (h : Equation46 G) : Equation3722 G

theorem Subgraph.Equation46_implies_Equation3744 (G : Type u_1) [Magma G] (h : Equation46 G) : Equation3744 G

theorem Subgraph.Equation3744_implies_Equation4512 (G : Type u_1) [Magma G] (h : Equation3744 G) : Equation4512 G

theorem Subgraph.Equation4564_implies_Equation4512 (G : Type u_1) [Magma G] (h : Equation4564 G) : Equation4512 G

theorem Subgraph.Equation4579_implies_Equation4512 (G : Type u_1) [Magma G] (h : Equation4579 G) : Equation4512 G

theorem Subgraph.Equation4579_implies_Equation4564 (G : Type u_1) [Magma G] (h : Equation4579 G) : Equation4564 G

theorem Subgraph.Equation4512_implies_Equation910472 (G : Type u_1) [Magma G] (h : Equation4512 G) : Equation910472 G

The Bol loop and Moufang loop identities are all weakenings of t

theorem Subgraph.Equation4512_implies_Equation930594 (G : Type u_1) [Magma G] (h : Equation4512 G) : Equation930594 G

theorem Subgraph.Equation4512_implies_Equation914612 (G : Type u_1) [Magma G] (h : Equation4512 G) : Equation914612 G

theorem Subgraph.Equation4512_implies_Equation916037 (G : Type u_1) [Magma G] (h : Equation4512 G) : Equation916037 G

theorem Subgraph.Equation4512_implies_Equation936498 (G : Type u_1) [Magma G] (h : Equation4512 G) : Equation936498 G

theorem Subgraph.Equation4512_implies_Equation921941 (G : Type u_1) [Magma G] (h : Equation4512 G) : Equation921941 G

theorem Subgraph.Equation3_not_implies_Equation39 : ∃ (G : Type) (x : Magma G), Equation3 G ∧ ¬Equation39 G

theorem Subgraph.Equation3_not_implies_Equation42 : ∃ (G : Type) (x : Magma G), Equation3 G ∧ ¬Equation42 G

theorem Subgraph.Equation3_not_implies_Equation4512 : ∃ (G : Type) (x : Magma G), Equation3 G ∧ ¬Equation4512 G

theorem Subgraph.Equation4_not_implies_Equation39 : ∃ (G : Type) (x : Magma G), Equation4 G ∧ ¬Equation39 G

theorem Subgraph.Equation4_not_implies_Equation40 : ∃ (G : Type) (x : Magma G), Equation4 G ∧ ¬Equation40 G

theorem Subgraph.Equation4_not_implies_Equation43 : ∃ (G : Type) (x : Magma G), Equation4 G ∧ ¬Equation43 G

theorem Subgraph.Equation4_not_implies_Equation4582 : ∃ (G : Type) (x : Magma G), Equation4 G ∧ ¬Equation4582 G

theorem Subgraph.Equation5_not_implies_Equation42 : ∃ (G : Type) (x : Magma G), Equation5 G ∧ ¬Equation42 G ∧ ¬Equation43 G ∧ ¬Equation4513 G

theorem Subgraph.Equation8_not_implies_Equation3 : ∃ (G : Type) (x : Magma G), Equation8 G ∧ ¬Equation3 G

theorem Subgraph.Equation23_not_implies_Equation3 : ∃ (G : Type) (x : Magma G), Equation23 G ∧ ¬Equation3 G

theorem Subgraph.Equation23_not_implies_Equation14 : ∃ (G : Type) (x : Magma G), Equation23 G ∧ ¬Equation14 G

theorem Subgraph.Equation38_not_implies_Equation23 : ∃ (G : Type) (x : Magma G), Equation38 G ∧ ¬Equation23 G

theorem Subgraph.Equation23_not_implies_Equation39 : ∃ (G : Type) (x : Magma G), Equation23 G ∧ ¬Equation39 G

theorem Subgraph.Equation39_not_implies_Equation8 : ∃ (G : Type) (x : Magma G), Equation39 G ∧ ¬Equation8 G

theorem Subgraph.Equation39_not_implies_Equation23 : ∃ (G : Type) (x : Magma G), Equation39 G ∧ ¬Equation23 G

theorem Subgraph.Equation39_not_implies_Equation40 : ∃ (G : Type) (x : Magma G), Equation39 G ∧ ¬Equation40 G

theorem Subgraph.Equation39_not_implies_Equation168 : ∃ (G : Type) (x : Magma G), Equation39 G ∧ ¬Equation168 G

theorem Subgraph.Equation39_not_implies_Equation4512 : ∃ (G : Type) (x : Magma G), Equation39 G ∧ ¬Equation4512 G

theorem Subgraph.Equation39_not_implies_Equation4513 : ∃ (G : Type) (x : Magma G), Equation39 G ∧ ¬Equation4513 G

theorem Subgraph.Equation39_not_implies_Equation4522 : ∃ (G : Type) (x : Magma G), Equation39 G ∧ ¬Equation4522 G

theorem Subgraph.Equation39_not_implies_Equation4564 : ∃ (G : Type) (x : Magma G), Equation39 G ∧ ¬Equation4564 G

theorem Subgraph.Equation39_not_implies_Equation4579 : ∃ (G : Type) (x : Magma G), Equation39 G ∧ ¬Equation4579 G

theorem Subgraph.Equation39_not_implies_Equation4582 : ∃ (G : Type) (x : Magma G), Equation39 G ∧ ¬Equation4582 G

theorem Subgraph.Equation40_not_implies_Equation3 : ∃ (G : Type) (x : Magma G), Equation40 G ∧ ¬Equation3 G

theorem Subgraph.Equation40_not_implies_Equation39 : ∃ (G : Type) (x : Magma G), Equation40 G ∧ ¬Equation39 G

theorem Subgraph.Equation40_not_implies_Equation42 : ∃ (G : Type) (x : Magma G), Equation40 G ∧ ¬Equation42 G

theorem Subgraph.Equation40_not_implies_Equation43 : ∃ (G : Type) (x : Magma G), Equation40 G ∧ ¬Equation43 G

theorem Subgraph.Equation40_not_implies_Equation4512 : ∃ (G : Type) (x : Magma G), Equation40 G ∧ ¬Equation4512 G

theorem Subgraph.Equation42_not_implies_Equation43 : ∃ (G : Type) (x : Magma G), Equation42 G ∧ ¬Equation43 G

theorem Subgraph.Equation42_not_implies_Equation4512 : ∃ (G : Type) (x : Magma G), Equation42 G ∧ ¬Equation4512 G

theorem Subgraph.Equation43_not_implies_Equation3 : ∃ (G : Type) (x : Magma G), Equation43 G ∧ ¬Equation3 G

theorem Subgraph.Equation43_not_implies_Equation39 : ∃ (G : Type) (x : Magma G), Equation43 G ∧ ¬Equation3 G

theorem Subgraph.Equation43_not_implies_Equation42 : ∃ (G : Type) (x : Magma G), Equation43 G ∧ ¬Equation42 G

theorem Subgraph.Equation43_not_implies_Equation387 : ∃ (G : Type) (x : Magma G), Equation43 G ∧ ¬Equation387 G

theorem Subgraph.Equation43_not_implies_Equation4512 : ∃ (G : Type) (x : Magma G), Equation43 G ∧ ¬Equation4512 G

theorem Subgraph.Equation46_not_implies_Equation3 : ∃ (G : Type) (x : Magma G), Equation46 G ∧ ¬Equation3 G

theorem Subgraph.Equation46_not_implies_Equation4 : ∃ (G : Type) (x : Magma G), Equation46 G ∧ ¬Equation4 G

theorem Subgraph.Equation168_not_implies_Equation8 : ∃ (G : Type) (x : Magma G), Equation168 G ∧ ¬Equation8 G

theorem Subgraph.Equation168_not_implies_Equation23 : ∃ (G : Type) (x : Magma G), Equation168 G ∧ ¬Equation23 G

theorem Subgraph.Equation168_not_implies_Equation39 : ∃ (G : Type) (x : Magma G), Equation168 G ∧ ¬Equation39 G

theorem Subgraph.Equation387_not_implies_Equation39 : ∃ (G : Type) (x : Magma G), Equation387 G ∧ ¬Equation39 G

theorem Subgraph.Equation387_not_implies_Equation40 : ∃ (G : Type) (x : Magma G), Equation387 G ∧ ¬Equation40 G

theorem Subgraph.Equation387_not_implies_Equation42 : ∃ (G : Type) (x : Magma G), Equation387 G ∧ ¬Equation42 G

theorem Subgraph.Equation387_not_implies_Equation4512 : ∃ (G : Type) (x : Magma G), Equation387 G ∧ ¬Equation4512 G

theorem Subgraph.Equation4512_not_implies_Equation42 : ∃ (G : Type) (x : Magma G), Equation4512 G ∧ ¬Equation42 G

theorem Subgraph.Equation4512_not_implies_Equation4513 : ∃ (G : Type) (x : Magma G), Equation4512 G ∧ ¬Equation4513 G

theorem Subgraph.Equation4513_not_implies_Equation4522 : ∃ (G : Type) (x : Magma G), Equation4513 G ∧ ¬Equation4522 G

inductive Subgraph.Th : Type

• t1 : Th
• t2 : Th
• t3 : Th

def Subgraph.add : Th → Th → Th

Equations

• Subgraph.add Subgraph.Th.t1 Subgraph.Th.t1 = Subgraph.Th.t2
• Subgraph.add Subgraph.Th.t1 Subgraph.Th.t2 = Subgraph.Th.t3
• Subgraph.add Subgraph.Th.t1 Subgraph.Th.t3 = Subgraph.Th.t3
• Subgraph.add Subgraph.Th.t2 Subgraph.Th.t1 = Subgraph.Th.t3
• Subgraph.add Subgraph.Th.t2 Subgraph.Th.t2 = Subgraph.Th.t3
• Subgraph.add Subgraph.Th.t2 Subgraph.Th.t3 = Subgraph.Th.t3
• Subgraph.add Subgraph.Th.t3 x✝ = Subgraph.Th.t3

theorem Subgraph.add3 (a b c : Th) : add (add a b) c = Th.t3

theorem Subgraph.add3_ (a b c : Th) : add a (add b c) = Th.t3

theorem Subgraph.Equation4582_not_implies_Equation39 : ∃ (G : Type) (x : Magma G), Equation4582 G ∧ ¬Equation39 G

theorem Subgraph.Equation4582_not_implies_Equation40 : ∃ (G : Type) (x : Magma G), Equation4582 G ∧ ¬Equation40 G

theorem Subgraph.Equation4582_not_implies_Equation42 : ∃ (G : Type) (x : Magma G), Equation4582 G ∧ ¬Equation42 G

theorem Subgraph.Equation4582_not_implies_Equation43 : ∃ (G : Type) (x : Magma G), Equation4582 G ∧ ¬Equation43 G

theorem Subgraph.Equation4582_not_implies_Equation46 : ∃ (G : Type) (x : Magma G), Equation4582 G ∧ ¬Equation46 G

theorem Subgraph.Equation43_not_implies_Equation910472 : ∃ (G : Type) (x : Magma G), Equation43 G ∧ ¬Equation910472 G

theorem Subgraph.Equation3_not_implies_Equation910472 : ∃ (G : Type) (x : Magma G), Equation3 G ∧ ¬Equation910472 G

theorem Subgraph.Equation43_not_implies_Equation930594 : ∃ (G : Type) (x : Magma G), Equation43 G ∧ ¬Equation930594 G

theorem Subgraph.Equation3_not_implies_Equation930594 : ∃ (G : Type) (x : Magma G), Equation3 G ∧ ¬Equation930594 G

theorem Subgraph.Equation43_not_implies_Equation914612 : ∃ (G : Type) (x : Magma G), Equation43 G ∧ ¬Equation914612 G

theorem Subgraph.Equation3_not_implies_Equation914612 : ∃ (G : Type) (x : Magma G), Equation3 G ∧ ¬Equation914612 G

theorem Subgraph.Equation43_not_implies_Equation916037 : ∃ (G : Type) (x : Magma G), Equation43 G ∧ ¬Equation916037 G

theorem Subgraph.Equation3_not_implies_Equation916037 : ∃ (G : Type) (x : Magma G), Equation3 G ∧ ¬Equation916037 G

theorem Subgraph.Equation43_not_implies_Equation936498 : ∃ (G : Type) (x : Magma G), Equation43 G ∧ ¬Equation936498 G

theorem Subgraph.Equation3_not_implies_Equation936498 : ∃ (G : Type) (x : Magma G), Equation3 G ∧ ¬Equation936498 G

theorem Subgraph.Equation3_not_implies_Equation921941 : ∃ (G : Type) (x : Magma G), Equation3 G ∧ ¬Equation921941 G

theorem Subgraph.Equation43_not_implies_Equation921941 : ∃ (G : Type) (x : Magma G), Equation43 G ∧ ¬Equation921941 G