let k be Integer; :: thesis: JUMP (goto k) = {}
set i = goto k;
set X = { (NIC ((goto k),l)) where l is Nat : verum } ;
hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: {} c= JUMP (goto k)
set l2 = 0 ;
set l1 = 1;
let x be object ; :: thesis: ( x in JUMP (goto k) implies b1 in {} )
assume A1: x in JUMP (goto k) ; :: thesis: b1 in {}
NIC ((goto k),0) in { (NIC ((goto k),l)) where l is Nat : verum } ;
then x in NIC ((goto k),0) by A1, SETFAM_1:def 1;
then consider s2 being Element of product (the_Values_of SCMPDS) such that
A2: x = IC (Exec ((goto k),s2)) and
A3: IC s2 = 0 ;
consider m2 being Element of NAT such that
A4: m2 = IC s2 and
A5: ICplusConst (s2,k) = |.(m2 + k).| by SCMPDS_2:def 18;
NIC ((goto k),1) in { (NIC ((goto k),l)) where l is Nat : verum } ;
then x in NIC ((goto k),1) by A1, SETFAM_1:def 1;
then consider s1 being Element of product (the_Values_of SCMPDS) such that
A6: x = IC (Exec ((goto k),s1)) and
A7: IC s1 = 1 ;
consider m1 being Element of NAT such that
A8: m1 = IC s1 and
A9: ICplusConst (s1,k) = |.(m1 + k).| by SCMPDS_2:def 18;
|.(m2 + k).| = ICplusConst (s2,k) by A5
.= IC (Exec ((goto k),s2)) by SCMPDS_2:54
.= IC (Exec ((goto k),s1)) by A2, A6
.= ICplusConst (s1,k) by SCMPDS_2:54
.= |.(m1 + k).| by A9 ;
per cases then ( 0 + k = 1 + k or 0 + k = - (1 + k) ) by A7, A8, A3, A4, ABSVALUE:28;
suppose 0 + k = 1 + k ; :: thesis: b1 in {}
hence x in {} ; :: thesis: verum
end;
suppose 0 + k = - (1 + k) ; :: thesis: b1 in {}
then - (- (1 / 2)) is integer ;
hence x in {} by NAT_D:33; :: thesis: verum
end;
end;
end;
thus {} c= JUMP (goto k) ; :: thesis: verum