added two requests to blueprint

teorth · Sep 26, 2024 · 211d2f7 · 211d2f7
1 parent 7844b2a
commit 211d2f7
Show file tree

Hide file tree

Showing 3 changed files with 18 additions and 0 deletions.
diff --git a/blueprint/src/chapter/counterexamples.tex b/blueprint/src/chapter/counterexamples.tex
@@ -66,3 +66,15 @@ \chapter{Counterexamples}
 
 \begin{proof}\leanok Use the natural numbers $\N$ with operation $x \circ y := x + y$.
 \end{proof}
+
+\begin{theorem}[Equation 387 does not imply Equation 42]\label{387_not_imply_42}\lean{Equation387_not_implies_Equation42}\leanok\uses{eq387,eq42} Definition \ref{eq387} does not imply Definition \ref{eq42}.
+\end{theorem}
+
+\begin{proof} ???
+\end{proof}
+
+\begin{theorem}[Equation 43 does not imply Equation 387]\label{43_not_imply_387}\lean{Equation43_not_implies_Equation387}\leanok\uses{eq43,eq387} Definition \ref{eq43} does not imply Definition \ref{eq387}.
+\end{theorem}
+
+\begin{proof} ???
+\end{proof}
diff --git a/blueprint/src/print.pdf b/blueprint/src/print.pdf
diff --git a/equational_theories/Basic.lean b/equational_theories/Basic.lean
@@ -243,3 +243,9 @@ theorem Equation4512_not_implies_Equation42 : ∃ (G: Type) (_: Magma G), Equati
   replace h := h 0 0 1
   dsimp [hG] at h
   linarith
+
+theorem Equation387_not_implies_Equation42 : ∃ (G: Type) (_: Magma G), Equation387 G ∧ ¬ Equation42 G := by
+  sorry
+
+theorem Equation43_not_implies_Equation387 : ∃ (G: Type) (_: Magma G), Equation387 G ∧ ¬ Equation42 G := by
+  sorry