let a, c be Data-Location ; :: thesis: for loc being Instruction-Location of SCM
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 ) = Next ) & (Exec (a >0_goto loc),s) . c = s . c )
let loc be Instruction-Location of SCM ; :: 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 ) = Next ) & (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 ) = Next ) & (Exec (a >0_goto loc),s) . c = s . c )
reconsider mj = loc as Element of NAT by AMI_1:def 4;
reconsider a' = a 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 ;
reconsider i = 8 as Element of Segm 9 by GR_CY_1:10;
A1: I = [i,<*mj,a'*>] ;
A2: Exec (a >0_goto loc),s = SCM-Exec-Res I,S by AMI_2:def 17
.= SCM-Chg S,(IFGT (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 ) = Next ) & (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 ) = IFGT (S . (I cond_address )),0 ,(I cjump_address ),(succ (IC S)) by A2, Th4, AMI_2:16
.= I cjump_address by A3, XXREAL_0:def 11
.= loc by A1, AMI_2:25 ; :: thesis: verum

end;

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

proof

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

end;

reconsider mn = c as Element of SCM-Data-Loc by Def2;
thus (Exec (a >0_goto loc),s) . c = S . mn by A2, AMI_2:17
.= s . c ; :: thesis: verum