Remove Defined marker

[ttuegel]

After #2249, we can modify the SideCondition to keep a set of all defined terms. Instead of looking for the Defined marker, we can look in the SideCondition.

---

• Add a HashSet of defined TermLikes to SideCondition. (appetite: S)
• Implement a function assumeDefined :: TermLike variable -> SideCondition variable which assumes the definedness of all sub-terms that are implied by the original term. In other words, if t is the original term, we assume a sub-term s is defined if \ceil(t) \implies \ceil(s). Take care with Map and Set to minimize storage! If the size of a Map or set is n, we only want n^2 entries and not n!. (appetite: M)
• Implement a function isDefined :: SideCondition variable -> TermLike variable -> Bool. Again, take care with Map and Set. (appetite: M)
• Remove Defined. Replace makeDefined with assumeDefined. Use isDefined instead of checking pattern attributes. (appetite: M)

[ttuegel]

The \ceil of a map or set reduces like this:

\defined: \ceil(X |-> U  Y |-> V  Z |-> W  M)
/* pair-wise \ceil of elements */ ∧ \ceil(X |-> U  M) ∧ \ceil(Y |-> V  M) ∧ \ceil(Z |-> W  M)

where the pair-wise parts are:

\ceil(X |-> U  Y |-> V) ∧ \ceil(X |-> U  Z |-> W) ∧ \ceil(Y |-> V  Z |-> W)