let a, c be Data-Location; 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; 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; ( ( 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 = 8 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 Nat ;
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,(IFGT ((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 )
( ( 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
;
(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 ) =
IFGT (
(S . (I cond_address)),
0,
(I cjump_address),
((IC S) + 1))
by A2, Th1, AMI_2:11
.=
I cjump_address
by A3, XXREAL_0:def 11
.=
loc
by A1, SCM_INST:7
;
verum
end;
thus
( s . a <= 0 implies (Exec ((a >0_goto loc),s)) . (IC ) = (IC s) + 1 )
(Exec ((a >0_goto loc),s)) . c = s . cproof
assume
s . a <= 0
;
(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 ) =
IFGT (
(S . (I cond_address)),
0,
(I cjump_address),
((IC S) + 1))
by A2, Th1, AMI_2:11
.=
(IC s) + 1
by A4, Th1, XXREAL_0:def 11
;
verum
end;
thus (Exec ((a >0_goto loc),s)) . c =
S . mn
by A2, AMI_2:12
.=
s . c
; verum