diff options
Diffstat (limited to 'libnormalform_all.c')
| -rw-r--r-- | libnormalform_all.c | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/libnormalform_all.c b/libnormalform_all.c index 1b8d6fc..1d948fc 100644 --- a/libnormalform_all.c +++ b/libnormalform_all.c @@ -421,7 +421,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_all(&dom1, libnormalform_true(), libnormalform_true())); ASSERT_NOTEQUAL(a, b); libnormalform_free(b); @@ -429,8 +429,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.(⊤ → Q(y)) ∵ 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(y)) ∵ 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.(⊤ → Q(y)) ∵ 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(y)) ∵ P → ¬Q ⊭ P(x) → ¬Q(y) */ ASSUME(b = libnormalform_all(&dom1, libnormalform_true(), REF(v2))); ASSERT_NOTEQUAL(a, b); libnormalform_free(b); |