let p be Instruction-Sequence of SCM+FSA; :: thesis: for s being State of SCM+FSA
for i being sequential good Instruction of SCM+FSA
for J being really-closed Program of SCM+FSA st ( J is parahalting or J is_halting_on Exec (i,(Initialized s)),p ) holds
DataPart (IExec ((i ";" J),p,s)) = DataPart (IExec (J,p,(Exec (i,(Initialized s)))))
let s be State of SCM+FSA; :: thesis: for i being sequential good Instruction of SCM+FSA
for J being really-closed Program of SCM+FSA st ( J is parahalting or J is_halting_on Exec (i,(Initialized s)),p ) holds
DataPart (IExec ((i ";" J),p,s)) = DataPart (IExec (J,p,(Exec (i,(Initialized s)))))
let i be sequential good Instruction of SCM+FSA; :: thesis: for J being really-closed Program of SCM+FSA st ( J is parahalting or J is_halting_on Exec (i,(Initialized s)),p ) holds
DataPart (IExec ((i ";" J),p,s)) = DataPart (IExec (J,p,(Exec (i,(Initialized s)))))
let J be really-closed Program of SCM+FSA; :: thesis: ( ( J is parahalting or J is_halting_on Exec (i,(Initialized s)),p ) implies DataPart (IExec ((i ";" J),p,s)) = DataPart (IExec (J,p,(Exec (i,(Initialized s))))) )
assume A1: ( J is parahalting or J is_halting_on Exec (i,(Initialized s)),p ) ; :: thesis: DataPart (IExec ((i ";" J),p,s)) = DataPart (IExec (J,p,(Exec (i,(Initialized s)))))
then A2: for f being FinSeq-Location holds (IExec ((i ";" J),p,s)) . f = (IExec (J,p,(Exec (i,(Initialized s))))) . f by Th14;
for a being Int-Location holds (IExec ((i ";" J),p,s)) . a = (IExec (J,p,(Exec (i,(Initialized s))))) . a by A1, Th13;
hence DataPart (IExec ((i ";" J),p,s)) = DataPart (IExec (J,p,(Exec (i,(Initialized s))))) by A2, SCMFSA_M:2; :: thesis: verum