let f be FinSeq-Location ; :: thesis: for a, c being Int-Location holds not f,a := c is halting
let a, c be Int-Location ; :: thesis: not f,a := c is halting
consider s being State of ;
(Exec (f,a := c),s) . (IC SCM+FSA ) = Next by Th99;
hence not f,a := c is halting by Th104; :: thesis: verum