From mathcomp.ssreflect
Require Import ssreflect ssrbool ssrnat eqtype ssrfun seq.
From mathcomp
Require Import path.
Require Import Eqdep.
Require Import Relation_Operators.
From fcsl
Require Import axioms pred prelude ordtype finmap pcm unionmap heap.
From DiSeL
Require Import Freshness State EqTypeX DepMaps Protocols Worlds NetworkSem Rely.
From DiSeL
Require Import Actions Injection Process InductiveInv.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

(* Goal: @InMem (PCM.sort (union_mapPCM Label dstatelet)) (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Mem state (PredPredType state) (Coh W)) *)
(* Goal: @always_sc this W A (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Inject this W A V K w q') scs (fun (m : state) (q : proc this W A) => @ex (UMDef.tp Label dstatelet) (fun i' : UMDef.tp Label dstatelet => @ex (UMDef.tp Label dstatelet) (fun j' : UMDef.tp Label dstatelet => and4 (@eq state m (@PCM.join (union_mapPCM Label dstatelet) i' j')) (@InMem (UMDef.tp Label dstatelet) i' (@Mem state (PredPredType state) (Coh V))) (network_rely (@inj_ext V W K w) this j j') (or (@ex (proc this V A) (fun q' : proc this V A => and (@eq (proc this W A) q (@Inject this W A V K w q')) (P i' q'))) (@ex A (fun v' : A => and (@eq (proc this W A) q (@Ret this W A v')) (P i' (@Ret this V A v')))))))) *)
(* Here we define Nanevski et al.-style modal predicates for giving
   the meaning to Hoare triples. *)

Section Always.

Variable this : nid.
Variable W : world.

Notation coherent := (Coh W).

Arguments proc [this W].

(* Goal: @InMem (PCM.sort (union_mapPCM Label dstatelet)) (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Mem state (PredPredType state) (Coh W)) *)
(* Goal: @always_sc this W A (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Inject this W A V K w q') scs (fun (m : state) (q : proc this W A) => @ex (UMDef.tp Label dstatelet) (fun i' : UMDef.tp Label dstatelet => @ex (UMDef.tp Label dstatelet) (fun j' : UMDef.tp Label dstatelet => and4 (@eq state m (@PCM.join (union_mapPCM Label dstatelet) i' j')) (@InMem (UMDef.tp Label dstatelet) i' (@Mem state (PredPredType state) (Coh V))) (network_rely (@inj_ext V W K w) this j j') (or (@ex (proc this V A) (fun q' : proc this V A => and (@eq (proc this W A) q (@Inject this W A V K w q')) (P i' q'))) (@ex A (fun v' : A => and (@eq (proc this W A) q (@Ret this W A v')) (P i' (@Ret this V A v')))))))) *)
Fixpoint always_sc A (s1 : state) p scs (P : state -> proc A -> Prop) : Prop :=
  s1 \In coherent /\ 
  if scs is sc :: scs' then 
(* Goal: @InMem (PCM.sort (union_mapPCM Label dstatelet)) (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Mem state (PredPredType state) (Coh W)) *)
(* Goal: @always_sc this W A (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Inject this W A V K w q') scs (fun (m : state) (q : proc this W A) => @ex (UMDef.tp Label dstatelet) (fun i' : UMDef.tp Label dstatelet => @ex (UMDef.tp Label dstatelet) (fun j' : UMDef.tp Label dstatelet => and4 (@eq state m (@PCM.join (union_mapPCM Label dstatelet) i' j')) (@InMem (UMDef.tp Label dstatelet) i' (@Mem state (PredPredType state) (Coh V))) (network_rely (@inj_ext V W K w) this j j') (or (@ex (proc this V A) (fun q' : proc this V A => and (@eq (proc this W A) q (@Inject this W A V K w q')) (P i' q'))) (@ex A (fun v' : A => and (@eq (proc this W A) q (@Ret this W A v')) (P i' (@Ret this V A v')))))))) *)
    forall s2, network_rely W this s1 s2 -> 
      [/\ safe p sc s2, P s2 p &
(* Goal: @InMem (PCM.sort (union_mapPCM Label dstatelet)) (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Mem state (PredPredType state) (Coh W)) *)
(* Goal: @always_sc this W A (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Inject this W A V K w q') scs (fun (m : state) (q : proc this W A) => @ex (UMDef.tp Label dstatelet) (fun i' : UMDef.tp Label dstatelet => @ex (UMDef.tp Label dstatelet) (fun j' : UMDef.tp Label dstatelet => and4 (@eq state m (@PCM.join (union_mapPCM Label dstatelet) i' j')) (@InMem (UMDef.tp Label dstatelet) i' (@Mem state (PredPredType state) (Coh V))) (network_rely (@inj_ext V W K w) this j j') (or (@ex (proc this V A) (fun q' : proc this V A => and (@eq (proc this W A) q (@Inject this W A V K w q')) (P i' q'))) (@ex A (fun v' : A => and (@eq (proc this W A) q (@Ret this W A v')) (P i' (@Ret this V A v')))))))) *)
          forall s3 q, @pstep this W A s2 p sc s3 q -> always_sc s3 q scs' P]
(* Goal: @InMem (PCM.sort (union_mapPCM Label dstatelet)) (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Mem state (PredPredType state) (Coh W)) *)
(* Goal: @always_sc this W A (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Inject this W A V K w q') scs (fun (m : state) (q : proc this W A) => @ex (UMDef.tp Label dstatelet) (fun i' : UMDef.tp Label dstatelet => @ex (UMDef.tp Label dstatelet) (fun j' : UMDef.tp Label dstatelet => and4 (@eq state m (@PCM.join (union_mapPCM Label dstatelet) i' j')) (@InMem (UMDef.tp Label dstatelet) i' (@Mem state (PredPredType state) (Coh V))) (network_rely (@inj_ext V W K w) this j j') (or (@ex (proc this V A) (fun q' : proc this V A => and (@eq (proc this W A) q (@Inject this W A V K w q')) (P i' q'))) (@ex A (fun v' : A => and (@eq (proc this W A) q (@Ret this W A v')) (P i' (@Ret this V A v')))))))) *)
  else forall s2, network_rely W this s1 s2 -> P s2 p.

Definition always A s (p : proc A) P := forall scs, always_sc s p scs P.

(* Some basic properties of the alwas predicate *)

Lemma alw_coh' A s (p : proc A) scs P : 
(* Goal: @InMem (PCM.sort (union_mapPCM Label dstatelet)) (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Mem state (PredPredType state) (Coh W)) *)
(* Goal: @always_sc this W A (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Inject this W A V K w q') scs (fun (m : state) (q : proc this W A) => @ex (UMDef.tp Label dstatelet) (fun i' : UMDef.tp Label dstatelet => @ex (UMDef.tp Label dstatelet) (fun j' : UMDef.tp Label dstatelet => and4 (@eq state m (@PCM.join (union_mapPCM Label dstatelet) i' j')) (@InMem (UMDef.tp Label dstatelet) i' (@Mem state (PredPredType state) (Coh V))) (network_rely (@inj_ext V W K w) this j j') (or (@ex (proc this V A) (fun q' : proc this V A => and (@eq (proc this W A) q (@Inject this W A V K w q')) (P i' q'))) (@ex A (fun v' : A => and (@eq (proc this W A) q (@Ret this W A v')) (P i' (@Ret this V A v')))))))) *)
        always_sc s p scs P -> s \In coherent.
(* Goal: forall _ : @ex A (fun v' : A => and (@eq (proc this (mkWorld (@ProtocolWithIndInv pr I ii)) A) (@Ret this (mkWorld (@ProtocolWithIndInv pr I ii)) A v) (@Ret this (mkWorld (@ProtocolWithIndInv pr I ii)) A v')) (forall (v : A) (_ : @eq (proc this (mkWorld pr) A) (@Ret this (mkWorld pr) A v') (@Ret this (mkWorld pr) A v)), P v s)), P v s *)
Proof. by case: scs=>/=[|a l]; case. Qed.

Lemma alw_coh A s (p : proc A) P : 
(* Goal: @InMem (PCM.sort (union_mapPCM Label dstatelet)) (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Mem state (PredPredType state) (Coh W)) *)
(* Goal: @always_sc this W A (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Inject this W A V K w q') scs (fun (m : state) (q : proc this W A) => @ex (UMDef.tp Label dstatelet) (fun i' : UMDef.tp Label dstatelet => @ex (UMDef.tp Label dstatelet) (fun j' : UMDef.tp Label dstatelet => and4 (@eq state m (@PCM.join (union_mapPCM Label dstatelet) i' j')) (@InMem (UMDef.tp Label dstatelet) i' (@Mem state (PredPredType state) (Coh V))) (network_rely (@inj_ext V W K w) this j j') (or (@ex (proc this V A) (fun q' : proc this V A => and (@eq (proc this W A) q (@Inject this W A V K w q')) (P i' q'))) (@ex A (fun v' : A => and (@eq (proc this W A) q (@Ret this W A v')) (P i' (@Ret this V A v')))))))) *)
        always s p P -> s \In coherent.
Proof. by move/(_ [::]); move/alw_coh'. Qed.

Lemma alw_safe' A s (p : proc A) sc scs P : 
(* Goal: @InMem (PCM.sort (union_mapPCM Label dstatelet)) (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Mem state (PredPredType state) (Coh W)) *)
(* Goal: @always_sc this W A (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Inject this W A V K w q') scs (fun (m : state) (q : proc this W A) => @ex (UMDef.tp Label dstatelet) (fun i' : UMDef.tp Label dstatelet => @ex (UMDef.tp Label dstatelet) (fun j' : UMDef.tp Label dstatelet => and4 (@eq state m (@PCM.join (union_mapPCM Label dstatelet) i' j')) (@InMem (UMDef.tp Label dstatelet) i' (@Mem state (PredPredType state) (Coh V))) (network_rely (@inj_ext V W K w) this j j') (or (@ex (proc this V A) (fun q' : proc this V A => and (@eq (proc this W A) q (@Inject this W A V K w q')) (P i' q'))) (@ex A (fun v' : A => and (@eq (proc this W A) q (@Ret this W A v')) (P i' (@Ret this V A v')))))))) *)
        always_sc s p (sc :: scs) P -> safe p sc s.
Proof.
(* Goal: forall _ : @ex A (fun v' : A => and (@eq (proc this (mkWorld (@ProtocolWithIndInv pr I ii)) A) (@Ret this (mkWorld (@ProtocolWithIndInv pr I ii)) A v) (@Ret this (mkWorld (@ProtocolWithIndInv pr I ii)) A v')) (forall (v : A) (_ : @eq (proc this (mkWorld pr) A) (@Ret this (mkWorld pr) A v') (@Ret this (mkWorld pr) A v)), P v s)), P v s *)
by case: scs=>[|a l][]C/(_ s (rely_refl this C))[].
Qed.    

Lemma alw_safe A s (p : proc A) P :
(* Goal: @InMem (PCM.sort (union_mapPCM Label dstatelet)) (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Mem state (PredPredType state) (Coh W)) *)
(* Goal: @always_sc this W A (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Inject this W A V K w q') scs (fun (m : state) (q : proc this W A) => @ex (UMDef.tp Label dstatelet) (fun i' : UMDef.tp Label dstatelet => @ex (UMDef.tp Label dstatelet) (fun j' : UMDef.tp Label dstatelet => and4 (@eq state m (@PCM.join (union_mapPCM Label dstatelet) i' j')) (@InMem (UMDef.tp Label dstatelet) i' (@Mem state (PredPredType state) (Coh V))) (network_rely (@inj_ext V W K w) this j j') (or (@ex (proc this V A) (fun q' : proc this V A => and (@eq (proc this W A) q (@Inject this W A V K w q')) (P i' q'))) (@ex A (fun v' : A => and (@eq (proc this W A) q (@Ret this W A v')) (P i' (@Ret this V A v')))))))) *)
        always s p P -> forall sc, safe p sc s.
Proof. by move=>H sc; apply: alw_safe' (H [:: sc]). Qed.

Lemma alw_refl' A s (p : proc A) sc P : always_sc s p sc P -> P s p.
Proof.
(* Goal: forall _ : @ex A (fun v' : A => and (@eq (proc this (mkWorld (@ProtocolWithIndInv pr I ii)) A) (@Ret this (mkWorld (@ProtocolWithIndInv pr I ii)) A v) (@Ret this (mkWorld (@ProtocolWithIndInv pr I ii)) A v')) (forall (v : A) (_ : @eq (proc this (mkWorld pr) A) (@Ret this (mkWorld pr) A v') (@Ret this (mkWorld pr) A v)), P v s)), P v s *)
by case: sc=>[|a l][C]/(_ s (rely_refl this C))//; case.
Qed.

Lemma alw_refl A s (p : proc A) P : always s p P -> P s p.
Proof. by move/(_ [::])/alw_refl'. Qed.

Lemma alw_envs' A s1 (p : proc A) scs s2 P : 
(* Goal: @InMem (PCM.sort (union_mapPCM Label dstatelet)) (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Mem state (PredPredType state) (Coh W)) *)
(* Goal: @always_sc this W A (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Inject this W A V K w q') scs (fun (m : state) (q : proc this W A) => @ex (UMDef.tp Label dstatelet) (fun i' : UMDef.tp Label dstatelet => @ex (UMDef.tp Label dstatelet) (fun j' : UMDef.tp Label dstatelet => and4 (@eq state m (@PCM.join (union_mapPCM Label dstatelet) i' j')) (@InMem (UMDef.tp Label dstatelet) i' (@Mem state (PredPredType state) (Coh V))) (network_rely (@inj_ext V W K w) this j j') (or (@ex (proc this V A) (fun q' : proc this V A => and (@eq (proc this W A) q (@Inject this W A V K w q')) (P i' q'))) (@ex A (fun v' : A => and (@eq (proc this W A) q (@Ret this W A v')) (P i' (@Ret this V A v')))))))) *)
        always_sc s1 p scs P -> network_rely W this s1 s2 -> always_sc s2 p scs P.
Proof.
by case: scs=>//[|a l][C]H R; move/rely_coh: (R)=>/=[]H1 H2;
   split=>//s3 R'; apply: H; apply: (rely_trans R).
Qed.
 
Lemma alw_envs A s1 (p : proc A) s2 P :
(* Goal: @InMem (PCM.sort (union_mapPCM Label dstatelet)) (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Mem state (PredPredType state) (Coh W)) *)
(* Goal: @always_sc this W A (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Inject this W A V K w q') scs (fun (m : state) (q : proc this W A) => @ex (UMDef.tp Label dstatelet) (fun i' : UMDef.tp Label dstatelet => @ex (UMDef.tp Label dstatelet) (fun j' : UMDef.tp Label dstatelet => and4 (@eq state m (@PCM.join (union_mapPCM Label dstatelet) i' j')) (@InMem (UMDef.tp Label dstatelet) i' (@Mem state (PredPredType state) (Coh V))) (network_rely (@inj_ext V W K w) this j j') (or (@ex (proc this V A) (fun q' : proc this V A => and (@eq (proc this W A) q (@Inject this W A V K w q')) (P i' q'))) (@ex A (fun v' : A => and (@eq (proc this W A) q (@Ret this W A v')) (P i' (@Ret this V A v')))))))) *)
        always s1 p P -> network_rely W this s1 s2 -> always s2 p P.
Proof. by move=>S E scs; apply: alw_envs' (S scs) E. Qed.

(* Goal: @InMem (PCM.sort (union_mapPCM Label dstatelet)) (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Mem state (PredPredType state) (Coh W)) *)
(* Goal: @always_sc this W A (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Inject this W A V K w q') scs (fun (m : state) (q : proc this W A) => @ex (UMDef.tp Label dstatelet) (fun i' : UMDef.tp Label dstatelet => @ex (UMDef.tp Label dstatelet) (fun j' : UMDef.tp Label dstatelet => and4 (@eq state m (@PCM.join (union_mapPCM Label dstatelet) i' j')) (@InMem (UMDef.tp Label dstatelet) i' (@Mem state (PredPredType state) (Coh V))) (network_rely (@inj_ext V W K w) this j j') (or (@ex (proc this V A) (fun q' : proc this V A => and (@eq (proc this W A) q (@Inject this W A V K w q')) (P i' q'))) (@ex A (fun v' : A => and (@eq (proc this W A) q (@Ret this W A v')) (P i' (@Ret this V A v')))))))) *)
(* Always is preserved by this-stepping *)

Lemma alw_step A s1 (p : proc A) sc s2 q P :
(* Goal: @InMem (PCM.sort (union_mapPCM Label dstatelet)) (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Mem state (PredPredType state) (Coh W)) *)
(* Goal: @always_sc this W A (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Inject this W A V K w q') scs (fun (m : state) (q : proc this W A) => @ex (UMDef.tp Label dstatelet) (fun i' : UMDef.tp Label dstatelet => @ex (UMDef.tp Label dstatelet) (fun j' : UMDef.tp Label dstatelet => and4 (@eq state m (@PCM.join (union_mapPCM Label dstatelet) i' j')) (@InMem (UMDef.tp Label dstatelet) i' (@Mem state (PredPredType state) (Coh V))) (network_rely (@inj_ext V W K w) this j j') (or (@ex (proc this V A) (fun q' : proc this V A => and (@eq (proc this W A) q (@Inject this W A V K w q')) (P i' q'))) (@ex A (fun v' : A => and (@eq (proc this W A) q (@Ret this W A v')) (P i' (@Ret this V A v')))))))) *)
        always s1 p P -> pstep s1 p sc s2 q -> always s2 q P.
Proof.
(* Goal: forall (s3 : state) (q : @proc this W A) (_ : @pstep this W A s2 p sc s3 q), @always_sc A s3 q scs (fun (s' : state) (p' : @proc this W A) => forall _ : P, Q s' p') *)
move=>Ls Ts; move: (Ls [:: sc])=>/= [C].
(* Goal: and (network_rely V this s1 s2) (network_rely (@inj_ext V W K w) this s1' s2') *)
(* Goal: forall (_ : and (@eq state (@PCM.join (union_mapPCM Label dstatelet) s1 s1') (@PCM.join (union_mapPCM Label dstatelet) s2 s2')) (@InMem state (@PCM.join (union_mapPCM Label dstatelet) s1 s1') (@Mem state (PredPredType state) (Coh W)))) (_ : @InMem state s1 (@Mem state (PredPredType state) (Coh V))) (_ : @InMem state s2 (@Mem state (PredPredType state) (Coh V))), and (network_rely V this s1 s2) (network_rely (@inj_ext V W K w) this s1' s2') *)
case/(_ _ (rely_refl this C))=>_ _; move/(_ _ _ Ts)=>_. 
(* Goal: forall (s3 : state) (q : @proc this W A) (_ : @pstep this W A s2 p sc s3 q), @always_sc A s3 q scs (fun (s' : state) (p' : @proc this W A) => forall _ : P, Q s' p') *)
move=>scs; move: (Ls (sc :: scs))=>/= [_].
(* Goal: forall _ : @ex A (fun v' : A => and (@eq (proc this (mkWorld (@ProtocolWithIndInv pr I ii)) A) (@Ret this (mkWorld (@ProtocolWithIndInv pr I ii)) A v) (@Ret this (mkWorld (@ProtocolWithIndInv pr I ii)) A v')) (forall (v : A) (_ : @eq (proc this (mkWorld pr) A) (@Ret this (mkWorld pr) A v') (@Ret this (mkWorld pr) A v)), P v s)), P v s *)
by case/(_ _ (rely_refl this C))=>_ _; move/(_ _ _ Ts). 
Qed.

(* Relaxing the predicate P wrt. rely *)
(* Goal: @InMem (PCM.sort (union_mapPCM Label dstatelet)) (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Mem state (PredPredType state) (Coh W)) *)
(* Goal: @always_sc this W A (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Inject this W A V K w q') scs (fun (m : state) (q : proc this W A) => @ex (UMDef.tp Label dstatelet) (fun i' : UMDef.tp Label dstatelet => @ex (UMDef.tp Label dstatelet) (fun j' : UMDef.tp Label dstatelet => and4 (@eq state m (@PCM.join (union_mapPCM Label dstatelet) i' j')) (@InMem (UMDef.tp Label dstatelet) i' (@Mem state (PredPredType state) (Coh V))) (network_rely (@inj_ext V W K w) this j j') (or (@ex (proc this V A) (fun q' : proc this V A => and (@eq (proc this W A) q (@Inject this W A V K w q')) (P i' q'))) (@ex A (fun v' : A => and (@eq (proc this W A) q (@Ret this W A v')) (P i' (@Ret this V A v')))))))) *)
Lemma alwp_envsq A s1 (p1 : proc A) scs (P : _ -> _ -> Prop) : 
(* Goal: @InMem (PCM.sort (union_mapPCM Label dstatelet)) (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Mem state (PredPredType state) (Coh W)) *)
(* Goal: @always_sc this W A (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Inject this W A V K w q') scs (fun (m : state) (q : proc this W A) => @ex (UMDef.tp Label dstatelet) (fun i' : UMDef.tp Label dstatelet => @ex (UMDef.tp Label dstatelet) (fun j' : UMDef.tp Label dstatelet => and4 (@eq state m (@PCM.join (union_mapPCM Label dstatelet) i' j')) (@InMem (UMDef.tp Label dstatelet) i' (@Mem state (PredPredType state) (Coh V))) (network_rely (@inj_ext V W K w) this j j') (or (@ex (proc this V A) (fun q' : proc this V A => and (@eq (proc this W A) q (@Inject this W A V K w q')) (P i' q'))) (@ex A (fun v' : A => and (@eq (proc this W A) q (@Ret this W A v')) (P i' (@Ret this V A v')))))))) *)
        always_sc s1 p1 scs P ->
        always_sc s1 p1 scs 
(* Goal: @InMem (PCM.sort (union_mapPCM Label dstatelet)) (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Mem state (PredPredType state) (Coh W)) *)
(* Goal: @always_sc this W A (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Inject this W A V K w q') scs (fun (m : state) (q : proc this W A) => @ex (UMDef.tp Label dstatelet) (fun i' : UMDef.tp Label dstatelet => @ex (UMDef.tp Label dstatelet) (fun j' : UMDef.tp Label dstatelet => and4 (@eq state m (@PCM.join (union_mapPCM Label dstatelet) i' j')) (@InMem (UMDef.tp Label dstatelet) i' (@Mem state (PredPredType state) (Coh V))) (network_rely (@inj_ext V W K w) this j j') (or (@ex (proc this V A) (fun q' : proc this V A => and (@eq (proc this W A) q (@Inject this W A V K w q')) (P i' q'))) (@ex A (fun v' : A => and (@eq (proc this W A) q (@Ret this W A v')) (P i' (@Ret this V A v')))))))) *)
          (fun s2 p2 => forall s3, network_rely W this s2 s3 -> P s3 p2).
Proof.
(* Goal: forall (_ : @always_sc A s p scs (fun (s' : state) (p' : @proc this W A) => forall _ : P, Q s' p')) (_ : P), @always_sc A s p scs (fun (s' : state) (p' : @proc this W A) => Q s' p') *)
(* Goal: forall _ : forall _ : P, @always_sc A s p scs (fun (s' : state) (p' : @proc this W A) => Q s' p'), @always_sc A s p scs (fun (s' : state) (p' : @proc this W A) => forall _ : P, Q s' p') *)
elim: scs s1 p1=>[|sc scs IH] /= s1 p1 [C H]; split=>// s2 M.
(* Goal: @InMem (PCM.sort (union_mapPCM Label dstatelet)) (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Mem state (PredPredType state) (Coh W)) *)
(* Goal: @always_sc this W A (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Inject this W A V K w q') scs (fun (m : state) (q : proc this W A) => @ex (UMDef.tp Label dstatelet) (fun i' : UMDef.tp Label dstatelet => @ex (UMDef.tp Label dstatelet) (fun j' : UMDef.tp Label dstatelet => and4 (@eq state m (@PCM.join (union_mapPCM Label dstatelet) i' j')) (@InMem (UMDef.tp Label dstatelet) i' (@Mem state (PredPredType state) (Coh V))) (network_rely (@inj_ext V W K w) this j j') (or (@ex (proc this V A) (fun q' : proc this V A => and (@eq (proc this W A) q (@Inject this W A V K w q')) (P i' q'))) (@ex A (fun v' : A => and (@eq (proc this W A) q (@Ret this W A v')) (P i' (@Ret this V A v')))))))) *)
- by move=>s3 /(rely_trans M); apply: H. 
(* Goal: P v s *)
split; first by case: (H _ M).
(* Goal: @InMem (PCM.sort (union_mapPCM Label dstatelet)) (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Mem state (PredPredType state) (Coh W)) *)
(* Goal: @always_sc this W A (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Inject this W A V K w q') scs (fun (m : state) (q : proc this W A) => @ex (UMDef.tp Label dstatelet) (fun i' : UMDef.tp Label dstatelet => @ex (UMDef.tp Label dstatelet) (fun j' : UMDef.tp Label dstatelet => and4 (@eq state m (@PCM.join (union_mapPCM Label dstatelet) i' j')) (@InMem (UMDef.tp Label dstatelet) i' (@Mem state (PredPredType state) (Coh V))) (network_rely (@inj_ext V W K w) this j j') (or (@ex (proc this V A) (fun q' : proc this V A => and (@eq (proc this W A) q (@Inject this W A V K w q')) (P i' q'))) (@ex A (fun v' : A => and (@eq (proc this W A) q (@Ret this W A v')) (P i' (@Ret this V A v')))))))) *)
- by move=>s3 /(rely_trans M) /H; case. 
(* Goal: forall _ : @ex A (fun v' : A => and (@eq (proc this (mkWorld (@ProtocolWithIndInv pr I ii)) A) (@Ret this (mkWorld (@ProtocolWithIndInv pr I ii)) A v) (@Ret this (mkWorld (@ProtocolWithIndInv pr I ii)) A v')) (forall (v : A) (_ : @eq (proc this (mkWorld pr) A) (@Ret this (mkWorld pr) A v') (@Ret this (mkWorld pr) A v)), P v s)), P v s *)
by move=>s3 q T; apply: IH; case: (H _ M)=>_ _; apply. 
Qed.

(* Goal: @InMem (PCM.sort (union_mapPCM Label dstatelet)) (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Mem state (PredPredType state) (Coh W)) *)
(* Goal: @always_sc this W A (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Inject this W A V K w q') scs (fun (m : state) (q : proc this W A) => @ex (UMDef.tp Label dstatelet) (fun i' : UMDef.tp Label dstatelet => @ex (UMDef.tp Label dstatelet) (fun j' : UMDef.tp Label dstatelet => and4 (@eq state m (@PCM.join (union_mapPCM Label dstatelet) i' j')) (@InMem (UMDef.tp Label dstatelet) i' (@Mem state (PredPredType state) (Coh V))) (network_rely (@inj_ext V W K w) this j j') (or (@ex (proc this V A) (fun q' : proc this V A => and (@eq (proc this W A) q (@Inject this W A V K w q')) (P i' q'))) (@ex A (fun v' : A => and (@eq (proc this W A) q (@Ret this W A v')) (P i' (@Ret this V A v')))))))) *)
Lemma alw_envsq A s1 (p1 : proc A) (P : _ -> _ -> Prop) : 
(* Goal: @InMem (PCM.sort (union_mapPCM Label dstatelet)) (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Mem state (PredPredType state) (Coh W)) *)
(* Goal: @always_sc this W A (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Inject this W A V K w q') scs (fun (m : state) (q : proc this W A) => @ex (UMDef.tp Label dstatelet) (fun i' : UMDef.tp Label dstatelet => @ex (UMDef.tp Label dstatelet) (fun j' : UMDef.tp Label dstatelet => and4 (@eq state m (@PCM.join (union_mapPCM Label dstatelet) i' j')) (@InMem (UMDef.tp Label dstatelet) i' (@Mem state (PredPredType state) (Coh V))) (network_rely (@inj_ext V W K w) this j j') (or (@ex (proc this V A) (fun q' : proc this V A => and (@eq (proc this W A) q (@Inject this W A V K w q')) (P i' q'))) (@ex A (fun v' : A => and (@eq (proc this W A) q (@Ret this W A v')) (P i' (@Ret this V A v')))))))) *)
        always s1 p1 P ->
(* Goal: @InMem (PCM.sort (union_mapPCM Label dstatelet)) (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Mem state (PredPredType state) (Coh W)) *)
(* Goal: @always_sc this W A (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Inject this W A V K w q') scs (fun (m : state) (q : proc this W A) => @ex (UMDef.tp Label dstatelet) (fun i' : UMDef.tp Label dstatelet => @ex (UMDef.tp Label dstatelet) (fun j' : UMDef.tp Label dstatelet => and4 (@eq state m (@PCM.join (union_mapPCM Label dstatelet) i' j')) (@InMem (UMDef.tp Label dstatelet) i' (@Mem state (PredPredType state) (Coh V))) (network_rely (@inj_ext V W K w) this j j') (or (@ex (proc this V A) (fun q' : proc this V A => and (@eq (proc this W A) q (@Inject this W A V K w q')) (P i' q'))) (@ex A (fun v' : A => and (@eq (proc this W A) q (@Ret this W A v')) (P i' (@Ret this V A v')))))))) *)
        always s1 p1 (fun s2 p2 => forall s3, network_rely W this s2 s3 -> P s3 p2).
Proof. by move=>H scs; apply: alwp_envsq (H scs). Qed.


(* Goal: @InMem (PCM.sort (union_mapPCM Label dstatelet)) (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Mem state (PredPredType state) (Coh W)) *)
(* Goal: @always_sc this W A (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Inject this W A V K w q') scs (fun (m : state) (q : proc this W A) => @ex (UMDef.tp Label dstatelet) (fun i' : UMDef.tp Label dstatelet => @ex (UMDef.tp Label dstatelet) (fun j' : UMDef.tp Label dstatelet => and4 (@eq state m (@PCM.join (union_mapPCM Label dstatelet) i' j')) (@InMem (UMDef.tp Label dstatelet) i' (@Mem state (PredPredType state) (Coh V))) (network_rely (@inj_ext V W K w) this j j') (or (@ex (proc this V A) (fun q' : proc this V A => and (@eq (proc this W A) q (@Inject this W A V K w q')) (P i' q'))) (@ex A (fun v' : A => and (@eq (proc this W A) q (@Ret this W A v')) (P i' (@Ret this V A v')))))))) *)
Lemma alw_unfin' A s1 scs (P : state -> proc A -> Prop) :
(* Goal: @InMem (PCM.sort (union_mapPCM Label dstatelet)) (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Mem state (PredPredType state) (Coh W)) *)
(* Goal: @always_sc this W A (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Inject this W A V K w q') scs (fun (m : state) (q : proc this W A) => @ex (UMDef.tp Label dstatelet) (fun i' : UMDef.tp Label dstatelet => @ex (UMDef.tp Label dstatelet) (fun j' : UMDef.tp Label dstatelet => and4 (@eq state m (@PCM.join (union_mapPCM Label dstatelet) i' j')) (@InMem (UMDef.tp Label dstatelet) i' (@Mem state (PredPredType state) (Coh V))) (network_rely (@inj_ext V W K w) this j j') (or (@ex (proc this V A) (fun q' : proc this V A => and (@eq (proc this W A) q (@Inject this W A V K w q')) (P i' q'))) (@ex A (fun v' : A => and (@eq (proc this W A) q (@Ret this W A v')) (P i' (@Ret this V A v')))))))) *)
        s1 \In coherent -> 
(* Goal: @InMem (PCM.sort (union_mapPCM Label dstatelet)) (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Mem state (PredPredType state) (Coh W)) *)
(* Goal: @always_sc this W A (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Inject this W A V K w q') scs (fun (m : state) (q : proc this W A) => @ex (UMDef.tp Label dstatelet) (fun i' : UMDef.tp Label dstatelet => @ex (UMDef.tp Label dstatelet) (fun j' : UMDef.tp Label dstatelet => and4 (@eq state m (@PCM.join (union_mapPCM Label dstatelet) i' j')) (@InMem (UMDef.tp Label dstatelet) i' (@Mem state (PredPredType state) (Coh V))) (network_rely (@inj_ext V W K w) this j j') (or (@ex (proc this V A) (fun q' : proc this V A => and (@eq (proc this W A) q (@Inject this W A V K w q')) (P i' q'))) (@ex A (fun v' : A => and (@eq (proc this W A) q (@Ret this W A v')) (P i' (@Ret this V A v')))))))) *)
        (forall s2, network_rely W this s1 s2 -> P s2 Unfinished) -> 
        always_sc s1 Unfinished scs P.
Proof. 
(* Goal: and (network_rely V this s1 s2) (network_rely (@inj_ext V W K w) this s1' s2') *)
(* Goal: forall (_ : and (@eq state (@PCM.join (union_mapPCM Label dstatelet) s1 s1') (@PCM.join (union_mapPCM Label dstatelet) s2 s2')) (@InMem state (@PCM.join (union_mapPCM Label dstatelet) s1 s1') (@Mem state (PredPredType state) (Coh W)))) (_ : @InMem state s1 (@Mem state (PredPredType state) (Coh V))) (_ : @InMem state s2 (@Mem state (PredPredType state) (Coh V))), and (network_rely V this s1 s2) (network_rely (@inj_ext V W K w) this s1' s2') *)
case: scs=>[|sc scs] C H; split=>// s2 E.
(* Goal: P v s *)
split=>[||s3 q/stepUnfin]//; first by case: sc=>//.
(* Goal: forall _ : @ex A (fun v' : A => and (@eq (proc this (mkWorld (@ProtocolWithIndInv pr I ii)) A) (@Ret this (mkWorld (@ProtocolWithIndInv pr I ii)) A v) (@Ret this (mkWorld (@ProtocolWithIndInv pr I ii)) A v')) (forall (v : A) (_ : @eq (proc this (mkWorld pr) A) (@Ret this (mkWorld pr) A v') (@Ret this (mkWorld pr) A v)), P v s)), P v s *)
by apply: H.
Qed.

(* Goal: @InMem (PCM.sort (union_mapPCM Label dstatelet)) (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Mem state (PredPredType state) (Coh W)) *)
(* Goal: @always_sc this W A (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Inject this W A V K w q') scs (fun (m : state) (q : proc this W A) => @ex (UMDef.tp Label dstatelet) (fun i' : UMDef.tp Label dstatelet => @ex (UMDef.tp Label dstatelet) (fun j' : UMDef.tp Label dstatelet => and4 (@eq state m (@PCM.join (union_mapPCM Label dstatelet) i' j')) (@InMem (UMDef.tp Label dstatelet) i' (@Mem state (PredPredType state) (Coh V))) (network_rely (@inj_ext V W K w) this j j') (or (@ex (proc this V A) (fun q' : proc this V A => and (@eq (proc this W A) q (@Inject this W A V K w q')) (P i' q'))) (@ex A (fun v' : A => and (@eq (proc this W A) q (@Ret this W A v')) (P i' (@Ret this V A v')))))))) *)
Lemma alw_unfin A s1 (P : state -> proc A -> Prop) :
(* Goal: @InMem (PCM.sort (union_mapPCM Label dstatelet)) (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Mem state (PredPredType state) (Coh W)) *)
(* Goal: @always_sc this W A (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Inject this W A V K w q') scs (fun (m : state) (q : proc this W A) => @ex (UMDef.tp Label dstatelet) (fun i' : UMDef.tp Label dstatelet => @ex (UMDef.tp Label dstatelet) (fun j' : UMDef.tp Label dstatelet => and4 (@eq state m (@PCM.join (union_mapPCM Label dstatelet) i' j')) (@InMem (UMDef.tp Label dstatelet) i' (@Mem state (PredPredType state) (Coh V))) (network_rely (@inj_ext V W K w) this j j') (or (@ex (proc this V A) (fun q' : proc this V A => and (@eq (proc this W A) q (@Inject this W A V K w q')) (P i' q'))) (@ex A (fun v' : A => and (@eq (proc this W A) q (@Ret this W A v')) (P i' (@Ret this V A v')))))))) *)
        s1 \In coherent -> 
(* Goal: @InMem (PCM.sort (union_mapPCM Label dstatelet)) (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Mem state (PredPredType state) (Coh W)) *)
(* Goal: @always_sc this W A (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Inject this W A V K w q') scs (fun (m : state) (q : proc this W A) => @ex (UMDef.tp Label dstatelet) (fun i' : UMDef.tp Label dstatelet => @ex (UMDef.tp Label dstatelet) (fun j' : UMDef.tp Label dstatelet => and4 (@eq state m (@PCM.join (union_mapPCM Label dstatelet) i' j')) (@InMem (UMDef.tp Label dstatelet) i' (@Mem state (PredPredType state) (Coh V))) (network_rely (@inj_ext V W K w) this j j') (or (@ex (proc this V A) (fun q' : proc this V A => and (@eq (proc this W A) q (@Inject this W A V K w q')) (P i' q'))) (@ex A (fun v' : A => and (@eq (proc this W A) q (@Ret this W A v')) (P i' (@Ret this V A v')))))))) *)
        (forall s2, network_rely W this s1 s2 -> P s2 Unfinished) ->
        always s1 Unfinished P.
Proof. by move=>C H scs; apply: alw_unfin'. Qed.

(* Goal: @InMem (PCM.sort (union_mapPCM Label dstatelet)) (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Mem state (PredPredType state) (Coh W)) *)
(* Goal: @always_sc this W A (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Inject this W A V K w q') scs (fun (m : state) (q : proc this W A) => @ex (UMDef.tp Label dstatelet) (fun i' : UMDef.tp Label dstatelet => @ex (UMDef.tp Label dstatelet) (fun j' : UMDef.tp Label dstatelet => and4 (@eq state m (@PCM.join (union_mapPCM Label dstatelet) i' j')) (@InMem (UMDef.tp Label dstatelet) i' (@Mem state (PredPredType state) (Coh V))) (network_rely (@inj_ext V W K w) this j j') (or (@ex (proc this V A) (fun q' : proc this V A => and (@eq (proc this W A) q (@Inject this W A V K w q')) (P i' q'))) (@ex A (fun v' : A => and (@eq (proc this W A) q (@Ret this W A v')) (P i' (@Ret this V A v')))))))) *)
Lemma alw_ret' A s1 (v : A) scs (P : state -> proc A -> Prop) : 
(* Goal: @InMem (PCM.sort (union_mapPCM Label dstatelet)) (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Mem state (PredPredType state) (Coh W)) *)
(* Goal: @always_sc this W A (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Inject this W A V K w q') scs (fun (m : state) (q : proc this W A) => @ex (UMDef.tp Label dstatelet) (fun i' : UMDef.tp Label dstatelet => @ex (UMDef.tp Label dstatelet) (fun j' : UMDef.tp Label dstatelet => and4 (@eq state m (@PCM.join (union_mapPCM Label dstatelet) i' j')) (@InMem (UMDef.tp Label dstatelet) i' (@Mem state (PredPredType state) (Coh V))) (network_rely (@inj_ext V W K w) this j j') (or (@ex (proc this V A) (fun q' : proc this V A => and (@eq (proc this W A) q (@Inject this W A V K w q')) (P i' q'))) (@ex A (fun v' : A => and (@eq (proc this W A) q (@Ret this W A v')) (P i' (@Ret this V A v')))))))) *)
        s1 \In coherent -> 
(* Goal: @InMem (PCM.sort (union_mapPCM Label dstatelet)) (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Mem state (PredPredType state) (Coh W)) *)
(* Goal: @always_sc this W A (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Inject this W A V K w q') scs (fun (m : state) (q : proc this W A) => @ex (UMDef.tp Label dstatelet) (fun i' : UMDef.tp Label dstatelet => @ex (UMDef.tp Label dstatelet) (fun j' : UMDef.tp Label dstatelet => and4 (@eq state m (@PCM.join (union_mapPCM Label dstatelet) i' j')) (@InMem (UMDef.tp Label dstatelet) i' (@Mem state (PredPredType state) (Coh V))) (network_rely (@inj_ext V W K w) this j j') (or (@ex (proc this V A) (fun q' : proc this V A => and (@eq (proc this W A) q (@Inject this W A V K w q')) (P i' q'))) (@ex A (fun v' : A => and (@eq (proc this W A) q (@Ret this W A v')) (P i' (@Ret this V A v')))))))) *)
        (forall s2, network_rely W this s1 s2 -> P s2 (Ret v)) -> 
        always_sc s1 (Ret v) scs P.
Proof. 
(* Goal: and (network_rely V this s1 s2) (network_rely (@inj_ext V W K w) this s1' s2') *)
(* Goal: forall (_ : and (@eq state (@PCM.join (union_mapPCM Label dstatelet) s1 s1') (@PCM.join (union_mapPCM Label dstatelet) s2 s2')) (@InMem state (@PCM.join (union_mapPCM Label dstatelet) s1 s1') (@Mem state (PredPredType state) (Coh W)))) (_ : @InMem state s1 (@Mem state (PredPredType state) (Coh V))) (_ : @InMem state s2 (@Mem state (PredPredType state) (Coh V))), and (network_rely V this s1 s2) (network_rely (@inj_ext V W K w) this s1' s2') *)
case: scs=>[|sc scs] C H; split=>// s2 E.
(* Goal: P v s *)
split; last by [move=>s3 q; move/stepRet].
(* Goal: @InMem (PCM.sort (union_mapPCM Label dstatelet)) (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Mem state (PredPredType state) (Coh W)) *)
(* Goal: @always_sc this W A (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Inject this W A V K w q') scs (fun (m : state) (q : proc this W A) => @ex (UMDef.tp Label dstatelet) (fun i' : UMDef.tp Label dstatelet => @ex (UMDef.tp Label dstatelet) (fun j' : UMDef.tp Label dstatelet => and4 (@eq state m (@PCM.join (union_mapPCM Label dstatelet) i' j')) (@InMem (UMDef.tp Label dstatelet) i' (@Mem state (PredPredType state) (Coh V))) (network_rely (@inj_ext V W K w) this j j') (or (@ex (proc this V A) (fun q' : proc this V A => and (@eq (proc this W A) q (@Inject this W A V K w q')) (P i' q'))) (@ex A (fun v' : A => and (@eq (proc this W A) q (@Ret this W A v')) (P i' (@Ret this V A v')))))))) *)
- by case: sc.
(* Goal: forall _ : @ex A (fun v' : A => and (@eq (proc this (mkWorld (@ProtocolWithIndInv pr I ii)) A) (@Ret this (mkWorld (@ProtocolWithIndInv pr I ii)) A v) (@Ret this (mkWorld (@ProtocolWithIndInv pr I ii)) A v')) (forall (v : A) (_ : @eq (proc this (mkWorld pr) A) (@Ret this (mkWorld pr) A v') (@Ret this (mkWorld pr) A v)), P v s)), P v s *)
by apply: H E.
Qed.

(* Goal: @InMem (PCM.sort (union_mapPCM Label dstatelet)) (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Mem state (PredPredType state) (Coh W)) *)
(* Goal: @always_sc this W A (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Inject this W A V K w q') scs (fun (m : state) (q : proc this W A) => @ex (UMDef.tp Label dstatelet) (fun i' : UMDef.tp Label dstatelet => @ex (UMDef.tp Label dstatelet) (fun j' : UMDef.tp Label dstatelet => and4 (@eq state m (@PCM.join (union_mapPCM Label dstatelet) i' j')) (@InMem (UMDef.tp Label dstatelet) i' (@Mem state (PredPredType state) (Coh V))) (network_rely (@inj_ext V W K w) this j j') (or (@ex (proc this V A) (fun q' : proc this V A => and (@eq (proc this W A) q (@Inject this W A V K w q')) (P i' q'))) (@ex A (fun v' : A => and (@eq (proc this W A) q (@Ret this W A v')) (P i' (@Ret this V A v')))))))) *)
Lemma alw_ret A s1 (v : A) (P : state -> proc A -> Prop) : 
(* Goal: @InMem (PCM.sort (union_mapPCM Label dstatelet)) (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Mem state (PredPredType state) (Coh W)) *)
(* Goal: @always_sc this W A (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Inject this W A V K w q') scs (fun (m : state) (q : proc this W A) => @ex (UMDef.tp Label dstatelet) (fun i' : UMDef.tp Label dstatelet => @ex (UMDef.tp Label dstatelet) (fun j' : UMDef.tp Label dstatelet => and4 (@eq state m (@PCM.join (union_mapPCM Label dstatelet) i' j')) (@InMem (UMDef.tp Label dstatelet) i' (@Mem state (PredPredType state) (Coh V))) (network_rely (@inj_ext V W K w) this j j') (or (@ex (proc this V A) (fun q' : proc this V A => and (@eq (proc this W A) q (@Inject this W A V K w q')) (P i' q'))) (@ex A (fun v' : A => and (@eq (proc this W A) q (@Ret this W A v')) (P i' (@Ret this V A v')))))))) *)
        s1 \In coherent -> 
(* Goal: @InMem (PCM.sort (union_mapPCM Label dstatelet)) (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Mem state (PredPredType state) (Coh W)) *)
(* Goal: @always_sc this W A (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Inject this W A V K w q') scs (fun (m : state) (q : proc this W A) => @ex (UMDef.tp Label dstatelet) (fun i' : UMDef.tp Label dstatelet => @ex (UMDef.tp Label dstatelet) (fun j' : UMDef.tp Label dstatelet => and4 (@eq state m (@PCM.join (union_mapPCM Label dstatelet) i' j')) (@InMem (UMDef.tp Label dstatelet) i' (@Mem state (PredPredType state) (Coh V))) (network_rely (@inj_ext V W K w) this j j') (or (@ex (proc this V A) (fun q' : proc this V A => and (@eq (proc this W A) q (@Inject this W A V K w q')) (P i' q'))) (@ex A (fun v' : A => and (@eq (proc this W A) q (@Ret this W A v')) (P i' (@Ret this V A v')))))))) *)
        (forall s2, network_rely W this s1 s2 -> P s2 (Ret v)) -> 
        always s1 (Ret v) P.
Proof. by move=>C H ps; apply: alw_ret'. Qed.

(* Goal: @InMem (PCM.sort (union_mapPCM Label dstatelet)) (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Mem state (PredPredType state) (Coh W)) *)
(* Goal: @always_sc this W A (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Inject this W A V K w q') scs (fun (m : state) (q : proc this W A) => @ex (UMDef.tp Label dstatelet) (fun i' : UMDef.tp Label dstatelet => @ex (UMDef.tp Label dstatelet) (fun j' : UMDef.tp Label dstatelet => and4 (@eq state m (@PCM.join (union_mapPCM Label dstatelet) i' j')) (@InMem (UMDef.tp Label dstatelet) i' (@Mem state (PredPredType state) (Coh V))) (network_rely (@inj_ext V W K w) this j j') (or (@ex (proc this V A) (fun q' : proc this V A => and (@eq (proc this W A) q (@Inject this W A V K w q')) (P i' q'))) (@ex A (fun v' : A => and (@eq (proc this W A) q (@Ret this W A v')) (P i' (@Ret this V A v')))))))) *)
Lemma alw_act A s1 (a : action W A this) (P : state -> proc A -> Prop) :
(* Goal: @InMem (PCM.sort (union_mapPCM Label dstatelet)) (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Mem state (PredPredType state) (Coh W)) *)
(* Goal: @always_sc this W A (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Inject this W A V K w q') scs (fun (m : state) (q : proc this W A) => @ex (UMDef.tp Label dstatelet) (fun i' : UMDef.tp Label dstatelet => @ex (UMDef.tp Label dstatelet) (fun j' : UMDef.tp Label dstatelet => and4 (@eq state m (@PCM.join (union_mapPCM Label dstatelet) i' j')) (@InMem (UMDef.tp Label dstatelet) i' (@Mem state (PredPredType state) (Coh V))) (network_rely (@inj_ext V W K w) this j j') (or (@ex (proc this V A) (fun q' : proc this V A => and (@eq (proc this W A) q (@Inject this W A V K w q')) (P i' q'))) (@ex A (fun v' : A => and (@eq (proc this W A) q (@Ret this W A v')) (P i' (@Ret this V A v')))))))) *)
        s1 \In coherent ->
(* Goal: @InMem (PCM.sort (union_mapPCM Label dstatelet)) (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Mem state (PredPredType state) (Coh W)) *)
(* Goal: @always_sc this W A (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Inject this W A V K w q') scs (fun (m : state) (q : proc this W A) => @ex (UMDef.tp Label dstatelet) (fun i' : UMDef.tp Label dstatelet => @ex (UMDef.tp Label dstatelet) (fun j' : UMDef.tp Label dstatelet => and4 (@eq state m (@PCM.join (union_mapPCM Label dstatelet) i' j')) (@InMem (UMDef.tp Label dstatelet) i' (@Mem state (PredPredType state) (Coh V))) (network_rely (@inj_ext V W K w) this j j') (or (@ex (proc this V A) (fun q' : proc this V A => and (@eq (proc this W A) q (@Inject this W A V K w q')) (P i' q'))) (@ex A (fun v' : A => and (@eq (proc this W A) q (@Ret this W A v')) (P i' (@Ret this V A v')))))))) *)
        (forall s2, network_rely W this s1 s2 -> exists S : a_safe a s2,
        P s2 (Act a) /\
(* Goal: @InMem (PCM.sort (union_mapPCM Label dstatelet)) (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Mem state (PredPredType state) (Coh W)) *)
(* Goal: @always_sc this W A (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Inject this W A V K w q') scs (fun (m : state) (q : proc this W A) => @ex (UMDef.tp Label dstatelet) (fun i' : UMDef.tp Label dstatelet => @ex (UMDef.tp Label dstatelet) (fun j' : UMDef.tp Label dstatelet => and4 (@eq state m (@PCM.join (union_mapPCM Label dstatelet) i' j')) (@InMem (UMDef.tp Label dstatelet) i' (@Mem state (PredPredType state) (Coh V))) (network_rely (@inj_ext V W K w) this j j') (or (@ex (proc this V A) (fun q' : proc this V A => and (@eq (proc this W A) q (@Inject this W A V K w q')) (P i' q'))) (@ex A (fun v' : A => and (@eq (proc this W A) q (@Ret this W A v')) (P i' (@Ret this V A v')))))))) *)
        forall s3 v s4, a_step S s3 v -> 
(* Goal: @InMem (PCM.sort (union_mapPCM Label dstatelet)) (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Mem state (PredPredType state) (Coh W)) *)
(* Goal: @always_sc this W A (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Inject this W A V K w q') scs (fun (m : state) (q : proc this W A) => @ex (UMDef.tp Label dstatelet) (fun i' : UMDef.tp Label dstatelet => @ex (UMDef.tp Label dstatelet) (fun j' : UMDef.tp Label dstatelet => and4 (@eq state m (@PCM.join (union_mapPCM Label dstatelet) i' j')) (@InMem (UMDef.tp Label dstatelet) i' (@Mem state (PredPredType state) (Coh V))) (network_rely (@inj_ext V W K w) this j j') (or (@ex (proc this V A) (fun q' : proc this V A => and (@eq (proc this W A) q (@Inject this W A V K w q')) (P i' q'))) (@ex A (fun v' : A => and (@eq (proc this W A) q (@Ret this W A v')) (P i' (@Ret this V A v')))))))) *)
                        network_rely W this s3 s4 -> P s4 (Ret v)) ->
        always s1 (Act a) P. 
Proof.
move=>C H [|sc scs]; split=>// s2; case/H=>// H1[H2]H3//. 
(* Goal: forall _ : @ex A (fun v' : A => and (@eq (proc this (mkWorld (@ProtocolWithIndInv pr I ii)) A) (@Ret this (mkWorld (@ProtocolWithIndInv pr I ii)) A v) (@Ret this (mkWorld (@ProtocolWithIndInv pr I ii)) A v')) (forall (v : A) (_ : @eq (proc this (mkWorld pr) A) (@Ret this (mkWorld pr) A v') (@Ret this (mkWorld pr) A v)), P v s)), P v s *)
split=>//; first by case: sc.
(* Goal: @InMem (PCM.sort (union_mapPCM Label dstatelet)) (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Mem state (PredPredType state) (Coh W)) *)
(* Goal: @always_sc this W A (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Inject this W A V K w q') scs (fun (m : state) (q : proc this W A) => @ex (UMDef.tp Label dstatelet) (fun i' : UMDef.tp Label dstatelet => @ex (UMDef.tp Label dstatelet) (fun j' : UMDef.tp Label dstatelet => and4 (@eq state m (@PCM.join (union_mapPCM Label dstatelet) i' j')) (@InMem (UMDef.tp Label dstatelet) i' (@Mem state (PredPredType state) (Coh V))) (network_rely (@inj_ext V W K w) this j j') (or (@ex (proc this V A) (fun q' : proc this V A => and (@eq (proc this W A) q (@Inject this W A V K w q')) (P i' q'))) (@ex A (fun v' : A => and (@eq (proc this W A) q (@Ret this W A v')) (P i' (@Ret this V A v')))))))) *)
move=>s3 q /stepAct [v][pf][_ -> St].
(* Goal: @always_sc this W A (@PCM.join (union_mapPCM Label dstatelet) i2 y1) (@Inject this W A V K w q') scs (fun (m : state) (q : proc this W A) => @ex (UMDef.tp Label dstatelet) (fun i' : UMDef.tp Label dstatelet => @ex (UMDef.tp Label dstatelet) (fun j' : UMDef.tp Label dstatelet => and4 (@eq state m (@PCM.join (union_mapPCM Label dstatelet) i' j')) (@InMem (UMDef.tp Label dstatelet) i' (@Mem state (PredPredType state) (Coh V))) (network_rely (@inj_ext V W K w) this j j') (or (@ex (proc this V A) (fun q' : proc this V A => and (@eq (proc this W A) q (@Inject this W A V K w q')) (P i' q'))) (@ex A (fun v' : A => and (@eq (proc this W A) q (@Ret this W A v')) (P i' (@Ret this V A v')))))))) *)
rewrite (pf_irr H1 pf) in H3.
(* Goal: P v s *)
apply: alw_ret'; last by move=>s4; apply: H3 St.
(* Goal: forall _ : @ex A (fun v' : A => and (@eq (proc this (mkWorld (@ProtocolWithIndInv pr I ii)) A) (@Ret this (mkWorld (@ProtocolWithIndInv pr I ii)) A v) (@Ret this (mkWorld (@ProtocolWithIndInv pr I ii)) A v')) (forall (v : A) (_ : @eq (proc this (mkWorld pr) A) (@Ret this (mkWorld pr) A v') (@Ret this (mkWorld pr) A v)), P v s)), P v s *)
by case: (step_coh (a_step_sem St)).
Qed.

(* The predicates, corresponding to weakest postconditions, necessary
   for defining safe executions of programs.  *)

Notation alwsafe_sc s p scs := (always_sc s p scs (fun _ _ => True)).
Notation alwsafe s p := (always s p (fun _ _ => True)).


(* Goal: @InMem (PCM.sort (union_mapPCM Label dstatelet)) (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Mem state (PredPredType state) (Coh W)) *)
(* Goal: @always_sc this W A (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Inject this W A V K w q') scs (fun (m : state) (q : proc this W A) => @ex (UMDef.tp Label dstatelet) (fun i' : UMDef.tp Label dstatelet => @ex (UMDef.tp Label dstatelet) (fun j' : UMDef.tp Label dstatelet => and4 (@eq state m (@PCM.join (union_mapPCM Label dstatelet) i' j')) (@InMem (UMDef.tp Label dstatelet) i' (@Mem state (PredPredType state) (Coh V))) (network_rely (@inj_ext V W K w) this j j') (or (@ex (proc this V A) (fun q' : proc this V A => and (@eq (proc this W A) q (@Inject this W A V K w q')) (P i' q'))) (@ex A (fun v' : A => and (@eq (proc this W A) q (@Ret this W A v')) (P i' (@Ret this V A v')))))))) *)
Lemma alw_imp' A s (p : proc A) scs (P1 P2 : state -> proc A -> Prop) : 
(* Goal: @InMem (PCM.sort (union_mapPCM Label dstatelet)) (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Mem state (PredPredType state) (Coh W)) *)
(* Goal: @always_sc this W A (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Inject this W A V K w q') scs (fun (m : state) (q : proc this W A) => @ex (UMDef.tp Label dstatelet) (fun i' : UMDef.tp Label dstatelet => @ex (UMDef.tp Label dstatelet) (fun j' : UMDef.tp Label dstatelet => and4 (@eq state m (@PCM.join (union_mapPCM Label dstatelet) i' j')) (@InMem (UMDef.tp Label dstatelet) i' (@Mem state (PredPredType state) (Coh V))) (network_rely (@inj_ext V W K w) this j j') (or (@ex (proc this V A) (fun q' : proc this V A => and (@eq (proc this W A) q (@Inject this W A V K w q')) (P i' q'))) (@ex A (fun v' : A => and (@eq (proc this W A) q (@Ret this W A v')) (P i' (@Ret this V A v')))))))) *)
         (forall s p, s \In coherent -> P1 s p -> P2 s p) -> 
(* Goal: @InMem (PCM.sort (union_mapPCM Label dstatelet)) (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Mem state (PredPredType state) (Coh W)) *)
(* Goal: @always_sc this W A (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Inject this W A V K w q') scs (fun (m : state) (q : proc this W A) => @ex (UMDef.tp Label dstatelet) (fun i' : UMDef.tp Label dstatelet => @ex (UMDef.tp Label dstatelet) (fun j' : UMDef.tp Label dstatelet => and4 (@eq state m (@PCM.join (union_mapPCM Label dstatelet) i' j')) (@InMem (UMDef.tp Label dstatelet) i' (@Mem state (PredPredType state) (Coh V))) (network_rely (@inj_ext V W K w) this j j') (or (@ex (proc this V A) (fun q' : proc this V A => and (@eq (proc this W A) q (@Inject this W A V K w q')) (P i' q'))) (@ex A (fun v' : A => and (@eq (proc this W A) q (@Ret this W A v')) (P i' (@Ret this V A v')))))))) *)
         always_sc s p scs P1 -> always_sc s p scs P2.
Proof.
(* Goal: forall (_ : forall (s : state) (p : @proc this W A) (_ : @InMem state s (@Mem state (PredPredType state) (Coh W))) (_ : P1 s p), P2 s p) (_ : @always_sc A s p scs P1), @always_sc A s p scs P2 *)
elim: scs s p=>[|sc scs IH] s p /= I; case=>C L; split=>// s2 E.
(* Goal: @InMem (PCM.sort (union_mapPCM Label dstatelet)) (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Mem state (PredPredType state) (Coh W)) *)
(* Goal: @always_sc this W A (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Inject this W A V K w q') scs (fun (m : state) (q : proc this W A) => @ex (UMDef.tp Label dstatelet) (fun i' : UMDef.tp Label dstatelet => @ex (UMDef.tp Label dstatelet) (fun j' : UMDef.tp Label dstatelet => and4 (@eq state m (@PCM.join (union_mapPCM Label dstatelet) i' j')) (@InMem (UMDef.tp Label dstatelet) i' (@Mem state (PredPredType state) (Coh V))) (network_rely (@inj_ext V W K w) this j j') (or (@ex (proc this V A) (fun q' : proc this V A => and (@eq (proc this W A) q (@Inject this W A V K w q')) (P i' q'))) (@ex A (fun v' : A => and (@eq (proc this W A) q (@Ret this W A v')) (P i' (@Ret this V A v')))))))) *)
- by apply: I (L _ E); case/rely_coh: E.
(* Goal: P v s *)
case/L: (E)=>S H T; split=>//; first by apply: I H; case/rely_coh: E. 
(* Goal: forall _ : @ex A (fun v' : A => and (@eq (proc this (mkWorld (@ProtocolWithIndInv pr I ii)) A) (@Ret this (mkWorld (@ProtocolWithIndInv pr I ii)) A v) (@Ret this (mkWorld (@ProtocolWithIndInv pr I ii)) A v')) (forall (v : A) (_ : @eq (proc this (mkWorld pr) A) (@Ret this (mkWorld pr) A v') (@Ret this (mkWorld pr) A v)), P v s)), P v s *)
by move=>s3 q; move/T; apply: IH I. 
Qed.

(* Goal: @InMem (PCM.sort (union_mapPCM Label dstatelet)) (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Mem state (PredPredType state) (Coh W)) *)
(* Goal: @always_sc this W A (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Inject this W A V K w q') scs (fun (m : state) (q : proc this W A) => @ex (UMDef.tp Label dstatelet) (fun i' : UMDef.tp Label dstatelet => @ex (UMDef.tp Label dstatelet) (fun j' : UMDef.tp Label dstatelet => and4 (@eq state m (@PCM.join (union_mapPCM Label dstatelet) i' j')) (@InMem (UMDef.tp Label dstatelet) i' (@Mem state (PredPredType state) (Coh V))) (network_rely (@inj_ext V W K w) this j j') (or (@ex (proc this V A) (fun q' : proc this V A => and (@eq (proc this W A) q (@Inject this W A V K w q')) (P i' q'))) (@ex A (fun v' : A => and (@eq (proc this W A) q (@Ret this W A v')) (P i' (@Ret this V A v')))))))) *)
Lemma alw_imp A s (p : proc A) (P1 P2 : state -> proc A -> Prop) : 
(* Goal: @InMem (PCM.sort (union_mapPCM Label dstatelet)) (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Mem state (PredPredType state) (Coh W)) *)
(* Goal: @always_sc this W A (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Inject this W A V K w q') scs (fun (m : state) (q : proc this W A) => @ex (UMDef.tp Label dstatelet) (fun i' : UMDef.tp Label dstatelet => @ex (UMDef.tp Label dstatelet) (fun j' : UMDef.tp Label dstatelet => and4 (@eq state m (@PCM.join (union_mapPCM Label dstatelet) i' j')) (@InMem (UMDef.tp Label dstatelet) i' (@Mem state (PredPredType state) (Coh V))) (network_rely (@inj_ext V W K w) this j j') (or (@ex (proc this V A) (fun q' : proc this V A => and (@eq (proc this W A) q (@Inject this W A V K w q')) (P i' q'))) (@ex A (fun v' : A => and (@eq (proc this W A) q (@Ret this W A v')) (P i' (@Ret this V A v')))))))) *)
        (forall s p, s \In coherent -> P1 s p -> P2 s p) -> 
(* Goal: @InMem (PCM.sort (union_mapPCM Label dstatelet)) (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Mem state (PredPredType state) (Coh W)) *)
(* Goal: @always_sc this W A (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Inject this W A V K w q') scs (fun (m : state) (q : proc this W A) => @ex (UMDef.tp Label dstatelet) (fun i' : UMDef.tp Label dstatelet => @ex (UMDef.tp Label dstatelet) (fun j' : UMDef.tp Label dstatelet => and4 (@eq state m (@PCM.join (union_mapPCM Label dstatelet) i' j')) (@InMem (UMDef.tp Label dstatelet) i' (@Mem state (PredPredType state) (Coh V))) (network_rely (@inj_ext V W K w) this j j') (or (@ex (proc this V A) (fun q' : proc this V A => and (@eq (proc this W A) q (@Inject this W A V K w q')) (P i' q'))) (@ex A (fun v' : A => and (@eq (proc this W A) q (@Ret this W A v')) (P i' (@Ret this V A v')))))))) *)
        always s p P1 -> always s p P2.
Proof. by move=>I H ps; apply: alw_imp' I _. Qed.

(* always commutes with universals, so we cann pull them out *)

(* Goal: @InMem (PCM.sort (union_mapPCM Label dstatelet)) (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Mem state (PredPredType state) (Coh W)) *)
(* Goal: @always_sc this W A (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Inject this W A V K w q') scs (fun (m : state) (q : proc this W A) => @ex (UMDef.tp Label dstatelet) (fun i' : UMDef.tp Label dstatelet => @ex (UMDef.tp Label dstatelet) (fun j' : UMDef.tp Label dstatelet => and4 (@eq state m (@PCM.join (union_mapPCM Label dstatelet) i' j')) (@InMem (UMDef.tp Label dstatelet) i' (@Mem state (PredPredType state) (Coh V))) (network_rely (@inj_ext V W K w) this j j') (or (@ex (proc this V A) (fun q' : proc this V A => and (@eq (proc this W A) q (@Inject this W A V K w q')) (P i' q'))) (@ex A (fun v' : A => and (@eq (proc this W A) q (@Ret this W A v')) (P i' (@Ret this V A v')))))))) *)
Lemma alwA' A B s (p : proc A) scs (P : B -> state -> proc A -> Prop) : 
(* Goal: @InMem (PCM.sort (union_mapPCM Label dstatelet)) (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Mem state (PredPredType state) (Coh W)) *)
(* Goal: @always_sc this W A (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Inject this W A V K w q') scs (fun (m : state) (q : proc this W A) => @ex (UMDef.tp Label dstatelet) (fun i' : UMDef.tp Label dstatelet => @ex (UMDef.tp Label dstatelet) (fun j' : UMDef.tp Label dstatelet => and4 (@eq state m (@PCM.join (union_mapPCM Label dstatelet) i' j')) (@InMem (UMDef.tp Label dstatelet) i' (@Mem state (PredPredType state) (Coh V))) (network_rely (@inj_ext V W K w) this j j') (or (@ex (proc this V A) (fun q' : proc this V A => and (@eq (proc this W A) q (@Inject this W A V K w q')) (P i' q'))) (@ex A (fun v' : A => and (@eq (proc this W A) q (@Ret this W A v')) (P i' (@Ret this V A v')))))))) *)
        alwsafe_sc s p scs ->
(* Goal: @InMem (PCM.sort (union_mapPCM Label dstatelet)) (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Mem state (PredPredType state) (Coh W)) *)
(* Goal: @always_sc this W A (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Inject this W A V K w q') scs (fun (m : state) (q : proc this W A) => @ex (UMDef.tp Label dstatelet) (fun i' : UMDef.tp Label dstatelet => @ex (UMDef.tp Label dstatelet) (fun j' : UMDef.tp Label dstatelet => and4 (@eq state m (@PCM.join (union_mapPCM Label dstatelet) i' j')) (@InMem (UMDef.tp Label dstatelet) i' (@Mem state (PredPredType state) (Coh V))) (network_rely (@inj_ext V W K w) this j j') (or (@ex (proc this V A) (fun q' : proc this V A => and (@eq (proc this W A) q (@Inject this W A V K w q')) (P i' q'))) (@ex A (fun v' : A => and (@eq (proc this W A) q (@Ret this W A v')) (P i' (@Ret this V A v')))))))) *)
        (always_sc s p scs (fun s' p' => forall x, P x s' p') <->
         forall x, always_sc s p scs (fun s' p' => P x s' p')).
Proof.
(* Goal: @InMem (PCM.sort (union_mapPCM Label dstatelet)) (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Mem state (PredPredType state) (Coh W)) *)
(* Goal: @always_sc this W A (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Inject this W A V K w q') scs (fun (m : state) (q : proc this W A) => @ex (UMDef.tp Label dstatelet) (fun i' : UMDef.tp Label dstatelet => @ex (UMDef.tp Label dstatelet) (fun j' : UMDef.tp Label dstatelet => and4 (@eq state m (@PCM.join (union_mapPCM Label dstatelet) i' j')) (@InMem (UMDef.tp Label dstatelet) i' (@Mem state (PredPredType state) (Coh V))) (network_rely (@inj_ext V W K w) this j j') (or (@ex (proc this V A) (fun q' : proc this V A => and (@eq (proc this W A) q (@Inject this W A V K w q')) (P i' q'))) (@ex A (fun v' : A => and (@eq (proc this W A) q (@Ret this W A v')) (P i' (@Ret this V A v')))))))) *)
move=>Ls; split=>[{Ls}|]. 
(* Goal: @InMem (PCM.sort (union_mapPCM Label dstatelet)) (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Mem state (PredPredType state) (Coh W)) *)
(* Goal: @always_sc this W A (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Inject this W A V K w q') scs (fun (m : state) (q : proc this W A) => @ex (UMDef.tp Label dstatelet) (fun i' : UMDef.tp Label dstatelet => @ex (UMDef.tp Label dstatelet) (fun j' : UMDef.tp Label dstatelet => and4 (@eq state m (@PCM.join (union_mapPCM Label dstatelet) i' j')) (@InMem (UMDef.tp Label dstatelet) i' (@Mem state (PredPredType state) (Coh V))) (network_rely (@inj_ext V W K w) this j j') (or (@ex (proc this V A) (fun q' : proc this V A => and (@eq (proc this W A) q (@Inject this W A V K w q')) (P i' q'))) (@ex A (fun v' : A => and (@eq (proc this W A) q (@Ret this W A v')) (P i' (@Ret this V A v')))))))) *)
- elim: scs s p=>[|sc scs IH] s p /= [C Et x]; split=>// s2; move/Et=>//.
(* Goal: forall _ : @ex A (fun v' : A => and (@eq (proc this (mkWorld (@ProtocolWithIndInv pr I ii)) A) (@Ret this (mkWorld (@ProtocolWithIndInv pr I ii)) A v) (@Ret this (mkWorld (@ProtocolWithIndInv pr I ii)) A v')) (forall (v : A) (_ : @eq (proc this (mkWorld pr) A) (@Ret this (mkWorld pr) A v') (@Ret this (mkWorld pr) A v)), P v s)), P v s *)
  by case=>S Ha L; split=>// s3 q; move/L/IH.
(* Goal: forall (_ : @always_sc A s p scs (fun (s' : state) (p' : @proc this W A) => forall _ : P, Q s' p')) (_ : P), @always_sc A s p scs (fun (s' : state) (p' : @proc this W A) => Q s' p') *)
(* Goal: forall _ : forall _ : P, @always_sc A s p scs (fun (s' : state) (p' : @proc this W A) => Q s' p'), @always_sc A s p scs (fun (s' : state) (p' : @proc this W A) => forall _ : P, Q s' p') *)
elim: scs s p Ls=>[|sc scs IH] s p /= [C Et Ha]; split=>// s2 E.
(* Goal: @InMem (PCM.sort (union_mapPCM Label dstatelet)) (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Mem state (PredPredType state) (Coh W)) *)
(* Goal: @always_sc this W A (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Inject this W A V K w q') scs (fun (m : state) (q : proc this W A) => @ex (UMDef.tp Label dstatelet) (fun i' : UMDef.tp Label dstatelet => @ex (UMDef.tp Label dstatelet) (fun j' : UMDef.tp Label dstatelet => and4 (@eq state m (@PCM.join (union_mapPCM Label dstatelet) i' j')) (@InMem (UMDef.tp Label dstatelet) i' (@Mem state (PredPredType state) (Coh V))) (network_rely (@inj_ext V W K w) this j j') (or (@ex (proc this V A) (fun q' : proc this V A => and (@eq (proc this W A) q (@Inject this W A V K w q')) (P i' q'))) (@ex A (fun v' : A => and (@eq (proc this W A) q (@Ret this W A v')) (P i' (@Ret this V A v')))))))) *)
- by move=>x; case: (Ha x)=>_; apply. 
(* Goal: and (network_rely V this s1 s2) (network_rely (@inj_ext V W K w) this s1' s2') *)
(* Goal: forall (_ : and (@eq state (@PCM.join (union_mapPCM Label dstatelet) s1 s1') (@PCM.join (union_mapPCM Label dstatelet) s2 s2')) (@InMem state (@PCM.join (union_mapPCM Label dstatelet) s1 s1') (@Mem state (PredPredType state) (Coh W)))) (_ : @InMem state s1 (@Mem state (PredPredType state) (Coh V))) (_ : @InMem state s2 (@Mem state (PredPredType state) (Coh V))), and (network_rely V this s1 s2) (network_rely (@inj_ext V W K w) this s1' s2') *)
case/Et: (E)=>/= S _ L; split=>//.
(* Goal: @InMem (PCM.sort (union_mapPCM Label dstatelet)) (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Mem state (PredPredType state) (Coh W)) *)
(* Goal: @always_sc this W A (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Inject this W A V K w q') scs (fun (m : state) (q : proc this W A) => @ex (UMDef.tp Label dstatelet) (fun i' : UMDef.tp Label dstatelet => @ex (UMDef.tp Label dstatelet) (fun j' : UMDef.tp Label dstatelet => and4 (@eq state m (@PCM.join (union_mapPCM Label dstatelet) i' j')) (@InMem (UMDef.tp Label dstatelet) i' (@Mem state (PredPredType state) (Coh V))) (network_rely (@inj_ext V W K w) this j j') (or (@ex (proc this V A) (fun q' : proc this V A => and (@eq (proc this W A) q (@Inject this W A V K w q')) (P i' q'))) (@ex A (fun v' : A => and (@eq (proc this W A) q (@Ret this W A v')) (P i' (@Ret this V A v')))))))) *)
- by move=>x; case: (Ha x)=>_; case/(_ _ E). 
(* Goal: P v s *)
move=>s3 q T; apply: IH; first by apply: L T.
(* Goal: forall _ : @ex A (fun v' : A => and (@eq (proc this (mkWorld (@ProtocolWithIndInv pr I ii)) A) (@Ret this (mkWorld (@ProtocolWithIndInv pr I ii)) A v) (@Ret this (mkWorld (@ProtocolWithIndInv pr I ii)) A v')) (forall (v : A) (_ : @eq (proc this (mkWorld pr) A) (@Ret this (mkWorld pr) A v') (@Ret this (mkWorld pr) A v)), P v s)), P v s *)
by move=>x; case: (Ha x)=>_; case/(_ _ E)=>_ _; apply. 
Qed.

(* Goal: @InMem (PCM.sort (union_mapPCM Label dstatelet)) (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Mem state (PredPredType state) (Coh W)) *)
(* Goal: @always_sc this W A (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Inject this W A V K w q') scs (fun (m : state) (q : proc this W A) => @ex (UMDef.tp Label dstatelet) (fun i' : UMDef.tp Label dstatelet => @ex (UMDef.tp Label dstatelet) (fun j' : UMDef.tp Label dstatelet => and4 (@eq state m (@PCM.join (union_mapPCM Label dstatelet) i' j')) (@InMem (UMDef.tp Label dstatelet) i' (@Mem state (PredPredType state) (Coh V))) (network_rely (@inj_ext V W K w) this j j') (or (@ex (proc this V A) (fun q' : proc this V A => and (@eq (proc this W A) q (@Inject this W A V K w q')) (P i' q'))) (@ex A (fun v' : A => and (@eq (proc this W A) q (@Ret this W A v')) (P i' (@Ret this V A v')))))))) *)
Lemma alwA A B s (p : proc A) (P : B -> state -> proc A -> Prop) : 
(* Goal: @InMem (PCM.sort (union_mapPCM Label dstatelet)) (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Mem state (PredPredType state) (Coh W)) *)
(* Goal: @always_sc this W A (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Inject this W A V K w q') scs (fun (m : state) (q : proc this W A) => @ex (UMDef.tp Label dstatelet) (fun i' : UMDef.tp Label dstatelet => @ex (UMDef.tp Label dstatelet) (fun j' : UMDef.tp Label dstatelet => and4 (@eq state m (@PCM.join (union_mapPCM Label dstatelet) i' j')) (@InMem (UMDef.tp Label dstatelet) i' (@Mem state (PredPredType state) (Coh V))) (network_rely (@inj_ext V W K w) this j j') (or (@ex (proc this V A) (fun q' : proc this V A => and (@eq (proc this W A) q (@Inject this W A V K w q')) (P i' q'))) (@ex A (fun v' : A => and (@eq (proc this W A) q (@Ret this W A v')) (P i' (@Ret this V A v')))))))) *)
        alwsafe s p ->
(* Goal: @InMem (PCM.sort (union_mapPCM Label dstatelet)) (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Mem state (PredPredType state) (Coh W)) *)
(* Goal: @always_sc this W A (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Inject this W A V K w q') scs (fun (m : state) (q : proc this W A) => @ex (UMDef.tp Label dstatelet) (fun i' : UMDef.tp Label dstatelet => @ex (UMDef.tp Label dstatelet) (fun j' : UMDef.tp Label dstatelet => and4 (@eq state m (@PCM.join (union_mapPCM Label dstatelet) i' j')) (@InMem (UMDef.tp Label dstatelet) i' (@Mem state (PredPredType state) (Coh V))) (network_rely (@inj_ext V W K w) this j j') (or (@ex (proc this V A) (fun q' : proc this V A => and (@eq (proc this W A) q (@Inject this W A V K w q')) (P i' q'))) (@ex A (fun v' : A => and (@eq (proc this W A) q (@Ret this W A v')) (P i' (@Ret this V A v')))))))) *)
        (always s p (fun s' p' => forall x, P x s' p') <->
         forall x, always s p (fun s' p' => P x s' p')).
Proof.
(* Goal: forall _ : @always A s p (fun (_ : state) (_ : @proc this W A) => True), iff (@always_sc A s p scs (fun (s' : state) (p' : @proc this W A) => forall _ : P, Q s' p')) (forall _ : P, @always_sc A s p scs (fun (s' : state) (p' : @proc this W A) => Q s' p')) *)
move=>Ls; split.
(* Goal: @InMem (PCM.sort (union_mapPCM Label dstatelet)) (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Mem state (PredPredType state) (Coh W)) *)
(* Goal: @always_sc this W A (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Inject this W A V K w q') scs (fun (m : state) (q : proc this W A) => @ex (UMDef.tp Label dstatelet) (fun i' : UMDef.tp Label dstatelet => @ex (UMDef.tp Label dstatelet) (fun j' : UMDef.tp Label dstatelet => and4 (@eq state m (@PCM.join (union_mapPCM Label dstatelet) i' j')) (@InMem (UMDef.tp Label dstatelet) i' (@Mem state (PredPredType state) (Coh V))) (network_rely (@inj_ext V W K w) this j j') (or (@ex (proc this V A) (fun q' : proc this V A => and (@eq (proc this W A) q (@Inject this W A V K w q')) (P i' q'))) (@ex A (fun v' : A => and (@eq (proc this W A) q (@Ret this W A v')) (P i' (@Ret this V A v')))))))) *)
- by move=>H x ps; move: x; apply/(alwA' _ (Ls ps)).
(* Goal: forall _ : @ex A (fun v' : A => and (@eq (proc this (mkWorld (@ProtocolWithIndInv pr I ii)) A) (@Ret this (mkWorld (@ProtocolWithIndInv pr I ii)) A v) (@Ret this (mkWorld (@ProtocolWithIndInv pr I ii)) A v')) (forall (v : A) (_ : @eq (proc this (mkWorld pr) A) (@Ret this (mkWorld pr) A v') (@Ret this (mkWorld pr) A v)), P v s)), P v s *)
by move=>H ps; apply/(alwA' _ (Ls ps))=>x; apply: H.
Qed.

Arguments alwA [A B s p P].

(* always commutes with implication, so we can weaken the postconditions *)

(* Goal: @InMem (PCM.sort (union_mapPCM Label dstatelet)) (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Mem state (PredPredType state) (Coh W)) *)
(* Goal: @always_sc this W A (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Inject this W A V K w q') scs (fun (m : state) (q : proc this W A) => @ex (UMDef.tp Label dstatelet) (fun i' : UMDef.tp Label dstatelet => @ex (UMDef.tp Label dstatelet) (fun j' : UMDef.tp Label dstatelet => and4 (@eq state m (@PCM.join (union_mapPCM Label dstatelet) i' j')) (@InMem (UMDef.tp Label dstatelet) i' (@Mem state (PredPredType state) (Coh V))) (network_rely (@inj_ext V W K w) this j j') (or (@ex (proc this V A) (fun q' : proc this V A => and (@eq (proc this W A) q (@Inject this W A V K w q')) (P i' q'))) (@ex A (fun v' : A => and (@eq (proc this W A) q (@Ret this W A v')) (P i' (@Ret this V A v')))))))) *)
Lemma alwI' A s (p : proc A) scs (P : Prop) (Q : state -> proc A -> Prop) : 
(* Goal: @InMem (PCM.sort (union_mapPCM Label dstatelet)) (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Mem state (PredPredType state) (Coh W)) *)
(* Goal: @always_sc this W A (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Inject this W A V K w q') scs (fun (m : state) (q : proc this W A) => @ex (UMDef.tp Label dstatelet) (fun i' : UMDef.tp Label dstatelet => @ex (UMDef.tp Label dstatelet) (fun j' : UMDef.tp Label dstatelet => and4 (@eq state m (@PCM.join (union_mapPCM Label dstatelet) i' j')) (@InMem (UMDef.tp Label dstatelet) i' (@Mem state (PredPredType state) (Coh V))) (network_rely (@inj_ext V W K w) this j j') (or (@ex (proc this V A) (fun q' : proc this V A => and (@eq (proc this W A) q (@Inject this W A V K w q')) (P i' q'))) (@ex A (fun v' : A => and (@eq (proc this W A) q (@Ret this W A v')) (P i' (@Ret this V A v')))))))) *)
        alwsafe s p ->
(* Goal: @InMem (PCM.sort (union_mapPCM Label dstatelet)) (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Mem state (PredPredType state) (Coh W)) *)
(* Goal: @always_sc this W A (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Inject this W A V K w q') scs (fun (m : state) (q : proc this W A) => @ex (UMDef.tp Label dstatelet) (fun i' : UMDef.tp Label dstatelet => @ex (UMDef.tp Label dstatelet) (fun j' : UMDef.tp Label dstatelet => and4 (@eq state m (@PCM.join (union_mapPCM Label dstatelet) i' j')) (@InMem (UMDef.tp Label dstatelet) i' (@Mem state (PredPredType state) (Coh V))) (network_rely (@inj_ext V W K w) this j j') (or (@ex (proc this V A) (fun q' : proc this V A => and (@eq (proc this W A) q (@Inject this W A V K w q')) (P i' q'))) (@ex A (fun v' : A => and (@eq (proc this W A) q (@Ret this W A v')) (P i' (@Ret this V A v')))))))) *)
        (always_sc s p scs (fun s' p' => P -> Q s' p') <->
(* Goal: @InMem (PCM.sort (union_mapPCM Label dstatelet)) (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Mem state (PredPredType state) (Coh W)) *)
(* Goal: @always_sc this W A (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Inject this W A V K w q') scs (fun (m : state) (q : proc this W A) => @ex (UMDef.tp Label dstatelet) (fun i' : UMDef.tp Label dstatelet => @ex (UMDef.tp Label dstatelet) (fun j' : UMDef.tp Label dstatelet => and4 (@eq state m (@PCM.join (union_mapPCM Label dstatelet) i' j')) (@InMem (UMDef.tp Label dstatelet) i' (@Mem state (PredPredType state) (Coh V))) (network_rely (@inj_ext V W K w) this j j') (or (@ex (proc this V A) (fun q' : proc this V A => and (@eq (proc this W A) q (@Inject this W A V K w q')) (P i' q'))) (@ex A (fun v' : A => and (@eq (proc this W A) q (@Ret this W A v')) (P i' (@Ret this V A v')))))))) *)
         (P -> always_sc s p scs (fun s' p' => Q s' p'))).
Proof.
(* Goal: forall _ : @always A s p (fun (_ : state) (_ : @proc this W A) => True), iff (@always_sc A s p scs (fun (s' : state) (p' : @proc this W A) => forall _ : P, Q s' p')) (forall _ : P, @always_sc A s p scs (fun (s' : state) (p' : @proc this W A) => Q s' p')) *)
move=>Ls; split.
(* Goal: @InMem (PCM.sort (union_mapPCM Label dstatelet)) (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Mem state (PredPredType state) (Coh W)) *)
(* Goal: @always_sc this W A (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Inject this W A V K w q') scs (fun (m : state) (q : proc this W A) => @ex (UMDef.tp Label dstatelet) (fun i' : UMDef.tp Label dstatelet => @ex (UMDef.tp Label dstatelet) (fun j' : UMDef.tp Label dstatelet => and4 (@eq state m (@PCM.join (union_mapPCM Label dstatelet) i' j')) (@InMem (UMDef.tp Label dstatelet) i' (@Mem state (PredPredType state) (Coh V))) (network_rely (@inj_ext V W K w) this j j') (or (@ex (proc this V A) (fun q' : proc this V A => and (@eq (proc this W A) q (@Inject this W A V K w q')) (P i' q'))) (@ex A (fun v' : A => and (@eq (proc this W A) q (@Ret this W A v')) (P i' (@Ret this V A v')))))))) *)
- elim: scs s p Ls=>[|sc scs IH] s p Ls /= [C Et H]; split=>// s2.
(* Goal: @InMem (PCM.sort (union_mapPCM Label dstatelet)) (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Mem state (PredPredType state) (Coh W)) *)
(* Goal: @always_sc this W A (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Inject this W A V K w q') scs (fun (m : state) (q : proc this W A) => @ex (UMDef.tp Label dstatelet) (fun i' : UMDef.tp Label dstatelet => @ex (UMDef.tp Label dstatelet) (fun j' : UMDef.tp Label dstatelet => and4 (@eq state m (@PCM.join (union_mapPCM Label dstatelet) i' j')) (@InMem (UMDef.tp Label dstatelet) i' (@Mem state (PredPredType state) (Coh V))) (network_rely (@inj_ext V W K w) this j j') (or (@ex (proc this V A) (fun q' : proc this V A => and (@eq (proc this W A) q (@Inject this W A V K w q')) (P i' q'))) (@ex A (fun v' : A => and (@eq (proc this W A) q (@Ret this W A v')) (P i' (@Ret this V A v')))))))) *)
  - by move/Et; apply.
(* Goal: forall (s3 : state) (q : @proc this W A) (_ : @pstep this W A s2 p sc s3 q), @always_sc A s3 q scs (fun (s' : state) (p' : @proc this W A) => forall _ : P, Q s' p') *)
  move=>M; move: (alw_envs Ls M)=>{Ls} Ls.
(* Goal: and (network_rely V this s1 s2) (network_rely (@inj_ext V W K w) this s1' s2') *)
(* Goal: forall (_ : and (@eq state (@PCM.join (union_mapPCM Label dstatelet) s1 s1') (@PCM.join (union_mapPCM Label dstatelet) s2 s2')) (@InMem state (@PCM.join (union_mapPCM Label dstatelet) s1 s1') (@Mem state (PredPredType state) (Coh W)))) (_ : @InMem state s1 (@Mem state (PredPredType state) (Coh V))) (_ : @InMem state s2 (@Mem state (PredPredType state) (Coh V))), and (network_rely V this s1 s2) (network_rely (@inj_ext V W K w) this s1' s2') *)
  case/Et: M=>H1 /(_ H) H2 H3; split=>// s3 q T.
(* Goal: forall _ : @ex A (fun v' : A => and (@eq (proc this (mkWorld (@ProtocolWithIndInv pr I ii)) A) (@Ret this (mkWorld (@ProtocolWithIndInv pr I ii)) A v) (@Ret this (mkWorld (@ProtocolWithIndInv pr I ii)) A v')) (forall (v : A) (_ : @eq (proc this (mkWorld pr) A) (@Ret this (mkWorld pr) A v') (@Ret this (mkWorld pr) A v)), P v s)), P v s *)
  by apply: IH H; [apply: alw_step T | apply: H3].
elim: scs s p Ls=>[|sc scs IH] s p /= Ls H; 
move: (alw_coh Ls)=>C; split=>// s2 M; first by case/H=>_; apply. 
(* Goal: @ex (PCM.sort (union_mapPCM Label dstatelet)) (fun i' : PCM.sort (union_mapPCM Label dstatelet) => @ex (PCM.sort (union_mapPCM Label dstatelet)) (fun j' : PCM.sort (union_mapPCM Label dstatelet) => and4 (@eq state (@PCM.join (union_mapPCM Label dstatelet) i1 j1) (@PCM.join (union_mapPCM Label dstatelet) i' j')) (@InMem (PCM.sort (union_mapPCM Label dstatelet)) i' (@Mem state (PredPredType state) (Coh V))) (network_rely (@inj_ext V W K w) this j j') (P v i'))) *)
move: (alw_envs Ls M)=>{Ls} Ls.
(* Goal: P v s *)
split; first by move/alw_safe: Ls.  
(* Goal: @InMem (PCM.sort (union_mapPCM Label dstatelet)) (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Mem state (PredPredType state) (Coh W)) *)
(* Goal: @always_sc this W A (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Inject this W A V K w q') scs (fun (m : state) (q : proc this W A) => @ex (UMDef.tp Label dstatelet) (fun i' : UMDef.tp Label dstatelet => @ex (UMDef.tp Label dstatelet) (fun j' : UMDef.tp Label dstatelet => and4 (@eq state m (@PCM.join (union_mapPCM Label dstatelet) i' j')) (@InMem (UMDef.tp Label dstatelet) i' (@Mem state (PredPredType state) (Coh V))) (network_rely (@inj_ext V W K w) this j j') (or (@ex (proc this V A) (fun q' : proc this V A => and (@eq (proc this W A) q (@Inject this W A V K w q')) (P i' q'))) (@ex A (fun v' : A => and (@eq (proc this W A) q (@Ret this W A v')) (P i' (@Ret this V A v')))))))) *)
- by case/H=>_; case/(_ _  M). 
(* Goal: forall (s3 : state) (q : @proc this W A) (_ : @pstep this W A s2 p sc s3 q), @always_sc A s3 q scs (fun (s' : state) (p' : @proc this W A) => forall _ : P, Q s' p') *)
move=>s3 q T; move: (alw_step Ls T)=>{Ls} Ls.
(* Goal: forall _ : @ex A (fun v' : A => and (@eq (proc this (mkWorld (@ProtocolWithIndInv pr I ii)) A) (@Ret this (mkWorld (@ProtocolWithIndInv pr I ii)) A v) (@Ret this (mkWorld (@ProtocolWithIndInv pr I ii)) A v')) (forall (v : A) (_ : @eq (proc this (mkWorld pr) A) (@Ret this (mkWorld pr) A v') (@Ret this (mkWorld pr) A v)), P v s)), P v s *)
by apply: IH Ls _; case/H=>_; case/(_ _ M)=>_ _; apply. 
Qed.

(* Goal: @InMem (PCM.sort (union_mapPCM Label dstatelet)) (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Mem state (PredPredType state) (Coh W)) *)
(* Goal: @always_sc this W A (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Inject this W A V K w q') scs (fun (m : state) (q : proc this W A) => @ex (UMDef.tp Label dstatelet) (fun i' : UMDef.tp Label dstatelet => @ex (UMDef.tp Label dstatelet) (fun j' : UMDef.tp Label dstatelet => and4 (@eq state m (@PCM.join (union_mapPCM Label dstatelet) i' j')) (@InMem (UMDef.tp Label dstatelet) i' (@Mem state (PredPredType state) (Coh V))) (network_rely (@inj_ext V W K w) this j j') (or (@ex (proc this V A) (fun q' : proc this V A => and (@eq (proc this W A) q (@Inject this W A V K w q')) (P i' q'))) (@ex A (fun v' : A => and (@eq (proc this W A) q (@Ret this W A v')) (P i' (@Ret this V A v')))))))) *)
Lemma alwI A s (p : proc A) (P : Prop) (Q : state -> proc A -> Prop) : 
(* Goal: @InMem (PCM.sort (union_mapPCM Label dstatelet)) (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Mem state (PredPredType state) (Coh W)) *)
(* Goal: @always_sc this W A (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Inject this W A V K w q') scs (fun (m : state) (q : proc this W A) => @ex (UMDef.tp Label dstatelet) (fun i' : UMDef.tp Label dstatelet => @ex (UMDef.tp Label dstatelet) (fun j' : UMDef.tp Label dstatelet => and4 (@eq state m (@PCM.join (union_mapPCM Label dstatelet) i' j')) (@InMem (UMDef.tp Label dstatelet) i' (@Mem state (PredPredType state) (Coh V))) (network_rely (@inj_ext V W K w) this j j') (or (@ex (proc this V A) (fun q' : proc this V A => and (@eq (proc this W A) q (@Inject this W A V K w q')) (P i' q'))) (@ex A (fun v' : A => and (@eq (proc this W A) q (@Ret this W A v')) (P i' (@Ret this V A v')))))))) *)
        alwsafe s p ->
(* Goal: @InMem (PCM.sort (union_mapPCM Label dstatelet)) (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Mem state (PredPredType state) (Coh W)) *)
(* Goal: @always_sc this W A (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Inject this W A V K w q') scs (fun (m : state) (q : proc this W A) => @ex (UMDef.tp Label dstatelet) (fun i' : UMDef.tp Label dstatelet => @ex (UMDef.tp Label dstatelet) (fun j' : UMDef.tp Label dstatelet => and4 (@eq state m (@PCM.join (union_mapPCM Label dstatelet) i' j')) (@InMem (UMDef.tp Label dstatelet) i' (@Mem state (PredPredType state) (Coh V))) (network_rely (@inj_ext V W K w) this j j') (or (@ex (proc this V A) (fun q' : proc this V A => and (@eq (proc this W A) q (@Inject this W A V K w q')) (P i' q'))) (@ex A (fun v' : A => and (@eq (proc this W A) q (@Ret this W A v')) (P i' (@Ret this V A v')))))))) *)
         always s p (fun s' p' => P -> Q s' p') <->
(* Goal: @InMem (PCM.sort (union_mapPCM Label dstatelet)) (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Mem state (PredPredType state) (Coh W)) *)
(* Goal: @always_sc this W A (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Inject this W A V K w q') scs (fun (m : state) (q : proc this W A) => @ex (UMDef.tp Label dstatelet) (fun i' : UMDef.tp Label dstatelet => @ex (UMDef.tp Label dstatelet) (fun j' : UMDef.tp Label dstatelet => and4 (@eq state m (@PCM.join (union_mapPCM Label dstatelet) i' j')) (@InMem (UMDef.tp Label dstatelet) i' (@Mem state (PredPredType state) (Coh V))) (network_rely (@inj_ext V W K w) this j j') (or (@ex (proc this V A) (fun q' : proc this V A => and (@eq (proc this W A) q (@Inject this W A V K w q')) (P i' q'))) (@ex A (fun v' : A => and (@eq (proc this W A) q (@Ret this W A v')) (P i' (@Ret this V A v')))))))) *)
         (P -> always s p (fun s' p' => Q s' p')). 
Proof.
(* Goal: P v s *)
move=>Ls; split; first by move=>H Hp scs; apply/alwI': Hp.
(* Goal: forall _ : @ex A (fun v' : A => and (@eq (proc this (mkWorld (@ProtocolWithIndInv pr I ii)) A) (@Ret this (mkWorld (@ProtocolWithIndInv pr I ii)) A v) (@Ret this (mkWorld (@ProtocolWithIndInv pr I ii)) A v')) (forall (v : A) (_ : @eq (proc this (mkWorld pr) A) (@Ret this (mkWorld pr) A v') (@Ret this (mkWorld pr) A v)), P v s)), P v s *)
by move=>H scs; apply/alwI'=>//; move/H; move/(_ scs).
Qed.

Arguments alwI [A s p P Q].


Lemma alw_bnd A B (p1 : proc A) (p12 : proc B) pp2 s1 
(* Goal: @InMem (PCM.sort (union_mapPCM Label dstatelet)) (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Mem state (PredPredType state) (Coh W)) *)
(* Goal: @always_sc this W A (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Inject this W A V K w q') scs (fun (m : state) (q : proc this W A) => @ex (UMDef.tp Label dstatelet) (fun i' : UMDef.tp Label dstatelet => @ex (UMDef.tp Label dstatelet) (fun j' : UMDef.tp Label dstatelet => and4 (@eq state m (@PCM.join (union_mapPCM Label dstatelet) i' j')) (@InMem (UMDef.tp Label dstatelet) i' (@Mem state (PredPredType state) (Coh V))) (network_rely (@inj_ext V W K w) this j j') (or (@ex (proc this V A) (fun q' : proc this V A => and (@eq (proc this W A) q (@Inject this W A V K w q')) (P i' q'))) (@ex A (fun v' : A => and (@eq (proc this W A) q (@Ret this W A v')) (P i' (@Ret this V A v')))))))) *)
                 (P : state -> B -> Prop) :
(* Goal: @InMem (PCM.sort (union_mapPCM Label dstatelet)) (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Mem state (PredPredType state) (Coh W)) *)
(* Goal: @always_sc this W A (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Inject this W A V K w q') scs (fun (m : state) (q : proc this W A) => @ex (UMDef.tp Label dstatelet) (fun i' : UMDef.tp Label dstatelet => @ex (UMDef.tp Label dstatelet) (fun j' : UMDef.tp Label dstatelet => and4 (@eq state m (@PCM.join (union_mapPCM Label dstatelet) i' j')) (@InMem (UMDef.tp Label dstatelet) i' (@Mem state (PredPredType state) (Coh V))) (network_rely (@inj_ext V W K w) this j j') (or (@ex (proc this V A) (fun q' : proc this V A => and (@eq (proc this W A) q (@Inject this W A V K w q')) (P i' q'))) (@ex A (fun v' : A => and (@eq (proc this W A) q (@Ret this W A v')) (P i' (@Ret this V A v')))))))) *)
        p12 \In pcat p1 pp2 -> 
        always s1 p1 (fun s2 p2 =>
          (* p2 is a process resulting from executing p1 *)              
(* Goal: @InMem (PCM.sort (union_mapPCM Label dstatelet)) (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Mem state (PredPredType state) (Coh W)) *)
(* Goal: @always_sc this W A (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Inject this W A V K w q') scs (fun (m : state) (q : proc this W A) => @ex (UMDef.tp Label dstatelet) (fun i' : UMDef.tp Label dstatelet => @ex (UMDef.tp Label dstatelet) (fun j' : UMDef.tp Label dstatelet => and4 (@eq state m (@PCM.join (union_mapPCM Label dstatelet) i' j')) (@InMem (UMDef.tp Label dstatelet) i' (@Mem state (PredPredType state) (Coh V))) (network_rely (@inj_ext V W K w) this j j') (or (@ex (proc this V A) (fun q' : proc this V A => and (@eq (proc this W A) q (@Inject this W A V K w q')) (P i' q'))) (@ex A (fun v' : A => and (@eq (proc this W A) q (@Ret this W A v')) (P i' (@Ret this V A v')))))))) *)
          forall p v, p2 = Ret v -> p \In pp2 v -> 
           (* Now assume p2 is a return and p is its continuation, 
              so we proceed until we reach the return *)
(* Goal: @InMem (PCM.sort (union_mapPCM Label dstatelet)) (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Mem state (PredPredType state) (Coh W)) *)
(* Goal: @always_sc this W A (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Inject this W A V K w q') scs (fun (m : state) (q : proc this W A) => @ex (UMDef.tp Label dstatelet) (fun i' : UMDef.tp Label dstatelet => @ex (UMDef.tp Label dstatelet) (fun j' : UMDef.tp Label dstatelet => and4 (@eq state m (@PCM.join (union_mapPCM Label dstatelet) i' j')) (@InMem (UMDef.tp Label dstatelet) i' (@Mem state (PredPredType state) (Coh V))) (network_rely (@inj_ext V W K w) this j j') (or (@ex (proc this V A) (fun q' : proc this V A => and (@eq (proc this W A) q (@Inject this W A V K w q')) (P i' q'))) (@ex A (fun v' : A => and (@eq (proc this W A) q (@Ret this W A v')) (P i' (@Ret this V A v')))))))) *)
           always s2 p (fun s q => forall v, q = Ret v -> P s v)) ->
(* Goal: @InMem (PCM.sort (union_mapPCM Label dstatelet)) (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Mem state (PredPredType state) (Coh W)) *)
(* Goal: @always_sc this W A (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Inject this W A V K w q') scs (fun (m : state) (q : proc this W A) => @ex (UMDef.tp Label dstatelet) (fun i' : UMDef.tp Label dstatelet => @ex (UMDef.tp Label dstatelet) (fun j' : UMDef.tp Label dstatelet => and4 (@eq state m (@PCM.join (union_mapPCM Label dstatelet) i' j')) (@InMem (UMDef.tp Label dstatelet) i' (@Mem state (PredPredType state) (Coh V))) (network_rely (@inj_ext V W K w) this j j') (or (@ex (proc this V A) (fun q' : proc this V A => and (@eq (proc this W A) q (@Inject this W A V K w q')) (P i' q'))) (@ex A (fun v' : A => and (@eq (proc this W A) q (@Ret this W A v')) (P i' (@Ret this V A v')))))))) *)
        always s1 p12 (fun s p => forall v, p = Ret v -> P s v).
Proof.
(* Goal: @ex (PCM.sort (union_mapPCM Label dstatelet)) (fun i' : PCM.sort (union_mapPCM Label dstatelet) => @ex (PCM.sort (union_mapPCM Label dstatelet)) (fun j' : PCM.sort (union_mapPCM Label dstatelet) => and4 (@eq state (@PCM.join (union_mapPCM Label dstatelet) i1 j1) (@PCM.join (union_mapPCM Label dstatelet) i' j')) (@InMem (PCM.sort (union_mapPCM Label dstatelet)) i' (@Mem state (PredPredType state) (Coh V))) (network_rely (@inj_ext V W K w) this j j') (P v i'))) *)
move=>Tc Ls scs.
(* Goal: @always_sc B s1 p12 scs (fun (s : state) (p : @proc this W B) => forall (v : B) (_ : @eq (@proc this W B) p (@Ret this W B v)), P s v) *)
elim: scs s1 p1 p12 Tc Ls=>[|sc scs IH] s1 p1 p12 Tc Ls /=.
(* Goal: @InMem (PCM.sort (union_mapPCM Label dstatelet)) (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Mem state (PredPredType state) (Coh W)) *)
(* Goal: @always_sc this W A (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Inject this W A V K w q') scs (fun (m : state) (q : proc this W A) => @ex (UMDef.tp Label dstatelet) (fun i' : UMDef.tp Label dstatelet => @ex (UMDef.tp Label dstatelet) (fun j' : UMDef.tp Label dstatelet => and4 (@eq state m (@PCM.join (union_mapPCM Label dstatelet) i' j')) (@InMem (UMDef.tp Label dstatelet) i' (@Mem state (PredPredType state) (Coh V))) (network_rely (@inj_ext V W K w) this j j') (or (@ex (proc this V A) (fun q' : proc this V A => and (@eq (proc this W A) q (@Inject this W A V K w q')) (P i' q'))) (@ex A (fun v' : A => and (@eq (proc this W A) q (@Ret this W A v')) (P i' (@Ret this V A v')))))))) *)
- by split=>[|s2]; [apply: alw_coh Ls | case: Tc=>k [->]].
(* Goal: P v s *)
split=>[|s2 E]; first by apply: alw_coh Ls.
(* Goal: @InMem (PCM.sort (union_mapPCM Label dstatelet)) (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Mem state (PredPredType state) (Coh W)) *)
(* Goal: @always_sc this W A (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Inject this W A V K w q') scs (fun (m : state) (q : proc this W A) => @ex (UMDef.tp Label dstatelet) (fun i' : UMDef.tp Label dstatelet => @ex (UMDef.tp Label dstatelet) (fun j' : UMDef.tp Label dstatelet => and4 (@eq state m (@PCM.join (union_mapPCM Label dstatelet) i' j')) (@InMem (UMDef.tp Label dstatelet) i' (@Mem state (PredPredType state) (Coh V))) (network_rely (@inj_ext V W K w) this j j') (or (@ex (proc this V A) (fun q' : proc this V A => and (@eq (proc this W A) q (@Inject this W A V K w q')) (P i' q'))) (@ex A (fun v' : A => and (@eq (proc this W A) q (@Ret this W A v')) (P i' (@Ret this V A v')))))))) *)
case: Tc IH=>k [->{p12}] H IH.
(* Goal: P v s *)
split=>//; last first.
(* Goal: @InMem (PCM.sort (union_mapPCM Label dstatelet)) (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Mem state (PredPredType state) (Coh W)) *)
(* Goal: @always_sc this W A (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Inject this W A V K w q') scs (fun (m : state) (q : proc this W A) => @ex (UMDef.tp Label dstatelet) (fun i' : UMDef.tp Label dstatelet => @ex (UMDef.tp Label dstatelet) (fun j' : UMDef.tp Label dstatelet => and4 (@eq state m (@PCM.join (union_mapPCM Label dstatelet) i' j')) (@InMem (UMDef.tp Label dstatelet) i' (@Mem state (PredPredType state) (Coh V))) (network_rely (@inj_ext V W K w) this j j') (or (@ex (proc this V A) (fun q' : proc this V A => and (@eq (proc this W A) q (@Inject this W A V K w q')) (P i' q'))) (@ex A (fun v' : A => and (@eq (proc this W A) q (@Ret this W A v')) (P i' (@Ret this V A v')))))))) *)
- move=>s3 q T; case/stepSeq: T Ls.
(* Goal: @InMem (PCM.sort (union_mapPCM Label dstatelet)) (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Mem state (PredPredType state) (Coh W)) *)
(* Goal: @always_sc this W A (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Inject this W A V K w q') scs (fun (m : state) (q : proc this W A) => @ex (UMDef.tp Label dstatelet) (fun i' : UMDef.tp Label dstatelet => @ex (UMDef.tp Label dstatelet) (fun j' : UMDef.tp Label dstatelet => and4 (@eq state m (@PCM.join (union_mapPCM Label dstatelet) i' j')) (@InMem (UMDef.tp Label dstatelet) i' (@Mem state (PredPredType state) (Coh V))) (network_rely (@inj_ext V W K w) this j j') (or (@ex (proc this V A) (fun q' : proc this V A => and (@eq (proc this W A) q (@Inject this W A V K w q')) (P i' q'))) (@ex A (fun v' : A => and (@eq (proc this W A) q (@Ret this W A v')) (P i' (@Ret this V A v')))))))) *)
  - case=>v [_ ->->-> C]; move/alw_refl/(_ _ _ (erefl _)). 
(* Goal: forall _ : @ex A (fun v' : A => and (@eq (proc this (mkWorld (@ProtocolWithIndInv pr I ii)) A) (@Ret this (mkWorld (@ProtocolWithIndInv pr I ii)) A v) (@Ret this (mkWorld (@ProtocolWithIndInv pr I ii)) A v')) (forall (v : A) (_ : @eq (proc this (mkWorld pr) A) (@Ret this (mkWorld pr) A v') (@Ret this (mkWorld pr) A v)), P v s)), P v s *)
    by move/(_ _ (H v))/alw_envs; apply. 
(* Goal: @InMem (PCM.sort (union_mapPCM Label dstatelet)) (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Mem state (PredPredType state) (Coh W)) *)
(* Goal: @always_sc this W A (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Inject this W A V K w q') scs (fun (m : state) (q : proc this W A) => @ex (UMDef.tp Label dstatelet) (fun i' : UMDef.tp Label dstatelet => @ex (UMDef.tp Label dstatelet) (fun j' : UMDef.tp Label dstatelet => and4 (@eq state m (@PCM.join (union_mapPCM Label dstatelet) i' j')) (@InMem (UMDef.tp Label dstatelet) i' (@Mem state (PredPredType state) (Coh V))) (network_rely (@inj_ext V W K w) this j j') (or (@ex (proc this V A) (fun q' : proc this V A => and (@eq (proc this W A) q (@Inject this W A V K w q')) (P i' q'))) (@ex A (fun v' : A => and (@eq (proc this W A) q (@Ret this W A v')) (P i' (@Ret this V A v')))))))) *)
  case=>sc' [p'][_ ->{q}] T; move/alw_envs/(_ E)/alw_step.
(* Goal: forall _ : @ex A (fun v' : A => and (@eq (proc this (mkWorld (@ProtocolWithIndInv pr I ii)) A) (@Ret this (mkWorld (@ProtocolWithIndInv pr I ii)) A v) (@Ret this (mkWorld (@ProtocolWithIndInv pr I ii)) A v')) (forall (v : A) (_ : @eq (proc this (mkWorld pr) A) (@Ret this (mkWorld pr) A v') (@Ret this (mkWorld pr) A v)), P v s)), P v s *)
  by move/(_ _ _ _ T)/IH; apply; exists k.
(* Goal: @ex (PCM.sort (union_mapPCM Label dstatelet)) (fun i' : PCM.sort (union_mapPCM Label dstatelet) => @ex (PCM.sort (union_mapPCM Label dstatelet)) (fun j' : PCM.sort (union_mapPCM Label dstatelet) => and4 (@eq state (@PCM.join (union_mapPCM Label dstatelet) i1 j1) (@PCM.join (union_mapPCM Label dstatelet) i' j')) (@InMem (PCM.sort (union_mapPCM Label dstatelet)) i' (@Mem state (PredPredType state) (Coh V))) (network_rely (@inj_ext V W K w) this j j') (P v i'))) *)
move/(alw_envs Ls): E=>{Ls} Ls. 
have Ls': always s2 p1 (fun s2 p2 =>
(* Goal: @InMem (PCM.sort (union_mapPCM Label dstatelet)) (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Mem state (PredPredType state) (Coh W)) *)
(* Goal: @always_sc this W A (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Inject this W A V K w q') scs (fun (m : state) (q : proc this W A) => @ex (UMDef.tp Label dstatelet) (fun i' : UMDef.tp Label dstatelet => @ex (UMDef.tp Label dstatelet) (fun j' : UMDef.tp Label dstatelet => and4 (@eq state m (@PCM.join (union_mapPCM Label dstatelet) i' j')) (@InMem (UMDef.tp Label dstatelet) i' (@Mem state (PredPredType state) (Coh V))) (network_rely (@inj_ext V W K w) this j j') (or (@ex (proc this V A) (fun q' : proc this V A => and (@eq (proc this W A) q (@Inject this W A V K w q')) (P i' q'))) (@ex A (fun v' : A => and (@eq (proc this W A) q (@Ret this W A v')) (P i' (@Ret this V A v')))))))) *)
  forall sc p v, p2 = Ret v -> p \In pp2 v -> safe p sc s2).
(* Goal: @InMem (PCM.sort (union_mapPCM Label dstatelet)) (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Mem state (PredPredType state) (Coh W)) *)
(* Goal: @always_sc this W A (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Inject this W A V K w q') scs (fun (m : state) (q : proc this W A) => @ex (UMDef.tp Label dstatelet) (fun i' : UMDef.tp Label dstatelet => @ex (UMDef.tp Label dstatelet) (fun j' : UMDef.tp Label dstatelet => and4 (@eq state m (@PCM.join (union_mapPCM Label dstatelet) i' j')) (@InMem (UMDef.tp Label dstatelet) i' (@Mem state (PredPredType state) (Coh V))) (network_rely (@inj_ext V W K w) this j j') (or (@ex (proc this V A) (fun q' : proc this V A => and (@eq (proc this W A) q (@Inject this W A V K w q')) (P i' q'))) (@ex A (fun v' : A => and (@eq (proc this W A) q (@Ret this W A v')) (P i' (@Ret this V A v')))))))) *)
- by apply: alw_imp Ls=>s p _ I sc' q v E; move/(I _ _ E)/alw_safe. 
(* Goal: P v s *)
case: sc=>//=; first by case: p1 {Ls} Ls'.
(* Goal: forall s : schedule, @safe this W A p1 s s2 *)
move=>sc; case: (Ls [:: sc])=>C.
(* Goal: forall _ : @ex A (fun v' : A => and (@eq (proc this (mkWorld (@ProtocolWithIndInv pr I ii)) A) (@Ret this (mkWorld (@ProtocolWithIndInv pr I ii)) A v) (@Ret this (mkWorld (@ProtocolWithIndInv pr I ii)) A v')) (forall (v : A) (_ : @eq (proc this (mkWorld pr) A) (@Ret this (mkWorld pr) A v') (@Ret this (mkWorld pr) A v)), P v s)), P v s *)
by move/(_ _ (rely_refl this C)); case.
Qed.

Lemma alwsafe_bnd A B (p1 : proc A) (p12 : proc B) s1 pp2 :
(* Goal: @InMem (PCM.sort (union_mapPCM Label dstatelet)) (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Mem state (PredPredType state) (Coh W)) *)
(* Goal: @always_sc this W A (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Inject this W A V K w q') scs (fun (m : state) (q : proc this W A) => @ex (UMDef.tp Label dstatelet) (fun i' : UMDef.tp Label dstatelet => @ex (UMDef.tp Label dstatelet) (fun j' : UMDef.tp Label dstatelet => and4 (@eq state m (@PCM.join (union_mapPCM Label dstatelet) i' j')) (@InMem (UMDef.tp Label dstatelet) i' (@Mem state (PredPredType state) (Coh V))) (network_rely (@inj_ext V W K w) this j j') (or (@ex (proc this V A) (fun q' : proc this V A => and (@eq (proc this W A) q (@Inject this W A V K w q')) (P i' q'))) (@ex A (fun v' : A => and (@eq (proc this W A) q (@Ret this W A v')) (P i' (@Ret this V A v')))))))) *)
        p12 \In pcat p1 pp2 ->
        always s1 p1 (fun s2 p2 =>
(* Goal: @InMem (PCM.sort (union_mapPCM Label dstatelet)) (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Mem state (PredPredType state) (Coh W)) *)
(* Goal: @always_sc this W A (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Inject this W A V K w q') scs (fun (m : state) (q : proc this W A) => @ex (UMDef.tp Label dstatelet) (fun i' : UMDef.tp Label dstatelet => @ex (UMDef.tp Label dstatelet) (fun j' : UMDef.tp Label dstatelet => and4 (@eq state m (@PCM.join (union_mapPCM Label dstatelet) i' j')) (@InMem (UMDef.tp Label dstatelet) i' (@Mem state (PredPredType state) (Coh V))) (network_rely (@inj_ext V W K w) this j j') (or (@ex (proc this V A) (fun q' : proc this V A => and (@eq (proc this W A) q (@Inject this W A V K w q')) (P i' q'))) (@ex A (fun v' : A => and (@eq (proc this W A) q (@Ret this W A v')) (P i' (@Ret this V A v')))))))) *)
          forall p v, p2 = Ret v -> p \In pp2 v -> alwsafe s2 p) ->
        alwsafe s1 p12.
Proof.
(* Goal: @ex (PCM.sort (union_mapPCM Label dstatelet)) (fun i' : PCM.sort (union_mapPCM Label dstatelet) => @ex (PCM.sort (union_mapPCM Label dstatelet)) (fun j' : PCM.sort (union_mapPCM Label dstatelet) => and4 (@eq state (@PCM.join (union_mapPCM Label dstatelet) i1 j1) (@PCM.join (union_mapPCM Label dstatelet) i' j')) (@InMem (PCM.sort (union_mapPCM Label dstatelet)) i' (@Mem state (PredPredType state) (Coh V))) (network_rely (@inj_ext V W K w) this j j') (P v i'))) *)
move=>T Ls.
(* Goal: @InMem (PCM.sort (union_mapPCM Label dstatelet)) (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Mem state (PredPredType state) (Coh W)) *)
(* Goal: @always_sc this W A (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Inject this W A V K w q') scs (fun (m : state) (q : proc this W A) => @ex (UMDef.tp Label dstatelet) (fun i' : UMDef.tp Label dstatelet => @ex (UMDef.tp Label dstatelet) (fun j' : UMDef.tp Label dstatelet => and4 (@eq state m (@PCM.join (union_mapPCM Label dstatelet) i' j')) (@InMem (UMDef.tp Label dstatelet) i' (@Mem state (PredPredType state) (Coh V))) (network_rely (@inj_ext V W K w) this j j') (or (@ex (proc this V A) (fun q' : proc this V A => and (@eq (proc this W A) q (@Inject this W A V K w q')) (P i' q'))) (@ex A (fun v' : A => and (@eq (proc this W A) q (@Ret this W A v')) (P i' (@Ret this V A v')))))))) *)
suff H: always s1 p12 (fun s p => forall v, p = Ret v -> True).
(* Goal: @InMem (PCM.sort (union_mapPCM Label dstatelet)) (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Mem state (PredPredType state) (Coh W)) *)
(* Goal: @always_sc this W A (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Inject this W A V K w q') scs (fun (m : state) (q : proc this W A) => @ex (UMDef.tp Label dstatelet) (fun i' : UMDef.tp Label dstatelet => @ex (UMDef.tp Label dstatelet) (fun j' : UMDef.tp Label dstatelet => and4 (@eq state m (@PCM.join (union_mapPCM Label dstatelet) i' j')) (@InMem (UMDef.tp Label dstatelet) i' (@Mem state (PredPredType state) (Coh V))) (network_rely (@inj_ext V W K w) this j j') (or (@ex (proc this V A) (fun q' : proc this V A => and (@eq (proc this W A) q (@Inject this W A V K w q')) (P i' q'))) (@ex A (fun v' : A => and (@eq (proc this W A) q (@Ret this W A v')) (P i' (@Ret this V A v')))))))) *)
- by apply: alw_imp H.
(* Goal: @always B s1 p12 (fun (_ : state) (p : @proc this W B) => forall (v : B) (_ : @eq (@proc this W B) p (@Ret this W B v)), True) *)
apply: alw_bnd T _; apply: alw_imp Ls=>s p _ I q v H.
(* Goal: forall _ : @ex A (fun v' : A => and (@eq (proc this (mkWorld (@ProtocolWithIndInv pr I ii)) A) (@Ret this (mkWorld (@ProtocolWithIndInv pr I ii)) A v) (@Ret this (mkWorld (@ProtocolWithIndInv pr I ii)) A v')) (forall (v : A) (_ : @eq (proc this (mkWorld pr) A) (@Ret this (mkWorld pr) A v') (@Ret this (mkWorld pr) A v)), P v s)), P v s *)
by move/(I _ _ H); apply: alw_imp.
Qed.

(* this suggest capturing the pattern by means of a new definition *)

(* Goal: @InMem (PCM.sort (union_mapPCM Label dstatelet)) (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Mem state (PredPredType state) (Coh W)) *)
(* Goal: @always_sc this W A (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Inject this W A V K w q') scs (fun (m : state) (q : proc this W A) => @ex (UMDef.tp Label dstatelet) (fun i' : UMDef.tp Label dstatelet => @ex (UMDef.tp Label dstatelet) (fun j' : UMDef.tp Label dstatelet => and4 (@eq state m (@PCM.join (union_mapPCM Label dstatelet) i' j')) (@InMem (UMDef.tp Label dstatelet) i' (@Mem state (PredPredType state) (Coh V))) (network_rely (@inj_ext V W K w) this j j') (or (@ex (proc this V A) (fun q' : proc this V A => and (@eq (proc this W A) q (@Inject this W A V K w q')) (P i' q'))) (@ex A (fun v' : A => and (@eq (proc this W A) q (@Ret this W A v')) (P i' (@Ret this V A v')))))))) *)
Definition after A s (p : proc A) (P : A -> state -> Prop) := 
(* Goal: @InMem (PCM.sort (union_mapPCM Label dstatelet)) (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Mem state (PredPredType state) (Coh W)) *)
(* Goal: @always_sc this W A (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Inject this W A V K w q') scs (fun (m : state) (q : proc this W A) => @ex (UMDef.tp Label dstatelet) (fun i' : UMDef.tp Label dstatelet => @ex (UMDef.tp Label dstatelet) (fun j' : UMDef.tp Label dstatelet => and4 (@eq state m (@PCM.join (union_mapPCM Label dstatelet) i' j')) (@InMem (UMDef.tp Label dstatelet) i' (@Mem state (PredPredType state) (Coh V))) (network_rely (@inj_ext V W K w) this j j') (or (@ex (proc this V A) (fun q' : proc this V A => and (@eq (proc this W A) q (@Inject this W A V K w q')) (P i' q'))) (@ex A (fun v' : A => and (@eq (proc this W A) q (@Ret this W A v')) (P i' (@Ret this V A v')))))))) *)
  always s p (fun s2 p2 => forall v, p2 = Ret v -> P v s2).

Lemma aft_bnd A B (p1 : proc A) (p12 : proc B) pp2 s1 P :
(* Goal: @InMem (PCM.sort (union_mapPCM Label dstatelet)) (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Mem state (PredPredType state) (Coh W)) *)
(* Goal: @always_sc this W A (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Inject this W A V K w q') scs (fun (m : state) (q : proc this W A) => @ex (UMDef.tp Label dstatelet) (fun i' : UMDef.tp Label dstatelet => @ex (UMDef.tp Label dstatelet) (fun j' : UMDef.tp Label dstatelet => and4 (@eq state m (@PCM.join (union_mapPCM Label dstatelet) i' j')) (@InMem (UMDef.tp Label dstatelet) i' (@Mem state (PredPredType state) (Coh V))) (network_rely (@inj_ext V W K w) this j j') (or (@ex (proc this V A) (fun q' : proc this V A => and (@eq (proc this W A) q (@Inject this W A V K w q')) (P i' q'))) (@ex A (fun v' : A => and (@eq (proc this W A) q (@Ret this W A v')) (P i' (@Ret this V A v')))))))) *)
        p12 \In pcat p1 pp2 -> 
        after s1 p1 (fun v s => 
(* Goal: @InMem (PCM.sort (union_mapPCM Label dstatelet)) (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Mem state (PredPredType state) (Coh W)) *)
(* Goal: @always_sc this W A (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Inject this W A V K w q') scs (fun (m : state) (q : proc this W A) => @ex (UMDef.tp Label dstatelet) (fun i' : UMDef.tp Label dstatelet => @ex (UMDef.tp Label dstatelet) (fun j' : UMDef.tp Label dstatelet => and4 (@eq state m (@PCM.join (union_mapPCM Label dstatelet) i' j')) (@InMem (UMDef.tp Label dstatelet) i' (@Mem state (PredPredType state) (Coh V))) (network_rely (@inj_ext V W K w) this j j') (or (@ex (proc this V A) (fun q' : proc this V A => and (@eq (proc this W A) q (@Inject this W A V K w q')) (P i' q'))) (@ex A (fun v' : A => and (@eq (proc this W A) q (@Ret this W A v')) (P i' (@Ret this V A v')))))))) *)
          forall p, p \In pp2 v -> after s p P) ->
        after s1 p12 P.
Proof. 
(* Goal: forall (_ : @InMem state i (@Mem state (PredPredType state) (Coh (mkWorld (@ProtocolWithIndInv pr I ii))))) (_ : @after this (mkWorld pr) A i p P), @after this (mkWorld (@ProtocolWithIndInv pr I ii)) A i (@WithInv this (mkWorld (@ProtocolWithIndInv pr I ii)) A pr I ii (@Logic.eq_refl world (mkWorld (@ProtocolWithIndInv pr I ii))) p) (fun (v : A) (m : state) => and (@InMem state m (@Mem state (PredPredType state) (Coh (mkWorld (@ProtocolWithIndInv pr I ii))))) (P v m)) *)
move=>T H; apply: alw_bnd T _.
(* Goal: forall _ : @ex A (fun v' : A => and (@eq (proc this (mkWorld (@ProtocolWithIndInv pr I ii)) A) (@Ret this (mkWorld (@ProtocolWithIndInv pr I ii)) A v) (@Ret this (mkWorld (@ProtocolWithIndInv pr I ii)) A v')) (forall (v : A) (_ : @eq (proc this (mkWorld pr) A) (@Ret this (mkWorld pr) A v') (@Ret this (mkWorld pr) A v)), P v s)), P v s *)
by apply: alw_imp H=>s p _ I q v E; move/(I v E).
Qed.



(* Goal: @InMem (PCM.sort (union_mapPCM Label dstatelet)) (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Mem state (PredPredType state) (Coh W)) *)
(* Goal: @always_sc this W A (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Inject this W A V K w q') scs (fun (m : state) (q : proc this W A) => @ex (UMDef.tp Label dstatelet) (fun i' : UMDef.tp Label dstatelet => @ex (UMDef.tp Label dstatelet) (fun j' : UMDef.tp Label dstatelet => and4 (@eq state m (@PCM.join (union_mapPCM Label dstatelet) i' j')) (@InMem (UMDef.tp Label dstatelet) i' (@Mem state (PredPredType state) (Coh V))) (network_rely (@inj_ext V W K w) this j j') (or (@ex (proc this V A) (fun q' : proc this V A => and (@eq (proc this W A) q (@Inject this W A V K w q')) (P i' q'))) (@ex A (fun v' : A => and (@eq (proc this W A) q (@Ret this W A v')) (P i' (@Ret this V A v')))))))) *)
Lemma aftI A s (p : proc A) (P : Prop) (Q : A -> state -> Prop) : 
(* Goal: @InMem (PCM.sort (union_mapPCM Label dstatelet)) (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Mem state (PredPredType state) (Coh W)) *)
(* Goal: @always_sc this W A (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Inject this W A V K w q') scs (fun (m : state) (q : proc this W A) => @ex (UMDef.tp Label dstatelet) (fun i' : UMDef.tp Label dstatelet => @ex (UMDef.tp Label dstatelet) (fun j' : UMDef.tp Label dstatelet => and4 (@eq state m (@PCM.join (union_mapPCM Label dstatelet) i' j')) (@InMem (UMDef.tp Label dstatelet) i' (@Mem state (PredPredType state) (Coh V))) (network_rely (@inj_ext V W K w) this j j') (or (@ex (proc this V A) (fun q' : proc this V A => and (@eq (proc this W A) q (@Inject this W A V K w q')) (P i' q'))) (@ex A (fun v' : A => and (@eq (proc this W A) q (@Ret this W A v')) (P i' (@Ret this V A v')))))))) *)
        alwsafe s p ->
(* Goal: @InMem (PCM.sort (union_mapPCM Label dstatelet)) (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Mem state (PredPredType state) (Coh W)) *)
(* Goal: @always_sc this W A (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Inject this W A V K w q') scs (fun (m : state) (q : proc this W A) => @ex (UMDef.tp Label dstatelet) (fun i' : UMDef.tp Label dstatelet => @ex (UMDef.tp Label dstatelet) (fun j' : UMDef.tp Label dstatelet => and4 (@eq state m (@PCM.join (union_mapPCM Label dstatelet) i' j')) (@InMem (UMDef.tp Label dstatelet) i' (@Mem state (PredPredType state) (Coh V))) (network_rely (@inj_ext V W K w) this j j') (or (@ex (proc this V A) (fun q' : proc this V A => and (@eq (proc this W A) q (@Inject this W A V K w q')) (P i' q'))) (@ex A (fun v' : A => and (@eq (proc this W A) q (@Ret this W A v')) (P i' (@Ret this V A v')))))))) *)
         after s p (fun v s' => P -> Q v s') <->
(* Goal: @InMem (PCM.sort (union_mapPCM Label dstatelet)) (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Mem state (PredPredType state) (Coh W)) *)
(* Goal: @always_sc this W A (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Inject this W A V K w q') scs (fun (m : state) (q : proc this W A) => @ex (UMDef.tp Label dstatelet) (fun i' : UMDef.tp Label dstatelet => @ex (UMDef.tp Label dstatelet) (fun j' : UMDef.tp Label dstatelet => and4 (@eq state m (@PCM.join (union_mapPCM Label dstatelet) i' j')) (@InMem (UMDef.tp Label dstatelet) i' (@Mem state (PredPredType state) (Coh V))) (network_rely (@inj_ext V W K w) this j j') (or (@ex (proc this V A) (fun q' : proc this V A => and (@eq (proc this W A) q (@Inject this W A V K w q')) (P i' q'))) (@ex A (fun v' : A => and (@eq (proc this W A) q (@Ret this W A v')) (P i' (@Ret this V A v')))))))) *)
         (P -> after s p (fun v s' => Q v s')).
Proof.
(* Goal: @InMem (PCM.sort (union_mapPCM Label dstatelet)) (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Mem state (PredPredType state) (Coh W)) *)
(* Goal: @always_sc this W A (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Inject this W A V K w q') scs (fun (m : state) (q : proc this W A) => @ex (UMDef.tp Label dstatelet) (fun i' : UMDef.tp Label dstatelet => @ex (UMDef.tp Label dstatelet) (fun j' : UMDef.tp Label dstatelet => and4 (@eq state m (@PCM.join (union_mapPCM Label dstatelet) i' j')) (@InMem (UMDef.tp Label dstatelet) i' (@Mem state (PredPredType state) (Coh V))) (network_rely (@inj_ext V W K w) this j j') (or (@ex (proc this V A) (fun q' : proc this V A => and (@eq (proc this W A) q (@Inject this W A V K w q')) (P i' q'))) (@ex A (fun v' : A => and (@eq (proc this W A) q (@Ret this W A v')) (P i' (@Ret this V A v')))))))) *)
move=>Ls; rewrite -(alwI Ls).
(* Goal: iff (@after A s p (fun (v : A) (s' : state) => forall x : B, P x v s')) (@always A s p (fun (s' : state) (p' : @proc this W A) => forall (x : B) (v : A) (_ : @eq (@proc this W A) p' (@Ret this W A v)), P x v s')) *)
split; apply: alw_imp=>t q _ I.
(* Goal: @InMem (PCM.sort (union_mapPCM Label dstatelet)) (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Mem state (PredPredType state) (Coh W)) *)
(* Goal: @always_sc this W A (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Inject this W A V K w q') scs (fun (m : state) (q : proc this W A) => @ex (UMDef.tp Label dstatelet) (fun i' : UMDef.tp Label dstatelet => @ex (UMDef.tp Label dstatelet) (fun j' : UMDef.tp Label dstatelet => and4 (@eq state m (@PCM.join (union_mapPCM Label dstatelet) i' j')) (@InMem (UMDef.tp Label dstatelet) i' (@Mem state (PredPredType state) (Coh V))) (network_rely (@inj_ext V W K w) this j j') (or (@ex (proc this V A) (fun q' : proc this V A => and (@eq (proc this W A) q (@Inject this W A V K w q')) (P i' q'))) (@ex A (fun v' : A => and (@eq (proc this W A) q (@Ret this W A v')) (P i' (@Ret this V A v')))))))) *)
- by move=>Hp v; move/I; apply. 
(* Goal: forall _ : @ex A (fun v' : A => and (@eq (proc this (mkWorld (@ProtocolWithIndInv pr I ii)) A) (@Ret this (mkWorld (@ProtocolWithIndInv pr I ii)) A v) (@Ret this (mkWorld (@ProtocolWithIndInv pr I ii)) A v')) (forall (v : A) (_ : @eq (proc this (mkWorld pr) A) (@Ret this (mkWorld pr) A v') (@Ret this (mkWorld pr) A v)), P v s)), P v s *)
by move=>v; move/I. 
Qed.

Lemma aft_alwsf A s (p : proc A) :
(* Goal: @InMem (PCM.sort (union_mapPCM Label dstatelet)) (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Mem state (PredPredType state) (Coh W)) *)
(* Goal: @always_sc this W A (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Inject this W A V K w q') scs (fun (m : state) (q : proc this W A) => @ex (UMDef.tp Label dstatelet) (fun i' : UMDef.tp Label dstatelet => @ex (UMDef.tp Label dstatelet) (fun j' : UMDef.tp Label dstatelet => and4 (@eq state m (@PCM.join (union_mapPCM Label dstatelet) i' j')) (@InMem (UMDef.tp Label dstatelet) i' (@Mem state (PredPredType state) (Coh V))) (network_rely (@inj_ext V W K w) this j j') (or (@ex (proc this V A) (fun q' : proc this V A => and (@eq (proc this W A) q (@Inject this W A V K w q')) (P i' q'))) (@ex A (fun v' : A => and (@eq (proc this W A) q (@Ret this W A v')) (P i' (@Ret this V A v')))))))) *)
        alwsafe s p <-> after s p (fun v s => True).
Proof. by split; apply: alw_imp. Qed.

(* Goal: @InMem (PCM.sort (union_mapPCM Label dstatelet)) (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Mem state (PredPredType state) (Coh W)) *)
(* Goal: @always_sc this W A (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Inject this W A V K w q') scs (fun (m : state) (q : proc this W A) => @ex (UMDef.tp Label dstatelet) (fun i' : UMDef.tp Label dstatelet => @ex (UMDef.tp Label dstatelet) (fun j' : UMDef.tp Label dstatelet => and4 (@eq state m (@PCM.join (union_mapPCM Label dstatelet) i' j')) (@InMem (UMDef.tp Label dstatelet) i' (@Mem state (PredPredType state) (Coh V))) (network_rely (@inj_ext V W K w) this j j') (or (@ex (proc this V A) (fun q' : proc this V A => and (@eq (proc this W A) q (@Inject this W A V K w q')) (P i' q'))) (@ex A (fun v' : A => and (@eq (proc this W A) q (@Ret this W A v')) (P i' (@Ret this V A v')))))))) *)
Lemma aft_imp A s (p : proc A) (P1 P2 : A -> state -> Prop) : 
(* Goal: @InMem (PCM.sort (union_mapPCM Label dstatelet)) (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Mem state (PredPredType state) (Coh W)) *)
(* Goal: @always_sc this W A (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Inject this W A V K w q') scs (fun (m : state) (q : proc this W A) => @ex (UMDef.tp Label dstatelet) (fun i' : UMDef.tp Label dstatelet => @ex (UMDef.tp Label dstatelet) (fun j' : UMDef.tp Label dstatelet => and4 (@eq state m (@PCM.join (union_mapPCM Label dstatelet) i' j')) (@InMem (UMDef.tp Label dstatelet) i' (@Mem state (PredPredType state) (Coh V))) (network_rely (@inj_ext V W K w) this j j') (or (@ex (proc this V A) (fun q' : proc this V A => and (@eq (proc this W A) q (@Inject this W A V K w q')) (P i' q'))) (@ex A (fun v' : A => and (@eq (proc this W A) q (@Ret this W A v')) (P i' (@Ret this V A v')))))))) *)
        (forall v s, s \In coherent -> 
(* Goal: @InMem (PCM.sort (union_mapPCM Label dstatelet)) (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Mem state (PredPredType state) (Coh W)) *)
(* Goal: @always_sc this W A (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Inject this W A V K w q') scs (fun (m : state) (q : proc this W A) => @ex (UMDef.tp Label dstatelet) (fun i' : UMDef.tp Label dstatelet => @ex (UMDef.tp Label dstatelet) (fun j' : UMDef.tp Label dstatelet => and4 (@eq state m (@PCM.join (union_mapPCM Label dstatelet) i' j')) (@InMem (UMDef.tp Label dstatelet) i' (@Mem state (PredPredType state) (Coh V))) (network_rely (@inj_ext V W K w) this j j') (or (@ex (proc this V A) (fun q' : proc this V A => and (@eq (proc this W A) q (@Inject this W A V K w q')) (P i' q'))) (@ex A (fun v' : A => and (@eq (proc this W A) q (@Ret this W A v')) (P i' (@Ret this V A v')))))))) *)
                     P1 v s -> P2 v s) -> 
(* Goal: @InMem (PCM.sort (union_mapPCM Label dstatelet)) (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Mem state (PredPredType state) (Coh W)) *)
(* Goal: @always_sc this W A (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Inject this W A V K w q') scs (fun (m : state) (q : proc this W A) => @ex (UMDef.tp Label dstatelet) (fun i' : UMDef.tp Label dstatelet => @ex (UMDef.tp Label dstatelet) (fun j' : UMDef.tp Label dstatelet => and4 (@eq state m (@PCM.join (union_mapPCM Label dstatelet) i' j')) (@InMem (UMDef.tp Label dstatelet) i' (@Mem state (PredPredType state) (Coh V))) (network_rely (@inj_ext V W K w) this j j') (or (@ex (proc this V A) (fun q' : proc this V A => and (@eq (proc this W A) q (@Inject this W A V K w q')) (P i' q'))) (@ex A (fun v' : A => and (@eq (proc this W A) q (@Ret this W A v')) (P i' (@Ret this V A v')))))))) *)
        after s p P1 -> after s p P2.
Proof. by move=>I; apply: alw_imp=>s1 p1 C H v; move/H; apply: I. Qed.

(* Goal: @InMem (PCM.sort (union_mapPCM Label dstatelet)) (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Mem state (PredPredType state) (Coh W)) *)
(* Goal: @always_sc this W A (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Inject this W A V K w q') scs (fun (m : state) (q : proc this W A) => @ex (UMDef.tp Label dstatelet) (fun i' : UMDef.tp Label dstatelet => @ex (UMDef.tp Label dstatelet) (fun j' : UMDef.tp Label dstatelet => and4 (@eq state m (@PCM.join (union_mapPCM Label dstatelet) i' j')) (@InMem (UMDef.tp Label dstatelet) i' (@Mem state (PredPredType state) (Coh V))) (network_rely (@inj_ext V W K w) this j j') (or (@ex (proc this V A) (fun q' : proc this V A => and (@eq (proc this W A) q (@Inject this W A V K w q')) (P i' q'))) (@ex A (fun v' : A => and (@eq (proc this W A) q (@Ret this W A v')) (P i' (@Ret this V A v')))))))) *)
Lemma aftA A B s (p : proc A) (P : B -> A -> state -> Prop) : 
(* Goal: @InMem (PCM.sort (union_mapPCM Label dstatelet)) (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Mem state (PredPredType state) (Coh W)) *)
(* Goal: @always_sc this W A (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Inject this W A V K w q') scs (fun (m : state) (q : proc this W A) => @ex (UMDef.tp Label dstatelet) (fun i' : UMDef.tp Label dstatelet => @ex (UMDef.tp Label dstatelet) (fun j' : UMDef.tp Label dstatelet => and4 (@eq state m (@PCM.join (union_mapPCM Label dstatelet) i' j')) (@InMem (UMDef.tp Label dstatelet) i' (@Mem state (PredPredType state) (Coh V))) (network_rely (@inj_ext V W K w) this j j') (or (@ex (proc this V A) (fun q' : proc this V A => and (@eq (proc this W A) q (@Inject this W A V K w q')) (P i' q'))) (@ex A (fun v' : A => and (@eq (proc this W A) q (@Ret this W A v')) (P i' (@Ret this V A v')))))))) *)
        alwsafe s p ->
(* Goal: @InMem (PCM.sort (union_mapPCM Label dstatelet)) (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Mem state (PredPredType state) (Coh W)) *)
(* Goal: @always_sc this W A (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Inject this W A V K w q') scs (fun (m : state) (q : proc this W A) => @ex (UMDef.tp Label dstatelet) (fun i' : UMDef.tp Label dstatelet => @ex (UMDef.tp Label dstatelet) (fun j' : UMDef.tp Label dstatelet => and4 (@eq state m (@PCM.join (union_mapPCM Label dstatelet) i' j')) (@InMem (UMDef.tp Label dstatelet) i' (@Mem state (PredPredType state) (Coh V))) (network_rely (@inj_ext V W K w) this j j') (or (@ex (proc this V A) (fun q' : proc this V A => and (@eq (proc this W A) q (@Inject this W A V K w q')) (P i' q'))) (@ex A (fun v' : A => and (@eq (proc this W A) q (@Ret this W A v')) (P i' (@Ret this V A v')))))))) *)
        (after s p (fun v s' => forall x, P x v s') <->
         forall x, after s p (fun v s' => P x v s')).
Proof.
(* Goal: @InMem (PCM.sort (union_mapPCM Label dstatelet)) (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Mem state (PredPredType state) (Coh W)) *)
(* Goal: @always_sc this W A (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Inject this W A V K w q') scs (fun (m : state) (q : proc this W A) => @ex (UMDef.tp Label dstatelet) (fun i' : UMDef.tp Label dstatelet => @ex (UMDef.tp Label dstatelet) (fun j' : UMDef.tp Label dstatelet => and4 (@eq state m (@PCM.join (union_mapPCM Label dstatelet) i' j')) (@InMem (UMDef.tp Label dstatelet) i' (@Mem state (PredPredType state) (Coh V))) (network_rely (@inj_ext V W K w) this j j') (or (@ex (proc this V A) (fun q' : proc this V A => and (@eq (proc this W A) q (@Inject this W A V K w q')) (P i' q'))) (@ex A (fun v' : A => and (@eq (proc this W A) q (@Ret this W A v')) (P i' (@Ret this V A v')))))))) *)
move=>Ls; rewrite -(alwA Ls).
(* Goal: iff (@after A s p (fun (v : A) (s' : state) => forall x : B, P x v s')) (@always A s p (fun (s' : state) (p' : @proc this W A) => forall (x : B) (v : A) (_ : @eq (@proc this W A) p' (@Ret this W A v)), P x v s')) *)
split; apply: alw_imp=>t q _ I.
(* Goal: @InMem (PCM.sort (union_mapPCM Label dstatelet)) (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Mem state (PredPredType state) (Coh W)) *)
(* Goal: @always_sc this W A (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Inject this W A V K w q') scs (fun (m : state) (q : proc this W A) => @ex (UMDef.tp Label dstatelet) (fun i' : UMDef.tp Label dstatelet => @ex (UMDef.tp Label dstatelet) (fun j' : UMDef.tp Label dstatelet => and4 (@eq state m (@PCM.join (union_mapPCM Label dstatelet) i' j')) (@InMem (UMDef.tp Label dstatelet) i' (@Mem state (PredPredType state) (Coh V))) (network_rely (@inj_ext V W K w) this j j') (or (@ex (proc this V A) (fun q' : proc this V A => and (@eq (proc this W A) q (@Inject this W A V K w q')) (P i' q'))) (@ex A (fun v' : A => and (@eq (proc this W A) q (@Ret this W A v')) (P i' (@Ret this V A v')))))))) *)
- by move=>x v; move/I.
(* Goal: forall _ : @ex A (fun v' : A => and (@eq (proc this (mkWorld (@ProtocolWithIndInv pr I ii)) A) (@Ret this (mkWorld (@ProtocolWithIndInv pr I ii)) A v) (@Ret this (mkWorld (@ProtocolWithIndInv pr I ii)) A v')) (forall (v : A) (_ : @eq (proc this (mkWorld pr) A) (@Ret this (mkWorld pr) A v') (@Ret this (mkWorld pr) A v)), P v s)), P v s *)
by move=>v; move/I.
Qed.

Arguments aftA [A B s p P].
Arguments aftI [A s p P Q].

End Always.

Section AlwaysInject.
Variables (V W : world) (K : hooks) (A : Type) (w : injects V W K) (this: nid).
Notation W2 := (inj_ext w).

Lemma rely_ext i j s : 
(* Goal: @InMem (PCM.sort (union_mapPCM Label dstatelet)) (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Mem state (PredPredType state) (Coh W)) *)
(* Goal: @always_sc this W A (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Inject this W A V K w q') scs (fun (m : state) (q : proc this W A) => @ex (UMDef.tp Label dstatelet) (fun i' : UMDef.tp Label dstatelet => @ex (UMDef.tp Label dstatelet) (fun j' : UMDef.tp Label dstatelet => and4 (@eq state m (@PCM.join (union_mapPCM Label dstatelet) i' j')) (@InMem (UMDef.tp Label dstatelet) i' (@Mem state (PredPredType state) (Coh V))) (network_rely (@inj_ext V W K w) this j j') (or (@ex (proc this V A) (fun q' : proc this V A => and (@eq (proc this W A) q (@Inject this W A V K w q')) (P i' q'))) (@ex A (fun v' : A => and (@eq (proc this W A) q (@Ret this W A v')) (P i' (@Ret this V A v')))))))) *)
        i \In Coh V -> 
(* Goal: @InMem (PCM.sort (union_mapPCM Label dstatelet)) (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Mem state (PredPredType state) (Coh W)) *)
(* Goal: @always_sc this W A (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Inject this W A V K w q') scs (fun (m : state) (q : proc this W A) => @ex (UMDef.tp Label dstatelet) (fun i' : UMDef.tp Label dstatelet => @ex (UMDef.tp Label dstatelet) (fun j' : UMDef.tp Label dstatelet => and4 (@eq state m (@PCM.join (union_mapPCM Label dstatelet) i' j')) (@InMem (UMDef.tp Label dstatelet) i' (@Mem state (PredPredType state) (Coh V))) (network_rely (@inj_ext V W K w) this j j') (or (@ex (proc this V A) (fun q' : proc this V A => and (@eq (proc this W A) q (@Inject this W A V K w q')) (P i' q'))) (@ex A (fun v' : A => and (@eq (proc this W A) q (@Ret this W A v')) (P i' (@Ret this V A v')))))))) *)
        network_rely W this (i \+ j) s ->  
(* Goal: network_rely V this s1 s2 *)
(* Goal: network_rely (@inj_ext V W K w) this s1' s2' *)
(* Goal: forall (_ : and (@eq state (@PCM.join (union_mapPCM Label dstatelet) s1 s1') (@PCM.join (union_mapPCM Label dstatelet) s2 s2')) (@InMem state (@PCM.join (union_mapPCM Label dstatelet) s1 s1') (@Mem state (PredPredType state) (Coh W)))) (_ : @InMem state s1 (@Mem state (PredPredType state) (Coh V))) (_ : @InMem state s2 (@Mem state (PredPredType state) (Coh V))), and (network_rely V this s1 s2) (network_rely (@inj_ext V W K w) this s1' s2') *)
        exists i' j', s = i' \+ j' /\ i' \In Coh V.
Proof.
(* Goal: forall (_ : @InMem state i (@Mem state (PredPredType state) (Coh V))) (_ : network_rely W this (@PCM.join (union_mapPCM Label dstatelet) i j) s), @ex (PCM.sort (union_mapPCM Label dstatelet)) (fun i' : PCM.sort (union_mapPCM Label dstatelet) => @ex (PCM.sort (union_mapPCM Label dstatelet)) (fun j' : PCM.sort (union_mapPCM Label dstatelet) => and (@eq state s (@PCM.join (union_mapPCM Label dstatelet) i' j')) (@InMem (PCM.sort (union_mapPCM Label dstatelet)) i' (@Mem state (PredPredType state) (Coh V))))) *)
move=>C M; case: (rely_coh M)=>_; rewrite (cohE w).
(* Goal: @InMem (PCM.sort (union_mapPCM Label dstatelet)) (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Mem state (PredPredType state) (Coh W)) *)
(* Goal: @always_sc this W A (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Inject this W A V K w q') scs (fun (m : state) (q : proc this W A) => @ex (UMDef.tp Label dstatelet) (fun i' : UMDef.tp Label dstatelet => @ex (UMDef.tp Label dstatelet) (fun j' : UMDef.tp Label dstatelet => and4 (@eq state m (@PCM.join (union_mapPCM Label dstatelet) i' j')) (@InMem (UMDef.tp Label dstatelet) i' (@Mem state (PredPredType state) (Coh V))) (network_rely (@inj_ext V W K w) this j j') (or (@ex (proc this V A) (fun q' : proc this V A => and (@eq (proc this W A) q (@Inject this W A V K w q')) (P i' q'))) (@ex A (fun v' : A => and (@eq (proc this W A) q (@Ret this W A v')) (P i' (@Ret this V A v')))))))) *)
by case=>[s1][s2][->] Cs1 _; exists s1, s2. 
Qed.

Lemma rely_split' z s1 s1' s2 s2' : 
(* Goal: @InMem (PCM.sort (union_mapPCM Label dstatelet)) (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Mem state (PredPredType state) (Coh W)) *)
(* Goal: @always_sc this W A (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Inject this W A V K w q') scs (fun (m : state) (q : proc this W A) => @ex (UMDef.tp Label dstatelet) (fun i' : UMDef.tp Label dstatelet => @ex (UMDef.tp Label dstatelet) (fun j' : UMDef.tp Label dstatelet => and4 (@eq state m (@PCM.join (union_mapPCM Label dstatelet) i' j')) (@InMem (UMDef.tp Label dstatelet) i' (@Mem state (PredPredType state) (Coh V))) (network_rely (@inj_ext V W K w) this j j') (or (@ex (proc this V A) (fun q' : proc this V A => and (@eq (proc this W A) q (@Inject this W A V K w q')) (P i' q'))) (@ex A (fun v' : A => and (@eq (proc this W A) q (@Ret this W A v')) (P i' (@Ret this V A v')))))))) *)
  s1 \In Coh V -> s2 \In Coh V ->
(* Goal: @InMem (PCM.sort (union_mapPCM Label dstatelet)) (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Mem state (PredPredType state) (Coh W)) *)
(* Goal: @always_sc this W A (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Inject this W A V K w q') scs (fun (m : state) (q : proc this W A) => @ex (UMDef.tp Label dstatelet) (fun i' : UMDef.tp Label dstatelet => @ex (UMDef.tp Label dstatelet) (fun j' : UMDef.tp Label dstatelet => and4 (@eq state m (@PCM.join (union_mapPCM Label dstatelet) i' j')) (@InMem (UMDef.tp Label dstatelet) i' (@Mem state (PredPredType state) (Coh V))) (network_rely (@inj_ext V W K w) this j j') (or (@ex (proc this V A) (fun q' : proc this V A => and (@eq (proc this W A) q (@Inject this W A V K w q')) (P i' q'))) (@ex A (fun v' : A => and (@eq (proc this W A) q (@Ret this W A v')) (P i' (@Ret this V A v')))))))) *)
  network_step W z (s1 \+ s1') (s2 \+ s2') ->
  network_step V z s1 s2 /\ network_step (inj_ext w) z s1' s2'.
Proof.
(* Goal: @ex (PCM.sort (union_mapPCM Label dstatelet)) (fun i' : PCM.sort (union_mapPCM Label dstatelet) => @ex (PCM.sort (union_mapPCM Label dstatelet)) (fun j' : PCM.sort (union_mapPCM Label dstatelet) => and4 (@eq state (@PCM.join (union_mapPCM Label dstatelet) i1 j1) (@PCM.join (union_mapPCM Label dstatelet) i' j')) (@InMem (PCM.sort (union_mapPCM Label dstatelet)) i' (@Mem state (PredPredType state) (Coh V))) (network_rely (@inj_ext V W K w) this j j') (P v i'))) *)
move=>C1 C2 N.
case: (sem_split w C1 C2 N); case=>R E; [subst s2'|subst s2];
split=>//; apply: Idle; split=>//.
(* Goal: forall (_ : @ex (PCM.sort (union_mapPCM Label dstatelet)) (fun i' : PCM.sort (union_mapPCM Label dstatelet) => @ex (PCM.sort (union_mapPCM Label dstatelet)) (fun j' : PCM.sort (union_mapPCM Label dstatelet) => and4 (@eq state s (@PCM.join (union_mapPCM Label dstatelet) i' j')) (@InMem (PCM.sort (union_mapPCM Label dstatelet)) i' (@Mem state (PredPredType state) (Coh V))) (network_rely (@inj_ext V W K w) this j j') (or (@ex (proc this V A) (fun q' : proc this V A => and (@eq (proc this W A) q (@Inject this W A V K w q')) (forall (v : A) (_ : @eq (proc this V A) q' (@Ret this V A v)), P v i'))) (@ex A (fun v' : A => and (@eq (proc this W A) q (@Ret this W A v')) (forall (v : A) (_ : @eq (proc this V A) (@Ret this V A v') (@Ret this V A v)), P v i'))))))) (v : A) (_ : @eq (proc this W A) q (@Ret this W A v)), @ex (PCM.sort (union_mapPCM Label dstatelet)) (fun i' : PCM.sort (union_mapPCM Label dstatelet) => @ex (PCM.sort (union_mapPCM Label dstatelet)) (fun j' : PCM.sort (union_mapPCM Label dstatelet) => and4 (@eq state s (@PCM.join (union_mapPCM Label dstatelet) i' j')) (@InMem (PCM.sort (union_mapPCM Label dstatelet)) i' (@Mem state (PredPredType state) (Coh V))) (network_rely (@inj_ext V W K w) this j j') (P v i'))) *)
case: (step_coh N)=>C _.
(* Goal: forall (_ : @ex (PCM.sort (union_mapPCM Label dstatelet)) (fun i' : PCM.sort (union_mapPCM Label dstatelet) => @ex (PCM.sort (union_mapPCM Label dstatelet)) (fun j' : PCM.sort (union_mapPCM Label dstatelet) => and4 (@eq state s (@PCM.join (union_mapPCM Label dstatelet) i' j')) (@InMem (PCM.sort (union_mapPCM Label dstatelet)) i' (@Mem state (PredPredType state) (Coh V))) (network_rely (@inj_ext V W K w) this j j') (or (@ex (proc this V A) (fun q' : proc this V A => and (@eq (proc this W A) q (@Inject this W A V K w q')) (forall (v : A) (_ : @eq (proc this V A) q' (@Ret this V A v)), P v i'))) (@ex A (fun v' : A => and (@eq (proc this W A) q (@Ret this W A v')) (forall (v : A) (_ : @eq (proc this V A) (@Ret this V A v') (@Ret this V A v)), P v i'))))))) (v : A) (_ : @eq (proc this W A) q (@Ret this W A v)), @ex (PCM.sort (union_mapPCM Label dstatelet)) (fun i' : PCM.sort (union_mapPCM Label dstatelet) => @ex (PCM.sort (union_mapPCM Label dstatelet)) (fun j' : PCM.sort (union_mapPCM Label dstatelet) => and4 (@eq state s (@PCM.join (union_mapPCM Label dstatelet) i' j')) (@InMem (PCM.sort (union_mapPCM Label dstatelet)) i' (@Mem state (PredPredType state) (Coh V))) (network_rely (@inj_ext V W K w) this j j') (P v i'))) *)
case/(cohE w): (C)=>s3[s4][E]C' C''.
(* Goal: @InMem state s1' (@Mem state (PredPredType state) (Coh (@inj_ext V W K w))) *)
move: (coh_prec (cohS C) C1 C' E)=>Z; subst s3.
(* Goal: forall _ : @ex A (fun v' : A => and (@eq (proc this (mkWorld (@ProtocolWithIndInv pr I ii)) A) (@Ret this (mkWorld (@ProtocolWithIndInv pr I ii)) A v) (@Ret this (mkWorld (@ProtocolWithIndInv pr I ii)) A v')) (forall (v : A) (_ : @eq (proc this (mkWorld pr) A) (@Ret this (mkWorld pr) A v') (@Ret this (mkWorld pr) A v)), P v s)), P v s *)
by rewrite (joinxK (cohS C) E).
Qed.

Lemma rely_split s1 s1' s2 s2' : 
(* Goal: @InMem (PCM.sort (union_mapPCM Label dstatelet)) (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Mem state (PredPredType state) (Coh W)) *)
(* Goal: @always_sc this W A (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Inject this W A V K w q') scs (fun (m : state) (q : proc this W A) => @ex (UMDef.tp Label dstatelet) (fun i' : UMDef.tp Label dstatelet => @ex (UMDef.tp Label dstatelet) (fun j' : UMDef.tp Label dstatelet => and4 (@eq state m (@PCM.join (union_mapPCM Label dstatelet) i' j')) (@InMem (UMDef.tp Label dstatelet) i' (@Mem state (PredPredType state) (Coh V))) (network_rely (@inj_ext V W K w) this j j') (or (@ex (proc this V A) (fun q' : proc this V A => and (@eq (proc this W A) q (@Inject this W A V K w q')) (P i' q'))) (@ex A (fun v' : A => and (@eq (proc this W A) q (@Ret this W A v')) (P i' (@Ret this V A v')))))))) *)
  s1 \In Coh V -> s2 \In Coh V ->
(* Goal: @InMem (PCM.sort (union_mapPCM Label dstatelet)) (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Mem state (PredPredType state) (Coh W)) *)
(* Goal: @always_sc this W A (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Inject this W A V K w q') scs (fun (m : state) (q : proc this W A) => @ex (UMDef.tp Label dstatelet) (fun i' : UMDef.tp Label dstatelet => @ex (UMDef.tp Label dstatelet) (fun j' : UMDef.tp Label dstatelet => and4 (@eq state m (@PCM.join (union_mapPCM Label dstatelet) i' j')) (@InMem (UMDef.tp Label dstatelet) i' (@Mem state (PredPredType state) (Coh V))) (network_rely (@inj_ext V W K w) this j j') (or (@ex (proc this V A) (fun q' : proc this V A => and (@eq (proc this W A) q (@Inject this W A V K w q')) (P i' q'))) (@ex A (fun v' : A => and (@eq (proc this W A) q (@Ret this W A v')) (P i' (@Ret this V A v')))))))) *)
  network_rely W this (s1 \+ s1') (s2 \+ s2') ->
  network_rely V this s1 s2 /\ network_rely (inj_ext w) this s1' s2'.
Proof.
(* Goal: @ex (PCM.sort (union_mapPCM Label dstatelet)) (fun i' : PCM.sort (union_mapPCM Label dstatelet) => @ex (PCM.sort (union_mapPCM Label dstatelet)) (fun j' : PCM.sort (union_mapPCM Label dstatelet) => and4 (@eq state (@PCM.join (union_mapPCM Label dstatelet) i1 j1) (@PCM.join (union_mapPCM Label dstatelet) i' j')) (@InMem (PCM.sort (union_mapPCM Label dstatelet)) i' (@Mem state (PredPredType state) (Coh V))) (network_rely (@inj_ext V W K w) this j j') (P v i'))) *)
move=>C1 C2 [n E].
(* Goal: P v s *)
elim: n s1 s1' E C1 C2=>[|n IH] /= s1 s1'; last first.
(* Goal: @InMem (PCM.sort (union_mapPCM Label dstatelet)) (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Mem state (PredPredType state) (Coh W)) *)
(* Goal: @always_sc this W A (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Inject this W A V K w q') scs (fun (m : state) (q : proc this W A) => @ex (UMDef.tp Label dstatelet) (fun i' : UMDef.tp Label dstatelet => @ex (UMDef.tp Label dstatelet) (fun j' : UMDef.tp Label dstatelet => and4 (@eq state m (@PCM.join (union_mapPCM Label dstatelet) i' j')) (@InMem (UMDef.tp Label dstatelet) i' (@Mem state (PredPredType state) (Coh V))) (network_rely (@inj_ext V W K w) this j j') (or (@ex (proc this V A) (fun q' : proc this V A => and (@eq (proc this W A) q (@Inject this W A V K w q')) (P i' q'))) (@ex A (fun v' : A => and (@eq (proc this W A) q (@Ret this W A v')) (P i' (@Ret this V A v')))))))) *)
- move=>[z][s3][N]H1 H2 C1 C2.
(* Goal: and (network_rely V this s1 s2) (network_rely (@inj_ext V W K w) this s1' s2') *)
(* Goal: forall (_ : and (@eq state (@PCM.join (union_mapPCM Label dstatelet) s1 s1') (@PCM.join (union_mapPCM Label dstatelet) s2 s2')) (@InMem state (@PCM.join (union_mapPCM Label dstatelet) s1 s1') (@Mem state (PredPredType state) (Coh W)))) (_ : @InMem state s1 (@Mem state (PredPredType state) (Coh V))) (_ : @InMem state s2 (@Mem state (PredPredType state) (Coh V))), and (network_rely V this s1 s2) (network_rely (@inj_ext V W K w) this s1' s2') *)
  case: (step_coh H1)=>D1 D2; move/(cohE w): D2=>[s4][s5][Z]C3 C4.
(* Goal: and (network_rely V this s1 s2) (network_rely (@inj_ext V W K w) this s1' s2') *)
(* Goal: forall (_ : and (@eq state (@PCM.join (union_mapPCM Label dstatelet) s1 s1') (@PCM.join (union_mapPCM Label dstatelet) s2 s2')) (@InMem state (@PCM.join (union_mapPCM Label dstatelet) s1 s1') (@Mem state (PredPredType state) (Coh W)))) (_ : @InMem state s1 (@Mem state (PredPredType state) (Coh V))) (_ : @InMem state s2 (@Mem state (PredPredType state) (Coh V))), and (network_rely V this s1 s2) (network_rely (@inj_ext V W K w) this s1' s2') *)
  subst s3; case: (IH s4 s5 H2 C3 C2)=>G1 G2.
(* Goal: and (network_rely V this s1 s2) (network_rely (@inj_ext V W K w) this s1' s2') *)
(* Goal: forall (_ : and (@eq state (@PCM.join (union_mapPCM Label dstatelet) s1 s1') (@PCM.join (union_mapPCM Label dstatelet) s2 s2')) (@InMem state (@PCM.join (union_mapPCM Label dstatelet) s1 s1') (@Mem state (PredPredType state) (Coh W)))) (_ : @InMem state s1 (@Mem state (PredPredType state) (Coh V))) (_ : @InMem state s2 (@Mem state (PredPredType state) (Coh V))), and (network_rely V this s1 s2) (network_rely (@inj_ext V W K w) this s1' s2') *)
  case: (rely_split' C1 _ H1)=>//H3 H4; split=>//.
(* Goal: network_rely V this s1 s2 *)
(* Goal: network_rely (@inj_ext V W K w) this s1' s2' *)
(* Goal: forall (_ : and (@eq state (@PCM.join (union_mapPCM Label dstatelet) s1 s1') (@PCM.join (union_mapPCM Label dstatelet) s2 s2')) (@InMem state (@PCM.join (union_mapPCM Label dstatelet) s1 s1') (@Mem state (PredPredType state) (Coh W)))) (_ : @InMem state s1 (@Mem state (PredPredType state) (Coh V))) (_ : @InMem state s2 (@Mem state (PredPredType state) (Coh V))), and (network_rely V this s1 s2) (network_rely (@inj_ext V W K w) this s1' s2') *)
  + by case: G1=>m R; exists m.+1, z, s4. 
(* Goal: network_rely V this s1 s2 *)
(* Goal: network_rely (@inj_ext V W K w) this s1' s2' *)
(* Goal: forall (_ : and (@eq state (@PCM.join (union_mapPCM Label dstatelet) s1 s1') (@PCM.join (union_mapPCM Label dstatelet) s2 s2')) (@InMem state (@PCM.join (union_mapPCM Label dstatelet) s1 s1') (@Mem state (PredPredType state) (Coh W)))) (_ : @InMem state s1 (@Mem state (PredPredType state) (Coh V))) (_ : @InMem state s2 (@Mem state (PredPredType state) (Coh V))), and (network_rely V this s1 s2) (network_rely (@inj_ext V W K w) this s1' s2') *)
  by case: G2=>m R; exists m.+1, z, s5. 
(* Goal: @ex (PCM.sort (union_mapPCM Label dstatelet)) (fun i' : PCM.sort (union_mapPCM Label dstatelet) => @ex (PCM.sort (union_mapPCM Label dstatelet)) (fun j' : PCM.sort (union_mapPCM Label dstatelet) => and4 (@eq state (@PCM.join (union_mapPCM Label dstatelet) i1 j1) (@PCM.join (union_mapPCM Label dstatelet) i' j')) (@InMem (PCM.sort (union_mapPCM Label dstatelet)) i' (@Mem state (PredPredType state) (Coh V))) (network_rely (@inj_ext V W K w) this j j') (P v i'))) *)
move=> [E1 E2] C1 C2.
(* Goal: and (network_rely V this s1 s2) (network_rely (@inj_ext V W K w) this s1' s2') *)
move: (coh_prec (cohS E2) C1 C2 E1)=>Z; subst s2.
(* Goal: and (network_rely V this s1 s1) (network_rely (@inj_ext V W K w) this s1' s2') *)
rewrite (joinxK (cohS E2) E1); split; exists 0=>//. 
(* Goal: @InMem (PCM.sort (union_mapPCM Label dstatelet)) (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Mem state (PredPredType state) (Coh W)) *)
(* Goal: @always_sc this W A (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Inject this W A V K w q') scs (fun (m : state) (q : proc this W A) => @ex (UMDef.tp Label dstatelet) (fun i' : UMDef.tp Label dstatelet => @ex (UMDef.tp Label dstatelet) (fun j' : UMDef.tp Label dstatelet => and4 (@eq state m (@PCM.join (union_mapPCM Label dstatelet) i' j')) (@InMem (UMDef.tp Label dstatelet) i' (@Mem state (PredPredType state) (Coh V))) (network_rely (@inj_ext V W K w) this j j') (or (@ex (proc this V A) (fun q' : proc this V A => and (@eq (proc this W A) q (@Inject this W A V K w q')) (P i' q'))) (@ex A (fun v' : A => and (@eq (proc this W A) q (@Ret this W A v')) (P i' (@Ret this V A v')))))))) *)
split=>//; rewrite -(joinxK (cohS E2) E1)=>{E1 s2' C2}.
(* Goal: @ex (PCM.sort (union_mapPCM Label dstatelet)) (fun i' : PCM.sort (union_mapPCM Label dstatelet) => @ex (PCM.sort (union_mapPCM Label dstatelet)) (fun j' : PCM.sort (union_mapPCM Label dstatelet) => and4 (@eq state (@PCM.join (union_mapPCM Label dstatelet) i1 j1) (@PCM.join (union_mapPCM Label dstatelet) i' j')) (@InMem (PCM.sort (union_mapPCM Label dstatelet)) i' (@Mem state (PredPredType state) (Coh V))) (network_rely (@inj_ext V W K w) this j j') (P v i'))) *)
move/(cohE w): (E2)=>[t1][t2][E]C' C''.
(* Goal: @InMem state s1' (@Mem state (PredPredType state) (Coh (@inj_ext V W K w))) *)
move: ((coh_prec (cohS E2)) C1 C' E)=>Z; subst t1.
(* Goal: forall _ : @ex A (fun v' : A => and (@eq (proc this (mkWorld (@ProtocolWithIndInv pr I ii)) A) (@Ret this (mkWorld (@ProtocolWithIndInv pr I ii)) A v) (@Ret this (mkWorld (@ProtocolWithIndInv pr I ii)) A v')) (forall (v : A) (_ : @eq (proc this (mkWorld pr) A) (@Ret this (mkWorld pr) A v') (@Ret this (mkWorld pr) A v)), P v s)), P v s *)
by rewrite (joinxK (cohS E2) E).
Qed.




Lemma alw_inject (p : proc this V A)
(* Goal: @InMem (PCM.sort (union_mapPCM Label dstatelet)) (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Mem state (PredPredType state) (Coh W)) *)
(* Goal: @always_sc this W A (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Inject this W A V K w q') scs (fun (m : state) (q : proc this W A) => @ex (UMDef.tp Label dstatelet) (fun i' : UMDef.tp Label dstatelet => @ex (UMDef.tp Label dstatelet) (fun j' : UMDef.tp Label dstatelet => and4 (@eq state m (@PCM.join (union_mapPCM Label dstatelet) i' j')) (@InMem (UMDef.tp Label dstatelet) i' (@Mem state (PredPredType state) (Coh V))) (network_rely (@inj_ext V W K w) this j j') (or (@ex (proc this V A) (fun q' : proc this V A => and (@eq (proc this W A) q (@Inject this W A V K w q')) (P i' q'))) (@ex A (fun v' : A => and (@eq (proc this W A) q (@Ret this W A v')) (P i' (@Ret this V A v')))))))) *)
      (P : state -> proc this V A -> Prop) i j :
(* Goal: @InMem (PCM.sort (union_mapPCM Label dstatelet)) (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Mem state (PredPredType state) (Coh W)) *)
(* Goal: @always_sc this W A (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Inject this W A V K w q') scs (fun (m : state) (q : proc this W A) => @ex (UMDef.tp Label dstatelet) (fun i' : UMDef.tp Label dstatelet => @ex (UMDef.tp Label dstatelet) (fun j' : UMDef.tp Label dstatelet => and4 (@eq state m (@PCM.join (union_mapPCM Label dstatelet) i' j')) (@InMem (UMDef.tp Label dstatelet) i' (@Mem state (PredPredType state) (Coh V))) (network_rely (@inj_ext V W K w) this j j') (or (@ex (proc this V A) (fun q' : proc this V A => and (@eq (proc this W A) q (@Inject this W A V K w q')) (P i' q'))) (@ex A (fun v' : A => and (@eq (proc this W A) q (@Ret this W A v')) (P i' (@Ret this V A v')))))))) *)
        i \+ j \In Coh W ->
(* Goal: @InMem (PCM.sort (union_mapPCM Label dstatelet)) (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Mem state (PredPredType state) (Coh W)) *)
(* Goal: @always_sc this W A (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Inject this W A V K w q') scs (fun (m : state) (q : proc this W A) => @ex (UMDef.tp Label dstatelet) (fun i' : UMDef.tp Label dstatelet => @ex (UMDef.tp Label dstatelet) (fun j' : UMDef.tp Label dstatelet => and4 (@eq state m (@PCM.join (union_mapPCM Label dstatelet) i' j')) (@InMem (UMDef.tp Label dstatelet) i' (@Mem state (PredPredType state) (Coh V))) (network_rely (@inj_ext V W K w) this j j') (or (@ex (proc this V A) (fun q' : proc this V A => and (@eq (proc this W A) q (@Inject this W A V K w q')) (P i' q'))) (@ex A (fun v' : A => and (@eq (proc this W A) q (@Ret this W A v')) (P i' (@Ret this V A v')))))))) *)
        always i p P ->
(* Goal: network_rely V this s1 s2 *)
(* Goal: network_rely (@inj_ext V W K w) this s1' s2' *)
(* Goal: forall (_ : and (@eq state (@PCM.join (union_mapPCM Label dstatelet) s1 s1') (@PCM.join (union_mapPCM Label dstatelet) s2 s2')) (@InMem state (@PCM.join (union_mapPCM Label dstatelet) s1 s1') (@Mem state (PredPredType state) (Coh W)))) (_ : @InMem state s1 (@Mem state (PredPredType state) (Coh V))) (_ : @InMem state s2 (@Mem state (PredPredType state) (Coh V))), and (network_rely V this s1 s2) (network_rely (@inj_ext V W K w) this s1' s2') *)
        always (i \+ j) (Inject w p)
          (fun m q => exists i' j', 
(* Goal: network_rely V this s1 s2 *)
(* Goal: network_rely (@inj_ext V W K w) this s1' s2' *)
(* Goal: forall (_ : and (@eq state (@PCM.join (union_mapPCM Label dstatelet) s1 s1') (@PCM.join (union_mapPCM Label dstatelet) s2 s2')) (@InMem state (@PCM.join (union_mapPCM Label dstatelet) s1 s1') (@Mem state (PredPredType state) (Coh W)))) (_ : @InMem state s1 (@Mem state (PredPredType state) (Coh V))) (_ : @InMem state s2 (@Mem state (PredPredType state) (Coh V))), and (network_rely V this s1 s2) (network_rely (@inj_ext V W K w) this s1' s2') *)
             [/\ m = i' \+ j', i' \In Coh V, network_rely W2 this j j' &
                 (exists q', q = Inject w q' /\ P i' q') \/
                 (exists v', q = Ret v' /\ P i' (Ret v'))]).
Proof.
move=>C Ls scs; elim: scs i j p C Ls=>[|sc scs IH] i j p C Ls /=; 
split=>// {C} s M; move: (alw_coh Ls) (proj2 (rely_coh M))=>Ci C;
(* Goal: @InMem (PCM.sort (union_mapPCM Label dstatelet)) (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Mem state (PredPredType state) (Coh W)) *)
(* Goal: @always_sc this W A (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Inject this W A V K w q') scs (fun (m : state) (q : proc this W A) => @ex (UMDef.tp Label dstatelet) (fun i' : UMDef.tp Label dstatelet => @ex (UMDef.tp Label dstatelet) (fun j' : UMDef.tp Label dstatelet => and4 (@eq state m (@PCM.join (union_mapPCM Label dstatelet) i' j')) (@InMem (UMDef.tp Label dstatelet) i' (@Mem state (PredPredType state) (Coh V))) (network_rely (@inj_ext V W K w) this j j') (or (@ex (proc this V A) (fun q' : proc this V A => and (@eq (proc this W A) q (@Inject this W A V K w q')) (P i' q'))) (@ex A (fun v' : A => and (@eq (proc this W A) q (@Ret this W A v')) (P i' (@Ret this V A v')))))))) *)
case/(rely_ext Ci): M C (M)=>i1 [j1][->{s}] Ci1 C;
case/(rely_split Ci Ci1)=> /(alw_envs Ls) {Ls} Ls S1.
(* Goal: @InMem (PCM.sort (union_mapPCM Label dstatelet)) (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Mem state (PredPredType state) (Coh W)) *)
(* Goal: @always_sc this W A (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Inject this W A V K w q') scs (fun (m : state) (q : proc this W A) => @ex (UMDef.tp Label dstatelet) (fun i' : UMDef.tp Label dstatelet => @ex (UMDef.tp Label dstatelet) (fun j' : UMDef.tp Label dstatelet => and4 (@eq state m (@PCM.join (union_mapPCM Label dstatelet) i' j')) (@InMem (UMDef.tp Label dstatelet) i' (@Mem state (PredPredType state) (Coh V))) (network_rely (@inj_ext V W K w) this j j') (or (@ex (proc this V A) (fun q' : proc this V A => and (@eq (proc this W A) q (@Inject this W A V K w q')) (P i' q'))) (@ex A (fun v' : A => and (@eq (proc this W A) q (@Ret this W A v')) (P i' (@Ret this V A v')))))))) *)
- by exists i1, j1; split=>//; left; exists p; move/alw_refl: Ls.
(* Goal: and3 match sc with | ActStep => True | SeqRet => True | SeqStep sc' => True | InjectStep sc' => @ex (UMDef.tp Label dstatelet) (fun s' : UMDef.tp Label dstatelet => and (@extends V W K w (@PCM.join (union_mapPCM Label dstatelet) i1 j1) s') (@safe this V A p sc' s')) | InjectRet => match p with | Unfinished => True | Ret a => @ex (UMDef.tp Label dstatelet) (fun s' : UMDef.tp Label dstatelet => @extends V W K w (@PCM.join (union_mapPCM Label dstatelet) i1 j1) s') | Act a => True | @Seq _ _ _ B p p0 => True | @Inject _ _ _ V0 K i p => True | WithInv p I0 ii e p0 => True end | WithInvStep sc' => True | WithInvRet => True end (@ex (UMDef.tp Label dstatelet) (fun i' : UMDef.tp Label dstatelet => @ex (UMDef.tp Label dstatelet) (fun j' : UMDef.tp Label dstatelet => and4 (@eq state (@PCM.join (union_mapPCM Label dstatelet) i1 j1) (@PCM.join (union_mapPCM Label dstatelet) i' j')) (@InMem (UMDef.tp Label dstatelet) i' (@Mem state (PredPredType state) (Coh V))) (network_rely (@inj_ext V W K w) this j j') (or (@ex (proc this V A) (fun q' : proc this V A => and (@eq (proc this W A) (@Inject this W A V K w p) (@Inject this W A V K w q')) (P i' q'))) (@ex A (fun v' : A => and (@eq (proc this W A) (@Inject this W A V K w p) (@Ret this W A v')) (P i' (@Ret this V A v')))))))) (forall (s3 : state) (q : proc this W A) (_ : @pstep this W A (@PCM.join (union_mapPCM Label dstatelet) i1 j1) (@Inject this W A V K w p) sc s3 q), @always_sc this W A s3 q scs (fun (m : state) (q0 : proc this W A) => @ex (UMDef.tp Label dstatelet) (fun i' : UMDef.tp Label dstatelet => @ex (UMDef.tp Label dstatelet) (fun j' : UMDef.tp Label dstatelet => and4 (@eq state m (@PCM.join (union_mapPCM Label dstatelet) i' j')) (@InMem (UMDef.tp Label dstatelet) i' (@Mem state (PredPredType state) (Coh V))) (network_rely (@inj_ext V W K w) this j j') (or (@ex (proc this V A) (fun q' : proc this V A => and (@eq (proc this W A) q0 (@Inject this W A V K w q')) (P i' q'))) (@ex A (fun v' : A => and (@eq (proc this W A) q0 (@Ret this W A v')) (P i' (@Ret this V A v'))))))))) *)
split.
(* Goal: @InMem (PCM.sort (union_mapPCM Label dstatelet)) (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Mem state (PredPredType state) (Coh W)) *)
(* Goal: @always_sc this W A (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Inject this W A V K w q') scs (fun (m : state) (q : proc this W A) => @ex (UMDef.tp Label dstatelet) (fun i' : UMDef.tp Label dstatelet => @ex (UMDef.tp Label dstatelet) (fun j' : UMDef.tp Label dstatelet => and4 (@eq state m (@PCM.join (union_mapPCM Label dstatelet) i' j')) (@InMem (UMDef.tp Label dstatelet) i' (@Mem state (PredPredType state) (Coh V))) (network_rely (@inj_ext V W K w) this j j') (or (@ex (proc this V A) (fun q' : proc this V A => and (@eq (proc this W A) q (@Inject this W A V K w q')) (P i' q'))) (@ex A (fun v' : A => and (@eq (proc this W A) q (@Ret this W A v')) (P i' (@Ret this V A v')))))))) *)
- case: sc=>//; last by case: p Ls=>// v; exists i1, j1.
(* Goal: forall _ : @ex A (fun v' : A => and (@eq (proc this (mkWorld (@ProtocolWithIndInv pr I ii)) A) (@Ret this (mkWorld (@ProtocolWithIndInv pr I ii)) A v) (@Ret this (mkWorld (@ProtocolWithIndInv pr I ii)) A v')) (forall (v : A) (_ : @eq (proc this (mkWorld pr) A) (@Ret this (mkWorld pr) A v') (@Ret this (mkWorld pr) A v)), P v s)), P v s *)
  by move=>sc; move: (alw_safe Ls sc)=>Sf; exists i1; split=>//; exists j1.
(* Goal: @InMem (PCM.sort (union_mapPCM Label dstatelet)) (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Mem state (PredPredType state) (Coh W)) *)
(* Goal: @always_sc this W A (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Inject this W A V K w q') scs (fun (m : state) (q : proc this W A) => @ex (UMDef.tp Label dstatelet) (fun i' : UMDef.tp Label dstatelet => @ex (UMDef.tp Label dstatelet) (fun j' : UMDef.tp Label dstatelet => and4 (@eq state m (@PCM.join (union_mapPCM Label dstatelet) i' j')) (@InMem (UMDef.tp Label dstatelet) i' (@Mem state (PredPredType state) (Coh V))) (network_rely (@inj_ext V W K w) this j j') (or (@ex (proc this V A) (fun q' : proc this V A => and (@eq (proc this W A) q (@Inject this W A V K w q')) (P i' q'))) (@ex A (fun v' : A => and (@eq (proc this W A) q (@Ret this W A v')) (P i' (@Ret this V A v')))))))) *)
- by exists i1, j1; split=>//; left; exists p; move/alw_refl: Ls.
(* Goal: @InMem (PCM.sort (union_mapPCM Label dstatelet)) (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Mem state (PredPredType state) (Coh W)) *)
(* Goal: @always_sc this W A (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Inject this W A V K w q') scs (fun (m : state) (q : proc this W A) => @ex (UMDef.tp Label dstatelet) (fun i' : UMDef.tp Label dstatelet => @ex (UMDef.tp Label dstatelet) (fun j' : UMDef.tp Label dstatelet => and4 (@eq state m (@PCM.join (union_mapPCM Label dstatelet) i' j')) (@InMem (UMDef.tp Label dstatelet) i' (@Mem state (PredPredType state) (Coh V))) (network_rely (@inj_ext V W K w) this j j') (or (@ex (proc this V A) (fun q' : proc this V A => and (@eq (proc this W A) q (@Inject this W A V K w q')) (P i' q'))) (@ex A (fun v' : A => and (@eq (proc this W A) q (@Ret this W A v')) (P i' (@Ret this V A v')))))))) *)
move=>s q; rewrite stepInject => H.
(* Goal: forall (_ : @ex (PCM.sort (union_mapPCM Label dstatelet)) (fun i' : PCM.sort (union_mapPCM Label dstatelet) => @ex (PCM.sort (union_mapPCM Label dstatelet)) (fun j' : PCM.sort (union_mapPCM Label dstatelet) => and4 (@eq state s (@PCM.join (union_mapPCM Label dstatelet) i' j')) (@InMem (PCM.sort (union_mapPCM Label dstatelet)) i' (@Mem state (PredPredType state) (Coh V))) (network_rely (@inj_ext V W K w) this j j') (or (@ex (proc this V A) (fun q' : proc this V A => and (@eq (proc this W A) q (@Inject this W A V K w q')) (forall (v : A) (_ : @eq (proc this V A) q' (@Ret this V A v)), P v i'))) (@ex A (fun v' : A => and (@eq (proc this W A) q (@Ret this W A v')) (forall (v : A) (_ : @eq (proc this V A) (@Ret this V A v') (@Ret this V A v)), P v i'))))))) (v : A) (_ : @eq (proc this W A) q (@Ret this W A v)), @ex (PCM.sort (union_mapPCM Label dstatelet)) (fun i' : PCM.sort (union_mapPCM Label dstatelet) => @ex (PCM.sort (union_mapPCM Label dstatelet)) (fun j' : PCM.sort (union_mapPCM Label dstatelet) => and4 (@eq state s (@PCM.join (union_mapPCM Label dstatelet) i' j')) (@InMem (PCM.sort (union_mapPCM Label dstatelet)) i' (@Mem state (PredPredType state) (Coh V))) (network_rely (@inj_ext V W K w) this j j') (P v i'))) *)
case: H Ls.
(* Goal: @InMem (PCM.sort (union_mapPCM Label dstatelet)) (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Mem state (PredPredType state) (Coh W)) *)
(* Goal: @always_sc this W A (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Inject this W A V K w q') scs (fun (m : state) (q : proc this W A) => @ex (UMDef.tp Label dstatelet) (fun i' : UMDef.tp Label dstatelet => @ex (UMDef.tp Label dstatelet) (fun j' : UMDef.tp Label dstatelet => and4 (@eq state m (@PCM.join (union_mapPCM Label dstatelet) i' j')) (@InMem (UMDef.tp Label dstatelet) i' (@Mem state (PredPredType state) (Coh V))) (network_rely (@inj_ext V W K w) this j j') (or (@ex (proc this V A) (fun q' : proc this V A => and (@eq (proc this W A) q (@Inject this W A V K w q')) (P i' q'))) (@ex A (fun v' : A => and (@eq (proc this W A) q (@Ret this W A v')) (P i' (@Ret this V A v')))))))) *)
- case=>_ [v][_ ->->->{p q s} _] Ls;  apply: alw_ret'=>// s M.
(* Goal: @InMem (PCM.sort (union_mapPCM Label dstatelet)) (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Mem state (PredPredType state) (Coh W)) *)
(* Goal: @always_sc this W A (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Inject this W A V K w q') scs (fun (m : state) (q : proc this W A) => @ex (UMDef.tp Label dstatelet) (fun i' : UMDef.tp Label dstatelet => @ex (UMDef.tp Label dstatelet) (fun j' : UMDef.tp Label dstatelet => and4 (@eq state m (@PCM.join (union_mapPCM Label dstatelet) i' j')) (@InMem (UMDef.tp Label dstatelet) i' (@Mem state (PredPredType state) (Coh V))) (network_rely (@inj_ext V W K w) this j j') (or (@ex (proc this V A) (fun q' : proc this V A => and (@eq (proc this W A) q (@Inject this W A V K w q')) (P i' q'))) (@ex A (fun v' : A => and (@eq (proc this W A) q (@Ret this W A v')) (P i' (@Ret this V A v')))))))) *)
  case/(rely_ext Ci1): M (M)=>i2 [j2][->{s}] Ci2.
(* Goal: forall (_ : @ex (PCM.sort (union_mapPCM Label dstatelet)) (fun i' : PCM.sort (union_mapPCM Label dstatelet) => @ex (PCM.sort (union_mapPCM Label dstatelet)) (fun j' : PCM.sort (union_mapPCM Label dstatelet) => and4 (@eq state s (@PCM.join (union_mapPCM Label dstatelet) i' j')) (@InMem (PCM.sort (union_mapPCM Label dstatelet)) i' (@Mem state (PredPredType state) (Coh V))) (network_rely (@inj_ext V W K w) this j j') (or (@ex (proc this V A) (fun q' : proc this V A => and (@eq (proc this W A) q (@Inject this W A V K w q')) (forall (v : A) (_ : @eq (proc this V A) q' (@Ret this V A v)), P v i'))) (@ex A (fun v' : A => and (@eq (proc this W A) q (@Ret this W A v')) (forall (v : A) (_ : @eq (proc this V A) (@Ret this V A v') (@Ret this V A v)), P v i'))))))) (v : A) (_ : @eq (proc this W A) q (@Ret this W A v)), @ex (PCM.sort (union_mapPCM Label dstatelet)) (fun i' : PCM.sort (union_mapPCM Label dstatelet) => @ex (PCM.sort (union_mapPCM Label dstatelet)) (fun j' : PCM.sort (union_mapPCM Label dstatelet) => and4 (@eq state s (@PCM.join (union_mapPCM Label dstatelet) i' j')) (@InMem (PCM.sort (union_mapPCM Label dstatelet)) i' (@Mem state (PredPredType state) (Coh V))) (network_rely (@inj_ext V W K w) this j j') (P v i'))) *)
  case/(rely_split Ci1 Ci2)=> /(alw_envs Ls) {Ls} Ls S2.
(* Goal: P v s *)
  exists i2, j2; split=>//; first by apply: rely_trans S1 S2.
  by right;  exists v; move/alw_refl: Ls.
(* Goal: @InMem (PCM.sort (union_mapPCM Label dstatelet)) (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Mem state (PredPredType state) (Coh W)) *)
(* Goal: @always_sc this W A (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Inject this W A V K w q') scs (fun (m : state) (q : proc this W A) => @ex (UMDef.tp Label dstatelet) (fun i' : UMDef.tp Label dstatelet => @ex (UMDef.tp Label dstatelet) (fun j' : UMDef.tp Label dstatelet => and4 (@eq state m (@PCM.join (union_mapPCM Label dstatelet) i' j')) (@InMem (UMDef.tp Label dstatelet) i' (@Mem state (PredPredType state) (Coh V))) (network_rely (@inj_ext V W K w) this j j') (or (@ex (proc this V A) (fun q' : proc this V A => and (@eq (proc this W A) q (@Inject this W A V K w q')) (P i' q'))) (@ex A (fun v' : A => and (@eq (proc this W A) q (@Ret this W A v')) (P i' (@Ret this V A v')))))))) *)
case=>sc' [q'][x1][i2][y1][_ -> E -> {sc q s}] _ T Ls.

(* Goal: @always_sc this W A (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Inject this W A V K w q') scs (fun (m : state) (q : proc this W A) => @ex (UMDef.tp Label dstatelet) (fun i' : UMDef.tp Label dstatelet => @ex (UMDef.tp Label dstatelet) (fun j' : UMDef.tp Label dstatelet => and4 (@eq state m (@PCM.join (union_mapPCM Label dstatelet) i' j')) (@InMem (UMDef.tp Label dstatelet) i' (@Mem state (PredPredType state) (Coh V))) (network_rely (@inj_ext V W K w) this j j') (or (@ex (proc this V A) (fun q' : proc this V A => and (@eq (proc this W A) q (@Inject this W A V K w q')) (P i' q'))) (@ex A (fun v' : A => and (@eq (proc this W A) q (@Ret this W A v')) (P i' (@Ret this V A v')))))))) *)
have [E1 E2] : x1 = i1 /\ y1 = j1.
(* Goal: @InMem (PCM.sort (union_mapPCM Label dstatelet)) (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Mem state (PredPredType state) (Coh W)) *)
(* Goal: @always_sc this W A (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Inject this W A V K w q') scs (fun (m : state) (q : proc this W A) => @ex (UMDef.tp Label dstatelet) (fun i' : UMDef.tp Label dstatelet => @ex (UMDef.tp Label dstatelet) (fun j' : UMDef.tp Label dstatelet => and4 (@eq state m (@PCM.join (union_mapPCM Label dstatelet) i' j')) (@InMem (UMDef.tp Label dstatelet) i' (@Mem state (PredPredType state) (Coh V))) (network_rely (@inj_ext V W K w) this j j') (or (@ex (proc this V A) (fun q' : proc this V A => and (@eq (proc this W A) q (@Inject this W A V K w q')) (P i' q'))) (@ex A (fun v' : A => and (@eq (proc this W A) q (@Ret this W A v')) (P i' (@Ret this V A v')))))))) *)
- case: T=>Cx1 _.
(* Goal: @InMem (PCM.sort (union_mapPCM Label dstatelet)) (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Mem state (PredPredType state) (Coh W)) *)
(* Goal: @always_sc this W A (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Inject this W A V K w q') scs (fun (m : state) (q : proc this W A) => @ex (UMDef.tp Label dstatelet) (fun i' : UMDef.tp Label dstatelet => @ex (UMDef.tp Label dstatelet) (fun j' : UMDef.tp Label dstatelet => and4 (@eq state m (@PCM.join (union_mapPCM Label dstatelet) i' j')) (@InMem (UMDef.tp Label dstatelet) i' (@Mem state (PredPredType state) (Coh V))) (network_rely (@inj_ext V W K w) this j j') (or (@ex (proc this V A) (fun q' : proc this V A => and (@eq (proc this W A) q (@Inject this W A V K w q')) (P i' q'))) (@ex A (fun v' : A => and (@eq (proc this W A) q (@Ret this W A v')) (P i' (@Ret this V A v')))))))) *)
  move: (coh_prec (cohS C) Ci1 Cx1 E) (E)=><-{E Cx1 x1}.
(* Goal: forall _ : @ex A (fun v' : A => and (@eq (proc this (mkWorld (@ProtocolWithIndInv pr I ii)) A) (@Ret this (mkWorld (@ProtocolWithIndInv pr I ii)) A v) (@Ret this (mkWorld (@ProtocolWithIndInv pr I ii)) A v')) (forall (v : A) (_ : @eq (proc this (mkWorld pr) A) (@Ret this (mkWorld pr) A v') (@Ret this (mkWorld pr) A v)), P v s)), P v s *)
  by move/(joinxK (cohS C)).
(* Goal: @always_sc this W A (@PCM.join (union_mapPCM Label dstatelet) i2 y1) (@Inject this W A V K w q') scs (fun (m : state) (q : proc this W A) => @ex (UMDef.tp Label dstatelet) (fun i' : UMDef.tp Label dstatelet => @ex (UMDef.tp Label dstatelet) (fun j' : UMDef.tp Label dstatelet => and4 (@eq state m (@PCM.join (union_mapPCM Label dstatelet) i' j')) (@InMem (UMDef.tp Label dstatelet) i' (@Mem state (PredPredType state) (Coh V))) (network_rely (@inj_ext V W K w) this j j') (or (@ex (proc this V A) (fun q' : proc this V A => and (@eq (proc this W A) q (@Inject this W A V K w q')) (P i' q'))) (@ex A (fun v' : A => and (@eq (proc this W A) q (@Ret this W A v')) (P i' (@Ret this V A v')))))))) *)
rewrite {E x1}E1 {y1}E2 in T *.
(* Goal: network_rely V this s1 s2 *)
(* Goal: network_rely (@inj_ext V W K w) this s1' s2' *)
(* Goal: forall (_ : and (@eq state (@PCM.join (union_mapPCM Label dstatelet) s1 s1') (@PCM.join (union_mapPCM Label dstatelet) s2 s2')) (@InMem state (@PCM.join (union_mapPCM Label dstatelet) s1 s1') (@Mem state (PredPredType state) (Coh W)))) (_ : @InMem state s1 (@Mem state (PredPredType state) (Coh V))) (_ : @InMem state s2 (@Mem state (PredPredType state) (Coh V))), and (network_rely V this s1 s2) (network_rely (@inj_ext V W K w) this s1' s2') *)
have C' : i2 \+ j1 \In Coh W.
(* Goal: @InMem (PCM.sort (union_mapPCM Label dstatelet)) (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Mem state (PredPredType state) (Coh W)) *)
(* Goal: @always_sc this W A (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Inject this W A V K w q') scs (fun (m : state) (q : proc this W A) => @ex (UMDef.tp Label dstatelet) (fun i' : UMDef.tp Label dstatelet => @ex (UMDef.tp Label dstatelet) (fun j' : UMDef.tp Label dstatelet => and4 (@eq state m (@PCM.join (union_mapPCM Label dstatelet) i' j')) (@InMem (UMDef.tp Label dstatelet) i' (@Mem state (PredPredType state) (Coh V))) (network_rely (@inj_ext V W K w) this j j') (or (@ex (proc this V A) (fun q' : proc this V A => and (@eq (proc this W A) q (@Inject this W A V K w q')) (P i' q'))) (@ex A (fun v' : A => and (@eq (proc this W A) q (@Ret this W A v')) (P i' (@Ret this V A v')))))))) *)
- move: (C)=>C'; rewrite (cohE w) in C *=>[[s1]][s2][E]D1 D2.
(* Goal: @InMem (PCM.sort (union_mapPCM Label dstatelet)) (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Mem state (PredPredType state) (Coh W)) *)
(* Goal: @always_sc this W A (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Inject this W A V K w q') scs (fun (m : state) (q : proc this W A) => @ex (UMDef.tp Label dstatelet) (fun i' : UMDef.tp Label dstatelet => @ex (UMDef.tp Label dstatelet) (fun j' : UMDef.tp Label dstatelet => and4 (@eq state m (@PCM.join (union_mapPCM Label dstatelet) i' j')) (@InMem (UMDef.tp Label dstatelet) i' (@Mem state (PredPredType state) (Coh V))) (network_rely (@inj_ext V W K w) this j j') (or (@ex (proc this V A) (fun q' : proc this V A => and (@eq (proc this W A) q (@Inject this W A V K w q')) (P i' q'))) (@ex A (fun v' : A => and (@eq (proc this W A) q (@Ret this W A v')) (P i' (@Ret this V A v')))))))) *)
  move: (coh_prec (cohS C') Ci1 D1 E)=>Z; subst i1.
(* Goal: @InMem (PCM.sort (union_mapPCM Label dstatelet)) (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Mem state (PredPredType state) (Coh W)) *)
(* Goal: @always_sc this W A (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Inject this W A V K w q') scs (fun (m : state) (q : proc this W A) => @ex (UMDef.tp Label dstatelet) (fun i' : UMDef.tp Label dstatelet => @ex (UMDef.tp Label dstatelet) (fun j' : UMDef.tp Label dstatelet => and4 (@eq state m (@PCM.join (union_mapPCM Label dstatelet) i' j')) (@InMem (UMDef.tp Label dstatelet) i' (@Mem state (PredPredType state) (Coh V))) (network_rely (@inj_ext V W K w) this j j') (or (@ex (proc this V A) (fun q' : proc this V A => and (@eq (proc this W A) q (@Inject this W A V K w q')) (P i' q'))) (@ex A (fun v' : A => and (@eq (proc this W A) q (@Ret this W A v')) (P i' (@Ret this V A v')))))))) *)
  move: (joinxK (cohS C') E)=>Z; subst s2; clear E.
(* Goal: @InMem (PCM.sort (union_mapPCM Label dstatelet)) (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Mem state (PredPredType state) (Coh W)) *)
(* Goal: @always_sc this W A (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Inject this W A V K w q') scs (fun (m : state) (q : proc this W A) => @ex (UMDef.tp Label dstatelet) (fun i' : UMDef.tp Label dstatelet => @ex (UMDef.tp Label dstatelet) (fun j' : UMDef.tp Label dstatelet => and4 (@eq state m (@PCM.join (union_mapPCM Label dstatelet) i' j')) (@InMem (UMDef.tp Label dstatelet) i' (@Mem state (PredPredType state) (Coh V))) (network_rely (@inj_ext V W K w) this j j') (or (@ex (proc this V A) (fun q' : proc this V A => and (@eq (proc this W A) q (@Inject this W A V K w q')) (P i' q'))) (@ex A (fun v' : A => and (@eq (proc this W A) q (@Ret this W A v')) (P i' (@Ret this V A v')))))))) *)
  apply/(cohE w); exists i2, j1; split=>//.
(* Goal: forall _ : @ex A (fun v' : A => and (@eq (proc this (mkWorld (@ProtocolWithIndInv pr I ii)) A) (@Ret this (mkWorld (@ProtocolWithIndInv pr I ii)) A v) (@Ret this (mkWorld (@ProtocolWithIndInv pr I ii)) A v')) (forall (v : A) (_ : @eq (proc this (mkWorld pr) A) (@Ret this (mkWorld pr) A v') (@Ret this (mkWorld pr) A v)), P v s)), P v s *)
  by case/step_coh: (pstep_network_sem T). 
(* Goal: @ex (PCM.sort (union_mapPCM Label dstatelet)) (fun i' : PCM.sort (union_mapPCM Label dstatelet) => @ex (PCM.sort (union_mapPCM Label dstatelet)) (fun j' : PCM.sort (union_mapPCM Label dstatelet) => and4 (@eq state (@PCM.join (union_mapPCM Label dstatelet) i1 j1) (@PCM.join (union_mapPCM Label dstatelet) i' j')) (@InMem (PCM.sort (union_mapPCM Label dstatelet)) i' (@Mem state (PredPredType state) (Coh V))) (network_rely (@inj_ext V W K w) this j j') (P v i'))) *)
move/(alw_step Ls): T=>{Ls} Ls.
(* Goal: @always_sc this W A (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Inject this W A V K w q') scs (fun (m : state) (q : proc this W A) => @ex (UMDef.tp Label dstatelet) (fun i' : UMDef.tp Label dstatelet => @ex (UMDef.tp Label dstatelet) (fun j' : UMDef.tp Label dstatelet => and4 (@eq state m (@PCM.join (union_mapPCM Label dstatelet) i' j')) (@InMem (UMDef.tp Label dstatelet) i' (@Mem state (PredPredType state) (Coh V))) (network_rely (@inj_ext V W K w) this j j') (or (@ex (proc this V A) (fun q' : proc this V A => and (@eq (proc this W A) q (@Inject this W A V K w q')) (P i' q'))) (@ex A (fun v' : A => and (@eq (proc this W A) q (@Ret this W A v')) (P i' (@Ret this V A v')))))))) *)
apply: alw_imp' (IH _ _ _ C' Ls)=>{IH Ls C' C Ci Ci1 i i1 i2 p q' sc' scs}.
(* Goal: @InMem (PCM.sort (union_mapPCM Label dstatelet)) (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Mem state (PredPredType state) (Coh W)) *)
(* Goal: @always_sc this W A (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Inject this W A V K w q') scs (fun (m : state) (q : proc this W A) => @ex (UMDef.tp Label dstatelet) (fun i' : UMDef.tp Label dstatelet => @ex (UMDef.tp Label dstatelet) (fun j' : UMDef.tp Label dstatelet => and4 (@eq state m (@PCM.join (union_mapPCM Label dstatelet) i' j')) (@InMem (UMDef.tp Label dstatelet) i' (@Mem state (PredPredType state) (Coh V))) (network_rely (@inj_ext V W K w) this j j') (or (@ex (proc this V A) (fun q' : proc this V A => and (@eq (proc this W A) q (@Inject this W A V K w q')) (P i' q'))) (@ex A (fun v' : A => and (@eq (proc this W A) q (@Ret this W A v')) (P i' (@Ret this V A v')))))))) *)
move=>s p _ [i2][j2][->{s}] Ci2 S2 H; exists i2, j2; split=>//.
(* Goal: forall _ : @ex A (fun v' : A => and (@eq (proc this (mkWorld (@ProtocolWithIndInv pr I ii)) A) (@Ret this (mkWorld (@ProtocolWithIndInv pr I ii)) A v) (@Ret this (mkWorld (@ProtocolWithIndInv pr I ii)) A v')) (forall (v : A) (_ : @eq (proc this (mkWorld pr) A) (@Ret this (mkWorld pr) A v') (@Ret this (mkWorld pr) A v)), P v s)), P v s *)
by apply: rely_trans S1 S2.  
Qed.

(* Goal: @InMem (PCM.sort (union_mapPCM Label dstatelet)) (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Mem state (PredPredType state) (Coh W)) *)
(* Goal: @always_sc this W A (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Inject this W A V K w q') scs (fun (m : state) (q : proc this W A) => @ex (UMDef.tp Label dstatelet) (fun i' : UMDef.tp Label dstatelet => @ex (UMDef.tp Label dstatelet) (fun j' : UMDef.tp Label dstatelet => and4 (@eq state m (@PCM.join (union_mapPCM Label dstatelet) i' j')) (@InMem (UMDef.tp Label dstatelet) i' (@Mem state (PredPredType state) (Coh V))) (network_rely (@inj_ext V W K w) this j j') (or (@ex (proc this V A) (fun q' : proc this V A => and (@eq (proc this W A) q (@Inject this W A V K w q')) (P i' q'))) (@ex A (fun v' : A => and (@eq (proc this W A) q (@Ret this W A v')) (P i' (@Ret this V A v')))))))) *)
Lemma aft_inject (p : proc this V A) (P : A -> state -> Prop) i j :
(* Goal: @InMem (PCM.sort (union_mapPCM Label dstatelet)) (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Mem state (PredPredType state) (Coh W)) *)
(* Goal: @always_sc this W A (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Inject this W A V K w q') scs (fun (m : state) (q : proc this W A) => @ex (UMDef.tp Label dstatelet) (fun i' : UMDef.tp Label dstatelet => @ex (UMDef.tp Label dstatelet) (fun j' : UMDef.tp Label dstatelet => and4 (@eq state m (@PCM.join (union_mapPCM Label dstatelet) i' j')) (@InMem (UMDef.tp Label dstatelet) i' (@Mem state (PredPredType state) (Coh V))) (network_rely (@inj_ext V W K w) this j j') (or (@ex (proc this V A) (fun q' : proc this V A => and (@eq (proc this W A) q (@Inject this W A V K w q')) (P i' q'))) (@ex A (fun v' : A => and (@eq (proc this W A) q (@Ret this W A v')) (P i' (@Ret this V A v')))))))) *)
        i \+ j \In Coh W ->
(* Goal: @InMem (PCM.sort (union_mapPCM Label dstatelet)) (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Mem state (PredPredType state) (Coh W)) *)
(* Goal: @always_sc this W A (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Inject this W A V K w q') scs (fun (m : state) (q : proc this W A) => @ex (UMDef.tp Label dstatelet) (fun i' : UMDef.tp Label dstatelet => @ex (UMDef.tp Label dstatelet) (fun j' : UMDef.tp Label dstatelet => and4 (@eq state m (@PCM.join (union_mapPCM Label dstatelet) i' j')) (@InMem (UMDef.tp Label dstatelet) i' (@Mem state (PredPredType state) (Coh V))) (network_rely (@inj_ext V W K w) this j j') (or (@ex (proc this V A) (fun q' : proc this V A => and (@eq (proc this W A) q (@Inject this W A V K w q')) (P i' q'))) (@ex A (fun v' : A => and (@eq (proc this W A) q (@Ret this W A v')) (P i' (@Ret this V A v')))))))) *)
        after i p P ->
(* Goal: network_rely V this s1 s2 *)
(* Goal: network_rely (@inj_ext V W K w) this s1' s2' *)
(* Goal: forall (_ : and (@eq state (@PCM.join (union_mapPCM Label dstatelet) s1 s1') (@PCM.join (union_mapPCM Label dstatelet) s2 s2')) (@InMem state (@PCM.join (union_mapPCM Label dstatelet) s1 s1') (@Mem state (PredPredType state) (Coh W)))) (_ : @InMem state s1 (@Mem state (PredPredType state) (Coh V))) (_ : @InMem state s2 (@Mem state (PredPredType state) (Coh V))), and (network_rely V this s1 s2) (network_rely (@inj_ext V W K w) this s1' s2') *)
        after (i \+ j) (Inject w p)
          (fun v m => exists i' j', 
(* Goal: network_rely V this s1 s2 *)
(* Goal: network_rely (@inj_ext V W K w) this s1' s2' *)
(* Goal: forall (_ : and (@eq state (@PCM.join (union_mapPCM Label dstatelet) s1 s1') (@PCM.join (union_mapPCM Label dstatelet) s2 s2')) (@InMem state (@PCM.join (union_mapPCM Label dstatelet) s1 s1') (@Mem state (PredPredType state) (Coh W)))) (_ : @InMem state s1 (@Mem state (PredPredType state) (Coh V))) (_ : @InMem state s2 (@Mem state (PredPredType state) (Coh V))), and (network_rely V this s1 s2) (network_rely (@inj_ext V W K w) this s1' s2') *)
             [/\ m = i' \+ j', i' \In Coh V, 
                 network_rely W2 this j j' & P v i']).
Proof.
(* Goal: forall (_ : @InMem state i (@Mem state (PredPredType state) (Coh (mkWorld (@ProtocolWithIndInv pr I ii))))) (_ : @after this (mkWorld pr) A i p P), @after this (mkWorld (@ProtocolWithIndInv pr I ii)) A i (@WithInv this (mkWorld (@ProtocolWithIndInv pr I ii)) A pr I ii (@Logic.eq_refl world (mkWorld (@ProtocolWithIndInv pr I ii))) p) (fun (v : A) (m : state) => and (@InMem state m (@Mem state (PredPredType state) (Coh (mkWorld (@ProtocolWithIndInv pr I ii))))) (P v m)) *)
move=>C /(alw_inject C); apply: alw_imp=>{p i C} s q _.
(* Goal: @InMem (PCM.sort (union_mapPCM Label dstatelet)) (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Mem state (PredPredType state) (Coh W)) *)
(* Goal: @always_sc this W A (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Inject this W A V K w q') scs (fun (m : state) (q : proc this W A) => @ex (UMDef.tp Label dstatelet) (fun i' : UMDef.tp Label dstatelet => @ex (UMDef.tp Label dstatelet) (fun j' : UMDef.tp Label dstatelet => and4 (@eq state m (@PCM.join (union_mapPCM Label dstatelet) i' j')) (@InMem (UMDef.tp Label dstatelet) i' (@Mem state (PredPredType state) (Coh V))) (network_rely (@inj_ext V W K w) this j j') (or (@ex (proc this V A) (fun q' : proc this V A => and (@eq (proc this W A) q (@Inject this W A V K w q')) (P i' q'))) (@ex A (fun v' : A => and (@eq (proc this W A) q (@Ret this W A v')) (P i' (@Ret this V A v')))))))) *)
case=>i1 [j1][->{s} Ci1 S1] H v E.
(* Goal: @InMem (PCM.sort (union_mapPCM Label dstatelet)) (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Mem state (PredPredType state) (Coh W)) *)
(* Goal: @always_sc this W A (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Inject this W A V K w q') scs (fun (m : state) (q : proc this W A) => @ex (UMDef.tp Label dstatelet) (fun i' : UMDef.tp Label dstatelet => @ex (UMDef.tp Label dstatelet) (fun j' : UMDef.tp Label dstatelet => and4 (@eq state m (@PCM.join (union_mapPCM Label dstatelet) i' j')) (@InMem (UMDef.tp Label dstatelet) i' (@Mem state (PredPredType state) (Coh V))) (network_rely (@inj_ext V W K w) this j j') (or (@ex (proc this V A) (fun q' : proc this V A => and (@eq (proc this W A) q (@Inject this W A V K w q')) (P i' q'))) (@ex A (fun v' : A => and (@eq (proc this W A) q (@Ret this W A v')) (P i' (@Ret this V A v')))))))) *)
move: E H=>-> [[q'][//]|[_][[<-]] H].
(* Goal: forall _ : @ex A (fun v' : A => and (@eq (proc this (mkWorld (@ProtocolWithIndInv pr I ii)) A) (@Ret this (mkWorld (@ProtocolWithIndInv pr I ii)) A v) (@Ret this (mkWorld (@ProtocolWithIndInv pr I ii)) A v')) (forall (v : A) (_ : @eq (proc this (mkWorld pr) A) (@Ret this (mkWorld pr) A v') (@Ret this (mkWorld pr) A v)), P v s)), P v s *)
by exists i1, j1; split=>//; apply: H. 
Qed.


End AlwaysInject.

Notation alwsafe_sc s p scs := (always_sc s p scs (fun _ _ => True)).
Notation alwsafe s p := (always s p (fun _ _ => True)).

Module AlwaysInductiveInv.
Section AlwaysInductiveInv.
Import InductiveInv.
Variable pr : protocol.

(* Decompose the initial protocol *)
Notation l := (plab pr).
Notation coh := (coh pr).
(* Goal: @InMem (PCM.sort (union_mapPCM Label dstatelet)) (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Mem state (PredPredType state) (Coh W)) *)
(* Goal: @always_sc this W A (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Inject this W A V K w q') scs (fun (m : state) (q : proc this W A) => @ex (UMDef.tp Label dstatelet) (fun i' : UMDef.tp Label dstatelet => @ex (UMDef.tp Label dstatelet) (fun j' : UMDef.tp Label dstatelet => and4 (@eq state m (@PCM.join (union_mapPCM Label dstatelet) i' j')) (@InMem (UMDef.tp Label dstatelet) i' (@Mem state (PredPredType state) (Coh V))) (network_rely (@inj_ext V W K w) this j j') (or (@ex (proc this V A) (fun q' : proc this V A => and (@eq (proc this W A) q (@Inject this W A V K w q')) (P i' q'))) (@ex A (fun v' : A => and (@eq (proc this W A) q (@Ret this W A v')) (P i' (@Ret this V A v')))))))) *)
Variable I : dstatelet -> pred nid -> Prop.
Variable ii : InductiveInv pr I.

(* Goal: @InMem (PCM.sort (union_mapPCM Label dstatelet)) (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Mem state (PredPredType state) (Coh W)) *)
(* Goal: @always_sc this W A (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Inject this W A V K w q') scs (fun (m : state) (q : proc this W A) => @ex (UMDef.tp Label dstatelet) (fun i' : UMDef.tp Label dstatelet => @ex (UMDef.tp Label dstatelet) (fun j' : UMDef.tp Label dstatelet => and4 (@eq state m (@PCM.join (union_mapPCM Label dstatelet) i' j')) (@InMem (UMDef.tp Label dstatelet) i' (@Mem state (PredPredType state) (Coh V))) (network_rely (@inj_ext V W K w) this j j') (or (@ex (proc this V A) (fun q' : proc this V A => and (@eq (proc this W A) q (@Inject this W A V K w q')) (P i' q'))) (@ex A (fun v' : A => and (@eq (proc this W A) q (@Ret this W A v')) (P i' (@Ret this V A v')))))))) *)
(* Tailored modal always-lemma *)

Variables (A : Type) (this: nid).
Notation V := (mkWorld pr).
Notation W := (mkWorld (ProtocolWithIndInv ii)).

Lemma alw_ind_inv (p : proc this V A)
(* Goal: @InMem (PCM.sort (union_mapPCM Label dstatelet)) (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Mem state (PredPredType state) (Coh W)) *)
(* Goal: @always_sc this W A (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Inject this W A V K w q') scs (fun (m : state) (q : proc this W A) => @ex (UMDef.tp Label dstatelet) (fun i' : UMDef.tp Label dstatelet => @ex (UMDef.tp Label dstatelet) (fun j' : UMDef.tp Label dstatelet => and4 (@eq state m (@PCM.join (union_mapPCM Label dstatelet) i' j')) (@InMem (UMDef.tp Label dstatelet) i' (@Mem state (PredPredType state) (Coh V))) (network_rely (@inj_ext V W K w) this j j') (or (@ex (proc this V A) (fun q' : proc this V A => and (@eq (proc this W A) q (@Inject this W A V K w q')) (P i' q'))) (@ex A (fun v' : A => and (@eq (proc this W A) q (@Ret this W A v')) (P i' (@Ret this V A v')))))))) *)
      (P : state -> proc this V A -> Prop) i :
(* Goal: @InMem (PCM.sort (union_mapPCM Label dstatelet)) (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Mem state (PredPredType state) (Coh W)) *)
(* Goal: @always_sc this W A (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Inject this W A V K w q') scs (fun (m : state) (q : proc this W A) => @ex (UMDef.tp Label dstatelet) (fun i' : UMDef.tp Label dstatelet => @ex (UMDef.tp Label dstatelet) (fun j' : UMDef.tp Label dstatelet => and4 (@eq state m (@PCM.join (union_mapPCM Label dstatelet) i' j')) (@InMem (UMDef.tp Label dstatelet) i' (@Mem state (PredPredType state) (Coh V))) (network_rely (@inj_ext V W K w) this j j') (or (@ex (proc this V A) (fun q' : proc this V A => and (@eq (proc this W A) q (@Inject this W A V K w q')) (P i' q'))) (@ex A (fun v' : A => and (@eq (proc this W A) q (@Ret this W A v')) (P i' (@Ret this V A v')))))))) *)
        i \In Coh W ->
(* Goal: @InMem (PCM.sort (union_mapPCM Label dstatelet)) (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Mem state (PredPredType state) (Coh W)) *)
(* Goal: @always_sc this W A (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Inject this W A V K w q') scs (fun (m : state) (q : proc this W A) => @ex (UMDef.tp Label dstatelet) (fun i' : UMDef.tp Label dstatelet => @ex (UMDef.tp Label dstatelet) (fun j' : UMDef.tp Label dstatelet => and4 (@eq state m (@PCM.join (union_mapPCM Label dstatelet) i' j')) (@InMem (UMDef.tp Label dstatelet) i' (@Mem state (PredPredType state) (Coh V))) (network_rely (@inj_ext V W K w) this j j') (or (@ex (proc this V A) (fun q' : proc this V A => and (@eq (proc this W A) q (@Inject this W A V K w q')) (P i' q'))) (@ex A (fun v' : A => and (@eq (proc this W A) q (@Ret this W A v')) (P i' (@Ret this V A v')))))))) *)
        always i p P ->
        always i (WithInv pr I ii (erefl _) p)
          (fun m q => m \In Coh W /\
                 ((exists q', q = WithInv pr I ii (erefl _) q' /\ P m q') \/
                  (exists v', q = Ret v' /\ P m (Ret v')))).
Proof.
move=>C Ls scs; elim: scs i p C Ls=>[|sc scs IH] i p C Ls /=;
split=>//{C}s M; move: (alw_coh Ls) (proj2 (rely_coh M))=>Ci C.
(* Goal: @InMem (PCM.sort (union_mapPCM Label dstatelet)) (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Mem state (PredPredType state) (Coh W)) *)
(* Goal: @always_sc this W A (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Inject this W A V K w q') scs (fun (m : state) (q : proc this W A) => @ex (UMDef.tp Label dstatelet) (fun i' : UMDef.tp Label dstatelet => @ex (UMDef.tp Label dstatelet) (fun j' : UMDef.tp Label dstatelet => and4 (@eq state m (@PCM.join (union_mapPCM Label dstatelet) i' j')) (@InMem (UMDef.tp Label dstatelet) i' (@Mem state (PredPredType state) (Coh V))) (network_rely (@inj_ext V W K w) this j j') (or (@ex (proc this V A) (fun q' : proc this V A => and (@eq (proc this W A) q (@Inject this W A V K w q')) (P i' q'))) (@ex A (fun v' : A => and (@eq (proc this W A) q (@Ret this W A v')) (P i' (@Ret this V A v')))))))) *)
- split; first by case:(rely_coh M)=>_/with_inv_coh.
  left; exists p; split=>//; apply: alw_refl.
(* Goal: forall _ : @ex A (fun v' : A => and (@eq (proc this (mkWorld (@ProtocolWithIndInv pr I ii)) A) (@Ret this (mkWorld (@ProtocolWithIndInv pr I ii)) A v) (@Ret this (mkWorld (@ProtocolWithIndInv pr I ii)) A v')) (forall (v : A) (_ : @eq (proc this (mkWorld pr) A) (@Ret this (mkWorld pr) A v') (@Ret this (mkWorld pr) A v)), P v s)), P v s *)
  by move/with_inv_rely': M; apply: (alw_envs). 
(* Goal: and3 match sc with | ActStep => True | SeqRet => True | SeqStep sc' => True | InjectStep sc' => @ex (UMDef.tp Label dstatelet) (fun s' : UMDef.tp Label dstatelet => and (@extends V W K w (@PCM.join (union_mapPCM Label dstatelet) i1 j1) s') (@safe this V A p sc' s')) | InjectRet => match p with | Unfinished => True | Ret a => @ex (UMDef.tp Label dstatelet) (fun s' : UMDef.tp Label dstatelet => @extends V W K w (@PCM.join (union_mapPCM Label dstatelet) i1 j1) s') | Act a => True | @Seq _ _ _ B p p0 => True | @Inject _ _ _ V0 K i p => True | WithInv p I0 ii e p0 => True end | WithInvStep sc' => True | WithInvRet => True end (@ex (UMDef.tp Label dstatelet) (fun i' : UMDef.tp Label dstatelet => @ex (UMDef.tp Label dstatelet) (fun j' : UMDef.tp Label dstatelet => and4 (@eq state (@PCM.join (union_mapPCM Label dstatelet) i1 j1) (@PCM.join (union_mapPCM Label dstatelet) i' j')) (@InMem (UMDef.tp Label dstatelet) i' (@Mem state (PredPredType state) (Coh V))) (network_rely (@inj_ext V W K w) this j j') (or (@ex (proc this V A) (fun q' : proc this V A => and (@eq (proc this W A) (@Inject this W A V K w p) (@Inject this W A V K w q')) (P i' q'))) (@ex A (fun v' : A => and (@eq (proc this W A) (@Inject this W A V K w p) (@Ret this W A v')) (P i' (@Ret this V A v')))))))) (forall (s3 : state) (q : proc this W A) (_ : @pstep this W A (@PCM.join (union_mapPCM Label dstatelet) i1 j1) (@Inject this W A V K w p) sc s3 q), @always_sc this W A s3 q scs (fun (m : state) (q0 : proc this W A) => @ex (UMDef.tp Label dstatelet) (fun i' : UMDef.tp Label dstatelet => @ex (UMDef.tp Label dstatelet) (fun j' : UMDef.tp Label dstatelet => and4 (@eq state m (@PCM.join (union_mapPCM Label dstatelet) i' j')) (@InMem (UMDef.tp Label dstatelet) i' (@Mem state (PredPredType state) (Coh V))) (network_rely (@inj_ext V W K w) this j j') (or (@ex (proc this V A) (fun q' : proc this V A => and (@eq (proc this W A) q0 (@Inject this W A V K w q')) (P i' q'))) (@ex A (fun v' : A => and (@eq (proc this W A) q0 (@Ret this W A v')) (P i' (@Ret this V A v'))))))))) *)
split.
(* Goal: @InMem (PCM.sort (union_mapPCM Label dstatelet)) (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Mem state (PredPredType state) (Coh W)) *)
(* Goal: @always_sc this W A (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Inject this W A V K w q') scs (fun (m : state) (q : proc this W A) => @ex (UMDef.tp Label dstatelet) (fun i' : UMDef.tp Label dstatelet => @ex (UMDef.tp Label dstatelet) (fun j' : UMDef.tp Label dstatelet => and4 (@eq state m (@PCM.join (union_mapPCM Label dstatelet) i' j')) (@InMem (UMDef.tp Label dstatelet) i' (@Mem state (PredPredType state) (Coh V))) (network_rely (@inj_ext V W K w) this j j') (or (@ex (proc this V A) (fun q' : proc this V A => and (@eq (proc this W A) q (@Inject this W A V K w q')) (P i' q'))) (@ex A (fun v' : A => and (@eq (proc this W A) q (@Ret this W A v')) (P i' (@Ret this V A v')))))))) *)
- case: sc=>//; last by case: p Ls=>//.
(* Goal: forall (s3 : state) (q : @proc this W A) (_ : @pstep this W A s2 p sc s3 q), @always_sc A s3 q scs (fun (s' : state) (p' : @proc this W A) => forall _ : P, Q s' p') *)
  move=>sc; move: (alw_safe Ls sc)=>Sf.
(* Goal: forall _ : @ex A (fun v' : A => and (@eq (proc this (mkWorld (@ProtocolWithIndInv pr I ii)) A) (@Ret this (mkWorld (@ProtocolWithIndInv pr I ii)) A v) (@Ret this (mkWorld (@ProtocolWithIndInv pr I ii)) A v')) (forall (v : A) (_ : @eq (proc this (mkWorld pr) A) (@Ret this (mkWorld pr) A v') (@Ret this (mkWorld pr) A v)), P v s)), P v s *)
  by move/with_inv_rely': M; move/(alw_envs Ls)=>H; apply: (alw_safe H).
(* Goal: @InMem (PCM.sort (union_mapPCM Label dstatelet)) (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Mem state (PredPredType state) (Coh W)) *)
(* Goal: @always_sc this W A (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Inject this W A V K w q') scs (fun (m : state) (q : proc this W A) => @ex (UMDef.tp Label dstatelet) (fun i' : UMDef.tp Label dstatelet => @ex (UMDef.tp Label dstatelet) (fun j' : UMDef.tp Label dstatelet => and4 (@eq state m (@PCM.join (union_mapPCM Label dstatelet) i' j')) (@InMem (UMDef.tp Label dstatelet) i' (@Mem state (PredPredType state) (Coh V))) (network_rely (@inj_ext V W K w) this j j') (or (@ex (proc this V A) (fun q' : proc this V A => and (@eq (proc this W A) q (@Inject this W A V K w q')) (P i' q'))) (@ex A (fun v' : A => and (@eq (proc this W A) q (@Ret this W A v')) (P i' (@Ret this V A v')))))))) *)
- split=>//; left; exists p; split=>//.
(* Goal: forall _ : @ex A (fun v' : A => and (@eq (proc this (mkWorld (@ProtocolWithIndInv pr I ii)) A) (@Ret this (mkWorld (@ProtocolWithIndInv pr I ii)) A v) (@Ret this (mkWorld (@ProtocolWithIndInv pr I ii)) A v')) (forall (v : A) (_ : @eq (proc this (mkWorld pr) A) (@Ret this (mkWorld pr) A v') (@Ret this (mkWorld pr) A v)), P v s)), P v s *)
  by move/with_inv_rely': M; move/(alw_envs Ls)=>H; apply: alw_refl.
(* Goal: forall (_ : @ex (PCM.sort (union_mapPCM Label dstatelet)) (fun i' : PCM.sort (union_mapPCM Label dstatelet) => @ex (PCM.sort (union_mapPCM Label dstatelet)) (fun j' : PCM.sort (union_mapPCM Label dstatelet) => and4 (@eq state s (@PCM.join (union_mapPCM Label dstatelet) i' j')) (@InMem (PCM.sort (union_mapPCM Label dstatelet)) i' (@Mem state (PredPredType state) (Coh V))) (network_rely (@inj_ext V W K w) this j j') (or (@ex (proc this V A) (fun q' : proc this V A => and (@eq (proc this W A) q (@Inject this W A V K w q')) (forall (v : A) (_ : @eq (proc this V A) q' (@Ret this V A v)), P v i'))) (@ex A (fun v' : A => and (@eq (proc this W A) q (@Ret this W A v')) (forall (v : A) (_ : @eq (proc this V A) (@Ret this V A v') (@Ret this V A v)), P v i'))))))) (v : A) (_ : @eq (proc this W A) q (@Ret this W A v)), @ex (PCM.sort (union_mapPCM Label dstatelet)) (fun i' : PCM.sort (union_mapPCM Label dstatelet) => @ex (PCM.sort (union_mapPCM Label dstatelet)) (fun j' : PCM.sort (union_mapPCM Label dstatelet) => and4 (@eq state s (@PCM.join (union_mapPCM Label dstatelet) i' j')) (@InMem (PCM.sort (union_mapPCM Label dstatelet)) i' (@Mem state (PredPredType state) (Coh V))) (network_rely (@inj_ext V W K w) this j j') (P v i'))) *)
move=>s' q/stepWithInv=>H; case: H Ls.
(* Goal: @InMem (PCM.sort (union_mapPCM Label dstatelet)) (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Mem state (PredPredType state) (Coh W)) *)
(* Goal: @always_sc this W A (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Inject this W A V K w q') scs (fun (m : state) (q : proc this W A) => @ex (UMDef.tp Label dstatelet) (fun i' : UMDef.tp Label dstatelet => @ex (UMDef.tp Label dstatelet) (fun j' : UMDef.tp Label dstatelet => and4 (@eq state m (@PCM.join (union_mapPCM Label dstatelet) i' j')) (@InMem (UMDef.tp Label dstatelet) i' (@Mem state (PredPredType state) (Coh V))) (network_rely (@inj_ext V W K w) this j j') (or (@ex (proc this V A) (fun q' : proc this V A => and (@eq (proc this W A) q (@Inject this W A V K w q')) (P i' q'))) (@ex A (fun v' : A => and (@eq (proc this W A) q (@Ret this W A v')) (P i' (@Ret this V A v')))))))) *)
- case=>[v][Z1]Z2 Z3 Z4 _ _ Ls; subst s' p q sc. apply: alw_ret'=>//=s' M'.
(* Goal: P v s *)
  split; first by case/rely_coh: M'.
  right; exists v; split=>//.
(* Goal: forall _ : @ex A (fun v' : A => and (@eq (proc this (mkWorld (@ProtocolWithIndInv pr I ii)) A) (@Ret this (mkWorld (@ProtocolWithIndInv pr I ii)) A v) (@Ret this (mkWorld (@ProtocolWithIndInv pr I ii)) A v')) (forall (v : A) (_ : @eq (proc this (mkWorld pr) A) (@Ret this (mkWorld pr) A v') (@Ret this (mkWorld pr) A v)), P v s)), P v s *)
  by move: (rely_trans M M')=>/with_inv_rely'/(alw_envs Ls)/alw_refl.
case=>sc'[q'][Z1]Z2 _ _ T Ls; subst q sc.
(* Goal: @always_sc this W A (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Inject this W A V K w q') scs (fun (m : state) (q : proc this W A) => @ex (UMDef.tp Label dstatelet) (fun i' : UMDef.tp Label dstatelet => @ex (UMDef.tp Label dstatelet) (fun j' : UMDef.tp Label dstatelet => and4 (@eq state m (@PCM.join (union_mapPCM Label dstatelet) i' j')) (@InMem (UMDef.tp Label dstatelet) i' (@Mem state (PredPredType state) (Coh V))) (network_rely (@inj_ext V W K w) this j j') (or (@ex (proc this V A) (fun q' : proc this V A => and (@eq (proc this W A) q (@Inject this W A V K w q')) (P i' q'))) (@ex A (fun v' : A => and (@eq (proc this W A) q (@Ret this W A v')) (P i' (@Ret this V A v')))))))) *)
have X: s' \In Coh W by apply: (pstep_inv (proj2 (rely_coh M)) T).
move/with_inv_rely': (M)=>/(alw_envs Ls)=>Ls'.
(* Goal: @ex (PCM.sort (union_mapPCM Label dstatelet)) (fun i' : PCM.sort (union_mapPCM Label dstatelet) => @ex (PCM.sort (union_mapPCM Label dstatelet)) (fun j' : PCM.sort (union_mapPCM Label dstatelet) => and4 (@eq state (@PCM.join (union_mapPCM Label dstatelet) i1 j1) (@PCM.join (union_mapPCM Label dstatelet) i' j')) (@InMem (PCM.sort (union_mapPCM Label dstatelet)) i' (@Mem state (PredPredType state) (Coh V))) (network_rely (@inj_ext V W K w) this j j') (P v i'))) *)
move/(alw_step Ls'): T=>{Ls'} Ls'.
(* Goal: forall _ : @ex A (fun v' : A => and (@eq (proc this (mkWorld (@ProtocolWithIndInv pr I ii)) A) (@Ret this (mkWorld (@ProtocolWithIndInv pr I ii)) A v) (@Ret this (mkWorld (@ProtocolWithIndInv pr I ii)) A v')) (forall (v : A) (_ : @eq (proc this (mkWorld pr) A) (@Ret this (mkWorld pr) A v') (@Ret this (mkWorld pr) A v)), P v s)), P v s *)
by apply: IH.
Qed.

(* Goal: @InMem (PCM.sort (union_mapPCM Label dstatelet)) (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Mem state (PredPredType state) (Coh W)) *)
(* Goal: @always_sc this W A (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Inject this W A V K w q') scs (fun (m : state) (q : proc this W A) => @ex (UMDef.tp Label dstatelet) (fun i' : UMDef.tp Label dstatelet => @ex (UMDef.tp Label dstatelet) (fun j' : UMDef.tp Label dstatelet => and4 (@eq state m (@PCM.join (union_mapPCM Label dstatelet) i' j')) (@InMem (UMDef.tp Label dstatelet) i' (@Mem state (PredPredType state) (Coh V))) (network_rely (@inj_ext V W K w) this j j') (or (@ex (proc this V A) (fun q' : proc this V A => and (@eq (proc this W A) q (@Inject this W A V K w q')) (P i' q'))) (@ex A (fun v' : A => and (@eq (proc this W A) q (@Ret this W A v')) (P i' (@Ret this V A v')))))))) *)
Lemma aft_ind_inv (p : proc this V A) (P : A -> state -> Prop) i :
(* Goal: @InMem (PCM.sort (union_mapPCM Label dstatelet)) (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Mem state (PredPredType state) (Coh W)) *)
(* Goal: @always_sc this W A (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Inject this W A V K w q') scs (fun (m : state) (q : proc this W A) => @ex (UMDef.tp Label dstatelet) (fun i' : UMDef.tp Label dstatelet => @ex (UMDef.tp Label dstatelet) (fun j' : UMDef.tp Label dstatelet => and4 (@eq state m (@PCM.join (union_mapPCM Label dstatelet) i' j')) (@InMem (UMDef.tp Label dstatelet) i' (@Mem state (PredPredType state) (Coh V))) (network_rely (@inj_ext V W K w) this j j') (or (@ex (proc this V A) (fun q' : proc this V A => and (@eq (proc this W A) q (@Inject this W A V K w q')) (P i' q'))) (@ex A (fun v' : A => and (@eq (proc this W A) q (@Ret this W A v')) (P i' (@Ret this V A v')))))))) *)
        i \In Coh W ->
(* Goal: @InMem (PCM.sort (union_mapPCM Label dstatelet)) (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Mem state (PredPredType state) (Coh W)) *)
(* Goal: @always_sc this W A (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Inject this W A V K w q') scs (fun (m : state) (q : proc this W A) => @ex (UMDef.tp Label dstatelet) (fun i' : UMDef.tp Label dstatelet => @ex (UMDef.tp Label dstatelet) (fun j' : UMDef.tp Label dstatelet => and4 (@eq state m (@PCM.join (union_mapPCM Label dstatelet) i' j')) (@InMem (UMDef.tp Label dstatelet) i' (@Mem state (PredPredType state) (Coh V))) (network_rely (@inj_ext V W K w) this j j') (or (@ex (proc this V A) (fun q' : proc this V A => and (@eq (proc this W A) q (@Inject this W A V K w q')) (P i' q'))) (@ex A (fun v' : A => and (@eq (proc this W A) q (@Ret this W A v')) (P i' (@Ret this V A v')))))))) *)
        after i p P ->
        after i (WithInv pr I ii (erefl _) p)
          (fun v m => m \In Coh W /\ P v m).
Proof.
(* Goal: forall (_ : @InMem state i (@Mem state (PredPredType state) (Coh (mkWorld (@ProtocolWithIndInv pr I ii))))) (_ : @after this (mkWorld pr) A i p P), @after this (mkWorld (@ProtocolWithIndInv pr I ii)) A i (@WithInv this (mkWorld (@ProtocolWithIndInv pr I ii)) A pr I ii (@Logic.eq_refl world (mkWorld (@ProtocolWithIndInv pr I ii))) p) (fun (v : A) (m : state) => and (@InMem state m (@Mem state (PredPredType state) (Coh (mkWorld (@ProtocolWithIndInv pr I ii))))) (P v m)) *)
move=>C /(alw_ind_inv C); apply: alw_imp=>{p i C} s q _.
(* Goal: forall (_ : and (@InMem state s (@Mem state (PredPredType state) (Coh (mkWorld (@ProtocolWithIndInv pr I ii))))) (or (@ex (proc this (mkWorld pr) A) (fun q' : proc this (mkWorld pr) A => and (@eq (proc this (mkWorld (@ProtocolWithIndInv pr I ii)) A) q (@WithInv this (mkWorld (@ProtocolWithIndInv pr I ii)) A pr I ii (@Logic.eq_refl world (mkWorld (@ProtocolWithIndInv pr I ii))) q')) (forall (v : A) (_ : @eq (proc this (mkWorld pr) A) q' (@Ret this (mkWorld pr) A v)), P v s))) (@ex A (fun v' : A => and (@eq (proc this (mkWorld (@ProtocolWithIndInv pr I ii)) A) q (@Ret this (mkWorld (@ProtocolWithIndInv pr I ii)) A v')) (forall (v : A) (_ : @eq (proc this (mkWorld pr) A) (@Ret this (mkWorld pr) A v') (@Ret this (mkWorld pr) A v)), P v s))))) (v : A) (_ : @eq (proc this (mkWorld (@ProtocolWithIndInv pr I ii)) A) q (@Ret this (mkWorld (@ProtocolWithIndInv pr I ii)) A v)), and (@InMem state s (@Mem state (PredPredType state) (Coh (mkWorld (@ProtocolWithIndInv pr I ii))))) (P v s) *)
case=>C H; split=>//; subst q.
(* Goal: P v s *)
case:H; first by move=>[?]; case. 
(* Goal: @InMem (PCM.sort (union_mapPCM Label dstatelet)) (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Mem state (PredPredType state) (Coh W)) *)
(* Goal: @always_sc this W A (@PCM.join (union_mapPCM Label dstatelet) i2 j1) (@Inject this W A V K w q') scs (fun (m : state) (q : proc this W A) => @ex (UMDef.tp Label dstatelet) (fun i' : UMDef.tp Label dstatelet => @ex (UMDef.tp Label dstatelet) (fun j' : UMDef.tp Label dstatelet => and4 (@eq state m (@PCM.join (union_mapPCM Label dstatelet) i' j')) (@InMem (UMDef.tp Label dstatelet) i' (@Mem state (PredPredType state) (Coh V))) (network_rely (@inj_ext V W K w) this j j') (or (@ex (proc this V A) (fun q' : proc this V A => and (@eq (proc this W A) q (@Inject this W A V K w q')) (P i' q'))) (@ex A (fun v' : A => and (@eq (proc this W A) q (@Ret this W A v')) (P i' (@Ret this V A v')))))))) *)
by case=>v'[][]<-{v'}/(_ v (erefl _)). 
Qed.

End AlwaysInductiveInv.
End AlwaysInductiveInv.

Export AlwaysInductiveInv.
