:: SCMFSA_4 semantic presentation

registration

let c₁ be set ;
let c₂ be AMI-Struct of c₁;
cluster -> finite FinPartState of a₂;
coherence by AMI_1:def 24;

end;

registration

let c₁ be set ;
let c₂ be AMI-Struct of c₁;
cluster finite programmed FinPartState of a₂;
existence

proof end;

end;

theorem Th1: :: SCMFSA_4:1

for b₁ being with_non-empty_elements set
for b₂ being non empty non void definite AMI-Struct of b₁
for b₃ being programmed FinPartState of b₂ holds rng b₃ c= the Instructions of b₂

proof end;

definition

let c₁ be set ;
let c₂ be AMI-Struct of c₁;
let c₃, c₄ be programmed FinPartState of c₂;
redefine func +* as c₃ +* c₄ -> programmed FinPartState of a₂;
coherence by AMI_3:35;

end;

theorem Th2: :: SCMFSA_4:2

for b₁ being with_non-empty_elements set
for b₂ being non empty non void definite AMI-Struct of b₁
for b₃ being Function of the Instructions of b₂,the Instructions of b₂
for b₄ being programmed FinPartState of b₂ holds dom (b₃ * b₄) = dom b₄

proof end;

definition

let c₁ be Instruction-Location of SCM+FSA ;
let c₂ be Nat;
func c₁ + c₂ -> Instruction-Location of SCM+FSA means :Def1: :: SCMFSA_4:def 1
ex b₁ being Nat st
( a₁ = insloc b₁ & a₃ = insloc (b₁ + a₂) );
existence

proof end;

uniqueness by SCMFSA_2:18;
func c₁ -' c₂ -> Instruction-Location of SCM+FSA means :Def2: :: SCMFSA_4:def 2
ex b₁ being Nat st
( a₁ = insloc b₁ & a₃ = insloc (b₁ -' a₂) );
existence

proof end;

uniqueness by SCMFSA_2:18;

end;

:: deftheorem Def1 defines + SCMFSA_4:def 1 :

:: deftheorem Def2 defines -' SCMFSA_4:def 2 :

theorem Th3: :: SCMFSA_4:3

for b₁ being Instruction-Location of SCM+FSA
for b₂, b₃ being Nat holds (b₁ + b₂) + b₃ = b₁ + (b₂ + b₃)

proof end;

theorem Th4: :: SCMFSA_4:4

for b₁ being Instruction-Location of SCM+FSA
for b₂ being Nat holds (b₁ + b₂) -' b₂ = b₁

proof end;

theorem Th5: :: SCMFSA_4:5

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

proof end;

theorem Th6: :: SCMFSA_4:6

for b₁, b₂ being Instruction-Location of SCM+FSA
for b₃ being Nat holds
( Start-At (b₁ + b₃) = Start-At (b₂ + b₃) iff Start-At b₁ = Start-At b₂ )

proof end;

theorem Th7: :: SCMFSA_4:7

for b₁, b₂ being Instruction-Location of SCM+FSA
for b₃ being Nat st Start-At b₁ = Start-At b₂ holds
Start-At (b₁ -' b₃) = Start-At (b₂ -' b₃)

proof end;

definition

let c₁ be Instruction of SCM+FSA ;
let c₂ be Nat;
func IncAddr c₁,c₂ -> Instruction of SCM+FSA means :Def3: :: SCMFSA_4:def 3
ex b₁ being Instruction of SCM st
( b₁ = a₁ & a₃ = IncAddr b₁,a₂ ) if InsCode a₁ in {6,7,8}
otherwise a₃ = a₁;
existence

proof end;

correctness ;

end;

:: deftheorem Def3 defines IncAddr SCMFSA_4:def 3 :

theorem Th8: :: SCMFSA_4:8

for b₁ being Nat holds IncAddr (halt SCM+FSA ),b₁ = halt SCM+FSA

proof end;

theorem Th9: :: SCMFSA_4:9

for b₁ being Nat
for b₂, b₃ being Int-Location holds IncAddr (b₂ := b₃),b₁ = b₂ := b₃

proof end;

theorem Th10: :: SCMFSA_4:10

for b₁ being Nat
for b₂, b₃ being Int-Location holds IncAddr (AddTo b₂,b₃),b₁ = AddTo b₂,b₃

proof end;

theorem Th11: :: SCMFSA_4:11

for b₁ being Nat
for b₂, b₃ being Int-Location holds IncAddr (SubFrom b₂,b₃),b₁ = SubFrom b₂,b₃

proof end;

theorem Th12: :: SCMFSA_4:12

for b₁ being Nat
for b₂, b₃ being Int-Location holds IncAddr (MultBy b₂,b₃),b₁ = MultBy b₂,b₃

proof end;

theorem Th13: :: SCMFSA_4:13

for b₁ being Nat
for b₂, b₃ being Int-Location holds IncAddr (Divide b₂,b₃),b₁ = Divide b₂,b₃

proof end;

theorem Th14: :: SCMFSA_4:14

for b₁ being Nat
for b₂ being Instruction-Location of SCM+FSA holds IncAddr (goto b₂),b₁ = goto (b₂ + b₁)

proof end;

theorem Th15: :: SCMFSA_4:15

for b₁ being Nat
for b₂ being Instruction-Location of SCM+FSA
for b₃ being Int-Location holds IncAddr (b₃ =0_goto b₂),b₁ = b₃ =0_goto (b₂ + b₁)

proof end;

theorem Th16: :: SCMFSA_4:16

for b₁ being Nat
for b₂ being Instruction-Location of SCM+FSA
for b₃ being Int-Location holds IncAddr (b₃ >0_goto b₂),b₁ = b₃ >0_goto (b₂ + b₁)

proof end;

theorem Th17: :: SCMFSA_4:17

for b₁ being Nat
for b₂, b₃ being Int-Location
for b₄ being FinSeq-Location holds IncAddr (b₃ := b₄,b₂),b₁ = b₃ := b₄,b₂

proof end;

theorem Th18: :: SCMFSA_4:18

for b₁ being Nat
for b₂, b₃ being Int-Location
for b₄ being FinSeq-Location holds IncAddr (b₄,b₂ := b₃),b₁ = b₄,b₂ := b₃

proof end;

theorem Th19: :: SCMFSA_4:19

for b₁ being Nat
for b₂ being Int-Location
for b₃ being FinSeq-Location holds IncAddr (b₂ :=len b₃),b₁ = b₂ :=len b₃

proof end;

theorem Th20: :: SCMFSA_4:20

for b₁ being Nat
for b₂ being Int-Location
for b₃ being FinSeq-Location holds IncAddr (b₃ :=<0,...,0> b₂),b₁ = b₃ :=<0,...,0> b₂

proof end;

theorem Th21: :: SCMFSA_4:21

for b₁ being Nat
for b₂ being Instruction of SCM+FSA
for b₃ being Instruction of SCM st b₂ = b₃ holds
IncAddr b₂,b₁ = IncAddr b₃,b₁

proof end;

theorem Th22: :: SCMFSA_4:22

for b₁ being Instruction of SCM+FSA
for b₂ being Nat holds InsCode (IncAddr b₁,b₂) = InsCode b₁

proof end;

definition

let c₁ be FinPartState of SCM+FSA ;
attr a₁ is initial means :: SCMFSA_4:def 4
for b₁, b₂ being Nat st insloc b₂ in dom a₁ & b₁ < b₂ holds
insloc b₁ in dom a₁;

end;

:: deftheorem Def4 defines initial SCMFSA_4:def 4 :

definition

func SCM+FSA-Stop -> FinPartState of SCM+FSA equals :: SCMFSA_4:def 5
(insloc 0) .--> (halt SCM+FSA );
correctness ;

end;

:: deftheorem Def5 defines SCM+FSA-Stop SCMFSA_4:def 5 :

registration

cluster SCM+FSA-Stop -> non empty finite programmed initial ;
coherence

proof end;

end;

registration

cluster non empty finite programmed initial FinPartState of SCM+FSA ;
existence

proof end;

end;

registration

let c₁ be Function;
let c₂ be finite Function;
cluster a₂ * a₁ -> finite ;
coherence

proof end;

end;

definition

let c₁ be non empty with_non-empty_elements set ;
let c₂ be non empty non void definite AMI-Struct of c₁;
let c₃ be programmed FinPartState of c₂;
let c₄ be Function of the Instructions of c₂,the Instructions of c₂;
redefine func * as c₄ * c₃ -> programmed FinPartState of a₂;
coherence

proof end;

end;

theorem Th23: :: SCMFSA_4:23

for b₁, b₂ being Nat
for b₃ being Instruction of SCM+FSA holds IncAddr (IncAddr b₃,b₁),b₂ = IncAddr b₃,(b₁ + b₂)

proof end;

definition

let c₁ be programmed FinPartState of SCM+FSA ;
let c₂ be Nat;
func IncAddr c₁,c₂ -> programmed FinPartState of SCM+FSA means :Def6: :: SCMFSA_4:def 6
( dom a₃ = dom a₁ & ( for b₁ being Nat st insloc b₁ in dom a₁ holds
a₃ . (insloc b₁) = IncAddr (pi a₁,(insloc b₁)),a₂ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def6 defines IncAddr SCMFSA_4:def 6 :

theorem Th24: :: SCMFSA_4:24

for b₁ being programmed FinPartState of SCM+FSA
for b₂ being Nat
for b₃ being Instruction-Location of SCM+FSA st b₃ in dom b₁ holds
(IncAddr b₁,b₂) . b₃ = IncAddr (pi b₁,b₃),b₂

proof end;

theorem Th25: :: SCMFSA_4:25

for b₁ being Nat
for b₂, b₃ being programmed FinPartState of SCM+FSA holds IncAddr (b₂ +* b₃),b₁ = (IncAddr b₂,b₁) +* (IncAddr b₃,b₁)

proof end;

theorem Th26: :: SCMFSA_4:26

for b₁ being Nat
for b₂ being Instruction of SCM+FSA
for b₃ being Function of the Instructions of SCM+FSA ,the Instructions of SCM+FSA st b₃ = (id the Instructions of SCM+FSA ) +* ((halt SCM+FSA ) .--> b₂) holds
for b₄ being programmed FinPartState of SCM+FSA holds IncAddr (b₃ * b₄),b₁ = ((id the Instructions of SCM+FSA ) +* ((halt SCM+FSA ) .--> (IncAddr b₂,b₁))) * (IncAddr b₄,b₁)

proof end;

theorem Th27: :: SCMFSA_4:27

for b₁, b₂ being Nat
for b₃ being programmed FinPartState of SCM+FSA holds IncAddr (IncAddr b₃,b₁),b₂ = IncAddr b₃,(b₁ + b₂)

proof end;

theorem Th28: :: SCMFSA_4:28

for b₁ being Nat
for b₂ being State of SCM+FSA holds Exec (IncAddr (CurInstr b₂),b₁),(b₂ +* (Start-At ((IC b₂) + b₁))) = (Following b₂) +* (Start-At ((IC (Following b₂)) + b₁))

proof end;

theorem Th29: :: SCMFSA_4:29

for b₁ being Instruction of SCM+FSA
for b₂ being State of SCM+FSA
for b₃ being FinPartState of SCM+FSA
for b₄, b₅, b₆ being Nat st IC b₂ = insloc (b₅ + b₆) holds
Exec b₁,(b₂ +* (Start-At ((IC b₂) -' b₆))) = (Exec (IncAddr b₁,b₆),b₂) +* (Start-At ((IC (Exec (IncAddr b₁,b₆),b₂)) -' b₆))

proof end;

definition

let c₁ be FinPartState of SCM+FSA ;
let c₂ be Nat;
func Shift c₁,c₂ -> programmed FinPartState of SCM+FSA means :Def7: :: SCMFSA_4:def 7
( dom a₃ = { (insloc (b₁ + a₂)) where B is Nat : insloc b₁ in dom a₁ } & ( for b₁ being Nat st insloc b₁ in dom a₁ holds
a₃ . (insloc (b₁ + a₂)) = a₁ . (insloc b₁) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def7 defines Shift SCMFSA_4:def 7 :

theorem Th30: :: SCMFSA_4:30

for b₁ being Instruction-Location of SCM+FSA
for b₂ being Nat
for b₃ being FinPartState of SCM+FSA st b₁ in dom b₃ holds
(Shift b₃,b₂) . (b₁ + b₂) = b₃ . b₁

proof end;

theorem Th31: :: SCMFSA_4:31

for b₁ being FinPartState of SCM+FSA
for b₂ being Nat holds dom (Shift b₁,b₂) = { (b₃ + b₂) where B is Instruction-Location of SCM+FSA : b₃ in dom b₁ }

proof end;

theorem Th32: :: SCMFSA_4:32

for b₁, b₂ being Nat
for b₃ being FinPartState of SCM+FSA holds Shift (Shift b₃,b₁),b₂ = Shift b₃,(b₁ + b₂)

proof end;

theorem Th33: :: SCMFSA_4:33

for b₁ being programmed FinPartState of SCM+FSA
for b₂ being Function of the Instructions of SCM+FSA ,the Instructions of SCM+FSA
for b₃ being Nat holds Shift (b₂ * b₁),b₃ = b₂ * (Shift b₁,b₃)

proof end;

theorem Th34: :: SCMFSA_4:34

for b₁ being Nat
for b₂, b₃ being FinPartState of SCM+FSA holds Shift (b₂ +* b₃),b₁ = (Shift b₂,b₁) +* (Shift b₃,b₁)

proof end;

theorem Th35: :: SCMFSA_4:35

for b₁, b₂ being Nat
for b₃ being programmed FinPartState of SCM+FSA holds Shift (IncAddr b₃,b₁),b₂ = IncAddr (Shift b₃,b₂),b₁

proof end;