let s be State of SCMPDS ; :: thesis: for k1 being Integer holds
( (Exec (goto k1),s) . (IC SCMPDS ) = ICplusConst s,k1 & ( for a being Int_position holds (Exec (goto k1),s) . a = s . a ) )
let k1 be Integer; :: thesis: ( (Exec (goto k1),s) . (IC SCMPDS ) = ICplusConst s,k1 & ( for a being Int_position holds (Exec (goto k1),s) . a = s . a ) )
reconsider i = 0 as Element of Segm 14 by NAT_1:45;
reconsider I = goto k1 as Element of SCMPDS-Instr ;
reconsider S = s as SCMPDS-State by PBOOLE:155;
A1: Exec (goto k1),s = SCM-Exec-Res I,S by SCMPDS_1:def 25
.= SCM-Chg S,(jump_address S,(I const_INT )) by SCMPDS_1:def 24 ;
I = [i,<*k1*>] ;
then A2: I const_INT = k1 by SCMPDS_1:34;
ex n being Element of NAT st
( n = IC s & ICplusConst s,k1 = abs (n + k1) ) by Def20;
hence (Exec (goto k1),s) . (IC SCMPDS ) = ICplusConst s,k1 by A1, A2, Th6, SCMPDS_1:26; :: thesis: for a being Int_position holds (Exec (goto k1),s) . a = s . a
let a be Int_position ; :: thesis: (Exec (goto k1),s) . a = s . a
reconsider mn = a as Element of SCM-Data-Loc by Def2;
thus (Exec (goto k1),s) . a = S . mn by A1, SCMPDS_1:27
.= s . a ; :: thesis: verum