Assumptionless example

This MR contains the definitions and lemmas of a concrete job-generation function in pair with the concrete arrival sequence. These facts sit at the basis of POET' s assumption-less examples, used to prove the absence of contradicting hypotheses in abstract RTA and the certificates.

Additionally, it adds some helper functions and a class instance that were missing in the concrete task files (MaxArrivals).

I currently explicitly phrased the new file and comments as "assumption-less example", but we should probably instead call this differently. I propose "concrete_job_generation".