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

### On the Composition of Macro Instructions. Part II

by
Noriko Asamoto,
Yatsuka Nakamura,
Piotr Rudnicki, and
Andrzej Trybulec

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

```environ

vocabulary FUNCT_1, RELAT_1, FUNCT_4, BOOLE, AMI_1, SCMFSA_2, SCMFSA6A, AMI_3,
CAT_1, SCM_1, INT_1, FUNCOP_1, FUNCT_7, SF_MASTR, AMI_5, FINSEQ_1, RELOC,
CARD_1, SCMFSA6B, CARD_3;
notation TARSKI, XBOOLE_0, NUMBERS, XCMPLX_0, XREAL_0, NAT_1, INT_1, RELAT_1,
FUNCT_1, FUNCT_2, FINSEQ_1, CARD_1, CQC_LANG, FUNCT_4, STRUCT_0, AMI_1,
AMI_3, SCM_1, AMI_5, FUNCT_7, SCMFSA_2, SCMFSA_4, SCMFSA_5, SCMFSA6A,
SF_MASTR;
constructors SCM_1, SCMFSA6A, SF_MASTR, FUNCT_7, SCMFSA_5, AMI_5, NAT_1,
MEMBERED;
clusters AMI_1, SCMFSA_2, FUNCT_1, SCMFSA_4, INT_1, SCMFSA6A, SF_MASTR,
CQC_LANG, RELSET_1, FRAENKEL, XREAL_0, MEMBERED, NUMBERS, ORDINAL2;
requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;

begin

canceled 2;

theorem :: SCMFSA6B:3
for f, g being Function, A being set st A /\ dom f c= A /\ dom g
holds (f+*g|A)|A = g|A;

begin

reserve m, n for Nat,
x for set,
i for Instruction of SCM+FSA,
I for Macro-Instruction,
a for Int-Location, f for FinSeq-Location,
l, l1 for Instruction-Location of SCM+FSA,
s,s1,s2 for State of SCM+FSA;

theorem :: SCMFSA6B:4
Start-At insloc 0 c= Initialized I;

theorem :: SCMFSA6B:5
I +* Start-At insloc n c= s implies I c= s;

theorem :: SCMFSA6B:6
(I +* Start-At insloc n)|the Instruction-Locations of SCM+FSA = I;

theorem :: SCMFSA6B:7
x in dom I implies I.x = (I +* Start-At insloc n).x;

theorem :: SCMFSA6B:8
Initialized I c= s implies I +* Start-At insloc 0 c= s;

theorem :: SCMFSA6B:9
not a in dom Start-At l;

theorem :: SCMFSA6B:10
not f in dom Start-At l;

theorem :: SCMFSA6B:11
not l1 in dom Start-At l;

theorem :: SCMFSA6B:12
not a in dom (I+*Start-At l);

theorem :: SCMFSA6B:13
not f in dom (I+*Start-At l);

theorem :: SCMFSA6B:14
s+*I+*Start-At insloc 0 = s+*Start-At insloc 0+*I;

begin ::  General theory

reserve N for non empty with_non-empty_elements set;

theorem :: SCMFSA6B:15
s = Following s implies for n holds (Computation s).n = s;

theorem :: SCMFSA6B:16
for S being halting IC-Ins-separated definite
(non empty non void AMI-Struct over N),
s being State of S st s is halting
holds Result s = (Computation s).LifeSpan s;

definition let N;
let S be IC-Ins-separated definite (non empty non void AMI-Struct over N);
let s be State of S, l be Instruction-Location of S, i be Instruction of S;
redefine func s+*(l,i) -> State of S;
end;

definition
let s be State of SCM+FSA, li be Int-Location, k be Integer;
redefine func s+*(li,k) -> State of SCM+FSA;
end;

theorem :: SCMFSA6B:17
for S being steady-programmed IC-Ins-separated definite
(non empty non void AMI-Struct over N)
for s being State of S, n
holds s|the Instruction-Locations of S
= ((Computation s).n)|the Instruction-Locations of S;

begin

definition let I be Macro-Instruction, s be State of SCM+FSA;
func IExec(I,s) -> State of SCM+FSA equals
:: SCMFSA6B:def 1

Result(s+*Initialized I) +* s|the Instruction-Locations of SCM+FSA;
end;

definition let I be Macro-Instruction;
attr I is paraclosed means
:: SCMFSA6B:def 2
for s being State of SCM+FSA, n being Nat
st I +* Start-At insloc 0 c= s
holds IC (Computation s).n in dom I;

attr I is parahalting means
:: SCMFSA6B:def 3
I +* Start-At insloc 0 is halting;

attr I is keeping_0 means
:: SCMFSA6B:def 4
::Lkeep
for s being State of SCM+FSA st I +* Start-At insloc 0 c= s
for k being Nat holds ((Computation s).k).intloc 0 = s.intloc 0;
end;

definition
cluster parahalting Macro-Instruction;
end;

theorem :: SCMFSA6B:18
for I being parahalting Macro-Instruction
st I +* Start-At insloc 0 c= s holds s is halting;

theorem :: SCMFSA6B:19
for I being parahalting Macro-Instruction
st Initialized I c= s holds s is halting;

definition let I be parahalting Macro-Instruction;
cluster Initialized I -> halting;
end;

theorem :: SCMFSA6B:20
s2 +*(IC s2, goto IC s2) is not halting;

theorem :: SCMFSA6B:21
s1,s2 equal_outside the Instruction-Locations of SCM+FSA &
I c= s1 & I c= s2 &
(for m st m < n holds IC((Computation s2).m) in dom I)
implies
for m st m <= n holds
(Computation s1).m, (Computation s2 ).m equal_outside
the Instruction-Locations of SCM+FSA;

definition
cluster parahalting -> paraclosed Macro-Instruction;

cluster keeping_0 -> paraclosed Macro-Instruction;
end;

theorem :: SCMFSA6B:22
for I being parahalting Macro-Instruction,
holds not a in UsedIntLoc I implies (IExec(I, s)).a = s.a;

theorem :: SCMFSA6B:23
for I being parahalting Macro-Instruction
holds not f in UsedInt*Loc I implies (IExec(I, s)).f = s.f;

theorem :: SCMFSA6B:24
IC s = l & s.l = goto l implies s is not halting;

definition
cluster parahalting -> non empty Macro-Instruction;
end;

theorem :: SCMFSA6B:25  ::T9'
for I being parahalting Macro-Instruction holds dom I <> {};

theorem :: SCMFSA6B:26  ::T9
for I being parahalting Macro-Instruction holds insloc 0 in dom I;

theorem :: SCMFSA6B:27  ::T0
for J being parahalting Macro-Instruction st J +* Start-At insloc 0 c= s1
for n being Nat st ProgramPart Relocated(J,n) c= s2 &
IC s2 = insloc n &
s1 | (Int-Locations \/ FinSeq-Locations)
= s2 | (Int-Locations \/ FinSeq-Locations)
for i being Nat holds
IC (Computation s1).i + n = IC (Computation s2).i &
IncAddr(CurInstr ((Computation s1).i),n) = CurInstr ((Computation s2).i) &
(Computation s1).i | (Int-Locations \/ FinSeq-Locations)
= (Computation s2).i | (Int-Locations \/ FinSeq-Locations);

theorem :: SCMFSA6B:28  ::T13
for I being parahalting Macro-Instruction st
I +* Start-At insloc 0 c= s1 & I +* Start-At insloc 0 c= s2 &
s1,s2 equal_outside the Instruction-Locations of SCM+FSA holds
for k being Nat holds
(Computation s1).k, (Computation s2).k
equal_outside the Instruction-Locations of SCM+FSA &
CurInstr (Computation s1).k = CurInstr (Computation s2).k;

theorem :: SCMFSA6B:29  ::T14
for I being parahalting Macro-Instruction st
I +* Start-At insloc 0 c= s1 & I +* Start-At insloc 0 c= s2 &
s1,s2 equal_outside the Instruction-Locations of SCM+FSA holds
LifeSpan s1 = LifeSpan s2 &
Result s1, Result s2 equal_outside the Instruction-Locations of SCM+FSA;

theorem :: SCMFSA6B:30  ::T27
for I being parahalting Macro-Instruction
holds IC IExec(I,s) = IC Result (s +* Initialized I);

theorem :: SCMFSA6B:31
for I being non empty Macro-Instruction
holds insloc 0 in dom I & insloc 0 in dom Initialized I &
insloc 0 in dom (I +* Start-At insloc 0);

theorem :: SCMFSA6B:32
x in dom Macro i iff x = insloc 0 or x = insloc 1;

theorem :: SCMFSA6B:33
(Macro i).(insloc 0) = i &
(Macro i).(insloc 1) = halt SCM+FSA &
(Initialized Macro i).insloc 0 = i &
(Initialized Macro i).insloc 1 = halt SCM+FSA &
((Macro i) +* Start-At insloc 0).insloc 0 = i;

theorem :: SCMFSA6B:34
Initialized I c= s implies IC s = insloc 0;

definition
cluster keeping_0 parahalting Macro-Instruction;
end;

theorem :: SCMFSA6B:35
for I being keeping_0 parahalting Macro-Instruction
holds IExec(I, s).intloc 0 = 1;

begin :: The composition of macroinstructions

theorem :: SCMFSA6B:36
for I being paraclosed Macro-Instruction, J being Macro-Instruction
st I +* Start-At insloc 0 c= s & s is halting
for m st m <= LifeSpan s
holds (Computation s).m,(Computation(s+*(I ';' J))).m
equal_outside the Instruction-Locations of SCM+FSA;

theorem :: SCMFSA6B:37  ::Lemma01
for I being paraclosed Macro-Instruction
st s +*I is halting & Directed I c= s & Start-At insloc 0 c= s holds
IC (Computation s).(LifeSpan (s +*I) + 1)
= insloc card I;

theorem :: SCMFSA6B:38  ::Lemma02
for I being paraclosed Macro-Instruction
st s +*I is halting & Directed I c= s & Start-At insloc 0 c= s
holds
(Computation s).(LifeSpan (s +*I)) |
(Int-Locations \/ FinSeq-Locations) =
(Computation s).(LifeSpan (s +*I) + 1) |
(Int-Locations \/ FinSeq-Locations);

theorem :: SCMFSA6B:39  ::Lemma0
for I being parahalting Macro-Instruction
st Initialized I c= s holds
for k being Nat st k <= LifeSpan s holds
CurInstr (Computation (s +* Directed I)).k <> halt SCM+FSA;

theorem :: SCMFSA6B:40
for I being paraclosed Macro-Instruction
st s +* (I +* Start-At insloc 0) is halting
for J being Macro-Instruction, k being Nat
st k <= LifeSpan (s +* (I +* Start-At insloc 0))
holds (Computation (s +* (I +* Start-At insloc 0))).k,
(Computation (s +* ((I ';' J) +* Start-At insloc 0))).k
equal_outside the Instruction-Locations of SCM+FSA;

definition
let I, J be parahalting Macro-Instruction;
cluster I ';' J -> parahalting;
end;

theorem :: SCMFSA6B:41
for I being keeping_0 Macro-Instruction
st not s +* (I +* Start-At insloc 0) is halting
for J being Macro-Instruction, k being Nat
holds (Computation (s +* (I +* Start-At insloc 0))).k,
(Computation (s +* ((I ';' J) +* Start-At insloc 0))).k
equal_outside the Instruction-Locations of SCM+FSA;

theorem :: SCMFSA6B:42
for I being keeping_0 Macro-Instruction
st s +* I is halting
for J being paraclosed Macro-Instruction
st (I ';' J) +* Start-At insloc 0 c= s
for k being Nat
holds (Computation (Result(s +*I)
+* (J +* Start-At insloc 0))).k
+* Start-At (IC (Computation ((Result(s +*I))
+* (J +* Start-At insloc 0))).k + card I),
(Computation (s +* (I ';' J))).
(LifeSpan (s +* I)+1+k)
equal_outside the Instruction-Locations of SCM+FSA;

definition
let I, J be keeping_0 Macro-Instruction;
cluster I ';' J -> keeping_0;
end;

theorem :: SCMFSA6B:43  ::T22
for I being keeping_0 parahalting Macro-Instruction,
J being parahalting Macro-Instruction
holds
LifeSpan (s +* Initialized (I ';' J))
= LifeSpan (s +* Initialized I) + 1
+ LifeSpan (Result (s +* Initialized I) +* Initialized J);

theorem :: SCMFSA6B:44
for I being keeping_0 parahalting Macro-Instruction,
J being parahalting Macro-Instruction
holds
IExec(I ';' J,s) =
IExec(J,IExec(I,s)) +* Start-At (IC IExec(J,IExec(I,s)) + card I);

```