:: On a Mathematical Model of Programs
:: by Yatsuka Nakamura and Andrzej Trybulec
::
:: Received December 29, 1992
:: Copyright (c) 1992-2011 Association of Mizar Users

begin

notation

synonym SCM-Halt for {} ;

end;

definition

:: original: SCM-Halt
redefine func SCM-Halt -> Element of Segm 9;
correctness
coherence
SCM-Halt is Element of Segm 9;
by NAT_1:45;

end;

definition

func SCM-Data-Loc -> set equals :: AMI_2:def 1
[:{1},NAT:];
coherence
[:{1},NAT:] is set ;

end;

:: deftheorem defines SCM-Data-Loc AMI_2:def 1 :
SCM-Data-Loc = [:{1},NAT:];

definition

canceled;
func SCM-Memory -> set equals :: AMI_2:def 3
({NAT} \/ SCM-Data-Loc) \/ NAT;
coherence
({NAT} \/ SCM-Data-Loc) \/ NAT is set ;

end;

:: deftheorem AMI_2:def 2 :
canceled;

:: deftheorem defines SCM-Memory AMI_2:def 3 :
SCM-Memory = ({NAT} \/ SCM-Data-Loc) \/ NAT;

registration

cluster SCM-Memory -> non empty ;
coherence
not SCM-Memory is empty ;

end;

definition

:: original: SCM-Data-Loc
redefine func SCM-Data-Loc -> Subset of SCM-Memory;
coherence
SCM-Data-Loc is Subset of SCM-Memory

proof end;

end;

registration

cluster SCM-Data-Loc -> non empty ;
coherence
not SCM-Data-Loc is empty ;

end;

definition

func SCM-Instr -> non empty set equals :: AMI_2:def 4
(({[SCM-Halt,{},{}]} \/ { [J,<*a*>,{}] where J is Element of Segm 9, a is Element of NAT : J = 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} } ) \/ { [I,{},<*b,c*>] where I is Element of Segm 9, b, c is Element of SCM-Data-Loc : I in {1,2,3,4,5} } ;
coherence
(({[SCM-Halt,{},{}]} \/ { [J,<*a*>,{}] where J is Element of Segm 9, a is Element of NAT : J = 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} } ) \/ { [I,{},<*b,c*>] where I is Element of Segm 9, b, c is Element of SCM-Data-Loc : I in {1,2,3,4,5} } is non empty set ;

end;

:: deftheorem defines SCM-Instr AMI_2:def 4 :
SCM-Instr = (({[SCM-Halt,{},{}]} \/ { [J,<*a*>,{}] where J is Element of Segm 9, a is Element of NAT : J = 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} } ) \/ { [I,{},<*b,c*>] where I is Element of Segm 9, b, c is Element of SCM-Data-Loc : I in {1,2,3,4,5} } ;

theorem :: AMI_2:1

canceled;

theorem :: AMI_2:2

[0,{},{}] in SCM-Instr

proof end;

registration

cluster SCM-Instr -> non empty ;
coherence
not SCM-Instr is empty ;

end;

theorem :: AMI_2:3

for a2 being Element of NAT holds [6,<*a2*>,{}] in SCM-Instr

proof end;

theorem :: AMI_2:4

for x being set
for a2 being Element of NAT
for b2 being Element of SCM-Data-Loc st x in {7,8} holds
[x,<*a2*>,<*b2*>] in SCM-Instr

proof end;

theorem :: AMI_2:5

for x being set
for b1, c1 being Element of SCM-Data-Loc st x in {1,2,3,4,5} holds
[x,{},<*b1,c1*>] in SCM-Instr

proof end;

Lm1: now

let k be Element of SCM-Memory ; :: thesis: ( k = NAT or k in SCM-Data-Loc or k in NAT )
( k in {NAT} \/ SCM-Data-Loc or k in NAT ) by XBOOLE_0:def 3;
then ( k in {NAT} or k in SCM-Data-Loc or k in NAT ) by XBOOLE_0:def 3;
hence ( k = NAT or k in SCM-Data-Loc or k in NAT ) by TARSKI:def 1; :: thesis: verum

end;

Lm2: not NAT in SCM-Data-Loc

proof end;

Lm3: SCM-Data-Loc misses NAT

proof end;

definition

func SCM-OK -> Function of SCM-Memory,({INT} \/ {SCM-Instr,NAT}) means :Def5: :: AMI_2:def 5
for k being Element of SCM-Memory holds
( ( k = NAT implies it . k = NAT ) & ( k in SCM-Data-Loc implies it . k = INT ) & ( k in NAT implies it . k = SCM-Instr ) );
existence
ex b₁ being Function of SCM-Memory,({INT} \/ {SCM-Instr,NAT}) st
for k being Element of SCM-Memory holds
( ( k = NAT implies b₁ . k = NAT ) & ( k in SCM-Data-Loc implies b₁ . k = INT ) & ( k in NAT implies b₁ . k = SCM-Instr ) )

proof end;

uniqueness
for b₁, b₂ being Function of SCM-Memory,({INT} \/ {SCM-Instr,NAT}) st ( for k being Element of SCM-Memory holds
( ( k = NAT implies b₁ . k = NAT ) & ( k in SCM-Data-Loc implies b₁ . k = INT ) & ( k in NAT implies b₁ . k = SCM-Instr ) ) ) & ( for k being Element of SCM-Memory holds
( ( k = NAT implies b₂ . k = NAT ) & ( k in SCM-Data-Loc implies b₂ . k = INT ) & ( k in NAT implies b₂ . k = SCM-Instr ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def5 defines SCM-OK AMI_2:def 5 :
for b₁ being Function of SCM-Memory,({INT} \/ {SCM-Instr,NAT}) holds
( b₁ = SCM-OK iff for k being Element of SCM-Memory holds
( ( k = NAT implies b₁ . k = NAT ) & ( k in SCM-Data-Loc implies b₁ . k = INT ) & ( k in NAT implies b₁ . k = SCM-Instr ) ) );

registration

let x, y, z be set ;
cluster [x,y,z] -> finite ;
coherence
[x,y,z] is finite ;

end;

registration

let x, y, z be set ;
cluster [x,y,z] -> non natural ;
coherence
not [x,y,z] is natural ;

end;

theorem Th6: :: AMI_2:6

( SCM-Instr <> INT & NAT <> SCM-Instr )

proof end;

theorem Th7: :: AMI_2:7

for i being Element of SCM-Memory holds
( SCM-OK . i = NAT iff i = NAT )

proof end;

theorem Th8: :: AMI_2:8

for i being Element of SCM-Memory holds
( SCM-OK . i = INT iff i in SCM-Data-Loc )

proof end;

theorem Th9: :: AMI_2:9

for i being Element of SCM-Memory holds
( SCM-OK . i = SCM-Instr iff i in NAT )

proof end;

definition

mode SCM-State is Element of product SCM-OK;

end;

theorem :: AMI_2:10

for a being Element of SCM-Data-Loc holds SCM-OK . a = INT by Th8;

Lm4: NAT c= SCM-Memory
by XBOOLE_1:7;

theorem :: AMI_2:11

for a being Element of NAT holds SCM-OK . a = SCM-Instr

proof end;

theorem :: AMI_2:12

for a being Element of NAT
for t being Element of SCM-Data-Loc holds a <> t

proof end;

Lm5: NAT in SCM-Memory

proof end;

theorem Th13: :: AMI_2:13

pi ((product SCM-OK),NAT) = NAT

proof end;

theorem Th14: :: AMI_2:14

for a being Element of SCM-Data-Loc holds pi ((product SCM-OK),a) = INT

proof end;

theorem :: AMI_2:15

for a being Element of NAT holds pi ((product SCM-OK),a) = SCM-Instr

proof end;

definition

let s be SCM-State;
func IC s -> Element of NAT equals :: AMI_2:def 6
s . NAT;
coherence
s . NAT is Element of NAT by Th13, CARD_3:def 6;

end;

:: deftheorem defines IC AMI_2:def 6 :
for s being SCM-State holds IC s = s . NAT;

definition

let s be SCM-State;
let u be Nat;
func SCM-Chg (s,u) -> SCM-State equals :: AMI_2:def 7
s +* (NAT .--> u);
coherence
s +* (NAT .--> u) is SCM-State

proof end;

end;

:: deftheorem defines SCM-Chg AMI_2:def 7 :
for s being SCM-State
for u being Nat holds SCM-Chg (s,u) = s +* (NAT .--> u);

theorem :: AMI_2:16

for s being SCM-State
for u being Nat holds (SCM-Chg (s,u)) . NAT = u

proof end;

theorem :: AMI_2:17

for s being SCM-State
for u being Nat
for mk being Element of SCM-Data-Loc holds (SCM-Chg (s,u)) . mk = s . mk

proof end;

theorem :: AMI_2:18

for s being SCM-State
for u, v being Nat holds (SCM-Chg (s,u)) . v = s . v

proof end;

definition

let s be SCM-State;
let t be Element of SCM-Data-Loc ;
let u be Integer;
func SCM-Chg (s,t,u) -> SCM-State equals :: AMI_2:def 8
s +* (t .--> u);
coherence
s +* (t .--> u) is SCM-State

proof end;

end;

:: deftheorem defines SCM-Chg AMI_2:def 8 :
for s being SCM-State
for t being Element of SCM-Data-Loc
for u being Integer holds SCM-Chg (s,t,u) = s +* (t .--> u);

theorem :: AMI_2:19

for s being SCM-State
for t being Element of SCM-Data-Loc
for u being Integer holds (SCM-Chg (s,t,u)) . NAT = s . NAT

proof end;

theorem :: AMI_2:20

for s being SCM-State
for t being Element of SCM-Data-Loc
for u being Integer holds (SCM-Chg (s,t,u)) . t = u

proof end;

theorem :: AMI_2:21

for s being SCM-State
for t being Element of SCM-Data-Loc
for u being Integer
for mk being Element of SCM-Data-Loc st mk <> t holds
(SCM-Chg (s,t,u)) . mk = s . mk

proof end;

theorem :: AMI_2:22

for s being SCM-State
for t being Element of SCM-Data-Loc
for u being Integer
for v being Element of NAT holds (SCM-Chg (s,t,u)) . v = s . v

proof end;

definition

let x be Element of SCM-Instr ;
given mk, ml being Element of SCM-Data-Loc , I being Element of Segm 9 such that A1: x = [I,{},<*mk,ml*>] ;
func x address_1 -> Element of SCM-Data-Loc means :Def9: :: AMI_2:def 9
ex f being FinSequence of SCM-Data-Loc st
( f = x `3_3 & it = f /. 1 );
existence
ex b<sub>1</sub> being Element of SCM-Data-Loc ex f being FinSequence of SCM-Data-Loc st
( f = x `3_3 & b₁ = f /. 1 )

proof end;

uniqueness
for b₁, b₂ being Element of SCM-Data-Loc st ex f being FinSequence of SCM-Data-Loc st
( f = x `3_3 & b<sub>1</sub> = f /. 1 ) & ex f being FinSequence of SCM-Data-Loc st
( f = x `3_3 & b₂ = f /. 1 ) holds
b₁ = b₂ ;
func x address_2 -> Element of SCM-Data-Loc means :Def10: :: AMI_2:def 10
ex f being FinSequence of SCM-Data-Loc st
( f = x `3_3 & it = f /. 2 );
existence
ex b<sub>1</sub> being Element of SCM-Data-Loc ex f being FinSequence of SCM-Data-Loc st
( f = x `3_3 & b₁ = f /. 2 )

proof end;

correctness
uniqueness
for b₁, b₂ being Element of SCM-Data-Loc st ex f being FinSequence of SCM-Data-Loc st
( f = x `3_3 & b<sub>1</sub> = f /. 2 ) & ex f being FinSequence of SCM-Data-Loc st
( f = x `3_3 & b₂ = f /. 2 ) holds
b₁ = b₂;
;

end;

:: deftheorem Def9 defines address_1 AMI_2:def 9 :
for x being Element of SCM-Instr st ex mk, ml being Element of SCM-Data-Loc ex I being Element of Segm 9 st x = [I,{},<*mk,ml*>] holds
for b₂ being Element of SCM-Data-Loc holds
( b₂ = x address_1 iff ex f being FinSequence of SCM-Data-Loc st
( f = x `3_3 & b₂ = f /. 1 ) );

:: deftheorem Def10 defines address_2 AMI_2:def 10 :
for x being Element of SCM-Instr st ex mk, ml being Element of SCM-Data-Loc ex I being Element of Segm 9 st x = [I,{},<*mk,ml*>] holds
for b₂ being Element of SCM-Data-Loc holds
( b₂ = x address_2 iff ex f being FinSequence of SCM-Data-Loc st
( f = x `3_3 & b₂ = f /. 2 ) );

theorem :: AMI_2:23

for x being Element of SCM-Instr
for mk, ml being Element of SCM-Data-Loc
for I being Element of Segm 9 st x = [I,{},<*mk,ml*>] holds
( x address_1 = mk & x address_2 = ml )

proof end;

definition

let x be Element of SCM-Instr ;
given mk being Element of NAT , I being Element of Segm 9 such that A1: x = [I,<*mk*>,{}] ;
func x jump_address -> Element of NAT means :Def11: :: AMI_2:def 11
ex f being FinSequence of NAT st
( f = x `2_3 & it = f /. 1 );
existence
ex b<sub>1</sub> being Element of NAT ex f being FinSequence of NAT st
( f = x `2_3 & b₁ = f /. 1 )

proof end;

correctness
uniqueness
for b₁, b₂ being Element of NAT st ex f being FinSequence of NAT st
( f = x `2_3 & b<sub>1</sub> = f /. 1 ) & ex f being FinSequence of NAT st
( f = x `2_3 & b₂ = f /. 1 ) holds
b₁ = b₂;
;

end;

:: deftheorem Def11 defines jump_address AMI_2:def 11 :
for x being Element of SCM-Instr st ex mk being Element of NAT ex I being Element of Segm 9 st x = [I,<*mk*>,{}] holds
for b₂ being Element of NAT holds
( b₂ = x jump_address iff ex f being FinSequence of NAT st
( f = x `2_3 & b₂ = f /. 1 ) );

theorem :: AMI_2:24

for x being Element of SCM-Instr
for mk being Element of NAT
for I being Element of Segm 9 st x = [I,<*mk*>,{}] holds
x jump_address = mk

proof end;

definition

let x be Element of SCM-Instr ;
given mk being Element of NAT , ml being Element of SCM-Data-Loc , I being Element of Segm 9 such that A1: x = [I,<*mk*>,<*ml*>] ;
func x cjump_address -> Element of NAT means :Def12: :: AMI_2:def 12
ex mk being Element of NAT st
( <*mk*> = x `2_3 & it = <*mk*> /. 1 );
existence
ex b<sub>1</sub>, mk being Element of NAT st
( <*mk*> = x `2_3 & b₁ = <*mk*> /. 1 )

proof end;

correctness
uniqueness
for b₁, b₂ being Element of NAT st ex mk being Element of NAT st
( <*mk*> = x `2_3 & b<sub>1</sub> = <*mk*> /. 1 ) & ex mk being Element of NAT st
( <*mk*> = x `2_3 & b₂ = <*mk*> /. 1 ) holds
b₁ = b₂;
;
func x cond_address -> Element of SCM-Data-Loc means :Def13: :: AMI_2:def 13
ex ml being Element of SCM-Data-Loc st
( <*ml*> = x `3_3 & it = <*ml*> /. 1 );
existence
ex b<sub>1</sub>, ml being Element of SCM-Data-Loc st
( <*ml*> = x `3_3 & b₁ = <*ml*> /. 1 )

proof end;

correctness
uniqueness
for b₁, b₂ being Element of SCM-Data-Loc st ex ml being Element of SCM-Data-Loc st
( <*ml*> = x `3_3 & b<sub>1</sub> = <*ml*> /. 1 ) & ex ml being Element of SCM-Data-Loc st
( <*ml*> = x `3_3 & b₂ = <*ml*> /. 1 ) holds
b₁ = b₂;
;

end;

:: deftheorem Def12 defines cjump_address AMI_2:def 12 :
for x being Element of SCM-Instr st ex mk being Element of NAT ex ml being Element of SCM-Data-Loc ex I being Element of Segm 9 st x = [I,<*mk*>,<*ml*>] holds
for b₂ being Element of NAT holds
( b₂ = x cjump_address iff ex mk being Element of NAT st
( <*mk*> = x `2_3 & b₂ = <*mk*> /. 1 ) );

:: deftheorem Def13 defines cond_address AMI_2:def 13 :
for x being Element of SCM-Instr st ex mk being Element of NAT ex ml being Element of SCM-Data-Loc ex I being Element of Segm 9 st x = [I,<*mk*>,<*ml*>] holds
for b₂ being Element of SCM-Data-Loc holds
( b₂ = x cond_address iff ex ml being Element of SCM-Data-Loc st
( <*ml*> = x `3_3 & b₂ = <*ml*> /. 1 ) );

theorem :: AMI_2:25

for x being Element of SCM-Instr
for mk being Element of NAT
for ml being Element of SCM-Data-Loc
for I being Element of Segm 9 st x = [I,<*mk*>,<*ml*>] holds
( x cjump_address = mk & x cond_address = ml )

proof end;

registration

let s be SCM-State;
let a be Element of SCM-Data-Loc ;
cluster s . a -> integer ;
coherence
s . a is integer

proof end;

end;

definition

canceled;
canceled;
let x be Element of SCM-Instr ;
let s be SCM-State;
func SCM-Exec-Res (x,s) -> SCM-State equals :: AMI_2:def 16
SCM-Chg ((SCM-Chg (s,(x address_1),(s . (x address_2)))),(succ (IC s))) if ex mk, ml being Element of SCM-Data-Loc st x = [1,{},<*mk,ml*>]
SCM-Chg ((SCM-Chg (s,(x address_1),((s . (x address_1)) + (s . (x address_2))))),(succ (IC s))) if ex mk, ml being Element of SCM-Data-Loc st x = [2,{},<*mk,ml*>]
SCM-Chg ((SCM-Chg (s,(x address_1),((s . (x address_1)) - (s . (x address_2))))),(succ (IC s))) if ex mk, ml being Element of SCM-Data-Loc st x = [3,{},<*mk,ml*>]
SCM-Chg ((SCM-Chg (s,(x address_1),((s . (x address_1)) * (s . (x address_2))))),(succ (IC s))) if ex mk, ml being Element of SCM-Data-Loc st x = [4,{},<*mk,ml*>]
SCM-Chg ((SCM-Chg ((SCM-Chg (s,(x address_1),((s . (x address_1)) div (s . (x address_2))))),(x address_2),((s . (x address_1)) mod (s . (x address_2))))),(succ (IC s))) if ex mk, ml being Element of SCM-Data-Loc st x = [5,{},<*mk,ml*>]
SCM-Chg (s,(x jump_address)) if ex mk being Element of NAT st x = [6,<*mk*>,{}]
SCM-Chg (s,(IFEQ ((s . (x cond_address)),0,(x cjump_address),(succ (IC s))))) if ex mk being Element of NAT ex ml being Element of SCM-Data-Loc st x = [7,<*mk*>,<*ml*>]
SCM-Chg (s,(IFGT ((s . (x cond_address)),0,(x cjump_address),(succ (IC s))))) if ex mk being Element of NAT ex ml being Element of SCM-Data-Loc st x = [8,<*mk*>,<*ml*>]
otherwise s;
consistency
for b₁ being SCM-State holds
( ( ex mk, ml being Element of SCM-Data-Loc st x = [1,{},<*mk,ml*>] & ex mk, ml being Element of SCM-Data-Loc st x = [2,{},<*mk,ml*>] implies ( b₁ = SCM-Chg ((SCM-Chg (s,(x address_1),(s . (x address_2)))),(succ (IC s))) iff b₁ = SCM-Chg ((SCM-Chg (s,(x address_1),((s . (x address_1)) + (s . (x address_2))))),(succ (IC s))) ) ) & ( ex mk, ml being Element of SCM-Data-Loc st x = [1,{},<*mk,ml*>] & ex mk, ml being Element of SCM-Data-Loc st x = [3,{},<*mk,ml*>] implies ( b₁ = SCM-Chg ((SCM-Chg (s,(x address_1),(s . (x address_2)))),(succ (IC s))) iff b₁ = SCM-Chg ((SCM-Chg (s,(x address_1),((s . (x address_1)) - (s . (x address_2))))),(succ (IC s))) ) ) & ( ex mk, ml being Element of SCM-Data-Loc st x = [1,{},<*mk,ml*>] & ex mk, ml being Element of SCM-Data-Loc st x = [4,{},<*mk,ml*>] implies ( b₁ = SCM-Chg ((SCM-Chg (s,(x address_1),(s . (x address_2)))),(succ (IC s))) iff b₁ = SCM-Chg ((SCM-Chg (s,(x address_1),((s . (x address_1)) * (s . (x address_2))))),(succ (IC s))) ) ) & ( ex mk, ml being Element of SCM-Data-Loc st x = [1,{},<*mk,ml*>] & ex mk, ml being Element of SCM-Data-Loc st x = [5,{},<*mk,ml*>] implies ( b₁ = SCM-Chg ((SCM-Chg (s,(x address_1),(s . (x address_2)))),(succ (IC s))) iff b₁ = SCM-Chg ((SCM-Chg ((SCM-Chg (s,(x address_1),((s . (x address_1)) div (s . (x address_2))))),(x address_2),((s . (x address_1)) mod (s . (x address_2))))),(succ (IC s))) ) ) & ( ex mk, ml being Element of SCM-Data-Loc st x = [1,{},<*mk,ml*>] & ex mk being Element of NAT st x = [6,<*mk*>,{}] implies ( b₁ = SCM-Chg ((SCM-Chg (s,(x address_1),(s . (x address_2)))),(succ (IC s))) iff b₁ = SCM-Chg (s,(x jump_address)) ) ) & ( ex mk, ml being Element of SCM-Data-Loc st x = [1,{},<*mk,ml*>] & ex mk being Element of NAT ex ml being Element of SCM-Data-Loc st x = [7,<*mk*>,<*ml*>] implies ( b₁ = SCM-Chg ((SCM-Chg (s,(x address_1),(s . (x address_2)))),(succ (IC s))) iff b₁ = SCM-Chg (s,(IFEQ ((s . (x cond_address)),0,(x cjump_address),(succ (IC s))))) ) ) & ( ex mk, ml being Element of SCM-Data-Loc st x = [1,{},<*mk,ml*>] & ex mk being Element of NAT ex ml being Element of SCM-Data-Loc st x = [8,<*mk*>,<*ml*>] implies ( b₁ = SCM-Chg ((SCM-Chg (s,(x address_1),(s . (x address_2)))),(succ (IC s))) iff b₁ = SCM-Chg (s,(IFGT ((s . (x cond_address)),0,(x cjump_address),(succ (IC s))))) ) ) & ( ex mk, ml being Element of SCM-Data-Loc st x = [2,{},<*mk,ml*>] & ex mk, ml being Element of SCM-Data-Loc st x = [3,{},<*mk,ml*>] implies ( b₁ = SCM-Chg ((SCM-Chg (s,(x address_1),((s . (x address_1)) + (s . (x address_2))))),(succ (IC s))) iff b₁ = SCM-Chg ((SCM-Chg (s,(x address_1),((s . (x address_1)) - (s . (x address_2))))),(succ (IC s))) ) ) & ( ex mk, ml being Element of SCM-Data-Loc st x = [2,{},<*mk,ml*>] & ex mk, ml being Element of SCM-Data-Loc st x = [4,{},<*mk,ml*>] implies ( b₁ = SCM-Chg ((SCM-Chg (s,(x address_1),((s . (x address_1)) + (s . (x address_2))))),(succ (IC s))) iff b₁ = SCM-Chg ((SCM-Chg (s,(x address_1),((s . (x address_1)) * (s . (x address_2))))),(succ (IC s))) ) ) & ( ex mk, ml being Element of SCM-Data-Loc st x = [2,{},<*mk,ml*>] & ex mk, ml being Element of SCM-Data-Loc st x = [5,{},<*mk,ml*>] implies ( b₁ = SCM-Chg ((SCM-Chg (s,(x address_1),((s . (x address_1)) + (s . (x address_2))))),(succ (IC s))) iff b₁ = SCM-Chg ((SCM-Chg ((SCM-Chg (s,(x address_1),((s . (x address_1)) div (s . (x address_2))))),(x address_2),((s . (x address_1)) mod (s . (x address_2))))),(succ (IC s))) ) ) & ( ex mk, ml being Element of SCM-Data-Loc st x = [2,{},<*mk,ml*>] & ex mk being Element of NAT st x = [6,<*mk*>,{}] implies ( b₁ = SCM-Chg ((SCM-Chg (s,(x address_1),((s . (x address_1)) + (s . (x address_2))))),(succ (IC s))) iff b₁ = SCM-Chg (s,(x jump_address)) ) ) & ( ex mk, ml being Element of SCM-Data-Loc st x = [2,{},<*mk,ml*>] & ex mk being Element of NAT ex ml being Element of SCM-Data-Loc st x = [7,<*mk*>,<*ml*>] implies ( b₁ = SCM-Chg ((SCM-Chg (s,(x address_1),((s . (x address_1)) + (s . (x address_2))))),(succ (IC s))) iff b₁ = SCM-Chg (s,(IFEQ ((s . (x cond_address)),0,(x cjump_address),(succ (IC s))))) ) ) & ( ex mk, ml being Element of SCM-Data-Loc st x = [2,{},<*mk,ml*>] & ex mk being Element of NAT ex ml being Element of SCM-Data-Loc st x = [8,<*mk*>,<*ml*>] implies ( b₁ = SCM-Chg ((SCM-Chg (s,(x address_1),((s . (x address_1)) + (s . (x address_2))))),(succ (IC s))) iff b₁ = SCM-Chg (s,(IFGT ((s . (x cond_address)),0,(x cjump_address),(succ (IC s))))) ) ) & ( ex mk, ml being Element of SCM-Data-Loc st x = [3,{},<*mk,ml*>] & ex mk, ml being Element of SCM-Data-Loc st x = [4,{},<*mk,ml*>] implies ( b₁ = SCM-Chg ((SCM-Chg (s,(x address_1),((s . (x address_1)) - (s . (x address_2))))),(succ (IC s))) iff b₁ = SCM-Chg ((SCM-Chg (s,(x address_1),((s . (x address_1)) * (s . (x address_2))))),(succ (IC s))) ) ) & ( ex mk, ml being Element of SCM-Data-Loc st x = [3,{},<*mk,ml*>] & ex mk, ml being Element of SCM-Data-Loc st x = [5,{},<*mk,ml*>] implies ( b₁ = SCM-Chg ((SCM-Chg (s,(x address_1),((s . (x address_1)) - (s . (x address_2))))),(succ (IC s))) iff b₁ = SCM-Chg ((SCM-Chg ((SCM-Chg (s,(x address_1),((s . (x address_1)) div (s . (x address_2))))),(x address_2),((s . (x address_1)) mod (s . (x address_2))))),(succ (IC s))) ) ) & ( ex mk, ml being Element of SCM-Data-Loc st x = [3,{},<*mk,ml*>] & ex mk being Element of NAT st x = [6,<*mk*>,{}] implies ( b₁ = SCM-Chg ((SCM-Chg (s,(x address_1),((s . (x address_1)) - (s . (x address_2))))),(succ (IC s))) iff b₁ = SCM-Chg (s,(x jump_address)) ) ) & ( ex mk, ml being Element of SCM-Data-Loc st x = [3,{},<*mk,ml*>] & ex mk being Element of NAT ex ml being Element of SCM-Data-Loc st x = [7,<*mk*>,<*ml*>] implies ( b₁ = SCM-Chg ((SCM-Chg (s,(x address_1),((s . (x address_1)) - (s . (x address_2))))),(succ (IC s))) iff b₁ = SCM-Chg (s,(IFEQ ((s . (x cond_address)),0,(x cjump_address),(succ (IC s))))) ) ) & ( ex mk, ml being Element of SCM-Data-Loc st x = [3,{},<*mk,ml*>] & ex mk being Element of NAT ex ml being Element of SCM-Data-Loc st x = [8,<*mk*>,<*ml*>] implies ( b₁ = SCM-Chg ((SCM-Chg (s,(x address_1),((s . (x address_1)) - (s . (x address_2))))),(succ (IC s))) iff b₁ = SCM-Chg (s,(IFGT ((s . (x cond_address)),0,(x cjump_address),(succ (IC s))))) ) ) & ( ex mk, ml being Element of SCM-Data-Loc st x = [4,{},<*mk,ml*>] & ex mk, ml being Element of SCM-Data-Loc st x = [5,{},<*mk,ml*>] implies ( b₁ = SCM-Chg ((SCM-Chg (s,(x address_1),((s . (x address_1)) * (s . (x address_2))))),(succ (IC s))) iff b₁ = SCM-Chg ((SCM-Chg ((SCM-Chg (s,(x address_1),((s . (x address_1)) div (s . (x address_2))))),(x address_2),((s . (x address_1)) mod (s . (x address_2))))),(succ (IC s))) ) ) & ( ex mk, ml being Element of SCM-Data-Loc st x = [4,{},<*mk,ml*>] & ex mk being Element of NAT st x = [6,<*mk*>,{}] implies ( b₁ = SCM-Chg ((SCM-Chg (s,(x address_1),((s . (x address_1)) * (s . (x address_2))))),(succ (IC s))) iff b₁ = SCM-Chg (s,(x jump_address)) ) ) & ( ex mk, ml being Element of SCM-Data-Loc st x = [4,{},<*mk,ml*>] & ex mk being Element of NAT ex ml being Element of SCM-Data-Loc st x = [7,<*mk*>,<*ml*>] implies ( b₁ = SCM-Chg ((SCM-Chg (s,(x address_1),((s . (x address_1)) * (s . (x address_2))))),(succ (IC s))) iff b₁ = SCM-Chg (s,(IFEQ ((s . (x cond_address)),0,(x cjump_address),(succ (IC s))))) ) ) & ( ex mk, ml being Element of SCM-Data-Loc st x = [4,{},<*mk,ml*>] & ex mk being Element of NAT ex ml being Element of SCM-Data-Loc st x = [8,<*mk*>,<*ml*>] implies ( b₁ = SCM-Chg ((SCM-Chg (s,(x address_1),((s . (x address_1)) * (s . (x address_2))))),(succ (IC s))) iff b₁ = SCM-Chg (s,(IFGT ((s . (x cond_address)),0,(x cjump_address),(succ (IC s))))) ) ) & ( ex mk, ml being Element of SCM-Data-Loc st x = [5,{},<*mk,ml*>] & ex mk being Element of NAT st x = [6,<*mk*>,{}] implies ( b₁ = SCM-Chg ((SCM-Chg ((SCM-Chg (s,(x address_1),((s . (x address_1)) div (s . (x address_2))))),(x address_2),((s . (x address_1)) mod (s . (x address_2))))),(succ (IC s))) iff b₁ = SCM-Chg (s,(x jump_address)) ) ) & ( ex mk, ml being Element of SCM-Data-Loc st x = [5,{},<*mk,ml*>] & ex mk being Element of NAT ex ml being Element of SCM-Data-Loc st x = [7,<*mk*>,<*ml*>] implies ( b₁ = SCM-Chg ((SCM-Chg ((SCM-Chg (s,(x address_1),((s . (x address_1)) div (s . (x address_2))))),(x address_2),((s . (x address_1)) mod (s . (x address_2))))),(succ (IC s))) iff b₁ = SCM-Chg (s,(IFEQ ((s . (x cond_address)),0,(x cjump_address),(succ (IC s))))) ) ) & ( ex mk, ml being Element of SCM-Data-Loc st x = [5,{},<*mk,ml*>] & ex mk being Element of NAT ex ml being Element of SCM-Data-Loc st x = [8,<*mk*>,<*ml*>] implies ( b₁ = SCM-Chg ((SCM-Chg ((SCM-Chg (s,(x address_1),((s . (x address_1)) div (s . (x address_2))))),(x address_2),((s . (x address_1)) mod (s . (x address_2))))),(succ (IC s))) iff b₁ = SCM-Chg (s,(IFGT ((s . (x cond_address)),0,(x cjump_address),(succ (IC s))))) ) ) & ( ex mk being Element of NAT st x = [6,<*mk*>,{}] & ex mk being Element of NAT ex ml being Element of SCM-Data-Loc st x = [7,<*mk*>,<*ml*>] implies ( b₁ = SCM-Chg (s,(x jump_address)) iff b₁ = SCM-Chg (s,(IFEQ ((s . (x cond_address)),0,(x cjump_address),(succ (IC s))))) ) ) & ( ex mk being Element of NAT st x = [6,<*mk*>,{}] & ex mk being Element of NAT ex ml being Element of SCM-Data-Loc st x = [8,<*mk*>,<*ml*>] implies ( b₁ = SCM-Chg (s,(x jump_address)) iff b₁ = SCM-Chg (s,(IFGT ((s . (x cond_address)),0,(x cjump_address),(succ (IC s))))) ) ) & ( ex mk being Element of NAT ex ml being Element of SCM-Data-Loc st x = [7,<*mk*>,<*ml*>] & ex mk being Element of NAT ex ml being Element of SCM-Data-Loc st x = [8,<*mk*>,<*ml*>] implies ( b₁ = SCM-Chg (s,(IFEQ ((s . (x cond_address)),0,(x cjump_address),(succ (IC s))))) iff b₁ = SCM-Chg (s,(IFGT ((s . (x cond_address)),0,(x cjump_address),(succ (IC s))))) ) ) ) by MCART_1:28;
coherence
( ( ex mk, ml being Element of SCM-Data-Loc st x = [1,{},<*mk,ml*>] implies SCM-Chg ((SCM-Chg (s,(x address_1),(s . (x address_2)))),(succ (IC s))) is SCM-State ) & ( ex mk, ml being Element of SCM-Data-Loc st x = [2,{},<*mk,ml*>] implies SCM-Chg ((SCM-Chg (s,(x address_1),((s . (x address_1)) + (s . (x address_2))))),(succ (IC s))) is SCM-State ) & ( ex mk, ml being Element of SCM-Data-Loc st x = [3,{},<*mk,ml*>] implies SCM-Chg ((SCM-Chg (s,(x address_1),((s . (x address_1)) - (s . (x address_2))))),(succ (IC s))) is SCM-State ) & ( ex mk, ml being Element of SCM-Data-Loc st x = [4,{},<*mk,ml*>] implies SCM-Chg ((SCM-Chg (s,(x address_1),((s . (x address_1)) * (s . (x address_2))))),(succ (IC s))) is SCM-State ) & ( ex mk, ml being Element of SCM-Data-Loc st x = [5,{},<*mk,ml*>] implies SCM-Chg ((SCM-Chg ((SCM-Chg (s,(x address_1),((s . (x address_1)) div (s . (x address_2))))),(x address_2),((s . (x address_1)) mod (s . (x address_2))))),(succ (IC s))) is SCM-State ) & ( ex mk being Element of NAT st x = [6,<*mk*>,{}] implies SCM-Chg (s,(x jump_address)) is SCM-State ) & ( ex mk being Element of NAT ex ml being Element of SCM-Data-Loc st x = [7,<*mk*>,<*ml*>] implies SCM-Chg (s,(IFEQ ((s . (x cond_address)),0,(x cjump_address),(succ (IC s))))) is SCM-State ) & ( ex mk being Element of NAT ex ml being Element of SCM-Data-Loc st x = [8,<*mk*>,<*ml*>] implies SCM-Chg (s,(IFGT ((s . (x cond_address)),0,(x cjump_address),(succ (IC s))))) is SCM-State ) & ( ( for mk, ml being Element of SCM-Data-Loc holds not x = [1,{},<*mk,ml*>] ) & ( for mk, ml being Element of SCM-Data-Loc holds not x = [2,{},<*mk,ml*>] ) & ( for mk, ml being Element of SCM-Data-Loc holds not x = [3,{},<*mk,ml*>] ) & ( for mk, ml being Element of SCM-Data-Loc holds not x = [4,{},<*mk,ml*>] ) & ( for mk, ml being Element of SCM-Data-Loc holds not x = [5,{},<*mk,ml*>] ) & ( for mk being Element of NAT holds not x = [6,<*mk*>,{}] ) & ( for mk being Element of NAT
for ml being Element of SCM-Data-Loc holds not x = [7,<*mk*>,<*ml*>] ) & ( for mk being Element of NAT
for ml being Element of SCM-Data-Loc holds not x = [8,<*mk*>,<*ml*>] ) implies s is SCM-State ) ) ;

end;

:: deftheorem AMI_2:def 14 :
canceled;

:: deftheorem AMI_2:def 15 :
canceled;

:: deftheorem defines SCM-Exec-Res AMI_2:def 16 :
for x being Element of SCM-Instr
for s being SCM-State holds
( ( ex mk, ml being Element of SCM-Data-Loc st x = [1,{},<*mk,ml*>] implies SCM-Exec-Res (x,s) = SCM-Chg ((SCM-Chg (s,(x address_1),(s . (x address_2)))),(succ (IC s))) ) & ( ex mk, ml being Element of SCM-Data-Loc st x = [2,{},<*mk,ml*>] implies SCM-Exec-Res (x,s) = SCM-Chg ((SCM-Chg (s,(x address_1),((s . (x address_1)) + (s . (x address_2))))),(succ (IC s))) ) & ( ex mk, ml being Element of SCM-Data-Loc st x = [3,{},<*mk,ml*>] implies SCM-Exec-Res (x,s) = SCM-Chg ((SCM-Chg (s,(x address_1),((s . (x address_1)) - (s . (x address_2))))),(succ (IC s))) ) & ( ex mk, ml being Element of SCM-Data-Loc st x = [4,{},<*mk,ml*>] implies SCM-Exec-Res (x,s) = SCM-Chg ((SCM-Chg (s,(x address_1),((s . (x address_1)) * (s . (x address_2))))),(succ (IC s))) ) & ( ex mk, ml being Element of SCM-Data-Loc st x = [5,{},<*mk,ml*>] implies SCM-Exec-Res (x,s) = SCM-Chg ((SCM-Chg ((SCM-Chg (s,(x address_1),((s . (x address_1)) div (s . (x address_2))))),(x address_2),((s . (x address_1)) mod (s . (x address_2))))),(succ (IC s))) ) & ( ex mk being Element of NAT st x = [6,<*mk*>,{}] implies SCM-Exec-Res (x,s) = SCM-Chg (s,(x jump_address)) ) & ( ex mk being Element of NAT ex ml being Element of SCM-Data-Loc st x = [7,<*mk*>,<*ml*>] implies SCM-Exec-Res (x,s) = SCM-Chg (s,(IFEQ ((s . (x cond_address)),0,(x cjump_address),(succ (IC s))))) ) & ( ex mk being Element of NAT ex ml being Element of SCM-Data-Loc st x = [8,<*mk*>,<*ml*>] implies SCM-Exec-Res (x,s) = SCM-Chg (s,(IFGT ((s . (x cond_address)),0,(x cjump_address),(succ (IC s))))) ) & ( ( for mk, ml being Element of SCM-Data-Loc holds not x = [1,{},<*mk,ml*>] ) & ( for mk, ml being Element of SCM-Data-Loc holds not x = [2,{},<*mk,ml*>] ) & ( for mk, ml being Element of SCM-Data-Loc holds not x = [3,{},<*mk,ml*>] ) & ( for mk, ml being Element of SCM-Data-Loc holds not x = [4,{},<*mk,ml*>] ) & ( for mk, ml being Element of SCM-Data-Loc holds not x = [5,{},<*mk,ml*>] ) & ( for mk being Element of NAT holds not x = [6,<*mk*>,{}] ) & ( for mk being Element of NAT
for ml being Element of SCM-Data-Loc holds not x = [7,<*mk*>,<*ml*>] ) & ( for mk being Element of NAT
for ml being Element of SCM-Data-Loc holds not x = [8,<*mk*>,<*ml*>] ) implies SCM-Exec-Res (x,s) = s ) );

definition

func SCM-Exec -> Action of SCM-Instr,(product SCM-OK) means :: AMI_2:def 17
for x being Element of SCM-Instr
for y being SCM-State holds (it . x) . y = SCM-Exec-Res (x,y);
existence
ex b₁ being Action of SCM-Instr,(product SCM-OK) st
for x being Element of SCM-Instr
for y being SCM-State holds (b₁ . x) . y = SCM-Exec-Res (x,y)

proof end;

uniqueness
for b₁, b₂ being Action of SCM-Instr,(product SCM-OK) st ( for x being Element of SCM-Instr
for y being SCM-State holds (b₁ . x) . y = SCM-Exec-Res (x,y) ) & ( for x being Element of SCM-Instr
for y being SCM-State holds (b₂ . x) . y = SCM-Exec-Res (x,y) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem defines SCM-Exec AMI_2:def 17 :
for b₁ being Action of SCM-Instr,(product SCM-OK) holds
( b₁ = SCM-Exec iff for x being Element of SCM-Instr
for y being SCM-State holds (b₁ . x) . y = SCM-Exec-Res (x,y) );

begin

theorem :: AMI_2:26

canceled;

theorem :: AMI_2:27

not NAT in SCM-Data-Loc by Lm2;

theorem :: AMI_2:28

canceled;

theorem :: AMI_2:29

SCM-Data-Loc misses NAT by Lm3;

theorem :: AMI_2:30

NAT in SCM-Memory by Lm5;

theorem :: AMI_2:31

canceled;

theorem :: AMI_2:32

for x being set st x in SCM-Data-Loc holds
ex k being Element of NAT st x = [1,k]

proof end;

theorem :: AMI_2:33

for k being natural number holds [1,k] in SCM-Data-Loc

proof end;

theorem :: AMI_2:34

SCM-Instr c= [:NAT,(NAT *),(proj2 SCM-Instr):]

proof end;

registration

cluster proj2 SCM-Instr -> FinSequence-membered ;
coherence
proj2 SCM-Instr is FinSequence-membered

proof end;

end;