let a be Int_position ; :: thesis: for l being Instruction-Location of SCMPDS
for k1, k2 being Integer holds NIC (a,k1 <=0_goto k2),l = {(Next l),(abs (k2 + (locnum l)))}
let l be Instruction-Location of SCMPDS ; :: thesis: for k1, k2 being Integer holds NIC (a,k1 <=0_goto k2),l = {(Next l),(abs (k2 + (locnum l)))}
let k1, k2 be Integer; :: thesis: NIC (a,k1 <=0_goto k2),l = {(Next l),(abs (k2 + (locnum l)))}
set i = a,k1 <=0_goto k2;
set t = abs (k2 + (locnum l));
A1: locnum l = l by Th8;

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: {(Next l),(abs (k2 + (locnum l)))} c= NIC (a,k1 <=0_goto k2),l

let x be set ; :: thesis: ( x in NIC (a,k1 <=0_goto k2),l implies b₁ in {(Next l),(abs (k2 + (locnum l)))} )
assume x in NIC (a,k1 <=0_goto k2),l ; :: thesis: b₁ in {(Next l),(abs (k2 + (locnum l)))}
then consider s being State of SCMPDS such that
A2: x = IC (Following s) and
A3: IC s = l and
A4: s . l = a,k1 <=0_goto k2 ;
consider m1 being Element of NAT such that
A5: m1 = IC s and
A6: ICplusConst s,k2 = abs (m1 + k2) by SCMPDS_2:def 20;

per cases ( s . (DataLoc (s . a),k1) <= 0 or s . (DataLoc (s . a),k1) > 0 ) ;

suppose A7: s . (DataLoc (s . a),k1) <= 0 ; :: thesis: b₁ in {(Next l),(abs (k2 + (locnum l)))}

x = (Exec (a,k1 <=0_goto k2),s) . (IC SCMPDS ) by A2, A3, A4, AMI_1:131
.= abs (k2 + (locnum l)) by A1, A3, A5, A6, A7, SCMPDS_2:68 ;
hence x in {(Next l),(abs (k2 + (locnum l)))} by TARSKI:def 2; :: thesis: verum

end;

suppose A8: s . (DataLoc (s . a),k1) > 0 ; :: thesis: b₁ in {(Next l),(abs (k2 + (locnum l)))}

x = (Exec (a,k1 <=0_goto k2),s) . (IC SCMPDS ) by A2, A3, A4, AMI_1:131
.= Next l by A3, A8, SCMPDS_2:68 ;
hence x in {(Next l),(abs (k2 + (locnum l)))} by TARSKI:def 2; :: thesis: verum

end;

end;

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in {(Next l),(abs (k2 + (locnum l)))} or x in NIC (a,k1 <=0_goto k2),l )
assume A9: x in {(Next l),(abs (k2 + (locnum l)))} ; :: thesis: x in NIC (a,k1 <=0_goto k2),l
consider s being State of SCMPDS ;
l in NAT by AMI_1:def 4;
then reconsider il1 = l as Element of ObjectKind (IC SCMPDS ) by AMI_1:def 11;
reconsider I = a,k1 <=0_goto k2 as Element of ObjectKind l by AMI_1:def 14;
set u = s +* ((IC SCMPDS ),l --> il1,I);

per cases ( x = Next l or x = abs (k2 + (locnum l)) ) by A9, TARSKI:def 2;

suppose A10: x = Next l ; :: thesis: x in NIC (a,k1 <=0_goto k2),l

set u1 = (s +* ((IC SCMPDS ),l --> il1,I)) +* (a .--> 1);
set u2 = ((s +* ((IC SCMPDS ),l --> il1,I)) +* (a .--> 1)) +* ((DataLoc (((s +* ((IC SCMPDS ),l --> il1,I)) +* (a .--> 1)) . a),k1) .--> 1);
A11: l <> a by SCMPDS_2:53;
l <> DataLoc (((s +* ((IC SCMPDS ),l --> il1,I)) +* (a .--> 1)) . a),k1 by SCMPDS_2:53;
then A12: (((s +* ((IC SCMPDS ),l --> il1,I)) +* (a .--> 1)) +* ((DataLoc (((s +* ((IC SCMPDS ),l --> il1,I)) +* (a .--> 1)) . a),k1) .--> 1)) . l = ((s +* ((IC SCMPDS ),l --> il1,I)) +* (a .--> 1)) . l by FUNCT_4:88
.= (s +* ((IC SCMPDS ),l --> il1,I)) . l by A11, FUNCT_4:88
.= a,k1 <=0_goto k2 by AMI_1:129 ;
A13: IC (((s +* ((IC SCMPDS ),l --> il1,I)) +* (a .--> 1)) +* ((DataLoc (((s +* ((IC SCMPDS ),l --> il1,I)) +* (a .--> 1)) . a),k1) .--> 1)) = (((s +* ((IC SCMPDS ),l --> il1,I)) +* (a .--> 1)) +* ((DataLoc (((s +* ((IC SCMPDS ),l --> il1,I)) +* (a .--> 1)) . a),k1) .--> 1)) . (IC SCMPDS ) by AMI_1:def 15
.= ((s +* ((IC SCMPDS ),l --> il1,I)) +* (a .--> 1)) . (IC SCMPDS ) by FUNCT_4:88, SCMPDS_2:52
.= (s +* ((IC SCMPDS ),l --> il1,I)) . (IC SCMPDS ) by FUNCT_4:88, SCMPDS_2:52
.= IC (s +* ((IC SCMPDS ),l --> il1,I)) by AMI_1:def 15
.= il1 by AMI_1:129 ;
A14: (((s +* ((IC SCMPDS ),l --> il1,I)) +* (a .--> 1)) +* ((DataLoc (((s +* ((IC SCMPDS ),l --> il1,I)) +* (a .--> 1)) . a),k1) .--> 1)) . (DataLoc (((s +* ((IC SCMPDS ),l --> il1,I)) +* (a .--> 1)) . a),k1) = 1 by FUNCT_7:96;
(((s +* ((IC SCMPDS ),l --> il1,I)) +* (a .--> 1)) +* ((DataLoc (((s +* ((IC SCMPDS ),l --> il1,I)) +* (a .--> 1)) . a),k1) .--> 1)) . (DataLoc ((((s +* ((IC SCMPDS ),l --> il1,I)) +* (a .--> 1)) +* ((DataLoc (((s +* ((IC SCMPDS ),l --> il1,I)) +* (a .--> 1)) . a),k1) .--> 1)) . a),k1) > 0

proof

per cases ( a = DataLoc (((s +* ((IC SCMPDS ),l --> il1,I)) +* (a .--> 1)) . a),k1 or a <> DataLoc (((s +* ((IC SCMPDS ),l --> il1,I)) +* (a .--> 1)) . a),k1 ) ;

suppose a = DataLoc (((s +* ((IC SCMPDS ),l --> il1,I)) +* (a .--> 1)) . a),k1 ; :: thesis: (((s +* ((IC SCMPDS ),l --> il1,I)) +* (a .--> 1)) +* ((DataLoc (((s +* ((IC SCMPDS ),l --> il1,I)) +* (a .--> 1)) . a),k1) .--> 1)) . (DataLoc ((((s +* ((IC SCMPDS ),l --> il1,I)) +* (a .--> 1)) +* ((DataLoc (((s +* ((IC SCMPDS ),l --> il1,I)) +* (a .--> 1)) . a),k1) .--> 1)) . a),k1) > 0

hence (((s +* ((IC SCMPDS ),l --> il1,I)) +* (a .--> 1)) +* ((DataLoc (((s +* ((IC SCMPDS ),l --> il1,I)) +* (a .--> 1)) . a),k1) .--> 1)) . (DataLoc ((((s +* ((IC SCMPDS ),l --> il1,I)) +* (a .--> 1)) +* ((DataLoc (((s +* ((IC SCMPDS ),l --> il1,I)) +* (a .--> 1)) . a),k1) .--> 1)) . a),k1) > 0 by A14, FUNCT_7:96; :: thesis: verum

end;

suppose a <> DataLoc (((s +* ((IC SCMPDS ),l --> il1,I)) +* (a .--> 1)) . a),k1 ; :: thesis: (((s +* ((IC SCMPDS ),l --> il1,I)) +* (a .--> 1)) +* ((DataLoc (((s +* ((IC SCMPDS ),l --> il1,I)) +* (a .--> 1)) . a),k1) .--> 1)) . (DataLoc ((((s +* ((IC SCMPDS ),l --> il1,I)) +* (a .--> 1)) +* ((DataLoc (((s +* ((IC SCMPDS ),l --> il1,I)) +* (a .--> 1)) . a),k1) .--> 1)) . a),k1) > 0

then (((s +* ((IC SCMPDS ),l --> il1,I)) +* (a .--> 1)) +* ((DataLoc (((s +* ((IC SCMPDS ),l --> il1,I)) +* (a .--> 1)) . a),k1) .--> 1)) . a = ((s +* ((IC SCMPDS ),l --> il1,I)) +* (a .--> 1)) . a by FUNCT_4:88;
hence (((s +* ((IC SCMPDS ),l --> il1,I)) +* (a .--> 1)) +* ((DataLoc (((s +* ((IC SCMPDS ),l --> il1,I)) +* (a .--> 1)) . a),k1) .--> 1)) . (DataLoc ((((s +* ((IC SCMPDS ),l --> il1,I)) +* (a .--> 1)) +* ((DataLoc (((s +* ((IC SCMPDS ),l --> il1,I)) +* (a .--> 1)) . a),k1) .--> 1)) . a),k1) > 0 by FUNCT_7:96; :: thesis: verum

end;

end;

end;

then x = (Exec (a,k1 <=0_goto k2),(((s +* ((IC SCMPDS ),l --> il1,I)) +* (a .--> 1)) +* ((DataLoc (((s +* ((IC SCMPDS ),l --> il1,I)) +* (a .--> 1)) . a),k1) .--> 1))) . (IC SCMPDS ) by A10, A13, SCMPDS_2:68
.= IC (Following (((s +* ((IC SCMPDS ),l --> il1,I)) +* (a .--> 1)) +* ((DataLoc (((s +* ((IC SCMPDS ),l --> il1,I)) +* (a .--> 1)) . a),k1) .--> 1))) by A12, A13, AMI_1:131 ;
hence x in NIC (a,k1 <=0_goto k2),l by A12, A13; :: thesis: verum

end;

suppose A15: x = abs (k2 + (locnum l)) ; :: thesis: x in NIC (a,k1 <=0_goto k2),l

set u1 = (s +* ((IC SCMPDS ),l --> il1,I)) +* (a .--> 0 );
set u2 = ((s +* ((IC SCMPDS ),l --> il1,I)) +* (a .--> 0 )) +* ((DataLoc (((s +* ((IC SCMPDS ),l --> il1,I)) +* (a .--> 0 )) . a),k1) .--> 0 );
A16: l <> a by SCMPDS_2:53;
l <> DataLoc (((s +* ((IC SCMPDS ),l --> il1,I)) +* (a .--> 0 )) . a),k1 by SCMPDS_2:53;
then A17: (((s +* ((IC SCMPDS ),l --> il1,I)) +* (a .--> 0 )) +* ((DataLoc (((s +* ((IC SCMPDS ),l --> il1,I)) +* (a .--> 0 )) . a),k1) .--> 0 )) . l = ((s +* ((IC SCMPDS ),l --> il1,I)) +* (a .--> 0 )) . l by FUNCT_4:88
.= (s +* ((IC SCMPDS ),l --> il1,I)) . l by A16, FUNCT_4:88
.= a,k1 <=0_goto k2 by AMI_1:129 ;
A18: IC (((s +* ((IC SCMPDS ),l --> il1,I)) +* (a .--> 0 )) +* ((DataLoc (((s +* ((IC SCMPDS ),l --> il1,I)) +* (a .--> 0 )) . a),k1) .--> 0 )) = (((s +* ((IC SCMPDS ),l --> il1,I)) +* (a .--> 0 )) +* ((DataLoc (((s +* ((IC SCMPDS ),l --> il1,I)) +* (a .--> 0 )) . a),k1) .--> 0 )) . (IC SCMPDS ) by AMI_1:def 15
.= ((s +* ((IC SCMPDS ),l --> il1,I)) +* (a .--> 0 )) . (IC SCMPDS ) by FUNCT_4:88, SCMPDS_2:52
.= (s +* ((IC SCMPDS ),l --> il1,I)) . (IC SCMPDS ) by FUNCT_4:88, SCMPDS_2:52
.= IC (s +* ((IC SCMPDS ),l --> il1,I)) by AMI_1:def 15
.= il1 by AMI_1:129 ;
A19: (((s +* ((IC SCMPDS ),l --> il1,I)) +* (a .--> 0 )) +* ((DataLoc (((s +* ((IC SCMPDS ),l --> il1,I)) +* (a .--> 0 )) . a),k1) .--> 0 )) . (DataLoc (((s +* ((IC SCMPDS ),l --> il1,I)) +* (a .--> 0 )) . a),k1) = 0 by FUNCT_7:96;
A20: (((s +* ((IC SCMPDS ),l --> il1,I)) +* (a .--> 0 )) +* ((DataLoc (((s +* ((IC SCMPDS ),l --> il1,I)) +* (a .--> 0 )) . a),k1) .--> 0 )) . (DataLoc ((((s +* ((IC SCMPDS ),l --> il1,I)) +* (a .--> 0 )) +* ((DataLoc (((s +* ((IC SCMPDS ),l --> il1,I)) +* (a .--> 0 )) . a),k1) .--> 0 )) . a),k1) <= 0

proof

per cases ( a = DataLoc (((s +* ((IC SCMPDS ),l --> il1,I)) +* (a .--> 0 )) . a),k1 or a <> DataLoc (((s +* ((IC SCMPDS ),l --> il1,I)) +* (a .--> 0 )) . a),k1 ) ;

suppose a = DataLoc (((s +* ((IC SCMPDS ),l --> il1,I)) +* (a .--> 0 )) . a),k1 ; :: thesis: (((s +* ((IC SCMPDS ),l --> il1,I)) +* (a .--> 0 )) +* ((DataLoc (((s +* ((IC SCMPDS ),l --> il1,I)) +* (a .--> 0 )) . a),k1) .--> 0 )) . (DataLoc ((((s +* ((IC SCMPDS ),l --> il1,I)) +* (a .--> 0 )) +* ((DataLoc (((s +* ((IC SCMPDS ),l --> il1,I)) +* (a .--> 0 )) . a),k1) .--> 0 )) . a),k1) <= 0

hence (((s +* ((IC SCMPDS ),l --> il1,I)) +* (a .--> 0 )) +* ((DataLoc (((s +* ((IC SCMPDS ),l --> il1,I)) +* (a .--> 0 )) . a),k1) .--> 0 )) . (DataLoc ((((s +* ((IC SCMPDS ),l --> il1,I)) +* (a .--> 0 )) +* ((DataLoc (((s +* ((IC SCMPDS ),l --> il1,I)) +* (a .--> 0 )) . a),k1) .--> 0 )) . a),k1) <= 0 by A19, FUNCT_7:96; :: thesis: verum

end;

suppose a <> DataLoc (((s +* ((IC SCMPDS ),l --> il1,I)) +* (a .--> 0 )) . a),k1 ; :: thesis: (((s +* ((IC SCMPDS ),l --> il1,I)) +* (a .--> 0 )) +* ((DataLoc (((s +* ((IC SCMPDS ),l --> il1,I)) +* (a .--> 0 )) . a),k1) .--> 0 )) . (DataLoc ((((s +* ((IC SCMPDS ),l --> il1,I)) +* (a .--> 0 )) +* ((DataLoc (((s +* ((IC SCMPDS ),l --> il1,I)) +* (a .--> 0 )) . a),k1) .--> 0 )) . a),k1) <= 0

then (((s +* ((IC SCMPDS ),l --> il1,I)) +* (a .--> 0 )) +* ((DataLoc (((s +* ((IC SCMPDS ),l --> il1,I)) +* (a .--> 0 )) . a),k1) .--> 0 )) . a = ((s +* ((IC SCMPDS ),l --> il1,I)) +* (a .--> 0 )) . a by FUNCT_4:88;
hence (((s +* ((IC SCMPDS ),l --> il1,I)) +* (a .--> 0 )) +* ((DataLoc (((s +* ((IC SCMPDS ),l --> il1,I)) +* (a .--> 0 )) . a),k1) .--> 0 )) . (DataLoc ((((s +* ((IC SCMPDS ),l --> il1,I)) +* (a .--> 0 )) +* ((DataLoc (((s +* ((IC SCMPDS ),l --> il1,I)) +* (a .--> 0 )) . a),k1) .--> 0 )) . a),k1) <= 0 by FUNCT_7:96; :: thesis: verum

end;

end;

end;

consider m1 being Element of NAT such that
A21: m1 = IC (((s +* ((IC SCMPDS ),l --> il1,I)) +* (a .--> 0 )) +* ((DataLoc (((s +* ((IC SCMPDS ),l --> il1,I)) +* (a .--> 0 )) . a),k1) .--> 0 )) and
A22: ICplusConst (((s +* ((IC SCMPDS ),l --> il1,I)) +* (a .--> 0 )) +* ((DataLoc (((s +* ((IC SCMPDS ),l --> il1,I)) +* (a .--> 0 )) . a),k1) .--> 0 )),k2 = abs (m1 + k2) by SCMPDS_2:def 20;
x = (Exec (a,k1 <=0_goto k2),(((s +* ((IC SCMPDS ),l --> il1,I)) +* (a .--> 0 )) +* ((DataLoc (((s +* ((IC SCMPDS ),l --> il1,I)) +* (a .--> 0 )) . a),k1) .--> 0 ))) . (IC SCMPDS ) by A1, A15, A18, A20, A21, A22, SCMPDS_2:68
.= IC (Following (((s +* ((IC SCMPDS ),l --> il1,I)) +* (a .--> 0 )) +* ((DataLoc (((s +* ((IC SCMPDS ),l --> il1,I)) +* (a .--> 0 )) . a),k1) .--> 0 ))) by A17, A18, AMI_1:131 ;
hence x in NIC (a,k1 <=0_goto k2),l by A17, A18; :: thesis: verum

end;

end;