let a, c be Data-Location ; :: thesis: for loc being Nat
for s being State of SCM holds
( ( s . a = 0 implies (Exec (a =0_goto loc),s) . (IC SCM ) = loc ) & ( s . a <> 0 implies (Exec (a =0_goto loc),s) . (IC SCM ) = succ (IC s) ) & (Exec (a =0_goto loc),s) . c = s . c )
let loc be Nat; :: thesis: for s being State of SCM holds
( ( s . a = 0 implies (Exec (a =0_goto loc),s) . (IC SCM ) = loc ) & ( s . a <> 0 implies (Exec (a =0_goto loc),s) . (IC SCM ) = succ (IC s) ) & (Exec (a =0_goto loc),s) . c = s . c )
let s be State of SCM ; :: thesis: ( ( s . a = 0 implies (Exec (a =0_goto loc),s) . (IC SCM ) = loc ) & ( s . a <> 0 implies (Exec (a =0_goto loc),s) . (IC SCM ) = succ (IC s) ) & (Exec (a =0_goto loc),s) . c = s . c )
reconsider mn = c as Element of SCM-Data-Loc by Def2;
reconsider I = a =0_goto loc as Element of SCM-Instr ;
reconsider S = s as SCM-State by PBOOLE:155;
reconsider i = 7 as Element of Segm 9 by NAT_1:45;
reconsider a9 = a as Element of SCM-Data-Loc by Def2;
reconsider mj = loc as Element of NAT by ORDINAL1:def 13;
A1: I = [i,<*mj,a9*>] ;
A2: Exec (a =0_goto loc),s = SCM-Exec-Res I,S by AMI_2:def 17
.= SCM-Chg S,(IFEQ (S . (I cond_address )),0 ,(I cjump_address ),(succ (IC S))) by A1, AMI_2:def 16 ;
thus ( s . a = 0 implies (Exec (a =0_goto loc),s) . (IC SCM ) = loc ) :: thesis: ( ( s . a <> 0 implies (Exec (a =0_goto loc),s) . (IC SCM ) = succ (IC s) ) & (Exec (a =0_goto loc),s) . c = s . c )

proof

assume s . a = 0 ; :: thesis: (Exec (a =0_goto loc),s) . (IC SCM ) = loc
then A3: S . (I cond_address ) = 0 by A1, AMI_2:25;
thus (Exec (a =0_goto loc),s) . (IC SCM ) = IFEQ (S . (I cond_address )),0 ,(I cjump_address ),(succ (IC S)) by A2, Th4, AMI_2:16
.= I cjump_address by A3, FUNCOP_1:def 8
.= loc by A1, AMI_2:25 ; :: thesis: verum

end;

thus ( s . a <> 0 implies (Exec (a =0_goto loc),s) . (IC SCM ) = succ (IC s) ) :: thesis: (Exec (a =0_goto loc),s) . c = s . c

proof

assume s . a <> 0 ; :: thesis: (Exec (a =0_goto loc),s) . (IC SCM ) = succ (IC s)
then A4: S . (I cond_address ) <> 0 by A1, AMI_2:25;
thus (Exec (a =0_goto loc),s) . (IC SCM ) = IFEQ (S . (I cond_address )),0 ,(I cjump_address ),(succ (IC S)) by A2, Th4, AMI_2:16
.= succ (IC s) by A4, Th4, FUNCOP_1:def 8 ; :: thesis: verum

end;

thus (Exec (a =0_goto loc),s) . c = S . mn by A2, AMI_2:17
.= s . c ; :: thesis: verum