From 8a2a27eb0611d13bd6355f6fa9fd460fc44927c0 Mon Sep 17 00:00:00 2001 From: Robbert Krebbers Date: Sun, 10 Dec 2017 14:07:32 +0100 Subject: [PATCH] Docs: fix reference to America/Rutten. --- docs/program-logic.tex | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) diff --git a/docs/program-logic.tex b/docs/program-logic.tex index 3541c107..de5055c1 100644 --- a/docs/program-logic.tex +++ b/docs/program-logic.tex @@ -36,10 +36,8 @@ Furthermore, since the $\iFunc_i$ are locally contractive, so is $\textdom{ResF} Now we can write down the recursive domain equation: $\iPreProp \cong \UPred(\textdom{ResF}(\iPreProp, \iPreProp))$ -$\iPreProp$is a COFE defined as the fixed-point of a locally contractive bifunctor. -This fixed-point exists and is unique\footnote{We have not proven uniqueness in Coq.} by America and Rutten's theorem~\cite{America-Rutten:JCSS89,birkedal:metric-space}. -We do not need to consider how the object is constructed. -We only need the isomorphism, given by +Here,$\iPreProp$is a COFE defined as the fixed-point of a locally contractive bifunctor, which exists by \thmref{thm:america_rutten}. +We do not need to consider how the object$\iPreProp\$ is constructed, we only need the isomorphism, given by: \begin{align*} \Res &\eqdef \textdom{ResF}(\iPreProp, \iPreProp) \\ \iProp &\eqdef \UPred(\Res) \\ -- GitLab