let s be State of SCMPDS; :: thesis: for k1 being Integer holds
( (Exec ((goto k1),s)) . (IC ) = 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 ) = 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:44;
reconsider I = goto k1 as Element of SCMPDS-Instr ;
reconsider S = s as SCMPDS-State by CARD_3:107;
A1: Exec ((goto k1),s) = SCM-Exec-Res (I,S) by SCMPDS_1:def 23
.= SCM-Chg (S,(jump_address (S,(I const_INT)))) by SCMPDS_1:def 22 ;
I = [i,{},<*k1*>] ;
then A2: I const_INT = k1 by SCMPDS_1:19;
ex n being Element of NAT st
( n = IC s & ICplusConst (s,k1) = abs (n + k1) ) by Def20;
hence (Exec ((goto k1),s)) . (IC ) = ICplusConst (s,k1) by A1, A2, Th6, SCMPDS_1:13; :: 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:14
.= s . a ; :: thesis: verum