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