Second commitHEADmaster

Signed-off-by: Mattias Andrée <m@maandree.se>

1 files changed, 3 insertions, 3 deletions

diff --git a/libnormalform_any.c b/libnormalform_any.c
index 7e69210..1cd79fa 100644
--- a/libnormalform_any.c
+++ b/libnormalform_any.c
@@ -420,7 +420,7 @@ main(void)
 	ASSERT_NOTEQUAL(a, b);
 	libnormalform_free(b);
 
-	/* P = Q ⊭ ∃{x,y}∈X.(P(x) ∧ Q(y)) = ∃{x,y}∈X.(P(x) ∧ P(y)) = ∃{x,y}∈X.⊤ = ⊤ ∵ P = Q ⊭ P(x) = Q(y) */
+	/* P = Q ⊭ ∃⟨x,y⟩∈X.(P(x) ∧ Q(y)) = ∃⟨x,y⟩∈X.(P(x) ∧ P(y)) = ∃⟨x,y⟩∈X.⊤ = ⊤ ∵ P = Q ⊭ P(x) = Q(y) */
 	ASSUME(b = libnormalform_any(&dom1, libnormalform_true(), libnormalform_true()));
 	ASSERT_NOTEQUAL(a, b);
 	libnormalform_free(b);
@@ -428,8 +428,8 @@ main(void)
 	ASSERT_NOTEQUAL(a, b);
 	libnormalform_free(b);
 
-	/* P = ¬Q ⊭ ∃{x,y}∈X.(P(x) ∧ Q(y)) = ∃{x,y}∈X.(¬Q(x) ∧ Q(y)) = ∃{x,y}∈X.⊥ = ⊥ ∵ P = ¬Q ⊭ P(x) = ¬Q(y) */
-	/* P = ¬Q ⊭ ∃{x,y}∈X.(P(x) ∧ Q(y)) = ∃{x,y}∈X.(P(x) ∧ ¬P(y)) = ∃{x,y}∈X.⊥ = ⊥ ∵ P = ¬Q ⊭ P(x) = ¬Q(y) */
+	/* P = ¬Q ⊭ ∃⟨x,y⟩∈X.(P(x) ∧ Q(y)) = ∃⟨x,y⟩∈X.(¬Q(x) ∧ Q(y)) = ∃⟨x,y⟩∈X.⊥ = ⊥ ∵ P = ¬Q ⊭ P(x) = ¬Q(y) */
+	/* P = ¬Q ⊭ ∃⟨x,y⟩∈X.(P(x) ∧ Q(y)) = ∃⟨x,y⟩∈X.(P(x) ∧ ¬P(y)) = ∃⟨x,y⟩∈X.⊥ = ⊥ ∵ P = ¬Q ⊭ P(x) = ¬Q(y) */
 	ASSUME(b = libnormalform_any(&dom1, libnormalform_false(), libnormalform_false()));
 	ASSERT_NOTEQUAL(a, b);
 	libnormalform_free(b);