let R be good Ring; :: thesis: for r being Element of R
for a being Data-Location of R holds not a := r is halting
let r be Element of R; :: thesis: for a being Data-Location of R holds not a := r is halting
let a be Data-Location of R; :: thesis: not a := r is halting
set s = the State of (SCM R);
(Exec ((a := r), the State of (SCM R))) . (IC ) = succ (IC the State of (SCM R)) by Th19;
hence not a := r is halting by Th20; :: thesis: verum