let s be State of SCM+FSA ; :: thesis: for I being InitHalting Program of SCM+FSA
for a being Int-Location st not I destroysdestroy a holds
(IExec I,s) . a = (Initialized s) . a
let I be InitHalting Program of SCM+FSA ; :: thesis: for a being Int-Location st not I destroysdestroy a holds
(IExec I,s) . a = (Initialized s) . a
let a be Int-Location ; :: thesis: ( not I destroysdestroy a implies (IExec I,s) . a = (Initialized s) . a )
A1: DataPart (Initialized s) = DataPart ((Initialized s) +* (I +* (Start-At 0 ,SCM+FSA ))) by SCMFSA8A:11;
assume not I destroysdestroy a ; :: thesis: (IExec I,s) . a = (Initialized s) . a
hence (IExec I,s) . a = (Comput (ProgramPart ((Initialized s) +* (I +* (Start-At 0 ,SCM+FSA )))),((Initialized s) +* (I +* (Start-At 0 ,SCM+FSA ))),0 ) . a by Th62
.= ((Initialized s) +* (I +* (Start-At 0 ,SCM+FSA ))) . a by AMI_1:13
.= (Initialized s) . a by A1, SCMFSA6A:38 ;
:: thesis: verum