proposition: Lemma State2 : forall (b : bool) (s : Stream A) (c : Channel) (w : Signal _ Act c) (q : Process), Trans c (SENDING b s || ACKING (negb b)) (Transmit _ Act c w) q -> c = lnk1 /\ q = SENDING b s || OUT b (hd s) \/ existS (Signal Channel Act) c w = existS (Signal Channel Act) lnk1 (Noise _ Act lnk1) /\ q = SENDING b s || ACKING (negb b).
proof: Proof. simple destruct c; simpl in |- *. intros w q T. inversion T using PAR_UinvT. intros p3 p5 v UTL. inversion UTL using SENDING_UinvTC1. intro UTR. inversion UTR using ACKING_UinvR. rewrite (negb_elim b). rewrite (eqb_reflx b). auto. intros p3 p5 v UTL UTR. inversion UTR using ACKING_UinvT. intros p3 UTL. rewrite (SENDING_ULoosed b s p3). auto. assumption. intros p4 UTR. inversion UTR using ACKING_UinvT. intros w q T. inversion T using PAR_UinvT. intros p3 p5 v UTL. inversion UTL using SENDING_UinvT2. intros p3 p5 v UTL UTR. inversion UTR using ACKING_UinvT. intros p3 UTL. inversion UTL using SENDING_UinvT2. intros p3 UTR. inversion UTR using ACKING_UinvT. intros w q T. inversion T using PAR_SinvT. intros p3 p5 v UTL. inversion UTL using SENDING_SinvT. intros p3 p5 v UTL UTR. inversion UTR using ACKING_SinvT. Defined.
imports: ABP.ABP.TRACES.Hypotheses