set D = Int-Locations \/ FinSeq-Locations ;
let s be State of SCM+FSA ; :: thesis: for I being parahalting Program of SCM+FSA
for a being Int-Location st I does_not_destroy a holds
(IExec I,s) . a = (Initialize s) . a
let I be parahalting Program of SCM+FSA ; :: thesis: for a being Int-Location st I does_not_destroy a holds
(IExec I,s) . a = (Initialize s) . a
let a be Int-Location ; :: thesis: ( I does_not_destroy a implies (IExec I,s) . a = (Initialize s) . a )
assume A1: I does_not_destroy a ; :: thesis: (IExec I,s) . a = (Initialize s) . a
A2: DataPart (Initialize s) = DataPart ((Initialize s) +* (I +* (Start-At (insloc 0 )))) by SCMFSA8A:11;
thus (IExec I,s) . a = (Computation ((Initialize s) +* (I +* (Start-At (insloc 0 )))),0 ) . a by A1, Th90
.= ((Initialize s) +* (I +* (Start-At (insloc 0 )))) . a by AMI_1:13
.= (Initialize s) . a by A2, SCMFSA6A:38 ; :: thesis: verum