SCMFSA6A: On the compositions of macro instructions

:: 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

canceled;

::$CD

definition

let P be preProgram of SCM+FSA;

func Directed P -> preProgram of SCM+FSA equals :: SCMFSA6A:def 1
P +~ ((halt SCM+FSA),(goto (card P)));

coherence ;
projectivity by FUNCT_4:127;

end;

:: deftheorem defines Directed SCMFSA6A:def 1 :

registration

let I be Program of ;

cluster Directed I -> non empty initial ;

proof end;

end;

theorem :: SCMFSA6A:1

for I being Program of holds not halt SCM+FSA in rng (Directed I) by FUNCT_4:100;

theorem :: SCMFSA6A:2

for m being Nat
for I being Program of holds Reloc ((Directed I),m) = ((id the InstructionsF of SCM+FSA) +* ((halt SCM+FSA) .--> (goto (m + (card I))))) * (Reloc (I,m))

proof end;

set q = (intloc 0) .--> 1;

set f = the_Values_of SCM+FSA;

theorem Th3: :: SCMFSA6A:3

for i being Instruction of SCM+FSA
for s being State of SCM+FSA holds
( InsCode i in {0,6,7,8} or (Exec (i,s)) . (IC ) = (IC s) + 1 )

proof end;

theorem :: SCMFSA6A:4

canceled;

theorem :: SCMFSA6A:5

canceled;

theorem :: SCMFSA6A:6

canceled;

theorem :: SCMFSA6A:7

canceled;

::$CT 4

theorem :: SCMFSA6A:8

for s1, s2 being State of SCM+FSA
for n being Nat
for i being Instruction of SCM+FSA st (IC s1) + n = IC s2 & DataPart s1 = DataPart s2 holds
( (IC (Exec (i,s1))) + n = IC (Exec ((IncAddr (i,n)),s2)) & DataPart (Exec (i,s1)) = DataPart (Exec ((IncAddr (i,n)),s2)) )

proof end;

theorem :: SCMFSA6A:9

canceled;

theorem :: SCMFSA6A:10

canceled;

theorem :: SCMFSA6A:11

canceled;

theorem :: SCMFSA6A:12

canceled;

theorem :: SCMFSA6A:13

canceled;

theorem :: SCMFSA6A:14

canceled;

definition

let I, J be Program of ;

func I ";" J -> Program of equals :: SCMFSA6A:def 3
(stop (Directed I)) ';' J;

end;

:: deftheorem SCMFSA6A:def 2 :

:: deftheorem defines ";" SCMFSA6A:def 3 :

registration

let I be Program of ;
let J be halt-ending Program of ;

cluster I ";" J -> halt-ending ;

end;

registration

let P be preProgram of SCM+FSA;

cluster Directed P -> halt-free ;

correctness by FUNCT_4:100;

end;

registration

cluster Relation-like NAT -defined the InstructionsF of SCM+FSA -valued V10() non empty Function-like V39() initial halt-free for set ;

proof end;

end;

registration

let I be Program of ;
let J be unique-halt Program of ;

cluster I ";" J -> unique-halt ;

end;

Lm1: for I being preProgram of SCM+FSA holds card (Directed I) = card I

proof end;

Lm2: for I being Program of holds card (stop (Directed I)) = card (stop I)

proof end;

theorem Th5: :: SCMFSA6A:15

for I, J being Program of
for l being Nat st l in dom I & I . l <> halt SCM+FSA holds
(I ";" J) . l = I . l

proof end;

theorem :: SCMFSA6A:16

for I, J being Program of holds Directed I c= I ";" J

proof end;

theorem Th7: :: SCMFSA6A:17

for I, J being Program of holds dom I c= dom (I ";" J)

proof end;

theorem :: SCMFSA6A:18

for I, J being Program of holds I +* (I ";" J) = I ";" J

proof end;

definition

let i be Instruction of SCM+FSA;
let J be Program of ;

func i ";" J -> Program of equals :: SCMFSA6A:def 4
(Macro i) ";" J;

end;

:: deftheorem defines ";" SCMFSA6A:def 4 :

definition

let I be Program of ;
let j be Instruction of SCM+FSA;

func I ";" j -> Program of equals :: SCMFSA6A:def 5
I ";" (Macro j);

end;

:: deftheorem defines ";" SCMFSA6A:def 5 :

definition

let i, j be Instruction of SCM+FSA;

func i ";" j -> Program of equals :: SCMFSA6A:def 6
(Macro i) ";" (Macro j);

end;

:: deftheorem defines ";" SCMFSA6A:def 6 :

registration

cluster with_explicit_jumps IC-relocable sequential for Element of the InstructionsF of SCM+FSA;

proof end;

end;

registration

cluster sequential -> No-StopCode for Element of the InstructionsF of SCM+FSA;

proof end;

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 ;
let j be sequential Instruction of SCM+FSA;

cluster I ";" j -> halt-ending unique-halt ;

end;

registration

let i be sequential Instruction of SCM+FSA;
let J be MacroInstruction of SCM+FSA ;

cluster i ";" J -> halt-ending unique-halt ;

end;

theorem :: SCMFSA6A:19

for i, j being Instruction of SCM+FSA holds i ";" j = (Macro i) ";" j ;

theorem :: SCMFSA6A:20

for i, j being Instruction of SCM+FSA holds i ";" j = i ";" (Macro j) ;

theorem Th11: :: SCMFSA6A:21

for I, J being Program of holds card (I ";" J) = (card I) + (card J)

proof end;

theorem :: SCMFSA6A:22

for I being preProgram of SCM+FSA st I is halt-free holds
Directed I = I by FUNCT_4:103;

theorem Th13: :: SCMFSA6A:23

for I being preProgram of SCM+FSA
for k being Element of NAT holds Reloc ((Directed I),k) = (Reloc (I,k)) +~ ((halt SCM+FSA),(goto ((card I) + k)))

proof end;

theorem Th14: :: SCMFSA6A:24

for I, J being Program of holds Directed (I ";" J) = I ";" (Directed J)

proof end;

theorem Th15: :: SCMFSA6A:25

for I, J, K being Program of holds (I ";" J) ";" K = I ";" (J ";" K)

proof end;

theorem :: SCMFSA6A:26

for k being Instruction of SCM+FSA
for I, J being Program of holds (I ";" J) ";" k = I ";" (J ";" k) by Th15;

theorem :: SCMFSA6A:27

for j being Instruction of SCM+FSA
for I, K being Program of holds (I ";" j) ";" K = I ";" (j ";" K) by Th15;

theorem :: SCMFSA6A:28

for j, k being Instruction of SCM+FSA
for I being Program of holds (I ";" j) ";" k = I ";" (j ";" k) by Th15;

theorem :: SCMFSA6A:29

for i being Instruction of SCM+FSA
for J, K being Program of holds (i ";" J) ";" K = i ";" (J ";" K) by Th15;

theorem :: SCMFSA6A:30

for i, k being Instruction of SCM+FSA
for J being Program of holds (i ";" J) ";" k = i ";" (J ";" k) by Th15;

theorem :: SCMFSA6A:31

for i, j being Instruction of SCM+FSA
for K being Program of holds (i ";" j) ";" K = i ";" (j ";" K) by Th15;

theorem :: SCMFSA6A:32

for i, j, k being Instruction of SCM+FSA holds (i ";" j) ";" k = i ";" (j ";" k) by Th15;

theorem :: SCMFSA6A:33

for i being Instruction of SCM+FSA
for J being Program of holds card (i ";" J) = (card J) + 2

proof end;

theorem :: SCMFSA6A:34

for j being Instruction of SCM+FSA
for I being Program of holds card (I ";" j) = (card I) + 2

proof end;

theorem :: SCMFSA6A:35

for i, j being Instruction of SCM+FSA holds card (i ";" j) = 4

proof end;

theorem :: SCMFSA6A:36

for I being preProgram of SCM+FSA holds card (Directed I) = card I by Lm1;

theorem Th27: :: SCMFSA6A:37

for I being Program of holds card (stop (Directed I)) = card (stop I) by Lm2;

theorem :: SCMFSA6A:38

for I, J being Program of holds Reloc (J,(card I)) c= I ";" J

proof end;

theorem :: SCMFSA6A:39

for I, J being Program of holds dom (I ";" J) = (dom I) \/ (dom (Reloc (J,(card I))))

proof end;

theorem :: SCMFSA6A:40

for n being Nat
for I, J being Program of st n in dom (Reloc (J,(card I))) holds
(I ";" J) . n = (Reloc (J,(card I))) . n

proof end;

registration

let I be really-closed Program of ;

cluster stop (Directed I) -> really-closed ;

proof end;

end;

registration

let I, J be really-closed Program of ;

cluster I ";" J -> really-closed ;

end;

theorem :: SCMFSA6A:41

for I, J being MacroInstruction of SCM+FSA
for n being Nat st n < LastLoc I holds
(I ";" J) . n = I . n

proof end;