Journal of Formalized Mathematics
Volume 8, 1996
University of Bialystok
Copyright (c) 1996 Association of Mizar Users

### On the Compositions of Macro Instructions. Part I

by
Andrzej Trybulec,
Yatsuka Nakamura, and
Noriko Asamoto

MML identifier: SCMFSA6A
[ Mizar article, MML identifier index ]

```environ

vocabulary FUNCT_1, RELAT_1, FUNCT_4, FUNCT_7, BOOLE, CAT_1, AMI_3, AMI_1,
SCMFSA_2, CARD_1, FUNCOP_1, FINSET_1, TARSKI, AMI_5, RELOC, INT_1, AMI_2,
ARYTM_1, NAT_1, ABSVALUE, FINSEQ_1, FINSEQ_2, SCMFSA6A, FINSEQ_4;
notation TARSKI, XBOOLE_0, ENUMSET1, SUBSET_1, NUMBERS, XCMPLX_0, XREAL_0,
NAT_1, INT_1, ABSVALUE, RELAT_1, FUNCT_1, FUNCT_2, FINSEQ_1, FINSEQ_2,
FINSEQ_4, CARD_1, CQC_LANG, FINSET_1, FUNCT_4, STRUCT_0, AMI_1, AMI_3,
AMI_5, FUNCT_7, SCMFSA_2, SCMFSA_4, SCMFSA_5;
constructors SCMFSA_4, WELLORD2, SCMFSA_5, NAT_1, AMI_5, ENUMSET1, FUNCT_7,
RELOC, FINSEQ_4, MEMBERED;
clusters XBOOLE_0, AMI_1, SCMFSA_2, FUNCT_1, FINSET_1, PRELAMB, FUNCT_7,
SCMFSA_4, RELSET_1, INT_1, FRAENKEL, MEMBERED, NUMBERS, ORDINAL2;
requirements NUMERALS, REAL, SUBSET, BOOLE, ARITHM;

begin :: Preliminaries

theorem :: SCMFSA6A:1
for f,g being Function, x,y being set st g c= f & not x in dom g
holds g c= f+*(x,y);

theorem :: SCMFSA6A:2
for f,g being Function, A being set st f|A = g|A &
f,g equal_outside A holds f = g;

theorem :: SCMFSA6A:3
for f being Function, a,b,A being set st a in A
holds f,f+*(a,b) equal_outside A;

theorem :: SCMFSA6A:4
for f being Function, a,b,A being set holds
a in A or (f+*(a,b))|A = f|A;

theorem :: SCMFSA6A:5
for f,g being Function, a,b,A being set st f|A = g|A
holds (f+*(a,b))|A = (g+*(a,b))|A;

theorem :: SCMFSA6A:6
for f,g,h being Function st f c= h & g c= h
holds f +* g c= h;

theorem :: SCMFSA6A:7
for a,b being set, f being Function holds
a.-->b c= f iff a in dom f & f.a = b;

theorem :: SCMFSA6A:8  ::Lemma12
for f being Function, A being set holds
dom (f | (dom f \ A)) = dom f \ A;

for f,g being Function, D being set st D c= dom f & D c= dom g holds
f | D = g | D iff for x being set st x in D holds f.x = g.x;

theorem :: SCMFSA6A:10  ::Lemma14
for f being Function, D being set holds
f | D = f | (dom f /\ D);

theorem :: SCMFSA6A:11  ::Lemma7
for f,g,h being Function, A being set holds
f, g equal_outside A implies f +* h, g +* h equal_outside A;

theorem :: SCMFSA6A:12  ::Lemma7'
for f,g,h being Function, A being set holds
f, g equal_outside A implies h +* f, h +* g equal_outside A;

theorem :: SCMFSA6A:13
for f,g,h being Function
holds f +* h = g +* h iff f,g equal_outside dom h;

begin

definition
mode Macro-Instruction is initial programmed FinPartState of SCM+FSA;
end;

reserve l, m, n for Nat,
i,j,k for Instruction of SCM+FSA,
I,J,K for Macro-Instruction;

definition let I be programmed FinPartState of SCM+FSA;
func Directed I -> programmed FinPartState of SCM+FSA equals
:: SCMFSA6A:def 1
((id the Instructions of SCM+FSA) +*
(halt SCM+FSA .--> goto insloc card I))*I;
end;

theorem :: SCMFSA6A:14
dom Directed I = dom I;

definition let I be Macro-Instruction;
cluster Directed I -> initial;
end;

definition let i;
func Macro i -> Macro-Instruction equals
:: SCMFSA6A:def 2
(insloc 0,insloc 1) --> (i,halt SCM+FSA);
end;

definition let i;
cluster Macro i -> non empty;
end;

theorem :: SCMFSA6A:15
for P being Macro-Instruction, n holds
n < card P iff insloc n in dom P;

definition let I be initial FinPartState of SCM+FSA;
cluster ProgramPart I -> initial;
end;

theorem :: SCMFSA6A:16
dom I misses dom ProgramPart Relocated(J, card I);

theorem :: SCMFSA6A:17
for I being programmed FinPartState of SCM+FSA
holds card ProgramPart Relocated(I, m) = card I;

theorem :: SCMFSA6A:18
not halt SCM+FSA in rng Directed I;

theorem :: SCMFSA6A:19
ProgramPart Relocated(Directed I, m) =
((id the Instructions of SCM+FSA) +*
(halt SCM+FSA .--> goto insloc(m + card I)))*
ProgramPart Relocated(I, m);

theorem :: SCMFSA6A:20
for I,J being FinPartState of SCM+FSA holds
ProgramPart(I +* J) = ProgramPart I +* ProgramPart J;

theorem :: SCMFSA6A:21
for I,J being FinPartState of SCM+FSA holds
ProgramPart Relocated(I +* J, n) =
ProgramPart Relocated(I,n) +* ProgramPart Relocated(J,n);

theorem :: SCMFSA6A:22
ProgramPart Relocated(ProgramPart Relocated(I, m), n)
= ProgramPart Relocated(I, m + n);

reserve a,b for Int-Location, f for FinSeq-Location,
s,s1,s2 for State of SCM+FSA;

definition let I be FinPartState of SCM+FSA;
func Initialized I -> FinPartState of SCM+FSA equals
:: SCMFSA6A:def 3
I +* ((intloc 0) .--> 1) +* Start-At(insloc 0);
end;

theorem :: SCMFSA6A:23
InsCode i in {0,6,7,8} or Exec(i,s).IC SCM+FSA = Next IC s;

theorem :: SCMFSA6A:24
IC SCM+FSA in dom Initialized I;

theorem :: SCMFSA6A:25
IC Initialized I = insloc 0;

theorem :: SCMFSA6A:26
I c= Initialized I;

theorem :: SCMFSA6A:27
for N being set, A being AMI-Struct over N, s being State of A,
I being programmed FinPartState of A holds
s,s+*I equal_outside the Instruction-Locations of A;

theorem :: SCMFSA6A:28
for s1,s2 being State of SCM+FSA
st IC s1 = IC s2 &
(for a being Int-Location holds s1.a = s2.a) &
for f being FinSeq-Location holds s1.f = s2.f
holds s1,s2 equal_outside the Instruction-Locations of SCM+FSA;

theorem :: SCMFSA6A:29
for N being with_non-empty_elements set,
S being realistic IC-Ins-separated definite
(non empty non void AMI-Struct over N),
s1, s2 being State of S holds
s1,s2 equal_outside the Instruction-Locations of S implies
IC s1 = IC s2;

theorem :: SCMFSA6A:30
s1,s2 equal_outside the Instruction-Locations of SCM+FSA implies
for a being Int-Location holds s1.a = s2.a;

theorem :: SCMFSA6A:31
s1,s2 equal_outside the Instruction-Locations of SCM+FSA implies
for f being FinSeq-Location holds s1.f = s2.f;

theorem :: SCMFSA6A:32
s1,s2 equal_outside the Instruction-Locations of SCM+FSA implies
Exec(i,s1),Exec(i,s2) equal_outside the Instruction-Locations of SCM+FSA;

theorem :: SCMFSA6A:33
(Initialized I)|the Instruction-Locations of SCM+FSA = I;

scheme SCMFSAEx{ F(set) -> Element of the Instructions of SCM+FSA,
G(set) -> Integer, H(set) -> FinSequence of INT,
I() -> Instruction-Location of SCM+FSA }:
ex S being State of SCM+FSA st IC S = I() &
for i being Nat holds
S.insloc i = F(i) & S.intloc i = G(i) & S.fsloc i = H(i);

theorem :: SCMFSA6A:34  ::T12
for s being State of SCM+FSA holds
dom s = Int-Locations \/ FinSeq-Locations \/ {IC SCM+FSA} \/
the Instruction-Locations of SCM+FSA;

theorem :: SCMFSA6A:35  ::T12'
for s being State of SCM+FSA, x being set st x in dom s holds
x is Int-Location or x is FinSeq-Location or
x = IC SCM+FSA or x is Instruction-Location of SCM+FSA;

theorem :: SCMFSA6A:36  ::T29
for s1,s2 being State of SCM+FSA holds
(for l being Instruction-Location of SCM+FSA holds s1.l = s2.l)
iff s1 | the Instruction-Locations of SCM+FSA =
s2 | the Instruction-Locations of SCM+FSA;

theorem :: SCMFSA6A:37  ::T32
for i being Instruction-Location of SCM+FSA holds
not i in Int-Locations \/ FinSeq-Locations &
not IC SCM+FSA in Int-Locations \/ FinSeq-Locations;

theorem :: SCMFSA6A:38  ::T28
for s1,s2 being State of SCM+FSA holds
((for a being Int-Location holds s1.a = s2.a) &
for f being FinSeq-Location holds s1.f = s2.f)
iff s1 | (Int-Locations \/ FinSeq-Locations) =
s2 | (Int-Locations \/ FinSeq-Locations);

theorem :: SCMFSA6A:39  ::T19
for s1,s2 being State of SCM+FSA st
s1,s2 equal_outside the Instruction-Locations of SCM+FSA holds
s1 | (Int-Locations \/ FinSeq-Locations) =
s2 | (Int-Locations \/ FinSeq-Locations);

theorem :: SCMFSA6A:40  ::T21
for s,ss being State of SCM+FSA, A being set holds
(ss +* s | A) | A = s | A;

theorem :: SCMFSA6A:41  ::Lemma
for s1,s2 being State of SCM+FSA, n being Nat,
i being Instruction of SCM+FSA holds
IC s1 + n = IC s2 &
s1 | (Int-Locations \/ FinSeq-Locations) =
s2 | (Int-Locations \/ FinSeq-Locations)
implies
IC Exec(i,s1) + n = IC Exec(IncAddr(i,n),s2) &
Exec(i,s1) | (Int-Locations \/ FinSeq-Locations) =

theorem :: SCMFSA6A:42  ::T18
for I,J being Macro-Instruction holds
I,J equal_outside the Instruction-Locations of SCM+FSA;

theorem :: SCMFSA6A:43  ::T3
for I being Macro-Instruction holds
dom Initialized I = dom I \/ {intloc 0} \/ {IC SCM+FSA};

theorem :: SCMFSA6A:44  ::T2
for I being Macro-Instruction, x being set st x in dom Initialized I holds
x in dom I or x = intloc 0 or x = IC SCM+FSA;

theorem :: SCMFSA6A:45  ::T3'
for I being Macro-Instruction holds intloc 0 in dom Initialized I;

theorem :: SCMFSA6A:46  ::T5
for I being Macro-Instruction holds
(Initialized I).intloc 0 = 1 & (Initialized I).IC SCM+FSA = insloc 0;

theorem :: SCMFSA6A:47  ::T7
for I being Macro-Instruction holds
not intloc 0 in dom I & not IC SCM+FSA in dom I;

theorem :: SCMFSA6A:48  ::T36
for I being Macro-Instruction, a being Int-Location st a <> intloc 0 holds
not a in dom Initialized I;

theorem :: SCMFSA6A:49  ::T37
for I being Macro-Instruction, f being FinSeq-Location holds
not f in dom Initialized I;

theorem :: SCMFSA6A:50  ::T8
for I being Macro-Instruction, x being set st x in dom I holds
I.x = (Initialized I).x;

theorem :: SCMFSA6A:51  ::T10'
for I,J being Macro-Instruction
for s being State of SCM+FSA st Initialized J c= s holds
s +* Initialized I = s +* I;

theorem :: SCMFSA6A:52  ::T10
for I,J being Macro-Instruction
for s being State of SCM+FSA st Initialized J c= s holds
Initialized I c= s +* I;

theorem :: SCMFSA6A:53  ::T23
for I,J being Macro-Instruction
for s being State of SCM+FSA holds
s +* Initialized I, s +* Initialized J
equal_outside the Instruction-Locations of SCM+FSA;

begin :: The composition of macroinstructions

definition let I,J be Macro-Instruction;
func I ';' J -> Macro-Instruction equals
:: SCMFSA6A:def 4
Directed I +* ProgramPart Relocated(J, card I);
end;

theorem :: SCMFSA6A:54
for I,J being Macro-Instruction, l being Instruction-Location of SCM+FSA
st l in dom I & I.l <> halt SCM+FSA
holds (I ';' J).l = I.l;

theorem :: SCMFSA6A:55  ::T16
for I,J being Macro-Instruction holds
Directed I c= I ';' J;

theorem :: SCMFSA6A:56  ::T4
for I,J being Macro-Instruction holds
dom I c= dom (I ';' J);

theorem :: SCMFSA6A:57  ::T6
for I,J being Macro-Instruction holds
I +* (I ';' J) = (I ';' J);

theorem :: SCMFSA6A:58  ::T1
for I,J being Macro-Instruction holds
Initialized I +* (I ';' J) = Initialized (I ';' J);

begin :: The compostion of instruction and macroinstructions

definition let i, J;
func i ';' J -> Macro-Instruction equals
:: SCMFSA6A:def 5
Macro i ';' J;
end;

definition let I, j;
func I ';' j -> Macro-Instruction equals
:: SCMFSA6A:def 6
I ';' Macro j;
end;

definition let i,j;
func i ';' j -> Macro-Instruction equals
:: SCMFSA6A:def 7
Macro i ';' Macro j;
end;

theorem :: SCMFSA6A:59
i ';' j = Macro i ';' j;

theorem :: SCMFSA6A:60
i ';' j = i ';' Macro j;

theorem :: SCMFSA6A:61
card(I ';' J) = card I + card J;

theorem :: SCMFSA6A:62
I ';' J ';' K = I ';' (J ';' K);

theorem :: SCMFSA6A:63
I ';' J ';' k = I ';' (J ';' k);

theorem :: SCMFSA6A:64
I ';' j ';' K = I ';' (j ';' K);

theorem :: SCMFSA6A:65
I ';' j ';' k = I ';' (j ';' k);

theorem :: SCMFSA6A:66
i ';' J ';' K = i ';' (J ';' K);

theorem :: SCMFSA6A:67
i ';' J ';' k = i ';' (J ';' k);

theorem :: SCMFSA6A:68
i ';' j ';' K = i ';' (j ';' K);

theorem :: SCMFSA6A:69
i ';' j ';' k = i ';' (j ';' k);
```