theorem Th27: :: SCMPDS_5:40

for P being Instruction-Sequence of SCMPDS
for s being 0 -started State of SCMPDS
for i being parahalting Instruction of SCMPDS holds Exec (i,s) = IExec ((Load i),P,s)