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 = goto k1 as Element of SCMPDS-Instr ;
reconsider S = s as SCMPDS-State ;
reconsider i = 0 as Element of Segm 14 by GR_CY_1:10;
A1: I = [i,<*k1*>] ;
A2: 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 ;
A3: I const_INT = k1 by A1, SCMPDS_1:34;
consider n being Element of NAT such that
A4: ( n = IC s & ICplusConst s,k1 = abs (n + k1) ) by Def20;
thus (Exec (goto k1),s) . (IC SCMPDS ) = ICplusConst s,k1 by A2, A3, A4, 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 A2, SCMPDS_1:27
.= s . a ; :: thesis: verum