let l be Instruction-Location of SCMPDS ; :: thesis: SUCC l = NAT
thus SUCC l c= NAT ; :: according to XBOOLE_0:def 10 :: thesis: NAT c= SUCC l
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in NAT or x in SUCC l )
assume x in NAT ; :: thesis: x in SUCC l
then reconsider x = x as Instruction-Location of SCMPDS by AMI_1:def 4;
set X = { ((NIC i,l) \ (JUMP i)) where i is Element of the Instructions of SCMPDS : verum } ;
set i = goto ((locnum x) - (locnum l));
NIC (goto ((locnum x) - (locnum l))),l = {(abs (((locnum x) - (locnum l)) + (locnum l)))} by Th14
.= {(locnum x)} by ABSVALUE:def 1
.= {x} by Th8 ;
then A1: x in NIC (goto ((locnum x) - (locnum l))),l by TARSKI:def 1;
(NIC (goto ((locnum x) - (locnum l))),l) \ (JUMP (goto ((locnum x) - (locnum l)))) in { ((NIC i,l) \ (JUMP i)) where i is Element of the Instructions of SCMPDS : verum } ;
hence x in SUCC l by A1, TARSKI:def 4; :: thesis: verum