let I be good really-closed parahalting MacroInstruction of SCM+FSA ; :: thesis: for a being read-write Int-Location st not I destroys a holds
Initialize ((intloc 0) .--> 1) is Times (a,I) -halted
let a be read-write Int-Location; :: thesis: ( not I destroys a implies Initialize ((intloc 0) .--> 1) is Times (a,I) -halted )
assume A1: not I destroys a ; :: thesis: Initialize ((intloc 0) .--> 1) is Times (a,I) -halted
now :: thesis: for s being State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA holds Times (a,I) is_halting_on Initialized s,P
let s be State of SCM+FSA; :: thesis: for P being Instruction-Sequence of SCM+FSA holds Times (a,I) is_halting_on Initialized s,P
let P be Instruction-Sequence of SCM+FSA; :: thesis: Times (a,I) is_halting_on Initialized s,P
(Initialized s) . (intloc 0) = 1 by SCMFSA_M:5;
hence Times (a,I) is_halting_on Initialized s,P by A1, Th56; :: thesis: verum
end;
hence Initialize ((intloc 0) .--> 1) is Times (a,I) -halted by SCMFSA8C:5; :: thesis: verum