:: SCMFSA6A semantic presentation

theorem Th1: :: SCMFSA6A:1

for b₁, b₂ being Function
for b₃, b₄ being set st b₂ c= b₁ & not b₃ in dom b₂ holds
b₂ c= b₁ +* b₃,b₄

proof end;

theorem Th2: :: SCMFSA6A:2

for b₁, b₂ being Function
for b₃ being set st b₁ | b₃ = b₂ | b₃ & b₁,b₂ equal_outside b₃ holds
b₁ = b₂

proof end;

theorem Th3: :: SCMFSA6A:3

for b₁ being Function
for b₂, b₃, b₄ being set st b₂ in b₄ holds
b₁,b₁ +* b₂,b₃ equal_outside b₄

proof end;

theorem Th4: :: SCMFSA6A:4

for b₁ being Function
for b₂, b₃, b₄ being set holds
( b₂ in b₄ or (b₁ +* b₂,b₃) | b₄ = b₁ | b₄ )

proof end;

theorem Th5: :: SCMFSA6A:5

for b₁, b₂ being Function
for b₃, b₄, b₅ being set st b₁ | b₅ = b₂ | b₅ holds
(b₁ +* b₃,b₄) | b₅ = (b₂ +* b₃,b₄) | b₅

proof end;

theorem Th6: :: SCMFSA6A:6

for b₁, b₂, b₃ being Function st b₁ c= b₃ & b₂ c= b₃ holds
b₁ +* b₂ c= b₃

proof end;

theorem Th7: :: SCMFSA6A:7

for b₁, b₂ being set
for b₃ being Function holds
( b₁ .--> b₂ c= b₃ iff ( b₁ in dom b₃ & b₃ . b₁ = b₂ ) )

proof end;

theorem Th8: :: SCMFSA6A:8

for b₁ being Function
for b₂ being set holds dom (b₁ | ((dom b₁) \ b₂)) = (dom b₁) \ b₂

proof end;

theorem Th9: :: SCMFSA6A:9

for b₁, b₂ being Function
for b₃ being set st b₃ c= dom b₁ & b₃ c= dom b₂ holds
( b₁ | b₃ = b₂ | b₃ iff for b₄ being set st b₄ in b₃ holds
b₁ . b₄ = b₂ . b₄ )

proof end;

theorem Th10: :: SCMFSA6A:10

for b₁ being Function
for b₂ being set holds b₁ | b₂ = b₁ | ((dom b₁) /\ b₂)

proof end;

theorem Th11: :: SCMFSA6A:11

for b₁, b₂, b₃ being Function
for b₄ being set st b₁,b₂ equal_outside b₄ holds
b₁ +* b₃,b₂ +* b₃ equal_outside b₄

proof end;

theorem Th12: :: SCMFSA6A:12

for b₁, b₂, b₃ being Function
for b₄ being set st b₁,b₂ equal_outside b₄ holds
b₃ +* b₁,b₃ +* b₂ equal_outside b₄

proof end;

theorem Th13: :: SCMFSA6A:13

for b₁, b₂, b₃ being Function holds
( b₁ +* b₃ = b₂ +* b₃ iff b₁,b₂ equal_outside dom b₃ )

proof end;

definition

mode Macro-Instruction is programmed initial FinPartState of SCM+FSA ;

end;

definition

let c₁ be programmed FinPartState of SCM+FSA ;
func Directed c₁ -> programmed FinPartState of SCM+FSA equals :: SCMFSA6A:def 1
((id the Instructions of SCM+FSA ) +* ((halt SCM+FSA ) .--> (goto (insloc (card a₁))))) * a₁;
coherence

proof end;

correctness ;

end;

:: deftheorem Def1 defines Directed SCMFSA6A:def 1 :

theorem Th14: :: SCMFSA6A:14

for b₁ being Macro-Instruction holds dom (Directed b₁) = dom b₁

proof end;

registration

let c₁ be Macro-Instruction;
cluster Directed a₁ -> programmed initial ;
coherence

proof end;

end;

definition

let c₁ be Instruction of SCM+FSA ;
func Macro c₁ -> Macro-Instruction equals :: SCMFSA6A:def 2
(insloc 0),(insloc 1) --> a₁,(halt SCM+FSA );
coherence

proof end;

correctness ;

end;

:: deftheorem Def2 defines Macro SCMFSA6A:def 2 :

registration

let c₁ be Instruction of SCM+FSA ;
cluster Macro a₁ -> non empty ;
coherence ;

end;

theorem Th15: :: SCMFSA6A:15

for b₁ being Macro-Instruction
for b₂ being Nat holds
( b₂ < card b₁ iff insloc b₂ in dom b₁ )

proof end;

registration

let c₁ be initial FinPartState of SCM+FSA ;
cluster ProgramPart a₁ -> initial ;
coherence

proof end;

end;

theorem Th16: :: SCMFSA6A:16

for b₁, b₂ being Macro-Instruction holds dom b₁ misses dom (ProgramPart (Relocated b₂,(card b₁)))

proof end;

theorem Th17: :: SCMFSA6A:17

for b₁ being Nat
for b₂ being programmed FinPartState of SCM+FSA holds card (ProgramPart (Relocated b₂,b₁)) = card b₂

proof end;

theorem Th18: :: SCMFSA6A:18

for b₁ being Macro-Instruction holds not halt SCM+FSA in rng (Directed b₁)

proof end;

theorem Th19: :: SCMFSA6A:19

for b₁ being Nat
for b₂ being Macro-Instruction holds ProgramPart (Relocated (Directed b₂),b₁) = ((id the Instructions of SCM+FSA ) +* ((halt SCM+FSA ) .--> (goto (insloc (b₁ + (card b₂)))))) * (ProgramPart (Relocated b₂,b₁))

proof end;

theorem Th20: :: SCMFSA6A:20

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

proof end;

theorem Th21: :: SCMFSA6A:21

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

proof end;

theorem Th22: :: SCMFSA6A:22

for b₁, b₂ being Nat
for b₃ being Macro-Instruction holds ProgramPart (Relocated (ProgramPart (Relocated b₃,b₁)),b₂) = ProgramPart (Relocated b₃,(b₁ + b₂))

proof end;

definition

let c₁ be FinPartState of SCM+FSA ;
func Initialized c₁ -> FinPartState of SCM+FSA equals :: SCMFSA6A:def 3
(a₁ +* ((intloc 0) .--> 1)) +* (Start-At (insloc 0));
coherence

proof end;

correctness ;

end;

:: deftheorem Def3 defines Initialized SCMFSA6A:def 3 :

theorem Th23: :: SCMFSA6A:23

for b₁ being Instruction of SCM+FSA
for b₂ being State of SCM+FSA holds
( InsCode b₁ in {0,6,7,8} or (Exec b₁,b₂) . (IC SCM+FSA ) = Next (IC b₂) )

proof end;

theorem Th24: :: SCMFSA6A:24

for b₁ being Macro-Instruction holds IC SCM+FSA in dom (Initialized b₁)

proof end;

theorem Th25: :: SCMFSA6A:25

for b₁ being Macro-Instruction holds IC (Initialized b₁) = insloc 0

proof end;

theorem Th26: :: SCMFSA6A:26

for b₁ being Macro-Instruction holds b₁ c= Initialized b₁

proof end;

theorem Th27: :: SCMFSA6A:27

for b₁ being set
for b₂ being AMI-Struct of b₁
for b₃ being State of b₂
for b₄ being programmed FinPartState of b₂ holds b₃,b₃ +* b₄ equal_outside the Instruction-Locations of b₂

proof end;

theorem Th28: :: SCMFSA6A:28

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₃ ) holds
b₁,b₂ equal_outside the Instruction-Locations of SCM+FSA

proof end;

theorem Th29: :: SCMFSA6A:29

for b₁ being with_non-empty_elements set
for b₂ being non empty non void IC-Ins-separated definite realistic AMI-Struct of b₁
for b₃, b₄ being State of b₂ st b₃,b₄ equal_outside the Instruction-Locations of b₂ holds
IC b₃ = IC b₄

proof end;

theorem Th30: :: SCMFSA6A:30

for b₁, b₂ being State of SCM+FSA st b₁,b₂ equal_outside the Instruction-Locations of SCM+FSA holds
for b₃ being Int-Location holds b₁ . b₃ = b₂ . b₃

proof end;

theorem Th31: :: SCMFSA6A:31

for b₁, b₂ being State of SCM+FSA st b₁,b₂ equal_outside the Instruction-Locations of SCM+FSA holds
for b₃ being FinSeq-Location holds b₁ . b₃ = b₂ . b₃

proof end;

theorem Th32: :: SCMFSA6A:32

for b₁ being Instruction of SCM+FSA
for b₂, b₃ being State of SCM+FSA st b₂,b₃ equal_outside the Instruction-Locations of SCM+FSA holds
Exec b₁,b₂, Exec b₁,b₃ equal_outside the Instruction-Locations of SCM+FSA

proof end;

theorem Th33: :: SCMFSA6A:33

for b₁ being Macro-Instruction holds (Initialized b₁) | the Instruction-Locations of SCM+FSA = b₁

proof end;

scheme :: SCMFSA6A:sch 1
s1{ F₁( set ) -> Element of the Instructions of SCM+FSA , F₂( set ) -> Integer, F₃( set ) -> FinSequence of INT , F₄() -> Instruction-Location of SCM+FSA } :

ex b₁ being State of SCM+FSA st
( IC b₁ = F₄() & ( for b₂ being Nat holds
( b₁ . (insloc b₂) = F₁(b₂) & b₁ . (intloc b₂) = F₂(b₂) & b₁ . (fsloc b₂) = F₃(b₂) ) ) )

proof end;

theorem Th34: :: SCMFSA6A:34

for b₁ being State of SCM+FSA holds dom b₁ = ((Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )}) \/ the Instruction-Locations of SCM+FSA by AMI_3:36, SCMFSA_2:8;

theorem Th35: :: SCMFSA6A:35

for b₁ being State of SCM+FSA
for b₂ being set holds
( not b₂ in dom b₁ or b₂ is Int-Location or b₂ is FinSeq-Location or b₂ = IC SCM+FSA or b₂ is Instruction-Location of SCM+FSA )

proof end;

theorem Th36: :: SCMFSA6A:36

for b₁, b₂ being State of SCM+FSA holds
( ( for b₃ being Instruction-Location of SCM+FSA holds b₁ . b₃ = b₂ . b₃ ) iff b₁ | the Instruction-Locations of SCM+FSA = b₂ | the Instruction-Locations of SCM+FSA )

proof end;

theorem Th37: :: SCMFSA6A:37

for b₁ being Instruction-Location of SCM+FSA holds
( not b₁ in Int-Locations \/ FinSeq-Locations & not IC SCM+FSA in Int-Locations \/ FinSeq-Locations )

proof end;

theorem Th38: :: SCMFSA6A:38

for b₁, b₂ being State of SCM+FSA holds
( ( ( for b₃ being Int-Location holds b₁ . b₃ = b₂ . b₃ ) & ( for b₃ being FinSeq-Location holds b₁ . b₃ = b₂ . b₃ ) ) iff b₁ | (Int-Locations \/ FinSeq-Locations ) = b₂ | (Int-Locations \/ FinSeq-Locations ) )

proof end;

theorem Th39: :: SCMFSA6A:39

for b₁, b₂ being State of SCM+FSA st b₁,b₂ equal_outside the Instruction-Locations of SCM+FSA holds
b₁ | (Int-Locations \/ FinSeq-Locations ) = b₂ | (Int-Locations \/ FinSeq-Locations )

proof end;

theorem Th40: :: SCMFSA6A:40

for b₁, b₂ being State of SCM+FSA
for b₃ being set holds (b₂ +* (b₁ | b₃)) | b₃ = b₁ | b₃

proof end;

theorem Th41: :: SCMFSA6A:41

for b₁, b₂ being State of SCM+FSA
for b₃ being Nat
for b₄ being Instruction of SCM+FSA st (IC b₁) + b₃ = IC b₂ & b₁ | (Int-Locations \/ FinSeq-Locations ) = b₂ | (Int-Locations \/ FinSeq-Locations ) holds
( (IC (Exec b₄,b₁)) + b₃ = IC (Exec (IncAddr b₄,b₃),b₂) & (Exec b₄,b₁) | (Int-Locations \/ FinSeq-Locations ) = (Exec (IncAddr b₄,b₃),b₂) | (Int-Locations \/ FinSeq-Locations ) )

proof end;

theorem Th42: :: SCMFSA6A:42

for b₁, b₂ being Macro-Instruction holds b₁,b₂ equal_outside the Instruction-Locations of SCM+FSA

proof end;

theorem Th43: :: SCMFSA6A:43

for b₁ being Macro-Instruction holds dom (Initialized b₁) = ((dom b₁) \/ {(intloc 0)}) \/ {(IC SCM+FSA )}

proof end;

theorem Th44: :: SCMFSA6A:44

for b₁ being Macro-Instruction
for b₂ being set holds
( not b₂ in dom (Initialized b₁) or b₂ in dom b₁ or b₂ = intloc 0 or b₂ = IC SCM+FSA )

proof end;

theorem Th45: :: SCMFSA6A:45

for b₁ being Macro-Instruction holds intloc 0 in dom (Initialized b₁)

proof end;

theorem Th46: :: SCMFSA6A:46

for b₁ being Macro-Instruction holds
( (Initialized b₁) . (intloc 0) = 1 & (Initialized b₁) . (IC SCM+FSA ) = insloc 0 )

proof end;

theorem Th47: :: SCMFSA6A:47

for b₁ being Macro-Instruction holds
( not intloc 0 in dom b₁ & not IC SCM+FSA in dom b₁ )

proof end;

theorem Th48: :: SCMFSA6A:48

for b₁ being Macro-Instruction
for b₂ being Int-Location st b₂ <> intloc 0 holds
not b₂ in dom (Initialized b₁)

proof end;

theorem Th49: :: SCMFSA6A:49

for b₁ being Macro-Instruction
for b₂ being FinSeq-Location holds not b₂ in dom (Initialized b₁)

proof end;

theorem Th50: :: SCMFSA6A:50

for b₁ being Macro-Instruction
for b₂ being set st b₂ in dom b₁ holds
b₁ . b₂ = (Initialized b₁) . b₂

proof end;

theorem Th51: :: SCMFSA6A:51

for b₁, b₂ being Macro-Instruction
for b₃ being State of SCM+FSA st Initialized b₂ c= b₃ holds
b₃ +* (Initialized b₁) = b₃ +* b₁

proof end;

theorem Th52: :: SCMFSA6A:52

for b₁, b₂ being Macro-Instruction
for b₃ being State of SCM+FSA st Initialized b₂ c= b₃ holds
Initialized b₁ c= b₃ +* b₁

proof end;

theorem Th53: :: SCMFSA6A:53

for b₁, b₂ being Macro-Instruction
for b₃ being State of SCM+FSA holds b₃ +* (Initialized b₁),b₃ +* (Initialized b₂) equal_outside the Instruction-Locations of SCM+FSA

proof end;

definition

let c₁, c₂ be Macro-Instruction;
func c₁ ';' c₂ -> Macro-Instruction equals :: SCMFSA6A:def 4
(Directed a₁) +* (ProgramPart (Relocated a₂,(card a₁)));
coherence

proof end;

correctness ;

end;

:: deftheorem Def4 defines ';' SCMFSA6A:def 4 :

theorem Th54: :: SCMFSA6A:54

for b₁, b₂ being Macro-Instruction
for b₃ being Instruction-Location of SCM+FSA st b₃ in dom b₁ & b₁ . b₃ <> halt SCM+FSA holds
(b₁ ';' b₂) . b₃ = b₁ . b₃

proof end;

theorem Th55: :: SCMFSA6A:55

for b₁, b₂ being Macro-Instruction holds Directed b₁ c= b₁ ';' b₂

proof end;

theorem Th56: :: SCMFSA6A:56

for b₁, b₂ being Macro-Instruction holds dom b₁ c= dom (b₁ ';' b₂)

proof end;

theorem Th57: :: SCMFSA6A:57

for b₁, b₂ being Macro-Instruction holds b₁ +* (b₁ ';' b₂) = b₁ ';' b₂

proof end;

theorem Th58: :: SCMFSA6A:58

for b₁, b₂ being Macro-Instruction holds (Initialized b₁) +* (b₁ ';' b₂) = Initialized (b₁ ';' b₂)

proof end;

definition

let c₁ be Instruction of SCM+FSA ;
let c₂ be Macro-Instruction;
func c₁ ';' c₂ -> Macro-Instruction equals :: SCMFSA6A:def 5
(Macro a₁) ';' a₂;
correctness ;

end;

:: deftheorem Def5 defines ';' SCMFSA6A:def 5 :

definition

let c₁ be Macro-Instruction;
let c₂ be Instruction of SCM+FSA ;
func c₁ ';' c₂ -> Macro-Instruction equals :: SCMFSA6A:def 6
a₁ ';' (Macro a₂);
correctness ;

end;

:: deftheorem Def6 defines ';' SCMFSA6A:def 6 :

definition

let c₁, c₂ be Instruction of SCM+FSA ;
func c₁ ';' c₂ -> Macro-Instruction equals :: SCMFSA6A:def 7
(Macro a₁) ';' (Macro a₂);
correctness ;

end;

:: deftheorem Def7 defines ';' SCMFSA6A:def 7 :

theorem Th59: :: SCMFSA6A:59

for b₁, b₂ being Instruction of SCM+FSA holds b₁ ';' b₂ = (Macro b₁) ';' b₂ ;

theorem Th60: :: SCMFSA6A:60

for b₁, b₂ being Instruction of SCM+FSA holds b₁ ';' b₂ = b₁ ';' (Macro b₂) ;

theorem Th61: :: SCMFSA6A:61

for b₁, b₂ being Macro-Instruction holds card (b₁ ';' b₂) = (card b₁) + (card b₂)

proof end;

theorem Th62: :: SCMFSA6A:62

for b₁, b₂, b₃ being Macro-Instruction holds (b₁ ';' b₂) ';' b₃ = b₁ ';' (b₂ ';' b₃)

proof end;

theorem Th63: :: SCMFSA6A:63

for b₁ being Instruction of SCM+FSA
for b₂, b₃ being Macro-Instruction holds (b₂ ';' b₃) ';' b₁ = b₂ ';' (b₃ ';' b₁) by Th62;

theorem Th64: :: SCMFSA6A:64

for b₁ being Instruction of SCM+FSA
for b₂, b₃ being Macro-Instruction holds (b₂ ';' b₁) ';' b₃ = b₂ ';' (b₁ ';' b₃) by Th62;

theorem Th65: :: SCMFSA6A:65

for b₁, b₂ being Instruction of SCM+FSA
for b₃ being Macro-Instruction holds (b₃ ';' b₁) ';' b₂ = b₃ ';' (b₁ ';' b₂)

proof end;

theorem Th66: :: SCMFSA6A:66

for b₁ being Instruction of SCM+FSA
for b₂, b₃ being Macro-Instruction holds (b₁ ';' b₂) ';' b₃ = b₁ ';' (b₂ ';' b₃) by Th62;

theorem Th67: :: SCMFSA6A:67

for b₁, b₂ being Instruction of SCM+FSA
for b₃ being Macro-Instruction holds (b₁ ';' b₃) ';' b₂ = b₁ ';' (b₃ ';' b₂) by Th63;

theorem Th68: :: SCMFSA6A:68

for b₁, b₂ being Instruction of SCM+FSA
for b₃ being Macro-Instruction holds (b₁ ';' b₂) ';' b₃ = b₁ ';' (b₂ ';' b₃)

proof end;

theorem Th69: :: SCMFSA6A:69

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

proof end;