:: On the compositions of macro instructions
:: by Andrzej Trybulec , Yatsuka Nakamura and Noriko Asamoto
::
:: 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 +~ ((),(goto (card P))); coherence P +~ ((),(goto (card P))) is preProgram of SCM+FSA ; projectivity for b1, b2 being preProgram of SCM+FSA st b1 = b2 +~ ((),(goto (card b2))) holds b1 = b1 +~ ((),(goto (card b1))) by FUNCT_4:127; end; :: deftheorem defines Directed SCMFSA6A:def 1 : for P being preProgram of SCM+FSA holds Directed P = P +~ ((),(goto (card P))); registration let I be Program of ; cluster Directed I -> non empty initial ; coherence ( Directed I is initial & not Directed I is empty ) proof end; end; theorem :: SCMFSA6A:1 for I being Program of holds not halt SCM+FSA in rng () by FUNCT_4:100; theorem :: SCMFSA6A:2 for m being Nat for I being Program of holds Reloc ((),m) = (() +* (() .--> (goto (m + (card I))))) * (Reloc (I,m)) proof end; set q = () .--> 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 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 ()) ';' J;
coherence
(stop ()) ';' J is Program of
;
end;

:: deftheorem SCMFSA6A:def 2 :
canceled;

:: deftheorem defines ";" SCMFSA6A:def 3 :
for I, J being Program of holds I ";" J = (stop ()) ';' J;

registration
let I be Program of ;
let J be halt-ending Program of ;
coherence
I ";" J is halt-ending
;
end;

registration
let P be preProgram of SCM+FSA;
correctness
coherence ;
by FUNCT_4:100;
end;

registration
existence
ex b1 being Program of st b1 is halt-free
proof end;
end;

registration
let I be Program of ;
let J be unique-halt Program of ;
coherence
I ";" J is unique-halt
;
end;

Lm1: for I being preProgram of SCM+FSA holds card () = card I
proof end;

Lm2: for I being Program of holds card (stop ()) = 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
() ";" J;
correctness
coherence
() ";" J is Program of
;
;
end;

:: deftheorem defines ";" SCMFSA6A:def 4 :
for i being Instruction of SCM+FSA
for J being Program of holds i ";" J = () ";" J;

definition
let I be Program of ;
let j be Instruction of SCM+FSA;
func I ";" j -> Program of equals :: SCMFSA6A:def 5
I ";" ();
correctness
coherence
I ";" () is Program of
;
;
end;

:: deftheorem defines ";" SCMFSA6A:def 5 :
for I being Program of
for j being Instruction of SCM+FSA holds I ";" j = I ";" ();

definition
let i, j be Instruction of SCM+FSA;
func i ";" j -> Program of equals :: SCMFSA6A:def 6
() ";" ();
correctness
coherence
() ";" () is Program of
;
;
end;

:: deftheorem defines ";" SCMFSA6A:def 6 :
for i, j being Instruction of SCM+FSA holds i ";" j = () ";" ();

registration
existence
ex b1 being Instruction of SCM+FSA st b1 is sequential
proof end;
end;

registration
cluster sequential -> No-StopCode for Element of the InstructionsF of SCM+FSA;
coherence
for b1 being Instruction of SCM+FSA st b1 is sequential holds
b1 is No-StopCode
proof end;
end;

registration
let i, j be sequential Instruction of SCM+FSA;
coherence
( i ";" j is halt-ending & i ";" j is unique-halt )
;
end;

registration
let I be MacroInstruction of SCM+FSA ;
let j be sequential Instruction of SCM+FSA;
coherence
( I ";" j is halt-ending & I ";" j is unique-halt )
;
end;

registration
let i be sequential Instruction of SCM+FSA;
let J be MacroInstruction of SCM+FSA ;
coherence
( i ";" J is halt-ending & i ";" J is unique-halt )
;
end;

theorem :: SCMFSA6A:19
for i, j being Instruction of SCM+FSA holds i ";" j = () ";" j ;

theorem :: SCMFSA6A:20
for i, j being Instruction of SCM+FSA holds i ";" j = i ";" () ;

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 ((),k) = (Reloc (I,k)) +~ ((),(goto ((card I) + k)))
proof end;

theorem Th14: :: SCMFSA6A:24
for I, J being Program of holds Directed (I ";" J) = I ";" ()
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 () = card I by Lm1;

theorem Th27: :: SCMFSA6A:37
for I being Program of holds card (stop ()) = 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 ;
coherence
proof end;
end;

registration
let I, J be really-closed Program of ;
coherence
I ";" J is 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;