:: On the compositions of macro instructions
:: by Andrzej Trybulec , Yatsuka Nakamura and Noriko Asamoto
::
:: Received June 20, 1996
:: Copyright (c) 1996-2011 Association of Mizar Users

begin

set SA0 = Start-At (0,SCM+FSA);

definition

let P be NAT -defined the Instructions of SCM+FSA -valued finite Function;
let l be Element of NAT ;
func Directed (P,l) -> preProgram of SCM+FSA equals :: SCMFSA6A:def 1
P +~ ((halt SCM+FSA),(goto l));
coherence
P +~ ((halt SCM+FSA),(goto l)) is preProgram of SCM+FSA ;

end;

:: deftheorem defines Directed SCMFSA6A:def 1 :
for P being NAT -defined the Instructions of SCM+FSA -valued finite Function
for l being Element of NAT holds Directed (P,l) = P +~ ((halt SCM+FSA),(goto l));

definition

let P be NAT -defined the Instructions of SCM+FSA -valued finite Function;
func Directed P -> preProgram of SCM+FSA equals :: SCMFSA6A:def 2
Directed (P,(card P));
coherence
Directed (P,(card P)) is preProgram of SCM+FSA ;

end;

:: deftheorem defines Directed SCMFSA6A:def 2 :
for P being NAT -defined the Instructions of SCM+FSA -valued finite Function holds Directed P = Directed (P,(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 (Directed I) by FUNCT_4:100;

theorem :: SCMFSA6A:2

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

proof end;

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

set f = the Object-Kind of SCM+FSA;

registration

let n be Nat;
let i be Integer;
cluster (intloc n) .--> i -> the Object-Kind of SCM+FSA -compatible ;
coherence
(intloc n) .--> i is the Object-Kind of SCM+FSA -compatible

proof end;

end;

definition

let I be PartState of SCM+FSA;
func Initialized I -> PartState of SCM+FSA equals :: SCMFSA6A:def 3
I +* (Initialize ((intloc 0) .--> 1));
coherence
I +* (Initialize ((intloc 0) .--> 1)) is PartState of SCM+FSA ;
projectivity
for b₁, b₂ being PartState of SCM+FSA st b₁ = b₂ +* (Initialize ((intloc 0) .--> 1)) holds
b₁ = b₁ +* (Initialize ((intloc 0) .--> 1))

proof end;

end;

:: deftheorem defines Initialized SCMFSA6A:def 3 :
for I being PartState of SCM+FSA holds Initialized I = I +* (Initialize ((intloc 0) .--> 1));

registration

let I be PartState of SCM+FSA;
cluster Initialized I -> 0 -started ;
coherence
Initialized I is 0 -started ;

end;

registration

let I be FinPartState of SCM+FSA;
cluster Initialized I -> finite ;
coherence
Initialized I is finite ;

end;

theorem Th23: :: 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 ) = succ (IC s) )

proof end;

scheme :: SCMFSA6A:sch 1
SCMFSAEx{ F₁( set ) -> Integer, F₂( set ) -> FinSequence of INT , F₃() -> Element of NAT } :

ex S being State of SCM+FSA st
( IC S = F₃() & ( for i being Element of NAT holds
( S . (intloc i) = F₁(i) & S . (fsloc i) = F₂(i) ) ) )

proof end;

theorem :: SCMFSA6A:4

canceled;

theorem :: SCMFSA6A:5

for s being State of SCM+FSA
for x being set holds
( not x in dom s or x is Int-Location or x is FinSeq-Location or x = IC )

proof end;

theorem :: SCMFSA6A:6

canceled;

theorem Th38: :: SCMFSA6A:7

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 DataPart s1 = DataPart s2 )

proof end;

theorem :: SCMFSA6A:8

for s1, s2 being State of SCM+FSA
for n being Element of 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 Th43: :: SCMFSA6A:9

for p being PartState of SCM+FSA holds dom (Initialized p) = ((dom p) \/ {(intloc 0)}) \/ {(IC )}

proof end;

registration

let s be State of SCM+FSA;
cluster Initialized s -> total ;
coherence
Initialized s is total ;

end;

theorem :: SCMFSA6A:10

for p being PartState of SCM+FSA holds intloc 0 in dom (Initialized p)

proof end;

theorem :: SCMFSA6A:11

for p being PartState of SCM+FSA holds
( (Initialized p) . (intloc 0) = 1 & (Initialized p) . (IC ) = 0 )

proof end;

theorem :: SCMFSA6A:12

for I being Program of holds not intloc 0 in dom I

proof end;

theorem :: SCMFSA6A:13

for p being PartState of SCM+FSA
for a being Int-Location st a <> intloc 0 & not a in dom p holds
not a in dom (Initialized p)

proof end;

theorem :: SCMFSA6A:14

for p being PartState of SCM+FSA
for f being FinSeq-Location st not f in dom p holds
not f in dom (Initialized p)

proof end;

begin

definition

let I, J be Program of ;
func I ';' J -> Program of equals :: SCMFSA6A:def 4
(Directed I) +* (Reloc (J,(card I)));
coherence
(Directed I) +* (Reloc (J,(card I))) is Program of

proof end;

correctness
;

end;

:: deftheorem defines ';' SCMFSA6A:def 4 :
for I, J being Program of holds I ';' J = (Directed I) +* (Reloc (J,(card I)));

registration

let I be Program of ;
let J be non halt-free Program of ;
cluster I ';' J -> non halt-free ;
coherence
not I ';' J is halt-free ;

end;

theorem :: SCMFSA6A:15

for I, J being Program of
for l being Element of 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 Th56: :: 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;

begin

definition

let i be Instruction of SCM+FSA;
let J be Program of ;
func i ';' J -> Program of equals :: SCMFSA6A:def 5
(Macro i) ';' J;
correctness
coherence
(Macro i) ';' J is Program of ;
;

end;

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

definition

let I be Program of ;
let j be Instruction of SCM+FSA;
func I ';' j -> Program of equals :: SCMFSA6A:def 6
I ';' (Macro j);
correctness
coherence
I ';' (Macro j) is Program of ;
;

end;

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

definition

let i, j be Instruction of SCM+FSA;
func i ';' j -> Program of equals :: SCMFSA6A:def 7
(Macro i) ';' (Macro j);
correctness
coherence
(Macro i) ';' (Macro j) is Program of ;
;

end;

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

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 Th61: :: SCMFSA6A:21

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

proof end;

registration

let P be preProgram of SCM+FSA;
let l be Element of NAT ;
cluster Directed (P,l) -> halt-free ;
correctness
coherence
Directed (P,l) is halt-free ;

proof end;

end;

registration

let P be preProgram of SCM+FSA;
cluster Directed P -> halt-free ;
correctness
coherence
Directed P is halt-free ;
;

end;

theorem Th63: :: SCMFSA6A:22

for I being preProgram of SCM+FSA
for l being Element of NAT st I is halt-free holds
Directed (I,l) = I

proof end;

theorem Th65: :: SCMFSA6A:23

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

proof end;

theorem Th66: :: SCMFSA6A:24

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

proof end;

theorem Th67: :: 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 Th67;

theorem :: SCMFSA6A:27

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

theorem :: SCMFSA6A:28

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

theorem :: SCMFSA6A:29

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

theorem :: SCMFSA6A:30

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

theorem :: SCMFSA6A:31

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

theorem :: SCMFSA6A:32

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

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

canceled;

theorem :: SCMFSA6A:37

for s being State of SCM+FSA st s . (intloc 0) = 1 & IC s = 0 holds
Initialized s = s

proof end;

theorem :: SCMFSA6A:38

for p being PartState of SCM+FSA holds (Initialized p) . (intloc 0) = 1

proof end;

theorem :: SCMFSA6A:39

canceled;

theorem :: SCMFSA6A:40

canceled;

theorem :: SCMFSA6A:41

intloc 0 in dom (Initialize ((intloc 0) .--> 1))

proof end;

theorem :: SCMFSA6A:42

dom (Initialize ((intloc 0) .--> 1)) = {(intloc 0),(IC )}

proof end;

theorem :: SCMFSA6A:43

(Initialize ((intloc 0) .--> 1)) . (intloc 0) = 1

proof end;

theorem :: SCMFSA6A:44

for p being PartState of SCM+FSA holds Initialize ((intloc 0) .--> 1) c= Initialized p by FUNCT_4:25;