diff --git a/proposal.tex b/proposal.tex index e78359e..6380989 100644 --- a/proposal.tex +++ b/proposal.tex @@ -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.