proposition: Theorem simulator : forall (x : List Pointer) (p : Process Chnl A), Trace x p.
proof: Proof. cofix. intros x p. case x. apply Stop. intros o y. case (say o p). intros c w q H0. apply (Evolve o y c p q w). assumption. apply simulator. intros H. apply (Refuse o y p). assumption. apply simulator. Defined.
imports: ABP.INTERPRETER.Processes