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))}
consider s being State of SCMPDS ;
set i = a,k1 <=0_goto k2;
set t = abs (k2 + l);
reconsider I = a,k1 <=0_goto k2 as Element of the Object-Kind of SCMPDS . l by COMPOS_1:def 8;
reconsider n = l as Element of NAT ;
reconsider il1 = l as Element of ObjectKind (IC SCMPDS ) by COMPOS_1:def 6;
X: ((IC SCMPDS ) .--> il1) +* (l .--> (a,k1 <=0_goto k2)) is the Object-Kind of SCMPDS -compatible PartState of SCMPDS ;
(IC SCMPDS ),l --> il1,I = ((IC SCMPDS ) .--> il1) +* (l .--> I) by FUNCT_4:def 4;
then reconsider u = s +* ((IC SCMPDS ),l --> il1,(a,k1 <=0_goto k2)) as Element of product the Object-Kind of SCMPDS by X, PBOOLE:155;

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 b₁ in {(succ l),(abs (k2 + l))} )
assume x in NIC (a,k1 <=0_goto k2),l ; :: thesis: b₁ in {(succ l),(abs (k2 + l))}
then consider s being Element of product the Object-Kind of SCMPDS such that
A2: x = IC (Following (ProgramPart s),s) and
A3: IC s = l and
A4: (ProgramPart s) /. l = a,k1 <=0_goto k2 ;
A5: ex m1 being Element of NAT st
( m1 = IC s & ICplusConst s,k2 = abs (m1 + k2) ) by SCMPDS_2:def 20;
Y: (ProgramPart s) /. (IC s) = s . (IC s) by COMPOS_1:38;
y: (ProgramPart s) . (IC s) = s . (IC s) by COMPOS_1:2;

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

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

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

end;

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

x = (Exec (a,k1 <=0_goto k2),s) . (IC SCMPDS ) by A2, A3, A4, Y, y, AMI_1:131
.= succ l by A3, A7, SCMPDS_2:68 ;
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 A8: x in {(succ l),(abs (k2 + l))} ; :: thesis: x in NIC (a,k1 <=0_goto k2),l

per cases ( x = succ l or x = abs (k2 + l) ) by A8, TARSKI:def 2;

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

set u1 = u +* (a .--> 1);
reconsider u2 = (u +* (a .--> 1)) +* ((DataLoc ((u +* (a .--> 1)) . a),k1) .--> 1) as Element of product the Object-Kind of SCMPDS by PBOOLE:155;
A10: l <> a by SCMPDS_2:53;
l <> DataLoc ((u +* (a .--> 1)) . a),k1 by SCMPDS_2:53;
then A11: u2 . l = (u +* (a .--> 1)) . l by FUNCT_4:88
.= u . n by A10, FUNCT_4:88
.= a,k1 <=0_goto k2 by AMI_1:129 ;
A12: IC u2 = u2 . (IC SCMPDS ) by COMPOS_1:def 9
.= (u +* (a .--> 1)) . (IC SCMPDS ) by FUNCT_4:88, SCMPDS_2:52
.= u . (IC SCMPDS ) by FUNCT_4:88, SCMPDS_2:52
.= IC u by COMPOS_1:def 9
.= n by AMI_1:129 ;
A13: u2 . (DataLoc ((u +* (a .--> 1)) . a),k1) = 1 by FUNCT_7:96;
X: (ProgramPart u2) /. (IC u2) = u2 . (IC u2) by COMPOS_1:38;
Y: (ProgramPart u2) . (IC u2) = u2 . (IC u2) by COMPOS_1:2;
u2 . (DataLoc (u2 . a),k1) > 0

proof

per cases ( a = DataLoc ((u +* (a .--> 1)) . a),k1 or a <> DataLoc ((u +* (a .--> 1)) . a),k1 ) ;

suppose a = DataLoc ((u +* (a .--> 1)) . a),k1 ; :: thesis: u2 . (DataLoc (u2 . a),k1) > 0

hence u2 . (DataLoc (u2 . a),k1) > 0 by A13, FUNCT_7:96; :: thesis: verum

end;

suppose a <> DataLoc ((u +* (a .--> 1)) . a),k1 ; :: thesis: u2 . (DataLoc (u2 . a),k1) > 0

then u2 . a = (u +* (a .--> 1)) . a by FUNCT_4:88;
hence u2 . (DataLoc (u2 . a),k1) > 0 by FUNCT_7:96; :: thesis: verum

end;

end;

end;

then x = (Exec (a,k1 <=0_goto k2),u2) . (IC SCMPDS ) by A9, A12, SCMPDS_2:68
.= IC (Following (ProgramPart u2),u2) by A11, A12, Y, AMI_1:131 ;
hence x in NIC (a,k1 <=0_goto k2),l by A11, A12, X; :: thesis: verum

end;

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

set u1 = u +* (a .--> 0 );
reconsider u2 = (u +* (a .--> 0 )) +* ((DataLoc ((u +* (a .--> 0 )) . a),k1) .--> 0 ) as Element of product the Object-Kind of SCMPDS by PBOOLE:155;
A15: l <> a by SCMPDS_2:53;
l <> DataLoc ((u +* (a .--> 0 )) . a),k1 by SCMPDS_2:53;
then A16: u2 . l = (u +* (a .--> 0 )) . l by FUNCT_4:88
.= u . n by A15, FUNCT_4:88
.= a,k1 <=0_goto k2 by AMI_1:129 ;
A17: u2 . (DataLoc ((u +* (a .--> 0 )) . a),k1) = 0 by FUNCT_7:96;
A18: u2 . (DataLoc (u2 . a),k1) <= 0

proof

per cases ( a = DataLoc ((u +* (a .--> 0 )) . a),k1 or a <> DataLoc ((u +* (a .--> 0 )) . a),k1 ) ;

suppose a = DataLoc ((u +* (a .--> 0 )) . a),k1 ; :: thesis: u2 . (DataLoc (u2 . a),k1) <= 0

hence u2 . (DataLoc (u2 . a),k1) <= 0 by A17, FUNCT_7:96; :: thesis: verum

end;

suppose a <> DataLoc ((u +* (a .--> 0 )) . a),k1 ; :: thesis: u2 . (DataLoc (u2 . a),k1) <= 0

then u2 . a = (u +* (a .--> 0 )) . a by FUNCT_4:88;
hence u2 . (DataLoc (u2 . a),k1) <= 0 by FUNCT_7:96; :: thesis: verum

end;

end;

end;

A19: IC u2 = u2 . (IC SCMPDS ) by COMPOS_1:def 9
.= (u +* (a .--> 0 )) . (IC SCMPDS ) by FUNCT_4:88, SCMPDS_2:52
.= u . (IC SCMPDS ) by FUNCT_4:88, SCMPDS_2:52
.= IC u by COMPOS_1:def 9
.= n by AMI_1:129 ;
X: (ProgramPart u2) /. (IC u2) = u2 . (IC u2) by COMPOS_1:38;
Y: (ProgramPart u2) . (IC u2) = u2 . (IC u2) by COMPOS_1:2;
ex m1 being Element of NAT st
( m1 = IC u2 & ICplusConst u2,k2 = abs (m1 + k2) ) by SCMPDS_2:def 20;
then x = (Exec (a,k1 <=0_goto k2),u2) . (IC SCMPDS ) by A14, A19, A18, SCMPDS_2:68
.= IC (Following (ProgramPart u2),u2) by A16, A19, Y, AMI_1:131 ;
hence x in NIC (a,k1 <=0_goto k2),l by A16, A19, X; :: thesis: verum

end;

end;