HOcore.IoMultiBis

Require Import HOcore.Prelim.

Require Import HOcore.ComplLat
               HOcore.Compat
               HOcore.Ren
               HOcore.Bis
               HOcore.BisDecInjRen
               HOcore.UpToNu.

This file gathers the properties obout IO bisimilarity (def. via variable multiset bisimulations)

IO multi bis is closed under decidable injective renamings

Lemma s_io_multi_sym_closed_under_decidable_inj_ren:
  congruence s_io_multi_sym decidable_inj_ren_clos.
Proof.
  apply compat_impl_congruence.
  eapply intersect_fun_bin_preserv_compat.
Qed.

Soundness of up-to bisimilarity technique

Lemma up_to_io_bisimilarity_sound:
  sound s_io_multi_sym (up_to_nu s_io_multi_sym).
Proof.
  apply compat_impl_sound.
  - eapply symmetrize_fun_preserv_mono.
  - apply up_to_nu_f_is_nu_f_compat.
Qed.