Appendices C-G to "Repairing time-determinism in the process algebra for hybrid systems ACPhssrt"

Abstract Appendix C. In this section of the Appendix we give the semantics for BPAsrt with future inconsistency, as it was developed in [15]. In Appendix E, we show that the semantics used in this paper is in fact equivalent to the semantics of [15]. Abstract Appendix D. In this section we prove, for process terms x and y of BPAsrt , that x = y implies [formula] . Abstract Appendix E. In this appendix, we prove that the following axioms are sound for the semantics of BPAsrt hs given in section 4.2 of this paper. Abstract Appendix F. In this section we prove that the axiomatization of Bergstra and Middelburg is sound for the semantics given in appendix C. Furthermore, we prove that axiom HSE13 also holds for r = 0. Abstract Appendix G. In this section we prove that the axiom [formula] is sound for the semantics given in appendix C.