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

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