From 97fc90ae0b79a1f5d44f700b6504aacf12045629 Mon Sep 17 00:00:00 2001
From: Yung-Chi Chien <ukichi19857@gmail.com>
Date: Sat, 28 Sep 2024 14:05:32 +0800
Subject: [PATCH] SUBGRAPH: Prove 5 does not imply 42, 43, 4513

---
 equational_theories/Subgraph.lean | 24 ++++++++++++++++++++++++
 1 file changed, 24 insertions(+)

diff --git a/equational_theories/Subgraph.lean b/equational_theories/Subgraph.lean
index 666937a8..f8d1e153 100644
--- a/equational_theories/Subgraph.lean
+++ b/equational_theories/Subgraph.lean
@@ -185,6 +185,30 @@ theorem Equation4_not_implies_Equation4582 : ∃ (G: Type) (_: Magma G), Equatio
   dsimp [hG] at h
   linarith
 
+theorem Equation5_not_implies_Equation42 : ∃ (G: Type) (_: Magma G), Equation5 G ∧ ¬ Equation42 G := by
+  let a : Type := Fin 2
+  let hG : Magma a := { op := fun _ x ↦ x }
+  refine ⟨a, hG, fun _ ↦ by simp [hG], ?_⟩
+  by_contra h
+  specialize h 0 1 0
+  simp [hG] at h
+
+theorem Equation5_not_implies_Equation43 : ∃ (G: Type) (_: Magma G), Equation5 G ∧ ¬ Equation43 G := by
+  let a : Type := Fin 2
+  let hG : Magma a := { op := fun _ x ↦ x }
+  refine ⟨a, hG, fun _ ↦ by simp [hG], ?_⟩
+  by_contra h
+  specialize h 0 1
+  simp [hG] at h
+
+theorem Equation5_not_implies_Equation4513 : ∃ (G: Type) (_: Magma G), Equation5 G ∧ ¬ Equation4513 G := by
+  let a : Type := Fin 2
+  let hG : Magma a := { op := fun _ x ↦ x }
+  refine ⟨a, hG, fun _ ↦ by simp [hG], ?_⟩
+  by_contra h
+  specialize h 0 0 0 1
+  simp [hG] at h
+
 theorem Equation42_not_implies_Equation43 : ∃ (G: Type) (_: Magma G), Equation42 G ∧ ¬ Equation43 G := by
   let hG : Magma Nat := { op := fun x _ ↦ x }
   refine ⟨ℕ, hG, fun _ _ _ ↦ rfl, ?_⟩