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