proposition: Lemma say : forall (o : Pointer) (p : Process Chnl A), Result o p.
proof: Proof. fix 1. simple destruct p. simple destruct g. case o. intros c1 a0 p0 c2 p1. apply (Tuple Succ (TALK Chnl A c1 a0 p0 c2 p1) c1 (Noise Chnl A c1) p0). apply uttalk4. intros c1 a0 p0 c2 p1. apply (Tuple Fail (TALK Chnl A c1 a0 p0 c2 p1) c1 (Clear Chnl A c1 a0) p0). apply uttalk1. intros. apply Error. red in |- *. intro. inversion_clear H. intros. apply Error. red in |- *. intro. inversion_clear H. intros. apply Error. red in |- *. intro. inversion_clear H. case o. intros. apply Error. red in |- *. intro. inversion_clear H. intros. apply Error. red in |- *. intro. inversion_clear H. intros ol p0 p1. case (say ol p0). simple destruct w. intros q H0. apply (Tuple (Left ol) (PAR Chnl A p0 p1) c (Noise Chnl A c) (PAR Chnl A q p1)). apply utpar4. assumption. intros a q H0. case (listen p1 c a). intros. apply (Tuple (Left ol) (PAR Chnl A p0 p1) c (Clear Chnl A c a) (PAR Chnl A q x)). apply utpar1. assumption. assumption. intros. apply Error. red in |- *. intro H. inversion_clear H. absurd (Wright p0 ol). assumption. assumption. intros or p0 p1. case (say or p1). simple destruct w. intros. apply (Tuple (Right or) (PAR Chnl A p0 p1) c (Noise Chnl A c) (PAR Chnl A p0 q)). apply utpar5. assumption. intros a q H0. case (listen p0 c a). intros. apply (Tuple (Right or) (PAR Chnl A p0 p1) c (Clear Chnl A c a) (PAR Chnl A x q)). apply utpar2. assumption. assumption. intros. apply Error. red in |- *. intro H. inversion_clear H. absurd (Wright p1 or). assumption. assumption. Defined.
imports: ABP.INTERPRETER.Processes