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 AMI_2:def 16;
reconsider S = s as SCM-State by CARD_3:107;
A1: ex n being Element of NAT st
( n = IC s & ICplusConst (s,k2) = abs (n + k2) ) by Def18;
reconsider da = a as Element of SCM-Data-Loc by AMI_2:def 16;
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 ((S . (Address_Add (S,(I P31address),(I P32const)))),0,(succ (IC S)),(jump_address (S,(I P33const))));
set Da = DataLoc ((s . a),k1);
reconsider i = 5 as Element of Segm 15 by NAT_1:44;
A2: I = [i,{},<*da,k1,k2*>] ;
then A3: ( I P31address = da & I P32const = k1 ) by SCMPDS_I:6;
A4: InsCode I = 5 by RECDEF_2:def 1;
A5: Exec (((a,k1) <=0_goto k2),s) = SCM-Exec-Res (I,S) by SCMPDS_1:def 23
.= SCM-Chg (S,(IFGT ((S . (Address_Add (S,(I P31address),(I P32const)))),0,(succ (IC S)),(jump_address (S,(I P33const)))))) by A4, SCMPDS_1:def 22 ;
A6: I P33const = k2 by A2, SCMPDS_I:6;
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 A7: 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 ((S . (Address_Add (S,(I P31address),(I P32const)))),0,(succ (IC S)),(jump_address (S,(I P33const)))) by A5, Th2, AMI_2:11
.= ICplusConst (s,k2) by A3, A6, A1, A7, Th2, 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 A8: 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 ((S . (Address_Add (S,(I P31address),(I P32const)))),0,(succ (IC S)),(jump_address (S,(I P33const)))) by A5, Th2, AMI_2:11
.= succ (IC S) by A3, A8, 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 A5, AMI_2:12
.= s . b ; :: thesis: verum