diff options
Diffstat (limited to 'libnormalform_any.c')
| -rw-r--r-- | libnormalform_any.c | 6 |
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); |