let s be State of SCM+FSA ; :: thesis: for I being InitHalting 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 InitHalting 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 )
A1: DataPart (Initialize s) = DataPart ((Initialize s) +* (I +* (Start-At 0 ,SCM+FSA ))) by SCMFSA8A:11;
assume I does_not_destroy a ; :: thesis: (IExec I,s) . a = (Initialize s) . a
hence (IExec I,s) . a = (Comput (ProgramPart ((Initialize s) +* (I +* (Start-At 0 ,SCM+FSA )))),((Initialize s) +* (I +* (Start-At 0 ,SCM+FSA ))),0 ) . a by Th62
.= ((Initialize s) +* (I +* (Start-At 0 ,SCM+FSA ))) . a by AMI_1:13
.= (Initialize s) . a by A1, SCMFSA6A:38 ;
:: thesis: verum