let s be State of SCMPDS ; :: thesis: for k1, k2 being Integer
for a, b being Int_position holds
( ( s . (DataLoc (s . a),k1) >= 0 implies (Exec (a,k1 >=0_goto k2),s) . (IC SCMPDS ) = ICplusConst s,k2 ) & ( s . (DataLoc (s . a),k1) < 0 implies (Exec (a,k1 >=0_goto k2),s) . (IC SCMPDS ) = Next (IC s) ) & (Exec (a,k1 >=0_goto k2),s) . b = s . b )
let k1, k2 be Integer; :: thesis: for a, b being Int_position holds
( ( s . (DataLoc (s . a),k1) >= 0 implies (Exec (a,k1 >=0_goto k2),s) . (IC SCMPDS ) = ICplusConst s,k2 ) & ( s . (DataLoc (s . a),k1) < 0 implies (Exec (a,k1 >=0_goto k2),s) . (IC SCMPDS ) = Next (IC s) ) & (Exec (a,k1 >=0_goto k2),s) . b = s . b )
let a, b be Int_position ; :: thesis: ( ( s . (DataLoc (s . a),k1) >= 0 implies (Exec (a,k1 >=0_goto k2),s) . (IC SCMPDS ) = ICplusConst s,k2 ) & ( s . (DataLoc (s . a),k1) < 0 implies (Exec (a,k1 >=0_goto k2),s) . (IC SCMPDS ) = Next (IC s) ) & (Exec (a,k1 >=0_goto k2),s) . b = s . b )
reconsider da = a as Element of SCM-Data-Loc by Def2;
reconsider I = a,k1 >=0_goto k2 as Element of SCMPDS-Instr ;
reconsider S = s as SCMPDS-State ;
reconsider i = 6 as Element of Segm 14 by GR_CY_1:10;
set A2 = Address_Add S,(I P31address ),(I P32const );
set JP = jump_address S,(I P33const );
set IF = IFGT 0 ,(S . (Address_Add S,(I P31address ),(I P32const ))),(succ (IC S)),(jump_address S,(I P33const ));
set Da = DataLoc (s . a),k1;
A1: I = [i,<*da,k1,k2*>] ;
A2: Exec (a,k1 >=0_goto k2),s = SCM-Exec-Res I,S by SCMPDS_1:def 25
.= SCM-Chg S,(IFGT 0 ,(S . (Address_Add S,(I P31address ),(I P32const ))),(succ (IC S)),(jump_address S,(I P33const ))) by A1, SCMPDS_1:def 24 ;
A3: ( I P31address = da & I P32const = k1 & I P33const = k2 ) by A1, SCMPDS_1:36;
consider n being Element of NAT such that
A4: ( n = IC s & ICplusConst s,k2 = abs (n + k2) ) by Def20;
thus ( s . (DataLoc (s . a),k1) >= 0 implies (Exec (a,k1 >=0_goto k2),s) . (IC SCMPDS ) = ICplusConst s,k2 ) :: thesis: ( ( s . (DataLoc (s . a),k1) < 0 implies (Exec (a,k1 >=0_goto k2),s) . (IC SCMPDS ) = Next (IC s) ) & (Exec (a,k1 >=0_goto k2),s) . b = s . b )

proof

assume A5: s . (DataLoc (s . a),k1) >= 0 ; :: thesis: (Exec (a,k1 >=0_goto k2),s) . (IC SCMPDS ) = ICplusConst s,k2
thus (Exec (a,k1 >=0_goto k2),s) . (IC SCMPDS ) = IFGT 0 ,(S . (Address_Add S,(I P31address ),(I P32const ))),(succ (IC S)),(jump_address S,(I P33const )) by A2, Th6, SCMPDS_1:26
.= ICplusConst s,k2 by A3, A4, A5, Th6, XXREAL_0:def 11 ; :: thesis: verum

end;

thus ( s . (DataLoc (s . a),k1) < 0 implies (Exec (a,k1 >=0_goto k2),s) . (IC SCMPDS ) = Next (IC s) ) :: thesis: (Exec (a,k1 >=0_goto k2),s) . b = s . b

proof

assume A6: s . (DataLoc (s . a),k1) < 0 ; :: thesis: (Exec (a,k1 >=0_goto k2),s) . (IC SCMPDS ) = Next (IC s)
thus (Exec (a,k1 >=0_goto k2),s) . (IC SCMPDS ) = IFGT 0 ,(S . (Address_Add S,(I P31address ),(I P32const ))),(succ (IC S)),(jump_address S,(I P33const )) by A2, Th6, SCMPDS_1:26
.= succ (IC S) by A3, A6, XXREAL_0:def 11
.= Next (IC s) by AMI_2:30, FUNCT_7:def 1 ; :: thesis: verum

end;

reconsider mn = b as Element of SCM-Data-Loc by Def2;
thus (Exec (a,k1 >=0_goto k2),s) . b = S . mn by A2, SCMPDS_1:27
.= s . b ; :: thesis: verum