other cases of an conformance distance $\delta$ that is a limit of converging distances are analogous, but we do not go here into detail.

Let us look at the last claims of the theorem. Suppose that ${\mathfrak{L}}(A) \subseteq {\mathfrak{L}}(B)$. Then for each timed trace of ${\mathfrak{L}}(A)$ there is an identical timed trace of ${\mathfrak{L}}(B)$. The projection to the discretized timed trace will also be identical, thus, $${\mathfrak{L}}(A) \subseteq {\mathfrak{L}}(B) \; \Rightarrow \; {\mathfrak{L}}({{A}_d}) \subseteq {\mathfrak{L}}({{B}_d}).$$ If ${\mathfrak{L}}(A) \nsubseteq \overline{{\mathfrak{L}}(B)}$ then $\delta > 0$. By , we have that $\delta_d > 0$. It follows that $${\mathfrak{L}}(A) \nsubseteq \overline{{\mathfrak{L}}(B)} \; \Rightarrow \; {\mathfrak{L}}({{A}_d}) \nsubseteq {\mathfrak{L}}({{B}_d}).$$

By $\eqref{qe:lang_dist}$, a similar result to Theorem \[th:inclusion\_gap\] holds with respect to distances between languages.

By Theorem \[th:inclusion\_gap\], in order to compute the conformance distance $c({\mathfrak{L}}(A), {\mathfrak{L}}(B))$, we can compute $c({\mathfrak{L}}({{A}_d}), {\mathfrak{L}}({{B}_d}))$, and know that we lie within an error of at most $\frac{1}{2}$ time unit. We may assume that ${{A}_d}$ is deterministic, as this is feasible. It is not necessary to determinize ${{B}_d}$.

The general goal in computing $c({\mathfrak{L}}({{A}_d}), {\mathfrak{L}}({{B}_d}))$ is to find the timed trace of ${\mathfrak{L}}({{A}_d})$ that is farthest from ${\mathfrak{L}}({{B}_d})$ (or a sequence of such timed traces if the distance is $\infty$). A 