Merge branch 'master' of git.wlog.site:pouya/coalgebraic-simulation

ACV-abstract-2026/Makefile

@@ -0,0 +1,2 @@
+export TEXINPUTS:=${TEXINPUTS}:.:TexCommon
+include ../TexCommons/Makefile

ACV-abstract-2026/TODO.md

@@ -0,0 +1,19 @@
+
+# TODO List
+
+- [ ] Half a page, that is 25% of the total available space of 2 pages, is spent on the example of combinatory logic (CL), but then the example is not connected to the abstract framework it was intended to illustrate. 
+- [ ] Very concretely, the functors Σ and B should be instantiated to CL, and then also the refinement of them presented in the "separability" part. 
+- [ ] This counterexample takes around 15% of the total space, and these 15% could be used instead to connect the abstract framework to the CL example. [Worth mentioning that the other reviewer was happy with the text!]
+- [ ] Category C, what do its objects and morphisms denote?
+> The objects of C are representing sets of terms, morphisms functions. 
+- [ ] What is the signature functor Σ for the case of xCL?
+> Σ is the "non-recursive" presentation of the language of xCL, e.g.
+   ```haskell
+   data Σ X = I | K | S | K' X | S' X | S'' X X | App X X
+   ```
+- [ ] What is the behavior functor B?
+> Here I am lost with my current background knowledge, as I would expect now some relation specifying the operational semantics, but B targets C.
+- [ ] Likewise what are then Σᵥ, Σ_c, D and T?
+- [ ] Guessing that X is for the lhss in accordance with paper [4], I do not understand why B(X,Y) becomes contravariant in X when in [4] it was covariant.
+- [ ] So, if the xCL example shall be of any use in this abstract, B needs to spelled out for xCL.
+

ACV-abstract-2026/big-step-short.cit

@@ -0,0 +1 @@
+d41d8cd98f00b204e9800998ecf8427e  -

ACV-abstract-2026/big-step-short.vtc

@@ -0,0 +1 @@
+\contitem\title{From Abstract Higher-Order GSOS to Abstract Big-Step Semantics, Abstractly (Early Idea)}\author{Sergey Goncharov, Pouya Partow, and Stelios Tsampas}\page{:1--:3}

ACV-abstract-2026/review.txt

@@ -0,0 +1,119 @@
+
+
+CAUTION: This email originated from outside the organisation. Do not click links or open attachments unless you recognise the sender and know the content is safe.
+
+
+Dear Sergey,
+
+On behalf of the Programme Committee of CALCO 2025, we are happy to inform you that your early idea contribution 11
+
+From Abstract Higher-Order GSOS to Abstract Big-Step Semantics, Abstractly (Early ideas)
+
+has been accepted for presentation at CALCO 2025.
+
+The reviews for your submission are attached below. Please take the reviewer comments into account when preparing the final version. More details regarding the final version will follow shortly.
+
+We look forward to seeing you in Glasgow!
+
+Best regards,
+Corina and Alexander.
+
+SUBMISSION: 11
+TITLE: From Abstract Higher-Order GSOS to Abstract Big-Step Semantics, Abstractly (Early ideas)
+
+
+----------------------- REVIEW 1 ---------------------
+SUBMISSION: 11
+TITLE: From Abstract Higher-Order GSOS to Abstract Big-Step Semantics, Abstractly (Early ideas)
+AUTHORS: Sergey Goncharov, Pouya Partow and Stelios Tsampas
+
+----------- Overall evaluation -----------
+SCORE: 2 (accept)
+----- TEXT:
+This "early idea" abstract on abstract big-step semantics through abstract higher-order GSOS (AHOGSOS) is well in scope of CALCO.
+I see no reason to reject it.
+
+That said, I am not an expert on GSOS and I failed to understand the technical content of this abstract.  I made an honest attempt, and my comments below could be seen as a proof-of-work.
+
+The failure to communicate might be due to the lack of space the authors had for the presentation, but I also see some essential shortcoming.  Half a page, that is 25% of the total available space of 2 pages, is spent on the example of combinatory logic (CL), but then the example is not connected to the abstract framework it was intended to illustrate.
+
+Very concretely, the functors Σ and B should be instantiated to CL, and then also the refinement of them presented in the "separability" part.
+
+The question is whether then there is enough space remaining for all of the content of the abstract.  If I had to make the choice, I would put the counterexample (l55ff) into a technical report and link to it from the abstract.  This counterexample takes around 15% of the total space, and these 15% could be used instead to connect the abstract framework to the CL example.
+
+Details
+=======
+
+Small-step and big-step semantic for CL are well-presented, but then AHOGSOS is introduced, CL is not connected to its formalism.  The question is, why do you prepare the reader by a concrete example just to drop it once you go to the abstract mathematics?
+
+From the level of difficulty, I think when you sit down an implement big-step operational semantics for CL, you quickly converge to the presentation you call xCL where you form "closures" for underapplied uses of K and S.  In contrast, an abstract framework for SOS is not something that suggests itself.
+
+Concretely, I am missing answers for the following questions:
+1. Category C, what do its objects and morphisms denote?
+2. What is the signature functor Σ for the case of xCL?
+3. What is the behavior functor B?
+4. Likewise what are then Σᵥ, Σ_c, D and T?
+
+My guesses:
+1. The objects of C are representing sets of terms, morphisms functions.
+2. Σ is the "non-recursive" presentation of the language of xCL, e.g.
+   ```haskell
+   data Σ X = I | K | S | K' X | S' X | S'' X X | App X X
+   ```
+3. Here I am lost with my current background knowledge, as I would expect now some relation specifying the operational semantics, but B targets C.
+
+Reading Turi and Plotkin [4], I might get some more clues.
+There, B is the "successor" functor for the operational semantics, producing for a set X of terms the collection B X of terms reachable by a single operational step.  This collection B is organized by the labels a ∈ A on the rules of the operational semantics.
+The "abstract GSOS" simply speaks of ρX : Σ(X × BX) → B(TX) which comes close to the presentation here assuming that the set TX of terms over X is Σ^⋆X.
+Somehow fact that the labels in xCL are also terms materializes in a B : Cᵒᵖ × C → C, but it is not clear to me which of the positions of B are for the labels and which for the lhss.
+Guessing that X is for the lhss in accordance with paper [4], I do not understand why B(X,Y) becomes contravariant in X when in [4] it was covariant.
+
+So, if the xCL example shall be of any use in this abstract, B needs to spelled out for xCL.
+
+
+
+----------------------- REVIEW 2 ---------------------
+SUBMISSION: 11
+TITLE: From Abstract Higher-Order GSOS to Abstract Big-Step Semantics, Abstractly (Early ideas)
+AUTHORS: Sergey Goncharov, Pouya Partow and Stelios Tsampas
+
+----------- Overall evaluation -----------
+SCORE: 1 (weak accept)
+----- TEXT:
+A categorical approach to relate big-step and small-step operational semantics in terms of higher-order GSOS is outlined.
+
+Though well-motivated in principle in a presentation it would seem advantageous to first see the workings of moving between the two operational semantics types on the rule level before diving into the categorical details.  In particular, it seems that some of the issues that still have to be solved - the strong separation condition - are best explained with conditions on rules.
+
+
+
+----------------------- REVIEW 3 ---------------------
+SUBMISSION: 11
+TITLE: From Abstract Higher-Order GSOS to Abstract Big-Step Semantics, Abstractly (Early ideas)
+AUTHORS: Sergey Goncharov, Pouya Partow and Stelios Tsampas
+
+----------- Overall evaluation -----------
+SCORE: 2 (accept)
+----- TEXT:
+The paper outlines an approach for relating small-step and big-step
+operational semantics in an abstract categorical setting. The authors
+build on the existing theory of abstract higher-order GSOS where the
+small-step semantics can be specified categorically. This is extended
+to a separated higher-order GSOS, separating the the syntax into value
+constructors and computation constructors. In this setting one can
+define a multistep semantics as least fixpoint and abstract the
+big-step semantics as a natural transformation from computation
+constructors applied to values to a monad of results.
+
+The authors observe that separability alone is not enough to prove the
+fundamental equivalence between small-step and big-step semantics and
+identify a stronger condition, which abstracts the idea of suitably
+constraining the shape of rule conclusions based on the premises, as a
+potential way to remedy this issue.
+
+The theme is surely of interest for CALCO. The authors did a good job
+in sythesizing in a limit space the main ideas of their work. For a
+non-expert (like me) the technical details are difficult to grasp from
+the short summary, but I do not see this as a problem. Rather, I think
+this can be a quite interesting and valuable addition to CALCO's program.
+
+

ACV-abstract-2026/sym-sim.cit

@@ -0,0 +1 @@
+d41d8cd98f00b204e9800998ecf8427e  -

ACV-abstract-2026/sym-sim.tex

@@ -0,0 +1,179 @@
+\RequirePackage[l2tabu, orthodox]{nag}
+\PassOptionsToPackage{final}{graphicx}
+\PassOptionsToPackage{nosumlimits,nonamelimits}{amsmath}
+\PassOptionsToPackage{colorlinks,linkcolor={blue},citecolor={blue},urlcolor={red},breaklinks=true,final}{hyperref}
+
+\documentclass[a4paper,UKenglish,cleveref, autoref, thm-restate, numberwithinsect,final]{lipics-v2021}
+\bibliographystyle{plainurl} % the mandatory bibstyle
+
+\sloppy
+
+\usepackage{proof}
+\usepackage{xspace}
+\usepackage{mdframed, ebproof}
+\usepackage{microtype}
+\usepackage{stackengine}
+
+
+\input{catprog}
+\renewcommand{\by}[1]{\text{/$\mspace{-2mu}$/~#1}}
+
+\renewcommand{\paragraph}[1]{\medskip\noindent{\bfseries\sffamily #1.}}
+
+\usepackage{ifdraft}
+\ifdraft{
+%  \usepackage{showframe}
+  \usepackage{showlabels}
+  \renewcommand{\showlabelfont}{\ttfamily\scriptsize}
+  \usepackage[layout=footnote,draft]{fixme}
+
+%  \usepackage[notcite,notref]{showkeys}
+%  \renewcommand*\showkeyslabelformat[1]{%
+%  \raisebox{1ex}{\raggedleft{\textit{\tiny #1}}}
+}{
+ \usepackage[layout=footnote,final]{fixme}
+}
+
+\FXRegisterAuthor{sg}{asg}{SG}  % Sergey
+\FXRegisterAuthor{fg}{afg}{FG}  % Florian
+
+\newcommand{\xCL}{\textbf{xCL}\xspace}  
+
+\usepackage{todos}
+
+\renewcommand{\xto}[1]{\mathrel{\raisebox{-.15pt}{$\xrightarrow{\;\smash{\raisebox{-.5pt}{\makebox(3,0)[b]{\scriptsize $#1$}}\;}}$}}}
+
+\newcommand{\val}{\mathsf{v}}
+\newcommand{\com}{\mathsf{c}}
+
+\newcommand{\dl}{\chi}
+
+\newcommand{\Fst}{\Pi_1} %{\oname{Fst}} 
+\newcommand{\Snd}{\Pi_2} %{\oname{Snd}} 
+
+\newcommand{\Sigmas}{\Sigma^\star}
+
+\newcommand{\mS}{\mu\Sigma}
+\newcommand{\mSv}{\mS_\val}
+\newcommand{\mSc}{\mS_\com}
+
+\renewcommand{\comp}{\cdot}
+\newcommand{\klstar}{\sharp}  			%% Kleisli star
+
+\title{Soundness and Completeness of Symmetric Relators} %TODO Please add
+%Or: It is expected from a symmetric simulation to be a bisimulation
+\titlerunning{From Abstract Higher-Order GSOS to Abstract Big-Step Semantics, Abstractly}
+
+\author{Sergey Goncharov}{University of Birmingham, UK}{s.goncharov@bham.ac.uk}{https://orcid.org/0000-0001-6924-8766}{}
+\author{Pouya Partow}{University of Birmingham, UK}{p.partow@bham.ac.uk}{https://orcid.org/0009-0003-9652-9469}{}
+
+
+\authorrunning{J. Open Access and J.\,R. Public} %TODO mandatory. First: Use abbreviated first/middle names. Second (only in severe cases): Use first author plus 'et al.'
+
+\Copyright{Jane Open Access and Joan R. Public} %TODO mandatory, please use full first names. LIPIcs license is "CC-BY";  http://creativecommons.org/licenses/by/3.0/
+
+%\ccsdesc[100]{\textcolor{red}{Replace ccsdesc macro with valid one}} %TODO mandatory: Please choose ACM 2012 classifications from https://dl.acm.org/ccs/ccs_flat.cfm 
+
+\keywords{Operational semantics, Higher-order GSOS, Extended combinatory logic}
+
+\category{} %optional, e.g. invited paper
+
+\relatedversion{} %optional, e.g. full version hosted on arXiv, HAL, or other respository/website
+%\relatedversiondetails[linktext={opt. text shown instead of the URL}, cite=DBLP:books/mk/GrayR93]{Classification (e.g. Full Version, Extended Version, Previous Version}{URL to related version} %linktext and cite are optional
+
+%\supplement{}%optional, e.g. related research data, source code, ... hosted on a repository like zenodo, figshare, GitHub, ...
+%\supplementdetails[linktext={opt. text shown instead of the URL}, cite=DBLP:books/mk/GrayR93, subcategory={Description, Subcategory}, swhid={Software Heritage Identifier}]{General Classification (e.g. Software, Dataset, Model, ...)}{URL to related version} %linktext, cite, and subcategory are optional
+
+%\funding{(Optional) general funding statement \dots}%optional, to capture a funding statement, which applies to all authors. Please enter author specific funding statements as fifth argument of the \author macro.
+
+%\acknowledgements{I want to thank \dots}%optional
+
+\nolinenumbers %uncomment to disable line numbering
+
+
+
+%Editor-only macros:: begin (do not touch as author)%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%\EventEditors{John Q. Open and Joan R. Access}
+%\EventNoEds{2}
+%\EventLongTitle{42nd Conference on Very Important Topics (CVIT 2016)}
+%\EventShortTitle{CVIT 2016}
+%\EventAcronym{CVIT}
+%\EventYear{2016}
+%\EventDate{December 24--27, 2016}
+%\EventLocation{Little Whinging, United Kingdom}
+%\EventLogo{}
+%\SeriesVolume{42}
+%\ArticleNo{23}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\hideLIPIcs
+
+\def\subjclassHeading{}
+\makeatletter
+\def\@ccsdescString{\erule\vspace{-5ex}}
+\makeatother
+
+
+\begin{document}
+\allowdisplaybreaks
+\let\cedilla\c
+\renewcommand{\c}{\colon}
+
+\maketitle
+
+%TODO mandatory: add short abstract of the document
+\begin{abstract}
+ 
+%One remarkable aspect of our approach is its potential for implementation in functional programming languages and proof assistants, 
+%to atomate SOS specification transformations and reasoning about them.
+\end{abstract}
+
+
+
+%
+
+%
+%\section{Mathematical Preliminaries}%\label{sec:}
+
+
+\paragraph{Compositionality}
+Given a labeled transition systems $(S,L,\to)$, where $S$ is a set of states, $L$ is a set of labels, and $\to\subseteq S\times L\times S$ is a set of labeled transitions, a \emph{simulation} is a relation $r\subseteq S\times S$ such that the following sentence holds:
+\begin{gather*}
+	(x,y)\in r, x\xto{l} x' \Rightarrow \exists y', y\xto{l} y' \;\text{ and } (x',y')\in r
+\end{gather*}  
+The greatest simulation relation over $S$ is called \emph{similarity} and shown with $\leq$. A simulation relation $r$ on $S$ is a \emph{bisimulation} iff the following sentence holds: 
+\begin{gather*}
+	(x,y)\in r, y\xto{l} y' \Rightarrow \exists x', x\xto{l} x' \;\text{ and } (x',y')\in r
+\end{gather*} 
+The greatest bisimulation relation over $S$ is called \emph{bisimilarity} and shown with $\sim$. This is the traditional definition of bisimilarity. There are many different notions. For this definition, we can say that the symmetric similarity is the bisimilarity. But it is not always true for different notions.
+
+\paragraph{Coalgebraic Bisimulation}
+For an endofunctor $F$ over a category $\BC$, a coalgebra, is a pair $(X,\alpha)$, where $X$ is an object of $\BC$ and $\alpha\c X\to FX$ is a morphism in $\BC$. Coalgebras serve as an abstraction of variant transition systems. For example, a labeled transition system $(S,L,\to)$ is a coalgebra $(S,\gamma)$, where $\gamma\c S\to\mathcal{P}(L\times S)$ and $\mathcal{P}$ is the powerset functor.
+
+$S$ can be the set of the terms of a programming language given by a signature $\Sigma$, and $\to$ can be the set of labeled inductions of the language, given by an operational semantics. Following that, a context $C$ is defined as:
+\begin{gather*}
+	C\Coloneqq\Box\mid f(C,\bar{t})\mid f(\bar{t},C)\mid f(\bar{u},C,\bar{s})
+\end{gather*}
+$f\in\Sigma$ and by $\bar{t}$, $\bar{s}$ and $\bar{u}$ we mean vectors of terms in $S$. $\Box$ is a placeholder. Assuming $t\in S$, then $C[t]\in S$. We call a relation $r$ congruence iff for terms $t$ and $s$, and a context $C$, $t\mathrel{r}s$ gives $C[t]\mathrel{r}C[s]$. A language with its operational semantics is compositional iff the bisimilarity relation over the terms of the language is a congruence.
+
+\paragraph{Howe's method}
+Howe's method has been traditionally used for compositionality results. \emph{Howe closure} of a relation $r$ is shown by $\hat{r}$ and is defined with the following inference rule: 
+\begin{gather*}
+	\infer{f(\bar{t})\mathrel{\hat{r}} s}{\bar{t}\mathrel{\hat{r}} \bar{s} & f(\bar{s})\mathrel{r} s}
+\end{gather*}
+Assuming that $r$ is reflexive, then $r\subseteq\hat{r}$, and $\hat{r}$ is a congruence. Additionally, if $r$ is reflexive and symmetric, then $\hat{r}^\star$, the transitive closure of $\hat{r}$ is symmetric (the transitive closure trick). So, to prove that bisimilarity is a congruence it is sufficient to prove that $\hat{\sim}$ is a bisimulation. Given the non-symmetric nature of the closure, it is more common to prove that $\hat{\sim}$ is a simulation. It is usually expected from a symmetric simulation to be a bisimulation. But it has not always been the case.
+
+\paragraph{Relators}
+
+
+
+\newpage
+\bibliography{references}
+
+
+\end{document}
+
+%%% Local Variables:
+%%% mode: LaTeX
+%%% TeX-master: t
+%%% End:

ACV-abstract-2026/sym-sim.vtc

@@ -0,0 +1 @@
+\contitem\title{Soundness and Completeness of Symmetric Relators}\author{Sergey Goncharov and Pouya Partow}\page{:1--:2}

draft/draft.tex

@@ -1144,17 +1144,15 @@ Another avenue would be to give another definition for simulation that does not
 
 Well! This counter example does not work! Because the described order $\appr$ does not satisfy the condition mentioned in Jacobs's paper. The condition is that the order on $FX$ should satisfy the property that for a morphism $f\c X\to Y$ the morphism $Ff\c FX\to FY$ preserves $\appr$. Probably, the only poset that has this property for $\mathbf{Id}$ is $\Delta$. If there is a counter-example, it is true for another functor.
 
-\begin{example}
-	Another counter-example! Assume that $F=\powf $, and take $R=\{(1,2),(2,1),(1,3),(3,1)\}$, and $X=\{1,2,3\}$. $\alpha(x)=X$ for every $x\in X$, and $\sigma$ is defined as below:
+(But still!)We have a counter-example for a symmetric relation $R$ that has a witness to be a simulation, but that morphism does not serve as a witness for $R$ to be a bisimulation. In the category of sets we assume that $F=\mathcal{P}$, and take $R=\{(1,2),(2,1),(1,3),(3,1)\}$, and $X=\{1,2,3\}$. $\alpha(x)=X$ for every $x\in X$, and $\sigma$ is defined as below:
 \begin{gather*}
 	\sigma(w)=
 	\begin{cases} 
-			R & w\neq (1,3)  \\
-			R\setminus\{(1,2)\} & w=(1,3)
+		(X,X) & w\neq (1,3)  \\
+		(X,X\setminus\{2\}) & w=(1,3)
 	\end{cases}
 \end{gather*}
-	In this scenario, $\sigma$ is a simulation, but it is not a bisimulation. It is a simulation since for every $w\in R$ we have $(\powf p_1(\sigma(w)))=X$, thus for every $x\in X$, $\alpha(x)=X\subseteq X$. Also, $\powf p_2(\sigma(w))\subseteq \alpha(p_2(w))$ as $\alpha(p_2(w))=X$ for every $w\in R$. But it is not a bisimulation, since $\alpha\comp p_2(1,3)=\alpha(3)=X\neq(\powf p_2)^\dagger(\sigma(1,3))=\{1,3\}$.
-\end{example}
+In this scenario, $\sigma$ is a witness for $R$ to be a simulation, but it is not a witness for $R$ to be a bisimulation. $\sigma$ is a witness for $R$ to be a simulation since for every $w\in R$ we have $\alpha(p_1(w))\subseteq((\mathcal{P}p_1)^\ddagger(\sigma(w)))=X$. Also, for every $w\in R$, $((\mathcal{P}p_2)^\ddagger(\sigma(w)))\subseteq\alpha(p_2(w))=X$. But it is not a bisimulation, since $\alpha(p_2(1,3))=\alpha(3)=X\neq(\mathcal{P}p_2)^\ddagger(\sigma(1,3))=X\setminus\{2\}$.
 %
 \begin{example}
 	And another counter-example!!! Assume that $F=\powf $, and take $R=X\times X\setminus\{(1,3),(3,1)\}$, and $X=\{1,2,3\}$. $\alpha$ is defined as below:
@@ -1787,7 +1785,7 @@ We define $\join$ and $\meet$ on morphisms as follows:
 \begin{lemma}
 	For every $S\in \powf R$,
 	\begin{gather*}
-		((\powf p_1)^\dagger(S),(\powf p_2)^\dagger(S))\in(\powf R)^\dagger\Leftrightarrow(\powf p_1)(S)\subseteq(\powf p_1)(R),(\powf p_2)(S)\subseteq(\powf p_2)(R)
+		((\powf p_1)(S),(\powf p_2)(S))\in(\powf R)^\dagger\Leftrightarrow(\powf p_1)(S)\subseteq(\powf p_1)(R),(\powf p_2)(S)\subseteq(\powf p_2)(R)
 	\end{gather*}
 \end{lemma}
 \begin{lemma}\label{lem:alph-prod}
@@ -2228,18 +2226,20 @@ Barr relator is a generalization of the Egli-Milner relator, where the functor i
 		&\iff s\;F\pi_2\comp\sappr\comp(F\pi_1)^\op\;t \qquad\&\qquad s\;(F\pi_1\comp\sappr\comp(F\pi_2)^\op)^\op\;t\\
 		&\iff s\;F\pi_2\comp\sappr\comp(F\pi_1)^\op\;t \qquad\&\qquad s\;F\pi_2\comp\appr\comp(F\pi_1)^\op\;t
 	\end{align*}
-	Since $F\pi_1$ is a function, then $(F\pi_1)^\op$ is an injective map, so there exist exactly one $w\in FA$ such that $(F\pi_1)^\op(s)=w$, and:
+	Since $F\pi_1$ is a surjective function, then exists at least one $w\in FA$ such that $(F\pi_1)^\op(s)=w$, and:
 	\begin{gather*}
 		w\;F\pi_2\comp\sappr\; t \qquad\&\qquad w\;F\pi_2\comp\appr\; t
 	\end{gather*}
-	And similarly, since $F\pi_2$ is also a function we have exactly one $v\in FA$ such that $(F\pi_2^\op)(t)=v$, and:
+	And similarly, since $F\pi_2$ is also a surjective function we have at least one $v\in FA$ such that $(F\pi_2^\op)(t)=v$, and:
 	\begin{align*}
 		&w\;\sappr\; v \qquad\&\qquad w\;\appr\; v\\
 		\iff&(F\pi_1)^\op(s)\;\sappr\; (F\pi_2^\op)(t) \qquad\&\qquad (F\pi_1)^\op(s)\;\appr\; (F\pi_2^\op)(t)\\
 		\iff&(F\pi_1)^\op(s)\;=\; (F\pi_2^\op)(t)\\
 		\iff&s\; F\pi_2\comp(F\pi_1)^\op\;t\\
 		\iff&s\;\bar{F}r\;t
-	\end{align*}\qed
+	\end{align*}
+	So we have $\hat{\overrightarrow{F}}\leq \bar{F}$.
+	Now, we are left to show that $\bar{F}\leq\hat{\overrightarrow{F}}$. For that, reading the given proof from the end to the starting point is sufficient.
 \end{proof}
 	
 \begin{prop}