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 = 14 as Element of Segm 15 by NAT_1:44;
reconsider I = goto k1 as Element of SCMPDS-Instr ;
reconsider S = s as SCM-State by CARD_3:107;
I = [i,{},<*k1*>] ;
then A1: I const_INT = k1 by SCMPDS_I:4;
A2: InsCode I = 14 ;
A3: Exec ((goto k1),s) = SCM-Exec-Res (I,S) by SCMPDS_1:def 23
.= SCM-Chg (S,(jump_address (S,(I const_INT)))) by A2, SCMPDS_1:def 22 ;
ex n being Element of NAT st
( n = IC s & ICplusConst (s,k1) = |.(n + k1).| ) by Def17;
hence (Exec ((goto k1),s)) . (IC ) = ICplusConst (s,k1) by A3, A1, Th1, AMI_2:11; :: 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 AMI_2:def 16;
thus (Exec ((goto k1),s)) . a = S . mn by A3, AMI_2:12
.= s . a ; :: thesis: verum