proposition: Lemma State4 : forall (b : bool) (s : Stream A) (c : Channel) (w : Signal _ Act c) (q : Process), Trans c (SENDING b s || ACK b) (Transmit _ Act c w) q -> c = lnk1 /\ q = SENDING b s || ACK b \/ c = lnk2 /\ q = SEND (negb b) (tl s) || ACKING b \/ existS (Signal Channel Act) c w = existS (Signal Channel Act) lnk2 (Noise _ Act lnk2) /\ q = SENDING b s || ACKING 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 ACK_UinvR. auto. intros p3 p5 v UTL UTR. inversion UTR using ACK_UinvTC1. intros p3 UTL. rewrite (SENDING_ULoosed b s p3). auto. assumption. intros p4 UTR. inversion UTR using ACK_UinvT1. 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 ACK_UinvTC2 in UTL. inversion UTL using SENDING_UinvR. rewrite (eqb_reflx b). auto. intros p3 UTL. inversion UTL using SENDING_UinvT2. intros p4 UTR. rewrite (ACK_ULoosed b lnk2 p4). auto. assumption. 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 ACK_SinvT. Defined.
imports: ABP.ABP.TRACES.Hypotheses