:: SCMFSA_2 semantic presentation

theorem Th1: :: SCMFSA_2:1

canceled;

theorem Th2: :: SCMFSA_2:2

canceled;

theorem Th3: :: SCMFSA_2:3

for b₁ being with_non-empty_elements set
for b₂ being non void AMI-Struct of b₁
for b₃ being State of b₂ holds the Instruction-Locations of b₂ c= dom b₃

proof end;

theorem Th4: :: SCMFSA_2:4

for b₁ being with_non-empty_elements set
for b₂ being non empty non void IC-Ins-separated AMI-Struct of b₁
for b₃ being State of b₂ holds IC b₃ in dom b₃

proof end;

theorem Th5: :: SCMFSA_2:5

for b₁ being with_non-empty_elements set
for b₂ being non empty non void AMI-Struct of b₁
for b₃ being State of b₂
for b₄ being Instruction-Location of b₂ holds b₄ in dom b₃

proof end;

definition

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

end;

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

registration

cluster SCM+FSA -> non empty strict non void ;
coherence by AMI_1:def 3, STRUCT_0:def 1;

end;

theorem Th6: :: SCMFSA_2:6

( the Instruction-Locations of SCM+FSA <> INT & the Instructions of SCM+FSA <> INT & the Instruction-Locations of SCM+FSA <> the Instructions of SCM+FSA & the Instruction-Locations of SCM+FSA <> INT * & the Instructions of SCM+FSA <> INT * ) by SCMFSA_1:13;

theorem Th7: :: SCMFSA_2:7

IC SCM+FSA = 0

proof end;

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 Def2 defines Int-Locations SCMFSA_2:def 2 :

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

theorem Th8: :: SCMFSA_2:8

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

definition

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

proof end;

mode FinSeq-Location -> Object of SCM+FSA means :Def5: :: SCMFSA_2:def 5
a₁ 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 Th9: :: SCMFSA_2:9

for b₁ being Int-Location holds b₁ in Int-Locations by Def4;

theorem Th10: :: SCMFSA_2:10

for b₁ being FinSeq-Location holds b₁ in FinSeq-Locations by Def5;

theorem Th11: :: SCMFSA_2:11

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

theorem Th12: :: SCMFSA_2:12

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

theorem Th13: :: SCMFSA_2:13

Int-Locations misses the Instruction-Locations of SCM+FSA by AMI_5:33, SCMFSA_1:def 1, SCMFSA_1:def 3;

theorem Th14: :: SCMFSA_2:14

FinSeq-Locations misses the Instruction-Locations of SCM+FSA

proof end;

theorem Th15: :: SCMFSA_2:15

Int-Locations misses FinSeq-Locations

proof end;

definition

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

proof end;

func insloc c₁ -> Instruction-Location of SCM+FSA equals :: SCMFSA_2:def 7
il. a₁;
coherence by AMI_3:def 1, SCMFSA_1:def 3;
func fsloc c₁ -> FinSeq-Location equals :: SCMFSA_2:def 8
- (a₁ + 1);
coherence

proof end;

end;

:: deftheorem Def6 defines intloc SCMFSA_2:def 6 :

:: deftheorem Def7 defines insloc SCMFSA_2:def 7 :

:: deftheorem Def8 defines fsloc SCMFSA_2:def 8 :

theorem Th16: :: SCMFSA_2:16

for b₁, b₂ being natural number st b₁ <> b₂ holds
intloc b₁ <> intloc b₂ by AMI_3:52;

theorem Th17: :: SCMFSA_2:17

for b₁, b₂ being natural number st b₁ <> b₂ holds
fsloc b₁ <> fsloc b₂

proof end;

theorem Th18: :: SCMFSA_2:18

for b₁, b₂ being natural number st b₁ <> b₂ holds
insloc b₁ <> insloc b₂ by AMI_3:53;

theorem Th19: :: SCMFSA_2:19

for b₁ being Int-Location ex b₂ being Nat st b₁ = intloc b₂

proof end;

theorem Th20: :: SCMFSA_2:20

for b₁ being FinSeq-Location ex b₂ being Nat st b₁ = fsloc b₂

proof end;

theorem Th21: :: SCMFSA_2:21

for b₁ being Instruction-Location of SCM+FSA ex b₂ being Nat st b₁ = insloc b₂

proof end;

theorem Th22: :: SCMFSA_2:22

not Int-Locations is finite by SCMFSA_1:def 1;

theorem Th23: :: SCMFSA_2:23

not FinSeq-Locations is finite

proof end;

theorem Th24: :: SCMFSA_2:24

not the Instruction-Locations of SCM+FSA is finite

proof end;

theorem Th25: :: SCMFSA_2:25

for b₁ being Int-Location holds b₁ is Data-Location

proof end;

theorem Th26: :: SCMFSA_2:26

for b₁ being Int-Location holds ObjectKind b₁ = INT

proof end;

theorem Th27: :: SCMFSA_2:27

for b₁ being FinSeq-Location holds ObjectKind b₁ = INT *

proof end;

theorem Th28: :: SCMFSA_2:28

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

theorem Th29: :: SCMFSA_2:29

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

theorem Th30: :: SCMFSA_2:30

for b₁ being set st b₁ in SCM+FSA-Instr-Loc holds
b₁ is Instruction-Location of SCM+FSA ;

definition

let c₁ be Instruction-Location of SCM+FSA ;
func Next c₁ -> Instruction-Location of SCM+FSA means :Def9: :: SCMFSA_2:def 9
ex b₁ being Element of SCM+FSA-Instr-Loc st
( b₁ = a₁ & a₂ = Next b₁ );
existence

proof end;

correctness ;

end;

:: deftheorem Def9 defines Next SCMFSA_2:def 9 :

theorem Th31: :: SCMFSA_2:31

for b₁ being Instruction-Location of SCM+FSA
for b₂ being Element of SCM+FSA-Instr-Loc st b₂ = b₁ holds
Next b₂ = Next b₁ by Def9;

theorem Th32: :: SCMFSA_2:32

for b₁ being natural number holds Next (insloc b₁) = insloc (b₁ + 1)

proof end;

theorem Th33: :: SCMFSA_2:33

for b₁ being Instruction-Location of SCM+FSA
for b₂ being Instruction-Location of SCM st b₁ = b₂ holds
Next b₁ = Next b₂

proof end;

registration

let c₁ be Instruction of SCM+FSA ;
cluster InsCode a₁ -> natural ;
coherence

proof end;

end;

theorem Th34: :: SCMFSA_2:34

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

proof end;

theorem Th35: :: SCMFSA_2:35

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

proof end;

theorem Th36: :: SCMFSA_2:36

canceled;

theorem Th37: :: SCMFSA_2:37

for b₁ being Instruction of SCM+FSA
for b₂ being Instruction of SCM st b₁ = b₂ holds
InsCode b₁ = InsCode b₂

proof end;

theorem Th38: :: SCMFSA_2:38

for b₁ being Instruction of SCM holds b₁ is Instruction of SCM+FSA

proof end;

definition

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

correctness ;

end;

:: deftheorem Def10 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 Th39: :: SCMFSA_2:39

the Instruction-Locations of SCM = the Instruction-Locations of SCM+FSA by AMI_3:def 1, SCMFSA_1:def 3;

definition

let c₁ be Instruction-Location of SCM+FSA ;
func goto c₁ -> Instruction of SCM+FSA means :Def16: :: SCMFSA_2:def 16
ex b₁ being Instruction-Location of SCM st
( a₁ = b₁ & a₂ = goto b₁ );
existence

proof end;

correctness ;
let c₂ be Int-Location ;
func c₂ =0_goto c₁ -> Instruction of SCM+FSA means :Def17: :: SCMFSA_2:def 17
ex b₁ being Data-Location ex b₂ being Instruction-Location of SCM st
( a₂ = b₁ & a₁ = b₂ & a₃ = b₁ =0_goto b₂ );
existence

proof end;

correctness ;
func c₂ >0_goto c₁ -> Instruction of SCM+FSA means :Def18: :: SCMFSA_2:def 18
ex b₁ being Data-Location ex b₂ being Instruction-Location of SCM st
( a₂ = b₁ & a₁ = b₂ & a₃ = b₁ >0_goto b₂ );
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₁, c₂ be Int-Location ;
let c₃ be FinSeq-Location ;
func c₁ := c₃,c₂ -> Instruction of SCM+FSA equals :: SCMFSA_2:def 19
[9,<*a₁,a₃,a₂*>];
coherence

proof end;

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

proof end;

end;

:: deftheorem Def19 defines := SCMFSA_2:def 19 :

:: deftheorem Def20 defines := SCMFSA_2:def 20 :

definition

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

proof end;

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

proof end;

end;

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

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

theorem Th40: :: SCMFSA_2:40

canceled;

theorem Th41: :: SCMFSA_2:41

canceled;

theorem Th42: :: SCMFSA_2:42

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

proof end;

theorem Th43: :: SCMFSA_2:43

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

proof end;

theorem Th44: :: SCMFSA_2:44

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

proof end;

theorem Th45: :: SCMFSA_2:45

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

proof end;

theorem Th46: :: SCMFSA_2:46

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

proof end;

theorem Th47: :: SCMFSA_2:47

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

proof end;

theorem Th48: :: SCMFSA_2:48

for b₁ being Instruction-Location of SCM+FSA
for b₂ being Int-Location holds InsCode (b₂ =0_goto b₁) = 7

proof end;

theorem Th49: :: SCMFSA_2:49

for b₁ being Instruction-Location of SCM+FSA
for b₂ being Int-Location holds InsCode (b₂ >0_goto b₁) = 8

proof end;

theorem Th50: :: SCMFSA_2:50

for b₁ being FinSeq-Location
for b₂, b₃ being Int-Location holds InsCode (b₂ := b₁,b₃) = 9

proof end;

theorem Th51: :: SCMFSA_2:51

for b₁ being FinSeq-Location
for b₂, b₃ being Int-Location holds InsCode (b₁,b₂ := b₃) = 10

proof end;

theorem Th52: :: SCMFSA_2:52

for b₁ being FinSeq-Location
for b₂ being Int-Location holds InsCode (b₂ :=len b₁) = 11

proof end;

theorem Th53: :: SCMFSA_2:53

for b₁ being FinSeq-Location
for b₂ being Int-Location holds InsCode (b₁ :=<0,...,0> b₂) = 12

proof end;

theorem Th54: :: SCMFSA_2:54

for b₁ being Instruction of SCM+FSA st InsCode b₁ = 1 holds
ex b₂, b₃ being Int-Location st b₁ = b₂ := b₃

proof end;

theorem Th55: :: SCMFSA_2:55

for b₁ being Instruction of SCM+FSA st InsCode b₁ = 2 holds
ex b₂, b₃ being Int-Location st b₁ = AddTo b₂,b₃

proof end;

theorem Th56: :: SCMFSA_2:56

for b₁ being Instruction of SCM+FSA st InsCode b₁ = 3 holds
ex b₂, b₃ being Int-Location st b₁ = SubFrom b₂,b₃

proof end;

theorem Th57: :: SCMFSA_2:57

for b₁ being Instruction of SCM+FSA st InsCode b₁ = 4 holds
ex b₂, b₃ being Int-Location st b₁ = MultBy b₂,b₃

proof end;

theorem Th58: :: SCMFSA_2:58

for b₁ being Instruction of SCM+FSA st InsCode b₁ = 5 holds
ex b₂, b₃ being Int-Location st b₁ = Divide b₂,b₃

proof end;

theorem Th59: :: SCMFSA_2:59

for b₁ being Instruction of SCM+FSA st InsCode b₁ = 6 holds
ex b₂ being Instruction-Location of SCM+FSA st b₁ = goto b₂

proof end;

theorem Th60: :: SCMFSA_2:60

for b₁ being Instruction of SCM+FSA st InsCode b₁ = 7 holds
ex b₂ being Instruction-Location of SCM+FSA ex b₃ being Int-Location st b₁ = b₃ =0_goto b₂

proof end;

theorem Th61: :: SCMFSA_2:61

for b₁ being Instruction of SCM+FSA st InsCode b₁ = 8 holds
ex b₂ being Instruction-Location of SCM+FSA ex b₃ being Int-Location st b₁ = b₃ >0_goto b₂

proof end;

theorem Th62: :: SCMFSA_2:62

for b₁ being Instruction of SCM+FSA st InsCode b₁ = 9 holds
ex b₂, b₃ being Int-Location ex b₄ being FinSeq-Location st b₁ = b₃ := b₄,b₂

proof end;

theorem Th63: :: SCMFSA_2:63

for b₁ being Instruction of SCM+FSA st InsCode b₁ = 10 holds
ex b₂, b₃ being Int-Location ex b₄ being FinSeq-Location st b₁ = b₄,b₂ := b₃

proof end;

theorem Th64: :: SCMFSA_2:64

for b₁ being Instruction of SCM+FSA st InsCode b₁ = 11 holds
ex b₂ being Int-Location ex b₃ being FinSeq-Location st b₁ = b₂ :=len b₃

proof end;

theorem Th65: :: SCMFSA_2:65

for b₁ being Instruction of SCM+FSA st InsCode b₁ = 12 holds
ex b₂ being Int-Location ex b₃ being FinSeq-Location st b₁ = b₃ :=<0,...,0> b₂

proof end;

theorem Th66: :: SCMFSA_2:66

for b₁ being State of SCM+FSA
for b₂ being Int-Location holds b₂ in dom b₁

proof end;

theorem Th67: :: SCMFSA_2:67

for b₁ being FinSeq-Location
for b₂ being State of SCM+FSA holds b₁ in dom b₂

proof end;

theorem Th68: :: SCMFSA_2:68

for b₁ being FinSeq-Location
for b₂ being State of SCM holds not b₁ in dom b₂

proof end;

theorem Th69: :: SCMFSA_2:69

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

proof end;

theorem Th70: :: SCMFSA_2:70

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

proof end;

theorem Th71: :: SCMFSA_2:71

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

proof end;

theorem Th72: :: SCMFSA_2:72

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

proof end;

theorem Th73: :: SCMFSA_2:73

for b₁ being State of SCM+FSA
for b₂ being Instruction of SCM holds (b₁ | NAT ) +* (SCM-Instr-Loc --> b₂) is State of SCM by AMI_3:def 1, SCMFSA_1:18;

theorem Th74: :: SCMFSA_2:74

for b₁ being State of SCM+FSA
for b₂ being State of SCM holds (b₁ +* b₂) +* (b₁ | SCM+FSA-Instr-Loc ) is State of SCM+FSA by AMI_3:def 1, SCMFSA_1:19;

theorem Th75: :: SCMFSA_2:75

for b₁ being Instruction of SCM
for b₂ being Instruction of SCM+FSA
for b₃ being State of SCM
for b₄ being State of SCM+FSA st b₁ = b₂ & b₃ = (b₄ | NAT ) +* (SCM-Instr-Loc --> b₁) holds
Exec b₂,b₄ = (b₄ +* (Exec b₁,b₃)) +* (b₄ | SCM+FSA-Instr-Loc )

proof end;

definition

let c₁ be State of SCM+FSA ;
let c₂ be Int-Location ;
redefine func . as c₁ . c₂ -> Integer;
coherence

proof end;

end;

definition

let c₁ be State of SCM+FSA ;
let c₂ be FinSeq-Location ;
redefine func . as c₁ . c₂ -> FinSequence of INT ;
coherence

proof end;

end;

theorem Th76: :: SCMFSA_2:76

for b₁ being Instruction of SCM
for b₂ being State of SCM
for b₃ being State of SCM+FSA st b₂ = (b₃ | NAT ) +* (SCM-Instr-Loc --> b₁) holds
b₃ = (b₃ +* b₂) +* (b₃ | SCM+FSA-Instr-Loc )

proof end;

theorem Th77: :: SCMFSA_2:77

for b₁ being Instruction of SCM+FSA
for b₂ being State of SCM+FSA
for b₃ being Element of SCM+FSA-Instr st b₃ = b₁ holds
for b₄ being SCM+FSA-State st b₄ = b₂ holds
Exec b₁,b₂ = SCM+FSA-Exec-Res b₃,b₄ by SCMFSA_1:def 18;

theorem Th78: :: SCMFSA_2:78

for b₁ being State of SCM
for b₂, b₃ being State of SCM+FSA st b₂ = (b₃ +* b₁) +* (b₃ | SCM+FSA-Instr-Loc ) holds
b₂ . (IC SCM+FSA ) = b₁ . (IC SCM )

proof end;

theorem Th79: :: SCMFSA_2:79

for b₁ being Data-Location
for b₂ being Int-Location
for b₃ being State of SCM
for b₄, b₅ being State of SCM+FSA st b₄ = (b₅ +* b₃) +* (b₅ | SCM+FSA-Instr-Loc ) & b₁ = b₂ holds
b₃ . b₁ = b₄ . b₂

proof end;

theorem Th80: :: SCMFSA_2:80

for b₁ being Instruction of SCM
for b₂ being Data-Location
for b₃ being Int-Location
for b₄ being State of SCM
for b₅ being State of SCM+FSA st b₄ = (b₅ | NAT ) +* (SCM-Instr-Loc --> b₁) & b₂ = b₃ holds
b₄ . b₂ = b₅ . b₃

proof end;

registration

cluster SCM+FSA -> non empty strict non void IC-Ins-separated data-oriented steady-programmed definite realistic ;
coherence

proof end;

end;

theorem Th81: :: SCMFSA_2:81

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

proof end;

theorem Th82: :: SCMFSA_2:82

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

proof end;

theorem Th83: :: SCMFSA_2:83

for b₁ being Int-Location
for b₂ being FinSeq-Location holds b₁ <> b₂

proof end;

theorem Th84: :: SCMFSA_2:84

for b₁ being Instruction-Location of SCM+FSA
for b₂ being Int-Location holds b₁ <> b₂

proof end;

theorem Th85: :: SCMFSA_2:85

for b₁ being Instruction-Location of SCM+FSA
for b₂ being FinSeq-Location holds b₁ <> b₂

proof end;

theorem Th86: :: SCMFSA_2:86

for b₁, b₂ being State of SCM+FSA st IC b₁ = IC b₂ & ( for b₃ being Int-Location holds b₁ . b₃ = b₂ . b₃ ) & ( for b₃ being FinSeq-Location holds b₁ . b₃ = b₂ . b₃ ) & ( for b₃ being Instruction-Location of SCM+FSA holds b₁ . b₃ = b₂ . b₃ ) holds
b₁ = b₂

proof end;

theorem Th87: :: SCMFSA_2:87

canceled;

theorem Th88: :: SCMFSA_2:88

for b₁ being Instruction of SCM
for b₂ being State of SCM
for b₃ being State of SCM+FSA st b₂ = (b₃ | NAT ) +* (SCM-Instr-Loc --> b₁) holds
IC b₃ = IC b₂

proof end;

theorem Th89: :: SCMFSA_2:89

for b₁, b₂ being Int-Location
for b₃ being State of SCM+FSA holds
( (Exec (b₁ := b₂),b₃) . (IC SCM+FSA ) = Next (IC b₃) & (Exec (b₁ := b₂),b₃) . b₁ = b₃ . b₂ & ( for b₄ being Int-Location st b₄ <> b₁ holds
(Exec (b₁ := b₂),b₃) . b₄ = b₃ . b₄ ) & ( for b₄ being FinSeq-Location holds (Exec (b₁ := b₂),b₃) . b₄ = b₃ . b₄ ) )

proof end;

theorem Th90: :: SCMFSA_2:90

for b₁, b₂ being Int-Location
for b₃ being State of SCM+FSA holds
( (Exec (AddTo b₁,b₂),b₃) . (IC SCM+FSA ) = Next (IC b₃) & (Exec (AddTo b₁,b₂),b₃) . b₁ = (b₃ . b₁) + (b₃ . b₂) & ( for b₄ being Int-Location st b₄ <> b₁ holds
(Exec (AddTo b₁,b₂),b₃) . b₄ = b₃ . b₄ ) & ( for b₄ being FinSeq-Location holds (Exec (AddTo b₁,b₂),b₃) . b₄ = b₃ . b₄ ) )

proof end;

theorem Th91: :: SCMFSA_2:91

for b₁, b₂ being Int-Location
for b₃ being State of SCM+FSA holds
( (Exec (SubFrom b₁,b₂),b₃) . (IC SCM+FSA ) = Next (IC b₃) & (Exec (SubFrom b₁,b₂),b₃) . b₁ = (b₃ . b₁) - (b₃ . b₂) & ( for b₄ being Int-Location st b₄ <> b₁ holds
(Exec (SubFrom b₁,b₂),b₃) . b₄ = b₃ . b₄ ) & ( for b₄ being FinSeq-Location holds (Exec (SubFrom b₁,b₂),b₃) . b₄ = b₃ . b₄ ) )

proof end;

theorem Th92: :: SCMFSA_2:92

for b₁, b₂ being Int-Location
for b₃ being State of SCM+FSA holds
( (Exec (MultBy b₁,b₂),b₃) . (IC SCM+FSA ) = Next (IC b₃) & (Exec (MultBy b₁,b₂),b₃) . b₁ = (b₃ . b₁) * (b₃ . b₂) & ( for b₄ being Int-Location st b₄ <> b₁ holds
(Exec (MultBy b₁,b₂),b₃) . b₄ = b₃ . b₄ ) & ( for b₄ being FinSeq-Location holds (Exec (MultBy b₁,b₂),b₃) . b₄ = b₃ . b₄ ) )

proof end;

theorem Th93: :: SCMFSA_2:93

for b₁, b₂ being Int-Location
for b₃ being State of SCM+FSA holds
( (Exec (Divide b₁,b₂),b₃) . (IC SCM+FSA ) = Next (IC b₃) & ( b₁ <> b₂ implies (Exec (Divide b₁,b₂),b₃) . b₁ = (b₃ . b₁) div (b₃ . b₂) ) & (Exec (Divide b₁,b₂),b₃) . b₂ = (b₃ . b₁) mod (b₃ . b₂) & ( for b₄ being Int-Location st b₄ <> b₁ & b₄ <> b₂ holds
(Exec (Divide b₁,b₂),b₃) . b₄ = b₃ . b₄ ) & ( for b₄ being FinSeq-Location holds (Exec (Divide b₁,b₂),b₃) . b₄ = b₃ . b₄ ) )

proof end;

theorem Th94: :: SCMFSA_2:94

for b₁ being Int-Location
for b₂ being State of SCM+FSA holds
( (Exec (Divide b₁,b₁),b₂) . (IC SCM+FSA ) = Next (IC b₂) & (Exec (Divide b₁,b₁),b₂) . b₁ = (b₂ . b₁) mod (b₂ . b₁) & ( for b₃ being Int-Location st b₃ <> b₁ holds
(Exec (Divide b₁,b₁),b₂) . b₃ = b₂ . b₃ ) & ( for b₃ being FinSeq-Location holds (Exec (Divide b₁,b₁),b₂) . b₃ = b₂ . b₃ ) )

proof end;

theorem Th95: :: SCMFSA_2:95

for b₁ being Instruction-Location of SCM+FSA
for b₂ being State of SCM+FSA holds
( (Exec (goto b₁),b₂) . (IC SCM+FSA ) = b₁ & ( for b₃ being Int-Location holds (Exec (goto b₁),b₂) . b₃ = b₂ . b₃ ) & ( for b₃ being FinSeq-Location holds (Exec (goto b₁),b₂) . b₃ = b₂ . b₃ ) )

proof end;

theorem Th96: :: SCMFSA_2:96

for b₁ being Instruction-Location of SCM+FSA
for b₂ being Int-Location
for b₃ being State of SCM+FSA holds
( ( b₃ . b₂ = 0 implies (Exec (b₂ =0_goto b₁),b₃) . (IC SCM+FSA ) = b₁ ) & ( b₃ . b₂ <> 0 implies (Exec (b₂ =0_goto b₁),b₃) . (IC SCM+FSA ) = Next (IC b₃) ) & ( for b₄ being Int-Location holds (Exec (b₂ =0_goto b₁),b₃) . b₄ = b₃ . b₄ ) & ( for b₄ being FinSeq-Location holds (Exec (b₂ =0_goto b₁),b₃) . b₄ = b₃ . b₄ ) )

proof end;

theorem Th97: :: SCMFSA_2:97

for b₁ being Instruction-Location of SCM+FSA
for b₂ being Int-Location
for b₃ being State of SCM+FSA holds
( ( b₃ . b₂ > 0 implies (Exec (b₂ >0_goto b₁),b₃) . (IC SCM+FSA ) = b₁ ) & ( b₃ . b₂ <= 0 implies (Exec (b₂ >0_goto b₁),b₃) . (IC SCM+FSA ) = Next (IC b₃) ) & ( for b₄ being Int-Location holds (Exec (b₂ >0_goto b₁),b₃) . b₄ = b₃ . b₄ ) & ( for b₄ being FinSeq-Location holds (Exec (b₂ >0_goto b₁),b₃) . b₄ = b₃ . b₄ ) )

proof end;

theorem Th98: :: SCMFSA_2:98

for b₁ being FinSeq-Location
for b₂, b₃ being Int-Location
for b₄ being State of SCM+FSA holds
( (Exec (b₂ := b₁,b₃),b₄) . (IC SCM+FSA ) = Next (IC b₄) & ex b₅ being Nat st
( b₅ = abs (b₄ . b₃) & (Exec (b₂ := b₁,b₃),b₄) . b₂ = (b₄ . b₁) /. b₅ ) & ( for b₅ being Int-Location st b₅ <> b₂ holds
(Exec (b₂ := b₁,b₃),b₄) . b₅ = b₄ . b₅ ) & ( for b₅ being FinSeq-Location holds (Exec (b₂ := b₁,b₃),b₄) . b₅ = b₄ . b₅ ) )

proof end;

theorem Th99: :: SCMFSA_2:99

for b₁ being FinSeq-Location
for b₂, b₃ being Int-Location
for b₄ being State of SCM+FSA holds
( (Exec (b₁,b₂ := b₃),b₄) . (IC SCM+FSA ) = Next (IC b₄) & ex b₅ being Nat st
( b₅ = abs (b₄ . b₂) & (Exec (b₁,b₂ := b₃),b₄) . b₁ = (b₄ . b₁) +* b₅,(b₄ . b₃) ) & ( for b₅ being Int-Location holds (Exec (b₁,b₂ := b₃),b₄) . b₅ = b₄ . b₅ ) & ( for b₅ being FinSeq-Location st b₅ <> b₁ holds
(Exec (b₁,b₂ := b₃),b₄) . b₅ = b₄ . b₅ ) )

proof end;

theorem Th100: :: SCMFSA_2:100

for b₁ being FinSeq-Location
for b₂ being Int-Location
for b₃ being State of SCM+FSA holds
( (Exec (b₂ :=len b₁),b₃) . (IC SCM+FSA ) = Next (IC b₃) & (Exec (b₂ :=len b₁),b₃) . b₂ = len (b₃ . b₁) & ( for b₄ being Int-Location st b₄ <> b₂ holds
(Exec (b₂ :=len b₁),b₃) . b₄ = b₃ . b₄ ) & ( for b₄ being FinSeq-Location holds (Exec (b₂ :=len b₁),b₃) . b₄ = b₃ . b₄ ) )

proof end;

theorem Th101: :: SCMFSA_2:101

for b₁ being FinSeq-Location
for b₂ being Int-Location
for b₃ being State of SCM+FSA holds
( (Exec (b₁ :=<0,...,0> b₂),b₃) . (IC SCM+FSA ) = Next (IC b₃) & ex b₄ being Nat st
( b₄ = abs (b₃ . b₂) & (Exec (b₁ :=<0,...,0> b₂),b₃) . b₁ = b₄ |-> 0 ) & ( for b₄ being Int-Location holds (Exec (b₁ :=<0,...,0> b₂),b₃) . b₄ = b₃ . b₄ ) & ( for b₄ being FinSeq-Location st b₄ <> b₁ holds
(Exec (b₁ :=<0,...,0> b₂),b₃) . b₄ = b₃ . b₄ ) )

proof end;

theorem Th102: :: SCMFSA_2:102

for b₁ being State of SCM+FSA
for b₂ being SCM+FSA-State st b₂ = b₁ holds
IC b₁ = IC b₂ by SCMFSA_1:def 16, Th7;

theorem Th103: :: SCMFSA_2:103

for b₁ being Instruction of SCM
for b₂ being Instruction of SCM+FSA st b₁ = b₂ & b₁ is halting holds
b₂ is halting

proof end;

theorem Th104: :: SCMFSA_2:104

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

proof end;

theorem Th105: :: SCMFSA_2:105

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

proof end;

theorem Th106: :: SCMFSA_2:106

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

proof end;

theorem Th107: :: SCMFSA_2:107

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

proof end;

theorem Th108: :: SCMFSA_2:108

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

proof end;

theorem Th109: :: SCMFSA_2:109

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

proof end;

theorem Th110: :: SCMFSA_2:110

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

proof end;

theorem Th111: :: SCMFSA_2:111

for b₁ being Instruction-Location of SCM+FSA
for b₂ being Int-Location holds not b₂ =0_goto b₁ is halting

proof end;

theorem Th112: :: SCMFSA_2:112

for b₁ being Instruction-Location of SCM+FSA
for b₂ being Int-Location holds not b₂ >0_goto b₁ is halting

proof end;

theorem Th113: :: SCMFSA_2:113

for b₁ being FinSeq-Location
for b₂, b₃ being Int-Location holds not b₂ := b₁,b₃ is halting

proof end;

theorem Th114: :: SCMFSA_2:114

for b₁ being FinSeq-Location
for b₂, b₃ being Int-Location holds not b₁,b₂ := b₃ is halting

proof end;

theorem Th115: :: SCMFSA_2:115

for b₁ being FinSeq-Location
for b₂ being Int-Location holds not b₂ :=len b₁ is halting

proof end;

theorem Th116: :: SCMFSA_2:116

for b₁ being FinSeq-Location
for b₂ being Int-Location holds not b₁ :=<0,...,0> b₂ is halting

proof end;

theorem Th117: :: SCMFSA_2:117

[0,{} ] is Instruction of SCM+FSA by SCMFSA_1:4;

theorem Th118: :: SCMFSA_2:118

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

theorem Th119: :: SCMFSA_2:119

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

proof end;

theorem Th120: :: SCMFSA_2:120

for b₁ being set holds
( b₁ is Instruction of SCM+FSA iff ( b₁ = [0,{} ] or ex b₂, b₃ being Int-Location st b₁ = b₂ := b₃ or ex b₂, b₃ being Int-Location st b₁ = AddTo b₂,b₃ or ex b₂, b₃ being Int-Location st b₁ = SubFrom b₂,b₃ or ex b₂, b₃ being Int-Location st b₁ = MultBy b₂,b₃ or ex b₂, b₃ being Int-Location st b₁ = Divide b₂,b₃ or ex b₂ being Instruction-Location of SCM+FSA st b₁ = goto b₂ or ex b₂ being Instruction-Location of SCM+FSA ex b₃ being Int-Location st b₁ = b₃ =0_goto b₂ or ex b₂ being Instruction-Location of SCM+FSA ex b₃ being Int-Location st b₁ = b₃ >0_goto b₂ or ex b₂, b₃ being Int-Location ex b₄ being FinSeq-Location st b₁ = b₃ := b₄,b₂ or ex b₂, b₃ being Int-Location ex b₄ being FinSeq-Location st b₁ = b₄,b₂ := b₃ or ex b₂ being Int-Location ex b₃ being FinSeq-Location st b₁ = b₂ :=len b₃ or ex b₂ being Int-Location ex b₃ being FinSeq-Location st b₁ = b₃ :=<0,...,0> b₂ ) )

proof end;

registration

cluster SCM+FSA -> non empty strict non void halting IC-Ins-separated data-oriented steady-programmed definite realistic ;
coherence

proof end;

end;

theorem Th121: :: SCMFSA_2:121

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

proof end;

theorem Th122: :: SCMFSA_2:122

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

proof end;

theorem Th123: :: SCMFSA_2:123

halt SCM = halt SCM+FSA

proof end;

theorem Th124: :: SCMFSA_2:124

InsCode (halt SCM+FSA ) = 0

proof end;

theorem Th125: :: SCMFSA_2:125

for b₁ being Instruction of SCM
for b₂ being Instruction of SCM+FSA st b₁ = b₂ & not b₁ is halting holds
not b₂ is halting by Th121, Th123;