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