let s be State of SCMPDS; 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; ( (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; for a being Int_position holds (Exec ((goto k1),s)) . a = s . a
let a be Int_position; (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
; verum