let c be Data-Location ; :: thesis: for loc being Nat
for s being State of SCM holds
( (Exec (SCM-goto loc),s) . (IC SCM ) = 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 SCM ) = loc & (Exec (SCM-goto loc),s) . c = s . c )
let s be State of SCM ; :: thesis: ( (Exec (SCM-goto loc),s) . (IC SCM ) = loc & (Exec (SCM-goto loc),s) . c = s . c )
reconsider mn = c as Element of SCM-Data-Loc by Def2;
reconsider mj = loc as Element of NAT by ORDINAL1:def 13;
reconsider I = SCM-goto loc as Element of SCM-Instr ;
reconsider S = s as SCM-State by PBOOLE:155;
reconsider i = 6 as Element of Segm 9 by NAT_1:45;
A1: I = [i,<*mj*>,{} ] ;
A2: Exec (SCM-goto loc),s = SCM-Exec-Res I,S by AMI_2:def 17
.= SCM-Chg S,(I jump_address ) by A1, AMI_2:def 16 ;
I jump_address = mj by A1, AMI_2:24;
hence (Exec (SCM-goto loc),s) . (IC SCM ) = loc by A2, Th4, AMI_2:16; :: thesis: (Exec (SCM-goto loc),s) . c = s . c
thus (Exec (SCM-goto loc),s) . c = S . mn by A2, AMI_2:17
.= s . c ; :: thesis: verum