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