let R be 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 ) = (IC the State of (SCM R)) + 1 by Th17;
hence not a := r is halting by Th18; :: thesis: verum