let a be Int_position ; :: thesis: for l being Instruction-Location of SCMPDS
for k1 being Integer holds NIC (saveIC a,k1),l = {(Next l)}
let l be Instruction-Location of SCMPDS ; :: thesis: for k1 being Integer holds NIC (saveIC a,k1),l = {(Next l)}
let k1 be Integer; :: thesis: NIC (saveIC a,k1),l = {(Next l)}
set i = saveIC a,k1;
for s being State of SCMPDS st IC s = l & s . l = saveIC a,k1 holds
(Exec (saveIC a,k1),s) . (IC SCMPDS ) = Next (IC s) by SCMPDS_2:71;
hence NIC (saveIC a,k1),l = {(Next l)} by Th12; :: thesis: verum