let s be State of SCM ; for i being Instruction of SCM
for l being Element of NAT holds (Exec i,s) . l = s . l
let i be Instruction of SCM ; for l being Element of NAT holds (Exec i,s) . l = s . l
let l be Element of NAT ; (Exec i,s) . l = s . l
reconsider c = i as Element of SCM-Instr ;
reconsider S = s as Element of product SCM-OK by PBOOLE:155;
reconsider l9 = l as Element of NAT ;
( c in ({[SCM-Halt ,{} ,{} ]} \/ { [Y,<*a2*>,{} ] where Y is Element of Segm 9, a2 is Element of NAT : Y = 6 } ) \/ { [K,<*a1*>,<*b1*>] where K is Element of Segm 9, a1 is Element of NAT , b1 is Element of SCM-Data-Loc : K in {7,8} } or c in { [T,{} ,<*b2,c1*>] where T is Element of Segm 9, b2, c1 is Element of SCM-Data-Loc : T in {1,2,3,4,5} } )
by XBOOLE_0:def 3;
then A1:
( c in {[SCM-Halt ,{} ,{} ]} \/ { [Y,<*a2*>,{} ] where Y is Element of Segm 9, a2 is Element of NAT : Y = 6 } or c in { [K,<*a1*>,<*b1*>] where K is Element of Segm 9, a1 is Element of NAT , b1 is Element of SCM-Data-Loc : K in {7,8} } or c in { [T,{} ,<*b2,c1*>] where T is Element of Segm 9, b2, c1 is Element of SCM-Data-Loc : T in {1,2,3,4,5} } )
by XBOOLE_0:def 3;
now per cases
( c in {[SCM-Halt ,{} ,{} ]} or c in { [Y,<*a2*>,{} ] where Y is Element of Segm 9, a2 is Element of NAT : Y = 6 } or c in { [K,<*a1*>,<*b1*>] where K is Element of Segm 9, a1 is Element of NAT , b1 is Element of SCM-Data-Loc : K in {7,8} } or c in { [T,{} ,<*b2,c1*>] where T is Element of Segm 9, b2, c1 is Element of SCM-Data-Loc : T in {1,2,3,4,5} } )
by A1, XBOOLE_0:def 3;
case
c in {[SCM-Halt ,{} ,{} ]}
;
(SCM-Exec-Res c,S) . l9 = S . l9then
c = [SCM-Halt ,{} ,{} ]
by TARSKI:def 1;
then A2:
(
c `3_3 = {} &
c `2_3 = {} )
by RECDEF_2:def 2, RECDEF_2:def 3;
then A3:
( ( for
mk,
ml being
Element of
SCM-Data-Loc holds not
c = [3,{} ,<*mk,ml*>] ) & ( for
mk,
ml being
Element of
SCM-Data-Loc holds not
c = [4,{} ,<*mk,ml*>] ) )
by RECDEF_2:def 3;
A4:
( ( for
mk being
Element of
NAT for
ml being
Element of
SCM-Data-Loc holds not
c = [7,<*mk*>,<*ml*>] ) & ( for
mk being
Element of
NAT for
ml being
Element of
SCM-Data-Loc holds not
c = [8,<*mk*>,<*ml*>] ) )
by A2, RECDEF_2:def 3;
A5:
( ( for
mk,
ml being
Element of
SCM-Data-Loc holds not
c = [5,{} ,<*mk,ml*>] ) & ( for
mk being
Element of
NAT holds not
c = [6,<*mk*>,{} ] ) )
by A2, RECDEF_2:def 2, RECDEF_2:def 3;
( ( for
mk,
ml being
Element of
SCM-Data-Loc holds not
c = [1,{} ,<*mk,ml*>] ) & ( for
mk,
ml being
Element of
SCM-Data-Loc holds not
c = [2,{} ,<*mk,ml*>] ) )
by A2, RECDEF_2:def 3;
hence
(SCM-Exec-Res c,S) . l9 = S . l9
by A3, A5, A4, AMI_2:def 16;
verum end; case
c in { [T,{} ,<*b2,c1*>] where T is Element of Segm 9, b2, c1 is Element of SCM-Data-Loc : T in {1,2,3,4,5} }
;
(SCM-Exec-Res c,S) . l9 = S . l9then consider T being
Element of
Segm 9,
b2,
c1 being
Element of
SCM-Data-Loc such that A8:
c = [T,{} ,<*b2,c1*>]
and A9:
T in {1,2,3,4,5}
;
now per cases
( T = 1 or T = 2 or T = 3 or T = 4 or T = 5 )
by A9, ENUMSET1:def 3;
case
T = 5
;
(SCM-Exec-Res c,S) . l9 = S . l9hence (SCM-Exec-Res c,S) . l9 =
(SCM-Chg (SCM-Chg (SCM-Chg S,(c address_1 ),((S . (c address_1 )) div (S . (c address_2 )))),(c address_2 ),((S . (c address_1 )) mod (S . (c address_2 )))),(succ (IC S))) . l9
by A8, AMI_2:def 16
.=
(SCM-Chg (SCM-Chg S,(c address_1 ),((S . (c address_1 )) div (S . (c address_2 )))),(c address_2 ),((S . (c address_1 )) mod (S . (c address_2 )))) . l9
by AMI_2:18
.=
(SCM-Chg S,(c address_1 ),((S . (c address_1 )) div (S . (c address_2 )))) . l9
by AMI_2:22
.=
S . l9
by AMI_2:22
;
verum end; hence
(SCM-Exec-Res c,S) . l9 = S . l9
;
verum end;
hence
(Exec i,s) . l = s . l
by AMI_2:def 17; verum