SCMFSA_1: An Extension of { \bf SCM }

:: An Extension of { \bf SCM }
:: by Andrzej Trybulec , Yatsuka Nakamura and Piotr Rudnicki
::
:: Received February 3, 1996
:: Copyright (c) 1996-2016 Association of Mizar Users

environ

vocabularies HIDDEN, NUMBERS, SUBSET_1, AMI_2, XBOOLE_0, TARSKI, CARD_1, FINSEQ_1, ZFMISC_1, RELAT_1, AMI_1, ORDINAL1, XXREAL_0, FUNCT_1, FUNCOP_1, FUNCT_4, INT_1, CARD_3, PBOOLE, NAT_1, PARTFUN1, COMPLEX1, FINSEQ_2, FUNCT_2, FUNCT_5, SCMFSA_1, GROUP_9, RECDEF_2, AFINSQ_1, ARYTM_3;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, XFAMILY, SUBSET_1, ORDINAL1, CARD_1, NUMBERS, INT_2, PBOOLE, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2, BINOP_1, XCMPLX_0, INT_1, AFINSQ_1, FINSEQ_1, FUNCT_4, FUNCT_5, FINSEQ_2, CARD_3, FUNCOP_1, FUNCT_7, XXREAL_0, RECDEF_2, MEMSTR_0, SCM_INST, AMI_2, SCMFSA_I;
definitions FUNCT_1;
theorems ZFMISC_1, FUNCT_2, TARSKI, FUNCOP_1, INT_1, CARD_3, FINSEQ_1, FUNCT_4, RELAT_1, FUNCT_1, FINSEQ_2, PRE_CIRC, AMI_2, FUNCT_7, RELSET_1, ORDINAL1, XBOOLE_0, XBOOLE_1, NUMBERS, PARTFUN1, AFINSQ_1, SCMFSA_I, FUNCT_5, XTUPLE_0;
schemes BINOP_1;
registrations XBOOLE_0, FUNCT_1, ORDINAL1, FUNCOP_1, XREAL_0, INT_1, FINSEQ_1, CARD_3, AMI_2, RELAT_1, FINSET_1, CARD_1, CARD_2, RELSET_1, FUNCT_2, AFINSQ_1, COMPOS_0, SCM_INST, SCMFSA_I;
constructors HIDDEN, INT_2, FUNCT_5, RELSET_1, FUNCT_7, PRE_POLY, AMI_3, SCMFSA_I, BINOP_1, XTUPLE_0, XFAMILY;
requirements HIDDEN, NUMERALS, REAL, BOOLE, SUBSET;
equalities TARSKI, FUNCOP_1, AMI_2, SCMFSA_I, ORDINAL1, CARD_1;
expansions TARSKI;

notation

synonym SCM+FSA-Data-Loc for SCM-Data-Loc ;

end;

definition

func SCM+FSA-Memory -> set equals :: SCMFSA_1:def 2
SCM-Memory \/ SCM+FSA-Data*-Loc;

end;

:: deftheorem SCMFSA_1:def 1 :

:: deftheorem defines SCM+FSA-Memory SCMFSA_1:def 2 :

registration

cluster SCM+FSA-Memory -> non empty ;

end;

theorem Th1: :: SCMFSA_1:1

SCM-Memory c= SCM+FSA-Memory by XBOOLE_1:7;

definition

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

proof end;

end;

definition

:: original: SCM+FSA-Data*-Loc
redefine func SCM+FSA-Data*-Loc -> Subset of SCM+FSA-Memory;
coherence by XBOOLE_1:7;

end;

registration

cluster SCM+FSA-Data*-Loc -> non empty ;

end;

definition

func SCM+FSA-OK -> Function of SCM+FSA-Memory,(Segm 3) equals :: SCMFSA_1:def 4
(SCM+FSA-Memory --> 2) +* SCM-OK;

proof end;

end;

:: deftheorem SCMFSA_1:def 3 :

:: deftheorem defines SCM+FSA-OK SCMFSA_1:def 4 :

theorem :: SCMFSA_1:2

canceled;

theorem :: SCMFSA_1:3

canceled;

theorem :: SCMFSA_1:4

canceled;

::$CT 3

theorem Th2: :: SCMFSA_1:5

NAT in SCM+FSA-Memory

proof end;

theorem :: SCMFSA_1:6

canceled;

theorem :: SCMFSA_1:7

canceled;

::$CT 2

theorem :: SCMFSA_1:8

SCM+FSA-Memory = ({NAT} \/ SCM+FSA-Data-Loc) \/ SCM+FSA-Data*-Loc ;

definition

func SCM*-VAL -> ManySortedSet of Segm 3 equals :: SCMFSA_1:def 5
<%NAT,INT,(INT *)%>;

end;

:: deftheorem defines SCM*-VAL SCMFSA_1:def 5 :

Lm1: SCM+FSA-Data*-Loc misses SCM-Memory

proof end;

Lm2: dom SCM-OK c= dom SCM+FSA-OK

proof end;

Lm3: NAT in dom SCM+FSA-OK

proof end;

Lm4: SCM+FSA-OK . NAT = 0

proof end;

theorem Th4: :: SCMFSA_1:9

(SCM*-VAL * SCM+FSA-OK) . NAT = NAT

proof end;

Lm5: for b being Element of SCM+FSA-Data-Loc holds SCM+FSA-OK . b = 1

proof end;

theorem Th5: :: SCMFSA_1:10

for b being Element of SCM+FSA-Data-Loc holds (SCM*-VAL * SCM+FSA-OK) . b = INT

proof end;

Lm6: for f being Element of SCM+FSA-Data*-Loc holds SCM+FSA-OK . f = 2

proof end;

theorem Th6: :: SCMFSA_1:11

for f being Element of SCM+FSA-Data*-Loc holds (SCM*-VAL * SCM+FSA-OK) . f = INT *

proof end;

Lm7: dom SCM+FSA-OK = SCM+FSA-Memory
by PARTFUN1:def 2;

len <%NAT,INT,(INT *)%> = 3
by AFINSQ_1:39;

then rng SCM+FSA-OK c= dom SCM*-VAL
by RELAT_1:def 19;

then Lm8: dom (SCM*-VAL * SCM+FSA-OK) = SCM+FSA-Memory
by Lm7, RELAT_1:27;

registration

cluster SCM+FSA-OK * SCM*-VAL -> non-empty ;

proof end;

end;

definition

mode SCM+FSA-State is Element of product (SCM*-VAL * SCM+FSA-OK);

end;

theorem :: SCMFSA_1:12

canceled;

theorem :: SCMFSA_1:13

canceled;

theorem :: SCMFSA_1:14

canceled;

theorem :: SCMFSA_1:15

canceled;

theorem :: SCMFSA_1:16

canceled;

::$CT 5

theorem Th7: :: SCMFSA_1:17

for s being SCM+FSA-State
for I being Element of SCM-Instr holds s | SCM-Memory is SCM-State

proof end;

theorem Th8: :: SCMFSA_1:18

for s being SCM+FSA-State
for s1 being SCM-State holds s +* s1 is SCM+FSA-State

proof end;

definition

let s be SCM+FSA-State;
let u be Nat;

func SCM+FSA-Chg (s,u) -> SCM+FSA-State equals :: SCMFSA_1:def 6
s +* (NAT .--> u);

proof end;

end;

:: deftheorem defines SCM+FSA-Chg SCMFSA_1:def 6 :

definition

let s be SCM+FSA-State;
let t be Element of SCM+FSA-Data-Loc ;
let u be Integer;

func SCM+FSA-Chg (s,t,u) -> SCM+FSA-State equals :: SCMFSA_1:def 7
s +* (t .--> u);

proof end;

end;

:: deftheorem defines SCM+FSA-Chg SCMFSA_1:def 7 :

definition

let s be SCM+FSA-State;
let t be Element of SCM+FSA-Data*-Loc ;
let u be FinSequence of INT ;

func SCM+FSA-Chg (s,t,u) -> SCM+FSA-State equals :: SCMFSA_1:def 8
s +* (t .--> u);

proof end;

end;

:: deftheorem defines SCM+FSA-Chg SCMFSA_1:def 8 :

registration

let s be SCM+FSA-State;
let a be Element of SCM+FSA-Data-Loc ;

cluster s . a -> integer ;

proof end;

end;

definition

let s be SCM+FSA-State;
let a be Element of SCM+FSA-Data*-Loc ;
:: original: .
redefine func s . a -> FinSequence of INT ;
coherence

proof end;

end;

definition

let s be SCM+FSA-State;

func IC s -> Element of NAT equals :: SCMFSA_1:def 15
s . NAT;

proof end;

end;

:: deftheorem SCMFSA_1:def 9 :

:: deftheorem SCMFSA_1:def 10 :

:: deftheorem SCMFSA_1:def 11 :

:: deftheorem SCMFSA_1:def 12 :

:: deftheorem SCMFSA_1:def 13 :

:: deftheorem SCMFSA_1:def 14 :

:: deftheorem defines IC SCMFSA_1:def 15 :

definition

let x be Element of SCM+FSA-Instr ;
let s be SCM+FSA-State;

func SCM+FSA-Exec-Res (x,s) -> SCM+FSA-State means :: SCMFSA_1:def 16
ex x9 being Element of SCM-Instr ex s9 being SCM-State st
( x = x9 & s9 = s | SCM-Memory & it = s +* (SCM-Exec-Res (x9,s9)) ) if x `1_3 <= 8
ex i being Integer ex k being Nat st
( k = |.(s . (x int_addr2)).| & i = (s . (x coll_addr1)) /. k & it = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x int_addr1),i)),((IC s) + 1)) ) if x `1_3 = 9
ex f being FinSequence of INT ex k being Nat st
( k = |.(s . (x int_addr2)).| & f = (s . (x coll_addr1)) +* (k,(s . (x int_addr1))) & it = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x coll_addr1),f)),((IC s) + 1)) ) if x `1_3 = 10
it = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x int_addr3),(len (s . (x coll_addr2))))),((IC s) + 1)) if x `1_3 = 11
ex f being FinSequence of INT ex k being Nat st
( k = |.(s . (x int_addr3)).| & f = k |-> 0 & it = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x coll_addr2),f)),((IC s) + 1)) ) if x `1_3 = 12
ex i being Integer st
( i = 1 & it = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x int_addr),i)),((IC s) + 1)) ) if x `1_3 = 13
otherwise it = s;

proof end;

uniqueness ;
consistency ;

end;

:: deftheorem defines SCM+FSA-Exec-Res SCMFSA_1:def 16 :

definition

func SCM+FSA-Exec -> Action of SCM+FSA-Instr,(product (SCM*-VAL * SCM+FSA-OK)) means :: SCMFSA_1:def 17
for x being Element of SCM+FSA-Instr
for y being SCM+FSA-State holds (it . x) . y = SCM+FSA-Exec-Res (x,y);

proof end;

proof end;

end;

:: deftheorem defines SCM+FSA-Exec SCMFSA_1:def 17 :

theorem :: SCMFSA_1:19

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

proof end;

theorem :: SCMFSA_1:20

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

proof end;

theorem :: SCMFSA_1:21

for s being SCM+FSA-State
for u being Nat
for p being Element of SCM+FSA-Data*-Loc holds (SCM+FSA-Chg (s,u)) . p = s . p

proof end;

theorem :: SCMFSA_1:22

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

proof end;

theorem :: SCMFSA_1:23

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

proof end;

theorem :: SCMFSA_1:24

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

proof end;

theorem :: SCMFSA_1:25

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

proof end;

theorem :: SCMFSA_1:26

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

proof end;

theorem :: SCMFSA_1:27

for s being SCM+FSA-State
for t being Element of SCM+FSA-Data*-Loc
for u being FinSequence of INT holds (SCM+FSA-Chg (s,t,u)) . t = u

proof end;

theorem :: SCMFSA_1:28

for s being SCM+FSA-State
for t being Element of SCM+FSA-Data*-Loc
for u being FinSequence of INT
for mk being Element of SCM+FSA-Data*-Loc st mk <> t holds
(SCM+FSA-Chg (s,t,u)) . mk = s . mk

proof end;

theorem :: SCMFSA_1:29

for s being SCM+FSA-State
for t being Element of SCM+FSA-Data*-Loc
for u being FinSequence of INT
for a being Element of SCM+FSA-Data-Loc holds (SCM+FSA-Chg (s,t,u)) . a = s . a

proof end;

theorem :: SCMFSA_1:30

SCM+FSA-Data*-Loc misses SCM-Memory by Lm1;

theorem :: SCMFSA_1:31

canceled;

::$CT

theorem :: SCMFSA_1:32

dom (SCM*-VAL * SCM+FSA-OK) = SCM+FSA-Memory by Lm8;

theorem :: SCMFSA_1:33

for s being SCM+FSA-State holds dom s = SCM+FSA-Memory by Lm8, CARD_3:9;