Port non-seq aRTA

Mostly it is just a copy-paste of the old Abstract RTA.

However, I add a new section FixpointIsNoLessThanArrival in file abstract_rta.v; so comments are very welcome.

PDF-file for convenience: abstract.core.abstract_rta.pdf