SCMFSA_2: The { \bf SCM

:: The { \bf SCM_FSA } computer
:: by Andrzej Trybulec , Yatsuka Nakamura and Piotr Rudnicki
::
:: Received February 7, 1996
:: Copyright (c) 1996 Association of Mizar Users

definition

func SCM+FSA -> strict AMI-Struct of NAT ,{INT ,(INT * )} equals :: SCMFSA_2:def 1
AMI-Struct(# SCM+FSA-Memory ,(In NAT ,SCM+FSA-Memory ),SCM+FSA-Instr ,SCM+FSA-OK ,SCM+FSA-Exec #);
coherence ;

end;

:: deftheorem defines SCM+FSA SCMFSA_2:def 1 :

registration

cluster SCM+FSA -> non empty strict stored-program standard-ins ;
coherence by AMI_1:def 3, AMI_1:def 32;

end;

theorem :: SCMFSA_2:1

canceled;

theorem :: SCMFSA_2:2

canceled;

theorem :: SCMFSA_2:3

canceled;

theorem :: SCMFSA_2:4

canceled;

theorem :: SCMFSA_2:5

canceled;

theorem :: SCMFSA_2:6

canceled;

theorem Th7: :: SCMFSA_2:7

IC SCM+FSA = NAT by FUNCT_7:def 1, SCMFSA_1:5;

definition

func Int-Locations -> Subset of SCM+FSA equals :: SCMFSA_2:def 2
SCM+FSA-Data-Loc ;
coherence ;
func FinSeq-Locations -> Subset of SCM+FSA equals :: SCMFSA_2:def 3
SCM+FSA-Data*-Loc ;
coherence ;

end;

:: deftheorem defines Int-Locations SCMFSA_2:def 2 :

:: deftheorem defines FinSeq-Locations SCMFSA_2:def 3 :

theorem :: SCMFSA_2:8

the carrier of SCM+FSA = ((Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )}) \/ NAT by Th7, SCMFSA_1:8, XBOOLE_1:4;

definition

mode Int-Location -> Object of SCM+FSA means :Def4: :: SCMFSA_2:def 4
it in SCM+FSA-Data-Loc ;
existence

proof end;

mode FinSeq-Location -> Object of SCM+FSA means :Def5: :: SCMFSA_2:def 5
it in SCM+FSA-Data*-Loc ;
existence

proof end;

end;

:: deftheorem Def4 defines Int-Location SCMFSA_2:def 4 :

:: deftheorem Def5 defines FinSeq-Location SCMFSA_2:def 5 :

theorem :: SCMFSA_2:9

for da being Int-Location holds da in Int-Locations by Def4;

theorem :: SCMFSA_2:10

for fa being FinSeq-Location holds fa in FinSeq-Locations by Def5;

theorem :: SCMFSA_2:11

for x being set st x in Int-Locations holds
x is Int-Location by Def4;

theorem :: SCMFSA_2:12

for x being set st x in FinSeq-Locations holds
x is FinSeq-Location by Def5;

theorem :: SCMFSA_2:13

Int-Locations misses NAT by AMI_2:29;

theorem Th14: :: SCMFSA_2:14

FinSeq-Locations misses NAT by SCMFSA_1:33, XBOOLE_1:63;

theorem :: SCMFSA_2:15

Int-Locations misses FinSeq-Locations by SCMFSA_1:33, XBOOLE_1:63;

definition

let k be natural number ;
func intloc k -> Int-Location equals :: SCMFSA_2:def 6
dl. k;
coherence

proof end;

func insloc k -> Instruction-Location of SCM+FSA equals :: SCMFSA_2:def 7
k;
coherence

proof end;

func fsloc k -> FinSeq-Location equals :: SCMFSA_2:def 8
- (k + 1);
coherence

proof end;

end;

:: deftheorem defines intloc SCMFSA_2:def 6 :

:: deftheorem defines insloc SCMFSA_2:def 7 :

:: deftheorem defines fsloc SCMFSA_2:def 8 :

theorem :: SCMFSA_2:16

canceled;

theorem :: SCMFSA_2:17

for k1, k2 being natural number st k1 <> k2 holds
fsloc k1 <> fsloc k2 ;

theorem :: SCMFSA_2:18

canceled;

theorem :: SCMFSA_2:19

for dl being Int-Location ex i being Element of NAT st dl = intloc i

proof end;

theorem Th20: :: SCMFSA_2:20

for fl being FinSeq-Location ex i being Element of NAT st fl = fsloc i

proof end;

theorem :: SCMFSA_2:21

canceled;

theorem :: SCMFSA_2:22

canceled;

theorem :: SCMFSA_2:23

not FinSeq-Locations is finite

proof end;

theorem :: SCMFSA_2:24

not NAT is finite ;

theorem Th25: :: SCMFSA_2:25

for I being Int-Location holds I is Data-Location

proof end;

theorem Th26: :: SCMFSA_2:26

for l being Int-Location holds ObjectKind l = INT

proof end;

theorem Th27: :: SCMFSA_2:27

for l being FinSeq-Location holds ObjectKind l = INT *

proof end;

theorem :: SCMFSA_2:28

for x being set st x in SCM+FSA-Data-Loc holds
x is Int-Location by Def4;

theorem :: SCMFSA_2:29

for x being set st x in SCM+FSA-Data*-Loc holds
x is FinSeq-Location by Def5;

registration

let I be Instruction of SCM+FSA ;
cluster I `1 -> natural ;
coherence ;

end;

theorem :: SCMFSA_2:30

canceled;

theorem :: SCMFSA_2:31

canceled;

theorem :: SCMFSA_2:32

canceled;

theorem :: SCMFSA_2:33

canceled;

theorem Th34: :: SCMFSA_2:34

for I being Instruction of SCM+FSA st InsCode I <= 8 holds
I is Instruction of SCM

proof end;

theorem Th35: :: SCMFSA_2:35

for I being Instruction of SCM+FSA holds InsCode I <= 12

proof end;

theorem :: SCMFSA_2:36

canceled;

theorem :: SCMFSA_2:37

for i being Instruction of SCM+FSA
for I being Instruction of SCM st i = I holds
InsCode i = InsCode I ;

theorem Th38: :: SCMFSA_2:38

for I being Instruction of SCM holds I is Instruction of SCM+FSA

proof end;

definition

let a, b be Int-Location ;
canceled;
canceled;
func a := b -> Instruction of SCM+FSA means :Def11: :: SCMFSA_2:def 11
ex A, B being Data-Location st
( a = A & b = B & it = A := B );
existence

proof end;

correctness ;
func AddTo a,b -> Instruction of SCM+FSA means :Def12: :: SCMFSA_2:def 12
ex A, B being Data-Location st
( a = A & b = B & it = AddTo A,B );
existence

proof end;

correctness ;
func SubFrom a,b -> Instruction of SCM+FSA means :Def13: :: SCMFSA_2:def 13
ex A, B being Data-Location st
( a = A & b = B & it = SubFrom A,B );
existence

proof end;

correctness ;
func MultBy a,b -> Instruction of SCM+FSA means :Def14: :: SCMFSA_2:def 14
ex A, B being Data-Location st
( a = A & b = B & it = MultBy A,B );
existence

proof end;

correctness ;
func Divide a,b -> Instruction of SCM+FSA means :Def15: :: SCMFSA_2:def 15
ex A, B being Data-Location st
( a = A & b = B & it = Divide A,B );
existence

proof end;

correctness ;

end;

:: deftheorem SCMFSA_2:def 9 :

:: deftheorem SCMFSA_2:def 10 :

:: deftheorem Def11 defines := SCMFSA_2:def 11 :

:: deftheorem Def12 defines AddTo SCMFSA_2:def 12 :

:: deftheorem Def13 defines SubFrom SCMFSA_2:def 13 :

:: deftheorem Def14 defines MultBy SCMFSA_2:def 14 :

:: deftheorem Def15 defines Divide SCMFSA_2:def 15 :

theorem :: SCMFSA_2:39

NAT = NAT ;

definition

let la be Instruction-Location of SCM+FSA ;
func goto la -> Instruction of SCM+FSA means :Def16: :: SCMFSA_2:def 16
ex La being Instruction-Location of SCM st
( la = La & it = goto La );
existence

proof end;

correctness ;
let a be Int-Location ;
func a =0_goto la -> Instruction of SCM+FSA means :Def17: :: SCMFSA_2:def 17
ex A being Data-Location ex La being Instruction-Location of SCM st
( a = A & la = La & it = A =0_goto La );
existence

proof end;

correctness ;
func a >0_goto la -> Instruction of SCM+FSA means :Def18: :: SCMFSA_2:def 18
ex A being Data-Location ex La being Instruction-Location of SCM st
( a = A & la = La & it = A >0_goto La );
existence

proof end;

correctness ;

end;

:: deftheorem Def16 defines goto SCMFSA_2:def 16 :

:: deftheorem Def17 defines =0_goto SCMFSA_2:def 17 :

:: deftheorem Def18 defines >0_goto SCMFSA_2:def 18 :

definition

let c, i be Int-Location ;
let a be FinSeq-Location ;
func c := a,i -> Instruction of SCM+FSA equals :: SCMFSA_2:def 19
[9,<*c,a,i*>];
coherence

proof end;

func a,i := c -> Instruction of SCM+FSA equals :: SCMFSA_2:def 20
[10,<*c,a,i*>];
coherence

proof end;

end;

:: deftheorem defines := SCMFSA_2:def 19 :

:: deftheorem defines := SCMFSA_2:def 20 :

definition

let i be Int-Location ;
let a be FinSeq-Location ;
func i :=len a -> Instruction of SCM+FSA equals :: SCMFSA_2:def 21
[11,<*i,a*>];
coherence

proof end;

func a :=<0,...,0> i -> Instruction of SCM+FSA equals :: SCMFSA_2:def 22
[12,<*i,a*>];
coherence

proof end;

end;

:: deftheorem defines :=len SCMFSA_2:def 21 :

:: deftheorem defines :=<0,...,0> SCMFSA_2:def 22 :

theorem :: SCMFSA_2:40

canceled;

theorem :: SCMFSA_2:41

canceled;

theorem :: SCMFSA_2:42

for a, b being Int-Location holds InsCode (a := b) = 1

proof end;

theorem :: SCMFSA_2:43

for a, b being Int-Location holds InsCode (AddTo a,b) = 2

proof end;

theorem :: SCMFSA_2:44

for a, b being Int-Location holds InsCode (SubFrom a,b) = 3

proof end;

theorem :: SCMFSA_2:45

for a, b being Int-Location holds InsCode (MultBy a,b) = 4

proof end;

theorem :: SCMFSA_2:46

for a, b being Int-Location holds InsCode (Divide a,b) = 5

proof end;

theorem :: SCMFSA_2:47

for lb being Instruction-Location of SCM+FSA holds InsCode (goto lb) = 6

proof end;

theorem :: SCMFSA_2:48

for lb being Instruction-Location of SCM+FSA
for a being Int-Location holds InsCode (a =0_goto lb) = 7

proof end;

theorem :: SCMFSA_2:49

for lb being Instruction-Location of SCM+FSA
for a being Int-Location holds InsCode (a >0_goto lb) = 8

proof end;

theorem :: SCMFSA_2:50

for fa being FinSeq-Location
for c, a being Int-Location holds InsCode (c := fa,a) = 9 by MCART_1:7;

theorem :: SCMFSA_2:51

for fa being FinSeq-Location
for a, c being Int-Location holds InsCode (fa,a := c) = 10 by MCART_1:7;

theorem :: SCMFSA_2:52

for fa being FinSeq-Location
for a being Int-Location holds InsCode (a :=len fa) = 11 by MCART_1:7;

theorem :: SCMFSA_2:53

for fa being FinSeq-Location
for a being Int-Location holds InsCode (fa :=<0,...,0> a) = 12 by MCART_1:7;

theorem Th54: :: SCMFSA_2:54

for ins being Instruction of SCM+FSA st InsCode ins = 1 holds
ex da, db being Int-Location st ins = da := db

proof end;

theorem Th55: :: SCMFSA_2:55

for ins being Instruction of SCM+FSA st InsCode ins = 2 holds
ex da, db being Int-Location st ins = AddTo da,db

proof end;

theorem Th56: :: SCMFSA_2:56

for ins being Instruction of SCM+FSA st InsCode ins = 3 holds
ex da, db being Int-Location st ins = SubFrom da,db

proof end;

theorem Th57: :: SCMFSA_2:57

for ins being Instruction of SCM+FSA st InsCode ins = 4 holds
ex da, db being Int-Location st ins = MultBy da,db

proof end;

theorem Th58: :: SCMFSA_2:58

for ins being Instruction of SCM+FSA st InsCode ins = 5 holds
ex da, db being Int-Location st ins = Divide da,db

proof end;

theorem Th59: :: SCMFSA_2:59

for ins being Instruction of SCM+FSA st InsCode ins = 6 holds
ex lb being Instruction-Location of SCM+FSA st ins = goto lb

proof end;

theorem Th60: :: SCMFSA_2:60

for ins being Instruction of SCM+FSA st InsCode ins = 7 holds
ex lb being Instruction-Location of SCM+FSA ex da being Int-Location st ins = da =0_goto lb

proof end;

theorem Th61: :: SCMFSA_2:61

for ins being Instruction of SCM+FSA st InsCode ins = 8 holds
ex lb being Instruction-Location of SCM+FSA ex da being Int-Location st ins = da >0_goto lb

proof end;

theorem Th62: :: SCMFSA_2:62

for ins being Instruction of SCM+FSA st InsCode ins = 9 holds
ex a, b being Int-Location ex fa being FinSeq-Location st ins = b := fa,a

proof end;

theorem Th63: :: SCMFSA_2:63

for ins being Instruction of SCM+FSA st InsCode ins = 10 holds
ex a, b being Int-Location ex fa being FinSeq-Location st ins = fa,a := b

proof end;

theorem Th64: :: SCMFSA_2:64

for ins being Instruction of SCM+FSA st InsCode ins = 11 holds
ex a being Int-Location ex fa being FinSeq-Location st ins = a :=len fa

proof end;

theorem Th65: :: SCMFSA_2:65

for ins being Instruction of SCM+FSA st InsCode ins = 12 holds
ex a being Int-Location ex fa being FinSeq-Location st ins = fa :=<0,...,0> a

proof end;

theorem :: SCMFSA_2:66

for s being State of SCM+FSA
for d being Int-Location holds d in dom s

proof end;

theorem :: SCMFSA_2:67

for f being FinSeq-Location
for s being State of SCM+FSA holds f in dom s

proof end;

theorem Th68: :: SCMFSA_2:68

for f being FinSeq-Location
for S being State of SCM holds not f in dom S

proof end;

theorem Th69: :: SCMFSA_2:69

for s being State of SCM+FSA holds Int-Locations c= dom s

proof end;

theorem Th70: :: SCMFSA_2:70

for s being State of SCM+FSA holds FinSeq-Locations c= dom s

proof end;

theorem :: SCMFSA_2:71

for s being State of SCM+FSA holds dom (s | Int-Locations ) = Int-Locations

proof end;

theorem :: SCMFSA_2:72

for s being State of SCM+FSA holds dom (s | FinSeq-Locations ) = FinSeq-Locations

proof end;

theorem :: SCMFSA_2:73

for s being State of SCM+FSA
for i being Instruction of SCM holds (s | SCM-Memory ) +* (NAT --> i) is State of SCM by SCMFSA_1:18;

theorem :: SCMFSA_2:74

for s being State of SCM+FSA
for s' being State of SCM holds (s +* s') +* (s | NAT ) is State of SCM+FSA by SCMFSA_1:19;

theorem Th75: :: SCMFSA_2:75

for i being Instruction of SCM
for ii being Instruction of SCM+FSA
for s being State of SCM
for ss being State of SCM+FSA st i = ii & s = (ss | SCM-Memory ) +* (NAT --> i) holds
Exec ii,ss = (ss +* (Exec i,s)) +* (ss | NAT )

proof end;

definition

let s be State of SCM+FSA ;
let d be Int-Location ;
:: original: .
redefine func s . d -> Integer;
coherence

proof end;

end;

definition

let s be State of SCM+FSA ;
let d be FinSeq-Location ;
:: original: .
redefine func s . d -> FinSequence of INT ;
coherence

proof end;

end;

theorem Th76: :: SCMFSA_2:76

for I being Instruction of SCM
for S being State of SCM
for s being State of SCM+FSA st S = (s | SCM-Memory ) +* (NAT --> I) holds
s = (s +* S) +* (s | NAT )

proof end;

theorem :: SCMFSA_2:77

canceled;

theorem Th78: :: SCMFSA_2:78

for S being State of SCM
for s1, s being State of SCM+FSA st s1 = (s +* S) +* (s | NAT ) holds
s1 . (IC SCM+FSA ) = S . (IC SCM )

proof end;

theorem Th79: :: SCMFSA_2:79

for A being Data-Location
for a being Int-Location
for S being State of SCM
for s1, s being State of SCM+FSA st s1 = (s +* S) +* (s | NAT ) & A = a holds
S . A = s1 . a

proof end;

theorem Th80: :: SCMFSA_2:80

for I being Instruction of SCM
for A being Data-Location
for a being Int-Location
for S being State of SCM
for s being State of SCM+FSA st S = (s | SCM-Memory ) +* (NAT --> I) & A = a holds
S . A = s . a

proof end;

registration

cluster SCM+FSA -> strict IC-Ins-separated steady-programmed definite realistic ;
coherence

proof end;

end;

theorem :: SCMFSA_2:81

for dl being Int-Location holds dl <> IC SCM+FSA

proof end;

theorem :: SCMFSA_2:82

for dl being FinSeq-Location holds dl <> IC SCM+FSA

proof end;

theorem :: SCMFSA_2:83

for il being Int-Location
for dl being FinSeq-Location holds il <> dl

proof end;

theorem :: SCMFSA_2:84

for il being Instruction-Location of SCM+FSA
for dl being Int-Location holds il <> dl

proof end;

theorem :: SCMFSA_2:85

for il being Instruction-Location of SCM+FSA
for dl being FinSeq-Location holds il <> dl

proof end;

theorem :: SCMFSA_2:86

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 ) & ( for i being Instruction-Location of SCM+FSA holds s1 . i = s2 . i ) holds
s1 = s2

proof end;

theorem :: SCMFSA_2:87

canceled;

theorem Th88: :: SCMFSA_2:88

for I being Instruction of SCM
for S being State of SCM
for s being State of SCM+FSA st S = (s | SCM-Memory ) +* (NAT --> I) holds
IC s = IC S

proof end;

theorem Th89: :: SCMFSA_2:89

for a, b being Int-Location
for s being State of SCM+FSA holds
( (Exec (a := b),s) . (IC SCM+FSA ) = Next & (Exec (a := b),s) . a = s . b & ( for c being Int-Location st c <> a holds
(Exec (a := b),s) . c = s . c ) & ( for f being FinSeq-Location holds (Exec (a := b),s) . f = s . f ) )

proof end;

theorem Th90: :: SCMFSA_2:90

for a, b being Int-Location
for s being State of SCM+FSA holds
( (Exec (AddTo a,b),s) . (IC SCM+FSA ) = Next & (Exec (AddTo a,b),s) . a = (s . a) + (s . b) & ( for c being Int-Location st c <> a holds
(Exec (AddTo a,b),s) . c = s . c ) & ( for f being FinSeq-Location holds (Exec (AddTo a,b),s) . f = s . f ) )

proof end;

theorem Th91: :: SCMFSA_2:91

for a, b being Int-Location
for s being State of SCM+FSA holds
( (Exec (SubFrom a,b),s) . (IC SCM+FSA ) = Next & (Exec (SubFrom a,b),s) . a = (s . a) - (s . b) & ( for c being Int-Location st c <> a holds
(Exec (SubFrom a,b),s) . c = s . c ) & ( for f being FinSeq-Location holds (Exec (SubFrom a,b),s) . f = s . f ) )

proof end;

theorem Th92: :: SCMFSA_2:92

for a, b being Int-Location
for s being State of SCM+FSA holds
( (Exec (MultBy a,b),s) . (IC SCM+FSA ) = Next & (Exec (MultBy a,b),s) . a = (s . a) * (s . b) & ( for c being Int-Location st c <> a holds
(Exec (MultBy a,b),s) . c = s . c ) & ( for f being FinSeq-Location holds (Exec (MultBy a,b),s) . f = s . f ) )

proof end;

theorem Th93: :: SCMFSA_2:93

for a, b being Int-Location
for s being State of SCM+FSA holds
( (Exec (Divide a,b),s) . (IC SCM+FSA ) = Next & ( a <> b implies (Exec (Divide a,b),s) . a = (s . a) div (s . b) ) & (Exec (Divide a,b),s) . b = (s . a) mod (s . b) & ( for c being Int-Location st c <> a & c <> b holds
(Exec (Divide a,b),s) . c = s . c ) & ( for f being FinSeq-Location holds (Exec (Divide a,b),s) . f = s . f ) )

proof end;

theorem :: SCMFSA_2:94

for a being Int-Location
for s being State of SCM+FSA holds
( (Exec (Divide a,a),s) . (IC SCM+FSA ) = Next & (Exec (Divide a,a),s) . a = (s . a) mod (s . a) & ( for c being Int-Location st c <> a holds
(Exec (Divide a,a),s) . c = s . c ) & ( for f being FinSeq-Location holds (Exec (Divide a,a),s) . f = s . f ) )

proof end;

theorem Th95: :: SCMFSA_2:95

for l being Instruction-Location of SCM+FSA
for s being State of SCM+FSA holds
( (Exec (goto l),s) . (IC SCM+FSA ) = l & ( for c being Int-Location holds (Exec (goto l),s) . c = s . c ) & ( for f being FinSeq-Location holds (Exec (goto l),s) . f = s . f ) )

proof end;

theorem Th96: :: SCMFSA_2:96

for l being Instruction-Location of SCM+FSA
for a being Int-Location
for s being State of SCM+FSA holds
( ( s . a = 0 implies (Exec (a =0_goto l),s) . (IC SCM+FSA ) = l ) & ( s . a <> 0 implies (Exec (a =0_goto l),s) . (IC SCM+FSA ) = Next ) & ( for c being Int-Location holds (Exec (a =0_goto l),s) . c = s . c ) & ( for f being FinSeq-Location holds (Exec (a =0_goto l),s) . f = s . f ) )

proof end;

theorem Th97: :: SCMFSA_2:97

for l being Instruction-Location of SCM+FSA
for a being Int-Location
for s being State of SCM+FSA holds
( ( s . a > 0 implies (Exec (a >0_goto l),s) . (IC SCM+FSA ) = l ) & ( s . a <= 0 implies (Exec (a >0_goto l),s) . (IC SCM+FSA ) = Next ) & ( for c being Int-Location holds (Exec (a >0_goto l),s) . c = s . c ) & ( for f being FinSeq-Location holds (Exec (a >0_goto l),s) . f = s . f ) )

proof end;

theorem Th98: :: SCMFSA_2:98

for g being FinSeq-Location
for c, a being Int-Location
for s being State of SCM+FSA holds
( (Exec (c := g,a),s) . (IC SCM+FSA ) = Next & ex k being Element of NAT st
( k = abs (s . a) & (Exec (c := g,a),s) . c = (s . g) /. k ) & ( for b being Int-Location st b <> c holds
(Exec (c := g,a),s) . b = s . b ) & ( for f being FinSeq-Location holds (Exec (c := g,a),s) . f = s . f ) )

proof end;

theorem Th99: :: SCMFSA_2:99

for g being FinSeq-Location
for a, c being Int-Location
for s being State of SCM+FSA holds
( (Exec (g,a := c),s) . (IC SCM+FSA ) = Next & ex k being Element of NAT st
( k = abs (s . a) & (Exec (g,a := c),s) . g = (s . g) +* k,(s . c) ) & ( for b being Int-Location holds (Exec (g,a := c),s) . b = s . b ) & ( for f being FinSeq-Location st f <> g holds
(Exec (g,a := c),s) . f = s . f ) )

proof end;

theorem Th100: :: SCMFSA_2:100

for g being FinSeq-Location
for c being Int-Location
for s being State of SCM+FSA holds
( (Exec (c :=len g),s) . (IC SCM+FSA ) = Next & (Exec (c :=len g),s) . c = len (s . g) & ( for b being Int-Location st b <> c holds
(Exec (c :=len g),s) . b = s . b ) & ( for f being FinSeq-Location holds (Exec (c :=len g),s) . f = s . f ) )

proof end;

theorem Th101: :: SCMFSA_2:101

for g being FinSeq-Location
for c being Int-Location
for s being State of SCM+FSA holds
( (Exec (g :=<0,...,0> c),s) . (IC SCM+FSA ) = Next & ex k being Element of NAT st
( k = abs (s . c) & (Exec (g :=<0,...,0> c),s) . g = k |-> 0 ) & ( for b being Int-Location holds (Exec (g :=<0,...,0> c),s) . b = s . b ) & ( for f being FinSeq-Location st f <> g holds
(Exec (g :=<0,...,0> c),s) . f = s . f ) )

proof end;

theorem :: SCMFSA_2:102

for s being State of SCM+FSA
for S being SCM+FSA-State st S = s holds
IC s = IC S by FUNCT_7:def 1, SCMFSA_1:5;

theorem Th103: :: SCMFSA_2:103

for i being Instruction of SCM
for I being Instruction of SCM+FSA st i = I & i is halting holds
I is halting

proof end;

theorem Th104: :: SCMFSA_2:104

for I being Instruction of SCM+FSA st ex s being State of SCM+FSA st (Exec I,s) . (IC SCM+FSA ) = Next holds
not I is halting

proof end;

theorem Th105: :: SCMFSA_2:105

for a, b being Int-Location holds not a := b is halting

proof end;

theorem Th106: :: SCMFSA_2:106

for a, b being Int-Location holds not AddTo a,b is halting

proof end;

theorem Th107: :: SCMFSA_2:107

for a, b being Int-Location holds not SubFrom a,b is halting

proof end;

theorem Th108: :: SCMFSA_2:108

for a, b being Int-Location holds not MultBy a,b is halting

proof end;

theorem Th109: :: SCMFSA_2:109

for a, b being Int-Location holds not Divide a,b is halting

proof end;

theorem Th110: :: SCMFSA_2:110

for la being Instruction-Location of SCM+FSA holds not goto la is halting

proof end;

theorem Th111: :: SCMFSA_2:111

for la being Instruction-Location of SCM+FSA
for a being Int-Location holds not a =0_goto la is halting

proof end;

theorem Th112: :: SCMFSA_2:112

for la being Instruction-Location of SCM+FSA
for a being Int-Location holds not a >0_goto la is halting

proof end;

theorem Th113: :: SCMFSA_2:113

for f being FinSeq-Location
for c, a being Int-Location holds not c := f,a is halting

proof end;

theorem Th114: :: SCMFSA_2:114

for f being FinSeq-Location
for a, c being Int-Location holds not f,a := c is halting

proof end;

theorem Th115: :: SCMFSA_2:115

for f being FinSeq-Location
for c being Int-Location holds not c :=len f is halting

proof end;

theorem Th116: :: SCMFSA_2:116

for f being FinSeq-Location
for c being Int-Location holds not f :=<0,...,0> c is halting

proof end;

theorem :: SCMFSA_2:117

canceled;

theorem :: SCMFSA_2:118

for I being Instruction of SCM+FSA st I = [0 ,{} ] holds
I is halting by Th103, AMI_3:71;

theorem Th119: :: SCMFSA_2:119

for I being Instruction of SCM+FSA st InsCode I = 0 holds
I = [0 ,{} ]

proof end;

theorem Th120: :: SCMFSA_2:120

for I being set holds
( I is Instruction of SCM+FSA iff ( I = [0 ,{} ] or ex a, b being Int-Location st I = a := b or ex a, b being Int-Location st I = AddTo a,b or ex a, b being Int-Location st I = SubFrom a,b or ex a, b being Int-Location st I = MultBy a,b or ex a, b being Int-Location st I = Divide a,b or ex la being Instruction-Location of SCM+FSA st I = goto la or ex lb being Instruction-Location of SCM+FSA ex da being Int-Location st I = da =0_goto lb or ex lb being Instruction-Location of SCM+FSA ex da being Int-Location st I = da >0_goto lb or ex b, a being Int-Location ex fa being FinSeq-Location st I = a := fa,b or ex a, b being Int-Location ex fa being FinSeq-Location st I = fa,a := b or ex a being Int-Location ex f being FinSeq-Location st I = a :=len f or ex a being Int-Location ex f being FinSeq-Location st I = f :=<0,...,0> a ) )

proof end;

Lm1: for W being Instruction of SCM+FSA st W is halting holds
W = [0 ,{} ]

proof end;

registration

cluster SCM+FSA -> strict halting ;
coherence

proof end;

end;

theorem Th121: :: SCMFSA_2:121

for I being Instruction of SCM+FSA st I is halting holds
I = halt SCM+FSA

proof end;

theorem Th122: :: SCMFSA_2:122

for I being Instruction of SCM+FSA st InsCode I = 0 holds
I = halt SCM+FSA

proof end;

theorem Th123: :: SCMFSA_2:123

halt SCM = halt SCM+FSA

proof end;

theorem :: SCMFSA_2:124

InsCode (halt SCM+FSA ) = 0 by Th123, AMI_5:37;

theorem :: SCMFSA_2:125

for i being Instruction of SCM
for I being Instruction of SCM+FSA st i = I & not i is halting holds
not I is halting by Th121, Th123;

theorem :: SCMFSA_2:126

for i, j being natural number holds fsloc i <> intloc j

proof end;

theorem :: SCMFSA_2:127

Data-Locations SCM+FSA = Int-Locations \/ FinSeq-Locations

proof end;