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;
((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 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 (Exec (((a,k1) >=0_goto k2),s)) and
A3: IC s = l ;
A5: ex m1 being Element of NAT st
( m1 = IC s & 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 A6: s . (DataLoc ((s . a),k1)) >= 0 ; :: thesis: b₁ in {(succ l),(abs (k2 + l))}

x = abs (k2 + l) by A2, A3, A5, A6, SCMPDS_2:69;
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 = succ l by A2, A3, A7, SCMPDS_2:69;
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)

A10: - 1 < 0 ;
set u1 = u +* (a .--> (- 1));
reconsider u1 = u +* (a .--> (- 1)) as Element of product the Object-Kind of SCMPDS by PBOOLE:155;
reconsider u2 = u1 +* ((DataLoc ((u1 . a),k1)) .--> (- 1)) as Element of product the Object-Kind of SCMPDS by PBOOLE:155;
A13: IC u2 = u1 . (IC SCMPDS) by FUNCT_4:88, SCMPDS_2:52
.= IC u by FUNCT_4:88, SCMPDS_2:52
.= n by EXTPRO_1:26 ;
A14: u2 . (DataLoc ((u1 . a),k1)) = - 1 by FUNCT_7:96;
u2 . (DataLoc ((u2 . a),k1)) < 0

proof

per cases ( 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 A14, A10, FUNCT_7:96; :: thesis: verum

end;

suppose a <> DataLoc ((u1 . a),k1) ; :: thesis: u2 . (DataLoc ((u2 . a),k1)) < 0

then u2 . a = u1 . a by FUNCT_4:88;
hence u2 . (DataLoc ((u2 . a),k1)) < 0 by A10, FUNCT_7:96; :: thesis: verum

end;

end;

end;

then x = IC (Exec (((a,k1) >=0_goto k2),u2)) by A9, A13, SCMPDS_2:69;
hence x in NIC (((a,k1) >=0_goto k2),l) by A13; :: thesis: verum

end;

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

set u1 = u +* (a .--> 0);
reconsider u1 = u +* (a .--> 0) as Element of product the Object-Kind of SCMPDS by PBOOLE:155;
reconsider u2 = u1 +* ((DataLoc ((u1 . a),k1)) .--> 0) as Element of product the Object-Kind of SCMPDS by PBOOLE:155;
A18: u2 . (DataLoc ((u1 . a),k1)) = 0 by FUNCT_7:96;
A19: u2 . (DataLoc ((u2 . a),k1)) >= 0

proof

per cases ( 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 A18, FUNCT_7:96; :: thesis: verum

end;

suppose a <> DataLoc ((u1 . a),k1) ; :: thesis: u2 . (DataLoc ((u2 . a),k1)) >= 0

then u2 . a = u1 . a by FUNCT_4:88;
hence u2 . (DataLoc ((u2 . a),k1)) >= 0 by FUNCT_7:96; :: thesis: verum

end;

end;

end;

A20: IC u2 = u1 . (IC SCMPDS) by FUNCT_4:88, SCMPDS_2:52
.= IC u by FUNCT_4:88, SCMPDS_2:52
.= n by EXTPRO_1:26 ;
ex m1 being Element of NAT st
( m1 = IC u2 & ICplusConst (u2,k2) = abs (m1 + k2) ) by SCMPDS_2:def 20;
then x = IC (Exec (((a,k1) >=0_goto k2),u2)) by A15, A20, A19, SCMPDS_2:69;
hence x in NIC (((a,k1) >=0_goto k2),l) by A20; :: thesis: verum

end;

end;