diff options
| author | Mattias Andrée <m@maandree.se> | 2026-06-01 19:07:14 +0200 |
|---|---|---|
| committer | Mattias Andrée <m@maandree.se> | 2026-06-01 19:07:14 +0200 |
| commit | 77ade8d20906fe9ca2cf6788ff1e1437e0912868 (patch) | |
| tree | 61495e90e057bf792bb1d8ce157cef0ecc2ab696 /libnormalform_one.c | |
| parent | First commit (diff) | |
| download | libnormalform-77ade8d20906fe9ca2cf6788ff1e1437e0912868.tar.gz libnormalform-77ade8d20906fe9ca2cf6788ff1e1437e0912868.tar.bz2 libnormalform-77ade8d20906fe9ca2cf6788ff1e1437e0912868.tar.xz | |
Signed-off-by: Mattias Andrée <m@maandree.se>
Diffstat (limited to '')
| -rw-r--r-- | libnormalform_one.c | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/libnormalform_one.c b/libnormalform_one.c index b5c17f1..3219097 100644 --- a/libnormalform_one.c +++ b/libnormalform_one.c @@ -426,8 +426,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_one(&dom1, libnormalform_false(), libnormalform_false())); ASSERT_NOTEQUAL(a, b); libnormalform_free(b); |