let a be Int_position ; :: thesis: for l being Element of NAT
for k1 being Integer holds NIC ((a := k1),l) = {(succ l)}
let l be Element of NAT ; :: thesis: for k1 being Integer holds NIC ((a := k1),l) = {(succ l)}
let k1 be Integer; :: thesis: NIC ((a := k1),l) = {(succ l)}
set i = a := k1;
for s being State of SCMPDS st IC s = l holds
(Exec ((a := k1),s)) . (IC ) = succ (IC s) by SCMPDS_2:45;
hence NIC ((a := k1),l) = {(succ l)} by Th7; :: thesis: verum