AG(proc1.proc_state = READING -> AF(proc1.proc_state=IDLE));