let a be Int_position; :: thesis: for l being Element of NAT

for k1 being Integer holds NIC ((saveIC (a,k1)),l) = {(l + 1)}

let l be Element of NAT ; :: thesis: for k1 being Integer holds NIC ((saveIC (a,k1)),l) = {(l + 1)}

let k1 be Integer; :: thesis: NIC ((saveIC (a,k1)),l) = {(l + 1)}

set i = saveIC (a,k1);

for s being State of SCMPDS st IC s = l holds

(Exec ((saveIC (a,k1)),s)) . (IC ) = (IC s) + 1 by SCMPDS_2:59;

hence NIC ((saveIC (a,k1)),l) = {(l + 1)} by Th1; :: thesis: verum

for k1 being Integer holds NIC ((saveIC (a,k1)),l) = {(l + 1)}

let l be Element of NAT ; :: thesis: for k1 being Integer holds NIC ((saveIC (a,k1)),l) = {(l + 1)}

let k1 be Integer; :: thesis: NIC ((saveIC (a,k1)),l) = {(l + 1)}

set i = saveIC (a,k1);

for s being State of SCMPDS st IC s = l holds

(Exec ((saveIC (a,k1)),s)) . (IC ) = (IC s) + 1 by SCMPDS_2:59;

hence NIC ((saveIC (a,k1)),l) = {(l + 1)} by Th1; :: thesis: verum