:: SCMFSA6A semantic presentation

theorem :: SCMFSA6A:1

for f, g being Function
for x, y being set st g c= f & not x in dom g holds
g c= f +* x,y

proof end;

theorem :: SCMFSA6A:2

for f, g being Function
for A being set st f | A = g | A & f,g equal_outside A holds
f = g

proof end;

theorem :: SCMFSA6A:3

for f being Function
for a, b, A being set st a in A holds
f,f +* a,b equal_outside A

proof end;

theorem Th4: :: SCMFSA6A:4

for f being Function
for a, b, A being set holds
( a in A or (f +* a,b) | A = f | A )

proof end;

theorem :: SCMFSA6A:5

for f, g being Function
for a, b, A being set st f | A = g | A holds
(f +* a,b) | A = (g +* a,b) | A

proof end;

theorem :: SCMFSA6A:6

for f, g, h being Function st f c= h & g c= h holds
f +* g c= h

proof end;

theorem :: SCMFSA6A:7

for a, b being set
for f being Function holds
( a .--> b c= f iff ( a in dom f & f . a = b ) )

proof end;

theorem Th8: :: SCMFSA6A:8

for f being Function
for A being set holds dom (f | ((dom f) \ A)) = (dom f) \ A

proof end;

theorem Th9: :: SCMFSA6A:9

for f, g being Function
for D being set st D c= dom f & D c= dom g holds
( f | D = g | D iff for x being set st x in D holds
f . x = g . x )

proof end;

theorem Th10: :: SCMFSA6A:10

for f being Function
for D being set holds f | D = f | ((dom f) /\ D)

proof end;

theorem :: SCMFSA6A:11

for f, g, h being Function
for A being set st f,g equal_outside A holds
f +* h,g +* h equal_outside A

proof end;

theorem :: SCMFSA6A:12

for f, g, h being Function
for A being set st f,g equal_outside A holds
h +* f,h +* g equal_outside A

proof end;

theorem :: SCMFSA6A:13

for f, g, h being Function holds
( f +* h = g +* h iff f,g equal_outside dom h )

proof end;

definition

mode Macro-Instruction is programmed initial FinPartState of SCM+FSA ;

end;

definition

let I be programmed FinPartState of SCM+FSA ;
func Directed I -> programmed FinPartState of SCM+FSA equals :: SCMFSA6A:def 1
((id the Instructions of SCM+FSA ) +* ((halt SCM+FSA ) .--> (goto (insloc (card I))))) * I;
coherence

proof end;

correctness ;

end;

:: deftheorem defines Directed SCMFSA6A:def 1 :

theorem Th14: :: SCMFSA6A:14

for I being Macro-Instruction holds dom (Directed I) = dom I

proof end;

registration

let I be Macro-Instruction;
cluster Directed I -> programmed initial ;
coherence

proof end;

end;

definition

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

proof end;

correctness ;

end;

:: deftheorem defines Macro SCMFSA6A:def 2 :

registration

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

end;

theorem Th15: :: SCMFSA6A:15

for P being Macro-Instruction
for n being Nat holds
( n < card P iff insloc n in dom P )

proof end;

registration

let I be initial FinPartState of SCM+FSA ;
cluster ProgramPart I -> initial ;
coherence

proof end;

end;

theorem Th16: :: SCMFSA6A:16

for I, J being Macro-Instruction holds dom I misses dom (ProgramPart (Relocated J,(card I)))

proof end;

theorem Th17: :: SCMFSA6A:17

for m being Nat
for I being programmed FinPartState of SCM+FSA holds card (ProgramPart (Relocated I,m)) = card I

proof end;

theorem Th18: :: SCMFSA6A:18

for I being Macro-Instruction holds not halt SCM+FSA in rng (Directed I)

proof end;

theorem Th19: :: SCMFSA6A:19

for m being Nat
for I being Macro-Instruction 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 Th20: :: SCMFSA6A:20

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

proof end;

theorem Th21: :: SCMFSA6A:21

for n being 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 Nat
for I being Macro-Instruction 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 3
(I +* ((intloc 0) .--> 1)) +* (Start-At (insloc 0));
coherence

proof end;

correctness ;

end;

:: deftheorem defines Initialized SCMFSA6A:def 3 :

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 Macro-Instruction holds IC SCM+FSA in dom (Initialized I)

proof end;

theorem :: SCMFSA6A:25

for I being Macro-Instruction holds IC (Initialized I) = insloc 0

proof end;

theorem Th26: :: SCMFSA6A:26

for I being Macro-Instruction holds I c= Initialized I

proof end;

theorem :: SCMFSA6A:27

for N being set
for A being AMI-Struct of N
for s being State of A
for I being programmed FinPartState of A holds s,s +* I equal_outside the Instruction-Locations of A

proof end;

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 the Instruction-Locations of SCM+FSA

proof end;

theorem Th29: :: SCMFSA6A:29

for N being with_non-empty_elements set
for S being non empty non void IC-Ins-separated definite realistic AMI-Struct of N
for s1, s2 being State of S st s1,s2 equal_outside the Instruction-Locations of S holds
IC s1 = IC s2

proof end;

theorem Th30: :: SCMFSA6A:30

for s1, s2 being State of SCM+FSA st s1,s2 equal_outside the Instruction-Locations of SCM+FSA 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 the Instruction-Locations of SCM+FSA 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 the Instruction-Locations of SCM+FSA holds
Exec i,s1, Exec i,s2 equal_outside the Instruction-Locations of SCM+FSA

proof end;

theorem :: SCMFSA6A:33

for I being Macro-Instruction holds (Initialized I) | the Instruction-Locations of SCM+FSA = 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 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 )}) \/ the Instruction-Locations of SCM+FSA by AMI_3:36, 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 | the Instruction-Locations of SCM+FSA = s2 | the Instruction-Locations of SCM+FSA )

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 s1 | (Int-Locations \/ FinSeq-Locations ) = s2 | (Int-Locations \/ FinSeq-Locations ) )

proof end;

theorem :: SCMFSA6A:39

for s1, s2 being State of SCM+FSA st s1,s2 equal_outside the Instruction-Locations of SCM+FSA holds
s1 | (Int-Locations \/ FinSeq-Locations ) = s2 | (Int-Locations \/ FinSeq-Locations )

proof end;

theorem :: SCMFSA6A:40

for s, ss being State of SCM+FSA
for A being set holds (ss +* (s | A)) | A = s | A

proof end;

theorem :: SCMFSA6A:41

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 & s1 | (Int-Locations \/ FinSeq-Locations ) = s2 | (Int-Locations \/ FinSeq-Locations ) holds
( (IC (Exec i,s1)) + n = IC (Exec (IncAddr i,n),s2) & (Exec i,s1) | (Int-Locations \/ FinSeq-Locations ) = (Exec (IncAddr i,n),s2) | (Int-Locations \/ FinSeq-Locations ) )

proof end;

theorem :: SCMFSA6A:42

for I, J being Macro-Instruction holds I,J equal_outside the Instruction-Locations of SCM+FSA

proof end;

theorem Th43: :: SCMFSA6A:43

for I being Macro-Instruction holds dom (Initialized I) = ((dom I) \/ {(intloc 0)}) \/ {(IC SCM+FSA )}

proof end;

theorem Th44: :: SCMFSA6A:44

for I being Macro-Instruction
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 Macro-Instruction holds intloc 0 in dom (Initialized I)

proof end;

theorem Th46: :: SCMFSA6A:46

for I being Macro-Instruction holds
( (Initialized I) . (intloc 0) = 1 & (Initialized I) . (IC SCM+FSA ) = insloc 0 )

proof end;

theorem Th47: :: SCMFSA6A:47

for I being Macro-Instruction holds
( not intloc 0 in dom I & not IC SCM+FSA in dom I )

proof end;

theorem Th48: :: SCMFSA6A:48

for I being Macro-Instruction
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 Macro-Instruction
for f being FinSeq-Location holds not f in dom (Initialized I)

proof end;

theorem Th50: :: SCMFSA6A:50

for I being Macro-Instruction
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 Macro-Instruction
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 Macro-Instruction
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 Macro-Instruction
for s being State of SCM+FSA holds s +* (Initialized I),s +* (Initialized J) equal_outside the Instruction-Locations of SCM+FSA

proof end;

definition

let I, J be Macro-Instruction;
func I ';' J -> Macro-Instruction equals :: SCMFSA6A:def 4
(Directed I) +* (ProgramPart (Relocated J,(card I)));
coherence

proof end;

correctness ;

end;

:: deftheorem defines ';' SCMFSA6A:def 4 :

theorem :: SCMFSA6A:54

for I, J being Macro-Instruction
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 Macro-Instruction holds Directed I c= I ';' J

proof end;

theorem Th56: :: SCMFSA6A:56

for I, J being Macro-Instruction holds dom I c= dom (I ';' J)

proof end;

theorem :: SCMFSA6A:57

for I, J being Macro-Instruction holds I +* (I ';' J) = I ';' J

proof end;

theorem :: SCMFSA6A:58

for I, J being Macro-Instruction holds (Initialized I) +* (I ';' J) = Initialized (I ';' J)

proof end;

definition

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

end;

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

definition

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

end;

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

definition

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

end;

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

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 Macro-Instruction holds card (I ';' J) = (card I) + (card J)

proof end;

theorem Th62: :: SCMFSA6A:62

for I, J, K being Macro-Instruction holds (I ';' J) ';' K = I ';' (J ';' K)

proof end;

theorem Th63: :: SCMFSA6A:63

for k being Instruction of SCM+FSA
for I, J being Macro-Instruction holds (I ';' J) ';' k = I ';' (J ';' k) by Th62;

theorem :: SCMFSA6A:64

for j being Instruction of SCM+FSA
for I, K being Macro-Instruction holds (I ';' j) ';' K = I ';' (j ';' K) by Th62;

theorem :: SCMFSA6A:65

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

proof end;

theorem Th66: :: SCMFSA6A:66

for i being Instruction of SCM+FSA
for J, K being Macro-Instruction holds (i ';' J) ';' K = i ';' (J ';' K) by Th62;

theorem :: SCMFSA6A:67

for i, k being Instruction of SCM+FSA
for J being Macro-Instruction holds (i ';' J) ';' k = i ';' (J ';' k) by Th63;

theorem Th68: :: SCMFSA6A:68

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

proof end;

theorem :: SCMFSA6A:69

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

proof end;