theorem Th20: :: SCM_HALT:22

for p being Instruction-Sequence of SCM+FSA
for I being InitHalting keepInt0_1 Program of SCM+FSA
for s being State of SCM+FSA holds DataPart (Initialized (IExec (I,p,s))) = DataPart (IExec (I,p,s))