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 ) = 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 SCMPDS ) = ICplusConst s,k2 ) & ( s . (DataLoc (s . a),k1) > 0 implies (Exec (a,k1 <=0_goto k2),s) . (IC SCMPDS ) = 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 SCMPDS ) = ICplusConst s,k2 ) & ( s . (DataLoc (s . a),k1) > 0 implies (Exec (a,k1 <=0_goto k2),s) . (IC SCMPDS ) = 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 PBOOLE:155;
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 (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 14 by NAT_1:45;
A2: I = [i,{} ,<*da,k1,k2*>] ;
then A3: ( I P31address = da & I P32const = k1 ) by SCMPDS_1:36;
A4: Exec (a,k1 <=0_goto k2),s = SCM-Exec-Res I,S by SCMPDS_1:def 25
.= SCM-Chg S,(IFGT (S . (Address_Add S,(I P31address ),(I P32const ))),0 ,(succ (IC S)),(jump_address S,(I P33const ))) by A2, SCMPDS_1:def 24 ;
A5: I P33const = k2 by A2, SCMPDS_1:36;
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 ) = 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 SCMPDS ) = ICplusConst s,k2
thus (Exec (a,k1 <=0_goto k2),s) . (IC SCMPDS ) = IFGT (S . (Address_Add S,(I P31address ),(I P32const ))),0 ,(succ (IC S)),(jump_address S,(I P33const )) by A4, Th6, SCMPDS_1:26
.= 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 SCMPDS ) = 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 SCMPDS ) = succ (IC s)
thus (Exec (a,k1 <=0_goto k2),s) . (IC SCMPDS ) = IFGT (S . (Address_Add S,(I P31address ),(I P32const ))),0 ,(succ (IC S)),(jump_address S,(I P33const )) by A4, Th6, SCMPDS_1:26
.= succ (IC S) by A3, A7, XXREAL_0:def 11
.= succ (IC s) by AMI_2:30, FUNCT_7:def 1 ; :: thesis: verum

end;

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