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 Protocols Worlds NetworkSem Rely.
From DiSeL
Require Import Actions Injection Process Always HoareTriples InferenceRules.
From DiSeL
Require Import InductiveInv StatePredicates.
From DiSeL
Require Import CalculatorProtocol.

Section CalculatorInductiveInv.

Variable l : Label.

Variable f : input -> option nat.
Variable prec : input -> bool.
Hypothesis prec_valid :
(* Goal: forall _ : and (@eq (msg TaggedMessage) (@mark_msg TaggedMessage vm) (@Msg TaggedMessage (TMsg resp (@cons nat v args)) to n true)) (@eq (@UMC.sort mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (dsoup d)) s1), @ex (PCM.sort (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)))) (fun s' : PCM.sort (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) => @eq soup (dsoup d) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i' (@Msg TaggedMessage (TMsg resp (@cons nat v args)) to n true)) s')) *)
(* Goal: forall _ : and3 (@eq (@UMC.sort mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i s1) (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i' (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (dsoup d)))) (@eq (@UMC.sort mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (dsoup d)) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@UMC.pts mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i' (@Msg TaggedMessage (TMsg resp (@cons nat v args)) to n true)) (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i s1))) (@eq (@UMC.sort mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) s1 (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@UMC.pts mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@mark_msg TaggedMessage vm)) (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i' (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (dsoup d))))), @ex (PCM.sort (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)))) (fun s' : PCM.sort (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) => @eq soup (dsoup d) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i' (@Msg TaggedMessage (TMsg resp (@cons nat v args)) to n true)) s')) *)
(* Goal: is_true (@PCM.valid (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i (@mark_msg TaggedMessage vm)) (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (dsoup d)))) *)
  forall i, prec i -> exists v, f i = Some v.

Variable cs: seq nid.
Variable cls : seq nid.
(* All nodes *)
Notation nodes := (cs ++ cls).
(* All nodes are unique *)
Hypothesis Huniq : uniq nodes.

(* Protocol and its transitions *)
Notation cal := (CalculatorProtocol f prec cs cls l).
Notation sts := (snd_trans cal).
Notation rts := (rcv_trans cal).

Definition reqs := cstate.
Notation coh := (coh cal).

Notation loc n d := (getLocal n d).

Lemma nodes_falso z : z \in cs -> z \in cls -> False.
Proof.
(* Goal: is_true (@PCM.valid (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i (@mark_msg TaggedMessage vm)) (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (dsoup d)))) *)
move=>H1 H2.
(* Goal: False *)
move: (Huniq); rewrite cat_uniq=>/andP[_]/andP[/negP H]_.
(* Goal: forall _ : is_true (@PCM.valid (union_mapPCM mid (msg TaggedMessage)) (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@mark_msg TaggedMessage vm) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@UMC.pts mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i vm) (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (dsoup d))))), is_true (@PCM.valid (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i (@mark_msg TaggedMessage vm)) (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (dsoup d)))) *)
by apply: H; apply/hasP; exists z.
Qed.

Definition CalcInv d :=
  forall (C: coh d) n to v args i s',
(* Goal: forall _ : and (@eq (msg TaggedMessage) (@mark_msg TaggedMessage vm) (@Msg TaggedMessage (TMsg resp (@cons nat v args)) to n true)) (@eq (@UMC.sort mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (dsoup d)) s1), @ex (PCM.sort (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)))) (fun s' : PCM.sort (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) => @eq soup (dsoup d) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i' (@Msg TaggedMessage (TMsg resp (@cons nat v args)) to n true)) s')) *)
(* Goal: forall _ : and3 (@eq (@UMC.sort mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i s1) (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i' (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (dsoup d)))) (@eq (@UMC.sort mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (dsoup d)) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@UMC.pts mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i' (@Msg TaggedMessage (TMsg resp (@cons nat v args)) to n true)) (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i s1))) (@eq (@UMC.sort mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) s1 (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@UMC.pts mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@mark_msg TaggedMessage vm)) (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i' (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (dsoup d))))), @ex (PCM.sort (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)))) (fun s' : PCM.sort (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) => @eq soup (dsoup d) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i' (@Msg TaggedMessage (TMsg resp (@cons nat v args)) to n true)) s')) *)
(* Goal: is_true (@PCM.valid (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i (@mark_msg TaggedMessage vm)) (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (dsoup d)))) *)
    n \in cls -> to \in cs -> 
(* Goal: forall _ : and (@eq (msg TaggedMessage) (@mark_msg TaggedMessage vm) (@Msg TaggedMessage (TMsg resp (@cons nat v args)) to n true)) (@eq (@UMC.sort mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (dsoup d)) s1), @ex (PCM.sort (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)))) (fun s' : PCM.sort (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) => @eq soup (dsoup d) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i' (@Msg TaggedMessage (TMsg resp (@cons nat v args)) to n true)) s')) *)
(* Goal: forall _ : and3 (@eq (@UMC.sort mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i s1) (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i' (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (dsoup d)))) (@eq (@UMC.sort mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (dsoup d)) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@UMC.pts mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i' (@Msg TaggedMessage (TMsg resp (@cons nat v args)) to n true)) (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i s1))) (@eq (@UMC.sort mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) s1 (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@UMC.pts mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@mark_msg TaggedMessage vm)) (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i' (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (dsoup d))))), @ex (PCM.sort (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)))) (fun s' : PCM.sort (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) => @eq soup (dsoup d) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i' (@Msg TaggedMessage (TMsg resp (@cons nat v args)) to n true)) s')) *)
(* Goal: is_true (@PCM.valid (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i (@mark_msg TaggedMessage vm)) (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (dsoup d)))) *)
    dsoup d = i \\-> (Msg (TMsg resp (v::args)) to n true) \+ s' ->
    f args = Some v.

Notation cal' := (CalculatorProtocol f prec cs cls l).
Notation coh' := (coh cal).
Notation Sinv := (@S_inv cal (fun d _ => CalcInv d)).
Notation Rinv := (@R_inv cal (fun d _ => CalcInv d)).
Notation PI := pf_irr.

Program Definition s1: Sinv (server_send_trans f prec cs cls).
Proof.
(* Goal: is_true (@PCM.valid (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i (@mark_msg TaggedMessage vm)) (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (dsoup d)))) *)
move=>this to d msg S b.
(* Goal: is_true (@PCM.valid (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i (@mark_msg TaggedMessage vm)) (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (dsoup d)))) *)
move=>/= Hi E G C' n to' v' args' i s1 N1 N2/= Es.
(* Goal: forall _ : is_true (CalculatorProtocol.entry_finder f to msg (@pair (Equality.sort (prod_eqType nat_eqType nat_eqType)) (Equality.sort (seq_eqType nat_eqType)) (@pair (Equality.sort nat_eqType) (Equality.sort nat_eqType) me cc) args)), @eq (option nat) (f args') (@Some nat v') *)
case: (S)=>_[_][C]/hasP[[[me cc]args]]_.
(* Goal: forall _ : is_true (CalculatorProtocol.entry_finder f to msg (@pair (Equality.sort (prod_eqType nat_eqType nat_eqType)) (Equality.sort (seq_eqType nat_eqType)) (@pair (Equality.sort nat_eqType) (Equality.sort nat_eqType) me cc) args)), @eq (option nat) (f args') (@Some nat v') *)
case/andP=>/eqP Z1/andP[/eqP Y]/eqP Z2. 
(* Goal: @ex (PCM.sort (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)))) (fun s' : PCM.sort (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) => @eq soup (dsoup d) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i' (@Msg TaggedMessage (TMsg resp (@cons nat v args)) to n true)) s')) *)
move: (cohVs C')=>V; rewrite joinC/= in Es V.
(* Goal: @ex (PCM.sort (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)))) (fun s' : PCM.sort (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) => @eq soup (dsoup d) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i' (@Msg TaggedMessage (TMsg resp (@cons nat v args)) to n true)) s')) *)
(* Goal: is_true (@PCM.valid (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i (@mark_msg TaggedMessage vm)) (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (dsoup d)))) *)
move: (cancel2 V Es)=>/=; case: ifP.
(* Goal: forall _ : and (@eq (msg TaggedMessage) (@mark_msg TaggedMessage vm) (@Msg TaggedMessage (TMsg resp (@cons nat v args)) to n true)) (@eq (@UMC.sort mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (dsoup d)) s1), @ex (PCM.sort (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)))) (fun s' : PCM.sort (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) => @eq soup (dsoup d) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i' (@Msg TaggedMessage (TMsg resp (@cons nat v args)) to n true)) s')) *)
(* Goal: forall _ : and3 (@eq (@UMC.sort mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i s1) (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i' (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (dsoup d)))) (@eq (@UMC.sort mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (dsoup d)) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@UMC.pts mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i' (@Msg TaggedMessage (TMsg resp (@cons nat v args)) to n true)) (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i s1))) (@eq (@UMC.sort mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) s1 (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@UMC.pts mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@mark_msg TaggedMessage vm)) (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i' (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (dsoup d))))), @ex (PCM.sort (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)))) (fun s' : PCM.sort (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) => @eq soup (dsoup d) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i' (@Msg TaggedMessage (TMsg resp (@cons nat v args)) to n true)) s')) *)
(* Goal: is_true (@PCM.valid (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i (@mark_msg TaggedMessage vm)) (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (dsoup d)))) *)
- move=>_; case. case=>Z3 Z4 Z5 Z6; subst s1 to to' msg.
(* Goal: forall _ : and (@eq (msg TaggedMessage) (@mark_msg TaggedMessage vm) (@Msg TaggedMessage (TMsg resp (@cons nat v args)) to n true)) (@eq (@UMC.sort mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (dsoup d)) s1), @ex (PCM.sort (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)))) (fun s' : PCM.sort (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) => @eq soup (dsoup d) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i' (@Msg TaggedMessage (TMsg resp (@cons nat v args)) to n true)) s')) *)
(* Goal: forall _ : and3 (@eq (@UMC.sort mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i s1) (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i' (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (dsoup d)))) (@eq (@UMC.sort mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (dsoup d)) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@UMC.pts mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i' (@Msg TaggedMessage (TMsg resp (@cons nat v args)) to n true)) (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i s1))) (@eq (@UMC.sort mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) s1 (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@UMC.pts mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@mark_msg TaggedMessage vm)) (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i' (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (dsoup d))))), @ex (PCM.sort (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)))) (fun s' : PCM.sort (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) => @eq soup (dsoup d) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i' (@Msg TaggedMessage (TMsg resp (@cons nat v args)) to n true)) s')) *)
(* Goal: is_true (@PCM.valid (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i (@mark_msg TaggedMessage vm)) (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (dsoup d)))) *)
  by simpl in Y; case: Z2=>->.
(* Goal: forall (_ : @eq bool (@eq_op (Ordered.eqType mid) (@fresh (State.msg TaggedMessage) (dsoup d)) i) false) (_ : and3 (@eq (UMDef.tp mid (State.msg TaggedMessage)) (@UMC.free mid (State.msg TaggedMessage) (union_mapUMC mid (State.msg TaggedMessage)) (@fresh (State.msg TaggedMessage) (dsoup d)) s1) (@UMC.free mid (State.msg TaggedMessage) (union_mapUMC mid (State.msg TaggedMessage)) i (dsoup d))) (@eq (UMDef.tp mid (State.msg TaggedMessage)) (dsoup d) (@PCM.join (@union_map_classPCM mid (State.msg TaggedMessage) (union_mapUMC mid (State.msg TaggedMessage))) (@UMC.pts mid (State.msg TaggedMessage) (union_mapUMC mid (State.msg TaggedMessage)) i (@Msg TaggedMessage (TMsg resp (@cons nat v' args')) to' n true)) (@UMC.free mid (State.msg TaggedMessage) (union_mapUMC mid (State.msg TaggedMessage)) (@fresh (State.msg TaggedMessage) (dsoup d)) s1))) (@eq (UMDef.tp mid (State.msg TaggedMessage)) s1 (@PCM.join (@union_map_classPCM mid (State.msg TaggedMessage) (union_mapUMC mid (State.msg TaggedMessage))) (@UMC.pts mid (State.msg TaggedMessage) (union_mapUMC mid (State.msg TaggedMessage)) (@fresh (State.msg TaggedMessage) (dsoup d)) (@Msg TaggedMessage (TMsg CalculatorProtocol.resp msg) this to true)) (@UMC.free mid (State.msg TaggedMessage) (union_mapUMC mid (State.msg TaggedMessage)) i (dsoup d))))), @eq (option nat) (f args') (@Some nat v') *)
move=>_[E1]/=E2 E3; subst to. clear Es V.
(* Goal: forall _ : is_true (@PCM.valid (union_mapPCM mid (msg TaggedMessage)) (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@mark_msg TaggedMessage vm) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@UMC.pts mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i vm) (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (dsoup d))))), is_true (@PCM.valid (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i (@mark_msg TaggedMessage vm)) (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (dsoup d)))) *)
by apply: (Hi C n to' v' args' i _ _ _ E2).
Qed.


Program Definition s2: Sinv (client_send_trans prec cs cls).
Proof.
(* Goal: is_true (@PCM.valid (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i (@mark_msg TaggedMessage vm)) (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (dsoup d)))) *)
move=>this to d msg S b.
(* Goal: is_true (@PCM.valid (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i (@mark_msg TaggedMessage vm)) (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (dsoup d)))) *)
move=>/= Hi E G C' n to' v' args' i s1 N1 N2/= Es.
(* Goal: @ex (PCM.sort (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)))) (fun s' : PCM.sort (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) => @eq soup (dsoup d) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i' (@Msg TaggedMessage (TMsg resp (@cons nat v args)) to n true)) s')) *)
move: (cohVs C')=>V; rewrite joinC/= in Es V.
(* Goal: @ex (PCM.sort (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)))) (fun s' : PCM.sort (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) => @eq soup (dsoup d) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i' (@Msg TaggedMessage (TMsg resp (@cons nat v args)) to n true)) s')) *)
move: (cancel2 V Es)=>/=; case: ifP; last first.
(* Goal: forall _ : and (@eq (msg TaggedMessage) (@mark_msg TaggedMessage vm) (@Msg TaggedMessage (TMsg resp (@cons nat v args)) to n true)) (@eq (@UMC.sort mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (dsoup d)) s1), @ex (PCM.sort (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)))) (fun s' : PCM.sort (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) => @eq soup (dsoup d) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i' (@Msg TaggedMessage (TMsg resp (@cons nat v args)) to n true)) s')) *)
(* Goal: forall _ : and3 (@eq (@UMC.sort mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i s1) (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i' (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (dsoup d)))) (@eq (@UMC.sort mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (dsoup d)) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@UMC.pts mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i' (@Msg TaggedMessage (TMsg resp (@cons nat v args)) to n true)) (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i s1))) (@eq (@UMC.sort mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) s1 (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@UMC.pts mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@mark_msg TaggedMessage vm)) (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i' (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (dsoup d))))), @ex (PCM.sort (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)))) (fun s' : PCM.sort (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) => @eq soup (dsoup d) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i' (@Msg TaggedMessage (TMsg resp (@cons nat v args)) to n true)) s')) *)
(* Goal: is_true (@PCM.valid (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i (@mark_msg TaggedMessage vm)) (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (dsoup d)))) *)
- move=>_[E1]/=E2 E3; clear Es V.
(* Goal: forall _ : is_true (@PCM.valid (union_mapPCM mid (msg TaggedMessage)) (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@mark_msg TaggedMessage vm) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@UMC.pts mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i vm) (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (dsoup d))))), is_true (@PCM.valid (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i (@mark_msg TaggedMessage vm)) (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (dsoup d)))) *)
  by case: (S)=>_[_]C _; apply: (Hi C n to' v' args' i _ _ _ E2).
(* Goal: forall (_ : is_true (@eq_op (Ordered.eqType mid) (@fresh (State.msg TaggedMessage) (dsoup d)) i)) (_ : and (@eq (State.msg TaggedMessage) (@Msg TaggedMessage (TMsg CalculatorProtocol.req msg) this to true) (@Msg TaggedMessage (TMsg resp (@cons nat v' args')) to' n true)) (@eq (UMDef.tp mid (State.msg TaggedMessage)) (dsoup d) s1)), @eq (option nat) (f args') (@Some nat v') *)
move/eqP=>Z; subst i; by case; discriminate.
Qed.

Program Definition r1: Rinv (server_recv_trans prec cs cls).
Proof.
(* Goal: is_true (@PCM.valid (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i (@mark_msg TaggedMessage vm)) (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (dsoup d)))) *)
move=>d from this i C m pf Hi F D Hw Et _.
(* Goal: is_true (@PCM.valid (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i (@mark_msg TaggedMessage vm)) (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (dsoup d)))) *)
move=> C' n to v args i' s1 N1 N2/=Es.
suff Es' : exists s', dsoup d =
(* Goal: forall _ : and (@eq (msg TaggedMessage) (@mark_msg TaggedMessage vm) (@Msg TaggedMessage (TMsg resp (@cons nat v args)) to n true)) (@eq (@UMC.sort mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (dsoup d)) s1), @ex (PCM.sort (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)))) (fun s' : PCM.sort (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) => @eq soup (dsoup d) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i' (@Msg TaggedMessage (TMsg resp (@cons nat v args)) to n true)) s')) *)
(* Goal: forall _ : and3 (@eq (@UMC.sort mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i s1) (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i' (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (dsoup d)))) (@eq (@UMC.sort mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (dsoup d)) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@UMC.pts mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i' (@Msg TaggedMessage (TMsg resp (@cons nat v args)) to n true)) (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i s1))) (@eq (@UMC.sort mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) s1 (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@UMC.pts mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@mark_msg TaggedMessage vm)) (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i' (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (dsoup d))))), @ex (PCM.sort (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)))) (fun s' : PCM.sort (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) => @eq soup (dsoup d) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i' (@Msg TaggedMessage (TMsg resp (@cons nat v args)) to n true)) s')) *)
(* Goal: is_true (@PCM.valid (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i (@mark_msg TaggedMessage vm)) (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (dsoup d)))) *)
       i' \\-> {| content := {| tag := resp; tms_cont := v :: args |};
                  from := to;  to := n;
                  active := true |} \+ s'.
(* Goal: forall _ : is_true (@PCM.valid (union_mapPCM mid (msg TaggedMessage)) (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@mark_msg TaggedMessage vm) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@UMC.pts mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i vm) (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (dsoup d))))), is_true (@PCM.valid (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i (@mark_msg TaggedMessage vm)) (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (dsoup d)))) *)
by case: Es'=>s' Es'; apply: (Hi C n to v args i' _ N1 N2 Es').
(* Goal: @ex (PCM.sort (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)))) (fun s' : PCM.sort (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) => @eq soup (dsoup d) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i' (@Msg TaggedMessage (TMsg resp (@cons nat v args)) to n true)) s')) *)
case B: (i \in dom (dsoup d)); last first.
(* Goal: forall _ : and (@eq (msg TaggedMessage) (@mark_msg TaggedMessage vm) (@Msg TaggedMessage (TMsg resp (@cons nat v args)) to n true)) (@eq (@UMC.sort mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (dsoup d)) s1), @ex (PCM.sort (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)))) (fun s' : PCM.sort (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) => @eq soup (dsoup d) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i' (@Msg TaggedMessage (TMsg resp (@cons nat v args)) to n true)) s')) *)
(* Goal: forall _ : and3 (@eq (@UMC.sort mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i s1) (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i' (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (dsoup d)))) (@eq (@UMC.sort mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (dsoup d)) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@UMC.pts mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i' (@Msg TaggedMessage (TMsg resp (@cons nat v args)) to n true)) (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i s1))) (@eq (@UMC.sort mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) s1 (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@UMC.pts mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@mark_msg TaggedMessage vm)) (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i' (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (dsoup d))))), @ex (PCM.sort (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)))) (fun s' : PCM.sort (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) => @eq soup (dsoup d) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i' (@Msg TaggedMessage (TMsg resp (@cons nat v args)) to n true)) s')) *)
(* Goal: is_true (@PCM.valid (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i (@mark_msg TaggedMessage vm)) (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (dsoup d)))) *)
by move: dom_find B Es; rewrite /consume_msg; case=>//->_->; exists s1.
(* Goal: is_true (@PCM.valid (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i (@mark_msg TaggedMessage vm)) (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (dsoup d)))) *)
move/um_eta: B=>[vm][_]S1.
(* Goal: @ex (PCM.sort (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)))) (fun s' : PCM.sort (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) => @eq soup (dsoup d) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i' (@Msg TaggedMessage (TMsg resp (@cons nat v args)) to n true)) s')) *)
move: (cohVs C)=>V; rewrite S1 in V.
(* Goal: forall _ : is_true (@PCM.valid (union_mapPCM mid (msg TaggedMessage)) (consume_msg (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@UMC.pts mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i vm) (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (dsoup d))) i)), is_true (@PCM.valid (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i (@mark_msg TaggedMessage vm)) (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (dsoup d)))) *)
rewrite S1 joinC consumeUn ?eqxx joinC// in Es. 
(* Goal: forall _ : and (@eq (msg TaggedMessage) (@mark_msg TaggedMessage vm) (@Msg TaggedMessage (TMsg resp (@cons nat v args)) to n true)) (@eq (@UMC.sort mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (dsoup d)) s1), @ex (PCM.sort (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)))) (fun s' : PCM.sort (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) => @eq soup (dsoup d) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i' (@Msg TaggedMessage (TMsg resp (@cons nat v args)) to n true)) s')) *)
(* Goal: forall _ : and3 (@eq (@UMC.sort mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i s1) (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i' (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (dsoup d)))) (@eq (@UMC.sort mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (dsoup d)) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@UMC.pts mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i' (@Msg TaggedMessage (TMsg resp (@cons nat v args)) to n true)) (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i s1))) (@eq (@UMC.sort mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) s1 (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@UMC.pts mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@mark_msg TaggedMessage vm)) (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i' (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (dsoup d))))), @ex (PCM.sort (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)))) (fun s' : PCM.sort (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) => @eq soup (dsoup d) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i' (@Msg TaggedMessage (TMsg resp (@cons nat v args)) to n true)) s')) *)
(* Goal: is_true (@PCM.valid (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i (@mark_msg TaggedMessage vm)) (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (dsoup d)))) *)
suff V': valid (i \\-> mark_msg vm \+
                free (cT:=union_mapUMC mid (msg TaggedMessage)) i (dsoup d)).
(* Goal: forall _ : and (@eq (msg TaggedMessage) (@mark_msg TaggedMessage vm) (@Msg TaggedMessage (TMsg resp (@cons nat v args)) to n true)) (@eq (@UMC.sort mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (dsoup d)) s1), @ex (PCM.sort (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)))) (fun s' : PCM.sort (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) => @eq soup (dsoup d) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i' (@Msg TaggedMessage (TMsg resp (@cons nat v args)) to n true)) s')) *)
(* Goal: forall _ : and3 (@eq (@UMC.sort mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i s1) (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i' (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (dsoup d)))) (@eq (@UMC.sort mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (dsoup d)) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@UMC.pts mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i' (@Msg TaggedMessage (TMsg resp (@cons nat v args)) to n true)) (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i s1))) (@eq (@UMC.sort mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) s1 (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@UMC.pts mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@mark_msg TaggedMessage vm)) (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i' (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (dsoup d))))), @ex (PCM.sort (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)))) (fun s' : PCM.sort (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) => @eq soup (dsoup d) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i' (@Msg TaggedMessage (TMsg resp (@cons nat v args)) to n true)) s')) *)
(* Goal: is_true (@PCM.valid (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i (@mark_msg TaggedMessage vm)) (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (dsoup d)))) *)
- move: (cancel2 V' Es); case: ifP=>B.
(* Goal: forall _ : and (@eq (msg TaggedMessage) (@mark_msg TaggedMessage vm) (@Msg TaggedMessage (TMsg resp (@cons nat v args)) to n true)) (@eq (@UMC.sort mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (dsoup d)) s1), @ex (PCM.sort (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)))) (fun s' : PCM.sort (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) => @eq soup (dsoup d) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i' (@Msg TaggedMessage (TMsg resp (@cons nat v args)) to n true)) s')) *)
(* Goal: forall _ : and3 (@eq (@UMC.sort mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i s1) (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i' (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (dsoup d)))) (@eq (@UMC.sort mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (dsoup d)) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@UMC.pts mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i' (@Msg TaggedMessage (TMsg resp (@cons nat v args)) to n true)) (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i s1))) (@eq (@UMC.sort mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) s1 (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@UMC.pts mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@mark_msg TaggedMessage vm)) (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i' (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (dsoup d))))), @ex (PCM.sort (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)))) (fun s' : PCM.sort (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) => @eq soup (dsoup d) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i' (@Msg TaggedMessage (TMsg resp (@cons nat v args)) to n true)) s')) *)
(* Goal: is_true (@PCM.valid (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i (@mark_msg TaggedMessage vm)) (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (dsoup d)))) *)
  - move/eqP:B=>B{S1 V V' Es}; subst i'.
(* Goal: forall _ : is_true (@PCM.valid (union_mapPCM mid (msg TaggedMessage)) (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@mark_msg TaggedMessage vm) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@UMC.pts mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i vm) (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (dsoup d))))), is_true (@PCM.valid (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i (@mark_msg TaggedMessage vm)) (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (dsoup d)))) *)
    by case: vm=>????/=; rewrite /mark_msg/=; case; discriminate.
(* Goal: forall _ : is_true (@PCM.valid (union_mapPCM mid (msg TaggedMessage)) (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@mark_msg TaggedMessage vm) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@UMC.pts mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i vm) (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (dsoup d))))), is_true (@PCM.valid (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i (@mark_msg TaggedMessage vm)) (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (dsoup d)))) *)
  by case=>_ X2 _; rewrite X2 joinCA in S1; rewrite S1; eexists _. 
(* Goal: is_true (@PCM.valid (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i (@mark_msg TaggedMessage vm)) (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (dsoup d)))) *)
move: (consume_valid i V).
(* Goal: forall _ : is_true (@PCM.valid (union_mapPCM mid (msg TaggedMessage)) (consume_msg (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@UMC.pts mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i vm) (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (dsoup d))) i)), is_true (@PCM.valid (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i (@mark_msg TaggedMessage vm)) (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (dsoup d)))) *)
rewrite /consume_msg/= findUnL// ?domPt inE/= eqxx findPt/=. 
(* Goal: forall _ : is_true (@PCM.valid (union_mapPCM mid (msg TaggedMessage)) (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@mark_msg TaggedMessage vm) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@UMC.pts mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i vm) (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (dsoup d))))), is_true (@PCM.valid (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i (@mark_msg TaggedMessage vm)) (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (dsoup d)))) *)
by rewrite updUnL/= domPt/=!inE eqxx !updPt/=.
Qed.

Program Definition r2: Rinv (client_recv_trans prec cs cls).
Proof.
(* Goal: is_true (@PCM.valid (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i (@mark_msg TaggedMessage vm)) (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (dsoup d)))) *)
move=>d from this i C m pf Hi F D Hw Et _.
(* Goal: is_true (@PCM.valid (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i (@mark_msg TaggedMessage vm)) (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (dsoup d)))) *)
move=> C' n to v args i' s1 N1 N2/=Es.
suff Es' : exists s', dsoup d =
(* Goal: forall _ : and (@eq (msg TaggedMessage) (@mark_msg TaggedMessage vm) (@Msg TaggedMessage (TMsg resp (@cons nat v args)) to n true)) (@eq (@UMC.sort mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (dsoup d)) s1), @ex (PCM.sort (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)))) (fun s' : PCM.sort (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) => @eq soup (dsoup d) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i' (@Msg TaggedMessage (TMsg resp (@cons nat v args)) to n true)) s')) *)
(* Goal: forall _ : and3 (@eq (@UMC.sort mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i s1) (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i' (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (dsoup d)))) (@eq (@UMC.sort mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (dsoup d)) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@UMC.pts mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i' (@Msg TaggedMessage (TMsg resp (@cons nat v args)) to n true)) (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i s1))) (@eq (@UMC.sort mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) s1 (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@UMC.pts mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@mark_msg TaggedMessage vm)) (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i' (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (dsoup d))))), @ex (PCM.sort (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)))) (fun s' : PCM.sort (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) => @eq soup (dsoup d) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i' (@Msg TaggedMessage (TMsg resp (@cons nat v args)) to n true)) s')) *)
(* Goal: is_true (@PCM.valid (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i (@mark_msg TaggedMessage vm)) (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (dsoup d)))) *)
       i' \\-> {| content := {| tag := resp; tms_cont := v :: args |};
                  from := to;  to := n;
                  active := true |} \+ s'.
(* Goal: forall _ : is_true (@PCM.valid (union_mapPCM mid (msg TaggedMessage)) (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@mark_msg TaggedMessage vm) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@UMC.pts mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i vm) (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (dsoup d))))), is_true (@PCM.valid (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i (@mark_msg TaggedMessage vm)) (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (dsoup d)))) *)
by case: Es'=>s' Es'; apply: (Hi C n to v args i' _ N1 N2 Es').
(* Goal: @ex (PCM.sort (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)))) (fun s' : PCM.sort (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) => @eq soup (dsoup d) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i' (@Msg TaggedMessage (TMsg resp (@cons nat v args)) to n true)) s')) *)
case B: (i \in dom (dsoup d)); last first.
(* Goal: forall _ : and (@eq (msg TaggedMessage) (@mark_msg TaggedMessage vm) (@Msg TaggedMessage (TMsg resp (@cons nat v args)) to n true)) (@eq (@UMC.sort mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (dsoup d)) s1), @ex (PCM.sort (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)))) (fun s' : PCM.sort (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) => @eq soup (dsoup d) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i' (@Msg TaggedMessage (TMsg resp (@cons nat v args)) to n true)) s')) *)
(* Goal: forall _ : and3 (@eq (@UMC.sort mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i s1) (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i' (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (dsoup d)))) (@eq (@UMC.sort mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (dsoup d)) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@UMC.pts mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i' (@Msg TaggedMessage (TMsg resp (@cons nat v args)) to n true)) (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i s1))) (@eq (@UMC.sort mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) s1 (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@UMC.pts mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@mark_msg TaggedMessage vm)) (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i' (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (dsoup d))))), @ex (PCM.sort (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)))) (fun s' : PCM.sort (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) => @eq soup (dsoup d) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i' (@Msg TaggedMessage (TMsg resp (@cons nat v args)) to n true)) s')) *)
(* Goal: is_true (@PCM.valid (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i (@mark_msg TaggedMessage vm)) (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (dsoup d)))) *)
by move: dom_find B Es; rewrite /consume_msg; case=>//->_->; exists s1.
(* Goal: is_true (@PCM.valid (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i (@mark_msg TaggedMessage vm)) (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (dsoup d)))) *)
move/um_eta: B=>[vm][_]S1.
(* Goal: @ex (PCM.sort (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)))) (fun s' : PCM.sort (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) => @eq soup (dsoup d) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i' (@Msg TaggedMessage (TMsg resp (@cons nat v args)) to n true)) s')) *)
move: (cohVs C)=>V; rewrite S1 in V.
(* Goal: forall _ : is_true (@PCM.valid (union_mapPCM mid (msg TaggedMessage)) (consume_msg (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@UMC.pts mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i vm) (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (dsoup d))) i)), is_true (@PCM.valid (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i (@mark_msg TaggedMessage vm)) (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (dsoup d)))) *)
rewrite S1 joinC consumeUn ?eqxx joinC// in Es. 
(* Goal: forall _ : and (@eq (msg TaggedMessage) (@mark_msg TaggedMessage vm) (@Msg TaggedMessage (TMsg resp (@cons nat v args)) to n true)) (@eq (@UMC.sort mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (dsoup d)) s1), @ex (PCM.sort (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)))) (fun s' : PCM.sort (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) => @eq soup (dsoup d) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i' (@Msg TaggedMessage (TMsg resp (@cons nat v args)) to n true)) s')) *)
(* Goal: forall _ : and3 (@eq (@UMC.sort mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i s1) (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i' (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (dsoup d)))) (@eq (@UMC.sort mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (dsoup d)) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@UMC.pts mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i' (@Msg TaggedMessage (TMsg resp (@cons nat v args)) to n true)) (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i s1))) (@eq (@UMC.sort mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) s1 (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@UMC.pts mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@mark_msg TaggedMessage vm)) (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i' (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (dsoup d))))), @ex (PCM.sort (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)))) (fun s' : PCM.sort (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) => @eq soup (dsoup d) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i' (@Msg TaggedMessage (TMsg resp (@cons nat v args)) to n true)) s')) *)
(* Goal: is_true (@PCM.valid (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i (@mark_msg TaggedMessage vm)) (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (dsoup d)))) *)
suff V': valid (i \\-> mark_msg vm \+
                free (cT:=union_mapUMC mid (msg TaggedMessage)) i (dsoup d)).
(* Goal: forall _ : and (@eq (msg TaggedMessage) (@mark_msg TaggedMessage vm) (@Msg TaggedMessage (TMsg resp (@cons nat v args)) to n true)) (@eq (@UMC.sort mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (dsoup d)) s1), @ex (PCM.sort (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)))) (fun s' : PCM.sort (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) => @eq soup (dsoup d) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i' (@Msg TaggedMessage (TMsg resp (@cons nat v args)) to n true)) s')) *)
(* Goal: forall _ : and3 (@eq (@UMC.sort mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i s1) (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i' (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (dsoup d)))) (@eq (@UMC.sort mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (dsoup d)) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@UMC.pts mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i' (@Msg TaggedMessage (TMsg resp (@cons nat v args)) to n true)) (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i s1))) (@eq (@UMC.sort mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) s1 (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@UMC.pts mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@mark_msg TaggedMessage vm)) (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i' (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (dsoup d))))), @ex (PCM.sort (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)))) (fun s' : PCM.sort (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) => @eq soup (dsoup d) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i' (@Msg TaggedMessage (TMsg resp (@cons nat v args)) to n true)) s')) *)
(* Goal: is_true (@PCM.valid (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i (@mark_msg TaggedMessage vm)) (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (dsoup d)))) *)
- move: (cancel2 V' Es); case: ifP=>B.
(* Goal: forall _ : and (@eq (msg TaggedMessage) (@mark_msg TaggedMessage vm) (@Msg TaggedMessage (TMsg resp (@cons nat v args)) to n true)) (@eq (@UMC.sort mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (dsoup d)) s1), @ex (PCM.sort (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)))) (fun s' : PCM.sort (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) => @eq soup (dsoup d) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i' (@Msg TaggedMessage (TMsg resp (@cons nat v args)) to n true)) s')) *)
(* Goal: forall _ : and3 (@eq (@UMC.sort mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i s1) (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i' (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (dsoup d)))) (@eq (@UMC.sort mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (dsoup d)) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@UMC.pts mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i' (@Msg TaggedMessage (TMsg resp (@cons nat v args)) to n true)) (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i s1))) (@eq (@UMC.sort mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) s1 (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@UMC.pts mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@mark_msg TaggedMessage vm)) (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i' (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (dsoup d))))), @ex (PCM.sort (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)))) (fun s' : PCM.sort (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) => @eq soup (dsoup d) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i' (@Msg TaggedMessage (TMsg resp (@cons nat v args)) to n true)) s')) *)
(* Goal: is_true (@PCM.valid (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i (@mark_msg TaggedMessage vm)) (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (dsoup d)))) *)
  - move/eqP:B=>B{S1 V V' Es}; subst i'.
(* Goal: forall _ : is_true (@PCM.valid (union_mapPCM mid (msg TaggedMessage)) (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@mark_msg TaggedMessage vm) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@UMC.pts mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i vm) (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (dsoup d))))), is_true (@PCM.valid (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i (@mark_msg TaggedMessage vm)) (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (dsoup d)))) *)
    by case: vm=>????/=; rewrite /mark_msg/=; case; discriminate.
(* Goal: forall _ : is_true (@PCM.valid (union_mapPCM mid (msg TaggedMessage)) (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@mark_msg TaggedMessage vm) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@UMC.pts mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i vm) (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (dsoup d))))), is_true (@PCM.valid (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i (@mark_msg TaggedMessage vm)) (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (dsoup d)))) *)
  by case=>_ X2 _; rewrite X2 joinCA in S1; rewrite S1; eexists _. 
(* Goal: is_true (@PCM.valid (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i (@mark_msg TaggedMessage vm)) (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (dsoup d)))) *)
move: (consume_valid i V).
(* Goal: forall _ : is_true (@PCM.valid (union_mapPCM mid (msg TaggedMessage)) (consume_msg (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@UMC.pts mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i vm) (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (dsoup d))) i)), is_true (@PCM.valid (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i (@mark_msg TaggedMessage vm)) (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (dsoup d)))) *)
rewrite /consume_msg/= findUnL// ?domPt inE/= eqxx findPt/=. 
(* Goal: forall _ : is_true (@PCM.valid (union_mapPCM mid (msg TaggedMessage)) (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@mark_msg TaggedMessage vm) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@UMC.pts mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i vm) (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (dsoup d))))), is_true (@PCM.valid (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i (@mark_msg TaggedMessage vm)) (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (dsoup d)))) *)
by rewrite updUnL/= domPt/=!inE eqxx !updPt/=.
Qed.

Definition sts' := [:: SI s1; SI s2].
Definition rts' := [:: RI r1; RI r2].

Program Definition ii := @ProtocolWithInvariant.II _ _ sts' rts' _ _.

Definition cal_with_inv := ProtocolWithIndInv ii.

(**************************************************)
(*
Overall Implementation effort:

(* Goal: forall _ : and (@eq (msg TaggedMessage) (@mark_msg TaggedMessage vm) (@Msg TaggedMessage (TMsg resp (@cons nat v args)) to n true)) (@eq (@UMC.sort mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (dsoup d)) s1), @ex (PCM.sort (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)))) (fun s' : PCM.sort (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) => @eq soup (dsoup d) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i' (@Msg TaggedMessage (TMsg resp (@cons nat v args)) to n true)) s')) *)
(* Goal: forall _ : and3 (@eq (@UMC.sort mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i s1) (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i' (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (dsoup d)))) (@eq (@UMC.sort mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (dsoup d)) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@UMC.pts mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i' (@Msg TaggedMessage (TMsg resp (@cons nat v args)) to n true)) (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i s1))) (@eq (@UMC.sort mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) s1 (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@UMC.pts mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@mark_msg TaggedMessage vm)) (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i' (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (dsoup d))))), @ex (PCM.sort (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)))) (fun s' : PCM.sort (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) => @eq soup (dsoup d) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i' (@Msg TaggedMessage (TMsg resp (@cons nat v args)) to n true)) s')) *)
(* Goal: is_true (@PCM.valid (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i (@mark_msg TaggedMessage vm)) (@UMC.free mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (dsoup d)))) *)
1 person-day

*)
(**************************************************)

        

End CalculatorInductiveInv.

