@@ -45,28 +45,29 @@ checkFormulas env beh trs defs (ProdCons (fp, ep) (fc, ec)) =
45 issues@(_ : _) -> for_ issues $ embedFormula beh . anItem
45 issues@(_ : _) -> for_ issues $ embedFormula beh . anItem
47 -- We have the following isomorphisms:
47 -- We have the following isomorphisms:
48− -- (A ⊂ X ∪ Y) = (A ⊂ X) \/ (A ⊂ Y)
49 -- (A ⊂ X ∩ Y) = (A ⊂ X) /\ (A ⊂ Y)
48 -- (A ⊂ X ∩ Y) = (A ⊂ X) /\ (A ⊂ Y)
50 -- (A ⊂ ⊤) = 1
49 -- (A ⊂ ⊤) = 1
51 -- (X ∪ Y ⊂ B) = (X ⊂ B) /\ (Y ⊂ B)
50 -- (X ∪ Y ⊂ B) = (X ⊂ B) /\ (Y ⊂ B)
52 -- (∅ ⊂ B) = 1
51 -- (∅ ⊂ B) = 1
53 -- The remaining cases are, notably, not isomorphisms:
52 -- The remaining cases are, notably, not isomorphisms:
54− -- 1) (A ⊂ ∅) <= 0
53+ -- 1) (A ⊂ X ∪ Y) <= (A ⊂ X) \/ (A ⊂ Y)
55− -- 2) (X ∩ Y ⊂ B) <= (X ⊂ B) \/ (Y ⊂ B)
54+ -- 2) (A ⊂ ∅) <= 0
55+ -- 3) (X ∩ Y ⊂ B) <= (X ⊂ B) \/ (Y ⊂ B)
56− -- 3) (⊤ ⊂ B) <= 0
56+ -- 4) (⊤ ⊂ B) <= 0
57− -- Therefore we have the isomorphisms with (∃ and ∀ being the N-ary
57+ -- Therefore we have the implications with (∃ and ∀ being the N-ary
58 -- versions of \/ and /\ respectively):
58 -- versions of \/ and /\ respectively):
59 -- (⋃_i ⋂_j A[i,j]) ⊂ (⋃_k ⋂_l B[k,l])
59 -- (⋃_i ⋂_j A[i,j]) ⊂ (⋃_k ⋂_l B[k,l])
60− -- = ∃k ∀l ∀i, (⋂_j A[i,j]) ⊂ B[k,l]
60+ -- <= ∃k ∀l ∀i, (⋂_j A[i,j]) ⊂ B[k,l]
61 -- = ∀i ∃k ∀l, (⋂_j A[i,j]) ⊂ B[k,l]
61 -- = ∀i ∃k ∀l, (⋂_j A[i,j]) ⊂ B[k,l]
62 -- with the caveat that the the set over which k ranges is nonempty.
62 -- with the caveat that the the set over which k ranges is nonempty.
63+ -- (because 2) is not an isomorphism), and that this is a sufficient
63− -- This is because 1) is not an isomorphism.
64+ -- but not necessary condition (because 1) is not an isomorphism).
64 -- Our disjunction loses information, so it makes sense to nest it as
65 -- Our disjunction loses information, so it makes sense to nest it as
65 -- deeply as possible, hence we choose the latter representation.
66 -- deeply as possible, hence we choose the latter representation.
67 -- We delegate the verification of (⋂_j A[j]) ⊂ B to a separate heuristic
68 -- We delegate the verification of (⋂_j A[j]) ⊂ B to a separate heuristic
68 -- function, with the understanding that ∃j, A[j] ⊂ B is a sufficient,
69 -- function, with the understanding that ∃j, A[j] ⊂ B is a sufficient,
69− -- but not necessary condition (because of 2) and 3)).
70+ -- but not necessary condition (because of 3) and 4)).
71 -- If k ranges over an empty set, we have the isomorphism:
72 -- If k ranges over an empty set, we have the isomorphism:
72 -- (⋃_i ⋂_j A[i,j]) ⊂ ∅ = ∀i, (⋂_j A[i,j]) ⊂ ∅
73 -- (⋃_i ⋂_j A[i,j]) ⊂ ∅ = ∀i, (⋂_j A[i,j]) ⊂ ∅