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 SCM+FSA ;
(Exec (f,a := c),s) . (IC SCM+FSA ) = succ (IC s) by Th99;
hence not f,a := c is halting by Th104; :: thesis: verum