proposition: Lemma ACK_UinvTC2 : forall (P : bool -> Process -> bool -> Prop) (v : bool) (q : Process) (b : bool), P b (ACKING b) b -> UnrelProcTrans Channel Act lnk2 (ACK b) (Transmit _ Act lnk2 (Clear _ Act lnk2 v)) q -> P v q b.
proof: Proof. intros P v q b H. rewrite (unfold_ACK b). intros H2. simple inversion H2. injection H1 as <-. rewrite (inj_Tmess lnk2 v0 b p (ACKING b) c2 lnk1 f (fun b1 : bool * A => ACK b)) . rewrite <- H3. injection H0 as ? ->. assumption. assumption. discriminate H1. discriminate H3. discriminate H1. discriminate H3. discriminate H1. discriminate H3. discriminate H3. discriminate H3. discriminate H3. discriminate H3. Defined.
imports: ABP.ABP.BISIMULATION.Hypotheses