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

begin

definition

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

end;

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

Lm1: NAT c= SCM-Memory
by XBOOLE_1:7;

then Lm2: NAT c= SCM+FSA-Memory
by XBOOLE_1:10;

registration

cluster SCM+FSA -> non empty stored-program standard-ins strict ;
coherence

proof end;

end;

registration

cluster Relation-like NAT -defined Function-like -> the carrier of SCM+FSA -defined set ;
coherence

proof end;

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 = NAT by FUNCT_7:def 1, SCMFSA_1:5;

begin

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 :

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

canceled;

theorem Th9: :: SCMFSA_2:9

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

theorem Th10: :: SCMFSA_2:10

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

theorem Th11: :: SCMFSA_2:11

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

theorem Th12: :: SCMFSA_2:12

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

theorem Th13: :: 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, Lm1;

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;

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

proof end;

end;

:: deftheorem defines intloc SCMFSA_2:def 6 :

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

registration

cluster FinSeq-Locations -> infinite ;
coherence

proof end;

end;

theorem :: SCMFSA_2:21

canceled;

theorem :: SCMFSA_2:22

canceled;

theorem :: SCMFSA_2:23

canceled;

theorem :: SCMFSA_2:24

canceled;

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;

begin

registration

let I be Instruction of SCM+FSA;
cluster I `1_3 -> 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 <= 13

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 :

definition

let la be Element of NAT ;
func goto la -> Instruction of SCM+FSA equals :: SCMFSA_2:def 16
SCM-goto la;
coherence by Th38;
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 st
( a = A & 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 st
( a = A & it = A >0_goto la );
existence

proof end;

correctness ;

end;

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

definition

let i be Int-Location ;
func i :==1 -> Instruction of SCM+FSA equals :: SCMFSA_2:def 23
[13,{},<*i*>];
coherence

proof end;

end;

:: deftheorem defines :==1 SCMFSA_2:def 23 :

theorem :: SCMFSA_2:39

canceled;

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 Element of NAT holds InsCode (goto lb) = 6 by RECDEF_2:def 1;

theorem :: SCMFSA_2:48

for lb being Element of NAT
for a being Int-Location holds InsCode (a =0_goto lb) = 7

proof end;

theorem :: SCMFSA_2:49

for lb being Element of NAT
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 RECDEF_2:def 1;

theorem :: SCMFSA_2:51

for fa being FinSeq-Location
for a, c being Int-Location holds InsCode ((fa,a) := c) = 10 by RECDEF_2:def 1;

theorem :: SCMFSA_2:52

for fa being FinSeq-Location
for a being Int-Location holds InsCode (a :=len fa) = 11 by RECDEF_2:def 1;

theorem :: SCMFSA_2:53

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

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 Element of NAT 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 Element of NAT 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 Element of NAT 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;

LmX: for ins being Instruction of SCM+FSA st InsCode ins = 13 holds
ex a being Int-Location st ins = a :==1

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;

begin

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

proof end;

theorem :: SCMFSA_2:74

for s being State of SCM+FSA
for s9 being State of SCM holds (s +* s9) +* (s | NAT) is State of SCM+FSA

proof end;

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 ) = S . (IC )

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;

[0,{},{}] in SCM+FSA-Instr
by SCMFSA_1:4;

then the haltF of SCM+FSA = [0,{},{}]
by FUNCT_7:def 1;

then Lm3: halt SCM+FSA = [0,{},{}]
;

registration

cluster SCM+FSA -> IC-Ins-separated definite realistic proper-halt strict ;
coherence

proof end;

end;

theorem Th81: :: SCMFSA_2:81

for dl being Int-Location holds dl <> IC

proof end;

theorem Th82: :: SCMFSA_2:82

for dl being FinSeq-Location holds dl <> IC

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 Element of NAT
for dl being Int-Location holds il <> dl

proof end;

theorem :: SCMFSA_2:85

for il being Element of NAT
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 Element of NAT 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;

begin

theorem Th89: :: SCMFSA_2:89

for a, b being Int-Location
for s being State of SCM+FSA holds
( (Exec ((a := b),s)) . (IC ) = succ (IC s) & (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 ) = succ (IC s) & (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 ) = succ (IC s) & (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 ) = succ (IC s) & (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 ) = succ (IC s) & ( 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 ) = succ (IC s) & (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 Element of NAT
for s being State of SCM+FSA holds
( (Exec ((goto l),s)) . (IC ) = 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 Element of NAT
for a being Int-Location
for s being State of SCM+FSA holds
( ( s . a = 0 implies (Exec ((a =0_goto l),s)) . (IC ) = l ) & ( s . a <> 0 implies (Exec ((a =0_goto l),s)) . (IC ) = succ (IC s) ) & ( 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 Element of NAT
for a being Int-Location
for s being State of SCM+FSA holds
( ( s . a > 0 implies (Exec ((a >0_goto l),s)) . (IC ) = l ) & ( s . a <= 0 implies (Exec ((a >0_goto l),s)) . (IC ) = succ (IC s) ) & ( 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 ) = succ (IC s) & 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 ) = succ (IC s) & 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 ) = succ (IC s) & (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 ) = succ (IC s) & 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;

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

proof end;

begin

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 ) = succ (IC s) holds
not I is halting

proof end;

registration

let a, b be Int-Location ;
set s = the State of SCM+FSA;
cluster a := b -> non halting ;
coherence

proof end;

cluster AddTo (a,b) -> non halting ;
coherence

proof end;

cluster SubFrom (a,b) -> non halting ;
coherence

proof end;

cluster MultBy (a,b) -> non halting ;
coherence

proof end;

cluster Divide (a,b) -> non halting ;
coherence

proof end;

end;

theorem :: SCMFSA_2:105

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

theorem :: SCMFSA_2:106

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

theorem :: SCMFSA_2:107

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

theorem :: SCMFSA_2:108

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

theorem :: SCMFSA_2:109

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

registration

let la be Element of NAT ;
cluster goto la -> non halting ;
coherence

proof end;

end;

theorem :: SCMFSA_2:110

for la being Element of NAT holds not goto la is halting ;

registration

let a be Int-Location ;
let la be Element of NAT ;
set f = the Object-Kind of SCM+FSA;
set s = the SCM+FSA-State;
cluster a =0_goto la -> non halting ;
coherence

proof end;

cluster a >0_goto la -> non halting ;
coherence

proof end;

end;

theorem :: SCMFSA_2:111

for la being Element of NAT
for a being Int-Location holds not a =0_goto la is halting ;

theorem :: SCMFSA_2:112

for la being Element of NAT
for a being Int-Location holds not a >0_goto la is halting ;

registration

let c be Int-Location ;
let f be FinSeq-Location ;
let a be Int-Location ;
set s = the State of SCM+FSA;
cluster c := (f,a) -> non halting ;
coherence

proof end;

cluster (f,a) := c -> non halting ;
coherence

proof end;

end;

theorem :: SCMFSA_2:113

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

theorem :: SCMFSA_2:114

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

registration

let c be Int-Location ;
let f be FinSeq-Location ;
set s = the State of SCM+FSA;
cluster c :=len f -> non halting ;
coherence

proof end;

cluster f :=<0,...,0> c -> non halting ;
coherence

proof end;

end;

theorem :: SCMFSA_2:115

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

theorem :: SCMFSA_2:116

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

registration

let a be Int-Location ;
cluster a :==1 -> non halting ;
coherence

proof end;

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 Element of NAT st I = goto la or ex lb being Element of NAT ex da being Int-Location st I = da =0_goto lb or ex lb being Element of NAT 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 or ex a being Int-Location st I = a :==1 ) )

proof end;

Lm4: 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 Th172: :: SCMFSA_2:127

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

proof end;

theorem :: SCMFSA_2:128

for i, j being Nat st i <> j holds
intloc i <> intloc j by AMI_3:52;

theorem :: SCMFSA_2:129

for s being State of SCM+FSA
for n being Element of NAT
for I being Program of SCM+FSA st I +* (Start-At (n,SCM+FSA)) c= s holds
I c= s

proof end;

theorem Th130: :: SCMFSA_2:130

for l being Element of NAT
for a being Int-Location holds not a in dom (Start-At (l,SCM+FSA))

proof end;

theorem Th131: :: SCMFSA_2:131

for l being Element of NAT
for f being FinSeq-Location holds not f in dom (Start-At (l,SCM+FSA))

proof end;

theorem :: SCMFSA_2:132

for l being Element of NAT
for a being Int-Location
for I being Program of SCM+FSA holds not a in dom (I +* (Start-At (l,SCM+FSA)))

proof end;

theorem :: SCMFSA_2:133

for l being Element of NAT
for f being FinSeq-Location
for I being Program of SCM+FSA holds not f in dom (I +* (Start-At (l,SCM+FSA)))

proof end;

begin

theorem :: SCMFSA_2:134

for ins being Instruction of SCM+FSA st InsCode ins = 13 holds
ex a being Int-Location st ins = a :==1 by LmX;

theorem :: SCMFSA_2:135

for a being Int-Location holds not a :==1 is halting ;

theorem :: SCMFSA_2:136

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

theorem :: SCMFSA_2:137

for a being Int-Location holds InsCode (a :==1) = 13 by RECDEF_2:def 1;

theorem :: SCMFSA_2:138

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
NPP s1 = NPP s2

proof end;