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) = {(l + 1),|.(k2 + l).|}
let l be Element of NAT ; :: thesis: for k1, k2 being Integer holds NIC (((a,k1) >=0_goto k2),l) = {(l + 1),|.(k2 + l).|}
let k1, k2 be Integer; :: thesis: NIC (((a,k1) >=0_goto k2),l) = {(l + 1),|.(k2 + l).|}
set s = the State of SCMPDS;
set i = (a,k1) >=0_goto k2;
set t = |.(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: {(l + 1),|.(k2 + l).|} c= NIC (((a,k1) >=0_goto k2),l)
let x be object ; :: thesis: ( x in NIC (((a,k1) >=0_goto k2),l) implies b1 in {(l + 1),|.(k2 + l).|} )
assume x in NIC (((a,k1) >=0_goto k2),l) ; :: thesis: b1 in {(l + 1),|.(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) = |.(m1 + k2).| ) by SCMPDS_2:def 18;
per cases ( s . (DataLoc ((s . a),k1)) >= 0 or s . (DataLoc ((s . a),k1)) < 0 ) ;
suppose A4: s . (DataLoc ((s . a),k1)) >= 0 ; :: thesis: b1 in {(l + 1),|.(k2 + l).|}
x = |.(k2 + l).| by A1, A2, A3, A4, SCMPDS_2:57;
hence x in {(l + 1),|.(k2 + l).|} by TARSKI:def 2; :: thesis: verum
end;
suppose A5: s . (DataLoc ((s . a),k1)) < 0 ; :: thesis: b1 in {(l + 1),|.(k2 + l).|}
x = l + 1 by A1, A2, A5, SCMPDS_2:57;
hence x in {(l + 1),|.(k2 + l).|} by TARSKI:def 2; :: thesis: verum
end;
end;
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {(l + 1),|.(k2 + l).|} or x in NIC (((a,k1) >=0_goto k2),l) )
assume A6: x in {(l + 1),|.(k2 + l).|} ; :: thesis: x in NIC (((a,k1) >=0_goto k2),l)
per cases ( x = l + 1 or x = |.(k2 + l).| ) by A6, TARSKI:def 2;
suppose A7: x = l + 1 ; :: 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
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 A10; :: 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;
suppose A11: x = |.(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
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 A12; :: 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) = |.(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;