Minor changes

master
David Holland 2021-08-16 22:00:30 +02:00
parent c492507dfc
commit a33367ccfb
1 changed files with 1 additions and 0 deletions

View File

@ -328,6 +328,7 @@ This is validated by looking at the epsilon substitution method, where it is man
The easiest thing, in terms of complexity of the challenges, etc., to implement from scratch in a normal software development setting, would probably be the \texttt{one} keyword, as that is the notion of the \emph{definite description}.
In this case I neither have to deal with the epsilon calculus, nor the non-deterministic nature.
% It's easiest to understand for the software developer. But implementation is magnitudes.
\emph{However} in terms of constructing proofs (read implementing it for KeY) I would rate the complexity \emph{much} higher compared to \texttt{\tbs{}some}!
Proving that any value out of a defined set is fulfilling a condition is in my understanding way easier than proving that either \texttt{\tbs{}all} or even exactly \texttt{\tbs{}one} does so.