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