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 Association of Mizar Users

begin

definition

let P be preProgram of SCM+FSA ;
let l be Instruction-Location of SCM+FSA ;
func Directed P,l -> preProgram of SCM+FSA equals :: SCMFSA6A:def 1
P +~ (halt SCM+FSA ),(goto l);
coherence

proof end;

end;

:: deftheorem defines Directed SCMFSA6A:def 1 :

definition

let P be preProgram of SCM+FSA ;
func Directed P -> preProgram of SCM+FSA equals :: SCMFSA6A:def 2
Directed P,(insloc (card P));
coherence ;

end;

:: deftheorem defines Directed SCMFSA6A:def 2 :

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 -> initial ;
coherence

proof end;

end;

definition

let i be Instruction of SCM+FSA ;
func Macro i -> Program of SCM+FSA equals :: SCMFSA6A:def 3
(insloc 0 ),(insloc 1) --> i,(halt SCM+FSA );
coherence

proof end;

end;

:: deftheorem defines Macro SCMFSA6A:def 3 :

registration

let i be Instruction of SCM+FSA ;
cluster Macro i -> non empty ;
coherence ;

end;

theorem Th15: :: SCMFSA6A:15

for P being Program of SCM+FSA
for n being Nat holds
( n < card P iff n in dom P )

proof end;

theorem Th16: :: SCMFSA6A:16

for I, J being Program of SCM+FSA holds dom I misses dom (ProgramPart (Relocated J,(card I)))

proof end;

theorem Th17: :: SCMFSA6A:17

for m being Element of NAT
for I being preProgram of SCM+FSA holds card (ProgramPart (Relocated I,m)) = card I

proof end;

theorem :: SCMFSA6A:18

for I being Program of SCM+FSA holds not halt SCM+FSA in rng (Directed I)

proof end;

theorem :: SCMFSA6A:19

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

proof end;

theorem :: SCMFSA6A:20

canceled;

theorem Th21: :: SCMFSA6A:21

for n being Element of NAT
for I, J being FinPartState of SCM+FSA holds ProgramPart (Relocated (I +* J),n) = (ProgramPart (Relocated I,n)) +* (ProgramPart (Relocated J,n))

proof end;

theorem Th22: :: SCMFSA6A:22

for m, n being Element of NAT
for I being Program of SCM+FSA holds ProgramPart (Relocated [(ProgramPart (Relocated I,m))],n) = ProgramPart (Relocated I,(m + n))

proof end;

definition

let I be FinPartState of SCM+FSA ;
func Initialized I -> FinPartState of SCM+FSA equals :: SCMFSA6A:def 4
(I +* ((intloc 0 ) .--> 1)) +* (Start-At (insloc 0 ));
coherence

proof end;

end;

:: deftheorem defines Initialized SCMFSA6A:def 4 :

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 SCM+FSA ) = Next (IC s) )

proof end;

theorem Th24: :: SCMFSA6A:24

for I being Program of SCM+FSA holds IC SCM+FSA in dom (Initialized I)

proof end;

theorem :: SCMFSA6A:25

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

proof end;

Lm1: now

assume intloc 0 in NAT ; :: thesis:
then reconsider l = intloc 0 as Instruction-Location of SCM+FSA by AMI_1:def 4;
l = intloc 0 ;
hence contradiction by SCMFSA_2:84; :: thesis:

end;

Lm2: now

assume IC SCM+FSA in NAT ; :: thesis:
then reconsider l = IC SCM+FSA as Instruction-Location of SCM+FSA by AMI_1:def 4;
l = IC SCM+FSA ;
hence contradiction by AMI_1:48; :: thesis:

end;

theorem Th26: :: SCMFSA6A:26

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

proof end;

theorem :: SCMFSA6A:27

canceled;

theorem Th28: :: SCMFSA6A:28

for s1, s2 being State of SCM+FSA st IC s1 = IC s2 & ( for a being Int-Location holds s1 . a = s2 . a ) & ( for f being FinSeq-Location holds s1 . f = s2 . f ) holds
s1,s2 equal_outside NAT

proof end;

theorem :: SCMFSA6A:29

canceled;

theorem Th30: :: SCMFSA6A:30

for s1, s2 being State of SCM+FSA st s1,s2 equal_outside NAT holds
for a being Int-Location holds s1 . a = s2 . a

proof end;

theorem Th31: :: SCMFSA6A:31

for s1, s2 being State of SCM+FSA st s1,s2 equal_outside NAT holds
for f being FinSeq-Location holds s1 . f = s2 . f

proof end;

theorem :: SCMFSA6A:32

for i being Instruction of SCM+FSA
for s1, s2 being State of SCM+FSA st s1,s2 equal_outside NAT holds
Exec i,s1, Exec i,s2 equal_outside NAT

proof end;

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₄() -> Instruction-Location of SCM+FSA } :

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

proof end;

theorem :: SCMFSA6A:34

for s being State of SCM+FSA holds dom s = ((Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )}) \/ NAT by AMI_1:79, SCMFSA_2:8;

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 SCM+FSA or x is Instruction-Location of SCM+FSA )

proof end;

theorem :: SCMFSA6A:36

for s1, s2 being State of SCM+FSA holds
( ( for l being Instruction-Location of SCM+FSA holds s1 . l = s2 . l ) iff s1 | NAT = s2 | NAT )

proof end;

theorem :: SCMFSA6A:37

for i being Instruction-Location of SCM+FSA holds
( not i in Int-Locations \/ FinSeq-Locations & not IC SCM+FSA in Int-Locations \/ FinSeq-Locations )

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

for s1, s2 being State of SCM+FSA st s1,s2 equal_outside NAT holds
DataPart s1 = DataPart s2

proof end;

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

for I, J being Program of SCM+FSA holds I,J equal_outside NAT

proof end;

theorem Th43: :: SCMFSA6A:43

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

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 SCM+FSA )

proof end;

theorem Th45: :: SCMFSA6A:45

for I being Program of SCM+FSA holds intloc 0 in dom (Initialized I)

proof end;

theorem Th46: :: SCMFSA6A:46

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

proof end;

theorem Th47: :: SCMFSA6A:47

for I being Program of SCM+FSA holds
( not intloc 0 in dom I & not IC SCM+FSA in dom I )

proof end;

theorem Th48: :: 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 Th49: :: 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;

theorem :: SCMFSA6A:53

for I, J being Program of SCM+FSA
for s being State of SCM+FSA holds s +* (Initialized I),s +* (Initialized J) equal_outside NAT

proof end;

begin

definition

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

proof end;

end;

:: deftheorem defines ';' SCMFSA6A:def 5 :

theorem :: SCMFSA6A:54

for I, J being Program of SCM+FSA
for l being Instruction-Location of SCM+FSA 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 ;

end;

:: deftheorem defines ';' SCMFSA6A:def 6 :

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 ;

end;

:: deftheorem defines ';' SCMFSA6A:def 7 :

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 ;

end;

:: deftheorem defines ';' SCMFSA6A:def 8 :

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;

theorem :: SCMFSA6A:62

for l being Element of NAT
for I being Program of SCM+FSA holds ProgramPart (Relocated I,l) = IncAddr (Shift I,l),l

proof end;

registration

let P be preProgram of SCM+FSA ;
let l be Instruction-Location of SCM+FSA ;
cluster Directed P,l -> halt-free ;
correctness

proof end;

end;

registration

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

end;

theorem Th63: :: SCMFSA6A:63

for I being preProgram of SCM+FSA
for l being Instruction-Location of SCM+FSA st I is halt-free holds
Directed I,l = I

proof end;

theorem Th64: :: SCMFSA6A:64

for I being preProgram of SCM+FSA
for x being set
for k being Element of NAT st x in dom (ProgramPart (Relocated I,k)) holds
(ProgramPart (Relocated I,k)) . x = (Relocated I,k) . x

proof end;

theorem Th65: :: SCMFSA6A:65

for I being preProgram of SCM+FSA
for k being Element of NAT holds ProgramPart (Relocated (Directed I),k) = Directed [(ProgramPart (Relocated I,k))],(insloc ((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;