The coq proofs are available below; is used either the excluded middle or a well-foundedness hypothesis over the reduction relation (instead of the non-divergence hypothesis).

**Instructions:** Download the sources. You can directly use the files in interactive mode or with coqide (no compilation is needed). The main result is in the file unique_sol_thm.v. Details are explained in the
comments, and in the README.

The files are split as follows, and in the following order:

- rels.v

A few lemmas and definitions regarding relations; the definitions of diagrams is usefull to define bisimulations and bisimilarities - LTS.v

Defines the notion of Labeled Transition System (with internal tau steps), and the usual definitions of weak transitions in such a LTS. - bsim.v

Definition and properties of weak bisimulations, and weak bisimilarity. Most of the work is related to the transitivity of weak bisimilarity. - operators.v

Definition of autonomous transitions, then of sets of operators; also includes some properties of functions, extensional equality of functions, and composition of functions. - divergences.v

Definitions of the notions of reducts of an operator and divergence of the infinite unfolding of an operator. - unique_sol_prop.v

The first lemma: if an operator 'protects its solutions', then it has a unique solution up to weak bisimilarity. - termination.v

A few lemmas regarding termination, non divergence, well-foundedness. - unique_solution_steps.v

The main part of the proof of the main theorem: we build a sequence of transitions and operators, and use non divergence to show it must terminate; if it does, that proves that the operator protects its solution. - unique_solution_thm.v

Putting everything together: statement of the main theorem.

**Some important definitions** (particularly those used as hypothesis, if one wants to check) are in:

LTS, weak transitions (wtrans, wttrans, whtrans): LTS.v

(strong and weak) bisimulation and bisimilarity: bsim.v

extensional equality of functions, autonomous transitions, guardedness, set of operators, weak autonomous transitions (waut, wtaut, whaut): operators.v

reduct (comp_red) of an operator, divergence (comp_div and div) of an operator (of its infinite unfolding): divergences.v

unique solution, protects its solutions: unique_sol_prop.v

the tau reduction relation (red_tau and reduction_tau) are in termination.v (for red_tau) and in unique_solution_thm.v (for reduction_tau). they are based on subrevR in termination.v, itself using comp_red from divergences.v