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 Element of NAT holds (Exec (b₁,s)) . b₂ = s . b₂
let i be Instruction of SCMPDS; :: thesis: for b₁ being Element of NAT holds (Exec (i,s)) . b₁ = s . b₁
let l be Element of NAT ; :: thesis: (Exec (i,s)) . l = s . l
thus (Exec (i,s)) . l = s . l by Th96; :: thesis: verum

end;

assume the Instruction-Counter of SCMPDS in NAT ; :: according to COMPOS_1:def 12 :: thesis: contradiction
hence contradiction by Th6; :: thesis: verum