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