let k be Integer; JUMP (goto k) = {}
set i = goto k;
set X = { (NIC ((goto k),l)) where l is Nat : verum } ;
hereby TARSKI:def 3,
XBOOLE_0:def 10 {} c= JUMP (goto k)
set l2 =
0 ;
set l1 = 1;
let x be
object ;
( x in JUMP (goto k) implies b1 in {} )assume A1:
x in JUMP (goto k)
;
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
;
end;
thus
{} c= JUMP (goto k)
; verum