:: by Yatsuka Nakamura and Andrzej Trybulec

::

:: Received December 29, 1992

:: Copyright (c) 1992-2021 Association of Mizar Users

definition

:: original: SCM-Data-Loc

redefine func SCM-Data-Loc -> Subset of SCM-Memory;

coherence

SCM-Data-Loc is Subset of SCM-Memory by XBOOLE_1:7;

end;
redefine func SCM-Data-Loc -> Subset of SCM-Memory;

coherence

SCM-Data-Loc is Subset of SCM-Memory by XBOOLE_1:7;

Lm1: now :: thesis: for k being Element of SCM-Memory holds

( k = NAT or k in SCM-Data-Loc )

( k = NAT or k in SCM-Data-Loc )

let k be Element of SCM-Memory ; :: thesis: ( k = NAT or k in SCM-Data-Loc )

( k in {NAT} or k in SCM-Data-Loc ) by XBOOLE_0:def 3;

hence ( k = NAT or k in SCM-Data-Loc ) by TARSKI:def 1; :: thesis: verum

end;
( k in {NAT} or k in SCM-Data-Loc ) by XBOOLE_0:def 3;

hence ( k = NAT or k in SCM-Data-Loc ) by TARSKI:def 1; :: thesis: verum

Lm2: not NAT in SCM-Data-Loc

proof end;

definition

ex b_{1} being Function of SCM-Memory,(Segm 2) st

for k being Element of SCM-Memory holds

( ( k = NAT implies b_{1} . k = 0 ) & ( k in SCM-Data-Loc implies b_{1} . k = 1 ) )

for b_{1}, b_{2} being Function of SCM-Memory,(Segm 2) st ( for k being Element of SCM-Memory holds

( ( k = NAT implies b_{1} . k = 0 ) & ( k in SCM-Data-Loc implies b_{1} . k = 1 ) ) ) & ( for k being Element of SCM-Memory holds

( ( k = NAT implies b_{2} . k = 0 ) & ( k in SCM-Data-Loc implies b_{2} . k = 1 ) ) ) holds

b_{1} = b_{2}
end;

::$CD 2

func SCM-OK -> Function of SCM-Memory,(Segm 2) means :Def2: :: AMI_2:def 4

for k being Element of SCM-Memory holds

( ( k = NAT implies it . k = 0 ) & ( k in SCM-Data-Loc implies it . k = 1 ) );

existence for k being Element of SCM-Memory holds

( ( k = NAT implies it . k = 0 ) & ( k in SCM-Data-Loc implies it . k = 1 ) );

ex b

for k being Element of SCM-Memory holds

( ( k = NAT implies b

proof end;

uniqueness for b

( ( k = NAT implies b

( ( k = NAT implies b

b

proof end;

:: deftheorem Def2 defines SCM-OK AMI_2:def 4 :

for b_{1} being Function of SCM-Memory,(Segm 2) holds

( b_{1} = SCM-OK iff for k being Element of SCM-Memory holds

( ( k = NAT implies b_{1} . k = 0 ) & ( k in SCM-Data-Loc implies b_{1} . k = 1 ) ) );

for b

( b

( ( k = NAT implies b

::$CT

Lm3: NAT in SCM-Memory

proof end;

::$CT 4

Lm4: dom SCM-OK = SCM-Memory

by PARTFUN1:def 2;

len <%NAT,INT%> = 2

by AFINSQ_1:38;

then rng SCM-OK c= dom SCM-VAL

by RELAT_1:def 19;

then Lm5: dom (SCM-VAL * SCM-OK) = SCM-Memory

by Lm4, RELAT_1:27;

registration
end;

definition
end;

:: deftheorem defines SCM-Chg AMI_2:def 7 :

for s being SCM-State

for u being natural Number holds SCM-Chg (s,u) = s +* (NAT .--> u);

for s being SCM-State

for u being natural Number holds SCM-Chg (s,u) = s +* (NAT .--> u);

theorem :: AMI_2:12

for s being SCM-State

for u being natural Number

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

for u being natural Number

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

proof end;

definition

let s be SCM-State;

let t be Element of SCM-Data-Loc ;

let u be Integer;

coherence

s +* (t .--> u) is SCM-State

end;
let t be Element of SCM-Data-Loc ;

let u be Integer;

coherence

s +* (t .--> u) is SCM-State

proof 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);

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:14

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

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:15

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

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:16

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

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;

registration
end;

definition

let x be Element of SCM-Instr ;

let s be SCM-State;

for b_{1} 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_{1} = SCM-Chg ((SCM-Chg (s,(x address_1),(s . (x address_2)))),((IC s) + 1)) iff b_{1} = SCM-Chg ((SCM-Chg (s,(x address_1),((s . (x address_1)) + (s . (x address_2))))),((IC s) + 1)) ) ) & ( 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_{1} = SCM-Chg ((SCM-Chg (s,(x address_1),(s . (x address_2)))),((IC s) + 1)) iff b_{1} = SCM-Chg ((SCM-Chg (s,(x address_1),((s . (x address_1)) - (s . (x address_2))))),((IC s) + 1)) ) ) & ( 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_{1} = SCM-Chg ((SCM-Chg (s,(x address_1),(s . (x address_2)))),((IC s) + 1)) iff b_{1} = SCM-Chg ((SCM-Chg (s,(x address_1),((s . (x address_1)) * (s . (x address_2))))),((IC s) + 1)) ) ) & ( 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_{1} = SCM-Chg ((SCM-Chg (s,(x address_1),(s . (x address_2)))),((IC s) + 1)) iff b_{1} = 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))))),((IC s) + 1)) ) ) & ( ex mk, ml being Element of SCM-Data-Loc st x = [1,{},<*mk,ml*>] & ex mk being Nat st x = [6,<*mk*>,{}] implies ( b_{1} = SCM-Chg ((SCM-Chg (s,(x address_1),(s . (x address_2)))),((IC s) + 1)) iff b_{1} = SCM-Chg (s,(x jump_address)) ) ) & ( ex mk, ml being Element of SCM-Data-Loc st x = [1,{},<*mk,ml*>] & ex mk being Nat ex ml being Element of SCM-Data-Loc st x = [7,<*mk*>,<*ml*>] implies ( b_{1} = SCM-Chg ((SCM-Chg (s,(x address_1),(s . (x address_2)))),((IC s) + 1)) iff b_{1} = SCM-Chg (s,(IFEQ ((s . (x cond_address)),0,(x cjump_address),((IC s) + 1)))) ) ) & ( ex mk, ml being Element of SCM-Data-Loc st x = [1,{},<*mk,ml*>] & ex mk being Nat ex ml being Element of SCM-Data-Loc st x = [8,<*mk*>,<*ml*>] implies ( b_{1} = SCM-Chg ((SCM-Chg (s,(x address_1),(s . (x address_2)))),((IC s) + 1)) iff b_{1} = SCM-Chg (s,(IFGT ((s . (x cond_address)),0,(x cjump_address),((IC s) + 1)))) ) ) & ( 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_{1} = SCM-Chg ((SCM-Chg (s,(x address_1),((s . (x address_1)) + (s . (x address_2))))),((IC s) + 1)) iff b_{1} = SCM-Chg ((SCM-Chg (s,(x address_1),((s . (x address_1)) - (s . (x address_2))))),((IC s) + 1)) ) ) & ( 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_{1} = SCM-Chg ((SCM-Chg (s,(x address_1),((s . (x address_1)) + (s . (x address_2))))),((IC s) + 1)) iff b_{1} = SCM-Chg ((SCM-Chg (s,(x address_1),((s . (x address_1)) * (s . (x address_2))))),((IC s) + 1)) ) ) & ( 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_{1} = SCM-Chg ((SCM-Chg (s,(x address_1),((s . (x address_1)) + (s . (x address_2))))),((IC s) + 1)) iff b_{1} = 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))))),((IC s) + 1)) ) ) & ( ex mk, ml being Element of SCM-Data-Loc st x = [2,{},<*mk,ml*>] & ex mk being Nat st x = [6,<*mk*>,{}] implies ( b_{1} = SCM-Chg ((SCM-Chg (s,(x address_1),((s . (x address_1)) + (s . (x address_2))))),((IC s) + 1)) iff b_{1} = SCM-Chg (s,(x jump_address)) ) ) & ( ex mk, ml being Element of SCM-Data-Loc st x = [2,{},<*mk,ml*>] & ex mk being Nat ex ml being Element of SCM-Data-Loc st x = [7,<*mk*>,<*ml*>] implies ( b_{1} = SCM-Chg ((SCM-Chg (s,(x address_1),((s . (x address_1)) + (s . (x address_2))))),((IC s) + 1)) iff b_{1} = SCM-Chg (s,(IFEQ ((s . (x cond_address)),0,(x cjump_address),((IC s) + 1)))) ) ) & ( ex mk, ml being Element of SCM-Data-Loc st x = [2,{},<*mk,ml*>] & ex mk being Nat ex ml being Element of SCM-Data-Loc st x = [8,<*mk*>,<*ml*>] implies ( b_{1} = SCM-Chg ((SCM-Chg (s,(x address_1),((s . (x address_1)) + (s . (x address_2))))),((IC s) + 1)) iff b_{1} = SCM-Chg (s,(IFGT ((s . (x cond_address)),0,(x cjump_address),((IC s) + 1)))) ) ) & ( 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_{1} = SCM-Chg ((SCM-Chg (s,(x address_1),((s . (x address_1)) - (s . (x address_2))))),((IC s) + 1)) iff b_{1} = SCM-Chg ((SCM-Chg (s,(x address_1),((s . (x address_1)) * (s . (x address_2))))),((IC s) + 1)) ) ) & ( 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_{1} = SCM-Chg ((SCM-Chg (s,(x address_1),((s . (x address_1)) - (s . (x address_2))))),((IC s) + 1)) iff b_{1} = 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))))),((IC s) + 1)) ) ) & ( ex mk, ml being Element of SCM-Data-Loc st x = [3,{},<*mk,ml*>] & ex mk being Nat st x = [6,<*mk*>,{}] implies ( b_{1} = SCM-Chg ((SCM-Chg (s,(x address_1),((s . (x address_1)) - (s . (x address_2))))),((IC s) + 1)) iff b_{1} = SCM-Chg (s,(x jump_address)) ) ) & ( ex mk, ml being Element of SCM-Data-Loc st x = [3,{},<*mk,ml*>] & ex mk being Nat ex ml being Element of SCM-Data-Loc st x = [7,<*mk*>,<*ml*>] implies ( b_{1} = SCM-Chg ((SCM-Chg (s,(x address_1),((s . (x address_1)) - (s . (x address_2))))),((IC s) + 1)) iff b_{1} = SCM-Chg (s,(IFEQ ((s . (x cond_address)),0,(x cjump_address),((IC s) + 1)))) ) ) & ( ex mk, ml being Element of SCM-Data-Loc st x = [3,{},<*mk,ml*>] & ex mk being Nat ex ml being Element of SCM-Data-Loc st x = [8,<*mk*>,<*ml*>] implies ( b_{1} = SCM-Chg ((SCM-Chg (s,(x address_1),((s . (x address_1)) - (s . (x address_2))))),((IC s) + 1)) iff b_{1} = SCM-Chg (s,(IFGT ((s . (x cond_address)),0,(x cjump_address),((IC s) + 1)))) ) ) & ( 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_{1} = SCM-Chg ((SCM-Chg (s,(x address_1),((s . (x address_1)) * (s . (x address_2))))),((IC s) + 1)) iff b_{1} = 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))))),((IC s) + 1)) ) ) & ( ex mk, ml being Element of SCM-Data-Loc st x = [4,{},<*mk,ml*>] & ex mk being Nat st x = [6,<*mk*>,{}] implies ( b_{1} = SCM-Chg ((SCM-Chg (s,(x address_1),((s . (x address_1)) * (s . (x address_2))))),((IC s) + 1)) iff b_{1} = SCM-Chg (s,(x jump_address)) ) ) & ( ex mk, ml being Element of SCM-Data-Loc st x = [4,{},<*mk,ml*>] & ex mk being Nat ex ml being Element of SCM-Data-Loc st x = [7,<*mk*>,<*ml*>] implies ( b_{1} = SCM-Chg ((SCM-Chg (s,(x address_1),((s . (x address_1)) * (s . (x address_2))))),((IC s) + 1)) iff b_{1} = SCM-Chg (s,(IFEQ ((s . (x cond_address)),0,(x cjump_address),((IC s) + 1)))) ) ) & ( ex mk, ml being Element of SCM-Data-Loc st x = [4,{},<*mk,ml*>] & ex mk being Nat ex ml being Element of SCM-Data-Loc st x = [8,<*mk*>,<*ml*>] implies ( b_{1} = SCM-Chg ((SCM-Chg (s,(x address_1),((s . (x address_1)) * (s . (x address_2))))),((IC s) + 1)) iff b_{1} = SCM-Chg (s,(IFGT ((s . (x cond_address)),0,(x cjump_address),((IC s) + 1)))) ) ) & ( ex mk, ml being Element of SCM-Data-Loc st x = [5,{},<*mk,ml*>] & ex mk being Nat st x = [6,<*mk*>,{}] implies ( b_{1} = 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))))),((IC s) + 1)) iff b_{1} = SCM-Chg (s,(x jump_address)) ) ) & ( ex mk, ml being Element of SCM-Data-Loc st x = [5,{},<*mk,ml*>] & ex mk being Nat ex ml being Element of SCM-Data-Loc st x = [7,<*mk*>,<*ml*>] implies ( b_{1} = 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))))),((IC s) + 1)) iff b_{1} = SCM-Chg (s,(IFEQ ((s . (x cond_address)),0,(x cjump_address),((IC s) + 1)))) ) ) & ( ex mk, ml being Element of SCM-Data-Loc st x = [5,{},<*mk,ml*>] & ex mk being Nat ex ml being Element of SCM-Data-Loc st x = [8,<*mk*>,<*ml*>] implies ( b_{1} = 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))))),((IC s) + 1)) iff b_{1} = SCM-Chg (s,(IFGT ((s . (x cond_address)),0,(x cjump_address),((IC s) + 1)))) ) ) & ( ex mk being Nat st x = [6,<*mk*>,{}] & ex mk being Nat ex ml being Element of SCM-Data-Loc st x = [7,<*mk*>,<*ml*>] implies ( b_{1} = SCM-Chg (s,(x jump_address)) iff b_{1} = SCM-Chg (s,(IFEQ ((s . (x cond_address)),0,(x cjump_address),((IC s) + 1)))) ) ) & ( ex mk being Nat st x = [6,<*mk*>,{}] & ex mk being Nat ex ml being Element of SCM-Data-Loc st x = [8,<*mk*>,<*ml*>] implies ( b_{1} = SCM-Chg (s,(x jump_address)) iff b_{1} = SCM-Chg (s,(IFGT ((s . (x cond_address)),0,(x cjump_address),((IC s) + 1)))) ) ) & ( ex mk being Nat ex ml being Element of SCM-Data-Loc st x = [7,<*mk*>,<*ml*>] & ex mk being Nat ex ml being Element of SCM-Data-Loc st x = [8,<*mk*>,<*ml*>] implies ( b_{1} = SCM-Chg (s,(IFEQ ((s . (x cond_address)),0,(x cjump_address),((IC s) + 1)))) iff b_{1} = SCM-Chg (s,(IFGT ((s . (x cond_address)),0,(x cjump_address),((IC s) + 1)))) ) ) )
by XTUPLE_0:3;

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)))),((IC s) + 1)) 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))))),((IC s) + 1)) 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))))),((IC s) + 1)) 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))))),((IC s) + 1)) 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))))),((IC s) + 1)) is SCM-State ) & ( ex mk being Nat st x = [6,<*mk*>,{}] implies SCM-Chg (s,(x jump_address)) is SCM-State ) & ( ex mk being 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),((IC s) + 1)))) is SCM-State ) & ( ex mk being 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),((IC s) + 1)))) 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 Nat holds not x = [6,<*mk*>,{}] ) & ( for mk being Nat

for ml being Element of SCM-Data-Loc holds not x = [7,<*mk*>,<*ml*>] ) & ( for mk being Nat

for ml being Element of SCM-Data-Loc holds not x = [8,<*mk*>,<*ml*>] ) implies s is SCM-State ) ) ;

end;
let s be SCM-State;

func SCM-Exec-Res (x,s) -> SCM-State equals :: AMI_2:def 14

SCM-Chg ((SCM-Chg (s,(x address_1),(s . (x address_2)))),((IC s) + 1)) 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))))),((IC s) + 1)) 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))))),((IC s) + 1)) 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))))),((IC s) + 1)) 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))))),((IC s) + 1)) 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 Nat st x = [6,<*mk*>,{}]

SCM-Chg (s,(IFEQ ((s . (x cond_address)),0,(x cjump_address),((IC s) + 1)))) if ex mk being 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),((IC s) + 1)))) if ex mk being Nat ex ml being Element of SCM-Data-Loc st x = [8,<*mk*>,<*ml*>]

otherwise s;

consistency SCM-Chg ((SCM-Chg (s,(x address_1),(s . (x address_2)))),((IC s) + 1)) 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))))),((IC s) + 1)) 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))))),((IC s) + 1)) 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))))),((IC s) + 1)) 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))))),((IC s) + 1)) 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 Nat st x = [6,<*mk*>,{}]

SCM-Chg (s,(IFEQ ((s . (x cond_address)),0,(x cjump_address),((IC s) + 1)))) if ex mk being 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),((IC s) + 1)))) if ex mk being Nat ex ml being Element of SCM-Data-Loc st x = [8,<*mk*>,<*ml*>]

otherwise s;

for b

( ( 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

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)))),((IC s) + 1)) 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))))),((IC s) + 1)) 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))))),((IC s) + 1)) 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))))),((IC s) + 1)) 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))))),((IC s) + 1)) is SCM-State ) & ( ex mk being Nat st x = [6,<*mk*>,{}] implies SCM-Chg (s,(x jump_address)) is SCM-State ) & ( ex mk being 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),((IC s) + 1)))) is SCM-State ) & ( ex mk being 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),((IC s) + 1)))) 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 Nat holds not x = [6,<*mk*>,{}] ) & ( for mk being Nat

for ml being Element of SCM-Data-Loc holds not x = [7,<*mk*>,<*ml*>] ) & ( for mk being Nat

for ml being Element of SCM-Data-Loc holds not x = [8,<*mk*>,<*ml*>] ) implies s is SCM-State ) ) ;

:: deftheorem defines SCM-Exec-Res AMI_2:def 14 :

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)))),((IC s) + 1)) ) & ( 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))))),((IC s) + 1)) ) & ( 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))))),((IC s) + 1)) ) & ( 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))))),((IC s) + 1)) ) & ( 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))))),((IC s) + 1)) ) & ( ex mk being Nat st x = [6,<*mk*>,{}] implies SCM-Exec-Res (x,s) = SCM-Chg (s,(x jump_address)) ) & ( ex mk being 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),((IC s) + 1)))) ) & ( ex mk being 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),((IC s) + 1)))) ) & ( ( 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 Nat holds not x = [6,<*mk*>,{}] ) & ( for mk being Nat

for ml being Element of SCM-Data-Loc holds not x = [7,<*mk*>,<*ml*>] ) & ( for mk being Nat

for ml being Element of SCM-Data-Loc holds not x = [8,<*mk*>,<*ml*>] ) implies SCM-Exec-Res (x,s) = s ) );

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)))),((IC s) + 1)) ) & ( 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))))),((IC s) + 1)) ) & ( 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))))),((IC s) + 1)) ) & ( 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))))),((IC s) + 1)) ) & ( 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))))),((IC s) + 1)) ) & ( ex mk being Nat st x = [6,<*mk*>,{}] implies SCM-Exec-Res (x,s) = SCM-Chg (s,(x jump_address)) ) & ( ex mk being 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),((IC s) + 1)))) ) & ( ex mk being 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),((IC s) + 1)))) ) & ( ( 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 Nat holds not x = [6,<*mk*>,{}] ) & ( for mk being Nat

for ml being Element of SCM-Data-Loc holds not x = [7,<*mk*>,<*ml*>] ) & ( for mk being Nat

for ml being Element of SCM-Data-Loc holds not x = [8,<*mk*>,<*ml*>] ) implies SCM-Exec-Res (x,s) = s ) );

definition

ex b_{1} being Action of SCM-Instr,(product (SCM-VAL * SCM-OK)) st

for x being Element of SCM-Instr

for y being SCM-State holds (b_{1} . x) . y = SCM-Exec-Res (x,y)

for b_{1}, b_{2} being Action of SCM-Instr,(product (SCM-VAL * SCM-OK)) st ( for x being Element of SCM-Instr

for y being SCM-State holds (b_{1} . x) . y = SCM-Exec-Res (x,y) ) & ( for x being Element of SCM-Instr

for y being SCM-State holds (b_{2} . x) . y = SCM-Exec-Res (x,y) ) holds

b_{1} = b_{2}
end;

func SCM-Exec -> Action of SCM-Instr,(product (SCM-VAL * SCM-OK)) means :: AMI_2:def 15

for x being Element of SCM-Instr

for y being SCM-State holds (it . x) . y = SCM-Exec-Res (x,y);

existence for x being Element of SCM-Instr

for y being SCM-State holds (it . x) . y = SCM-Exec-Res (x,y);

ex b

for x being Element of SCM-Instr

for y being SCM-State holds (b

proof end;

uniqueness for b

for y being SCM-State holds (b

for y being SCM-State holds (b

b

proof end;

:: deftheorem defines SCM-Exec AMI_2:def 15 :

for b_{1} being Action of SCM-Instr,(product (SCM-VAL * SCM-OK)) holds

( b_{1} = SCM-Exec iff for x being Element of SCM-Instr

for y being SCM-State holds (b_{1} . x) . y = SCM-Exec-Res (x,y) );

for b

( b

for y being SCM-State holds (b

:: missing, 2007.07.27, A.T.

::$CT 3

::$CT 3

:: missing, 2007.07.27, A.T.

::$CT 3

::$CT 3

::$CT

::$CT

theorem :: AMI_2:26

:: deftheorem defines Int-like AMI_2:def 16 :

for x being set holds

( x is Int-like iff x in SCM-Data-Loc );

for x being set holds

( x is Int-like iff x in SCM-Data-Loc );

::definition

:: func SCM-Data-Loc equals

:: [:{1},NAT:];

:: coherence;

::end;