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

theorem :: SCMFSA6A:1

canceled;

theorem :: SCMFSA6A:2

canceled;

theorem :: SCMFSA6A:3

canceled;

theorem :: SCMFSA6A:4

canceled;

theorem :: SCMFSA6A:5

canceled;

theorem :: SCMFSA6A:6

canceled;

theorem :: SCMFSA6A:7

canceled;

theorem :: SCMFSA6A:8

canceled;

theorem :: SCMFSA6A:9

canceled;

theorem :: SCMFSA6A:10

canceled;

theorem :: SCMFSA6A:11

canceled;

theorem :: SCMFSA6A:12

canceled;

theorem :: SCMFSA6A:13

canceled;

theorem :: SCMFSA6A:14

canceled;

registration

let I be Program of SCM+FSA;
cluster Directed I -> non empty initial ;
coherence
( Directed I is initial & not Directed I is empty )

proof end;

end;

theorem :: SCMFSA6A:15

canceled;

theorem :: SCMFSA6A:16

canceled;

theorem :: SCMFSA6A:17

canceled;

theorem :: SCMFSA6A:18

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

theorem :: SCMFSA6A:19

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

canceled;
let I be PartState of SCM+FSA;
func Initialized I -> PartState of SCM+FSA equals :: SCMFSA6A:def 4
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 SCMFSA6A:def 3 :
canceled;

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

registration

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

end;

theorem :: SCMFSA6A:20

canceled;

theorem :: SCMFSA6A:21

canceled;

theorem :: SCMFSA6A:22

canceled;

theorem Th23: :: SCMFSA6A:23

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;

theorem Th24: :: SCMFSA6A:24

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

proof end;

theorem :: SCMFSA6A:25

for I being Program of SCM+FSA holds IC (Initialized I) = 0

proof end;

Lm2: not intloc 0 in NAT
by SCMFSA_2:84;

Lm3: not IC in NAT
by COMPOS_1:3;

theorem Th26: :: SCMFSA6A:26

for I being Program of SCM+FSA holds I c= Initialized I

proof end;

registration

let I be non halt-free Program of SCM+FSA;
cluster Initialized I -> non halt-free ;
coherence
not Initialized I is halt-free

proof end;

end;

theorem :: SCMFSA6A:27

canceled;

theorem :: SCMFSA6A:28

canceled;

theorem :: SCMFSA6A:29

canceled;

theorem :: SCMFSA6A:30

canceled;

theorem :: SCMFSA6A:31

canceled;

theorem :: SCMFSA6A:32

canceled;

theorem :: SCMFSA6A:33

for I being Program of SCM+FSA holds (Initialized I) | NAT = I

proof end;

scheme :: SCMFSA6A:sch 1
SCMFSAEx{ F₁( set ) -> Element of the Instructions of SCM+FSA, 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 . i = F₁(i) & S . (intloc i) = F₂(i) & S . (fsloc i) = F₃(i) ) ) )

proof end;

theorem :: SCMFSA6A:34

canceled;

theorem :: SCMFSA6A:35

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 or x is Element of NAT )

proof end;

theorem :: SCMFSA6A:36

canceled;

theorem :: SCMFSA6A:37

for i being Element of NAT holds
( not i in Data-Locations SCM+FSA & not IC in Data-Locations SCM+FSA )

proof end;

theorem Th38: :: SCMFSA6A:38

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

canceled;

theorem :: SCMFSA6A:40

canceled;

theorem :: SCMFSA6A:41

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

canceled;

theorem Th43: :: SCMFSA6A:43

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

proof end;

theorem Th44: :: SCMFSA6A:44

for I being Program of SCM+FSA
for x being set holds
( not x in dom (Initialized I) or x in dom I or x = intloc 0 or x = IC )

proof end;

theorem Th45: :: SCMFSA6A:45

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

proof end;

theorem Th46: :: SCMFSA6A:46

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

proof end;

theorem Th47: :: SCMFSA6A:47

for I being Program of SCM+FSA holds not intloc 0 in dom I

proof end;

theorem :: SCMFSA6A:48

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

proof end;

theorem :: SCMFSA6A:49

for I being Program of SCM+FSA
for f being FinSeq-Location holds not f in dom (Initialized I)

proof end;

theorem Th50: :: SCMFSA6A:50

for I being Program of SCM+FSA
for x being set st x in dom I holds
I . x = (Initialized I) . x

proof end;

theorem Th51: :: SCMFSA6A:51

for I, J being Program of SCM+FSA
for s being State of SCM+FSA st Initialized J c= s holds
s +* (Initialized I) = s +* I

proof end;

theorem :: SCMFSA6A:52

for I, J being Program of SCM+FSA
for s being State of SCM+FSA st Initialized J c= s holds
Initialized I c= s +* I

proof end;

LmB: for i, j being Nat holds NPP ((intloc i) .--> j) = (intloc i) .--> j

proof end;

theorem :: SCMFSA6A:53

canceled;

begin

definition

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

proof end;

correctness
;

end;

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

registration

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

end;

theorem :: SCMFSA6A:54

for I, J being Program of SCM+FSA
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:55

for I, J being Program of SCM+FSA holds Directed I c= I ';' J

proof end;

theorem Th56: :: SCMFSA6A:56

for I, J being Program of SCM+FSA holds dom I c= dom (I ';' J)

proof end;

theorem :: SCMFSA6A:57

for I, J being Program of SCM+FSA holds I +* (I ';' J) = I ';' J

proof end;

theorem :: SCMFSA6A:58

for I, J being Program of SCM+FSA holds (Initialized I) +* (I ';' J) = Initialized (I ';' J)

proof end;

begin

definition

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

end;

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

definition

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

end;

:: deftheorem defines ';' SCMFSA6A:def 7 :
for I being Program of SCM+FSA
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 SCM+FSA equals :: SCMFSA6A:def 8
(Macro i) ';' (Macro j);
correctness
coherence
(Macro i) ';' (Macro j) is Program of SCM+FSA;
;

end;

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

theorem :: SCMFSA6A:59

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

theorem :: SCMFSA6A:60

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

theorem Th61: :: SCMFSA6A:61

for I, J being Program of SCM+FSA 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 :: SCMFSA6A:62

canceled;

theorem Th63: :: SCMFSA6A:63

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

canceled;

theorem Th65: :: SCMFSA6A:65

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

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

proof end;

theorem Th67: :: SCMFSA6A:67

for I, J, K being Program of SCM+FSA holds (I ';' J) ';' K = I ';' (J ';' K)

proof end;

theorem :: SCMFSA6A:68

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

theorem :: SCMFSA6A:69

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

theorem :: SCMFSA6A:70

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

theorem :: SCMFSA6A:71

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

theorem :: SCMFSA6A:72

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

theorem :: SCMFSA6A:73

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

theorem :: SCMFSA6A:74

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

theorem :: SCMFSA6A:75

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

proof end;

theorem :: SCMFSA6A:76

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

proof end;

theorem :: SCMFSA6A:77

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

proof end;

theorem :: SCMFSA6A:78

for i, j being Nat holds NPP ((intloc i) .--> j) = (intloc i) .--> j by LmB;

theorem Th79: :: SCMFSA6A:79

for I being Program of SCM+FSA holds NPP (Initialized I) = Initialize ((intloc 0) .--> 1)

proof end;

theorem :: SCMFSA6A:80

for I being Program of SCM+FSA holds Initialize I c= Initialized I

proof end;

theorem :: SCMFSA6A:81

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

proof end;

theorem :: SCMFSA6A:82

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

proof end;

theorem :: SCMFSA6A:83

for p being PartState of SCM+FSA holds Initialize (Initialized p) = Initialized p

proof end;

theorem :: SCMFSA6A:84

for s being State of SCM+FSA
for I being Program of SCM+FSA holds s +* (NPP (Initialized I)) = (Initialized s) +* (Start-At (0,SCM+FSA))

proof end;

theorem :: SCMFSA6A:85

for p, q being PartState of SCM+FSA holds IC in dom (p +* (Initialized q))

proof end;

theorem :: SCMFSA6A:86

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

proof end;

theorem :: SCMFSA6A:87

dom (Initialize ((intloc 0) .--> 1)) misses NAT

proof end;