:: SCMPDS_9 semantic presentation

begin


definition
let la, lb be Int_position;
let a, b be Integer;
:: original: -->
redefine func(la,lb) --> (a,b) ->  PartState of SCMPDS;
coherence
 (la,lb) --> (a,b) is PartState of SCMPDS
proof
A1: ( Values la = INT & Values lb = INT ) by SCMPDS_2:5;
A2: ( a is Element of INT & b is Element of INT ) by INT_1:def_2;
reconsider a = a as Element of Values la by A1, A2;
reconsider b = b as Element of Values lb by A1, A2;
 (la,lb) --> (a,b) is PartState of SCMPDS ;
hence  (la,lb) --> (a,b) is PartState of SCMPDS ; ::_thesis: verum
end;
end;

Lm1:  for k being Integer holds JUMP (goto k) = {}
proof
let k be Integer; ::_thesis: JUMP (goto k) = {}
set i = goto k;
set X =  {  (NIC ((goto k),l)) where l is Element of NAT : verum  }  ;
hereby  :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: {} c= JUMP (goto k)
set l2 = 1;
set l1 = 0 ;
let x be set ; ::_thesis: ( x in JUMP (goto k) implies b1 in {} )
assume A1: x in JUMP (goto k) ; ::_thesis: b1 in {}
 NIC ((goto k),1) in  {  (NIC ((goto k),l)) where l is Element of NAT : verum  }  ;
then  x in NIC ((goto k),1) 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 = 1 ;
consider m2 being Element of NAT  such that
A4: m2 = IC s2 and
A5: ICplusConst (s2,k) = abs (m2 + k) by SCMPDS_2:def_18;
 NIC ((goto k),0) in  {  (NIC ((goto k),l)) where l is Element of NAT : verum  }  ;
then  x in NIC ((goto k),0) 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 = 0 ;
consider m1 being Element of NAT  such that
A8: m1 = IC s1 and
A9: ICplusConst (s1,k) = abs (m1 + k) by SCMPDS_2:def_18;
A10: x = abs (m1 + k) by A6, A9, SCMPDS_2:54;
percases ( 0 + k = 1 + k or k = - (1 + k) ) by A7, A8, A10, A3, A4, A2, A5, ABSVALUE:28, SCMPDS_2:54;
suppose 0 + k = 1 + k ; ::_thesis: b1 in {}
hence  x in {} ; ::_thesis: verum
end;
suppose 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) by XBOOLE_1:2; ::_thesis: verum
end;

registration
let k be Integer;
cluster JUMP (goto k) ->  empty ;
coherence
 JUMP (goto k) is empty by Lm1;
end;

theorem Th1: :: SCMPDS_9:1
for i being Instruction of SCMPDS
for l being Element of NAT st ( for s being State of SCMPDS st IC s = l holds
(Exec (i,s)) . (IC ) = succ (IC s) ) holds
NIC (i,l) = {(succ l)}
proof
let i be Instruction of SCMPDS; ::_thesis: for l being Element of NAT st ( for s being State of SCMPDS st IC s = l holds
(Exec (i,s)) . (IC ) = succ (IC s) ) holds
NIC (i,l) = {(succ l)}
let l be Element of NAT ; ::_thesis: ( ( for s being State of SCMPDS st IC s = l holds
(Exec (i,s)) . (IC ) = succ (IC s) ) implies NIC (i,l) = {(succ l)} )
reconsider I = i as Instruction of SCMPDS ;
reconsider n = l as Element of NAT ;
assume A1: for s being State of SCMPDS st IC s = l holds
(Exec (i,s)) . (IC ) = succ (IC s) ; ::_thesis: NIC (i,l) = {(succ l)}
hereby  :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: {(succ l)} c= NIC (i,l)
let x be set ; ::_thesis: ( x in NIC (i,l) implies x in {(succ l)} )
assume  x in NIC (i,l) ; ::_thesis: x in {(succ l)}
then consider s being Element of product (the_Values_of SCMPDS) such that
A2: x = IC (Exec (i,s)) and
A3: IC s = l ;
 x = succ l by A1, A2, A3;
hence  x in {(succ l)} by TARSKI:def_1; ::_thesis: verum
end;
set t = the l -started State of SCMPDS;
reconsider t = the l -started State of SCMPDS as Element of product (the_Values_of SCMPDS) by CARD_3:107;
A4: IC t = l by MEMSTR_0:def_11;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {(succ l)} or x in NIC (i,l) )
assume  x in {(succ l)} ; ::_thesis: x in NIC (i,l)
then A5: x = succ l by TARSKI:def_1;
 IC (Exec (I,t)) = succ l by A1, A4;
hence  x in NIC (i,l) by A5, A4; ::_thesis: verum
end;

theorem Th2: :: SCMPDS_9:2
for i being Instruction of SCMPDS st ( for l being Element of NAT holds NIC (i,l) = {(succ l)} ) holds
JUMP i is empty
proof
let i be Instruction of SCMPDS; ::_thesis: ( ( for l being Element of NAT holds NIC (i,l) = {(succ l)} ) implies JUMP i is empty )
set p = 1;
set q = 2;
assume A1: for l being Element of NAT holds NIC (i,l) = {(succ l)} ; ::_thesis: JUMP i is empty
set X =  {  (NIC (i,f)) where f is Element of NAT : verum  }  ;
reconsider p = 1, q = 2 as Element of NAT ;
assume  not JUMP i is empty ; ::_thesis: contradiction
then consider x being set  such that
A2: x in meet  {  (NIC (i,f)) where f is Element of NAT : verum  }  by XBOOLE_0:def_1;
 NIC (i,p) = {(succ p)} by A1;
then  {(succ p)} in  {  (NIC (i,f)) where f is Element of NAT : verum  }  ;
then  x in {(succ p)} by A2, SETFAM_1:def_1;
then A3: x = succ p by TARSKI:def_1;
 NIC (i,q) = {(succ q)} by A1;
then  {(succ q)} in  {  (NIC (i,f)) where f is Element of NAT : verum  }  ;
then  x in {(succ q)} by A2, SETFAM_1:def_1;
hence  contradiction by A3, TARSKI:def_1; ::_thesis: verum
end;

theorem Th3: :: SCMPDS_9:3
for l being Element of NAT
for k being Integer holds NIC ((goto k),l) = {(abs (k + l))}
proof
let l be Element of NAT ; ::_thesis: for k being Integer holds NIC ((goto k),l) = {(abs (k + l))}
let k be Integer; ::_thesis: NIC ((goto k),l) = {(abs (k + l))}
set s = the State of SCMPDS;
set i = goto k;
set t = abs (k + l);
set I = goto k;
reconsider n = l as Element of NAT ;
hereby  :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: {(abs (k + l))} c= NIC ((goto k),l)
let x be set ; ::_thesis: ( x in NIC ((goto k),l) implies x in {(abs (k + l))} )
assume  x in NIC ((goto k),l) ; ::_thesis: x in {(abs (k + l))}
then consider s being Element of product (the_Values_of SCMPDS) such that
A1: x = IC (Exec ((goto k),s)) and
A2: IC s = l ;
A3: ex m1 being Element of NAT st
( m1 = IC s & ICplusConst (s,k) = abs (m1 + k) ) by SCMPDS_2:def_18;
 x = abs (k + l) by A1, A2, A3, SCMPDS_2:54;
hence  x in {(abs (k + l))} by TARSKI:def_1; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {(abs (k + l))} or x in NIC ((goto k),l) )
reconsider u = the n -started State of SCMPDS as Element of product (the_Values_of SCMPDS) by CARD_3:107;
A4: IC u = n by MEMSTR_0:def_11;
consider m1 being Element of NAT  such that
A5: m1 = IC u and
A6: ICplusConst (u,k) = abs (m1 + k) by SCMPDS_2:def_18;
assume  x in {(abs (k + l))} ; ::_thesis: x in NIC ((goto k),l)
then x = abs (m1 + k) by A4, A5, TARSKI:def_1
.= IC (Exec ((goto k),u)) by A6, SCMPDS_2:54 ;
hence  x in NIC ((goto k),l) by A4; ::_thesis: verum
end;

Lm2:  for k being Nat st k > 1 holds
k - 2 is Element of NAT
proof
let k be Nat; ::_thesis: ( k > 1 implies k - 2 is Element of NAT )
assume  k > 1 ; ::_thesis: k - 2 is Element of NAT
then  k >= 1 + 1 by NAT_1:13;
then  k - 2 >= 2 - 2 by XREAL_1:9;
hence  k - 2 is Element of NAT by INT_1:3; ::_thesis: verum
end;

theorem Th4: :: SCMPDS_9:4
for a being Int_position
for l being Element of NAT holds NIC ((return a),l) =  {  k where k is Element of NAT : k > 1  }
proof
let a be Int_position; ::_thesis: for l being Element of NAT holds NIC ((return a),l) =  {  k where k is Element of NAT : k > 1  }
let l be Element of NAT ; ::_thesis: NIC ((return a),l) =  {  k where k is Element of NAT : k > 1  }
set s = the State of SCMPDS;
set X =  {  k where k is Element of NAT : k > 1  }  ;
set i = return a;
hereby  :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis:  {  k where k is Element of NAT : k > 1  }  c= NIC ((return a),l)
let x be set ; ::_thesis: ( x in NIC ((return a),l) implies x in  {  k where k is Element of NAT : k > 1  }  )
assume  x in NIC ((return a),l) ; ::_thesis: x in  {  k where k is Element of NAT : k > 1  }
then consider s being Element of product (the_Values_of SCMPDS) such that
A1: x = IC (Exec ((return a),s)) and
 IC s = l ;
reconsider k = x as Element of NAT by A1;
A2: (abs (s . (DataLoc ((s . a),1)))) + 2 >= 0 + 2 by XREAL_1:6;
 k >= 1 + 1 by A2, A1, SCMPDS_2:58, SCMPDS_I:def_14;
then  k > 1 by NAT_1:13;
hence  x in  {  k where k is Element of NAT : k > 1  }  ; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  k where k is Element of NAT : k > 1  }  or x in NIC ((return a),l) )
set I = return a;
reconsider n = l as Element of NAT ;
assume  x in  {  k where k is Element of NAT : k > 1  }  ; ::_thesis: x in NIC ((return a),l)
then consider k being Element of NAT  such that
A3: x = k and
A4: k > 1 ;
reconsider k2 = k - 2 as Element of NAT by A4, Lm2;
reconsider u = the n -started State of SCMPDS as Element of product (the_Values_of SCMPDS) by CARD_3:107;
A5: IC u = n by MEMSTR_0:def_11;
 a in SCM-Data-Loc by AMI_2:def_16;
then consider j being Element of NAT  such that
A6: a = [1,j] by AMI_2:23;
set t = [1,(j + 1)];
 [1,(j + 1)] in SCM-Data-Loc by AMI_2:24;
then reconsider t1 = [1,(j + 1)] as Int_position by AMI_2:def_16;
A7: DataLoc (j,1) = [1,(abs (j + 1))]
.= [1,(j + 1)] by ABSVALUE:def_1 ;
set g = (a,t1) --> (j,k2);
reconsider v = u +* ((a,t1) --> (j,k2)) as Element of product (the_Values_of SCMPDS) by CARD_3:107;
A8: dom ((a,t1) --> (j,k2)) = {a,[1,(j + 1)]} by FUNCT_4:62;
 j <> j + 1 ;
then A9: a <> [1,(j + 1)] by A6, XTUPLE_0:1;
then A10: v . a = j by FUNCT_4:84;
 ( a <> IC & t1 <> IC ) by SCMPDS_2:43;
then A11: not IC in dom ((a,t1) --> (j,k2)) by A8, TARSKI:def_2;
A12: IC v = l by A5, A11, FUNCT_4:11;
A13: v . [1,(j + 1)] = k2 by A9, FUNCT_4:84;
x = k2 + 2 by A3
.= (abs (v . (DataLoc (j,1)))) + 2 by A13, A7, ABSVALUE:def_1
.= IC (Exec ((return a),v)) by A10, SCMPDS_2:58, SCMPDS_I:def_14 ;
hence  x in NIC ((return a),l) by A12; ::_thesis: verum
end;

theorem Th5: :: SCMPDS_9:5
for a being Int_position
for l being Element of NAT
for k1 being Integer holds NIC ((saveIC (a,k1)),l) = {(succ l)}
proof
let a be Int_position; ::_thesis: for l being Element of NAT
for k1 being Integer holds NIC ((saveIC (a,k1)),l) = {(succ l)}
let l be Element of NAT ; ::_thesis: for k1 being Integer holds NIC ((saveIC (a,k1)),l) = {(succ l)}
let k1 be Integer; ::_thesis: NIC ((saveIC (a,k1)),l) = {(succ l)}
set i = saveIC (a,k1);
 for s being State of SCMPDS st IC s = l holds
(Exec ((saveIC (a,k1)),s)) . (IC ) = succ (IC s) by SCMPDS_2:59;
hence  NIC ((saveIC (a,k1)),l) = {(succ l)} by Th1; ::_thesis: verum
end;

theorem Th6: :: SCMPDS_9:6
for a being Int_position
for l being Element of NAT
for k1 being Integer holds NIC ((a := k1),l) = {(succ l)}
proof
let a be Int_position; ::_thesis: for l being Element of NAT
for k1 being Integer holds NIC ((a := k1),l) = {(succ l)}
let l be Element of NAT ; ::_thesis: for k1 being Integer holds NIC ((a := k1),l) = {(succ l)}
let k1 be Integer; ::_thesis: NIC ((a := k1),l) = {(succ l)}
set i = a := k1;
 for s being State of SCMPDS st IC s = l holds
(Exec ((a := k1),s)) . (IC ) = succ (IC s) by SCMPDS_2:45;
hence  NIC ((a := k1),l) = {(succ l)} by Th1; ::_thesis: verum
end;

theorem Th7: :: SCMPDS_9:7
for a being Int_position
for l being Element of NAT
for k1, k2 being Integer holds NIC (((a,k1) := k2),l) = {(succ l)}
proof
let a be Int_position; ::_thesis: for l being Element of NAT
for k1, k2 being Integer holds NIC (((a,k1) := k2),l) = {(succ l)}
let l be Element of NAT ; ::_thesis: for k1, k2 being Integer holds NIC (((a,k1) := k2),l) = {(succ l)}
let k1, k2 be Integer; ::_thesis: NIC (((a,k1) := k2),l) = {(succ l)}
set i = (a,k1) := k2;
 for s being State of SCMPDS st IC s = l holds
(Exec (((a,k1) := k2),s)) . (IC ) = succ (IC s) by SCMPDS_2:46;
hence  NIC (((a,k1) := k2),l) = {(succ l)} by Th1; ::_thesis: verum
end;

theorem Th8: :: SCMPDS_9:8
for a, b being Int_position
for l being Element of NAT
for k1, k2 being Integer holds NIC (((a,k1) := (b,k2)),l) = {(succ l)}
proof
let a, b be Int_position; ::_thesis: for l being Element of NAT
for k1, k2 being Integer holds NIC (((a,k1) := (b,k2)),l) = {(succ l)}
let l be Element of NAT ; ::_thesis: for k1, k2 being Integer holds NIC (((a,k1) := (b,k2)),l) = {(succ l)}
let k1, k2 be Integer; ::_thesis: NIC (((a,k1) := (b,k2)),l) = {(succ l)}
set i = (a,k1) := (b,k2);
 for s being State of SCMPDS st IC s = l holds
(Exec (((a,k1) := (b,k2)),s)) . (IC ) = succ (IC s) by SCMPDS_2:47;
hence  NIC (((a,k1) := (b,k2)),l) = {(succ l)} by Th1; ::_thesis: verum
end;

theorem Th9: :: SCMPDS_9:9
for a being Int_position
for l being Element of NAT
for k1, k2 being Integer holds NIC ((AddTo (a,k1,k2)),l) = {(succ l)}
proof
let a be Int_position; ::_thesis: for l being Element of NAT
for k1, k2 being Integer holds NIC ((AddTo (a,k1,k2)),l) = {(succ l)}
let l be Element of NAT ; ::_thesis: for k1, k2 being Integer holds NIC ((AddTo (a,k1,k2)),l) = {(succ l)}
let k1, k2 be Integer; ::_thesis: NIC ((AddTo (a,k1,k2)),l) = {(succ l)}
set i = AddTo (a,k1,k2);
 for s being State of SCMPDS st IC s = l holds
(Exec ((AddTo (a,k1,k2)),s)) . (IC ) = succ (IC s) by SCMPDS_2:48;
hence  NIC ((AddTo (a,k1,k2)),l) = {(succ l)} by Th1; ::_thesis: verum
end;

theorem Th10: :: SCMPDS_9:10
for a, b being Int_position
for l being Element of NAT
for k1, k2 being Integer holds NIC ((AddTo (a,k1,b,k2)),l) = {(succ l)}
proof
let a, b be Int_position; ::_thesis: for l being Element of NAT
for k1, k2 being Integer holds NIC ((AddTo (a,k1,b,k2)),l) = {(succ l)}
let l be Element of NAT ; ::_thesis: for k1, k2 being Integer holds NIC ((AddTo (a,k1,b,k2)),l) = {(succ l)}
let k1, k2 be Integer; ::_thesis: NIC ((AddTo (a,k1,b,k2)),l) = {(succ l)}
set i = AddTo (a,k1,b,k2);
 for s being State of SCMPDS st IC s = l holds
(Exec ((AddTo (a,k1,b,k2)),s)) . (IC ) = succ (IC s) by SCMPDS_2:49;
hence  NIC ((AddTo (a,k1,b,k2)),l) = {(succ l)} by Th1; ::_thesis: verum
end;

theorem Th11: :: SCMPDS_9:11
for a, b being Int_position
for l being Element of NAT
for k1, k2 being Integer holds NIC ((SubFrom (a,k1,b,k2)),l) = {(succ l)}
proof
let a, b be Int_position; ::_thesis: for l being Element of NAT
for k1, k2 being Integer holds NIC ((SubFrom (a,k1,b,k2)),l) = {(succ l)}
let l be Element of NAT ; ::_thesis: for k1, k2 being Integer holds NIC ((SubFrom (a,k1,b,k2)),l) = {(succ l)}
let k1, k2 be Integer; ::_thesis: NIC ((SubFrom (a,k1,b,k2)),l) = {(succ l)}
set i = SubFrom (a,k1,b,k2);
 for s being State of SCMPDS st IC s = l holds
(Exec ((SubFrom (a,k1,b,k2)),s)) . (IC ) = succ (IC s) by SCMPDS_2:50;
hence  NIC ((SubFrom (a,k1,b,k2)),l) = {(succ l)} by Th1; ::_thesis: verum
end;

theorem Th12: :: SCMPDS_9:12
for a, b being Int_position
for l being Element of NAT
for k1, k2 being Integer holds NIC ((MultBy (a,k1,b,k2)),l) = {(succ l)}
proof
let a, b be Int_position; ::_thesis: for l being Element of NAT
for k1, k2 being Integer holds NIC ((MultBy (a,k1,b,k2)),l) = {(succ l)}
let l be Element of NAT ; ::_thesis: for k1, k2 being Integer holds NIC ((MultBy (a,k1,b,k2)),l) = {(succ l)}
let k1, k2 be Integer; ::_thesis: NIC ((MultBy (a,k1,b,k2)),l) = {(succ l)}
set i = MultBy (a,k1,b,k2);
 for s being State of SCMPDS st IC s = l holds
(Exec ((MultBy (a,k1,b,k2)),s)) . (IC ) = succ (IC s) by SCMPDS_2:51;
hence  NIC ((MultBy (a,k1,b,k2)),l) = {(succ l)} by Th1; ::_thesis: verum
end;

theorem Th13: :: SCMPDS_9:13
for a, b being Int_position
for l being Element of NAT
for k1, k2 being Integer holds NIC ((Divide (a,k1,b,k2)),l) = {(succ l)}
proof
let a, b be Int_position; ::_thesis: for l being Element of NAT
for k1, k2 being Integer holds NIC ((Divide (a,k1,b,k2)),l) = {(succ l)}
let l be Element of NAT ; ::_thesis: for k1, k2 being Integer holds NIC ((Divide (a,k1,b,k2)),l) = {(succ l)}
let k1, k2 be Integer; ::_thesis: NIC ((Divide (a,k1,b,k2)),l) = {(succ l)}
set i = Divide (a,k1,b,k2);
 for s being State of SCMPDS st IC s = l holds
(Exec ((Divide (a,k1,b,k2)),s)) . (IC ) = succ (IC s) by SCMPDS_2:52;
hence  NIC ((Divide (a,k1,b,k2)),l) = {(succ l)} by Th1; ::_thesis: verum
end;

theorem :: SCMPDS_9:14
for a being Int_position
for l being Element of NAT
for k1, k2 being Integer holds NIC (((a,k1) <>0_goto k2),l) = {(succ l),(abs (k2 + l))}
proof
let a be Int_position; ::_thesis: for l being Element of NAT
for k1, k2 being Integer holds NIC (((a,k1) <>0_goto k2),l) = {(succ l),(abs (k2 + l))}
let l be Element of NAT ; ::_thesis: for k1, k2 being Integer holds NIC (((a,k1) <>0_goto k2),l) = {(succ l),(abs (k2 + l))}
let k1, k2 be Integer; ::_thesis: NIC (((a,k1) <>0_goto k2),l) = {(succ l),(abs (k2 + l))}
set s = the State of SCMPDS;
set i = (a,k1) <>0_goto k2;
set t = abs (k2 + l);
set I = (a,k1) <>0_goto k2;
reconsider n = l as Element of NAT ;
reconsider u = the n -started State of SCMPDS as Element of product (the_Values_of SCMPDS) by CARD_3:107;
hereby  :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: {(succ l),(abs (k2 + l))} c= NIC (((a,k1) <>0_goto k2),l)
let x be set ; ::_thesis: ( x in NIC (((a,k1) <>0_goto k2),l) implies b1 in {(succ l),(abs (k2 + l))} )
assume  x in NIC (((a,k1) <>0_goto k2),l) ; ::_thesis: b1 in {(succ l),(abs (k2 + l))}
then consider s being Element of product (the_Values_of SCMPDS) such that
A1: x = IC (Exec (((a,k1) <>0_goto k2),s)) and
A2: IC s = l ;
A3: ex m1 being Element of NAT st
( m1 = IC s & ICplusConst (s,k2) = abs (m1 + k2) ) by SCMPDS_2:def_18;
percases ( s . (DataLoc ((s . a),k1)) <> 0 or s . (DataLoc ((s . a),k1)) = 0 ) ;
supposeA4: s . (DataLoc ((s . a),k1)) <> 0 ; ::_thesis: b1 in {(succ l),(abs (k2 + l))}
 x = abs (k2 + l) by A1, A2, A3, A4, SCMPDS_2:55;
hence  x in {(succ l),(abs (k2 + l))} by TARSKI:def_2; ::_thesis: verum
end;
supposeA5: s . (DataLoc ((s . a),k1)) = 0 ; ::_thesis: b1 in {(succ l),(abs (k2 + l))}
 x = succ l by A1, A2, A5, SCMPDS_2:55;
hence  x in {(succ l),(abs (k2 + l))} by TARSKI:def_2; ::_thesis: verum
end;
end;
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {(succ l),(abs (k2 + l))} or x in NIC (((a,k1) <>0_goto k2),l) )
assume A6: x in {(succ l),(abs (k2 + l))} ; ::_thesis: x in NIC (((a,k1) <>0_goto k2),l)
percases ( x = succ l or x = abs (k2 + l) ) by A6, TARSKI:def_2;
supposeA7: x = succ l ; ::_thesis: x in NIC (((a,k1) <>0_goto k2),l)
reconsider u1 = u +* (a .--> 0) as State of SCMPDS ;
reconsider u2 = u1 +* ((DataLoc ((u1 . a),k1)) .--> 0) as Element of product (the_Values_of SCMPDS) by CARD_3:107;
A8: IC u2 = u1 . (IC ) by FUNCT_4:83, SCMPDS_2:43
.= IC u by FUNCT_4:83, SCMPDS_2:43
.= n by MEMSTR_0:def_11 ;
A9: u2 . (DataLoc ((u1 . a),k1)) = 0 by FUNCT_7:94;
 u2 . (DataLoc ((u2 . a),k1)) = 0
proof
percases ( a = DataLoc ((u1 . a),k1) or a <> DataLoc ((u1 . a),k1) ) ;
suppose a = DataLoc ((u1 . a),k1) ; ::_thesis: u2 . (DataLoc ((u2 . a),k1)) = 0
hence  u2 . (DataLoc ((u2 . a),k1)) = 0 by A9, FUNCT_7:94; ::_thesis: verum
end;
suppose a <> DataLoc ((u1 . a),k1) ; ::_thesis: u2 . (DataLoc ((u2 . a),k1)) = 0
then  u2 . a = u1 . a by FUNCT_4:83;
hence  u2 . (DataLoc ((u2 . a),k1)) = 0 by FUNCT_7:94; ::_thesis: verum
end;
end;
end;
then  x = IC (Exec (((a,k1) <>0_goto k2),u2)) by A7, A8, SCMPDS_2:55;
hence  x in NIC (((a,k1) <>0_goto k2),l) by A8; ::_thesis: verum
end;
supposeA10: x = abs (k2 + l) ; ::_thesis: x in NIC (((a,k1) <>0_goto k2),l)
reconsider u1 = u +* (a .--> 1) as State of SCMPDS ;
reconsider u2 = u1 +* ((DataLoc ((u1 . a),k1)) .--> 1) as Element of product (the_Values_of SCMPDS) by CARD_3:107;
A11: u2 . (DataLoc ((u1 . a),k1)) = 1 by FUNCT_7:94;
A12: u2 . (DataLoc ((u2 . a),k1)) <> 0
proof
percases ( a = DataLoc ((u1 . a),k1) or a <> DataLoc ((u1 . a),k1) ) ;
suppose a = DataLoc ((u1 . a),k1) ; ::_thesis: u2 . (DataLoc ((u2 . a),k1)) <> 0
hence  u2 . (DataLoc ((u2 . a),k1)) <> 0 by A11, FUNCT_7:94; ::_thesis: verum
end;
suppose a <> DataLoc ((u1 . a),k1) ; ::_thesis: u2 . (DataLoc ((u2 . a),k1)) <> 0
then  u2 . a = u1 . a by FUNCT_4:83;
hence  u2 . (DataLoc ((u2 . a),k1)) <> 0 by FUNCT_7:94; ::_thesis: verum
end;
end;
end;
A13: IC u2 = u1 . (IC ) by FUNCT_4:83, SCMPDS_2:43
.= IC u by FUNCT_4:83, SCMPDS_2:43
.= n by MEMSTR_0:def_11 ;
 ex m1 being Element of NAT st
( m1 = IC u2 & ICplusConst (u2,k2) = abs (m1 + k2) ) by SCMPDS_2:def_18;
then  x = IC (Exec (((a,k1) <>0_goto k2),u2)) by A10, A13, A12, SCMPDS_2:55;
hence  x in NIC (((a,k1) <>0_goto k2),l) by A13; ::_thesis: verum
end;
end;
end;

theorem :: SCMPDS_9:15
for a being Int_position
for l being Element of NAT
for k1, k2 being Integer holds NIC (((a,k1) <=0_goto k2),l) = {(succ l),(abs (k2 + l))}
proof
let a be Int_position; ::_thesis: for l being Element of NAT
for k1, k2 being Integer holds NIC (((a,k1) <=0_goto k2),l) = {(succ l),(abs (k2 + l))}
let l be Element of NAT ; ::_thesis: for k1, k2 being Integer holds NIC (((a,k1) <=0_goto k2),l) = {(succ l),(abs (k2 + l))}
let k1, k2 be Integer; ::_thesis: NIC (((a,k1) <=0_goto k2),l) = {(succ l),(abs (k2 + l))}
set s = the State of SCMPDS;
set i = (a,k1) <=0_goto k2;
set t = abs (k2 + l);
set I = (a,k1) <=0_goto k2;
reconsider n = l as Element of NAT ;
reconsider u = the n -started State of SCMPDS as Element of product (the_Values_of SCMPDS) by CARD_3:107;
hereby  :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: {(succ l),(abs (k2 + l))} c= NIC (((a,k1) <=0_goto k2),l)
let x be set ; ::_thesis: ( x in NIC (((a,k1) <=0_goto k2),l) implies b1 in {(succ l),(abs (k2 + l))} )
assume  x in NIC (((a,k1) <=0_goto k2),l) ; ::_thesis: b1 in {(succ l),(abs (k2 + l))}
then consider s being Element of product (the_Values_of SCMPDS) such that
A1: x = IC (Exec (((a,k1) <=0_goto k2),s)) and
A2: IC s = l ;
A3: ex m1 being Element of NAT st
( m1 = IC s & ICplusConst (s,k2) = abs (m1 + k2) ) by SCMPDS_2:def_18;
percases ( s . (DataLoc ((s . a),k1)) <= 0 or s . (DataLoc ((s . a),k1)) > 0 ) ;
supposeA4: s . (DataLoc ((s . a),k1)) <= 0 ; ::_thesis: b1 in {(succ l),(abs (k2 + l))}
 x = abs (k2 + l) by A1, A2, A3, A4, SCMPDS_2:56;
hence  x in {(succ l),(abs (k2 + l))} by TARSKI:def_2; ::_thesis: verum
end;
supposeA5: s . (DataLoc ((s . a),k1)) > 0 ; ::_thesis: b1 in {(succ l),(abs (k2 + l))}
 x = succ l by A1, A2, A5, SCMPDS_2:56;
hence  x in {(succ l),(abs (k2 + l))} by TARSKI:def_2; ::_thesis: verum
end;
end;
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {(succ l),(abs (k2 + l))} or x in NIC (((a,k1) <=0_goto k2),l) )
assume A6: x in {(succ l),(abs (k2 + l))} ; ::_thesis: x in NIC (((a,k1) <=0_goto k2),l)
percases ( x = succ l or x = abs (k2 + l) ) by A6, TARSKI:def_2;
supposeA7: x = succ l ; ::_thesis: x in NIC (((a,k1) <=0_goto k2),l)
reconsider u1 = u +* (a .--> 1) as State of SCMPDS ;
reconsider u2 = u1 +* ((DataLoc ((u1 . a),k1)) .--> 1) as Element of product (the_Values_of SCMPDS) by CARD_3:107;
A8: IC u2 = u1 . (IC ) by FUNCT_4:83, SCMPDS_2:43
.= IC u by FUNCT_4:83, SCMPDS_2:43
.= n by MEMSTR_0:def_11 ;
A9: u2 . (DataLoc ((u1 . a),k1)) = 1 by FUNCT_7:94;
 u2 . (DataLoc ((u2 . a),k1)) > 0
proof
percases ( a = DataLoc ((u1 . a),k1) or a <> DataLoc ((u1 . a),k1) ) ;
suppose a = DataLoc ((u1 . a),k1) ; ::_thesis: u2 . (DataLoc ((u2 . a),k1)) > 0
hence  u2 . (DataLoc ((u2 . a),k1)) > 0 by A9, FUNCT_7:94; ::_thesis: verum
end;
suppose a <> DataLoc ((u1 . a),k1) ; ::_thesis: u2 . (DataLoc ((u2 . a),k1)) > 0
then  u2 . a = u1 . a by FUNCT_4:83;
hence  u2 . (DataLoc ((u2 . a),k1)) > 0 by FUNCT_7:94; ::_thesis: verum
end;
end;
end;
then  x = IC (Exec (((a,k1) <=0_goto k2),u2)) by A7, A8, SCMPDS_2:56;
hence  x in NIC (((a,k1) <=0_goto k2),l) by A8; ::_thesis: verum
end;
supposeA10: x = abs (k2 + l) ; ::_thesis: x in NIC (((a,k1) <=0_goto k2),l)
reconsider u1 = u +* (a .--> 0) as State of SCMPDS ;
reconsider u2 = u1 +* ((DataLoc ((u1 . a),k1)) .--> 0) as Element of product (the_Values_of SCMPDS) by CARD_3:107;
A11: u2 . (DataLoc ((u1 . a),k1)) = 0 by FUNCT_7:94;
A12: u2 . (DataLoc ((u2 . a),k1)) <= 0
proof
percases ( a = DataLoc ((u1 . a),k1) or a <> DataLoc ((u1 . a),k1) ) ;
suppose a = DataLoc ((u1 . a),k1) ; ::_thesis: u2 . (DataLoc ((u2 . a),k1)) <= 0
hence  u2 . (DataLoc ((u2 . a),k1)) <= 0 by A11, FUNCT_7:94; ::_thesis: verum
end;
suppose a <> DataLoc ((u1 . a),k1) ; ::_thesis: u2 . (DataLoc ((u2 . a),k1)) <= 0
then  u2 . a = u1 . a by FUNCT_4:83;
hence  u2 . (DataLoc ((u2 . a),k1)) <= 0 by FUNCT_7:94; ::_thesis: verum
end;
end;
end;
A13: IC u2 = u1 . (IC ) by FUNCT_4:83, SCMPDS_2:43
.= IC u by FUNCT_4:83, SCMPDS_2:43
.= n by MEMSTR_0:def_11 ;
 ex m1 being Element of NAT st
( m1 = IC u2 & ICplusConst (u2,k2) = abs (m1 + k2) ) by SCMPDS_2:def_18;
then  x = IC (Exec (((a,k1) <=0_goto k2),u2)) by A10, A13, A12, SCMPDS_2:56;
hence  x in NIC (((a,k1) <=0_goto k2),l) by A13; ::_thesis: verum
end;
end;
end;

theorem :: SCMPDS_9:16
for a being Int_position
for l being Element of NAT
for k1, k2 being Integer holds NIC (((a,k1) >=0_goto k2),l) = {(succ l),(abs (k2 + l))}
proof
let a be Int_position; ::_thesis: for l being Element of NAT
for k1, k2 being Integer holds NIC (((a,k1) >=0_goto k2),l) = {(succ l),(abs (k2 + l))}
let l be Element of NAT ; ::_thesis: for k1, k2 being Integer holds NIC (((a,k1) >=0_goto k2),l) = {(succ l),(abs (k2 + l))}
let k1, k2 be Integer; ::_thesis: NIC (((a,k1) >=0_goto k2),l) = {(succ l),(abs (k2 + l))}
set s = the State of SCMPDS;
set i = (a,k1) >=0_goto k2;
set t = abs (k2 + l);
set I = (a,k1) >=0_goto k2;
reconsider n = l as Element of NAT ;
reconsider u = the n -started State of SCMPDS as Element of product (the_Values_of SCMPDS) by CARD_3:107;
hereby  :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: {(succ l),(abs (k2 + l))} c= NIC (((a,k1) >=0_goto k2),l)
let x be set ; ::_thesis: ( x in NIC (((a,k1) >=0_goto k2),l) implies b1 in {(succ l),(abs (k2 + l))} )
assume  x in NIC (((a,k1) >=0_goto k2),l) ; ::_thesis: b1 in {(succ l),(abs (k2 + l))}
then consider s being Element of product (the_Values_of SCMPDS) such that
A1: x = IC (Exec (((a,k1) >=0_goto k2),s)) and
A2: IC s = l ;
A3: ex m1 being Element of NAT st
( m1 = IC s & ICplusConst (s,k2) = abs (m1 + k2) ) by SCMPDS_2:def_18;
percases ( s . (DataLoc ((s . a),k1)) >= 0 or s . (DataLoc ((s . a),k1)) < 0 ) ;
supposeA4: s . (DataLoc ((s . a),k1)) >= 0 ; ::_thesis: b1 in {(succ l),(abs (k2 + l))}
 x = abs (k2 + l) by A1, A2, A3, A4, SCMPDS_2:57;
hence  x in {(succ l),(abs (k2 + l))} by TARSKI:def_2; ::_thesis: verum
end;
supposeA5: s . (DataLoc ((s . a),k1)) < 0 ; ::_thesis: b1 in {(succ l),(abs (k2 + l))}
 x = succ l by A1, A2, A5, SCMPDS_2:57;
hence  x in {(succ l),(abs (k2 + l))} by TARSKI:def_2; ::_thesis: verum
end;
end;
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {(succ l),(abs (k2 + l))} or x in NIC (((a,k1) >=0_goto k2),l) )
assume A6: x in {(succ l),(abs (k2 + l))} ; ::_thesis: x in NIC (((a,k1) >=0_goto k2),l)
percases ( x = succ l or x = abs (k2 + l) ) by A6, TARSKI:def_2;
supposeA7: x = succ l ; ::_thesis: x in NIC (((a,k1) >=0_goto k2),l)
A8: - 1 < 0 ;
reconsider u1 = u +* (a .--> (- 1)) as State of SCMPDS ;
reconsider u1 = u +* (a .--> (- 1)) as Element of product (the_Values_of SCMPDS) by CARD_3:107;
reconsider u2 = u1 +* ((DataLoc ((u1 . a),k1)) .--> (- 1)) as Element of product (the_Values_of SCMPDS) by CARD_3:107;
A9: IC u2 = u1 . (IC ) by FUNCT_4:83, SCMPDS_2:43
.= IC u by FUNCT_4:83, SCMPDS_2:43
.= n by MEMSTR_0:def_11 ;
A10: u2 . (DataLoc ((u1 . a),k1)) = - 1 by FUNCT_7:94;
 u2 . (DataLoc ((u2 . a),k1)) < 0
proof
percases ( a = DataLoc ((u1 . a),k1) or a <> DataLoc ((u1 . a),k1) ) ;
suppose a = DataLoc ((u1 . a),k1) ; ::_thesis: u2 . (DataLoc ((u2 . a),k1)) < 0
hence  u2 . (DataLoc ((u2 . a),k1)) < 0 by A10, A8, FUNCT_7:94; ::_thesis: verum
end;
suppose a <> DataLoc ((u1 . a),k1) ; ::_thesis: u2 . (DataLoc ((u2 . a),k1)) < 0
then  u2 . a = u1 . a by FUNCT_4:83;
hence  u2 . (DataLoc ((u2 . a),k1)) < 0 by A8, FUNCT_7:94; ::_thesis: verum
end;
end;
end;
then  x = IC (Exec (((a,k1) >=0_goto k2),u2)) by A7, A9, SCMPDS_2:57;
hence  x in NIC (((a,k1) >=0_goto k2),l) by A9; ::_thesis: verum
end;
supposeA11: x = abs (k2 + l) ; ::_thesis: x in NIC (((a,k1) >=0_goto k2),l)
reconsider u1 = u +* (a .--> (- 1)) as State of SCMPDS ;
reconsider u1 = u +* (a .--> 0) as Element of product (the_Values_of SCMPDS) by CARD_3:107;
reconsider u2 = u1 +* ((DataLoc ((u1 . a),k1)) .--> 0) as Element of product (the_Values_of SCMPDS) by CARD_3:107;
A12: u2 . (DataLoc ((u1 . a),k1)) = 0 by FUNCT_7:94;
A13: u2 . (DataLoc ((u2 . a),k1)) >= 0
proof
percases ( a = DataLoc ((u1 . a),k1) or a <> DataLoc ((u1 . a),k1) ) ;
suppose a = DataLoc ((u1 . a),k1) ; ::_thesis: u2 . (DataLoc ((u2 . a),k1)) >= 0
hence  u2 . (DataLoc ((u2 . a),k1)) >= 0 by A12, FUNCT_7:94; ::_thesis: verum
end;
suppose a <> DataLoc ((u1 . a),k1) ; ::_thesis: u2 . (DataLoc ((u2 . a),k1)) >= 0
then  u2 . a = u1 . a by FUNCT_4:83;
hence  u2 . (DataLoc ((u2 . a),k1)) >= 0 by FUNCT_7:94; ::_thesis: verum
end;
end;
end;
A14: IC u2 = u1 . (IC ) by FUNCT_4:83, SCMPDS_2:43
.= IC u by FUNCT_4:83, SCMPDS_2:43
.= n by MEMSTR_0:def_11 ;
 ex m1 being Element of NAT st
( m1 = IC u2 & ICplusConst (u2,k2) = abs (m1 + k2) ) by SCMPDS_2:def_18;
then  x = IC (Exec (((a,k1) >=0_goto k2),u2)) by A11, A14, A13, SCMPDS_2:57;
hence  x in NIC (((a,k1) >=0_goto k2),l) by A14; ::_thesis: verum
end;
end;
end;

theorem Th17: :: SCMPDS_9:17
for a being Int_position holds JUMP (return a) =  {  k where k is Element of NAT : k > 1  }
proof
let a be Int_position; ::_thesis: JUMP (return a) =  {  k where k is Element of NAT : k > 1  }
set A =  {  k where k is Element of NAT : k > 1  }  ;
set i = return a;
set X =  {  (NIC ((return a),l)) where l is Element of NAT : verum  }  ;
 JUMP (return a) c= NIC ((return a),0) by AMISTD_1:19;
hence  JUMP (return a) c=  {  k where k is Element of NAT : k > 1  }  by Th4; :: according to XBOOLE_0:def_10 ::_thesis:  {  k where k is Element of NAT : k > 1  }  c= JUMP (return a)
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  k where k is Element of NAT : k > 1  }  or x in JUMP (return a) )
assume A1: x in  {  k where k is Element of NAT : k > 1  }  ; ::_thesis: x in JUMP (return a)
now__::_thesis:_(__{__(NIC_((return_a),l))_where_l_is_Element_of_NAT_:_verum__}__<>_{}_&_(_for_y_being_set_st_y_in__{__(NIC_((return_a),l))_where_l_is_Element_of_NAT_:_verum__}__holds_
x_in_y_)_)
consider k being Element of NAT  such that
A2: x = k and
A3: k > 1 by A1;
reconsider k2 = k - 2 as Element of NAT by A3, Lm2;
 NIC ((return a),0) in  {  (NIC ((return a),l)) where l is Element of NAT : verum  }  ;
hence   {  (NIC ((return a),l)) where l is Element of NAT : verum  }  <> {} ; ::_thesis: for y being set st y in  {  (NIC ((return a),l)) where l is Element of NAT : verum  }  holds
x in y
 a in SCM-Data-Loc by AMI_2:def_16;
then consider j being Element of NAT  such that
A4: a = [1,j] by AMI_2:23;
set t = [1,(j + 1)];
set s = the State of SCMPDS;
let y be set ; ::_thesis: ( y in  {  (NIC ((return a),l)) where l is Element of NAT : verum  }  implies x in y )
A5: DataLoc (j,1) = [1,(abs (j + 1))]
.= [1,(j + 1)] by ABSVALUE:def_1 ;
 [1,(j + 1)] in SCM-Data-Loc by AMI_2:24;
then reconsider t1 = [1,(j + 1)] as Int_position by AMI_2:def_16;
assume  y in  {  (NIC ((return a),l)) where l is Element of NAT : verum  }  ; ::_thesis: x in y
then consider l being Element of NAT  such that
A6: y = NIC ((return a),l) ;
reconsider n = l as Element of NAT ;
set I = return a;
reconsider u = the n -started State of SCMPDS as Element of product (the_Values_of SCMPDS) by CARD_3:107;
A7: IC u = n by MEMSTR_0:def_11;
set g = (a,t1) --> (j,k2);
reconsider v = u +* ((a,t1) --> (j,k2)) as Element of product (the_Values_of SCMPDS) by CARD_3:107;
 j <> j + 1 ;
then A8: a <> t1 by A4, XTUPLE_0:1;
then A9: v . a = j by FUNCT_4:84;
A10: v . t1 = k2 by A8, FUNCT_4:84;
A11: dom ((a,t1) --> (j,k2)) = {a,t1} by FUNCT_4:62;
 ( a <> IC & t1 <> IC ) by SCMPDS_2:43;
then A12: not IC in dom ((a,t1) --> (j,k2)) by A11, TARSKI:def_2;
A13: IC v = l by A7, A12, FUNCT_4:11;
x = k2 + 2 by A2
.= (abs (v . (DataLoc (j,1)))) + 2 by A10, A5, ABSVALUE:def_1
.= IC (Exec ((return a),v)) by A9, SCMPDS_2:58, SCMPDS_I:def_14 ;
hence  x in y by A6, A13; ::_thesis: verum
end;
hence  x in JUMP (return a) by SETFAM_1:def_1; ::_thesis: verum
end;

registration
let a be Int_position;
cluster JUMP (return a) ->  infinite ;
coherence
 not JUMP (return a) is finite
proof
  {  k where k is Element of NAT : k > 1  }  is infinite by PRE_CIRC:23;
hence  not JUMP (return a) is finite by Th17; ::_thesis: verum
end;
end;

registration
let a be Int_position;
let k1 be Integer;
cluster JUMP (saveIC (a,k1)) ->  empty ;
coherence
 JUMP (saveIC (a,k1)) is empty
proof
 for l being Element of NAT holds NIC ((saveIC (a,k1)),l) = {(succ l)} by Th5;
hence  JUMP (saveIC (a,k1)) is empty by Th2; ::_thesis: verum
end;
end;

registration
let a be Int_position;
let k1 be Integer;
cluster JUMP (a := k1) ->  empty ;
coherence
 JUMP (a := k1) is empty
proof
 for l being Element of NAT holds NIC ((a := k1),l) = {(succ l)} by Th6;
hence  JUMP (a := k1) is empty by Th2; ::_thesis: verum
end;
end;

registration
let a be Int_position;
let k1, k2 be Integer;
cluster JUMP ((a,k1) := k2) ->  empty ;
coherence
 JUMP ((a,k1) := k2) is empty
proof
 for l being Element of NAT holds NIC (((a,k1) := k2),l) = {(succ l)} by Th7;
hence  JUMP ((a,k1) := k2) is empty by Th2; ::_thesis: verum
end;
end;

registration
let a, b be Int_position;
let k1, k2 be Integer;
cluster JUMP ((a,k1) := (b,k2)) ->  empty ;
coherence
 JUMP ((a,k1) := (b,k2)) is empty
proof
 for l being Element of NAT holds NIC (((a,k1) := (b,k2)),l) = {(succ l)} by Th8;
hence  JUMP ((a,k1) := (b,k2)) is empty by Th2; ::_thesis: verum
end;
end;

registration
let a be Int_position;
let k1, k2 be Integer;
cluster JUMP (AddTo (a,k1,k2)) ->  empty ;
coherence
 JUMP (AddTo (a,k1,k2)) is empty
proof
 for l being Element of NAT holds NIC ((AddTo (a,k1,k2)),l) = {(succ l)} by Th9;
hence  JUMP (AddTo (a,k1,k2)) is empty by Th2; ::_thesis: verum
end;
end;

registration
let a, b be Int_position;
let k1, k2 be Integer;
cluster JUMP (AddTo (a,k1,b,k2)) ->  empty ;
coherence
 JUMP (AddTo (a,k1,b,k2)) is empty
proof
 for l being Element of NAT holds NIC ((AddTo (a,k1,b,k2)),l) = {(succ l)} by Th10;
hence  JUMP (AddTo (a,k1,b,k2)) is empty by Th2; ::_thesis: verum
end;
cluster JUMP (SubFrom (a,k1,b,k2)) ->  empty ;
coherence
 JUMP (SubFrom (a,k1,b,k2)) is empty
proof
 for l being Element of NAT holds NIC ((SubFrom (a,k1,b,k2)),l) = {(succ l)} by Th11;
hence  JUMP (SubFrom (a,k1,b,k2)) is empty by Th2; ::_thesis: verum
end;
cluster JUMP (MultBy (a,k1,b,k2)) ->  empty ;
coherence
 JUMP (MultBy (a,k1,b,k2)) is empty
proof
 for l being Element of NAT holds NIC ((MultBy (a,k1,b,k2)),l) = {(succ l)} by Th12;
hence  JUMP (MultBy (a,k1,b,k2)) is empty by Th2; ::_thesis: verum
end;
cluster JUMP (Divide (a,k1,b,k2)) ->  empty ;
coherence
 JUMP (Divide (a,k1,b,k2)) is empty
proof
 for l being Element of NAT holds NIC ((Divide (a,k1,b,k2)),l) = {(succ l)} by Th13;
hence  JUMP (Divide (a,k1,b,k2)) is empty by Th2; ::_thesis: verum
end;
end;

Lm3:  not 5 / 3 is integer
proof
 not 3 divides 5
proof
assume  3 divides 5 ; ::_thesis: contradiction
then A1: 5 mod 3 = 0 by PEPIN:6;
 5 = (3 * 1) + 2 ;
hence  contradiction by A1, NAT_D:def_2; ::_thesis: verum
end;
hence  not 5 / 3 is integer by WSIERP_1:17; ::_thesis: verum
end;

Lm4:  for d being real number holds ((((abs d) + (((- d) + (abs d)) + 4)) + 2) - 2) + d <> - ((((((abs d) + (((- d) + (abs d)) + 4)) + (((- d) + (abs d)) + 4)) + 2) - 2) + d)
proof
let d be real number ; ::_thesis: ((((abs d) + (((- d) + (abs d)) + 4)) + 2) - 2) + d <> - ((((((abs d) + (((- d) + (abs d)) + 4)) + (((- d) + (abs d)) + 4)) + 2) - 2) + d)
set c = ((- d) + (abs d)) + 4;
set xx = ((((- d) + (abs d)) + 4) + (((- d) + (abs d)) + 4)) + (((- d) + (abs d)) + 4);
 (- d) + (abs d) >= 0 by ABSVALUE:27;
then  (- 2) * (((((- d) + (abs d)) + 4) + (((- d) + (abs d)) + 4)) + (((- d) + (abs d)) + 4)) < (- 2) * 0 by XREAL_1:69;
then A1: ((- 2) * (((((- d) + (abs d)) + 4) + (((- d) + (abs d)) + 4)) + (((- d) + (abs d)) + 4))) / 4 < 0 / 4 by XREAL_1:74;
assume  ((((abs d) + (((- d) + (abs d)) + 4)) + 2) - 2) + d = - ((((((abs d) + (((- d) + (abs d)) + 4)) + (((- d) + (abs d)) + 4)) + 2) - 2) + d) ; ::_thesis: contradiction
then  d + (abs d) = ((- 2) * (((((- d) + (abs d)) + 4) + (((- d) + (abs d)) + 4)) + (((- d) + (abs d)) + 4))) / 4 ;
hence  contradiction by A1, ABSVALUE:26; ::_thesis: verum
end;

Lm5:  for b, d being real number holds b + 1 <> b + ((((- d) + (abs d)) + 4) + d)
proof
let b, d be real number ; ::_thesis: b + 1 <> b + ((((- d) + (abs d)) + 4) + d)
set c = ((- d) + (abs d)) + 4;
 abs d >= 0 by COMPLEX1:46;
then A1: (abs d) + 3 >= 0 + 3 by XREAL_1:7;
assume  b + 1 = b + ((((- d) + (abs d)) + 4) + d) ; ::_thesis: contradiction
hence  contradiction by A1; ::_thesis: verum
end;

Lm6:  for c, d being real number st c > 0 holds
((abs d) + c) + 1 <> - ((((abs d) + c) + c) + d)
proof
let c, d be real number ; ::_thesis: ( c > 0 implies ((abs d) + c) + 1 <> - ((((abs d) + c) + c) + d) )
assume A1: c > 0 ; ::_thesis: ((abs d) + c) + 1 <> - ((((abs d) + c) + c) + d)
assume A2: ((abs d) + c) + 1 = - ((((abs d) + c) + c) + d) ; ::_thesis: contradiction
percases ( d >= 0 or d < 0 ) ;
supposeA3: d >= 0 ; ::_thesis: contradiction
then  abs d = d by ABSVALUE:def_1;
hence  contradiction by A1, A2, A3; ::_thesis: verum
end;
supposeA4: d < 0 ; ::_thesis: contradiction
then  abs d = - d by ABSVALUE:def_1;
then  ((- d) + (3 * c)) + 1 = 0 by A2;
hence  contradiction by A1, A4; ::_thesis: verum
end;
end;
end;

Lm7:  for b being real number
for d being Integer st d <> 5 holds
(b + (((- d) + (abs d)) + 4)) + 1 <> b + d
proof
let b be real number ; ::_thesis: for d being Integer st d <> 5 holds
(b + (((- d) + (abs d)) + 4)) + 1 <> b + d
let d be Integer; ::_thesis: ( d <> 5 implies (b + (((- d) + (abs d)) + 4)) + 1 <> b + d )
assume A1: d <> 5 ; ::_thesis: (b + (((- d) + (abs d)) + 4)) + 1 <> b + d
assume A2: (b + (((- d) + (abs d)) + 4)) + 1 = b + d ; ::_thesis: contradiction
percases ( d >= 0 or d < 0 ) ;
suppose d >= 0 ; ::_thesis: contradiction
then  abs d = d by ABSVALUE:def_1;
hence  contradiction by A1, A2; ::_thesis: verum
end;
suppose d < 0 ; ::_thesis: contradiction
then  abs d = - d by ABSVALUE:def_1;
hence  contradiction by A2, Lm3; ::_thesis: verum
end;
end;
end;

Lm8:  for c, d being real number st c > 0 holds
(((abs d) + c) + c) + 1 <> - (((abs d) + c) + d)
proof
let c, d be real number ; ::_thesis: ( c > 0 implies (((abs d) + c) + c) + 1 <> - (((abs d) + c) + d) )
assume A1: c > 0 ; ::_thesis: (((abs d) + c) + c) + 1 <> - (((abs d) + c) + d)
assume A2: (((abs d) + c) + c) + 1 = - (((abs d) + c) + d) ; ::_thesis: contradiction
percases ( d >= 0 or d < 0 ) ;
supposeA3: d >= 0 ; ::_thesis: contradiction
then  abs d = d by ABSVALUE:def_1;
hence  contradiction by A1, A2, A3; ::_thesis: verum
end;
supposeA4: d < 0 ; ::_thesis: contradiction
then  abs d = - d by ABSVALUE:def_1;
hence  contradiction by A1, A2, A4; ::_thesis: verum
end;
end;
end;

Lm9:  for a being Int_position
for k1 being Integer holds JUMP ((a,k1) <>0_goto 5) = {}
proof
let a be Int_position; ::_thesis: for k1 being Integer holds JUMP ((a,k1) <>0_goto 5) = {}
let k1 be Integer; ::_thesis: JUMP ((a,k1) <>0_goto 5) = {}
set k2 = 5;
set i = (a,k1) <>0_goto 5;
set X =  {  (NIC (((a,k1) <>0_goto 5),l)) where l is Element of NAT : verum  }  ;
hereby  :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: {} c= JUMP ((a,k1) <>0_goto 5)
set nl2 = 8;
set nl1 = 5;
let x be set ; ::_thesis: ( x in JUMP ((a,k1) <>0_goto 5) implies b1 in {} )
assume A1: x in JUMP ((a,k1) <>0_goto 5) ; ::_thesis: b1 in {}
set l2 = 8;
 NIC (((a,k1) <>0_goto 5),8) in  {  (NIC (((a,k1) <>0_goto 5),l)) where l is Element of NAT : verum  }  ;
then  x in NIC (((a,k1) <>0_goto 5),8) by A1, SETFAM_1:def_1;
then consider s2 being Element of product (the_Values_of SCMPDS) such that
A2: x = IC (Exec (((a,k1) <>0_goto 5),s2)) and
A3: IC s2 = 8 ;
set l1 = 5;
 NIC (((a,k1) <>0_goto 5),5) in  {  (NIC (((a,k1) <>0_goto 5),l)) where l is Element of NAT : verum  }  ;
then  x in NIC (((a,k1) <>0_goto 5),5) by A1, SETFAM_1:def_1;
then consider s1 being Element of product (the_Values_of SCMPDS) such that
A4: x = IC (Exec (((a,k1) <>0_goto 5),s1)) and
A5: IC s1 = 5 ;
consider m2 being Element of NAT  such that
A6: m2 = IC s2 and
A7: ICplusConst (s2,5) = abs (m2 + 5) by SCMPDS_2:def_18;
consider m1 being Element of NAT  such that
A8: m1 = IC s1 and
A9: ICplusConst (s1,5) = abs (m1 + 5) by SCMPDS_2:def_18;
percases ( ( s1 . (DataLoc ((s1 . a),k1)) <> 0 & s2 . (DataLoc ((s2 . a),k1)) <> 0 ) or ( s1 . (DataLoc ((s1 . a),k1)) = 0 & s2 . (DataLoc ((s2 . a),k1)) = 0 ) or ( s1 . (DataLoc ((s1 . a),k1)) = 0 & s2 . (DataLoc ((s2 . a),k1)) <> 0 ) or ( s1 . (DataLoc ((s1 . a),k1)) <> 0 & s2 . (DataLoc ((s2 . a),k1)) = 0 ) ) ;
supposethat A10: s1 . (DataLoc ((s1 . a),k1)) <> 0 and
A11: s2 . (DataLoc ((s2 . a),k1)) <> 0 ; ::_thesis: b1 in {}
A12: x = abs (m2 + 5) by A2, A7, A11, SCMPDS_2:55;
 x = abs (m1 + 5) by A4, A9, A10, SCMPDS_2:55;
then  ( 5 + 5 = 8 + 5 or 5 + 5 = - (8 + 5) ) by A5, A8, A3, A6, A12, ABSVALUE:28;
hence  x in {} ; ::_thesis: verum
end;
supposethat A13: s1 . (DataLoc ((s1 . a),k1)) = 0 and
A14: s2 . (DataLoc ((s2 . a),k1)) = 0 ; ::_thesis: b1 in {}
A15: x = succ 8 by A2, A3, A14, SCMPDS_2:55;
 x = succ 5 by A4, A5, A13, SCMPDS_2:55;
hence  x in {} by A15; ::_thesis: verum
end;
supposethat A16: s1 . (DataLoc ((s1 . a),k1)) = 0 and
A17: s2 . (DataLoc ((s2 . a),k1)) <> 0 ; ::_thesis: b1 in {}
reconsider n1 = 5 as Element of NAT ;
set w1 = n1;
A18: x = abs (m2 + 5) by A2, A7, A17, SCMPDS_2:55;
x = succ n1 by A4, A5, A16, SCMPDS_2:55
.= n1 + 1 ;
then  ( n1 + 1 = m2 + 5 or n1 + 1 = - (m2 + 5) ) by A18, ABSVALUE:1;
hence  x in {} by A3, A6; ::_thesis: verum
end;
supposethat A19: s1 . (DataLoc ((s1 . a),k1)) <> 0 and
A20: s2 . (DataLoc ((s2 . a),k1)) = 0 ; ::_thesis: b1 in {}
reconsider n2 = 8 as Element of NAT ;
A21: x = succ n2 by A2, A3, A20, SCMPDS_2:55
.= n2 + 1 ;
set w2 = n2;
 x = abs (m1 + 5) by A4, A9, A19, SCMPDS_2:55;
then  ( n2 + 1 = m1 + 5 or n2 + 1 = - (m1 + 5) ) by A21, ABSVALUE:1;
hence  x in {} by A5, A8; ::_thesis: verum
end;
end;
end;
thus  {} c= JUMP ((a,k1) <>0_goto 5) by XBOOLE_1:2; ::_thesis: verum
end;

Lm10:  for a being Int_position
for k2, k1 being Integer st k2 <> 5 holds
JUMP ((a,k1) <>0_goto k2) = {}
proof
let a be Int_position; ::_thesis: for k2, k1 being Integer st k2 <> 5 holds
JUMP ((a,k1) <>0_goto k2) = {}
let k2, k1 be Integer; ::_thesis: ( k2 <> 5 implies JUMP ((a,k1) <>0_goto k2) = {} )
set i = (a,k1) <>0_goto k2;
set X =  {  (NIC (((a,k1) <>0_goto k2),l)) where l is Element of NAT : verum  }  ;
assume A1: k2 <> 5 ; ::_thesis: JUMP ((a,k1) <>0_goto k2) = {}
hereby  :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: {} c= JUMP ((a,k1) <>0_goto k2)
set x1 = ((- k2) + (abs k2)) + 4;
let x be set ; ::_thesis: ( x in JUMP ((a,k1) <>0_goto k2) implies b1 in {} )
assume A2: x in JUMP ((a,k1) <>0_goto k2) ; ::_thesis: b1 in {}
A3: ((- k2) + (abs k2)) + 4 > ((- k2) + (abs k2)) + 0 by XREAL_1:6;
then A4: ((- k2) + (abs k2)) + 4 > 0 by ABSVALUE:27;
then reconsider x1 = ((- k2) + (abs k2)) + 4 as Element of NAT by INT_1:3;
set nl1 = (abs k2) + x1;
set nl2 = ((abs k2) + x1) + x1;
set l1 = (abs k2) + x1;
set l2 = ((abs k2) + x1) + x1;
 NIC (((a,k1) <>0_goto k2),((abs k2) + x1)) in  {  (NIC (((a,k1) <>0_goto k2),l)) where l is Element of NAT : verum  }  ;
then  x in NIC (((a,k1) <>0_goto k2),((abs k2) + x1)) by A2, SETFAM_1:def_1;
then consider s1 being Element of product (the_Values_of SCMPDS) such that
A5: x = IC (Exec (((a,k1) <>0_goto k2),s1)) and
A6: IC s1 = (abs k2) + x1 ;
consider m1 being Element of NAT  such that
A7: m1 = IC s1 and
A8: ICplusConst (s1,k2) = abs (m1 + k2) by SCMPDS_2:def_18;
 NIC (((a,k1) <>0_goto k2),(((abs k2) + x1) + x1)) in  {  (NIC (((a,k1) <>0_goto k2),l)) where l is Element of NAT : verum  }  ;
then  x in NIC (((a,k1) <>0_goto k2),(((abs k2) + x1) + x1)) by A2, SETFAM_1:def_1;
then consider s2 being Element of product (the_Values_of SCMPDS) such that
A9: x = IC (Exec (((a,k1) <>0_goto k2),s2)) and
A10: IC s2 = ((abs k2) + x1) + x1 ;
consider m2 being Element of NAT  such that
A11: m2 = IC s2 and
A12: ICplusConst (s2,k2) = abs (m2 + k2) by SCMPDS_2:def_18;
percases ( ( s1 . (DataLoc ((s1 . a),k1)) <> 0 & s2 . (DataLoc ((s2 . a),k1)) <> 0 ) or ( s1 . (DataLoc ((s1 . a),k1)) = 0 & s2 . (DataLoc ((s2 . a),k1)) = 0 ) or ( s1 . (DataLoc ((s1 . a),k1)) = 0 & s2 . (DataLoc ((s2 . a),k1)) <> 0 ) or ( s1 . (DataLoc ((s1 . a),k1)) <> 0 & s2 . (DataLoc ((s2 . a),k1)) = 0 ) ) ;
supposethat A13: s1 . (DataLoc ((s1 . a),k1)) <> 0 and
A14: s2 . (DataLoc ((s2 . a),k1)) <> 0 ; ::_thesis: b1 in {}
A15: x = abs (m2 + k2) by A9, A12, A14, SCMPDS_2:55;
A16: x = abs (m1 + k2) by A5, A8, A13, SCMPDS_2:55;
thus  x in {} ::_thesis: verum
proof
percases ( ((((abs k2) + x1) + 2) - 2) + k2 = (((((abs k2) + x1) + x1) + 2) - 2) + k2 or ((((abs k2) + x1) + 2) - 2) + k2 = - ((((((abs k2) + x1) + x1) + 2) - 2) + k2) ) by A6, A7, A10, A11, A16, A15, ABSVALUE:28;
suppose ((((abs k2) + x1) + 2) - 2) + k2 = (((((abs k2) + x1) + x1) + 2) - 2) + k2 ; ::_thesis: x in {}
hence  x in {} by A3, ABSVALUE:27; ::_thesis: verum
end;
suppose ((((abs k2) + x1) + 2) - 2) + k2 = - ((((((abs k2) + x1) + x1) + 2) - 2) + k2) ; ::_thesis: x in {}
hence  x in {} by Lm4; ::_thesis: verum
end;
end;
end;
end;
supposethat A17: s1 . (DataLoc ((s1 . a),k1)) = 0 and
A18: s2 . (DataLoc ((s2 . a),k1)) = 0 ; ::_thesis: b1 in {}
A19: x = succ (((abs k2) + x1) + x1) by A9, A10, A18, SCMPDS_2:55;
 x = succ ((abs k2) + x1) by A5, A6, A17, SCMPDS_2:55;
hence  x in {} by A3, A19, ABSVALUE:27; ::_thesis: verum
end;
supposethat A20: s1 . (DataLoc ((s1 . a),k1)) = 0 and
A21: s2 . (DataLoc ((s2 . a),k1)) <> 0 ; ::_thesis: b1 in {}
reconsider n1 = (abs k2) + x1 as Element of NAT ;
set w1 = n1;
A22: x = abs (m2 + k2) by A9, A12, A21, SCMPDS_2:55;
A23: x = succ n1 by A5, A6, A20, SCMPDS_2:55
.= n1 + 1 ;
thus  x in {} ::_thesis: verum
proof
percases ( n1 + 1 = m2 + k2 or n1 + 1 = - (m2 + k2) ) by A23, A22, ABSVALUE:1;
suppose n1 + 1 = m2 + k2 ; ::_thesis: x in {}
then  ((abs k2) + x1) + 1 = ((abs k2) + x1) + (x1 + k2) by A10, A11;
hence  x in {} by Lm5; ::_thesis: verum
end;
suppose n1 + 1 = - (m2 + k2) ; ::_thesis: x in {}
hence  x in {} by A4, A10, A11, Lm6; ::_thesis: verum
end;
end;
end;
end;
supposethat A24: s1 . (DataLoc ((s1 . a),k1)) <> 0 and
A25: s2 . (DataLoc ((s2 . a),k1)) = 0 ; ::_thesis: b1 in {}
reconsider n2 = ((abs k2) + x1) + x1 as Element of NAT ;
A26: x = succ n2 by A9, A10, A25, SCMPDS_2:55
.= n2 + 1 ;
set w2 = n2;
A27: x = abs (m1 + k2) by A5, A8, A24, SCMPDS_2:55;
thus  x in {} ::_thesis: verum
proof
percases ( n2 + 1 = m1 + k2 or n2 + 1 = - (m1 + k2) ) by A27, A26, ABSVALUE:1;
suppose n2 + 1 = m1 + k2 ; ::_thesis: x in {}
hence  x in {} by A1, A6, A7, Lm7; ::_thesis: verum
end;
suppose n2 + 1 = - (m1 + k2) ; ::_thesis: x in {}
hence  x in {} by A4, A6, A7, Lm8; ::_thesis: verum
end;
end;
end;
end;
end;
end;
thus  {} c= JUMP ((a,k1) <>0_goto k2) by XBOOLE_1:2; ::_thesis: verum
end;

Lm11:  for a being Int_position
for k1 being Integer holds JUMP ((a,k1) <=0_goto 5) = {}
proof
let a be Int_position; ::_thesis: for k1 being Integer holds JUMP ((a,k1) <=0_goto 5) = {}
let k1 be Integer; ::_thesis: JUMP ((a,k1) <=0_goto 5) = {}
set k2 = 5;
set i = (a,k1) <=0_goto 5;
set X =  {  (NIC (((a,k1) <=0_goto 5),l)) where l is Element of NAT : verum  }  ;
hereby  :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: {} c= JUMP ((a,k1) <=0_goto 5)
set nl2 = 8;
set nl1 = 5;
let x be set ; ::_thesis: ( x in JUMP ((a,k1) <=0_goto 5) implies b1 in {} )
assume A1: x in JUMP ((a,k1) <=0_goto 5) ; ::_thesis: b1 in {}
set l2 = 8;
 NIC (((a,k1) <=0_goto 5),8) in  {  (NIC (((a,k1) <=0_goto 5),l)) where l is Element of NAT : verum  }  ;
then  x in NIC (((a,k1) <=0_goto 5),8) by A1, SETFAM_1:def_1;
then consider s2 being Element of product (the_Values_of SCMPDS) such that
A2: x = IC (Exec (((a,k1) <=0_goto 5),s2)) and
A3: IC s2 = 8 ;
set l1 = 5;
 NIC (((a,k1) <=0_goto 5),5) in  {  (NIC (((a,k1) <=0_goto 5),l)) where l is Element of NAT : verum  }  ;
then  x in NIC (((a,k1) <=0_goto 5),5) by A1, SETFAM_1:def_1;
then consider s1 being Element of product (the_Values_of SCMPDS) such that
A4: x = IC (Exec (((a,k1) <=0_goto 5),s1)) and
A5: IC s1 = 5 ;
consider m2 being Element of NAT  such that
A6: m2 = IC s2 and
A7: ICplusConst (s2,5) = abs (m2 + 5) by SCMPDS_2:def_18;
consider m1 being Element of NAT  such that
A8: m1 = IC s1 and
A9: ICplusConst (s1,5) = abs (m1 + 5) by SCMPDS_2:def_18;
percases ( ( s1 . (DataLoc ((s1 . a),k1)) <= 0 & s2 . (DataLoc ((s2 . a),k1)) <= 0 ) or ( s1 . (DataLoc ((s1 . a),k1)) > 0 & s2 . (DataLoc ((s2 . a),k1)) > 0 ) or ( s1 . (DataLoc ((s1 . a),k1)) > 0 & s2 . (DataLoc ((s2 . a),k1)) <= 0 ) or ( s1 . (DataLoc ((s1 . a),k1)) <= 0 & s2 . (DataLoc ((s2 . a),k1)) > 0 ) ) ;
supposethat A10: s1 . (DataLoc ((s1 . a),k1)) <= 0 and
A11: s2 . (DataLoc ((s2 . a),k1)) <= 0 ; ::_thesis: b1 in {}
A12: x = abs (m2 + 5) by A2, A7, A11, SCMPDS_2:56;
 x = abs (m1 + 5) by A4, A9, A10, SCMPDS_2:56;
then  ( 5 + 5 = 8 + 5 or 5 + 5 = - (8 + 5) ) by A5, A8, A3, A6, A12, ABSVALUE:28;
hence  x in {} ; ::_thesis: verum
end;
supposethat A13: s1 . (DataLoc ((s1 . a),k1)) > 0 and
A14: s2 . (DataLoc ((s2 . a),k1)) > 0 ; ::_thesis: b1 in {}
A15: x = succ 8 by A2, A3, A14, SCMPDS_2:56;
 x = succ 5 by A4, A5, A13, SCMPDS_2:56;
hence  x in {} by A15; ::_thesis: verum
end;
supposethat A16: s1 . (DataLoc ((s1 . a),k1)) > 0 and
A17: s2 . (DataLoc ((s2 . a),k1)) <= 0 ; ::_thesis: b1 in {}
reconsider n1 = 5 as Element of NAT ;
set w1 = n1;
A18: x = abs (m2 + 5) by A2, A7, A17, SCMPDS_2:56;
x = succ n1 by A4, A5, A16, SCMPDS_2:56
.= n1 + 1 ;
then  ( n1 + 1 = m2 + 5 or n1 + 1 = - (m2 + 5) ) by A18, ABSVALUE:1;
hence  x in {} by A3, A6; ::_thesis: verum
end;
supposethat A19: s1 . (DataLoc ((s1 . a),k1)) <= 0 and
A20: s2 . (DataLoc ((s2 . a),k1)) > 0 ; ::_thesis: b1 in {}
reconsider n2 = 8 as Element of NAT ;
A21: x = succ n2 by A2, A3, A20, SCMPDS_2:56
.= n2 + 1 ;
set w2 = n2;
 x = abs (m1 + 5) by A4, A9, A19, SCMPDS_2:56;
then  ( n2 + 1 = m1 + 5 or n2 + 1 = - (m1 + 5) ) by A21, ABSVALUE:1;
hence  x in {} by A5, A8; ::_thesis: verum
end;
end;
end;
thus  {} c= JUMP ((a,k1) <=0_goto 5) by XBOOLE_1:2; ::_thesis: verum
end;

Lm12:  for a being Int_position
for k2, k1 being Integer st k2 <> 5 holds
JUMP ((a,k1) <=0_goto k2) = {}
proof
let a be Int_position; ::_thesis: for k2, k1 being Integer st k2 <> 5 holds
JUMP ((a,k1) <=0_goto k2) = {}
let k2, k1 be Integer; ::_thesis: ( k2 <> 5 implies JUMP ((a,k1) <=0_goto k2) = {} )
set i = (a,k1) <=0_goto k2;
set X =  {  (NIC (((a,k1) <=0_goto k2),l)) where l is Element of NAT : verum  }  ;
assume A1: k2 <> 5 ; ::_thesis: JUMP ((a,k1) <=0_goto k2) = {}
hereby  :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: {} c= JUMP ((a,k1) <=0_goto k2)
set x1 = ((- k2) + (abs k2)) + 4;
let x be set ; ::_thesis: ( x in JUMP ((a,k1) <=0_goto k2) implies b1 in {} )
assume A2: x in JUMP ((a,k1) <=0_goto k2) ; ::_thesis: b1 in {}
A3: ((- k2) + (abs k2)) + 4 > ((- k2) + (abs k2)) + 0 by XREAL_1:6;
then A4: ((- k2) + (abs k2)) + 4 > 0 by ABSVALUE:27;
then reconsider x1 = ((- k2) + (abs k2)) + 4 as Element of NAT by INT_1:3;
set nl1 = (abs k2) + x1;
set nl2 = ((abs k2) + x1) + x1;
set l1 = (abs k2) + x1;
set l2 = ((abs k2) + x1) + x1;
 NIC (((a,k1) <=0_goto k2),((abs k2) + x1)) in  {  (NIC (((a,k1) <=0_goto k2),l)) where l is Element of NAT : verum  }  ;
then  x in NIC (((a,k1) <=0_goto k2),((abs k2) + x1)) by A2, SETFAM_1:def_1;
then consider s1 being Element of product (the_Values_of SCMPDS) such that
A5: x = IC (Exec (((a,k1) <=0_goto k2),s1)) and
A6: IC s1 = (abs k2) + x1 ;
consider m1 being Element of NAT  such that
A7: m1 = IC s1 and
A8: ICplusConst (s1,k2) = abs (m1 + k2) by SCMPDS_2:def_18;
 NIC (((a,k1) <=0_goto k2),(((abs k2) + x1) + x1)) in  {  (NIC (((a,k1) <=0_goto k2),l)) where l is Element of NAT : verum  }  ;
then  x in NIC (((a,k1) <=0_goto k2),(((abs k2) + x1) + x1)) by A2, SETFAM_1:def_1;
then consider s2 being Element of product (the_Values_of SCMPDS) such that
A9: x = IC (Exec (((a,k1) <=0_goto k2),s2)) and
A10: IC s2 = ((abs k2) + x1) + x1 ;
consider m2 being Element of NAT  such that
A11: m2 = IC s2 and
A12: ICplusConst (s2,k2) = abs (m2 + k2) by SCMPDS_2:def_18;
percases ( ( s1 . (DataLoc ((s1 . a),k1)) <= 0 & s2 . (DataLoc ((s2 . a),k1)) <= 0 ) or ( s1 . (DataLoc ((s1 . a),k1)) > 0 & s2 . (DataLoc ((s2 . a),k1)) > 0 ) or ( s1 . (DataLoc ((s1 . a),k1)) > 0 & s2 . (DataLoc ((s2 . a),k1)) <= 0 ) or ( s1 . (DataLoc ((s1 . a),k1)) <= 0 & s2 . (DataLoc ((s2 . a),k1)) > 0 ) ) ;
supposethat A13: s1 . (DataLoc ((s1 . a),k1)) <= 0 and
A14: s2 . (DataLoc ((s2 . a),k1)) <= 0 ; ::_thesis: b1 in {}
A15: x = abs (m2 + k2) by A9, A12, A14, SCMPDS_2:56;
A16: x = abs (m1 + k2) by A5, A8, A13, SCMPDS_2:56;
thus  x in {} ::_thesis: verum
proof
percases ( ((abs k2) + x1) + k2 = (((abs k2) + x1) + x1) + k2 or ((((abs k2) + x1) + 2) - 2) + k2 = - ((((((abs k2) + x1) + x1) + 2) - 2) + k2) ) by A6, A7, A10, A11, A16, A15, ABSVALUE:28;
suppose ((abs k2) + x1) + k2 = (((abs k2) + x1) + x1) + k2 ; ::_thesis: x in {}
hence  x in {} by A3, ABSVALUE:27; ::_thesis: verum
end;
suppose ((((abs k2) + x1) + 2) - 2) + k2 = - ((((((abs k2) + x1) + x1) + 2) - 2) + k2) ; ::_thesis: x in {}
hence  x in {} by Lm4; ::_thesis: verum
end;
end;
end;
end;
supposethat A17: s1 . (DataLoc ((s1 . a),k1)) > 0 and
A18: s2 . (DataLoc ((s2 . a),k1)) > 0 ; ::_thesis: b1 in {}
A19: x = succ (((abs k2) + x1) + x1) by A9, A10, A18, SCMPDS_2:56;
 x = succ ((abs k2) + x1) by A5, A6, A17, SCMPDS_2:56;
hence  x in {} by A3, A19, ABSVALUE:27; ::_thesis: verum
end;
supposethat A20: s1 . (DataLoc ((s1 . a),k1)) > 0 and
A21: s2 . (DataLoc ((s2 . a),k1)) <= 0 ; ::_thesis: b1 in {}
reconsider n1 = (abs k2) + x1 as Element of NAT ;
set w1 = n1;
A22: x = abs (m2 + k2) by A9, A12, A21, SCMPDS_2:56;
A23: x = succ n1 by A5, A6, A20, SCMPDS_2:56
.= n1 + 1 ;
thus  x in {} ::_thesis: verum
proof
percases ( n1 + 1 = m2 + k2 or n1 + 1 = - (m2 + k2) ) by A23, A22, ABSVALUE:1;
suppose n1 + 1 = m2 + k2 ; ::_thesis: x in {}
then  ((abs k2) + x1) + 1 = ((abs k2) + x1) + (x1 + k2) by A10, A11;
hence  x in {} by Lm5; ::_thesis: verum
end;
suppose n1 + 1 = - (m2 + k2) ; ::_thesis: x in {}
hence  x in {} by A4, A10, A11, Lm6; ::_thesis: verum
end;
end;
end;
end;
supposethat A24: s1 . (DataLoc ((s1 . a),k1)) <= 0 and
A25: s2 . (DataLoc ((s2 . a),k1)) > 0 ; ::_thesis: b1 in {}
reconsider n2 = ((abs k2) + x1) + x1 as Element of NAT ;
A26: x = succ n2 by A9, A10, A25, SCMPDS_2:56
.= n2 + 1 ;
set w2 = n2;
A27: x = abs (m1 + k2) by A5, A8, A24, SCMPDS_2:56;
thus  x in {} ::_thesis: verum
proof
percases ( n2 + 1 = m1 + k2 or n2 + 1 = - (m1 + k2) ) by A27, A26, ABSVALUE:1;
suppose n2 + 1 = m1 + k2 ; ::_thesis: x in {}
hence  x in {} by A1, A6, A7, Lm7; ::_thesis: verum
end;
suppose n2 + 1 = - (m1 + k2) ; ::_thesis: x in {}
hence  x in {} by A4, A6, A7, Lm8; ::_thesis: verum
end;
end;
end;
end;
end;
end;
thus  {} c= JUMP ((a,k1) <=0_goto k2) by XBOOLE_1:2; ::_thesis: verum
end;

Lm13:  for a being Int_position
for k1 being Integer holds JUMP ((a,k1) >=0_goto 5) = {}
proof
let a be Int_position; ::_thesis: for k1 being Integer holds JUMP ((a,k1) >=0_goto 5) = {}
let k1 be Integer; ::_thesis: JUMP ((a,k1) >=0_goto 5) = {}
set k2 = 5;
set i = (a,k1) >=0_goto 5;
set X =  {  (NIC (((a,k1) >=0_goto 5),l)) where l is Element of NAT : verum  }  ;
hereby  :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: {} c= JUMP ((a,k1) >=0_goto 5)
set nl2 = 8;
set nl1 = 5;
let x be set ; ::_thesis: ( x in JUMP ((a,k1) >=0_goto 5) implies b1 in {} )
assume A1: x in JUMP ((a,k1) >=0_goto 5) ; ::_thesis: b1 in {}
set l2 = 8;
 NIC (((a,k1) >=0_goto 5),8) in  {  (NIC (((a,k1) >=0_goto 5),l)) where l is Element of NAT : verum  }  ;
then  x in NIC (((a,k1) >=0_goto 5),8) by A1, SETFAM_1:def_1;
then consider s2 being Element of product (the_Values_of SCMPDS) such that
A2: x = IC (Exec (((a,k1) >=0_goto 5),s2)) and
A3: IC s2 = 8 ;
set l1 = 5;
 NIC (((a,k1) >=0_goto 5),5) in  {  (NIC (((a,k1) >=0_goto 5),l)) where l is Element of NAT : verum  }  ;
then  x in NIC (((a,k1) >=0_goto 5),5) by A1, SETFAM_1:def_1;
then consider s1 being Element of product (the_Values_of SCMPDS) such that
A4: x = IC (Exec (((a,k1) >=0_goto 5),s1)) and
A5: IC s1 = 5 ;
consider m2 being Element of NAT  such that
A6: m2 = IC s2 and
A7: ICplusConst (s2,5) = abs (m2 + 5) by SCMPDS_2:def_18;
consider m1 being Element of NAT  such that
A8: m1 = IC s1 and
A9: ICplusConst (s1,5) = abs (m1 + 5) by SCMPDS_2:def_18;
percases ( ( s1 . (DataLoc ((s1 . a),k1)) >= 0 & s2 . (DataLoc ((s2 . a),k1)) >= 0 ) or ( s1 . (DataLoc ((s1 . a),k1)) < 0 & s2 . (DataLoc ((s2 . a),k1)) < 0 ) or ( s1 . (DataLoc ((s1 . a),k1)) < 0 & s2 . (DataLoc ((s2 . a),k1)) >= 0 ) or ( s1 . (DataLoc ((s1 . a),k1)) >= 0 & s2 . (DataLoc ((s2 . a),k1)) < 0 ) ) ;
supposethat A10: s1 . (DataLoc ((s1 . a),k1)) >= 0 and
A11: s2 . (DataLoc ((s2 . a),k1)) >= 0 ; ::_thesis: b1 in {}
A12: x = abs (m2 + 5) by A2, A7, A11, SCMPDS_2:57;
 x = abs (m1 + 5) by A4, A9, A10, SCMPDS_2:57;
then  ( ((5 + 2) - 2) + 5 = ((8 + 2) - 2) + 5 or ((5 + 2) - 2) + 5 = - (((8 + 2) - 2) + 5) ) by A5, A8, A3, A6, A12, ABSVALUE:28;
hence  x in {} ; ::_thesis: verum
end;
supposethat A13: s1 . (DataLoc ((s1 . a),k1)) < 0 and
A14: s2 . (DataLoc ((s2 . a),k1)) < 0 ; ::_thesis: b1 in {}
A15: x = succ 8 by A2, A3, A14, SCMPDS_2:57;
 x = succ 5 by A4, A5, A13, SCMPDS_2:57;
hence  x in {} by A15; ::_thesis: verum
end;
supposethat A16: s1 . (DataLoc ((s1 . a),k1)) < 0 and
A17: s2 . (DataLoc ((s2 . a),k1)) >= 0 ; ::_thesis: b1 in {}
reconsider n1 = 5 as Element of NAT ;
set w1 = n1;
A18: x = abs (m2 + 5) by A2, A7, A17, SCMPDS_2:57;
x = succ n1 by A4, A5, A16, SCMPDS_2:57
.= n1 + 1 ;
then  ( n1 + 1 = m2 + 5 or n1 + 1 = - (m2 + 5) ) by A18, ABSVALUE:1;
hence  x in {} by A3, A6; ::_thesis: verum
end;
supposethat A19: s1 . (DataLoc ((s1 . a),k1)) >= 0 and
A20: s2 . (DataLoc ((s2 . a),k1)) < 0 ; ::_thesis: b1 in {}
reconsider n2 = 8 as Element of NAT ;
A21: x = succ n2 by A2, A3, A20, SCMPDS_2:57
.= n2 + 1 ;
set w2 = n2;
 x = abs (m1 + 5) by A4, A9, A19, SCMPDS_2:57;
then  ( n2 + 1 = m1 + 5 or n2 + 1 = - (m1 + 5) ) by A21, ABSVALUE:1;
hence  x in {} by A5, A8; ::_thesis: verum
end;
end;
end;
thus  {} c= JUMP ((a,k1) >=0_goto 5) by XBOOLE_1:2; ::_thesis: verum
end;

Lm14:  for a being Int_position
for k2, k1 being Integer st k2 <> 5 holds
JUMP ((a,k1) >=0_goto k2) = {}
proof
let a be Int_position; ::_thesis: for k2, k1 being Integer st k2 <> 5 holds
JUMP ((a,k1) >=0_goto k2) = {}
let k2, k1 be Integer; ::_thesis: ( k2 <> 5 implies JUMP ((a,k1) >=0_goto k2) = {} )
set i = (a,k1) >=0_goto k2;
set X =  {  (NIC (((a,k1) >=0_goto k2),l)) where l is Element of NAT : verum  }  ;
assume A1: k2 <> 5 ; ::_thesis: JUMP ((a,k1) >=0_goto k2) = {}
hereby  :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: {} c= JUMP ((a,k1) >=0_goto k2)
set x1 = ((- k2) + (abs k2)) + 4;
let x be set ; ::_thesis: ( x in JUMP ((a,k1) >=0_goto k2) implies b1 in {} )
assume A2: x in JUMP ((a,k1) >=0_goto k2) ; ::_thesis: b1 in {}
A3: ((- k2) + (abs k2)) + 4 > ((- k2) + (abs k2)) + 0 by XREAL_1:6;
then A4: ((- k2) + (abs k2)) + 4 > 0 by ABSVALUE:27;
then reconsider x1 = ((- k2) + (abs k2)) + 4 as Element of NAT by INT_1:3;
set nl1 = (abs k2) + x1;
set nl2 = ((abs k2) + x1) + x1;
set l1 = (abs k2) + x1;
set l2 = ((abs k2) + x1) + x1;
 NIC (((a,k1) >=0_goto k2),((abs k2) + x1)) in  {  (NIC (((a,k1) >=0_goto k2),l)) where l is Element of NAT : verum  }  ;
then  x in NIC (((a,k1) >=0_goto k2),((abs k2) + x1)) by A2, SETFAM_1:def_1;
then consider s1 being Element of product (the_Values_of SCMPDS) such that
A5: x = IC (Exec (((a,k1) >=0_goto k2),s1)) and
A6: IC s1 = (abs k2) + x1 ;
consider m1 being Element of NAT  such that
A7: m1 = IC s1 and
A8: ICplusConst (s1,k2) = abs (m1 + k2) by SCMPDS_2:def_18;
 NIC (((a,k1) >=0_goto k2),(((abs k2) + x1) + x1)) in  {  (NIC (((a,k1) >=0_goto k2),l)) where l is Element of NAT : verum  }  ;
then  x in NIC (((a,k1) >=0_goto k2),(((abs k2) + x1) + x1)) by A2, SETFAM_1:def_1;
then consider s2 being Element of product (the_Values_of SCMPDS) such that
A9: x = IC (Exec (((a,k1) >=0_goto k2),s2)) and
A10: IC s2 = ((abs k2) + x1) + x1 ;
consider m2 being Element of NAT  such that
A11: m2 = IC s2 and
A12: ICplusConst (s2,k2) = abs (m2 + k2) by SCMPDS_2:def_18;
percases ( ( s1 . (DataLoc ((s1 . a),k1)) >= 0 & s2 . (DataLoc ((s2 . a),k1)) >= 0 ) or ( s1 . (DataLoc ((s1 . a),k1)) < 0 & s2 . (DataLoc ((s2 . a),k1)) < 0 ) or ( s1 . (DataLoc ((s1 . a),k1)) < 0 & s2 . (DataLoc ((s2 . a),k1)) >= 0 ) or ( s1 . (DataLoc ((s1 . a),k1)) >= 0 & s2 . (DataLoc ((s2 . a),k1)) < 0 ) ) ;
supposethat A13: s1 . (DataLoc ((s1 . a),k1)) >= 0 and
A14: s2 . (DataLoc ((s2 . a),k1)) >= 0 ; ::_thesis: b1 in {}
A15: x = abs (m2 + k2) by A9, A12, A14, SCMPDS_2:57;
A16: x = abs (m1 + k2) by A5, A8, A13, SCMPDS_2:57;
thus  x in {} ::_thesis: verum
proof
percases ( ((((abs k2) + x1) + 2) - 2) + k2 = (((((abs k2) + x1) + x1) + 2) - 2) + k2 or ((((abs k2) + x1) + 2) - 2) + k2 = - ((((((abs k2) + x1) + x1) + 2) - 2) + k2) ) by A6, A7, A10, A11, A16, A15, ABSVALUE:28;
suppose ((((abs k2) + x1) + 2) - 2) + k2 = (((((abs k2) + x1) + x1) + 2) - 2) + k2 ; ::_thesis: x in {}
hence  x in {} by A3, ABSVALUE:27; ::_thesis: verum
end;
suppose ((((abs k2) + x1) + 2) - 2) + k2 = - ((((((abs k2) + x1) + x1) + 2) - 2) + k2) ; ::_thesis: x in {}
hence  x in {} by Lm4; ::_thesis: verum
end;
end;
end;
end;
supposethat A17: s1 . (DataLoc ((s1 . a),k1)) < 0 and
A18: s2 . (DataLoc ((s2 . a),k1)) < 0 ; ::_thesis: b1 in {}
A19: x = succ (((abs k2) + x1) + x1) by A9, A10, A18, SCMPDS_2:57;
 x = succ ((abs k2) + x1) by A5, A6, A17, SCMPDS_2:57;
hence  x in {} by A3, A19, ABSVALUE:27; ::_thesis: verum
end;
supposethat A20: s1 . (DataLoc ((s1 . a),k1)) < 0 and
A21: s2 . (DataLoc ((s2 . a),k1)) >= 0 ; ::_thesis: b1 in {}
reconsider n1 = (abs k2) + x1 as Element of NAT ;
set w1 = n1;
A22: x = abs (m2 + k2) by A9, A12, A21, SCMPDS_2:57;
A23: x = succ n1 by A5, A6, A20, SCMPDS_2:57
.= n1 + 1 ;
thus  x in {} ::_thesis: verum
proof
percases ( n1 + 1 = m2 + k2 or n1 + 1 = - (m2 + k2) ) by A23, A22, ABSVALUE:1;
suppose n1 + 1 = m2 + k2 ; ::_thesis: x in {}
then  ((abs k2) + x1) + 1 = ((abs k2) + x1) + (x1 + k2) by A10, A11;
hence  x in {} by Lm5; ::_thesis: verum
end;
suppose n1 + 1 = - (m2 + k2) ; ::_thesis: x in {}
hence  x in {} by A4, A10, A11, Lm6; ::_thesis: verum
end;
end;
end;
end;
supposethat A24: s1 . (DataLoc ((s1 . a),k1)) >= 0 and
A25: s2 . (DataLoc ((s2 . a),k1)) < 0 ; ::_thesis: b1 in {}
reconsider n2 = ((abs k2) + x1) + x1 as Element of NAT ;
A26: x = succ n2 by A9, A10, A25, SCMPDS_2:57
.= n2 + 1 ;
set w2 = n2;
A27: x = abs (m1 + k2) by A5, A8, A24, SCMPDS_2:57;
thus  x in {} ::_thesis: verum
proof
percases ( n2 + 1 = m1 + k2 or n2 + 1 = - (m1 + k2) ) by A27, A26, ABSVALUE:1;
suppose n2 + 1 = m1 + k2 ; ::_thesis: x in {}
hence  x in {} by A1, A6, A7, Lm7; ::_thesis: verum
end;
suppose n2 + 1 = - (m1 + k2) ; ::_thesis: x in {}
hence  x in {} by A4, A6, A7, Lm8; ::_thesis: verum
end;
end;
end;
end;
end;
end;
thus  {} c= JUMP ((a,k1) >=0_goto k2) by XBOOLE_1:2; ::_thesis: verum
end;

registration
let a be Int_position;
let k1, k2 be Integer;
cluster JUMP ((a,k1) <>0_goto k2) ->  empty ;
coherence
 JUMP ((a,k1) <>0_goto k2) is empty
proof
 ( k2 = 5 or k2 <> 5 ) ;
hence  JUMP ((a,k1) <>0_goto k2) is empty by Lm9, Lm10; ::_thesis: verum
end;
cluster JUMP ((a,k1) <=0_goto k2) ->  empty ;
coherence
 JUMP ((a,k1) <=0_goto k2) is empty
proof
 ( k2 = 5 or k2 <> 5 ) ;
hence  JUMP ((a,k1) <=0_goto k2) is empty by Lm11, Lm12; ::_thesis: verum
end;
cluster JUMP ((a,k1) >=0_goto k2) ->  empty ;
coherence
 JUMP ((a,k1) >=0_goto k2) is empty
proof
 ( k2 = 5 or k2 <> 5 ) ;
hence  JUMP ((a,k1) >=0_goto k2) is empty by Lm13, Lm14; ::_thesis: verum
end;
end;

theorem Th18: :: SCMPDS_9:18
for l being Element of NAT holds SUCC (l,SCMPDS) = NAT
proof
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 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) = {(abs ((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
end;

registration
cluster SCMPDS  ->  non InsLoc-antisymmetric ;
coherence
 not SCMPDS is InsLoc-antisymmetric
proof
 SUCC (2,SCMPDS) = NAT by Th18;
then A1: 2 <= 1, SCMPDS by AMI_WSTD:33;
 SUCC (1,SCMPDS) = NAT by Th18;
then A2: 1 <= 2, SCMPDS by AMI_WSTD:33;
assume  SCMPDS is InsLoc-antisymmetric ; ::_thesis: contradiction
hence  contradiction by A2, A1, AMI_WSTD:def_2; ::_thesis: verum
end;
end;

registration
cluster SCMPDS  ->  non weakly_standard ;
coherence
 not SCMPDS is weakly_standard by AMI_WSTD:10;
end;