text:
\section{Introduction}
Reachability Logic (RL)~\cite{DBLP:journals/lmcs/StefanescuCMMSR19} has been introduced as a language-parametric program logic: a formalism for specifying the functional  correctness of programs, which may belong to any programming language whose
operational semantics is also specified in RL.  The functional correctness of a program is
stated as the validity of a set of RL formulas (specifying the program's expected properties) with respect to another set of RL formulas (specifying the operational semantics of the language containing the program).

Such  statements are proved by means of a proof system, which has  adequate meta-properties with respect to validity: soundness (i.e., only valid RL formulas can be proved) and relative completeness (all valid RL formulas can, in principle, be proved, modulo the existence of ``oracles'' for auxiliary tasks).  The proof of  meta-properties for the RL proof system is highly nontrivial, but it only needs to be done once.

Program logics already have a half-century history between them,  from the first occurrence of Hoare logic~\cite{DBLP:journals/cacm/Hoare69} to  contemporary separation logics~\cite{DBLP:journals/cacm/OHearn19}. However, all those logics  depend on a
language's syntax and therefore have to be defined over and over again, for each new language (or even, for each new language version).
In particular, the  meta-properties of the corresponding proof systems should  be reproved over and over again, a
 tedious task that is often  postponed to an indeterminate future.

Despite being language-parametric, Reachability Logic does not come in only one version.
Several  versions of the logic have been proposed over the years~\cite{DBLP:conf/lics/RosuSCM13,DBLP:conf/oopsla/StefanescuPYLR16,DBLP:journals/lmcs/StefanescuCMMSR19}. The formalism has been generalised from programming languages to more abstract models: rewriting logic~\cite{DBLP:conf/birthday/LucanuRAN15,DBLP:conf/lopstr/SkeirikSM17} and transition systems~\cite{DBLP:conf/tase/RusuGH18}, which can be used for specifying designs, and verifying them before they are implemented in program code. This does not replace code verification, just as code verification does not replace the testing of the final running software;  but it enables the early catching of errors and the early discovery of key functional-correctness properties, all of which are known to have practical, cost-effective benefits.

\paragraph*{Contributions.} We further study RL on transition systems (TS). We propose  three proof systems for
RL, and formalise them in the Coq~\cite{DBLP:series/txtcs/BertotC04} and Isabelle/HOL~\cite{DBLP:books/sp/NipkowPW02} proof assistants. One may
naturally ask: why having several proof systems and  proof assistants - why not one of each?
The answer is manyfold:
\begin{itemize}

\item the proof systems we propose have  some common features: the soundness and completenes meta-properties, and the
  coinductiveness nature inherited from RL. However, they do differ in others aspects:  (i) the ``amount''  of induction they contain; (ii)  their degree of compositionality (i.e., their ability to prove local formulas  on ``components'' of a TS, and then to use those formulas as lemmas in proofs of global formulas on the TS); and (iii) the difficulty level of their soundness proofs.

\item  we show that the more induction  a proof system uses, and the closest its coinduction style to our problem domain of proving reachability-logic formulas,
  the more  compositional the proof system is, but the more difficult its soundness proof. There is a  winner: the most compositional proof system of the three, but we found that the other ones exhibit  interesting, worth-presenting features as well.

\item Coq and Isabelle/HOL have different styles of coinduction: Knaster-Tarski style vs.\ Curry-Howard style. Experiencing this first-hand with the nontrivial examples constituted by proof systems suggested a spinoff project, which amounts to porting some of the features of one proof assistant into the other one. For the moment, porting  Knaster-Tarski features into the Curry-Howard coinduction of Coq produced promising results, with possible practical impact for a broader class of Coq users.
\end{itemize}

\paragraph{Related Work.}  Regarding RL, most papers in the  above-given list of  references mention its coinductive nature,
but do not actually use it. Several Coq mechanisations of soundness proofs for RL proof systems are presented,  but Coq's coinduction is absent from them.  In~\cite{DBLP:conf/cade/CiobacaL18,DBLP:journals/jsc/LucanuRA17} coinduction is used for formalising RL and  for proving RL properties
for programs and for term-rewriting systems,
but their approach is not mechanised in a proof assistant.
More closely related work to ours is reported in~\cite{DBLP:conf/esop/MoorePR18}; they attack, however, the problem
exactly in the opposite way: they develop a general theory of coinduction in Coq and use it to verify programs directly based on the semantics of  programming languages, i.e., without using a proof system. They do show that  a proof system for RL is an instance of their approach for theoretical reasons, in order to give a formal meaning to the  completeness of their approach.

Regarding coinduction in Isabelle/HOL, which is based on the Knaster-Tarski fixpoint theorems, we used only a small portion of what is available: coinductive predicates, primitive coinductive datatypes and primitive corecursive functions. More advanced developments are reported in~\cite{DBLP:conf/esop/BlanchetteBL0T17}. Regarding coinduction in Coq, it is based on the Curry-Howard isomorphism that views proofs as programs, hence, coinductive proofs are well-formed corecursive programs~\cite{DBLP:conf/types/Gimenez94}. An approach that bridges the gap between this  and
the Knaster-Tarski style of coinduction is~\cite{DBLP:conf/popl/HurNDV13}.
A presentation of our own  results on porting Knaster-Tarski style coinduction to Coq and a detailed comparison with the above is left for future work.

Regarding coinduction in formal methods, we note that it is mostly used for proving bisimulations. The book~\cite{sangiorgi2011} serves as introduction to both these notions and explores the relationships between them.

Regarding compositional verification, most existing techniques decompose proofs among  parallel composition
operators. Various compositional methods for various parallel composition operators (rely-guarantee for variable-based composition, assumption-commitment for synchronisation-based composition, \ldots) are presented in the book~\cite{DBLP:books/cu/RoeverBH2001}.
We employ compositionality in a different sense - structural, for transition systems, and logical, for formulas.
We note, however, that many of the techniques presented in~\cite{DBLP:books/cu/RoeverBH2001} have a coinductive
nature, which could perhaps be
 exploited in future versions of RL proof systems.

\paragraph*{Organisation.} The next section recaps preliminary notions: Knaster-Tarski style induction and coinduction, transition systems, and RL on transition systems. A first compositionality result, of RL-validity with respect to certain sub-transition systems, is given. The  three following sections present our three proof systems in increasing order of complexity. Soundness and completeness results are given  and a notion of compositionality  with respect to formulas,  in two versions: asymmetrical and symmetrical, is introduced and combined with the compositionality regarding sub-transition systems. The three proof systems are shown to have increasingly demanding compositionality features. We then briefly discuss the mechanisations of the proof systems in the Coq and Isabelle/HOL proof assistants before we  present future work and conclude.
The Coq and Isabelle/HOL formalisations, as well as a full paper containing proofs of all the results, are available at \url{http://project.inria.fr/from2019}.

\section{Preliminaries}
\label{sec:prelim}
\subsection{Induction and Coinduction}

Consider a complete lattice $(L, \sqsubseteq, \sqcup, \sqcap, \bot, \top)$
and a monotone function $F : L \to L$. According to the Knaster-Tarski fixpoint theorem, $F$ has a least fixpoint $\mu F$ (respectively, greatest fixpoint $\nu F$), which is the least (respectively, greatest) element of $L$ such that $F(x) \sqsubseteq x$ (resp.\ $x \sqsubseteq F(x)$). From this one deduces Tarski's induction and coinduction principles:
$\mbox{$F(x) \sqsubseteq x$ implies $\mu F \sqsubseteq x$}$
and $\mbox{$x \sqsubseteq F(x)$ implies $x \sqsubseteq \nu F$}$.

Those principles can be used
to define inductive and coinductive datatypes and recursive and corecursive functions. For example, the type of natural numbers
is defined as the least fixpoint of the function $F(X) = \{ 0 \} \cup \{ \mathit{Suc}(x) \mid x \in X \}$.
The greatest fixpoint of $F$ is the type of natural numbers with infinity.

As another example, let $\mathcal{S} = (S, \to)$ be a transition system where $S$ is the set of states and $\to \; \subseteq \; S \times S$ is the transition relation.
A state $s$ is \emph{final}, and we write $\bullet\,  s$, if there exists no $s'$ such that $s \to s'$.
A path is a nonempty, possibly infinite sequence of states. More formally, the set $\mbox{$\mathit{Paths}$}$ of paths   is the greatest fixpoint $\nu F$, where
$F(X) \;\; = \;\; \{ s \; \mid \; \bullet\, s  \} \; \cup \; \{ s \, \tau \; \mid \; s \in S \; \wedge \; \tau \in X \; \wedge  \; s \to (\mbox{$\mathit{hd}$}\, \tau) \}$,  with
$\mbox{$\mathit{hd}$}:\mbox{$\mathit{Paths}$} \to S$ being simultaneously defined as $\mbox{$\mathit{hd}$}(s) = s$ and $\mbox{$\mathit{hd}$}(s\, \tau) = s$ for all $s \in S$ and $\tau \in X$.
One can then corecursively define the length of a path as a value in  the  natural numbers with infinity:
$\mbox{$\mathit{len}$}\,  s = 0$ and $\mbox{$\mathit{len}$}(s\, \tau) = \mathit{Suc}(\mbox{$\mathit{len}$}\, \tau)$.

Hereafter, whenever necessary, we emphasise the fact that certain  notions are relative to a  transition system  $\mathcal{S}$ by postfixing them with $_\mathcal{S}$. We omit this subscript when it can be inferred from the context.

A complete lattice associated to a transition system $\mathcal{S} = (S, \to)$,  is the set of state predicates $\Pi$
defined as the set of functions from $S$ to the set of Booleans $\mathbb{B} = \{ \mbox{\textsc{f}}, \mbox{\textsc{t}} \}$. Its operations are defined by
$p \sqsubseteq q \; \mbox{$\triangleq$} \; \forall s, p\, s \Rightarrow q\, s$,
$(p \sqcup q)\, s\; \mbox{$\triangleq$} \;\; p\, s \vee q\, s$,  $(p \sqcap q)\, s \; \mbox{$\triangleq$} \; p\, s \wedge q\, s$,
$\bot\, s \; \mbox{$\triangleq$} \; \mbox{\textsc{f}}$, $\top\, s \; \mbox{$\triangleq$} \; \mbox{\textsc{t}}$.
We  also extend the transition relation $\to$ of  $\mathcal{S}$ into a \emph{symbolic transition function} $\mbox{$\mathit{\partial}$} :  \Pi \to \Pi$, defined by
$\mbox{$\mathit{\partial}$} p \; \mbox{$\triangleq$} \; \lambda s \;.\; \exists s' \;.\; p\, s' \, \wedge \, s' \to s$.

It is sometimes  convenient to use a stronger variant of Tarski's coinduction principle:
$X \sqsubseteq F(X \sqcup \nu F)$ iff $X \sqsubseteq  \nu F$.
Regarding induction, it is sometimes  convenient to use \emph{continuous} functions, i.e., functions $F$ such that
$F(\bigsqcup_{i \in I} x_i) = \bigsqcup_{i \in I}(F x_i)$, and use Kleene's fixpoint theorem:  $\mu F$ exists and is equal to $\bigsqcup_{n = 0}^{\infty} F^n(\bot)$.

\subsection{Reachability Formulas}
We adapt Reachability Logic  to  transition systems. Assume a transition system $\mathcal{S} = (S,\to)$.
Syntactically,
a reachability formula (or, simply, a formula) over $\mathcal{S}$ is a pair $p \mbox{$\mathit{\,\Rightarrow\!\!\!\Diamond}\,$} q$ with  $p,q \in \Pi$. We let $\mathit{lhs}(p \mbox{$\mathit{\,\Rightarrow\!\!\!\Diamond}\,$} q) \;\mbox{$\triangleq$}\; p$ and  $\mathit{rhs}(p \mbox{$\mathit{\,\Rightarrow\!\!\!\Diamond}\,$} q) \;\mbox{$\triangleq$}\; q$.
We denote by $\Phi_\mathcal{S}$ the set of all reachability formulas over the transition system $\mathcal{S}$.

\begin{example}
  Figure~\ref{fig:sum} depicts  an extended finite-state machine having three natural-number variables: $i$,$s$, and $m$, and three control nodes: $c_0$, $c_1$, and $c_2$.
  Arrows connect the nodes and are possibly decorated with a Boolean guard and a set of parallel assignments of the variables. The variable $m$ is never assigned, thus, it stays constant. The  purpose of the machine is to compute in $s$ the sum of the first $m$ natural numbers.

  The machine is a finite representation of an infinite-state transition system whose
  state-set is the Cartesian product $ \{c_0, c_1, c_2\} \times \mathbb{N}^3$

  and whose  transition relation is
  $\bigcup_{i,s,m \in \mathbb{N}}\{((c_0,i,s,m),(c_0,0,0,m))\}$ $\cup \bigcup_{i, s,m \in \mathbb{N}, i <m}\{((c_1,i,s,m),(c_1,i+1,s+i+1,m))\} \cup \bigcup_{i, s,m \in \mathbb{N}, i \geq m}\{((c_1,i,s,m),(c_2,i,s,m))\}$.
   A  formula expressing the transition systems's functional correctness is
$(c = c_0)\mbox{$\mathit{\,\Rightarrow\!\!\!\Diamond}\,$} (c =c_2 \wedge s =  m\times (m+1)/2)$.

\begin{figure}[t]
\begin{center}
\begin{tikzpicture}
\node[state] (c1) {$c_0$};
\node[state, right of=c1] (c2) {$c_1$};
\node[state, right of=c2] (c3) {$c_2$};
\draw
(c1) edge[above] node[yshift = -1.1mm]{\small  $\begin{array}{l} i := 0 \\ s := 0 \end{array}$} (c2)
(c2) edge[loop] node[yshift = 7mm]{\small  $\begin{array}{l} i < m  \\ i := i+1 \\ s := s+i+1 \end{array}$} (c2)
(c2) edge[above] node{\small $i \geq m$} (c3);
\end{tikzpicture}
\end{center}
\vspace*{-4mm}
\caption{\label{fig:sum} Sum up to $m$}
\vspace*{-3mm}
 \end{figure}
\end{example}

In order to define the semantics of reachability formulas we first introduce the following relation.

\begin{definition
  \label{def:leadsto}
  $\leadsto$ is the largest set of pairs $(\tau, r) \in  \mbox{$\mathit{Paths}$} \times \Pi$ such that: (i) $\tau = s$ for some $ s\in S$, and $r\, s$;
  or (ii) $\tau = \ s\, \tau'$, for some $s \in S$, $\tau'\in \mbox{$\mathit{Paths}$}$, and  $r\, s$;  or (iii)  $\tau = \ s\, \tau'$ for some $s \in S$, $\tau'\in \mbox{$\mathit{Paths}$}$,  and $(\tau',r) \in \leadsto$.
\end{definition}
We write $\tau \leadsto r$
  for  $(\tau,r) \in \leadsto$. Tarski's  principle  induces the following coinduction principle for $\leadsto$:

\begin{lemma}
\label{lem:coindleadsto}
  For  $R \subseteq Paths \times \Pi$,
 if for all $(\tau, r) \in R$,  it holds that either $ (\exists s. \tau = s \wedge r \, s)$, or  $(\exists s.\exists \tau'.\tau = s\, \tau' \wedge r \, s) $  or $ (\exists s.\exists \tau'. \tau = s\, \tau' \wedge (\tau',r) \in R) $,
    then $R \subseteq\,  \leadsto$.
\end{lemma}

\begin{definition}[Validity]
  \label{def:valid}
 A formula
$\varphi \in \Phi_{\mathcal{S}}$ is \emph{valid} over $\mathcal{S}$, denoted by $\mathcal{S} \models \varphi$, whenever for all $\tau \in \mbox{$\mathit{Paths}$}_{\mathcal{S}}$ such that $(\mathit{lhs}\,  \varphi) \, (\mbox{$\mathit{hd}$}\, \tau)$ holds, it also holds that $\tau \leadsto_{\mathcal{S}} (\mathit{rhs}\, \varphi)$.
\end{definition}

\begin{example}
  \label{ex:valid}
 The formula $(c = c_0)\mbox{$\mathit{\,\Rightarrow\!\!\!\Diamond}\,$} (c =c_2 \wedge s =  m\times (m+1)/2)$ is valid over the transition system denoted by the state-machine depicted in Figure~\ref{fig:sum}. Intuitively, this means that all finite paths ``starting'' in the control node $c_0$ ``eventually reach'' $c_2$ with $s = m\times (m+1)/2$ holding. The ``eventually reach'' expression justifies the $\mbox{$\mathit{\,\Rightarrow\!\!\!\Diamond}\,$}$ notation borrowed from Linear Temporal Logic (LTL). Indeed, reachability formulas are essentially  LTL formulas for a certain version of LTL interpreted over finite paths.

\end{example}

We close the section with a simple notion of \emph{component} of  a transition system, and show that, if a formula is valid on a component,
then it is valid on the whole transition system.

\begin{definition}[Component]
  \label{def:comp}
 A transition system $(S', \to')$ is a \emph{component} of  $(S, \to)$  if
 \begin{itemize}
  \item $S' \subseteq S$ and $\to' \; \subseteq \; \to$;
 \item  for all $s',s \in S'$,  $s' \to s$ implies $s' \to' s$;
  \item  for all  $s' \in S'$,  $s \in S\setminus S'$,   $s' \to s$ implies  $s' \in \bullet_{\mathcal{S}'}$.
 \end{itemize}
 We  write   $\mathcal{S}' \leftslice \mathcal{S}$ when $\mathcal{S}'$ is a component of  $\mathcal{S}$.
 \end{definition}
That is,  $\mathcal{S}'$ is a full sub-transition system of $\mathcal{S}$,
and  one  may only ``exit''   from  $\mathcal{S}'$  via its final states.
We  often interchangeably use sets of states and their characteristic predicates, like we did for $\bullet_{\mathcal{S}'}$ above.

\begin{theorem}[Compositionality of $\models$ w.r.t\ transition systems]
  \label{th:tscomp}
   $\mathcal{S}' \leftslice \mathcal{S}$  and $\mathcal{S}' \models \varphi$ imply $\mathcal{S} \models \varphi$.
\end{theorem}
\begin{example}
  \label{ex:tscomp}
  In Figure~\ref{fig:sum}, the self-loop on the control node $c_1$

  denotes a transition system $\mathcal{S}'$ that is a component of the transition system $\mathcal{S}$ denoted by the whole state machine. Let $\varphi \mbox{$\triangleq$} (c = c_1 \wedge i = 0 \wedge s = 0) \mbox{$\mathit{\,\Rightarrow\!\!\!\Diamond}\,$} (c = c_1 \wedge i = m \wedge s = i\times(i+1)/2 )$.
  One can show  that
  $\mathcal{S}' \models \varphi$, thus, $\varphi$  is also valid over $\mathcal{S}$.
\end{example}
One could, in principle, prove the validity of reachability formulas directly from the semantical definitions. However, this has several disadvantages: lack of a methodology - each formula is proved in its own ad-hoc way, and lack of a notion of completeness - is there a uniform way for  proving every valid formula?  These issues are addressed by the  proof systems presented by increasing order of complexity in the next sections.

\section{A One-Rule Proof System}
\label{sec:one-rule}

\begin{figure}[t]
\small
 \begin{align*}
\textsf{[Stp]~}
&
\dfrac{\mathcal{S} \vdash \mbox{$\mathit{\partial}$} l' \mbox{$\mathit{\,\Rightarrow\!\!\!\Diamond}\,$} r}
      {\mathcal{S} \vdash l \mbox{$\mathit{\,\Rightarrow\!\!\!\Diamond}\,$} r}\nu \ \mathit{\ if \ } l \sqsubseteq l' \sqcup r,  l' \sqcap \bullet \sqsubseteq \bot
 \end{align*}
 \caption{\label{fig:pf1} One-rule proof system.}
 \vspace*{-3mm}
\end{figure}

Our first proof system is depicted as  the one-rule  inference system in Figure~\ref{fig:pf1}. It is parameterised by a transition system $\mathcal{S}$, and everything therein depends on it; we omit  $_\mathcal{S}$ subscripts for simplicity.  Intuitively, an application of the \textsf{[Stp]} rule can be seen as a symbolic execution step, taking a formula $l \mbox{$\mathit{\,\Rightarrow\!\!\!\Diamond}\,$} r$ and ``moving'' $l$ ``one step closer'' to $r$ - specifically, taking an over-approximation $l'$ of the ``difference'' between $l$ and $r$ (encoded in the side-condition $l \sqsubseteq l' \sqcup r$) that contains no final states ($l' \sqcap \bullet \sqsubseteq \bot$) and performing a symbolic execution step from $l'$ (encoded in the $\partial$ symbolic transition function). The rule is applicable infinitely many times, hence the $\nu$ symbol next to~it.
Note that there are no hypotheses in the proof system: those would be reachability formulas in the left-hand side of the $\vdash$ symbol, not allowed here.

For a more formal definition, consider the function $F : \mbox{$\mathcal{P}$}(\Phi) \to \mbox{$\mathcal{P}$}(\Phi)$ defined by

$$F(X) =  \bigcup_{l,l'r\in \Pi, \, l \sqsubseteq l' \sqcup r, l\, ' \sqcap \bullet \sqsubseteq \bot, \, \partial l' \mbox{\scriptsize{$\mathit{\,\Rightarrow\!\!\!\Diamond}\,$}} r \in X} \{  l \mbox{$\mathit{\,\Rightarrow\!\!\!\Diamond}\,$} r \}$$

\noindent  $F$ is monotone, and, by Knaster-Tarski's theorem, $F$ has a greatest fixpoint $\nu F$.
We now define $\mathcal{S}\vdash \varphi$
by $\varphi \in \nu F$.
Tarski's  coinduction principle then  induces the following coinduction principle for~$\vdash$:

\begin{lemma}
  \label{lem:coindvdash1}
For all  set $X\subseteq \Phi$ of hypotheses and $\varphi \in X$, if \emph{for all $l \mbox{$\mathit{\,\Rightarrow\!\!\!\Diamond}\,$} r  \in X $, there is $l' \in \Pi$  such that $l \sqsubseteq l' \sqcup r$, $ l' \sqcap \bullet \sqsubseteq \bot$ and  $\mbox{$\mathit{\partial}$} l' \mbox{$\mathit{\,\Rightarrow\!\!\!\Diamond}\,$} r\in X$},  then $\mathcal{S} \vdash \varphi$.
\end{lemma}

\paragraph*{Soundness.} Soundness means that only valid formulas are proved:
\begin{theorem}[Soundness of $\vdash$]
  \label{th:soundness}
  $\mathcal{S} \vdash \varphi$ implies $\mathcal{S} \models \varphi$.
\end{theorem}
The proof uses the coinduction principle of the $\leadsto$ relation (Lemma~\ref{lem:coindleadsto}), which occurs in the definition of validity, instantiated with the relation $R \subseteq \mbox{$\mathit{Paths}$} \times \Pi$ defined by $R \;\mbox{$\triangleq$}\; \lambda (\tau,r). \exists l.( \mathcal{S}\vdash l \mbox{$\mathit{\,\Rightarrow\!\!\!\Diamond}\,$} r \wedge l \,(\mbox{$\mathit{hd}$} \tau))$. As a general observation, all proofs by coinduction use a specific coinduction principle instantiated with a specific predicate/relation. The instantiation step is where the user's creativity is most involved.

\paragraph*{Completeness.}
Completeness is the reciprocal to soundness: any valid formula is provable. It is based on the following lemma, which essentially reduces reachability to a form of inductive invariance.

\begin{lemma}
  \label{lem:redtoinv}
If $l \sqsubseteq q \sqcup r$, $q \sqcap \bullet \sqsubseteq \bot$, and $\mbox{$\mathit{\partial}$} q \sqsubseteq q \sqcup r$ then $\mathcal{S} \vdash l \mbox{$\mathit{\,\Rightarrow\!\!\!\Diamond}\,$} r$.
\end{lemma}
The proof of this lemma uses Lemma~\ref{lem:coindvdash1} with an appropriate instantion of the set $X$ therein.
\begin{example}
  \label{ex:redtoinv}
  In order to establish $\mathcal{S}' \models (c = c_1 \wedge i = 0 \wedge s = 0) \mbox{$\mathit{\,\Rightarrow\!\!\!\Diamond}\,$} (c = c_1 \wedge i = m \wedge s = i\times(i+1)/2 )$ - which has been claimed in~Example~\ref{ex:tscomp} - one can use Lemma~\ref{lem:redtoinv} with $q \; \mbox{$\triangleq$} \;  (c = c_1 \wedge i < m \wedge s = i \times (i+1)/2) $.
\end{example}

 \begin{theorem}[Completeness of $\vdash$]
   \label{th:completeness}
   $\mathcal{S} \models \varphi$ implies $\mathcal{S} \vdash \varphi$.
 \end{theorem}
 The  proof of completeness is constructive: it   uses the predicate  $q \;\mbox{$\triangleq$} \; \lambda s.\,\neg r s \wedge \forall \tau \in \mbox{$\mathit{Paths}$}.(\,s = \mbox{$\mathit{hd}$}\, \tau$ $\Rightarrow$ $\tau \leadsto r)$  that, for valid formulas $l \mbox{$\mathit{\,\Rightarrow\!\!\!\Diamond}\,$} r$, is shown to satisfy the three inclusions of Lemma~\ref{lem:redtoinv}.
 One may wonder: even when one does not know whether a  formula $l \mbox{$\mathit{\,\Rightarrow\!\!\!\Diamond}\,$} r$ is valid, can one still use the above-defined $q$ and Lemma~\ref{lem:redtoinv}
 in order to prove it? The answer is negative:  proving the first implication $l \sqsubseteq q \sqcup r$ with the above-defined $q$
 amounts to proving validity directly from the semantics of formulas, thus losing any benefit of having   a proof system.
 Hence, completeness is  a theoretical property; the practically useful property is  Lemma~\ref{lem:redtoinv},  which users have to provide with a suitable $q$ that
 satisfy the three inclusions therein. In~\cite{rusu:hal-01962912} we use this lemmma for verifying  an infinite-state transition-system specification of a  hypervisor.

 \smallskip

 Looking back at the  proof system $\vdash$, we note that it is purely coinductive  -  no induction  is present at all.
 This is unlike the proof systems in forthcoming sections. Regarding compositionality (with respect to transition systems)
 our proof system has it, since, by soundness and completeness and Theorem~\ref{th:tscomp}, one has that $\mathcal{S}' \leftslice \mathcal{S}$ and $\mathcal{S}' \vdash \varphi$ implies $\mathcal{S}\vdash \varphi$.  However, we show below that $\vdash$ does not have another, equally  desirable compositionality feature:~\emph{asymmetrical compositionality} with respect to  formulas.

 \paragraph{Asymmetrical compositionality with respect to formulas.}
A proof system with this feature
 decomposes a proof of a formula $\varphi$ into a proof of a formula $\varphi'$ and one of $\varphi$ assuming~$\varphi'$. The asymmetry between the formulas involed suggested the property's name.
 In Definition~\ref{def:weakcomp} below, $\VDash$ is a binary relation - a subset of $\mbox{$\mathcal{P}$}(\Phi) \times \Phi$
(equivalently,  a predicate of type $\mbox{$\mathcal{P}$}(\Phi) \to \Phi \to \mathbb{B}$), parameterised by a transition system $\mathcal{S}$.
For \emph{hypotheses} $\mbox{$\mathcal{H}$} \subseteq \Phi$ and $\varphi \in \Phi$, we write $\mathcal{S}\!, \mbox{$\mathcal{H}$} \VDash \phi$ for $(\mbox{$\mathcal{H}$},\phi)  \in \; \VDash$ and $\mathcal{S} \VDash \phi$ for
$\mathcal{S}\!, \emptyset \VDash \phi$.

\begin{definition}[Asymmetrical compositionality with respect to formulas]
  \label{def:weakcomp}
  A  proof system $\VDash$ is asymmetrically compositional with respect to formulas  if
  $\mathcal{S} \!\VDash\varphi'$ and $\mathcal{S}\!, \{\varphi'\} \VDash \varphi $ imply $\mathcal{S}\! \VDash \varphi$.
\end{definition}
The proof system $\vdash$ is not asymmetrically compositional w.r.t.\ formulas, because that requires hypotheses,
which $\vdash$  does not have. One could add hypotheses to it, and a new rule to prove a formula if it is found among the hypotheses.
However,  note that, unlike the \textsf{[Stp]} rule, the new  rule has an inductive nature: it can only  occur a finite number of times in a $\vdash$ proof (specifically, at most once, at the end of a finite proof).

\section{An Asymmetrically-Compositional Proof System}

In this section we propose another proof system $\Vdash$ and show that it is  compositional with respect  to transition systems and asymmetrically compositional with respect to  formulas. These gains are achieved
thanks to a the introduction of inductive rules in the proof system, enabling a better distribution of roles between these rules and the remaining coinductive rule;  all at the cost of a more involved soundness proof.

\begin{figure}[t]
\small
\begin{align*}
 \textsf{[Hyp]~}
&
\dfrac{}
      {\mathcal{S}\!,\mbox{$\mathcal{H}$} \Vdash \varphi} \mu\ \mathit{\ if \ } \varphi \in \mbox{$\mathcal{H}$}\\
\textsf{[Trv]~}
&
\dfrac{}
      {\mathcal{S}\!,\mbox{$\mathcal{H}$} \Vdash r \mbox{$\mathit{\,\Rightarrow\!\!\!\Diamond}\,$} r}\mu\\
\textsf{[Str]~}
&
\dfrac{\mathcal{S}\!,\mbox{$\mathcal{H}$} \Vdash l' \mbox{$\mathit{\,\Rightarrow\!\!\!\Diamond}\,$} r}
      {\mathcal{S}\!,\mbox{$\mathcal{H}$} \Vdash l \mbox{$\mathit{\,\Rightarrow\!\!\!\Diamond}\,$} r}\mu \ \mathit{\ if \ } l \sqsubseteq l'\\
\textsf{[Spl]~}
&
\dfrac{\mathcal{S}\!,\mbox{$\mathcal{H}$} \Vdash l_1 \mbox{$\mathit{\,\Rightarrow\!\!\!\Diamond}\,$} r \qquad \mathcal{S}\!,\mbox{$\mathcal{H}$} \Vdash l_2 \mbox{$\mathit{\,\Rightarrow\!\!\!\Diamond}\,$} r}
      {\mathcal{S}\!,\mbox{$\mathcal{H}$} \Vdash (l_1 \sqcup l_2) \mbox{$\mathit{\,\Rightarrow\!\!\!\Diamond}\,$} r} \mu\\
\textsf{[Tra]~}
&
\dfrac{\mathcal{S}\!\models  l \mbox{$\mathit{\,\Rightarrow\!\!\!\Diamond}\,$} m \qquad \mathcal{S}\!,\mbox{$\mathcal{H}$} \Vdash m \mbox{$\mathit{\,\Rightarrow\!\!\!\Diamond}\,$} r}
      {\mathcal{S}\!,\mbox{$\mathcal{H}$} \Vdash l \mbox{$\mathit{\,\Rightarrow\!\!\!\Diamond}\,$} r} \mu \\
\textsf{[Stp]~}
&
\dfrac{\mathcal{S}\!,\mbox{$\mathcal{H}$}  \Vdash \mbox{$\mathit{\partial}$} l \mbox{$\mathit{\,\Rightarrow\!\!\!\Diamond}\,$} r}
      {\mathcal{S}\!,\mbox{$\mathcal{H}$} \Vdash l \mbox{$\mathit{\,\Rightarrow\!\!\!\Diamond}\,$} r}\nu \mathit{\ if \ }  l \sqcap \bullet \sqsubseteq \bot
 \end{align*}
   \caption{\label{fig:pf2} Mixed inductive-coinductive proof system.}
\end{figure}
Our second proof system is depicted in Figure~\ref{fig:pf2}. It is a binary relation - a subset of
$\mbox{$\mathcal{P}$}(\Phi) \times \Phi$ (or equivalently, a binary predicate of type $\mbox{$\mathcal{P}$}(\Phi) \to \Phi \to \mathbb{B}$),  parameterised by a transition system $\mathcal{S}$.
Intuitively, the rule  \textsf{[Stp]}, labelled with $\nu$, is coinductive, i.e., it can be applied infinitely many times, and
the rules \textsf{[Hyp]}, \textsf{[Trv]}, \textsf{[Str]}, \textsf{[Spl]}, and \textsf{[Tra]}, labelled by $\mu$ are inductive, i.e., they can only be applied finitely many times between two consecutive applications of \textsf{[Stp]}. Stated differently, a proof in $\Vdash$ is a possibly infinite series of \emph{phases}, and in each phase there are finitely many applications of \textsf{[Hyp]}, \textsf{[Trv]}, \textsf{[Str]}, \textsf{[Spl]}, and \textsf{[Tra]} and,  except in the last phase (if such a last phase exists), one application of \textsf{[Stp]}.

Note that making the inductive rules coinductive would compromise soundness, because, e.g., the
\textsf{[Str]} rule could forever reduce a proof of any formula to itself, thus proving any formula, valid or not.

The roles of the rules are the following ones.  \textsf{[Hyp]} allows one to prove a formula if it is among the hypotheses.   \textsf{[Trv]}  is in charge of proving trivially valid formulas. \textsf{[Str]} is a general principle that amounts to strengthening a formula before proving it. \textsf{[Spl]} is used for getting rid of disjunctions in left-hand sides of formulas,
which occur when several, alternative symbolic behaviours are explored in a proof search.
 \textsf{[Tra]} is a transitivity rule, used for proving facts about sequential symbolic behaviour.
 Note also the asymmetry in hypotheses of the rule \textsf{[Tra]}: for one formula validity is required, while for the other one, it is provability. This asymmetry is used to avoid technical difficulties that arise when proving the soundness of~$\Vdash$, but, as we shall see, it generates difficulties of its own.
Finally, \textsf{[Stp]} makes the  connection between the concrete paths  and the symbolic ones, which the proof system explores during proof search.

For a formal definition: consider the following functions from $\mbox{$\mathcal{P}$}(\Phi)$ to $\mbox{$\mathcal{P}$}(\Phi)$ defined by

\begin{itemize}
 \item $\vdash_{{\cal S,H},\, Y}^{\mathsf{[Hyp]}}(X) = \mbox{$\mathcal{H}$}$

\item $\vdash_{{\cal S,H},\, Y}^{\mathsf{[Trv]}}(X) = \bigcup_{r \in \Pi} \{r \mbox{$\mathit{\,\Rightarrow\!\!\!\Diamond}\,$} r\}$

\item  $\vdash_{{\cal S, H},\, Y}^{\mathsf{[Str]}}(X) = \bigcup_{l,l',r \in \Pi, \, l' \mbox{\scriptsize{$\mathit{\,\Rightarrow\!\!\!\Diamond}\,$}} r \in X, \,  l \sqsubseteq l'} \{l \mbox{$\mathit{\,\Rightarrow\!\!\!\Diamond}\,$} r\}$
 \item $\vdash_{{\cal S, H},\, Y}^{\mathsf{[Spl]}}(X) = \bigcup_{l_1, l_2, r\, \in \Pi,\,  \{l_1 \mbox{\scriptsize{$\mathit{\,\Rightarrow\!\!\!\Diamond}\,$}} r,\, l_2 \mbox{\scriptsize{$\mathit{\,\Rightarrow\!\!\!\Diamond}\,$}} r\} \subseteq X} \{(l_1 \sqcup l_2) \mbox{$\mathit{\,\Rightarrow\!\!\!\Diamond}\,$} r\}$
 \item  $\vdash_{{\cal S, H},\, Y}^{\mathsf{[Tra]}}(X) = \bigcup_{l,r,m \in \Pi, \, \mathcal{S} \models l \mbox{\scriptsize{$\mathit{\,\Rightarrow\!\!\!\Diamond}\,$}} m, \; m\mbox{\scriptsize{$\mathit{\,\Rightarrow\!\!\!\Diamond}\,$}} r \in X} \{l \mbox{$\mathit{\,\Rightarrow\!\!\!\Diamond}\,$} r\}$

\item $\vdash_{{\cal S, H},\, Y}^{\mathsf{[Stp]}}(X) =  \bigcup_{l,r\in \Pi, \, l \sqcap \bullet \sqsubseteq \bot, \, \partial l \mbox{\scriptsize{$\mathit{\,\Rightarrow\!\!\!\Diamond}\,$}} r \in Y} \{  l \mbox{$\mathit{\,\Rightarrow\!\!\!\Diamond}\,$} r \}$
\end{itemize}
Let  $\vdash_{{\cal S, H}, Y}\!(X) \!= \vdash_{{\cal S, H}, Y}^{\mathsf{[Hyp]}}\!(X) \cup\!\vdash_{{\cal S, H}, Y}^{\mathsf{[Trv]}}\!(X)  \cup\!\vdash_{{\cal S, H}, Y}^{\mathsf{[Str]}}\!(X)   \cup\!\vdash_{{\cal S, H}, Y}^{\mathsf{[Spl]}}\!(X)   \cup\!\vdash_{{\cal S, H}, Y}^{\mathsf{[Tra]}}\!(X)  \cup\!\vdash_{{\cal S, H}, Y}^{\mathsf{[Stp]}}\!(X)$.
 It is not hard to show that $\vdash_{{\cal S,H},\, Y} : \mbox{$\mathcal{P}$}(\Phi) \to \mbox{$\mathcal{P}$}(\Phi)$ is continuous, thus, by the Knaster Tarski and Kleene fixpoint theorems
 it has a smallest fixpoint $\mu\!\vdash_{{\cal S, H},\, Y} =\bigcup_{n=1}^{\infty} \vdash_{{\cal S, H},\, Y}^n(\emptyset)$.

Now,  we define the function $F_{{\cal S, H}} : \mbox{$\mathcal{P}$}(\Phi) \to \mbox{$\mathcal{P}$}(\Phi)$ by
$F_{{\cal S, H}}(Y) = \mu\!\vdash_{{\cal S, H}, \, Y}$.   $F_{{\cal S, H}}$ is monotone, thus,  it has a greatest fixpoint
$\nu F_{{\cal S, H}} = \nu (\lambda Y.\mu\!\vdash_{{\cal S, H}, \, Y})$ $ = \nu\mu\!\vdash_{\cal S, H}$.

We  define the proof system $\Vdash$ as follows : for all $\mbox{$\mathcal{H}$}  \subseteq \Phi$ and $\varphi \in \Phi$,
$\mathcal{S}\!,\mbox{$\mathcal{H}$} \Vdash\phi $ iff  $\varphi \in \nu\mu\!\vdash_{\cal S, H}$.
The  inductive-coiductive nature of  $\Vdash$ is visible from its definition. It admits the following coinduction principle:

\begin{lemma}
  \label{def:coindps2}
If  $ X \subseteq\mu\!\vdash_{{\cal S, H}, \ X}$
then for all
$ \varphi \in X$ it holds that  $\mathcal{S}\!, \mbox{$\mathcal{H}$} \Vdash\varphi$.
\end{lemma}

\paragraph*{Using the coinduction principle.} For proving statements of the form $\mathcal{S}\!, \mbox{$\mathcal{H}$} \Vdash\varphi$, one can:
\begin{itemize}

 \item   find a sequence  $X = X_0, \cdots X_n = \emptyset$ of sets
   such that $X_i \; \subseteq  \; \vdash_{{\cal S, H}\, , X} (X_{i+1})$, for $i = 0, \ldots, n-1$, and $\varphi\in X$;
\item  since
  $\mu\!\vdash_{{\cal S, H}, \, X } =\bigcup_{n=1}^{\infty} \vdash_{{\cal S, H}, \, X}^n(\emptyset)$, we obtain by induction on $n$
that   $X_i \subseteq \mu\!\vdash_{{\cal S, H}\, ,X}$ for  $i = 0, \ldots, n-1$ and in particular
  $X \subseteq  \mu\!\vdash_{{\cal S, H}\, , X }$. By Lemma~\ref{def:coindps2}, $\mathcal{S}\!, \mbox{$\mathcal{H}$} \Vdash\varphi$.
\end{itemize}

We illustrate the  above approach by proving a key lemma for the completeness of $\Vdash$.

  \begin{lemma}
  \label{lem:redtoinv2}
If $l \sqsubseteq q \sqcup r$, $q \sqcap \bullet \sqsubseteq \bot$, and $\mbox{$\mathit{\partial}$} q \sqsubseteq q \sqcup r$ then $\mathcal{S}\Vdash l \mbox{$\mathit{\,\Rightarrow\!\!\!\Diamond}\,$} r$.
\end{lemma}
  \begin{proof}
    We apply the above  approach. Note that $\mbox{$\mathcal{H}$} = \emptyset$.
   We choose  $X= X_0 = \{l \mbox{$\mathit{\,\Rightarrow\!\!\!\Diamond}\,$} r, q \mbox{$\mathit{\,\Rightarrow\!\!\!\Diamond}\,$} r, \mbox{$\mathit{\partial}$} q \mbox{$\mathit{\,\Rightarrow\!\!\!\Diamond}\,$} r\}$.
\begin{itemize}
\item Let
  $X_1  = \{(q \sqcup r)\mbox{$\mathit{\,\Rightarrow\!\!\!\Diamond}\,$} r,  q \mbox{$\mathit{\,\Rightarrow\!\!\!\Diamond}\,$} r, \mbox{$\mathit{\partial}$} q \mbox{$\mathit{\,\Rightarrow\!\!\!\Diamond}\,$} r\}$;  using the hypothesis $l \sqsubseteq q \sqcup r$,
  $X_0  \subseteq \vdash^{\mathsf{[Str]}}_{{\mathcal{S}}\, , \emptyset, \, X}(X_1) \subseteq \vdash_{{\mathcal{S}}\,, \emptyset, \, X}(X_1)$;

\item Let $X_2 =\{q \mbox{$\mathit{\,\Rightarrow\!\!\!\Diamond}\,$} r, r\mbox{$\mathit{\,\Rightarrow\!\!\!\Diamond}\,$} r, \mbox{$\mathit{\partial}$} q \mbox{$\mathit{\,\Rightarrow\!\!\!\Diamond}\,$} r\}$ ; we obtain
  $X_1  \subseteq  \vdash^{\mathsf{[Spl]}}_{{\mathcal{S}},\emptyset,\, X} (X_2) \subseteq \vdash_{{\mathcal{S}},\emptyset,\, X}(X_2)$;
    \item Let $X_3 = \{q \mbox{$\mathit{\,\Rightarrow\!\!\!\Diamond}\,$} r\,, \mbox{$\mathit{\partial}$} q \mbox{$\mathit{\,\Rightarrow\!\!\!\Diamond}\,$} r\}$; we obtain $X_2 \subseteq \vdash^{\mathsf{[Trv]}}_{{\mathcal{S}},\emptyset,\, X}(X_3) \subseteq \vdash_{{\mathcal{S}},\emptyset,\, X}(X_3)$;
    \item Let $X_4 = \{\mbox{$\mathit{\partial}$} q \mbox{$\mathit{\,\Rightarrow\!\!\!\Diamond}\,$} r\}$; using  the second  hypothesis $q \sqcap \bullet \sqsubseteq \bot$ and  the fact that $\partial q \mbox{$\mathit{\,\Rightarrow\!\!\!\Diamond}\,$} l \in  X $ we obtain
      $X_3 \subseteq \vdash^{\mathsf{[Stp]}}_{{\mathcal{S}},\emptyset,\, X}(X_4) \subseteq\vdash_{{\mathcal{S}},\emptyset,\, X} (X_4)$
      ;
    \item Let  $X_5 = \{(q \sqcup r) \mbox{$\mathit{\,\Rightarrow\!\!\!\Diamond}\,$} r\}$ ; using the  hypothesis $\mbox{$\mathit{\partial}$} q \sqsubseteq q \sqcup r$, we obtain
  $X_4 \subseteq \vdash^{\mathsf{[Str]}}_{{\mathcal{S}}, \emptyset,\, X}(X_5) \subseteq \vdash_{{\mathcal{S}}, \emptyset,\, X}(X_5)$;
    \item Let $X_6 = \{q \mbox{$\mathit{\,\Rightarrow\!\!\!\Diamond}\,$} r, r\mbox{$\mathit{\,\Rightarrow\!\!\!\Diamond}\,$} r\}$; we obtain $X_5 \subseteq \vdash^{\mathsf{[Spl]}}_{{\mathcal{S}},\emptyset,\, X}(X_6) \subseteq \vdash_{{\mathcal{S}},\emptyset,\, X}(X_6)$;

\item    Let $X_7 = \{q \mbox{$\mathit{\,\Rightarrow\!\!\!\Diamond}\,$} r\}$; we obtain $X_6 \subseteq \vdash^{\mathsf{[Trv]}}_{{\mathcal{S}},\emptyset,\, X}(X_7) \subseteq \vdash_{{\mathcal{S}},\emptyset,\, X}(X_7)$;

\item  Let $X_8 = \emptyset$; using the second hypothesis $q \sqcap \bullet \sqsubseteq \bot$ and  the fact that $\partial q \mbox{$\mathit{\,\Rightarrow\!\!\!\Diamond}\,$} l \in  X$, we obtain $X_7 \subseteq \vdash^{\mathsf{[Stp]}}_{{\mathcal{S}},\emptyset,\, X}(X_8) \subseteq \vdash_{{\mathcal{S}},\emptyset,\, X}(X_8)$.
\end{itemize}
Hence, by basic properties of inclusion, $X\subseteq \bigcup_{n = 0}^{7} \vdash^{n}_{{\mathcal{S}},\emptyset,\, X} (\emptyset) \subseteq \bigcup_{n = 0}^{\infty} \vdash^{n}_{{\mathcal{S}},\emptyset,\, X} (\emptyset) = \mu\!\vdash _{{\mathcal{S}},\emptyset,\, X}$, and from $l \mbox{$\mathit{\,\Rightarrow\!\!\!\Diamond}\,$} r \in X$ and Lemma~\ref{def:coindps2}  we obtain $\mathcal{S}\vdash l \mbox{$\mathit{\,\Rightarrow\!\!\!\Diamond}\,$} r$.
\end{proof}

  \paragraph*{Soundness.}
  We define the recursive function $\mbox{$\mathit{suf}$} :  \{\tau \in \mbox{$\mathit{Paths}$} \} \to \{i : \mathbb{N} \mid i \leq (\mbox{$\mathit{len}$}\,  \tau)\}  \to \mbox{$\mathit{Paths}$}$ by
  $\mbox{$\mathit{suf}$}\,  \tau \, 0 = \tau$ and $ \mbox{$\mathit{suf}$} (s\, \tau) (i + 1) = \mbox{$\mathit{suf}$} \, \tau \, i$. Intuitively, $\mbox{$\mathit{suf}$} \, \tau \, i$ is the sequence obtained by removing $i \leq (\mbox{$\mathit{len}$} \, \tau)$ elements from the ``beginning'' of $\tau$.
  This  is required in the definition of the following relation and is used hereafter.

\begin{definition
  \label{def:hookright}
  $\hookrightarrow \subseteq \mbox{$\mathit{Paths}$} \times \Pi$ is the largest set of pairs $(\tau, r)$ such that: (i) $\tau = s$ for some $ \in S$ such that $r\, s$;
  or (ii) $\tau = \ s\, \tau'$, for some $s \in S$, $\tau'\in \mbox{$\mathit{Paths}$}$ such that  $r\, s$;  or (iii)  $\tau = \ s\, \tau'$ for some $s \in S$, $\tau'\in \mbox{$\mathit{Paths}$}$  and $n \leq (\mbox{$\mathit{len}$}\,  \tau')$
  such that $((\mbox{$\mathit{suf}$}\, \tau' \, n),r) \in \hookrightarrow$.
\end{definition}
We write $\tau \hookrightarrow r$  instead of $(\tau,r) \in \hookrightarrow$. By analogy with Lemma~\ref{lem:coindleadsto} (coinduction principle for the  $\leadsto$ relation), but using Tarski's strong induction principle, we obtain:

\begin{lemma}
\label{lem:coindhookright}
 Let $R\!\subseteq\!Paths\!\times\!\Pi$ be s.t.\  $(\tau, r) \in R\!\Rightarrow\!(\exists s. \tau\!=\!s\!\wedge\!r \, s)\!\vee\!(\exists s.\exists \tau'.\tau = s\, \tau' \wedge r \, s) \vee (\exists s.\exists \tau' .\exists n.\exists \tau''. \tau = s\, \tau'
  \wedge \tau'' =  (\mbox{$\mathit{suf}$}\,  \tau'\, n) \wedge (\tau'',r) \in R \vee \tau''\hookrightarrow r)) $.
     Then $R \subseteq\,  \hookrightarrow$.
\end{lemma}
The following lemma is easily proved, by instantiating the parameter relation $R$, which occurs
in both the coinduction principles  of the relations $\leadsto, \hookrightarrow$, with the other relation:

\begin{lemma}[$\leadsto$ equals  $\hookrightarrow$]
  \label{lem:eqrel}
  For all $\tau \in \mbox{$\mathit{Paths}$}$ and $r \in \Pi$, $\tau \leadsto r$ if and only if $\tau \hookrightarrow r$.
\end{lemma}
Using the coinduction principle for $\hookrightarrow$ and the above equality, as well as the induction principle for the functional $\vdash_{ {\cal S, H}, \, \nu\mu\vdash_{\cal S, H}  } $
we obtain, in a rather involved proof  mixing induction and coinduction:

\begin{theorem}[Soundness of $\Vdash$]
  \label{th:soundps2}
  If for all $\varphi' \in \mbox{$\mathcal{H}$}$,  $\mathcal{S} \models \varphi'$, then $\mathcal{S}\!,\mbox{$\mathcal{H}$} \Vdash \varphi$ implies $\mathcal{S}\models \varphi$.
\end{theorem}

   \begin{example}
   \label{ex:ps2}
   We sketch a proof of the fact that the transition system $\mathcal{S}$ denoted by the state machine in Figure~\ref{fig:sum}  meets its functional correcteness property:
  (i) $\mathcal{S} \models (c = c_0)\mbox{$\mathit{\,\Rightarrow\!\!\!\Diamond}\,$} (c =c_2 \wedge s =  m\times (m+1)/2)$. We first show

   (ii) $\mathcal{S} \models (c = c_0) \mbox{$\mathit{\,\Rightarrow\!\!\!\Diamond}\,$} (c = c_1 \wedge i = 0 \wedge s = 0)$, which can be done using
   in sequence the rules \textsf{[Stp]}, \textsf{[Str]}, and \textsf{[Trv]} of the $\Vdash$ proof system together with its soundness.
   Using (ii) and the \textsf{[Tra]} rule, (i) reduces to
    proving (iii) $\mathcal{S} \Vdash  (c = c_1 \wedge i = 0 \wedge s = 0)\mbox{$\mathit{\,\Rightarrow\!\!\!\Diamond}\,$} (c =c_2 \wedge s =  m\times (m+1)/2)$. Next, in Examples~\ref{ex:tscomp} and~\ref{ex:redtoinv}
   we established\footnote{Example~\ref{ex:redtoinv} used the proof system $\Vdash$ and its Lemma~\ref{lem:redtoinv}, but $\Vdash$ and its corresponding Lemma~\ref{lem:redtoinv2} can be used just as well.} $\mathcal{S} \models (c = c_1 \wedge i = 0 \wedge s = 0) \mbox{$\mathit{\,\Rightarrow\!\!\!\Diamond}\,$} (c = c_1 \wedge i = m \wedge s = i\times(i+1)/2 )$, hence, using this and the \textsf{[Tra]} rule,  (iii)  reduces to proving
   $\mathcal{S} \Vdash (c = c_1 \wedge i = m \wedge s = i\times(i+1)/2 ) \mbox{$\mathit{\,\Rightarrow\!\!\!\Diamond}\,$} (c = c_2 \wedge s = m\times(m+1)/2 )$. This  is performed by applying in sequence the rules \textsf{[Stp]}, \textsf{[Str]}, and \textsf{[Trv]}, which concludes the proof.
 \end{example}

 \paragraph*{Completeness.}
 By  analogy with Theorem~\ref{th:completeness}, but using Lemma~\ref{lem:redtoinv2} instead of Lemma~\ref{lem:redtoinv}:

  \begin{theorem}[Completeness of $\Vdash$]
    \label{th:completeness2}
   $\mathcal{S} \models \varphi$ implies $\mathcal{S}\Vdash \varphi$.
  \end{theorem}

  \paragraph*{Compositionality.}
  Remembering Definition~\ref{def:weakcomp} of asymmetrical compositionality w.r.t\ formulas:

  \begin{theorem}
    \label{th:ps2comp} $\Vdash$ is  asymetrically compositional with respect to formulas.
  \end{theorem}
  \begin{proof}
    We have to show that if  (i) $\mathcal{S}\Vdash \varphi'$ and (ii) $\mathcal{S}\!,  \{\varphi'\} \Vdash \varphi $ then $\mathcal{S}\Vdash \varphi$.
    Now, (i) and (ii) and the soundness of $\Vdash$ imply  $\mathcal{S} \models \varphi'$ and  then $\mathcal{S} \models \varphi$, and then
    the conclusion $\mathcal{S}\Vdash \varphi$ holds by the completeness of $\Vdash$.
  \end{proof}

     Note that the statement (i) can be replaced by a weaker $\mathcal{S}'\!\Vdash \varphi'$  for  components $\mathcal{S}' \leftslice \mathcal{S}$, thanks to the
     soundness and completenesss of $\Vdash$ and of Theorem~\ref{th:tscomp}. This allows us to mix
     the compositionality of $\Vdash $ with respect to transition systems and the asymetrical one with respect to formulas.

     The $\Vdash$ proof system is thus better at compositionality than $\vdash$, thanks to the inclusion of inductive rules, in particular, of the rule $\textsf{[Hyp]}$, but
     at the cost of a more involved soundness proof.
  It still has a problem: the asymmetry of the $\textsf{[Tra]}$ rule, required by the soundness proof, is not  elegant since the rule
  mixes semantics $\models$ and syntax $\Vdash$. This is not only an issue of elegance, but a practical issue as well.
  \begin{example}
    \label{ex:astra}
    We attempt to prove the property (i) from Example~\ref{ex:ps2} using the asymmetrical  compositionality
    of $\Vdash$ w.r.t formulas. The first step, similar to that of Example~\ref{ex:ps2},
    is proving  (ii') $\mathcal{S} \Vdash (c = c_0) \mbox{$\mathit{\,\Rightarrow\!\!\!\Diamond}\,$} (c = c_1 \wedge i = 0 \wedge s = 0)$ by using
    in sequence the rules \textsf{[Stp]}, \textsf{[Str]}, and \textsf{[Trv]} of  $\Vdash$.
    Then, Theorem~\ref{th:ps2comp} reduces (i) to (iii') $\mathcal{S},\{(c = c_0) \mbox{$\mathit{\,\Rightarrow\!\!\!\Diamond}\,$} (c = c_1 \wedge i = 0 \wedge s = 0)\} \Vdash  (c = c_0)\mbox{$\mathit{\,\Rightarrow\!\!\!\Diamond}\,$} (c =c_2 \wedge s =  m\times (m+1)/2)$.
    The natural next step would be to use  the  \textsf{[Tra]} rule of  $\Vdash$,
    splitting  (iii') in two parts:  $\mathcal{S},\{(c = c_0) \mbox{$\mathit{\,\Rightarrow\!\!\!\Diamond}\,$} (c = c_1 \wedge i = 0 \wedge s = 0)\} \Vdash  (c = c_0)\mbox{$\mathit{\,\Rightarrow\!\!\!\Diamond}\,$} (c = c_1 \wedge i = 0 \wedge s = 0)$,  discharged by \textsf{[Hyp]}, and
   then $\mathcal{S},\{(c = c_0) \mbox{$\mathit{\,\Rightarrow\!\!\!\Diamond}\,$} (c = c_1 \wedge i = 0 \wedge s = 0)\} \Vdash  (c = c_1  \wedge i = 0 \wedge s = 0)\mbox{$\mathit{\,\Rightarrow\!\!\!\Diamond}\,$}  \mbox{$\mathit{\,\Rightarrow\!\!\!\Diamond}\,$} (c = c_1 \wedge i = 0 \wedge s = 0)$. But the \textsf{[Tra]} rule of  $\Vdash$, as it is, does not allow this. Hence, when one uses compositionality, one may get stuck in proofs because of technical issues with \textsf{[Tra]}.
  \end{example}
These issues are solved in the third proof system, which incorporates even more induction that the second one, and specialises its coinduction even closer to our problem domain. The third proof system also has better compositionality features. These gains come at the cost of an even more involved soundness proof.

\section{A Symmetrically-Compositional Proof System}

\begin{figure}[t]
\small
\begin{align*}
 \textsf{[Hyp]~}
&
\dfrac{}
      {\mathcal{S}\!,\mbox{$\mathcal{H}$} \Vvdash (\mbox{\textsc{t}},\varphi)} \mu\ \mathit{\ if \ } (\mbox{\textsc{f}},\varphi) \in \mbox{$\mathcal{H}$}\\
\textsf{[Trv]~}
&
\dfrac{}
      {\mathcal{S}\!,\mbox{$\mathcal{H}$} \Vvdash (b,r \mbox{$\mathit{\,\Rightarrow\!\!\!\Diamond}\,$} r)}\mu\\
\textsf{[Str]~}
&
\dfrac{\mathcal{S}\!,\mbox{$\mathcal{H}$} \Vvdash (b,l' \mbox{$\mathit{\,\Rightarrow\!\!\!\Diamond}\,$} r)}
      {\mathcal{S}\!,\mbox{$\mathcal{H}$} \Vvdash (b,l \mbox{$\mathit{\,\Rightarrow\!\!\!\Diamond}\,$} r)}\mu \ \mathit{\ if \ } l \sqsubseteq l'\\
\textsf{[Spl]~}
&
\dfrac{\mathcal{S}\!,\mbox{$\mathcal{H}$} \Vvdash (b,l_1 \mbox{$\mathit{\,\Rightarrow\!\!\!\Diamond}\,$} r) \qquad \mathcal{S}\!,\mbox{$\mathcal{H}$} \Vvdash (b,l_1 \mbox{$\mathit{\,\Rightarrow\!\!\!\Diamond}\,$} r)}
      {\mathcal{S}\!,\mbox{$\mathcal{H}$} \Vvdash (b,(l_1 \sqcup l_2)) \mbox{$\mathit{\,\Rightarrow\!\!\!\Diamond}\,$} r} \mu\\
\textsf{[Tra]~}
&
\dfrac{\mathcal{S}\!, \mbox{$\mathcal{H}$}  \Vvdash  (b,l \mbox{$\mathit{\,\Rightarrow\!\!\!\Diamond}\,$} m) \qquad \mathcal{S},\mbox{$\mathcal{H}$} \Vvdash (b,m \mbox{$\mathit{\,\Rightarrow\!\!\!\Diamond}\,$} r)}
      {\mathcal{S}\!,\mbox{$\mathcal{H}$} \Vvdash (b,l \mbox{$\mathit{\,\Rightarrow\!\!\!\Diamond}\,$} r)} \mu \\
\textsf{[Stp]~}
&
\dfrac{\mathcal{S}\!,\mbox{$\mathcal{H}$}  \Vvdash (\mbox{\textsc{t}},\mbox{$\mathit{\partial}$} l \mbox{$\mathit{\,\Rightarrow\!\!\!\Diamond}\,$} r)}
      {\mathcal{S}\!,\mbox{$\mathcal{H}$} \Vvdash (b,l \mbox{$\mathit{\,\Rightarrow\!\!\!\Diamond}\,$} r)}\mu \mathit{\ if \ }  l \sqcap \bullet \sqsubseteq \bot \\
 \textsf{[Cut]~}
&
\dfrac{\mathcal{S}\!,\mbox{$\mathcal{H}$}  \Vvdash (\mbox{\textsc{f}}, \varphi') \qquad  \mathcal{S}\!,\mbox{$\mathcal{H}$}\cup\{(\mbox{\textsc{f}},\varphi')\}  \Vvdash (b, \varphi)}
      {\mathcal{S}\!,\mbox{$\mathcal{H}$} \Vvdash (b, \varphi)}\mu \\
 \textsf{[Cof]~}
&
\dfrac{\mathcal{S}\!,\mbox{$\mathcal{H}$}\cup\{(\mbox{\textsc{f}},\varphi)\}  \Vvdash (\mbox{\textsc{f}}, \varphi)}
      {\mathcal{S}\!,\mbox{$\mathcal{H}$} \Vvdash (b, \varphi)}\mu\\
  \textsf{[Clr]~}
&
\dfrac{\mathcal{S}\!,\mbox{$\mathcal{H}$} \Vvdash (b, \varphi)}
      {\mathcal{S}\!,\mbox{$\mathcal{H}$}\cup\{(b',\varphi')\}  \Vvdash (b, \varphi)}\mu
 \end{align*}
   \caption{\label{fig:pf3}  Inductive proof system, with coinduction managed in hypotheses.}
\end{figure}

Our third proof system is depicted in Figure~\ref{fig:pf3}. A first difference with the previous one is that hypotheses and conclusions
are pairs of a Boolean tag and a formula. We call them tagged formulas, or simply formulas when there is no risk of confusion. The role of the tags is  to avoid unsoundness.

  The second difference is that the proof system is essentially inductive, i.e., there are no more infinite proofs, and
 no coinduction principle any more; whatever coinduction remains is tailored to our problem and emulated by the proof system, as can be seen seen below in the description of the proof system's rules.

Another difference, especially with the second proof system $\Vdash$, is that the hypotheses set is not constant.  The following rules change the hypotheses set.  First, the \textsf{[Cut]} rule, which says that in order to prove $(b,\varphi)$ under hypotheses $\mbox{$\mathcal{H}$}$, it is enough to prove $(\mbox{\textsc{f}},\varphi')$
  -  for some formula $\varphi'$ - under hypotheses $\mbox{$\mathcal{H}$}$, and to prove  $(b,\varphi)$ under $\mbox{$\mathcal{H}$} \cup \{(\mbox{\textsc{f}},\varphi')\}$. This resembles a standard cut rule, but it is taylored to our specific setting. Second, the \textsf{[Cof]} rule adds a ``copy'' of the conclusion in the
  hypotheses, but tagged with \mbox{\textsc{f}}\ -  and the new conclusion is also tagged with $\mbox{\textsc{f}}$. It is called  this way in reference to the Coq \texttt{cofix} tactic that builds coinductive proofs in Coq  also by copying a conclusion in the hypotheses; hence, we emulate in our proof system's hypotheses a certain existing coinduction mechanism, and taylor it to proving reachability formulas. Note that, without the tags,  one could simply assume any formula by \textsf{[Cof]} and prove it by \textsf{[Hyp]}, which would be unsound since it would prove any

  formula, valid or not. Third, the \textsf{[Clr]} rule  removes a formula from the hypotheses.
  Note that the \textsf{[Stp]} rule, when applied bottom to top, switches the Boolean from whatever value $b$ it has to $\mbox{\textsc{t}}$. Hence, it is  \textsf{[Stp]} that makes ``progress'' in our setting, enabling the use of \textsf{[Hyp]} in a sound way.
  The other rules have the same respective roles as their homonyms in  $\Vdash$.

\paragraph*{Soundness.} We present the
  soundness proof of $\Vvdash$ at a higher level of abstraction than for
  the other proof systems. For example, we define  $\Vvdash$-proofs as finite trees, and   assume that finite trees are known to the readers.
  For the other proof systems we adopted a more formal approach
  because the  proofs in those systems were certain kinds of possibly infinite trees, whose a priori knowledge
  cannot be  assumed.

  \begin{definition}[Proof]
    A \emph{proof} of a tagged formula $(b,\varphi)$ for a transition system $\mathcal{S}$  and under hypotheses $\mbox{$\mathcal{H}$}$ - for short,
    a proof of $\mathcal{S}\!,\mbox{$\mathcal{H}$} \Vvdash (b,\varphi)$
    - is a finite tree, whose root is labelled by the sequent  $\mathcal{S}\!,\mbox{$\mathcal{H}$} \Vvdash (b,\varphi)$, whose nodes are also labelled by sequents, obtained by applying bottom-up the rules depicted in Figure~\ref{fig:pf3}.
  \end{definition}
  We sometimes just write $\mathcal{S}\!,\mbox{$\mathcal{H}$} \Vvdash (b,\varphi)$ for ``there is a proof of  $\mathcal{S}\!,\mbox{$\mathcal{H}$} \Vvdash (b,\varphi)$'' as defined above. The following definition introduces the sets of all hypotheses and of all conclusions occuring in a proof.

  \begin{definition}[All hypotheses and conclusions occuring  in proof] Assume a proof $\Theta$  of $\mathcal{S}\!,\mbox{$\mathcal{H}$} \Vvdash (b,\varphi)$. The set $\mbox{$\mathsf{Hyp}$}$ is the union of all sets $\mbox{$\mathcal{H}$}'$ of  formulas, for all the node-labels $\mathcal{S}\!,\mbox{$\mathcal{H}$}' \Vvdash (b',\varphi')$
    in  the tree $\Theta$. The set $\mbox{$\mathsf{Con}$}$  is the set of all  formulas  $(b',\varphi')$, for all the node-labels $\mathcal{S}\!,\mbox{$\mathcal{H}$}' \Vvdash (b',\varphi')$ occuring in~$\Theta$.
  \end{definition}
Hereafter in the currenct subsection about soundness we assume a proof (tree) $\Theta$ of $\mathcal{S}\!,\mbox{$\mathcal{H}$} \Vvdash (b,\varphi)$ with corresponding sets $\mbox{$\mathsf{Hyp}$}$ and $\mbox{$\mathsf{Con}$}$.
The following technical lemma is  proved by structural induction on such trees. It says that tagged fomulas in  $\mbox{$\mathsf{Hyp}$}$ are  among the
hypotheses  $\mbox{$\mathcal{H}$}$ present at the root of  $\Theta$, plus the conclusions $\mbox{$\mathsf{Con}$}$, and, except perhaps
for those in $\mbox{$\mathcal{H}$}$, the formulas in $\mbox{$\mathsf{Hyp}$}$ are tagged with
  $\mbox{\textsc{f}}$.

  \begin{lemma}
    \label{lem:aux}
    $\mbox{$\mathsf{Hyp}$} \subseteq  \mbox{$\mathcal{H}$} \cup \mbox{$\mathsf{Con}$}$, and,  if $(b', \varphi') \in \mbox{$\mathsf{Hyp}$} \setminus \mbox{$\mathcal{H}$}$, then $b' = \mbox{\textsc{f}}$.
  \end{lemma}

  Some  more notions need to be defined.
First, a \emph{pad} in a tree  is a sequence of consecutive edges, and the length of a pad is the number of nodes on the pad. Hence, the length of a pad is strictly positive.
  \begin{definition}
    The \emph{last occurence of a tagged formula $(b',\varphi') \in \mbox{$\mathsf{Con}$}$ in $\Theta$ } is the maximal length of a pad from the root $\mathcal{S}\!,\mbox{$\mathcal{H}$} \Vvdash (b,\varphi)$ of $\Theta$ to some node labelled by $\mathcal{S}, \mbox{$\mathcal{H}$}' \Vvdash (b',\varphi')$. For formulas  $(b',\varphi') \notin \mbox{$\mathsf{Con}$}$ we define by convention their last occurence in $\Theta$ to be $0$. This defines a total function $\mbox{$\mathit{last}$} : \mathbb{B} \times  \Phi \to \mathbb{N}$.
  \end{definition}
  Let also $\mbox{$\mathit{fPaths}$}$ denote the set of finite paths of the transition system under consideration.
  We now define the set $\mbox{$\mathcal{D}$} \;\mbox{$\triangleq$}\; \{(\tau',b',\varphi') \in  \mbox{$\mathit{fPaths}$} \times \mathbb{B} \times \Phi \mid (\mathit{lhs}\, \varphi')(\mbox{$\mathit{hd}$}\, \tau') \wedge (b',\varphi') \in \mbox{$\mathsf{Con}$}\}$ on which we shall reason by well-founded induction.
  We equip $\mbox{$\mathcal{D}$}$ with a well-founded order, namely, with the restriction to $\mbox{$\mathcal{D}$}$ of the lexicographic-product order on $\mbox{$\mathit{fPaths}$} \times \mathbb{B} \times \Phi$  defined by $(\tau_1,b_1,\varphi_1) \prec (\tau_2,b_2,\varphi_2) $ iff

  \begin{enumerate}
 \item   $\mbox{$\mathit{len}$}\, \tau_1 < \mbox{$\mathit{len}$},\tau_2$, or
 \item $\mbox{$\mathit{len}$}\, \tau_1 = \mbox{$\mathit{len}$},\tau_2$ and $b_1 < b_2$, with $<$ on Booleans is defined by $\mbox{\textsc{f}} < \mbox{\textsc{t}}$, or
 \item  $\mbox{$\mathit{len}$}\, \tau_1 = \mbox{$\mathit{len}$},\tau_2$ and $b_1 = b_2$, and $\mbox{$\mathit{last}$}(b_1,\varphi_1) > \mbox{$\mathit{last}$}(b_2,\varphi_2)$.
   \end{enumerate}
  The first two orders in the product, on natural numbers and on Booleans, are well-founded. For the third one, since the order $\prec$ on $\mbox{$\mathit{fPaths}$} \times \mathbb{B} \times \Phi$ is restricted to $\mbox{$\mathcal{D}$}$,
  all  last occurences are bounded by the height of $\Theta$, ensuring that the inequality  $\mbox{$\mathit{last}$}(b_1,\varphi_1) > \mbox{$\mathit{last}$}(b_2,\varphi_2)$ induces a well-founded order.  Hence, the restriction of $\prec$  on $\mbox{$\mathcal{D}$}$ (also denoted by $\prec$) is a well-founded order as well. The following lemma uses this.

 \begin{lemma}
   \label{lem:key}
   Assume $\mathcal{S}\!,\mbox{$\mathcal{H}$} \Vvdash (\mbox{\textsc{f}}, l \mbox{$\mathit{\,\Rightarrow\!\!\!\Diamond}\,$} r)$ and  for all $(b',\varphi')\in \mbox{$\mathcal{H}$}$, $b' = \mbox{\textsc{f}}$ and $\mathcal{S}\models \varphi'$.
   Let $\mbox{$\mathcal{D}$}$ be the domain corresponding to $\mathcal{S}\!,\mbox{$\mathcal{H}$} \Vvdash (\mbox{\textsc{f}}, l \mbox{$\mathit{\,\Rightarrow\!\!\!\Diamond}\,$} r)$.
   Then, for all $(\tau,b,\varphi) \in \mbox{$\mathcal{D}$}$,  there is
   $k \leq \mbox{$\mathit{len}$}\, \tau$ such that $(\mathit{rhs}\, \varphi)\, (\tau\,  k)$.
 \end{lemma}

 As a corollary to Lemma~\ref{lem:key} we obtain:

 \begin{theorem}[Soundness of $\Vvdash$]
    \label{th:soundp32}
  If for all $(b',\varphi') \in \mbox{$\mathcal{H}$}$, $b' = \mbox{\textsc{f}}$ and $\mathcal{S} \models \varphi'$, then $\mathcal{S}\!,\mbox{$\mathcal{H}$} \Vvdash (\mbox{\textsc{f}},\varphi)$ implies $\mathcal{S}\models \varphi$.
 \end{theorem}

 \paragraph*{Completeness.} Proving the completeness of $\Vvdash$ is the same as for the other proof system: prove a lemma reducing reachability to an invariance property and then show that for valid formulas that property holds.

 \begin{lemma}
     \label{lem:redtoinv3}
If $l \sqsubseteq q \sqcup r$, $q \sqcap \bullet \sqsubseteq \bot$, and $\mbox{$\mathit{\partial}$} q \sqsubseteq q \sqcup r$ then $\mathcal{S}\Vvdash  (\mbox{\textsc{f}}, l \mbox{$\mathit{\,\Rightarrow\!\!\!\Diamond}\,$} r)$.
 \end{lemma}
 \begin{proof}
   We build a proof (tree) for $\mathcal{S}\Vvdash (\mbox{\textsc{f}}, l \mbox{$\mathit{\,\Rightarrow\!\!\!\Diamond}\,$} r)$. The root of the  tree is a node $N_0$ labelled $\mathcal{S}\Vvdash  (\mbox{\textsc{f}}, l\mbox{$\mathit{\,\Rightarrow\!\!\!\Diamond}\,$} r)$.
   $N_0$  has one successor $N_1$, generated by the \textsf{[Str]} rule, thanks to the hypothesis $l \sqsubseteq q \sqcup r$, and labelled
   $\mathcal{S}\Vvdash  (\mbox{\textsc{f}}, (q \sqcup r)\mbox{$\mathit{\,\Rightarrow\!\!\!\Diamond}\,$} r)$. $N_1$ has two successors $N_{2,1}$ and $N_{2,2}$, generated by the \textsf{[Spl]} rule, and labelled
   $\mathcal{S}\Vvdash  (\mbox{\textsc{f}}, q \mbox{$\mathit{\,\Rightarrow\!\!\!\Diamond}\,$} r)$ and $\mathcal{S}\Vvdash  (\mbox{\textsc{f}}, r \mbox{$\mathit{\,\Rightarrow\!\!\!\Diamond}\,$} r)$, respectively.
Usinng the \textsf{[Trv]} rule, $N_{2,2}$  has no succesors.
    $N_{2,1}$ has one successor $N_3$, generated by the \textsf{[Cof]} rule, labelled
   $\mathcal{S}\!, \{   (\mbox{\textsc{f}}, q \mbox{$\mathit{\,\Rightarrow\!\!\!\Diamond}\,$} r) \} \Vvdash  (\mbox{\textsc{f}}, q \mbox{$\mathit{\,\Rightarrow\!\!\!\Diamond}\,$} r)$. $N_3$ has one successor
   $N_4$, generated by the
   \textsf{[Stp]} rule, thanks to the hypothesis  $q \sqcap \bullet \sqsubseteq \bot$, and labelled
   $\mathcal{S}\!, \{   (\mbox{\textsc{f}}, q \mbox{$\mathit{\,\Rightarrow\!\!\!\Diamond}\,$} r) \} \Vvdash  (\mbox{\textsc{t}}, \mbox{$\mathit{\partial}$} q \mbox{$\mathit{\,\Rightarrow\!\!\!\Diamond}\,$} r)$. Note that the Boolean has switched from
   \mbox{\textsc{f}}\ to \mbox{\textsc{t}}, which enables us to later use  the \textsf{[Hyp]} rule. The node $N_4$ has one successor,
   generated by the \textsf{[Str]} rule thanks to the hypothesis $\mbox{$\mathit{\partial}$} q \sqsubseteq q \sqcup r$:
   $\mathcal{S}\!, \{   (\mbox{\textsc{f}}, q \mbox{$\mathit{\,\Rightarrow\!\!\!\Diamond}\,$} r) \} \Vvdash  (\mbox{\textsc{t}},  (q \sqcup r) \mbox{$\mathit{\,\Rightarrow\!\!\!\Diamond}\,$} r)$. $N_4$ has two successors $N_{5,1}$ and  $N_{5,2}$, labelled
    $\mathcal{S}\!, \{   (\mbox{\textsc{f}}, q \mbox{$\mathit{\,\Rightarrow\!\!\!\Diamond}\,$} r) \} \Vvdash  (\mbox{\textsc{t}}, q \mbox{$\mathit{\,\Rightarrow\!\!\!\Diamond}\,$} r)$ and  $\mathcal{S}\!, \{   (\mbox{\textsc{f}}, q \mbox{$\mathit{\,\Rightarrow\!\!\!\Diamond}\,$} r) \} \Vvdash  (\mbox{\textsc{t}}, r \mbox{$\mathit{\,\Rightarrow\!\!\!\Diamond}\,$} r)$, respectively. Neither has any successor: $N_{5,1}$, by the \textsf{[Hyp]} rule, and $N_{5,2}$, by the $\textsf{[Trv]}$ rule.
 \end{proof}

 By  analogy with Theorems~\ref{th:completeness} and \ref{th:completeness2}  but using Lemma~\ref{lem:redtoinv3} (instead of
\ref{lem:redtoinv} and~\ref{lem:redtoinv2}, respectively) :

\begin{theorem}[Completeness of $\Vvdash$]
    \label{th:completeness3}
   $\mathcal{S} \models \varphi$ implies $\mathcal{S}\Vvdash \varphi$.
  \end{theorem}

  \paragraph*{Compositionality w.r.t. Formulas} $\Vvdash$ has a symmetrical version of   compositionality w.r.t.\ formulas:
  \begin{theorem}
    \label{lem:compform}
    $\mathcal{S}\!, \mbox{$\mathcal{H}$} \cup \{ (\mbox{\textsc{f}},\varphi_1)\} \Vvdash (\mbox{\textsc{f}}, \varphi_2)$ and  $\mathcal{S}\!, \mbox{$\mathcal{H}$} \cup \{ (\mbox{\textsc{f}},\varphi_2)\} \Vvdash (\mbox{\textsc{f}},\varphi_1)$
    imply  $\mathcal{S}\!, \mbox{$\mathcal{H}$}  \Vvdash (\mbox{\textsc{f}}, \varphi_1)$ and  $\mathcal{S}\!, \mbox{$\mathcal{H}$}  \Vvdash (\mbox{\textsc{f}},\varphi_2)$.
  \end{theorem}
  \begin{proof}
    The statement is symmetrical in $\varphi_1, \varphi_2$; we prove it for the first formula. The rule\textsf{[Cof]}
    generates one successor for the root $N_0$ labelled $\mathcal{S}\!, \mbox{$\mathcal{H}$}  \Vvdash (\mbox{\textsc{f}}, \varphi_1)$:
  $N_1$, labelled   $\mathcal{S}\!, \mbox{$\mathcal{H}$} \cup \{ (\mbox{\textsc{f}},\varphi_1)\} \Vvdash (\mbox{\textsc{f}}, \varphi_1)$. From $N_1$, the rule \textsf{[Cut]}
    generates two successors, $N_{2,1}$ labelled $\mathcal{S}\!, \mbox{$\mathcal{H}$} \cup \{ (\mbox{\textsc{f}},\varphi_1)\} \Vvdash (\mbox{\textsc{f}}, \varphi_2)$, which we assumed as a hypothesis,
    and $N_{2,2}$, labelled $\mathcal{S}\!, \mbox{$\mathcal{H}$} \cup \{ (\mbox{\textsc{f}},\varphi_1), (\mbox{\textsc{f}},\varphi_2)\} \Vvdash (\mbox{\textsc{f}}, \varphi_1)$. From $N_{2,2}$ the rule \textsf{[Clr]}
    removes the first hypothesis and generates a node labelled $\mathcal{S}\!, \mbox{$\mathcal{H}$} \cup \{ (\mbox{\textsc{f}},\varphi_2)\} \Vvdash (\mbox{\textsc{f}}, \varphi_1)$, which we assumed as a hypothesis as well.
  \end{proof}

  \begin{example}
    \label{ex:asymcompps3}
    In Example~\ref{ex:astra} we tried to prove $\mathcal{S} \models (c = c_0)\mbox{$\mathit{\,\Rightarrow\!\!\!\Diamond}\,$} (c =c_2 \wedge s =  m\times (m+1)/2)$ using the asymmetrical compositionality of $\Vdash$, and noted that a certain
    proof step was impossible because of the asymmetry of the \textsf{[Tra]} rule of $\Vdash$.
    We show that $\Vvdash$ does not suffer from the same issue. The problem, reformulated in terms of $\Vvdash$, was to start the sequent
  (iii')  $\mathcal{S},\{(\mbox{\textsc{f}},(c = c_0) \mbox{$\mathit{\,\Rightarrow\!\!\!\Diamond}\,$} (c = c_1 \wedge i = 0 \wedge s = 0))\} \Vdash  (\mbox{\textsc{f}}, (c = c_0)\mbox{$\mathit{\,\Rightarrow\!\!\!\Diamond}\,$} (c =c_2 \wedge s =  m\times (m+1)/2))$ and  to use  the  \textsf{[Tra]} rule
  in order to  split this sequent in two:  $\mathcal{S},\{(\mbox{\textsc{f}},(c = c_0) \mbox{$\mathit{\,\Rightarrow\!\!\!\Diamond}\,$} (c = c_1 \wedge i = 0 \wedge s = 0))\} \Vdash (\mbox{\textsc{f}}, (c = c_0)\mbox{$\mathit{\,\Rightarrow\!\!\!\Diamond}\,$} (c = c_1 \wedge i = 0 \wedge s = 0))$ and
   then $\mathcal{S},\{(\mbox{\textsc{f}},(c = c_0) \mbox{$\mathit{\,\Rightarrow\!\!\!\Diamond}\,$} (c = c_1 \wedge i = 0 \wedge s = 0))\} \Vdash (\mbox{\textsc{f}}, (c = c_1  \wedge i = 0 \wedge s = 0)\mbox{$\mathit{\,\Rightarrow\!\!\!\Diamond}\,$}  \mbox{$\mathit{\,\Rightarrow\!\!\!\Diamond}\,$} (c = c_1 \wedge i = 0 \wedge s = 0))$. This inference step, which we have just performed above, was not a problem for the $\Vvdash$ proof system.
 \end{example}

Finally, we show how to combine compositionality w.r.t. transition systems and w.r.t. formulas.
  The following lemma says that $\Vvdash$ is compositional w.r.t.
  transition systems even in the presence of hypotheses.

  \begin{lemma}
    \label{lem:compts}
    If $ \mathcal{S}'\!, \mbox{$\mathcal{H}$}  \Vvdash (b,\varphi)$ and  $\mathcal{S}' \leftslice \mathcal{S}$ then
    $ \mathcal{S}\!, \mbox{$\mathcal{H}$} \Vvdash (b,\varphi)$.
  \end{lemma}

  Combining Theorem~\ref{lem:compform} and Lemma~\ref{lem:compts} we obtain as a corollary the following theorem, which combines symmetrical compositionality w.r.t. formulas and compositionality w.r.t. transition systems.

  \begin{theorem}
    \label{th:compps3}
    If, for $i  \in \{0, 1\}$, $\mathcal{S}_i \leftslice \mathcal{S}$  and
    $\mathcal{S}_i, \mbox{$\mathcal{H}$} \cup\{(\mbox{\textsc{f}}, \varphi_{1-i})\} \Vvdash (\mbox{\textsc{f}},\varphi_i)$,  then,  for $i  \in \{0, 1\}$, $\mathcal{S}\!, \mbox{$\mathcal{H}$} \Vvdash (\mbox{\textsc{f}},\varphi_i)$.
  \end{theorem}

\begin{example}
    \label{ex:gcd}
    We sketch the verification of another infinite-state transition system, denoted by the
    state machine in Figure~\ref{fig:gcd}, which computes the greatest common divisor of two strictly positive natural numbers. The obtained proof is not, by far, the simplest; for such simple systems a global (non-compositional) proof is much shorter. Our goal here is to use all the  compositionality features of $\Vvdash$ embodied in Theorem~\ref{th:compps3}.

\begin{figure}[t]
\begin{center}
  \begin{tikzpicture}
\node[state] (c0) {$c_0$};
\node[state, right of=c0] (c1) {$c_1$};
\node[state,right  of=c1] (c2) {$c_2$};

\path[->] (c0) edge [above] node[yshift= -10mm]{ \small  $\begin{array}{l} x_0> 0 \wedge \\ y_0 > 0   \\ x := x_0 \\ y := y_0 \end{array}$} (c1);
\path[->] (c1) edge [loop above] node[yshift=-1mm,  xshift=2mm]{\small  $\begin{array}{l} x < y \\ y := y - x \end{array}$} ();
\path[->] (c1) edge  [loop below] node[yshift=1mm, xshift=2mm] {\small  $\begin{array}{l} y < x \\ x := x - y \end{array}$} ();
\path[->] (c1) edge [above] node[yshift=-1mm]{\small  $x = y$} (c2);
 \end{tikzpicture}
\end{center}
\caption{\label{fig:gcd} Computing a greatest common divisor}
 \end{figure}

The state machine has three control nodes and operates with four natural-number variables: $x$, $y$, $x_0$ and $y_0$. The last two variables are ``symbolic constants'', not modified by the transitions of the state machine, whose greatest-common divisor the machine is supposed to compute. On the leftmost transition $x$ and $y$ are initialised to $x_0$ and $y_0$, provided that
the guard $x_0 > 0 \wedge y_0> 0$ holds. On the upper self-loop arrow, $x$ is substracted from $y$ provided the guard $x < y$ holds. The lower self-loop arrow inverses the roles of $x$ and $y$. The rightmost arrow is taken provided its guard
$x = y$ holds.  The state-machine denotes an infinite-state transition system $\mathcal{S}$ with state-set
$\{c_0, c_1, c_2\} \times \mathbb{N}^{4}$  and transition relation
{\small
$\bigcup_{x,y,x_0,y_0 \in \mathbb{N}, x_0 > 0, y_0 > 0}\{((c_0,x,y,x_0,y_0), (c_1, x_0,y_0,x_0, y_0))\} \cup$
$\bigcup_{x,y,x_0, y_0 \in \mathbb{N}, x < y} \{((c_1,x,y,x_0,y_0), (c_1,x,y-x,x_0,y_0))\} \cup$
$\bigcup_{x,y,x_0,y_0 \in \mathbb{N}, y < x}  \{((c_1,x,y,x_0,y_0), (c_1, x-y,y,x_0,y_0))\} \cup$
$\bigcup_{x,y,x_0,y_0 \in \mathbb{N}, x = y}\{((c_1,x,y,x_0,y_0), (c_2, x,y,x_0, y_0))\}$.
}

We identify two components of this transition system: $\mathcal{S}_1$, encoded by the upper self-loop and rightmost arrow, and
$\mathcal{S}_2$, encoded by the lower self-loop and rightmost arrow. Their state-spaces are both $\{c_1, c_2\} \times \mathbb{N}^{4}$.
Their  transition relations are $\bigcup_{x,y,x_0, y_0 \in \mathbb{N}, x < y} \{((c_1,x,y,x_0,y_0), (c_1,x,y-x,x_0,y_0))\} \cup$
$\bigcup_{x,y,x_0,y_0 \in \mathbb{N}, x = y}\{((c_1,x,y,x_0,y_0), (c_2, x,y,x_0, y_0))\}$ and
$\bigcup_{x,y,x_0,y_0 \in \mathbb{N}, y < x}  \{((c_1,x,y,x_0,y_0), (c_1, x-y,y,x_0,y_0))\} \cup$
$\bigcup_{x,y,x_0,y_0 \in \mathbb{N}, x = y}\{((c_1,x,y,x_0,y_0), (c_2, x,y,x_0, y_0))\}$,  induced by their respective arrow subsets.
We will show

\smallskip

(1) $\mathcal{S} \models (c = c_0 \wedge x_0 > 0 \wedge y_0 > 0) \mbox{$\mathit{\,\Rightarrow\!\!\!\Diamond}\,$} (c =c_2 \wedge x = y \wedge x =\mathit{gcd}(x_0,y_0))$.

\smallskip \noindent
which is the functional correctness of the system. Using the soundness of $\Vvdash$ then the $\textsf{[Tra]}$ rule, the latter reduces to (2) $\mathcal{S} \Vvdash (\mbox{\textsc{f}},(c = c_0 \wedge x_0 > 0 \wedge y_0 > 0) \mbox{$\mathit{\,\Rightarrow\!\!\!\Diamond}\,$} (c =c_1 \wedge x = y_0 \wedge y = y_0 \wedge x_0 > 0 \wedge y_0 > 0))$ and
(3) $\mathcal{S} \Vvdash (\mbox{\textsc{f}},(c = c_1 \wedge x = y_0 \wedge y = y_0 \wedge x_0 > 0 \wedge y_0 > 0) \mbox{$\mathit{\,\Rightarrow\!\!\!\Diamond}\,$} (c =c_2 \wedge  x = y \wedge x =\mathit{gcd}(x_0,y_0)))$. Now, (2) is  discharged by the sequence of rules~\textsf{[Stp]}, \textsf{[Str]} and \textsf{[Trv]}, thus, we focus on (3).
Using several times
\textsf{[Str]} and \textsf{[Spl]}, and also ($x = x_0 \wedge y = y_0) \sqsubseteq  (\mathit{gcd}(x,y)  = \mathit{gcd}(x_0,y_0))$, (3) reduces to proving the   subgoals

(4) :  $\mathcal{S} \Vvdash (\mbox{\textsc{f}},(c_1, \mathit{gcd}(x,y)  = \mathit{gcd}(x_0,y_0) \wedge x_0 > 0 \wedge y_0 > 0 \wedge x < y ) \mbox{$\mathit{\,\Rightarrow\!\!\!\Diamond}\,$} (c = c_2 \wedge x = y \wedge x =\mathit{gcd}(x_0,y_0)))$;

(5) : $\mathcal{S} \Vvdash (\mbox{\textsc{f}},(c_1,  \mathit{gcd}(x,y)  = \mathit{gcd}(x_0,y_0) \wedge x_0 > 0 \wedge y_0 > 0 \wedge x = y) \mbox{$\mathit{\,\Rightarrow\!\!\!\Diamond}\,$} (c = c_2 \wedge x = y \wedge x =\mathit{gcd}(x_0,y_0)))$;

(6) : $\mathcal{S} \Vvdash (\mbox{\textsc{f}},(c_1,  \mathit{gcd}(x,y)  = \mathit{gcd}(x_0,y_0) \wedge x_0 > 0 \wedge y_0 > 0 \wedge y < x) \mbox{$\mathit{\,\Rightarrow\!\!\!\Diamond}\,$} (c = c_2 \wedge x = y \wedge x =\mathit{gcd}(x_0,y_0)))$.

\noindent The subgoal (5) is immediately discharged by applying the sequence of rules~\textsf{[Stp]}, \textsf{[Str]} and \textsf{[Trv]}.

The two other ones we  prove by reducing them, thanks to Theorem~\ref{th:compps3} to the two following subgoals, with
 $\varphi_1 \; \mbox{$\triangleq$} \; (c = c_1\wedge \mathit{gcd}(x,y)  = \mathit{gcd}(x_0,y_0) \wedge x_0 > 0 \wedge y_0 > 0 \wedge x < y) \mbox{$\mathit{\,\Rightarrow\!\!\!\Diamond}\,$} (c = c_2 \wedge x = y \wedge x =\mathit{gcd}(x_0,y_0))$ and
$\varphi_2 \; \mbox{$\triangleq$} \; (c = c_1\wedge \mathit{gcd}(x,y)  = \mathit{gcd}(x_0,y_0) \wedge x_0 > 0 \wedge y_0 > 0 \wedge y < x) \mbox{$\mathit{\,\Rightarrow\!\!\!\Diamond}\,$} (c = c_2 \wedge x = y \wedge x =\mathit{gcd}(x_0,y_0))$:

 (7) : $\mathcal{S}_1, \{(\mbox{\textsc{f}}, \varphi_2)\} \Vvdash (\mbox{\textsc{f}}, \varphi_1)$ and (8) : $\mathcal{S}_2, \{(\mbox{\textsc{f}}, \varphi_1)\} \Vvdash (\mbox{\textsc{f}}, \varphi_2)$. We prove (7), the proof of (8) is similar. Using \textsf{[Tra]}, (7) reduces to (9) :
$\mathcal{S}_1, \{(\mbox{\textsc{f}}, \varphi_2)\} \Vvdash (\mbox{\textsc{f}},  (\phi \wedge x < y) \mbox{$\mathit{\,\Rightarrow\!\!\!\Diamond}\,$} (\phi \wedge y \leq x)))$ and (10) :
$\mathcal{S}_1, \{(\mbox{\textsc{f}}, \varphi_2)\} \Vvdash  (\mbox{\textsc{f}}, (\phi \wedge y \leq x) \mbox{$\mathit{\,\Rightarrow\!\!\!\Diamond}\,$} (c = c_2 \wedge x = y \wedge x =\mathit{gcd}(x_0,y_0)))$ where $\phi \; \mbox{$\triangleq$} \; (c= c_1 \wedge \mathit{gcd}(x,y)  = \mathit{gcd}(x_0,y_0) \wedge x_0 > 0 \wedge y_0 > 0)$.

The  subgoal (9) is  proved after simplification by \textsf{[Clr]} using Lemma~\ref{lem:redtoinv3} with $q \; \mbox{$\triangleq$} \;  (\phi \wedge x < y) $.

For the subgoal (10), it is first decomposed using \textsf{[Str]} then  \textsf{[Spl]} into (11) :
$\mathcal{S}_1, \{(\mbox{\textsc{f}}, \varphi_2)\} \Vvdash  (\mbox{\textsc{f}}, (\phi \wedge y = x) \mbox{$\mathit{\,\Rightarrow\!\!\!\Diamond}\,$} (c = c_2 \wedge x = y \wedge x =\mathit{gcd}(x_0,y_0)))$ -  which is easily discharged by  \textsf{[Stp]}, \textsf{[Str]} then  \textsf{[Trv]} -  and

(12) : $\mathcal{S}_1, \{(\mbox{\textsc{f}}, \varphi_2)\} \Vvdash  (\mbox{\textsc{f}}, (\phi \wedge y < x) \mbox{$\mathit{\,\Rightarrow\!\!\!\Diamond}\,$} (c = c_2 \wedge x = y \wedge x =\mathit{gcd}(x_0,y_0)))$. Using \textsf{[Cof]},  (12) becomes

(13) : $\mathcal{S}_1, \{(\mbox{\textsc{f}}, \varphi_2), (\mbox{\textsc{f}}, (\phi \wedge y < x) \mbox{$\mathit{\,\Rightarrow\!\!\!\Diamond}\,$} \psi)\} \Vvdash  (\mbox{\textsc{f}}, (\phi \wedge y < x) \mbox{$\mathit{\,\Rightarrow\!\!\!\Diamond}\,$} \psi)$ with $\psi \mbox{$\triangleq$} (c = c_2 \wedge x = y \wedge x =\mathit{gcd}(x_0,y_0))$.

\noindent We now apply \textsf{[Stp]} followed by \textsf{[Str]} to (13) and get (14) :  $\mathcal{S}_1, \{(\mbox{\textsc{f}}, \varphi_2), (\mbox{\textsc{f}}, (\phi \wedge y < x) \mbox{$\mathit{\,\Rightarrow\!\!\!\Diamond}\,$} \psi)\} \Vvdash  (\mbox{\textsc{t}}, \phi\mbox{$\mathit{\,\Rightarrow\!\!\!\Diamond}\,$} \psi)$.

After several applications of \textsf{[Str]} and  \textsf{[Spl]}
(14) is reduced to proving the three last following subgoals:

(15) :  $\mathcal{S}_1, \{(\mbox{\textsc{f}}, \varphi_2), (\mbox{\textsc{f}}, (\phi \wedge y < x) \mbox{$\mathit{\,\Rightarrow\!\!\!\Diamond}\,$} \psi)\} \Vvdash  (\mbox{\textsc{t}},( \phi \wedge y < x)\mbox{$\mathit{\,\Rightarrow\!\!\!\Diamond}\,$} \psi)$, discharged using \textsf{[Hyp]};

(16) :  $\mathcal{S}_1, \{(\mbox{\textsc{f}}, \varphi_2), (\mbox{\textsc{f}}, (\phi \wedge y = x) \mbox{$\mathit{\,\Rightarrow\!\!\!\Diamond}\,$} \psi)\} \Vvdash  (\mbox{\textsc{t}},( \phi \wedge y < x)\mbox{$\mathit{\,\Rightarrow\!\!\!\Diamond}\,$} \psi)$, discharged using \textsf{[Stp]}, \textsf{[Str]}, and \textsf{[Trv]};

(17) : $\mathcal{S}_1, \{(\mbox{\textsc{f}}, \varphi_2), (\mbox{\textsc{f}}, (\phi \wedge x < y) \mbox{$\mathit{\,\Rightarrow\!\!\!\Diamond}\,$} \psi)\} \Vvdash  (\mbox{\textsc{t}},( \phi \wedge y < x)\mbox{$\mathit{\,\Rightarrow\!\!\!\Diamond}\,$} \psi)$, discharged using \textsf{[Hyp]} by noting that $\varphi_2$ is $( \phi \wedge y < x)\mbox{$\mathit{\,\Rightarrow\!\!\!\Diamond}\,$} \psi$. All the subgoals have been  discharged, and the proof of (1) is complete.

  \end{example}

 \section{Implementations in Isabelle/HOL and Coq}
 We have implemented all the proof systems in Coq and (currently) the first two ones in Isabelle/HOL as well. Our initial goal was to use only Coq, and the reason we also tried Isabelle/HOL (learning it in the process) was that we wanted a ``second opinion'' when faced with difficulties using Coq's coinduction.

 The Isabelle/HOL implementation for proof systems $\vdash$ and $\Vdash $is essentially the same as the one described in the paper. The tool automatically generates and proves
 induction and coinduction principles from inductive and coinductive datatypes or predicates.
 Proof commands \texttt{induction} resp. \texttt{coinduction} apply an induction (resp., a coinduction principle) by instantiating the predicate therein via unification with the conclusion, possibly generalised by universally quantifying some variables, (resp., with a conjunction of hypotheses, possibly generalised by existentially quantifying some variables). The overall level of automation is high, which is pleasant to use in practice, the only down side being that users might not understand what is going on. Overall, the proofs in this paper are sketches of the formal Isabelle/HOL proofs, which we did with a lower automation level in order to be able to understand and describe them.

 The Coq implementation for the proof systems $\vdash$ and $\Vdash $ is rather different from the above, because support for coinduction in Coq is also rather different. The standard way to perform a proof by coinduction in Coq is to use the  \texttt{cofix} tactic, which (like the \textsf{[Cof]} rule in our third proof system that emulates it), copies the current goal's conclusion as a new hypothesis, which can only be used after appropriate ``progress'' has been made in the interactive proof. A proof by coinduction in Coq is ultimately
 a well-formed corecursive function, where well-formedness is defined as a  syntactical guardedness condition, which is quite complex  in the theory~\cite{DBLP:conf/types/Gimenez94}, and even more so in the implementation.
 We have nonetheless managed to prove the soundness and completeness of $\vdash$ using this tactic:
 \textsf{cofix}-style proofs of soundness and completeness for $\vdash$, described in standard mathematical notation,
   are reported in~\cite{rusu:hal-01962912}.
   For $\Vdash$, however, \textsf{cofix} became useless because, for some reason,
   it does not accept to be mixed in a proof by induction. Fortunately, there is a better version, \texttt{pcofix}, part of a
   Coq package called Paco, based on an extenstion of Knaster-Tarski coinduction called \emph{parameterised}
   coinduction~\cite{DBLP:conf/popl/HurNDV13}. Even though the theory is an extension of Knaster-Tarski, anything related to
   fixpoints of functionals is hidden from the user; a set of tactics, including \textsf{pcofix}, leaves the user with the impression that they are using \textsf{cofix} but without its issues.

   The soundness proof of $\Vvdash$, only in Coq for now, generally follows the lines shown in this paper.
   It is also completely different from the corresponding proofs for the two other proof systems: it does not use general (co)induction principles, but one well-founded induction principle specific to our problem.

\section{Conclusions and Future Work}
We have presented three proof systems for Reachability Logic on Transition Systems, which use coinduction and induction in different proportions. We have proved their soundness and completeness, and have noted that the more inductive a proof system is, and the more specialised its coinduction style is with respect to our problem domain, the more compositional  the proof system is, but the harder its soundness proof.
Mechanisations of the proof systems in Isabelle/HOL and Coq have also been briefly presented.

In future work we shall make the formal proof of compositionality with respect to transition systems; and prove the third proof system (currently only proved in Coq) in Isabelle/HOL. We are also planning to port Knaster-Tarski coinduction to Coq, and redo the proofs in this paper in that style, in order to obtain Coq proofs closer in spirit to those in the paper and in Isabelle/HOL. A medium-term project is to use the most compositional proof system, among the three proposed ones, for verifying monadic code, a sizeable amount of which is available to us from earlier projects; and, in the longer term, to enrich our proof system with assume-guarantee-style compositional reasoning related to parallel composition.

 \paragraph*{Acknowledgment.}
\hspace*{-0.4cm}  We would like to thank Andrei Popescu for his help with coinduction in Isabelle/HOL.
We acknowledge the support of the CNRS-JSPS Joint Research Project ``FoRmal tools for IoT sEcurity'' (PRC2199), and thank all the participants of this project for fruitful discussions.

\bibliographystyle{eptcs}

redpajama_set_name: RedPajamaArXiv


text:
Ohio Soccer Announces 2014 Schedule
Posted on: Monday, May 5, 2014
The Ohio soccer team announced its schedule for the 2014 season on Monday, with eight nonconference games and 11 games against Mid-American Conference opponents.
The Bobcats' nonconference schedule includes a tournament at West Lafayette, Ind., where they'll take on Butler and Purdue, and games against Wright State and Kentucky. Head coach Aaron Rodgers came to Ohio last year after being an assistant coach for the University of Kentucky for four seasons.
"Our pre-conference schedule will really test us as a group and really prepare us for what is always an extremely competitive Mid-American Conference," Rodgers told OhioBobcats.com.
Ohio went 4-3-2 in nonconference games last season. It opens the season with a home exhibition game against UNC Greensboro, who the Bobcats tied 0-0 in last year's exhibition.
They finish their nonconference schedule with three home games against Xavier, Eastern Kentucky and Detroit, and then a one-game road trip to Dayton.
Ohio begins its conference schedule with two home contests against Akron (Sept. 26) and Buffalo (Sept. 28). Six of the 11 conference games will be played at home, with notable games coming against rival Miami on Oct. 12 and Kent State on Oct. 30.
Ohio travels to defending MAC champs Western Michigan on Oct. 3, and it takes on Eastern Michigan in Ypsilanti, Mich., on Oct. 19. The Eagles eliminated Ohio in the first round of the MAC Tournament last season.
If the Bobcats finish in the top eight of the conference, they will participate in the MAC Tournament, which starts on Nov. 2 with the quarterfinals. The winner of the MAC Tournament will advance to the 2014 NCAA Tournament, which starts on Nov. 14.
Ohio Soccer Releases 2013 Schedule Ohio Softball Announces 2014 Schedule 2014 MAC Schedule Set For Ohio Ohio Announces 2014 Mid-American Conference Slate

redpajama_set_name: RedPajamaCommonCrawl


Empower your operators to manage their tasks and to start and end paperless work orders. Give planners/managers a complete overview of your production orders.
The planners/managers cockpit provides a complete overview of your production orders and their progress. While the operators cockpit offers a visually intuitive overview of ongoing and incoming orders with prioritisation.
You can introduce paperless and accurate communication between departments, collect data, report Q&A activities, variable MAT issues register time & attendance and allocate serial and lot number tracking.
Many of our customers have reported a reduction in lead-time, reduced operating costs, and reduction of administrative time as a result of implementing ShopFloor.
ShopFloor is a module for Microsoft Dynamics NAV which can be implemented in few hours. The module does not make any changes to your standard NAV solution.
ShopFloor is a dual cockpit system for the planners/managers and the operators in the workshop. The cockpit for the planners provides a complete overview of your production orders and their progress. The windows based cockpit for the operators offers a visually intuitive overview of ongoing and incoming orders with prioritisation. From the cockpit, the operator can start and end the orders via the use of our intuitive action buttons.
With ShopFloor, you can introduce paperless and accurate communication between departments, collect data, report Q&A activities, variable MAT issues register time & attendance and allocate serial and lot number tracking. Many of our customers have reported a reduction in lead-time, reduced operating costs, and reduction of administrative time as a result of implementing ShopFloor.
Single screen cockpit with real-time information.
Operator function for full traceability and serial number control.
Automatic collection of data for cost calculations, etc.
ShopFloor can be implemented in a few hours (plug and play). The module does not make any changes to your standard MS Dynamics NAV solution.
For more information on how NAVEKSA ShopFloor could benefit your company fill out the enquiry form or contact us on 02 9672 4222 for a FREE no obligation chat.


The PGA of Alberta is proud to present the largest Buying Show in Canada each year in Edmonton, Alberta. The purpose of this show is to bring Golf Professionals and Equipment Manufacturers together, so as to prepare their inventories for the following season. Over the course of three days, close to 1,200 people gather from across the country and around the world, for a look at what's new and exciting in the golf industry.


text:
Sokolow Has Book Launch Puretz Publishes New Novel
Young Co-Edits Innovative Journal on 19-Century Art
By Michael Bettencourt On November 14, 2018 · Leave a Comment
Dr. Marnin Young, associate professor and chair of art history at Stern College for Women, has co-edited a special issue of Nonsite, an online peer-reviewed journal, devoted to new research on 19-century art.
"Editing a special issue of an academic journal," said Dr. Young, "is a laborious process. Dr. Bridget Alsdorf, my co-editor from Princeton University, and I solicited contributions and sent all of them for peer review (where they were each read and evaluated by different scholars in the field). We sent the evaluations to the authors, who revised their articles, then sent the revised articles to a copyeditor, who cleaned up language, citations, formatting and so on. We also commented extensively on the style and format of the articles. We then had to assist authors in obtaining the high-quality reproductions that complement art history publications. Once the authors had approved the text and imagery, we formatted them for the website, including producing thumbnails and abstracts. All in all, the process has lasted over a year."
But the quality of what they have produced more than rewards the effort put into producing the work. "We both felt a need for a site online for serious scholarship on 19-century art. All the contributions are by art historians working on new topics or new theoretical angles in the field. None of the articles has been published before. Some of the articles break ground by presenting new objects of inquiry or by reframing the way we look at established artists, while one essay attempts to rethink the very nature and significance of 19-century art from the roots up."
They are already at work on second set of articles for a follow-up issue scheduled for early 2019. "We hope efforts like ours will be a regular part of the Nonsite publication."
Tagged with: 19th-century art • Marnin Young


text:
US Republicans sharply criticise Pakistan in debate
Arab League suspends Syria, calls for sanctions
US 'deeply troubled' by Yemen violence
In statement, State Department spokeswoman calls for "prompt investigation" into deaths of civilians in Taez.
Afp November 13, 2011
WASHINGTON: The United States said Saturday it was "deeply troubled" by reports of attacks on civilians in the Yemeni flashpoint city of Taez, and urged all parties to exercise "maximum restraint."
In a statement, State Department spokeswoman Victoria Nuland also called for a "prompt investigation" into the deaths of civilians in Taez, Yemen's second city located south of the capital Sanaa.
"We are deeply troubled by reports of attacks against civilians in the city of Taez. We extend our condolences to the families of those who lost their lives," Nuland said.
"We condemn violence by all parties in Yemen and call for all sides to exercise maximum restraint.
"We also call for a prompt investigation into the circumstances of these attacks and for those responsible to be brought to justice."
On Friday, government forces shelled a protest site in Taez, killing 15 civilians, including at least three women and three children, according to medics. At least 40 other people were wounded.
The violence erupted when security forces loyal to President Ali Abdullah Saleh began shelling areas around Freedom Square, the epicenter of the protest movement in Taez.
Witnesses blamed the violence on the Republican Guard, an elite unit commanded by Saleh's son Ahmed, accusing it of firing tank and artillery rounds into a crowd of protesting civilians.
The violence continued Saturday as armed tribesmen who have thrown their support behind the protest movement clashed with government troops in the city's Hassab district, witnesses said.
"If President Saleh cares about Yemen's future and the well-being of the Yemeni people, he must immediately initiate a full transfer of power" within the framework of a Gulf peace plan, Nuland said.
The spokeswoman called on Saleh to make good on his promise to step down "without delay."
MarkH | 10 years ago | Reply
@ur reality is ........: Oh, no, that's like an aphrodisiac for us. You should see the drone "pilots" every Wednesday. They blindfold themselves and play pin the tail on the terrorist for giggles. If they hit one they get a free turn and if they miss them and hit a civilian they're given a raise. But, if they don't hit anything they get suspended.
Don't get feeling too important. They're just generic statements. Remember to look under your bed and in your closet before you go to bed. The one night you don't, and we know because we're always watching you since you're so important, we'll be there.
ur reality is ........ | 10 years ago | Reply
US 'deeply troubled'
R u troubled by death & destruction in Iraq and elsewhere? Some have no shame.
Awlaqi son among militants killed in Yemen strikes: Tribe
Yemen unrest: Nine killed as UN action looms
Al Zawahiri: To plot or not to be


Casual, modern and inviting- that's the new look at Cirque, Fernie Alpine Resort's hottest new dining location.
Sink into a leather couch by the grand four-sided river-rock fireplace for a welcome activity break and enjoy rich hot chocolate on a cold day or a cooling beer when its sunny outside. Groups can gather at giant stripped pine tables or there's a stylish oyster bar for a quick snack or cocktail. Modern, understated neutral tones and striking chandeliers create a luxurious atmosphere that's as welcoming as it is exotic.
Step inside the sanctum of the Ice Bar, a stunning cavern of carved ice with illuminated by glowing lights in shades of pink, blue, grey and green. Wrap up in a fur-trimmed parka and sip perfectly chilled vodka or champagne - romantic for couples and fun for groups!
The Food & Beverage Team at Cirque understand the importance of using absolutely fresh, healthy ingredients that are prepared with utmost care. The menu is a Canadian and European fusion with specialities including fresh oysters and bison carpaccio, new twists on old favourites like elk meatball tagliatelle and truffle fries, and classics including spaghetti bolognaise and eggplant parmigiana. The breakfast and après ski menu are equally tantalizing.


This entry was posted in Buying an automobile and tagged Buying an automobile automobile resale value, car advertising, car buying, car cost, car deal, car shopping, e automobile auto deal truck motorcycle, Leasing Buy Here Pay Here, trade? automobile lease, truck buying. Bookmark the permalink.


text:
Home » Wharton, TX Flood, Apr 1900
Wharton, TX Flood, Apr 1900
Texas |
Floods |
TEXAS FLOOD GROWS.
Half the Town of Wharton Now Under Water.
Houston, Tex., April 13.---The Colorado river flood has now reached Wharton, and half the town is under water. So far there has been only one casualty, a Negro refugee being drowned in trying to reach the town. The people all got out of the bottoms and flocked to the town, driving their cattle before hem.
There will be some suffering because of the large number to be cared for. The loss to crops is heavy. The situation at Eagle Lake is very serious, as the waters of the river have poured into the lake and the country about is under water.
The Kansas Semi-Weekly Capital, Topeka, KS 17 Apr 1900
SPANS TOPPLE OVER INTO WATER.
Wreck of Southern Pacific Bridge at Wharton Is Almost Complete.
Special To The News.
Houston, Tex., April 12.---News received this afternoon at the manager's office of the Southern Pacific says that the flood in the Colorado at Columbus in receding and has already gone down about twelve inches. It has not yet, however, receded far enough to allow work to begin on the damage done by the flood. The company, however, has already sent to the scene a large force of men and bridge material, and as soon as the water will permit the work of replacing the bridge across the river will commence and will be pushed night and day to an early completion. The bridge which has just been destroyed by the overflow was a magnificent iron structure and a telegram received this morning from the railroad officials at Columbus says that at 9 o'clock last night both of the iron spans toppled over into the river and now lie in the bed of the stream, a mass of ruined bridge material.
The latest information obtainable here about the San Antonio and Aransas Pass bridge across the Colorado is that while it is out of line the structure stiff remains on the piers and abutments and as soon as the water recedes sufficiently it can quickly be righted.
Some fears were entertained for the bridges of the Katy over the Colorado and Brazos, but they have not been damaged in the least and the trains on that road are running as usual.
Dallas Morning News, Dallas, TX 13 Apr 1900
WHARTON IS DIVIDED BY WATER.
Caney Creek Is Two Hundred Feet Wide in Some Places.
Wharton, Tex., April 13.---The flood caught people so unprepared here in the way of boats that but little has been done in the way of relief. Breaks and sloughs are high from back water and outside communication is cut off. A negro boy named Will Mathis attempted to swim his horse across Caney, which is now in places 200 feet wide. The horse refused to swim and the boy was drowned in sight of town. William Kincheloe and H. Klein went in a boat to the relief of Wm. Lambert and family below town. Though they were surrounded by water and water ran in his house he refused to leave. They returned. The Caney with a rapid current divides the town. Water is well up in the streets. It will be tomorrow before anything like an accurate estimate of the damage can be made. The young cane crop will suffer most, as many hundreds of acres are planted along the Caney and the water standing longer that thirty hours will sour it. Business to a great extent in town is supposed.
Texas Disasters
Hurricanes (12)
Tornadoes (125)
Fort Worth, TX Flood, Sept 1900
Austin, TX Dam Break and Flood, Apr 1900
Brownwood, TX Flood, Sept 1900
Dallas, TX Streetcar Accident, Jul 1900
Ben Ficklin, TX Area Concho River Flood, Aug 1882


text:
Otto Bühler (* 11. Juni 1882 in Einöllen im Landkreis Kusel; † 14. April 1945 in Homburg) war ein deutscher Verwaltungsjurist und Landrat.

Leben
Otto Bühler studierte in den Jahren von 1900 bis 1904 Rechtswissenschaften an der Humboldt-Universität zu Berlin, der Universität Leipzig, der Ludwig-Maximilians-Universität München und der Julius-Maximilians-Universität Würzburg. Nach der ersten juristischen Staatsprüfung war er als Rechtspraktikant beim Amtsgericht Wolfstein, Landgericht Würzburg, Stadtverwaltung Würzburg und beim Bezirksamt Ochsenfurt eingesetzt und machte im Dezember 1907 das Große juristische Staatsexamen. Bevor Bühler zum 1. Dezember 1908 als Akzessist zur Regierung von Unterfranken kam, war er als geprüfter Rechtspraktikant beim Bezirksamt Kaiserslautern und bei der Handelskammer Würzburg tätig. Zum 1. Oktober 1912 erhielt er eine Anstellung als Assessor beim Bezirksamt Homburg, wurde dort 1920 Bezirksamtmann und zum 1. Juli 1921 Regierungsrat. In der Zeit vom 24. März 1923 bis zum 31. März 1933 war Bühler Vorsitzender der Saarfürsorge beim Reichsversicherungsgericht, das beim Reichsversicherungsamt angesiedelt war. 1926 wurde er Oberregierungsrat und zum 1. April 1933 zum Bezirksamtsvorstand in Frankenthal ernannt. Bereits einige Tage später wurde er vorübergehend  zur Dienstleistung bei der Regierung des Saarlandes, das unter dem Mandat des Völkerbundes stand, beurlaubt. Zum 1. April 1935 übernahm er wieder die Leitung der Verwaltung in Homburg, wo er später (ab 1939) Landrat wurde. 1942/1943 war er gleichzeitig mit der Führung des Landratsamtes St. Ingbert beauftragt.  Bühler kam bei einem Luftangriff auf Homburg am 14. April 1945 ums Leben.

Einzelnachweise

Jurist in der Kommunalverwaltung
Regierungsrat (Deutschland)
Oberregierungsrat
Landrat (Saarland)
Einöllen
Person (Landkreis Kusel)
Deutscher
Geboren 1882
Gestorben 1945
Mann

redpajama_set_name: RedPajamaWikipedia


London, UK , April 11, 2017: Integral Ad Science (IAS), the technology and data company that empowers the advertising industry to effectively influence consumers everywhere, is working with Google to deliver brand safety reporting on YouTube . With brand safety concerns at the forefront for advertisers, Google and IAS are looking to give advertisers additional visibility into how their ads are appearing on YouTube against a company's brand safety requirements.
With this initiative, advertisers will be able to access brand safety reporting metrics, providing additional, independent assurances around where their ads are appearing on YouTube. Given the uniqueness of YouTube's content, and that of the experience it provides to users, IAS and Google will seek to develop a secure and safe solution together that answers the industry's need for transparency.
The current IAS solution available to clients is MRC-accredited, and reports on eight separate brand risk categories – adult content, alcohol content, gambling content, hate speech, illegal downloads, illegal drugs, offensive language, and violence – to give advertisers a comprehensive understanding of their brand risk. Additional specifications are available to customise risk thresholds, as well as option for geo-compliance, keywords, and blacklists.


Pilot fish is the IT web page supervisor for a small paper mill the place he's accountable for supporting maximum of the customers.
And as the truck-management other folks need to be proper on web page, that suggests fish is accountable for the community, however the outsourcer handles beef up for one of the community's customers.
And that's who will get the decision when the truck-management customers have an issue scanning photographs from a multifunction printer/scanner and importing them to a website online.
Outsourcer's tech cannot resolve the issue, however he comes up with a workaround: He tells one consumer to connect the printer/scanner without delay to his computer the usage of a USB cable.


text:
Egidio Raúl Arévalo Ríos (Paysandú, 1 januari 1982) is een voetballer uit Uruguay die doorgaans als controlerende speelt. Hij debuteerde in 2006 in het Uruguayaans voetbalelftal. Arévalo was actief op het WK 2010, het WK 2014, de Copa América 2007, de Copa América 2011, de Copa América 2015, de Copa América Centenario en de Confederations Cup 2013. Hij was basisspeler in de Uruguayaanse ploeg die in 2011 het toernooi om de Copa América won.

Erelijst

Zie ook
Lijst van spelers van CF Monterrey

Uruguayaans voetballer
Uruguayaans olympisch deelnemer


The Westray mine disaster devastated families and a community. Robert Thompson reveals why what happened to him at the mine still haunts him.
Will a new land tenure system and three promising deep-water basins be enough to convince Big Oil to explore in Labrador waters?
When a large mine is built or a mammoth oil and gas field is brought on line, they can alter the economic fortunes of an entire region. We bring you 10 Atlantic Canadian projects that have the potential to do just that.
Could an emissions-busting technology keep King Coal alive in Nova Scotia?