:: On a Mathematical Model of Programs
:: by Yatsuka Nakamura and Andrzej Trybulec
::
:: Copyright (c) 1992-2017 Association of Mizar Users

:: Na razie potrzebny w SCM_INST
::definition
:: func SCM-Data-Loc equals
:: [:{1},NAT:];
:: coherence;
::end;
definition
coherence ;
end;

:: deftheorem defines SCM-Memory AMI_2:def 1 :

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 by XBOOLE_1:7;
end;

Lm1: now :: thesis: for k being Element of SCM-Memory holds
( 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 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;

Lm2:
proof end;

definition
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
ex b1 being Function of SCM-Memory,(Segm 2) st
for k being Element of SCM-Memory holds
( ( k = NAT implies b1 . k = 0 ) & ( k in SCM-Data-Loc implies b1 . k = 1 ) )
proof end;
uniqueness
for b1, b2 being Function of SCM-Memory,(Segm 2) st ( for k being Element of SCM-Memory holds
( ( k = NAT implies b1 . k = 0 ) & ( k in SCM-Data-Loc implies b1 . k = 1 ) ) ) & ( for k being Element of SCM-Memory holds
( ( k = NAT implies b2 . k = 0 ) & ( k in SCM-Data-Loc implies b2 . k = 1 ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem AMI_2:def 2 :
canceled;

:: deftheorem AMI_2:def 3 :
canceled;

:: deftheorem Def2 defines SCM-OK AMI_2:def 4 :
for b1 being Function of SCM-Memory,(Segm 2) holds
( b1 = SCM-OK iff for k being Element of SCM-Memory holds
( ( k = NAT implies b1 . k = 0 ) & ( k in SCM-Data-Loc implies b1 . k = 1 ) ) );

theorem :: AMI_2:1
canceled;

::\$CT
definition
func SCM-VAL -> ManySortedSet of Segm 2 equals :: AMI_2:def 5
;
coherence ;
end;

:: deftheorem defines SCM-VAL AMI_2:def 5 :

Lm3:
proof end;

theorem :: AMI_2:2
canceled;

theorem :: AMI_2:3
canceled;

theorem :: AMI_2:4
canceled;

theorem :: AMI_2:5
canceled;

::\$CT 4
theorem Th1: :: AMI_2:6
proof end;

theorem Th2: :: AMI_2:7
for i being Element of SCM-Memory st i in SCM-Data-Loc holds
() . i = INT
proof end;

Lm4:
by PARTFUN1:def 2;

by AFINSQ_1:38;

then
by RELAT_1:def 19;

then Lm5:
by ;

registration
coherence
proof end;
end;

definition end;

theorem :: AMI_2:8
for a being Element of SCM-Data-Loc holds () . a = INT by Th2;

theorem Th4: :: AMI_2:9
pi ((),NAT) = NAT by ;

theorem Th5: :: AMI_2:10
for a being Element of SCM-Data-Loc holds pi ((),a) = INT
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 ;
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 natural Number ;
func SCM-Chg (s,u) -> SCM-State equals :: AMI_2:def 7
s +* ();
coherence
s +* () is SCM-State
proof end;
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 +* ();

theorem :: AMI_2:11
for s being SCM-State
for u being natural Number holds (SCM-Chg (s,u)) . NAT = u
proof end;

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

theorem :: AMI_2:13
for s being SCM-State
for u, v being natural Number 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: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
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
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
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;

registration
let x, y be ExtReal;
let a, b be Nat;
cluster IFGT (x,y,a,b) -> natural ;
coherence
IFGT (x,y,a,b) is natural
;
end;

definition
let x be Element of SCM-Instr ;
let s be SCM-State;
func SCM-Exec-Res (x,s) -> SCM-State equals :: AMI_2:def 14
SCM-Chg ((SCM-Chg (s,(),(s . ()))),((IC s) + 1)) if ex mk, ml being Element of SCM-Data-Loc st x = [1,{},<*mk,ml*>]
SCM-Chg ((SCM-Chg (s,(),((s . ()) + (s . ())))),((IC s) + 1)) if ex mk, ml being Element of SCM-Data-Loc st x = [2,{},<*mk,ml*>]
SCM-Chg ((SCM-Chg (s,(),((s . ()) - (s . ())))),((IC s) + 1)) if ex mk, ml being Element of SCM-Data-Loc st x = [3,{},<*mk,ml*>]
SCM-Chg ((SCM-Chg (s,(),((s . ()) * (s . ())))),((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,(),((s . ()) div (s . ())))),(),((s . ()) mod (s . ())))),((IC s) + 1)) if ex mk, ml being Element of SCM-Data-Loc st x = [5,{},<*mk,ml*>]
SCM-Chg (s,()) if ex mk being Nat st x = [6,<*mk*>,{}]
SCM-Chg (s,(IFEQ ((s . ()),0,(),((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 . ()),0,(),((IC s) + 1)))) if ex mk being Nat ex ml being Element of SCM-Data-Loc st x = [8,<*mk*>,<*ml*>]
otherwise s;
consistency
for b1 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 ( b1 = SCM-Chg ((SCM-Chg (s,(),(s . ()))),((IC s) + 1)) iff b1 = SCM-Chg ((SCM-Chg (s,(),((s . ()) + (s . ())))),((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 ( b1 = SCM-Chg ((SCM-Chg (s,(),(s . ()))),((IC s) + 1)) iff b1 = SCM-Chg ((SCM-Chg (s,(),((s . ()) - (s . ())))),((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 ( b1 = SCM-Chg ((SCM-Chg (s,(),(s . ()))),((IC s) + 1)) iff b1 = SCM-Chg ((SCM-Chg (s,(),((s . ()) * (s . ())))),((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 ( b1 = SCM-Chg ((SCM-Chg (s,(),(s . ()))),((IC s) + 1)) iff b1 = SCM-Chg ((SCM-Chg ((SCM-Chg (s,(),((s . ()) div (s . ())))),(),((s . ()) mod (s . ())))),((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 ( b1 = SCM-Chg ((SCM-Chg (s,(),(s . ()))),((IC s) + 1)) iff b1 = SCM-Chg (s,()) ) ) & ( 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 ( b1 = SCM-Chg ((SCM-Chg (s,(),(s . ()))),((IC s) + 1)) iff b1 = SCM-Chg (s,(IFEQ ((s . ()),0,(),((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 ( b1 = SCM-Chg ((SCM-Chg (s,(),(s . ()))),((IC s) + 1)) iff b1 = SCM-Chg (s,(IFGT ((s . ()),0,(),((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 ( b1 = SCM-Chg ((SCM-Chg (s,(),((s . ()) + (s . ())))),((IC s) + 1)) iff b1 = SCM-Chg ((SCM-Chg (s,(),((s . ()) - (s . ())))),((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 ( b1 = SCM-Chg ((SCM-Chg (s,(),((s . ()) + (s . ())))),((IC s) + 1)) iff b1 = SCM-Chg ((SCM-Chg (s,(),((s . ()) * (s . ())))),((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 ( b1 = SCM-Chg ((SCM-Chg (s,(),((s . ()) + (s . ())))),((IC s) + 1)) iff b1 = SCM-Chg ((SCM-Chg ((SCM-Chg (s,(),((s . ()) div (s . ())))),(),((s . ()) mod (s . ())))),((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 ( b1 = SCM-Chg ((SCM-Chg (s,(),((s . ()) + (s . ())))),((IC s) + 1)) iff b1 = SCM-Chg (s,()) ) ) & ( 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 ( b1 = SCM-Chg ((SCM-Chg (s,(),((s . ()) + (s . ())))),((IC s) + 1)) iff b1 = SCM-Chg (s,(IFEQ ((s . ()),0,(),((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 ( b1 = SCM-Chg ((SCM-Chg (s,(),((s . ()) + (s . ())))),((IC s) + 1)) iff b1 = SCM-Chg (s,(IFGT ((s . ()),0,(),((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 ( b1 = SCM-Chg ((SCM-Chg (s,(),((s . ()) - (s . ())))),((IC s) + 1)) iff b1 = SCM-Chg ((SCM-Chg (s,(),((s . ()) * (s . ())))),((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 ( b1 = SCM-Chg ((SCM-Chg (s,(),((s . ()) - (s . ())))),((IC s) + 1)) iff b1 = SCM-Chg ((SCM-Chg ((SCM-Chg (s,(),((s . ()) div (s . ())))),(),((s . ()) mod (s . ())))),((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 ( b1 = SCM-Chg ((SCM-Chg (s,(),((s . ()) - (s . ())))),((IC s) + 1)) iff b1 = SCM-Chg (s,()) ) ) & ( 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 ( b1 = SCM-Chg ((SCM-Chg (s,(),((s . ()) - (s . ())))),((IC s) + 1)) iff b1 = SCM-Chg (s,(IFEQ ((s . ()),0,(),((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 ( b1 = SCM-Chg ((SCM-Chg (s,(),((s . ()) - (s . ())))),((IC s) + 1)) iff b1 = SCM-Chg (s,(IFGT ((s . ()),0,(),((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 ( b1 = SCM-Chg ((SCM-Chg (s,(),((s . ()) * (s . ())))),((IC s) + 1)) iff b1 = SCM-Chg ((SCM-Chg ((SCM-Chg (s,(),((s . ()) div (s . ())))),(),((s . ()) mod (s . ())))),((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 ( b1 = SCM-Chg ((SCM-Chg (s,(),((s . ()) * (s . ())))),((IC s) + 1)) iff b1 = SCM-Chg (s,()) ) ) & ( 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 ( b1 = SCM-Chg ((SCM-Chg (s,(),((s . ()) * (s . ())))),((IC s) + 1)) iff b1 = SCM-Chg (s,(IFEQ ((s . ()),0,(),((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 ( b1 = SCM-Chg ((SCM-Chg (s,(),((s . ()) * (s . ())))),((IC s) + 1)) iff b1 = SCM-Chg (s,(IFGT ((s . ()),0,(),((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 ( b1 = SCM-Chg ((SCM-Chg ((SCM-Chg (s,(),((s . ()) div (s . ())))),(),((s . ()) mod (s . ())))),((IC s) + 1)) iff b1 = SCM-Chg (s,()) ) ) & ( 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 ( b1 = SCM-Chg ((SCM-Chg ((SCM-Chg (s,(),((s . ()) div (s . ())))),(),((s . ()) mod (s . ())))),((IC s) + 1)) iff b1 = SCM-Chg (s,(IFEQ ((s . ()),0,(),((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 ( b1 = SCM-Chg ((SCM-Chg ((SCM-Chg (s,(),((s . ()) div (s . ())))),(),((s . ()) mod (s . ())))),((IC s) + 1)) iff b1 = SCM-Chg (s,(IFGT ((s . ()),0,(),((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 ( b1 = SCM-Chg (s,()) iff b1 = SCM-Chg (s,(IFEQ ((s . ()),0,(),((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 ( b1 = SCM-Chg (s,()) iff b1 = SCM-Chg (s,(IFGT ((s . ()),0,(),((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 ( b1 = SCM-Chg (s,(IFEQ ((s . ()),0,(),((IC s) + 1)))) iff b1 = SCM-Chg (s,(IFGT ((s . ()),0,(),((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,(),(s . ()))),((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,(),((s . ()) + (s . ())))),((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,(),((s . ()) - (s . ())))),((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,(),((s . ()) * (s . ())))),((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,(),((s . ()) div (s . ())))),(),((s . ()) mod (s . ())))),((IC s) + 1)) is SCM-State ) & ( ex mk being Nat st x = [6,<*mk*>,{}] implies SCM-Chg (s,()) 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 . ()),0,(),((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 . ()),0,(),((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;

:: deftheorem AMI_2:def 9 :
canceled;

:: deftheorem AMI_2:def 10 :
canceled;

:: deftheorem AMI_2:def 11 :
canceled;

:: deftheorem AMI_2:def 12 :
canceled;

:: deftheorem AMI_2:def 13 :
canceled;

:: 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,(),(s . ()))),((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,(),((s . ()) + (s . ())))),((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,(),((s . ()) - (s . ())))),((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,(),((s . ()) * (s . ())))),((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,(),((s . ()) div (s . ())))),(),((s . ()) mod (s . ())))),((IC s) + 1)) ) & ( ex mk being Nat st x = [6,<*mk*>,{}] implies SCM-Exec-Res (x,s) = SCM-Chg (s,()) ) & ( 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 . ()),0,(),((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 . ()),0,(),((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
func SCM-Exec -> Action of SCM-Instr,() 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
ex b1 being Action of SCM-Instr,() st
for x being Element of SCM-Instr
for y being SCM-State holds (b1 . x) . y = SCM-Exec-Res (x,y)
proof end;
uniqueness
for b1, b2 being Action of SCM-Instr,() st ( for x being Element of SCM-Instr
for y being SCM-State holds (b1 . x) . y = SCM-Exec-Res (x,y) ) & ( for x being Element of SCM-Instr
for y being SCM-State holds (b2 . x) . y = SCM-Exec-Res (x,y) ) holds
b1 = b2
proof end;
end;

:: deftheorem defines SCM-Exec AMI_2:def 15 :
for b1 being Action of SCM-Instr,() holds
( b1 = SCM-Exec iff for x being Element of SCM-Instr
for y being SCM-State holds (b1 . x) . y = SCM-Exec-Res (x,y) );

theorem :: AMI_2:17
canceled;

theorem :: AMI_2:18
canceled;

theorem :: AMI_2:19
canceled;

:: missing, 2007.07.27, A.T.
::\$CT 3
theorem :: AMI_2:20
not NAT in SCM-Data-Loc by Lm2;

theorem :: AMI_2:21
canceled;

::\$CT
theorem :: AMI_2:22

theorem :: AMI_2:23
for x being set st x in SCM-Data-Loc holds
ex k being Nat st x = [1,k]
proof end;

theorem :: AMI_2:24
for k being Nat holds [1,k] in SCM-Data-Loc
proof end;

theorem :: AMI_2:25
canceled;

::\$CT
theorem :: AMI_2:26
for k being Element of SCM-Memory holds
( k = NAT or k in SCM-Data-Loc ) by Lm1;

theorem :: AMI_2:27

theorem :: AMI_2:28
for s being SCM-State holds dom s = SCM-Memory by ;

definition
let x be set ;
end;

:: deftheorem defines Int-like AMI_2:def 16 :
for x being set holds
( x is Int-like iff x in SCM-Data-Loc );

theorem :: AMI_2:29
for S being SCM-State holds S is SCM-Memory -defined total Function ;