proposition: Lemma ACKING_UinvR : forall (P : bool * A -> Process -> bool -> Prop) (v : bool * A) (q : Process) (b : bool), P v (let (b1, a) := v in if eqb b1 (negb b) then OUT (negb b) a else ACK b) b -> UnrelProcTrans Channel Act lnk1 (ACKING b) (Receive _ Act lnk1 v) q -> P v q b.
proof: Proof. intros P b1 q b H. rewrite unfold_ACKING. intros H0. simple inversion H0. discriminate H2. discriminate H1. discriminate H2. discriminate H1. rewrite <- H4. rewrite (inj_Lfun lnk1 f (fun v : bool * A => let (b1, a) := v in if eqb b1 (negb b) then OUT (negb b) a else ACK b)) . intro. rewrite <- H1. injection H3 as ->. assumption. assumption. intro. absurd (d = lnk1). assumption. injection H2; trivial. discriminate H3. discriminate H3. discriminate H3. discriminate H3. discriminate H3. Defined.
imports: ABP.ABP.BISIMULATION.Hypotheses