let l be Element of NAT ; :: thesis: SUCC (l,SCMPDS) = NAT

thus SUCC (l,SCMPDS) c= NAT ; :: according to XBOOLE_0:def 10 :: thesis: NAT c= SUCC (l,SCMPDS)

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in NAT or x in SUCC (l,SCMPDS) )

set X = { ((NIC (i,l)) \ (JUMP i)) where i is Element of the InstructionsF of SCMPDS : verum } ;

assume x in NAT ; :: thesis: x in SUCC (l,SCMPDS)

then reconsider x = x as Element of NAT ;

reconsider xx = x as Element of NAT ;

set i = goto (xx - l);

NIC ((goto (xx - l)),l) = {|.((xx - l) + l).|} by Th3

.= {x} by ABSVALUE:def 1 ;

then A1: x in (NIC ((goto (xx - l)),l)) \ (JUMP (goto (xx - l))) by TARSKI:def 1;

(NIC ((goto (xx - l)),l)) \ (JUMP (goto (xx - l))) in { ((NIC (i,l)) \ (JUMP i)) where i is Element of the InstructionsF of SCMPDS : verum } ;

hence x in SUCC (l,SCMPDS) by A1, TARSKI:def 4; :: thesis: verum

thus SUCC (l,SCMPDS) c= NAT ; :: according to XBOOLE_0:def 10 :: thesis: NAT c= SUCC (l,SCMPDS)

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in NAT or x in SUCC (l,SCMPDS) )

set X = { ((NIC (i,l)) \ (JUMP i)) where i is Element of the InstructionsF of SCMPDS : verum } ;

assume x in NAT ; :: thesis: x in SUCC (l,SCMPDS)

then reconsider x = x as Element of NAT ;

reconsider xx = x as Element of NAT ;

set i = goto (xx - l);

NIC ((goto (xx - l)),l) = {|.((xx - l) + l).|} by Th3

.= {x} by ABSVALUE:def 1 ;

then A1: x in (NIC ((goto (xx - l)),l)) \ (JUMP (goto (xx - l))) by TARSKI:def 1;

(NIC ((goto (xx - l)),l)) \ (JUMP (goto (xx - l))) in { ((NIC (i,l)) \ (JUMP i)) where i is Element of the InstructionsF of SCMPDS : verum } ;

hence x in SUCC (l,SCMPDS) by A1, TARSKI:def 4; :: thesis: verum