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 ) = loc ) & ( s . a <> 0 implies (Exec ((a =0_goto loc),s)) . (IC ) = 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 ) = loc ) & ( s . a <> 0 implies (Exec ((a =0_goto loc),s)) . (IC ) = 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 ) = loc ) & ( s . a <> 0 implies (Exec ((a =0_goto loc),s)) . (IC ) = 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 CARD_3:107;
reconsider i = 7 as Element of Segm 9 by NAT_1:44;
reconsider a9 = a as Element of SCM-Data-Loc by Def2;
reconsider mj = loc as Element of NAT by ORDINAL1:def 12;
A1: I = [i,<*mj*>,<*a9*>] ;
A2: Exec ((a =0_goto loc),s) = SCM-Exec-Res (I,S) by AMI_2:def 14
.= SCM-Chg (S,(IFEQ ((S . (I cond_address)),0,(I cjump_address),(succ (IC S))))) by A1, AMI_2:def 13 ;
thus ( s . a = 0 implies (Exec ((a =0_goto loc),s)) . (IC ) = loc ) :: thesis: ( ( s . a <> 0 implies (Exec ((a =0_goto loc),s)) . (IC ) = 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 ) = loc
then A3: S . (I cond_address) = 0 by A1, AMI_2:19;
thus (Exec ((a =0_goto loc),s)) . (IC ) = IFEQ ((S . (I cond_address)),0,(I cjump_address),(succ (IC S))) by A2, Th4, AMI_2:11
.= I cjump_address by A3, FUNCOP_1:def 8
.= loc by A1, AMI_2:19 ; :: thesis: verum

end;

thus ( s . a <> 0 implies (Exec ((a =0_goto loc),s)) . (IC ) = 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 ) = succ (IC s)
then A4: S . (I cond_address) <> 0 by A1, AMI_2:19;
thus (Exec ((a =0_goto loc),s)) . (IC ) = IFEQ ((S . (I cond_address)),0,(I cjump_address),(succ (IC S))) by A2, Th4, AMI_2:11
.= 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:12
.= s . c ; :: thesis: verum