let p be Instruction-Sequence of SCM+FSA; :: thesis: for s being State of SCM+FSA
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)),p & J is_closed_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 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)),p & J is_closed_on Exec (i,(Initialized s)),p ) ) holds
DataPart (IExec ((i ';' J),p,s)) = DataPart (IExec (J,p,(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)),p & J is_closed_on Exec (i,(Initialized s)),p ) ) holds
DataPart (IExec ((i ';' J),p,s)) = DataPart (IExec (J,p,(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)),p & J is_closed_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 & J is_closed_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 Th16;
for a being Int-Location holds (IExec ((i ';' J),p,s)) . a = (IExec (J,p,(Exec (i,(Initialized s))))) . a by A1, Th15;
hence DataPart (IExec ((i ';' J),p,s)) = DataPart (IExec (J,p,(Exec (i,(Initialized s))))) by A2, SCMFSA6A:7; :: thesis: verum