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 ) = (IC s) + 1 ) & (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 ) = (IC s) + 1 ) & (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 ) = (IC s) + 1 ) & (Exec ((a =0_goto loc),s)) . c = s . c )
reconsider mn = c as Element of SCM-Data-Loc by AMI_2:def 16;
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 AMI_2:def 16;
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 15
.= SCM-Chg (S,(IFEQ ((S . (I cond_address)),0,(I cjump_address),((IC S) + 1)))) by A1, AMI_2:def 14 ;
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 ) = (IC s) + 1 ) & (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, SCM_INST:7;
thus (Exec ((a =0_goto loc),s)) . (IC ) = IFEQ ((S . (I cond_address)),0,(I cjump_address),((IC S) + 1)) by A2, Th1, AMI_2:11
.= I cjump_address by A3, FUNCOP_1:def 8
.= loc by A1, SCM_INST:7 ; :: thesis: verum
end;
thus ( s . a <> 0 implies (Exec ((a =0_goto loc),s)) . (IC ) = (IC s) + 1 ) :: thesis: (Exec ((a =0_goto loc),s)) . c = s . c
proof
assume s . a <> 0 ; :: thesis: (Exec ((a =0_goto loc),s)) . (IC ) = (IC s) + 1
then A4: S . (I cond_address) <> 0 by A1, SCM_INST:7;
thus (Exec ((a =0_goto loc),s)) . (IC ) = IFEQ ((S . (I cond_address)),0,(I cjump_address),((IC S) + 1)) by A2, Th1, AMI_2:11
.= (IC s) + 1 by A4, Th1, 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