thus SCMPDS is steady-programmed :: thesis: SCMPDS is realistic

proof

let s be State of SCMPDS ; :: according to AMI_1:def 13 :: thesis: for b₁ being Element of the Instructions of SCMPDS
for b₂ being Instruction-Location of SCMPDS holds (Exec b₁,s) . b₂ = s . b₂
let i be Instruction of SCMPDS ; :: thesis: for b₁ being Instruction-Location of SCMPDS holds (Exec i,s) . b₁ = s . b₁
let l be Instruction-Location of SCMPDS ; :: thesis: (Exec i,s) . l = s . l
thus (Exec i,s) . l = s . l by Th96; :: thesis: verum

end;

thus SCMPDS is realistic by Th97; :: thesis: verum