@@ -45,28 +45,29 @@ checkFormulas env beh trs defs (ProdCons (fp, ep) (fc, ec)) =
4545 issues@(_ : _) -> for_ issues $ embedFormula beh . anItem
4646 [] -> do
4747 -- We have the following isomorphisms:
48− -- (A ⊂ X ∪ Y) = (A ⊂ X) \/ (A ⊂ Y)
4948 -- (A ⊂ X ∩ Y) = (A ⊂ X) /\ (A ⊂ Y)
5049 -- (A ⊂ ⊤) = 1
5150 -- (X ∪ Y ⊂ B) = (X ⊂ B) /\ (Y ⊂ B)
5251 -- (∅ ⊂ B) = 1
5352 -- The remaining cases are, notably, not isomorphisms:
54− -- 1) (A ⊂ ∅) <= 0
55− -- 2) (X ∩ Y ⊂ B) <= (X ⊂ B) \/ (Y ⊂ B)
56− -- 3) (⊤ ⊂ B) <= 0
57− -- Therefore we have the isomorphisms with (∃ and ∀ being the N-ary
53+ -- 1) (A ⊂ X ∪ Y) <= (A ⊂ X) \/ (A ⊂ Y)
54+ -- 2) (A ⊂ ∅) <= 0
55+ -- 3) (X ∩ Y ⊂ B) <= (X ⊂ B) \/ (Y ⊂ B)
56+ -- 4) (⊤ ⊂ B) <= 0
57+ -- Therefore we have the implications with (∃ and ∀ being the N-ary
5858 -- versions of \/ and /\ respectively):
5959 -- (⋃_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]
6161 -- = ∀i ∃k ∀l, (⋂_j A[i,j]) ⊂ B[k,l]
6262 -- with the caveat that the the set over which k ranges is nonempty.
63− -- This is because 1) is not an isomorphism.
63+ -- (because 2) is not an isomorphism), and that this is a sufficient
64+ -- but not necessary condition (because 1) is not an isomorphism).
6465 -- Our disjunction loses information, so it makes sense to nest it as
6566 -- deeply as possible, hence we choose the latter representation.
6667 --
6768 -- We delegate the verification of (⋂_j A[j]) ⊂ B to a separate heuristic
6869 -- 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)).
7071 --
7172 -- If k ranges over an empty set, we have the isomorphism:
7273 -- (⋃_i ⋂_j A[i,j]) ⊂ ∅ = ∀i, (⋂_j A[i,j]) ⊂ ∅