Retrofiting of:
CpsG.thy (the parallel copy of PIPBasics.thy),
ExtGG.thy (The paralell copy of Implemenation.thy),
PrioG.thy (The paralell copy of Correctness.thy)
has completed.
The next step is to overwite original copies with the paralell ones.
There are low priority threads,
which do not hold any resources,
such thread will not block th.
Theorem 3 does not exclude such threads.
There are resources, which are not held by any low prioirty threads,
such resources can not cause blockage of th neither. And similiary,
theorem 6 does not exlude them.
Our one bound excudle them by using a different formaulation.