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 set ; :: 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 Instructions 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 = {(abs ((xx - l) + l))} by Th9
.= {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 Instructions of SCMPDS : verum } ;
hence x in SUCC l,SCMPDS by A1, TARSKI:def 4; :: thesis: verum