let s be State of SCM+FSA; :: thesis: for J being Program of SCM+FSA
for i being parahalting good Instruction of SCM+FSA st ( J is parahalting or ( J is_halting_on Exec (i,(Initialized s)) & J is_closed_on Exec (i,(Initialized s)) ) ) holds
DataPart (IExec ((i ';' J),s)) = DataPart (IExec (J,(Exec (i,(Initialized s)))))
let J be Program of SCM+FSA; :: thesis: for i being parahalting good Instruction of SCM+FSA st ( J is parahalting or ( J is_halting_on Exec (i,(Initialized s)) & J is_closed_on Exec (i,(Initialized s)) ) ) holds
DataPart (IExec ((i ';' J),s)) = DataPart (IExec (J,(Exec (i,(Initialized s)))))
let i be parahalting good Instruction of SCM+FSA; :: thesis: ( ( J is parahalting or ( J is_halting_on Exec (i,(Initialized s)) & J is_closed_on Exec (i,(Initialized s)) ) ) implies DataPart (IExec ((i ';' J),s)) = DataPart (IExec (J,(Exec (i,(Initialized s))))) )
assume A1: ( J is parahalting or ( J is_halting_on Exec (i,(Initialized s)) & J is_closed_on Exec (i,(Initialized s)) ) ) ; :: thesis: DataPart (IExec ((i ';' J),s)) = DataPart (IExec (J,(Exec (i,(Initialized s)))))
then A2: for f being FinSeq-Location holds (IExec ((i ';' J),s)) . f = (IExec (J,(Exec (i,(Initialized s))))) . f by Th16;
for a being Int-Location holds (IExec ((i ';' J),s)) . a = (IExec (J,(Exec (i,(Initialized s))))) . a by A1, Th15;
hence DataPart (IExec ((i ';' J),s)) = DataPart (IExec (J,(Exec (i,(Initialized s))))) by A2, SCMFSA6A:38; :: thesis: verum