let c be Data-Location; :: thesis: for loc being Nat
for s being State of SCM holds
( (Exec ((SCM-goto loc),s)) . (IC ) = loc & (Exec ((SCM-goto loc),s)) . c = s . c )
let loc be Nat; :: thesis: for s being State of SCM holds
( (Exec ((SCM-goto loc),s)) . (IC ) = loc & (Exec ((SCM-goto loc),s)) . c = s . c )
let s be State of SCM; :: thesis: ( (Exec ((SCM-goto loc),s)) . (IC ) = loc & (Exec ((SCM-goto loc),s)) . c = s . c )
reconsider mn = c as Element of SCM-Data-Loc by AMI_2:def 16;
reconsider mj = loc as Element of NAT by ORDINAL1:def 12;
reconsider I = SCM-goto loc as Element of SCM-Instr ;
reconsider S = s as SCM-State by CARD_3:107;
reconsider i = 6 as Element of Segm 9 by NAT_1:44;
A1: I = [i,<*mj*>,{}] ;
A2: Exec ((SCM-goto loc),s) = SCM-Exec-Res (I,S) by AMI_2:def 15
.= SCM-Chg (S,(I jump_address)) by AMI_2:def 14 ;
I jump_address = mj by A1, SCM_INST:6;
hence (Exec ((SCM-goto loc),s)) . (IC ) = loc by A2, Th1, AMI_2:11; :: thesis: (Exec ((SCM-goto loc),s)) . c = s . c
thus (Exec ((SCM-goto loc),s)) . c = S . mn by A2, AMI_2:12
.= s . c ; :: thesis: verum