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