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 )
set X = { ((NIC i,l) \ (JUMP i)) where i is Element of the Instructions of SCMPDS : verum } ;
assume x in NAT ; :: thesis: x in SUCC l
then reconsider x = x as Instruction-Location of SCMPDS by AMI_1:def 4;
set i = goto (x - l);
NIC (goto (x - l)),l = {(abs ((x - l) + l))} by Th9
.= {x} by ABSVALUE:def 1
.= {x} ;
then A1: x in NIC (goto (x - l)),l by TARSKI:def 1;
(NIC (goto (x - l)),l) \ (JUMP (goto (x - 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