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

definition

func SCM+FSA -> strict AMI-Struct over Segm 3 equals :: SCMFSA_2:def 1
AMI-Struct(# SCM+FSA-Memory,(In (NAT,SCM+FSA-Memory)),SCM+FSA-Instr,SCM+FSA-OK,SCM*-VAL,SCM+FSA-Exec #);

coherence
AMI-Struct(# SCM+FSA-Memory,(In (NAT,SCM+FSA-Memory)),SCM+FSA-Instr,SCM+FSA-OK,SCM*-VAL,SCM+FSA-Exec #) is strict AMI-Struct over Segm 3 ;

end;

:: deftheorem defines SCM+FSA SCMFSA_2:def 1 :
SCM+FSA = AMI-Struct(# SCM+FSA-Memory,(In (NAT,SCM+FSA-Memory)),SCM+FSA-Instr,SCM+FSA-OK,SCM*-VAL,SCM+FSA-Exec #);

registration

cluster SCM+FSA -> non empty with_non-empty_values strict ;

coherence
( not SCM+FSA is empty & SCM+FSA is with_non-empty_values ) ;

end;

registration

cluster SCM+FSA -> strict with_non_trivial_Instructions ;

coherence
SCM+FSA is with_non_trivial_Instructions

proof end;

end;

theorem Th1: :: SCMFSA_2:1

IC = NAT by SCMFSA_1:5, SUBSET_1:def 8;

notation

synonym Int-Locations for SCM+FSA-Data-Loc ;

end;

definition

:: original: Int-Locations
redefine func Int-Locations -> Subset of SCM+FSA;
coherence
Int-Locations is Subset of SCM+FSA

proof end;

::$CD

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

coherence
SCM+FSA-Data*-Loc is Subset of SCM+FSA ;

end;

:: deftheorem SCMFSA_2:def 2 :
canceled;

:: deftheorem defines FinSeq-Locations SCMFSA_2:def 3 :
FinSeq-Locations = SCM+FSA-Data*-Loc ;

registration

cluster Int-like for Element of the carrier of SCM+FSA;

existence
ex b₁ being Object of SCM+FSA st b₁ is Int-like

proof end;

end;

definition

mode Int-Location is Int-like Object of SCM+FSA;

::$CD

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

existence
ex b₁ being Object of SCM+FSA st b₁ in SCM+FSA-Data*-Loc

proof end;

end;

:: deftheorem SCMFSA_2:def 4 :
canceled;

:: deftheorem Def3 defines FinSeq-Location SCMFSA_2:def 5 :
for b₁ being Object of SCM+FSA holds
( b₁ is FinSeq-Location iff b₁ in SCM+FSA-Data*-Loc );

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;

::$CT 5

definition

let k be Nat;

func intloc k -> Int-Location equals :: SCMFSA_2:def 6
dl. k;

coherence
dl. k is Int-Location

proof end;

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

coherence
- (k + 1) is FinSeq-Location

proof end;

end;

:: deftheorem defines intloc SCMFSA_2:def 6 :
for k being Nat holds intloc k = dl. k;

:: deftheorem defines fsloc SCMFSA_2:def 7 :
for k being Nat holds fsloc k = - (k + 1);

theorem :: SCMFSA_2:7

for k1, k2 being Nat st k1 <> k2 holds
fsloc k1 <> fsloc k2 ;

theorem :: SCMFSA_2:8

for dl being Int-Location ex i being Nat st dl = intloc i

proof end;

theorem Th4: :: SCMFSA_2:9

for fl being FinSeq-Location ex i being Nat st fl = fsloc i

proof end;

registration

cluster FinSeq-Locations -> infinite ;

coherence
not FinSeq-Locations is finite

proof end;

end;

theorem Th5: :: SCMFSA_2:10

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

proof end;

theorem Th6: :: SCMFSA_2:11

for l being Int-Location holds Values l = INT

proof end;

theorem Th7: :: SCMFSA_2:12

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

proof end;

theorem :: SCMFSA_2:13

canceled;

theorem :: SCMFSA_2:14

canceled;

::$CT 2

theorem Th8: :: SCMFSA_2:15

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

proof end;

theorem Th9: :: SCMFSA_2:16

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

proof end;

theorem Th10: :: SCMFSA_2:17

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

proof end;

definition

let a, b be Int-Location;

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

existence
ex b₁ being Instruction of SCM+FSA ex A, B being Data-Location st
( a = A & b = B & b₁ = A := B )

proof end;

correctness
uniqueness
for b₁, b₂ being Instruction of SCM+FSA st ex A, B being Data-Location st
( a = A & b = B & b₁ = A := B ) & ex A, B being Data-Location st
( a = A & b = B & b₂ = A := B ) holds
b₁ = b₂;
;

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

existence
ex b₁ being Instruction of SCM+FSA ex A, B being Data-Location st
( a = A & b = B & b₁ = AddTo (A,B) )

proof end;

correctness
uniqueness
for b₁, b₂ being Instruction of SCM+FSA st ex A, B being Data-Location st
( a = A & b = B & b₁ = AddTo (A,B) ) & ex A, B being Data-Location st
( a = A & b = B & b₂ = AddTo (A,B) ) holds
b₁ = b₂;
;

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

existence
ex b₁ being Instruction of SCM+FSA ex A, B being Data-Location st
( a = A & b = B & b₁ = SubFrom (A,B) )

proof end;

correctness
uniqueness
for b₁, b₂ being Instruction of SCM+FSA st ex A, B being Data-Location st
( a = A & b = B & b₁ = SubFrom (A,B) ) & ex A, B being Data-Location st
( a = A & b = B & b₂ = SubFrom (A,B) ) holds
b₁ = b₂;
;

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

existence
ex b₁ being Instruction of SCM+FSA ex A, B being Data-Location st
( a = A & b = B & b₁ = MultBy (A,B) )

proof end;

correctness
uniqueness
for b₁, b₂ being Instruction of SCM+FSA st ex A, B being Data-Location st
( a = A & b = B & b₁ = MultBy (A,B) ) & ex A, B being Data-Location st
( a = A & b = B & b₂ = MultBy (A,B) ) holds
b₁ = b₂;
;

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

existence
ex b₁ being Instruction of SCM+FSA ex A, B being Data-Location st
( a = A & b = B & b₁ = Divide (A,B) )

proof end;

correctness
uniqueness
for b₁, b₂ being Instruction of SCM+FSA st ex A, B being Data-Location st
( a = A & b = B & b₁ = Divide (A,B) ) & ex A, B being Data-Location st
( a = A & b = B & b₂ = Divide (A,B) ) holds
b₁ = b₂;
;

end;

:: deftheorem Def6 defines := SCMFSA_2:def 8 :
for a, b being Int-Location
for b₃ being Instruction of SCM+FSA holds
( b₃ = a := b iff ex A, B being Data-Location st
( a = A & b = B & b₃ = A := B ) );

:: deftheorem Def7 defines AddTo SCMFSA_2:def 9 :
for a, b being Int-Location
for b₃ being Instruction of SCM+FSA holds
( b₃ = AddTo (a,b) iff ex A, B being Data-Location st
( a = A & b = B & b₃ = AddTo (A,B) ) );

:: deftheorem Def8 defines SubFrom SCMFSA_2:def 10 :
for a, b being Int-Location
for b₃ being Instruction of SCM+FSA holds
( b₃ = SubFrom (a,b) iff ex A, B being Data-Location st
( a = A & b = B & b₃ = SubFrom (A,B) ) );

:: deftheorem Def9 defines MultBy SCMFSA_2:def 11 :
for a, b being Int-Location
for b₃ being Instruction of SCM+FSA holds
( b₃ = MultBy (a,b) iff ex A, B being Data-Location st
( a = A & b = B & b₃ = MultBy (A,B) ) );

:: deftheorem Def10 defines Divide SCMFSA_2:def 12 :
for a, b being Int-Location
for b₃ being Instruction of SCM+FSA holds
( b₃ = Divide (a,b) iff ex A, B being Data-Location st
( a = A & b = B & b₃ = Divide (A,B) ) );

definition

let la be Nat;

func goto la -> Instruction of SCM+FSA equals :: SCMFSA_2:def 13
SCM-goto la;

coherence
SCM-goto la is Instruction of SCM+FSA by Th10;
let a be Int-Location;

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

existence
ex b₁ being Instruction of SCM+FSA ex A being Data-Location st
( a = A & b₁ = A =0_goto la )

proof end;

correctness
uniqueness
for b₁, b₂ being Instruction of SCM+FSA st ex A being Data-Location st
( a = A & b₁ = A =0_goto la ) & ex A being Data-Location st
( a = A & b₂ = A =0_goto la ) holds
b₁ = b₂;
;

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

existence
ex b₁ being Instruction of SCM+FSA ex A being Data-Location st
( a = A & b₁ = A >0_goto la )

proof end;

correctness
uniqueness
for b₁, b₂ being Instruction of SCM+FSA st ex A being Data-Location st
( a = A & b₁ = A >0_goto la ) & ex A being Data-Location st
( a = A & b₂ = A >0_goto la ) holds
b₁ = b₂;
;

end;

:: deftheorem defines goto SCMFSA_2:def 13 :
for la being Nat holds goto la = SCM-goto la;

:: deftheorem Def12 defines =0_goto SCMFSA_2:def 14 :
for la being Nat
for a being Int-Location
for b₃ being Instruction of SCM+FSA holds
( b₃ = a =0_goto la iff ex A being Data-Location st
( a = A & b₃ = A =0_goto la ) );

:: deftheorem Def13 defines >0_goto SCMFSA_2:def 15 :
for la being Nat
for a being Int-Location
for b₃ being Instruction of SCM+FSA holds
( b₃ = a >0_goto la iff ex A being Data-Location st
( a = A & b₃ = A >0_goto la ) );

definition

let c, i be Int-Location;
let a be FinSeq-Location ;

func c := (a,i) -> Instruction of SCM+FSA equals :: SCMFSA_2:def 16
[9,{},<*c,a,i*>];

coherence
[9,{},<*c,a,i*>] is Instruction of SCM+FSA

proof end;

func (a,i) := c -> Instruction of SCM+FSA equals :: SCMFSA_2:def 17
[10,{},<*c,a,i*>];

coherence
[10,{},<*c,a,i*>] is Instruction of SCM+FSA

proof end;

end;

:: deftheorem defines := SCMFSA_2:def 16 :
for c, i being Int-Location
for a being FinSeq-Location holds c := (a,i) = [9,{},<*c,a,i*>];

:: deftheorem defines := SCMFSA_2:def 17 :
for c, i being Int-Location
for a being FinSeq-Location holds (a,i) := c = [10,{},<*c,a,i*>];

definition

let i be Int-Location;
let a be FinSeq-Location ;

func i :=len a -> Instruction of SCM+FSA equals :: SCMFSA_2:def 18
[11,{},<*i,a*>];

coherence
[11,{},<*i,a*>] is Instruction of SCM+FSA

proof end;

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

coherence
[12,{},<*i,a*>] is Instruction of SCM+FSA

proof end;

end;

:: deftheorem defines :=len SCMFSA_2:def 18 :
for i being Int-Location
for a being FinSeq-Location holds i :=len a = [11,{},<*i,a*>];

:: deftheorem defines :=<0,...,0> SCMFSA_2:def 19 :
for i being Int-Location
for a being FinSeq-Location holds a :=<0,...,0> i = [12,{},<*i,a*>];

theorem :: SCMFSA_2:18

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

proof end;

theorem :: SCMFSA_2:19

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

proof end;

theorem :: SCMFSA_2:20

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

proof end;

theorem :: SCMFSA_2:21

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

proof end;

theorem :: SCMFSA_2:22

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

proof end;

theorem :: SCMFSA_2:23

for lb being Nat holds InsCode (goto lb) = 6 ;

theorem :: SCMFSA_2:24

for lb being Nat
for a being Int-Location holds InsCode (a =0_goto lb) = 7

proof end;

theorem :: SCMFSA_2:25

for lb being Nat
for a being Int-Location holds InsCode (a >0_goto lb) = 8

proof end;

theorem :: SCMFSA_2:26

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

theorem :: SCMFSA_2:27

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

theorem :: SCMFSA_2:28

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

theorem :: SCMFSA_2:29

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

theorem Th23: :: SCMFSA_2:30

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 Th24: :: SCMFSA_2:31

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 Th25: :: SCMFSA_2:32

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 Th26: :: SCMFSA_2:33

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 Th27: :: SCMFSA_2:34

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 Th28: :: SCMFSA_2:35

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

proof end;

theorem Th29: :: SCMFSA_2:36

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

proof end;

theorem Th30: :: SCMFSA_2:37

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

proof end;

theorem Th31: :: SCMFSA_2:38

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

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 Th33: :: SCMFSA_2:40

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 Th34: :: SCMFSA_2:41

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

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

proof end;

theorem :: SCMFSA_2:43

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

proof end;

theorem Th37: :: SCMFSA_2:44

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

proof end;

theorem Th38: :: SCMFSA_2:45

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

proof end;

theorem Th39: :: SCMFSA_2:46

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

proof end;

theorem :: SCMFSA_2:47

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

proof end;

theorem :: SCMFSA_2:48

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

proof end;

theorem Th42: :: SCMFSA_2:49

for s being State of SCM+FSA
for i being Instruction of SCM holds s | SCM-Memory is State of SCM

proof end;

theorem :: SCMFSA_2:50

for s being State of SCM+FSA
for s9 being State of SCM holds s +* s9 is State of SCM+FSA

proof end;

theorem Th44: :: SCMFSA_2:51

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 holds
Exec (ii,ss) = ss +* (Exec (i,s))

proof end;

registration

let s be State of SCM+FSA;
let d be Int-Location;

cluster s . d -> integer ;

coherence
s . d is integer

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
s . d is FinSequence of INT

proof end;

end;

theorem Th45: :: SCMFSA_2:52

for S being State of SCM
for s being State of SCM+FSA st S = s | SCM-Memory holds
s = s +* S by FUNCT_4:75;

theorem Th46: :: SCMFSA_2:53

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

proof end;

theorem Th47: :: SCMFSA_2:54

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

proof end;

theorem Th48: :: SCMFSA_2:55

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 & A = a holds
S . A = s . a

proof end;

registration

cluster SCM+FSA -> IC-Ins-separated strict ;

coherence
SCM+FSA is IC-Ins-separated by SCMFSA_1:5, SCMFSA_1:9, SUBSET_1:def 8;

end;

theorem Th49: :: SCMFSA_2:56

for dl being Int-Location holds dl <> IC by AMI_2:def 16, Th1, FINSET_1:15;

theorem Th50: :: SCMFSA_2:57

for dl being FinSeq-Location holds dl <> IC

proof end;

theorem :: SCMFSA_2:58

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

proof end;

theorem :: SCMFSA_2:59

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

proof end;

theorem :: SCMFSA_2:60

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

proof end;

theorem :: SCMFSA_2:61

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

proof end;

theorem Th55: :: SCMFSA_2:62

for S being State of SCM
for s being State of SCM+FSA st S = s | SCM-Memory holds
IC s = IC S

proof end;

theorem Th56: :: SCMFSA_2:63

for a, b being Int-Location
for s being State of SCM+FSA holds
( (Exec ((a := b),s)) . (IC ) = (IC s) + 1 & (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 Th57: :: SCMFSA_2:64

for a, b being Int-Location
for s being State of SCM+FSA holds
( (Exec ((AddTo (a,b)),s)) . (IC ) = (IC s) + 1 & (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 Th58: :: SCMFSA_2:65

for a, b being Int-Location
for s being State of SCM+FSA holds
( (Exec ((SubFrom (a,b)),s)) . (IC ) = (IC s) + 1 & (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 Th59: :: SCMFSA_2:66

for a, b being Int-Location
for s being State of SCM+FSA holds
( (Exec ((MultBy (a,b)),s)) . (IC ) = (IC s) + 1 & (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 Th60: :: SCMFSA_2:67

for a, b being Int-Location
for s being State of SCM+FSA holds
( (Exec ((Divide (a,b)),s)) . (IC ) = (IC s) + 1 & ( 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:68

for a being Int-Location
for s being State of SCM+FSA holds
( (Exec ((Divide (a,a)),s)) . (IC ) = (IC s) + 1 & (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 Th62: :: SCMFSA_2:69

for l being 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 Th63: :: SCMFSA_2:70

for l being 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 ) = (IC s) + 1 ) & ( 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 Th64: :: SCMFSA_2:71

for l being 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 ) = (IC s) + 1 ) & ( 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 Th65: :: SCMFSA_2:72

for g being FinSeq-Location
for a, c being Int-Location
for s being State of SCM+FSA holds
( (Exec ((c := (g,a)),s)) . (IC ) = (IC s) + 1 & ex k being Nat st
( k = |.(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 Th66: :: SCMFSA_2:73

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 ) = (IC s) + 1 & ex k being Nat st
( k = |.(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 Th67: :: SCMFSA_2:74

for g being FinSeq-Location
for c being Int-Location
for s being State of SCM+FSA holds
( (Exec ((c :=len g),s)) . (IC ) = (IC s) + 1 & (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 Th68: :: SCMFSA_2:75

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 ) = (IC s) + 1 & ex k being Nat st
( k = |.(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:76

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

theorem Th70: :: SCMFSA_2:77

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 Th71: :: SCMFSA_2:78

for I being Instruction of SCM+FSA st ex s being State of SCM+FSA st (Exec (I,s)) . (IC ) = (IC s) + 1 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
not a := b is halting

proof end;

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

coherence
not AddTo (a,b) is halting

proof end;

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

coherence
not SubFrom (a,b) is halting

proof end;

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

coherence
not MultBy (a,b) is halting

proof end;

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

coherence
not Divide (a,b) is halting

proof end;

end;

theorem :: SCMFSA_2:79

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

theorem :: SCMFSA_2:80

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

theorem :: SCMFSA_2:81

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

theorem :: SCMFSA_2:82

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

theorem :: SCMFSA_2:83

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

registration

let la be Nat;

cluster goto la -> non halting ;

coherence
not goto la is halting

proof end;

end;

theorem :: SCMFSA_2:84

for la being Nat holds not goto la is halting ;

registration

let a be Int-Location;
let la be Nat;
set f = the_Values_of SCM+FSA;
set s = the SCM+FSA-State;

cluster a =0_goto la -> non halting ;

coherence
not a =0_goto la is halting

proof end;

cluster a >0_goto la -> non halting ;

coherence
not a >0_goto la is halting

proof end;

end;

theorem :: SCMFSA_2:85

for la being Nat
for a being Int-Location holds not a =0_goto la is halting ;

theorem :: SCMFSA_2:86

for la being 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
not c := (f,a) is halting

proof end;

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

coherence
not (f,a) := c is halting

proof end;

end;

theorem :: SCMFSA_2:87

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

theorem :: SCMFSA_2:88

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
not c :=len f is halting

proof end;

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

coherence
not f :=<0,...,0> c is halting

proof end;

end;

theorem :: SCMFSA_2:89

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

theorem :: SCMFSA_2:90

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

theorem :: SCMFSA_2:91

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

theorem Th85: :: SCMFSA_2:92

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

proof end;

theorem Th86: :: SCMFSA_2:93

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 Nat st I = goto la or ex lb being Nat ex da being Int-Location st I = da =0_goto lb or ex lb being 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 ) )

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
SCM+FSA is halting by Th70, AMI_3:26;

end;

theorem Th87: :: SCMFSA_2:94

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

theorem :: SCMFSA_2:95

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

theorem Th89: :: SCMFSA_2:96

halt SCM = halt SCM+FSA ;

theorem :: SCMFSA_2:97

canceled;

::$CT

theorem :: SCMFSA_2:98

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 Th87, Th89;

theorem :: SCMFSA_2:99

for i, j being Nat holds fsloc i <> intloc j

proof end;

theorem Th92: :: SCMFSA_2:100

Data-Locations = Int-Locations \/ FinSeq-Locations

proof end;

theorem :: SCMFSA_2:101

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

theorem :: SCMFSA_2:102

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

proof end;

theorem :: SCMFSA_2:103

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

proof end;

theorem :: SCMFSA_2:104

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

proof end;

registration

let f be FinSeq-Location ;
let w be FinSequence of INT ;

cluster f .--> w -> data-only for PartState of SCM+FSA;

coherence
for b₁ being PartState of SCM+FSA st b₁ = f .--> w holds
b₁ is data-only by Th50, ZFMISC_1:11;

end;

registration

let x be Int-Location;
let i be Integer;

cluster x .--> i -> data-only for PartState of SCM+FSA;

coherence
for b₁ being PartState of SCM+FSA st b₁ = x .--> i holds
b₁ is data-only by Th49, ZFMISC_1:11;

end;

registration

let a, b be Int-Location;

cluster a := b -> No-StopCode ;

coherence
a := b is No-StopCode

proof end;

end;

registration

let a, b be Int-Location;

cluster AddTo (a,b) -> No-StopCode ;

coherence
AddTo (a,b) is No-StopCode

proof end;

end;

registration

let a, b be Int-Location;

cluster SubFrom (a,b) -> No-StopCode ;

coherence
SubFrom (a,b) is No-StopCode

proof end;

end;

registration

let a, b be Int-Location;

cluster MultBy (a,b) -> No-StopCode ;

coherence
MultBy (a,b) is No-StopCode

proof end;

end;

registration

let a, b be Int-Location;

cluster Divide (a,b) -> No-StopCode ;

coherence
Divide (a,b) is No-StopCode

proof end;

end;

registration

let lb be Nat;

cluster goto lb -> No-StopCode ;

coherence
goto lb is No-StopCode

proof end;

end;

registration

let lb be Nat;
let a be Int-Location;

cluster a =0_goto lb -> No-StopCode ;

coherence
a =0_goto lb is No-StopCode

proof end;

end;

registration

let lb be Nat;
let a be Int-Location;

cluster a >0_goto lb -> No-StopCode ;

coherence
a >0_goto lb is No-StopCode

proof end;

end;

registration

let fa be FinSeq-Location ;
let a, c be Int-Location;

cluster c := (fa,a) -> No-StopCode ;

coherence
c := (fa,a) is No-StopCode

proof end;

end;

registration

let fa be FinSeq-Location ;
let a, c be Int-Location;

cluster (fa,a) := c -> No-StopCode ;

coherence
(fa,a) := c is No-StopCode

proof end;

end;

registration

let fa be FinSeq-Location ;
let a be Int-Location;

cluster a :=len fa -> No-StopCode ;

coherence
a :=len fa is No-StopCode

proof end;

end;

registration

let fa be FinSeq-Location ;
let a be Int-Location;

cluster fa :=<0,...,0> a -> No-StopCode ;

coherence
fa :=<0,...,0> a is No-StopCode

proof end;

end;