:: On the compositions of macro instructions
:: by Andrzej Trybulec , Yatsuka Nakamura and Noriko Asamoto
::
:: Received June 20, 1996
:: Copyright (c) 1996-2021 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, SUBSET_1, AMI_1, SCMFSA_2, EXTPRO_1, FUNCT_4, AMI_3,
FUNCOP_1, RELAT_1, FUNCT_1, TARSKI, XBOOLE_0, CARD_1, CAT_1, NAT_1,
ARYTM_3, XXREAL_0, AMISTD_2, VALUED_1, FSM_1, GRAPHSP, ARYTM_1, INT_1,
COMPLEX1, PARTFUN1, FINSEQ_1, FINSEQ_2, SCMFSA6A, RELOC, MEMSTR_0,
SCMPDS_4, TURING_1, AMISTD_1, FRECHET, COMPOS_1, SCMPDS_5;
notations TARSKI, XBOOLE_0, SUBSET_1, CARD_1, ORDINAL1, NUMBERS, XCMPLX_0,
COMPLEX1, NAT_1, INT_1, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2, FINSEQ_1,
FINSEQ_2, FUNCT_4, DOMAIN_1, VALUED_1, AFINSQ_1, NAT_D, STRUCT_0,
MEMSTR_0, COMPOS_0, COMPOS_1, EXTPRO_1, FUNCT_7, SCMFSA_2, AMISTD_1,
AMISTD_2, FUNCOP_1, XXREAL_0, SCMFSA_M;
constructors WELLORD2, DOMAIN_1, XXREAL_0, INT_2, AMISTD_2, SCMFSA_2,
RELSET_1, VALUED_1, AMI_3, PRE_POLY, AMISTD_1, FUNCT_7, MEMSTR_0,
SCMFSA_1, SCMFSA_M, NAT_D, COMPOS_2, AFINSQ_1;
registrations XBOOLE_0, FUNCT_1, ORDINAL1, RELSET_1, FUNCOP_1, FINSET_1,
XREAL_0, INT_1, SCMFSA_2, FUNCT_4, RELAT_1, VALUED_1, SCMFSA10, AMISTD_2,
COMPOS_1, EXTPRO_1, AMI_3, COMPOS_0, NAT_1, AMISTD_1, COMPOS_2, AFINSQ_1;
requirements NUMERALS, REAL, SUBSET, BOOLE, ARITHM;
begin
reserve l, m, n for Nat,
i,j,k for Instruction of SCM+FSA,
I,J,K for Program of SCM+FSA;
::$CD
definition
let P be preProgram of SCM+FSA;
func Directed P -> preProgram of SCM+FSA equals
:: SCMFSA6A:def 2
P +~ (halt SCM+FSA,goto card P);
projectivity;
end;
registration
let I be Program of SCM+FSA;
cluster Directed I -> initial non empty;
end;
theorem :: SCMFSA6A:1
not halt SCM+FSA in rng Directed I;
theorem :: SCMFSA6A:2
Reloc(Directed I, m) = ((id the InstructionsF of
SCM+FSA) +* (halt SCM+FSA .--> goto (m + card I)))* Reloc(I, m);
reserve a,b for Int-Location,
f for FinSeq-Location,
s,s1,s2 for State of SCM+FSA;
theorem :: SCMFSA6A:3
InsCode i in {0,6,7,8} or Exec(i,s).IC SCM+FSA = IC s + 1;
::$CT 4
theorem :: SCMFSA6A:8
for s1,s2 being State of SCM+FSA, n being Nat, i being
Instruction of SCM+FSA holds IC s1 + n = IC s2 & DataPart s1 = DataPart s2
implies IC Exec(i,s1) + n = IC Exec(IncAddr(i,n),s2) & DataPart Exec(i,s1) =
DataPart Exec(IncAddr(i,n),s2);
::$CT 6
begin :: The composition of macroinstructions
definition
::$CD
let I,J be Program of SCM+FSA;
func I ";" J -> Program of SCM+FSA equals
:: SCMFSA6A:def 4
stop Directed I ';' J;
end;
registration
let I be Program of SCM+FSA, J be halt-ending Program of SCM+FSA;
cluster I ";" J -> halt-ending;
end;
registration
let P be preProgram of SCM+FSA;
cluster Directed P -> halt-free;
end;
registration
cluster halt-free for Program of SCM+FSA;
end;
registration
let I be Program of SCM+FSA, J be unique-halt Program of SCM+FSA;
cluster I ";" J -> unique-halt;
end;
theorem :: SCMFSA6A:15
for I,J being Program of SCM+FSA, l being Nat
st l in dom I & I.l <> halt SCM+FSA holds (I ";" J).l = I.l;
theorem :: SCMFSA6A:16
for I,J being Program of SCM+FSA holds Directed I c= I ";" J;
theorem :: SCMFSA6A:17
for I,J being Program of SCM+FSA holds dom I c= dom (I ";" J);
theorem :: SCMFSA6A:18
for I,J being Program of SCM+FSA holds I +* (I ";" J) = (I ";" J);
begin :: The compostion of instruction and macroinstructions
definition
let i, J;
func i ";" J -> Program of SCM+FSA equals
:: SCMFSA6A:def 5
Macro i ";" J;
end;
definition
let I, j;
func I ";" j -> Program of SCM+FSA equals
:: SCMFSA6A:def 6
I ";" Macro j;
end;
definition
let i,j;
func i ";" j -> Program of SCM+FSA equals
:: SCMFSA6A:def 7
Macro i ";" Macro j;
end;
registration
cluster sequential for Instruction of SCM+FSA;
end;
registration
cluster sequential -> No-StopCode for Instruction of SCM+FSA;
end;
registration let i,j be sequential Instruction of SCM+FSA;
cluster i ";" j -> halt-ending unique-halt;
end;
registration
let I be MacroInstruction of SCM+FSA,
j be sequential Instruction of SCM+FSA;
cluster I ";" j -> halt-ending unique-halt;
end;
registration
let i be sequential Instruction of SCM+FSA,
J be MacroInstruction of SCM+FSA;
cluster i ";" J -> halt-ending unique-halt;
end;
theorem :: SCMFSA6A:19
i ";" j = Macro i ";" j;
theorem :: SCMFSA6A:20
i ";" j = i ";" Macro j;
theorem :: SCMFSA6A:21
card(I ";" J) = card I + card J;
theorem :: SCMFSA6A:22
for I being preProgram of SCM+FSA
holds I is halt-free implies Directed I = I;
theorem :: SCMFSA6A:23
for I being preProgram of SCM+FSA, k being Element of NAT holds
Reloc(Directed I,k) = Reloc(I,k) +~ (halt SCM+FSA,goto(card I + k));
theorem :: SCMFSA6A:24
for I,J being Program of SCM+FSA holds Directed (I ";" J) = I ";" Directed J;
theorem :: SCMFSA6A:25
I ";" J ";" K = I ";" (J ";" K);
theorem :: SCMFSA6A:26
I ";" J ";" k = I ";" (J ";" k);
theorem :: SCMFSA6A:27
I ";" j ";" K = I ";" (j ";" K);
theorem :: SCMFSA6A:28
I ";" j ";" k = I ";" (j ";" k);
theorem :: SCMFSA6A:29
i ";" J ";" K = i ";" (J ";" K);
theorem :: SCMFSA6A:30
i ";" J ";" k = i ";" (J ";" k);
theorem :: SCMFSA6A:31
i ";" j ";" K = i ";" (j ";" K);
theorem :: SCMFSA6A:32
i ";" j ";" k = i ";" (j ";" k);
theorem :: SCMFSA6A:33
card(i ";" J) = card J + 2;
theorem :: SCMFSA6A:34
card(I ";" j) = card I + 2;
theorem :: SCMFSA6A:35
card(i ";" j) = 4;
theorem :: SCMFSA6A:36
for I being preProgram of SCM+FSA
holds card Directed I = card I;
theorem :: SCMFSA6A:37
for I being Program of SCM+FSA
holds card stop Directed I = card stop I;
theorem :: SCMFSA6A:38
Reloc(J,card I) c= I ";" J;
theorem :: SCMFSA6A:39
dom(I ";" J) = dom I \/ dom Reloc(J, card I);
theorem :: SCMFSA6A:40
n in dom Reloc(J,card I)
implies (I ";" J).n = Reloc(J,card I).n;
begin :: closedness
registration let I be really-closed Program of SCM+FSA;
cluster stop Directed I -> really-closed;
end;
registration let I,J be really-closed Program of SCM+FSA;
cluster I ";" J -> really-closed;
end;
theorem :: SCMFSA6A:41
for I,J being MacroInstruction of SCM+FSA, n being Nat
st n < LastLoc I holds (I ";" J).n = I.n;