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 ) = ICplusConst (s,k2) ) & ( s . (DataLoc ((s . a),k1)) < 0 implies (Exec (((a,k1) >=0_goto k2),s)) . (IC ) = succ (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 ) = ICplusConst (s,k2) ) & ( s . (DataLoc ((s . a),k1)) < 0 implies (Exec (((a,k1) >=0_goto k2),s)) . (IC ) = succ (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 ) = ICplusConst (s,k2) ) & ( s . (DataLoc ((s . a),k1)) < 0 implies (Exec (((a,k1) >=0_goto k2),s)) . (IC ) = succ (IC s) ) & (Exec (((a,k1) >=0_goto k2),s)) . b = s . b )
reconsider mn = b as Element of SCM-Data-Loc by Def2;
reconsider S = s as SCMPDS-State by CARD_3:107;
A1: ex n being Element of NAT st
( n = IC s & ICplusConst (s,k2) = abs (n + k2) ) by Def20;
reconsider da = a as Element of SCM-Data-Loc by Def2;
reconsider I = (a,k1) >=0_goto k2 as Element of SCMPDS-Instr ;
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);
reconsider i = 6 as Element of Segm 14 by NAT_1:44;
A2: I = [i,{},<*da,k1,k2*>] ;
then A3: ( I P31address = da & I P32const = k1 ) by SCMPDS_1:21;
A4: Exec (((a,k1) >=0_goto k2),s) = SCM-Exec-Res (I,S) by SCMPDS_1:def 23
.= SCM-Chg (S,(IFGT (0,(S . (Address_Add (S,(I P31address),(I P32const)))),(succ (IC S)),(jump_address (S,(I P33const)))))) by A2, SCMPDS_1:def 22 ;
A5: I P33const = k2 by A2, SCMPDS_1:21;
thus ( s . (DataLoc ((s . a),k1)) >= 0 implies (Exec (((a,k1) >=0_goto k2),s)) . (IC ) = ICplusConst (s,k2) ) :: thesis: ( ( s . (DataLoc ((s . a),k1)) < 0 implies (Exec (((a,k1) >=0_goto k2),s)) . (IC ) = succ (IC s) ) & (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 ) = ICplusConst (s,k2)
thus (Exec (((a,k1) >=0_goto k2),s)) . (IC ) = IFGT (0,(S . (Address_Add (S,(I P31address),(I P32const)))),(succ (IC S)),(jump_address (S,(I P33const)))) by A4, Th6, SCMPDS_1:13
.= ICplusConst (s,k2) by A3, A5, A1, A6, Th6, XXREAL_0:def 11 ; :: thesis: verum

end;

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

proof

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

end;

thus (Exec (((a,k1) >=0_goto k2),s)) . b = S . mn by A4, SCMPDS_1:14
.= s . b ; :: thesis: verum