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