prove sRTA (starting with a non-IID system)

rt/analysis/pRTA/pRTA_full.v

rt/analysis/scheduler_properties.v

rt/analysis/transformation_properties.v

rt/analysis/work_bound.v

util/seq.v