let k be Integer; :: thesis: JUMP (goto k) = {}

set i = goto k;

set X = { (NIC ((goto k),l)) where l is Nat : verum } ;

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)

thus
{} c= JUMP (goto k)
; :: thesis: verumset l2 = 0 ;

set l1 = 1;

let x be object ; :: thesis: ( x in JUMP (goto k) implies b_{1} in {} )

assume A1: x in JUMP (goto k) ; :: thesis: b_{1} 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 ;

end;set l1 = 1;

let x be object ; :: thesis: ( x in JUMP (goto k) implies b

assume A1: x in JUMP (goto k) ; :: thesis: b

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 ;