:: SCMPDS_4 semantic presentation

definition

mode Program-block is programmed initial FinPartState of SCMPDS ;

end;

definition

let c₁ be Instruction of SCMPDS ;
func Load c₁ -> Program-block equals :: SCMPDS_4:def 1
(inspos 0) .--> a₁;
coherence

proof end;

correctness ;

end;

:: deftheorem Def1 defines Load SCMPDS_4:def 1 :

registration

let c₁ be Instruction of SCMPDS ;
cluster Load a₁ -> non empty ;
coherence ;

end;

theorem Th1: :: SCMPDS_4:1

for b₁ being Program-block
for b₂ being Nat holds
( b₂ < card b₁ iff inspos b₂ in dom b₁ )

proof end;

registration

let c₁ be initial FinPartState of SCMPDS ;
cluster ProgramPart a₁ -> initial ;
coherence

proof end;

end;

theorem Th2: :: SCMPDS_4:2

for b₁, b₂ being Program-block holds dom b₁ misses dom (Shift b₂,(card b₁))

proof end;

theorem Th3: :: SCMPDS_4:3

for b₁ being Nat
for b₂ being programmed FinPartState of SCMPDS holds card (Shift b₂,b₁) = card b₂

proof end;

theorem Th4: :: SCMPDS_4:4

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

proof end;

theorem Th5: :: SCMPDS_4:5

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

proof end;

definition

let c₁ be Program-block;
func Initialized c₁ -> FinPartState of SCMPDS equals :: SCMPDS_4:def 2
a₁ +* (Start-At (inspos 0));
coherence ;
correctness ;

end;

:: deftheorem Def2 defines Initialized SCMPDS_4:def 2 :

theorem Th6: :: SCMPDS_4:6

for b₁ being Instruction of SCMPDS
for b₂ being State of SCMPDS holds
( InsCode b₁ in {0,1,4,5,6} or (Exec b₁,b₂) . (IC SCMPDS ) = Next (IC b₂) )

proof end;

theorem Th7: :: SCMPDS_4:7

for b₁ being Program-block holds IC SCMPDS in dom (Initialized b₁)

proof end;

theorem Th8: :: SCMPDS_4:8

for b₁ being Program-block holds IC (Initialized b₁) = inspos 0

proof end;

theorem Th9: :: SCMPDS_4:9

for b₁ being Program-block holds b₁ c= Initialized b₁

proof end;

theorem Th10: :: SCMPDS_4:10

canceled;

theorem Th11: :: SCMPDS_4:11

for b₁, b₂ being State of SCMPDS st IC b₁ = IC b₂ & ( for b₃ being Int_position holds b₁ . b₃ = b₂ . b₃ ) holds
b₁,b₂ equal_outside the Instruction-Locations of SCMPDS

proof end;

theorem Th12: :: SCMPDS_4:12

canceled;

theorem Th13: :: SCMPDS_4:13

for b₁, b₂ being State of SCMPDS st b₁,b₂ equal_outside the Instruction-Locations of SCMPDS holds
for b₃ being Int_position holds b₁ . b₃ = b₂ . b₃

proof end;

theorem Th14: :: SCMPDS_4:14

for b₁ being Int_position
for b₂, b₃ being State of SCMPDS
for b₄ being Integer st b₂,b₃ equal_outside the Instruction-Locations of SCMPDS holds
b₂ . (DataLoc (b₂ . b₁),b₄) = b₃ . (DataLoc (b₃ . b₁),b₄)

proof end;

theorem Th15: :: SCMPDS_4:15

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

proof end;

theorem Th16: :: SCMPDS_4:16

for b₁ being Program-block holds (Initialized b₁) | the Instruction-Locations of SCMPDS = b₁

proof end;

theorem Th17: :: SCMPDS_4:17

for b₁, b₂ being Nat st b₁ <> b₂ holds
DataLoc b₁,0 <> DataLoc b₂,0

proof end;

theorem Th18: :: SCMPDS_4:18

for b₁ being Int_position ex b₂ being Nat st b₁ = DataLoc b₂,0

proof end;

scheme :: SCMPDS_4:sch 1
s1{ F₁( set ) -> Instruction of SCMPDS , F₂( set ) -> Integer, F₃() -> Instruction-Location of SCMPDS } :

ex b₁ being State of SCMPDS st
( IC b₁ = F₃() & ( for b₂ being Nat holds
( b₁ . (inspos b₂) = F₁(b₂) & b₁ . (DataLoc b₂,0) = F₂(b₂) ) ) )

proof end;

theorem Th19: :: SCMPDS_4:19

for b₁ being State of SCMPDS holds dom b₁ = ({(IC SCMPDS )} \/ SCM-Data-Loc ) \/ the Instruction-Locations of SCMPDS by AMI_3:36, SCMPDS_3:5;

theorem Th20: :: SCMPDS_4:20

for b₁ being State of SCMPDS
for b₂ being set holds
( not b₂ in dom b₁ or b₂ is Int_position or b₂ = IC SCMPDS or b₂ is Instruction-Location of SCMPDS )

proof end;

theorem Th21: :: SCMPDS_4:21

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

proof end;

theorem Th22: :: SCMPDS_4:22

for b₁ being Instruction-Location of SCMPDS holds not b₁ in SCM-Data-Loc by SCMPDS_2:10, XBOOLE_0:3;

theorem Th23: :: SCMPDS_4:23

for b₁, b₂ being State of SCMPDS holds
( ( for b₃ being Int_position holds b₁ . b₃ = b₂ . b₃ ) iff b₁ | SCM-Data-Loc = b₂ | SCM-Data-Loc )

proof end;

theorem Th24: :: SCMPDS_4:24

for b₁, b₂ being State of SCMPDS st b₁,b₂ equal_outside the Instruction-Locations of SCMPDS holds
b₁ | SCM-Data-Loc = b₂ | SCM-Data-Loc

proof end;

theorem Th25: :: SCMPDS_4:25

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

proof end;

theorem Th26: :: SCMPDS_4:26

for b₁, b₂ being Program-block holds b₁,b₂ equal_outside the Instruction-Locations of SCMPDS

proof end;

theorem Th27: :: SCMPDS_4:27

for b₁ being Program-block holds dom (Initialized b₁) = (dom b₁) \/ {(IC SCMPDS )}

proof end;

theorem Th28: :: SCMPDS_4:28

for b₁ being Program-block
for b₂ being set holds
( not b₂ in dom (Initialized b₁) or b₂ in dom b₁ or b₂ = IC SCMPDS )

proof end;

theorem Th29: :: SCMPDS_4:29

for b₁ being Program-block holds (Initialized b₁) . (IC SCMPDS ) = inspos 0

proof end;

theorem Th30: :: SCMPDS_4:30

for b₁ being Program-block holds not IC SCMPDS in dom b₁

proof end;

theorem Th31: :: SCMPDS_4:31

for b₁ being Program-block
for b₂ being Int_position holds not b₂ in dom (Initialized b₁)

proof end;

theorem Th32: :: SCMPDS_4:32

for b₁ being Nat
for b₂ being Program-block
for b₃ being set st b₃ in dom b₂ holds
b₂ . b₃ = (b₂ +* (Start-At (inspos b₁))) . b₃

proof end;

theorem Th33: :: SCMPDS_4:33

for b₁ being Program-block
for b₂ being set st b₂ in dom b₁ holds
b₁ . b₂ = (Initialized b₁) . b₂ by Th32;

theorem Th34: :: SCMPDS_4:34

for b₁, b₂ being Program-block
for b₃ being State of SCMPDS st Initialized b₂ c= b₃ holds
b₃ +* (Initialized b₁) = b₃ +* b₁

proof end;

theorem Th35: :: SCMPDS_4:35

for b₁, b₂ being Program-block
for b₃ being State of SCMPDS st Initialized b₂ c= b₃ holds
Initialized b₁ c= b₃ +* b₁

proof end;

theorem Th36: :: SCMPDS_4:36

for b₁, b₂ being Program-block
for b₃ being State of SCMPDS holds b₃ +* (Initialized b₁),b₃ +* (Initialized b₂) equal_outside the Instruction-Locations of SCMPDS

proof end;

definition

let c₁, c₂ be Program-block;
func c₁ ';' c₂ -> Program-block equals :: SCMPDS_4:def 3
a₁ +* (Shift a₂,(card a₁));
coherence

proof end;

correctness ;

end;

:: deftheorem Def3 defines ';' SCMPDS_4:def 3 :

theorem Th37: :: SCMPDS_4:37

for b₁, b₂ being Program-block
for b₃ being Instruction-Location of SCMPDS st b₃ in dom b₁ holds
(b₁ ';' b₂) . b₃ = b₁ . b₃

proof end;

theorem Th38: :: SCMPDS_4:38

for b₁, b₂ being Program-block
for b₃ being Instruction-Location of SCMPDS st b₃ in dom b₂ holds
(b₁ ';' b₂) . (b₃ + (card b₁)) = b₂ . b₃

proof end;

theorem Th39: :: SCMPDS_4:39

for b₁, b₂ being Program-block holds dom b₁ c= dom (b₁ ';' b₂)

proof end;

theorem Th40: :: SCMPDS_4:40

for b₁, b₂ being Program-block holds b₁ c= b₁ ';' b₂

proof end;

theorem Th41: :: SCMPDS_4:41

for b₁, b₂ being Program-block holds b₁ +* (b₁ ';' b₂) = b₁ ';' b₂

proof end;

theorem Th42: :: SCMPDS_4:42

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

proof end;

definition

let c₁ be Instruction of SCMPDS ;
let c₂ be Program-block;
func c₁ ';' c₂ -> Program-block equals :: SCMPDS_4:def 4
(Load a₁) ';' a₂;
correctness ;

end;

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

definition

let c₁ be Program-block;
let c₂ be Instruction of SCMPDS ;
func c₁ ';' c₂ -> Program-block equals :: SCMPDS_4:def 5
a₁ ';' (Load a₂);
correctness ;

end;

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

definition

let c₁, c₂ be Instruction of SCMPDS ;
func c₁ ';' c₂ -> Program-block equals :: SCMPDS_4:def 6
(Load a₁) ';' (Load a₂);
correctness ;

end;

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

theorem Th43: :: SCMPDS_4:43

for b₁, b₂ being Instruction of SCMPDS holds b₁ ';' b₂ = (Load b₁) ';' b₂ ;

theorem Th44: :: SCMPDS_4:44

for b₁, b₂ being Instruction of SCMPDS holds b₁ ';' b₂ = b₁ ';' (Load b₂) ;

theorem Th45: :: SCMPDS_4:45

for b₁, b₂ being Program-block holds card (b₁ ';' b₂) = (card b₁) + (card b₂)

proof end;

theorem Th46: :: SCMPDS_4:46

for b₁, b₂, b₃ being Program-block holds (b₁ ';' b₂) ';' b₃ = b₁ ';' (b₂ ';' b₃)

proof end;

theorem Th47: :: SCMPDS_4:47

for b₁ being Instruction of SCMPDS
for b₂, b₃ being Program-block holds (b₂ ';' b₃) ';' b₁ = b₂ ';' (b₃ ';' b₁) by Th46;

theorem Th48: :: SCMPDS_4:48

for b₁ being Instruction of SCMPDS
for b₂, b₃ being Program-block holds (b₂ ';' b₁) ';' b₃ = b₂ ';' (b₁ ';' b₃) by Th46;

theorem Th49: :: SCMPDS_4:49

for b₁, b₂ being Instruction of SCMPDS
for b₃ being Program-block holds (b₃ ';' b₁) ';' b₂ = b₃ ';' (b₁ ';' b₂)

proof end;

theorem Th50: :: SCMPDS_4:50

for b₁ being Instruction of SCMPDS
for b₂, b₃ being Program-block holds (b₁ ';' b₂) ';' b₃ = b₁ ';' (b₂ ';' b₃) by Th46;

theorem Th51: :: SCMPDS_4:51

for b₁, b₂ being Instruction of SCMPDS
for b₃ being Program-block holds (b₁ ';' b₃) ';' b₂ = b₁ ';' (b₃ ';' b₂) by Th47;

theorem Th52: :: SCMPDS_4:52

for b₁, b₂ being Instruction of SCMPDS
for b₃ being Program-block holds (b₁ ';' b₂) ';' b₃ = b₁ ';' (b₂ ';' b₃)

proof end;

theorem Th53: :: SCMPDS_4:53

for b₁, b₂, b₃ being Instruction of SCMPDS holds (b₁ ';' b₂) ';' b₃ = b₁ ';' (b₂ ';' b₃)

proof end;

theorem Th54: :: SCMPDS_4:54

for b₁ being Nat
for b₂ being Program-block holds dom b₂ misses dom (Start-At (inspos b₁))

proof end;

theorem Th55: :: SCMPDS_4:55

for b₁ being Program-block holds Start-At (inspos 0) c= Initialized b₁ by FUNCT_4:26;

theorem Th56: :: SCMPDS_4:56

for b₁ being Nat
for b₂ being Program-block
for b₃ being State of SCMPDS st b₂ +* (Start-At (inspos b₁)) c= b₃ holds
b₂ c= b₃

proof end;

theorem Th57: :: SCMPDS_4:57

for b₁ being Program-block
for b₂ being State of SCMPDS st Initialized b₁ c= b₂ holds
b₁ c= b₂ by Th56;

theorem Th58: :: SCMPDS_4:58

for b₁ being Nat
for b₂ being Program-block holds (b₂ +* (Start-At (inspos b₁))) | the Instruction-Locations of SCMPDS = b₂

proof end;

theorem Th59: :: SCMPDS_4:59

for b₁ being Int_position
for b₂ being Instruction-Location of SCMPDS holds not b₁ in dom (Start-At b₂)

proof end;

theorem Th60: :: SCMPDS_4:60

for b₁, b₂ being Instruction-Location of SCMPDS holds not b₁ in dom (Start-At b₂)

proof end;

theorem Th61: :: SCMPDS_4:61

for b₁ being Program-block
for b₂ being Int_position
for b₃ being Instruction-Location of SCMPDS holds not b₂ in dom (b₁ +* (Start-At b₃))

proof end;

theorem Th62: :: SCMPDS_4:62

for b₁ being Program-block
for b₂ being State of SCMPDS holds (b₂ +* b₁) +* (Start-At (inspos 0)) = (b₂ +* (Start-At (inspos 0))) +* b₁

proof end;

definition

let c₁ be State of SCMPDS ;
let c₂ be Int_position ;
let c₃ be Integer;
redefine func +* as c₁ +* c₂,c₃ -> State of SCMPDS ;
coherence

proof end;

end;

definition

let c₁ be Program-block;
func stop c₁ -> Program-block equals :: SCMPDS_4:def 7
a₁ ';' SCMPDS-Stop ;
coherence ;

end;

:: deftheorem Def7 defines stop SCMPDS_4:def 7 :

definition

let c₁ be Program-block;
let c₂ be State of SCMPDS ;
func IExec c₁,c₂ -> State of SCMPDS equals :: SCMPDS_4:def 8
(Result (a₂ +* (Initialized (stop a₁)))) +* (a₂ | the Instruction-Locations of SCMPDS );
coherence by AMI_5:82;

end;

:: deftheorem Def8 defines IExec SCMPDS_4:def 8 :

definition

let c₁ be Program-block;
attr a₁ is paraclosed means :Def9: :: SCMPDS_4:def 9
for b₁ being State of SCMPDS
for b₂ being Nat st Initialized (stop a₁) c= b₁ holds
IC ((Computation b₁) . b₂) in dom (stop a₁);
attr a₁ is parahalting means :Def10: :: SCMPDS_4:def 10
Initialized (stop a₁) is halting;

end;

:: deftheorem Def9 defines paraclosed SCMPDS_4:def 9 :

:: deftheorem Def10 defines parahalting SCMPDS_4:def 10 :

Lemma37: Load (halt SCMPDS ) is parahalting

proof end;

registration

cluster parahalting FinPartState of SCMPDS ;
existence by Lemma37;

end;

theorem Th63: :: SCMPDS_4:63

for b₁ being State of SCMPDS
for b₂ being parahalting Program-block st Initialized (stop b₂) c= b₁ holds
b₁ is halting

proof end;

registration

let c₁ be parahalting Program-block;
cluster Initialized (stop a₁) -> halting ;
coherence

proof end;

end;

definition

let c₁, c₂ be Instruction-Location of SCMPDS ;
let c₃, c₄ be Instruction of SCMPDS ;
redefine func --> as c₁,c₂ --> c₃,c₄ -> FinPartState of SCMPDS ;
coherence

proof end;

end;

theorem Th64: :: SCMPDS_4:64

canceled;

theorem Th65: :: SCMPDS_4:65

for b₁ being State of SCMPDS holds IC b₁ <> Next (IC b₁)

proof end;

theorem Th66: :: SCMPDS_4:66

for b₁ being State of SCMPDS holds not b₁ +* ((IC b₁),(Next (IC b₁)) --> (goto 1),(goto (- 1))) is halting

proof end;

theorem Th67: :: SCMPDS_4:67

for b₁ being Nat
for b₂ being Program-block
for b₃, b₄ being State of SCMPDS st b₃,b₄ equal_outside the Instruction-Locations of SCMPDS & b₂ c= b₃ & b₂ c= b₄ & ( for b₅ being Nat st b₅ < b₁ holds
IC ((Computation b₄) . b₅) in dom b₂ ) holds
for b₅ being Nat st b₅ <= b₁ holds
(Computation b₃) . b₅,(Computation b₄) . b₅ equal_outside the Instruction-Locations of SCMPDS

proof end;

theorem Th68: :: SCMPDS_4:68

for b₁ being State of SCMPDS
for b₂ being Instruction-Location of SCMPDS holds b₂ in dom b₁

proof end;

theorem Th69: :: SCMPDS_4:69

for b₁ being State of SCMPDS
for b₂, b₃ being Instruction-Location of SCMPDS
for b₄, b₅ being Instruction of SCMPDS holds b₁ +* (b₂,b₃ --> b₄,b₅) = (b₁ +* b₂,b₄) +* b₃,b₅

proof end;

theorem Th70: :: SCMPDS_4:70

for b₁ being Nat holds Next (inspos b₁) = inspos (b₁ + 1)

proof end;

theorem Th71: :: SCMPDS_4:71

for b₁ being Program-block
for b₂ being State of SCMPDS st not IC b₂ in dom b₁ holds
not Next (IC b₂) in dom b₁

proof end;

registration

cluster parahalting -> paraclosed FinPartState of SCMPDS ;
coherence

proof end;

end;

theorem Th72: :: SCMPDS_4:72

dom SCMPDS-Stop = {(inspos 0)} by CQC_LANG:5;

theorem Th73: :: SCMPDS_4:73

( inspos 0 in dom SCMPDS-Stop & SCMPDS-Stop . (inspos 0) = halt SCMPDS ) by Th72, CQC_LANG:6, TARSKI:def 1;

theorem Th74: :: SCMPDS_4:74

card SCMPDS-Stop = 1

proof end;

theorem Th75: :: SCMPDS_4:75

for b₁ being Program-block holds inspos 0 in dom (stop b₁)

proof end;

theorem Th76: :: SCMPDS_4:76

for b₁ being programmed FinPartState of SCMPDS
for b₂ being Nat
for b₃ being Instruction-Location of SCMPDS st b₃ in dom b₁ holds
b₃ + b₂ in dom (Shift b₁,b₂)

proof end;

definition

let c₁ be Instruction of SCMPDS ;
let c₂ be Nat;
pred c₁ valid_at c₂ means :Def11: :: SCMPDS_4:def 11
( ( InsCode a₁ = 0 implies ex b₁ being Integer st
( a₁ = goto b₁ & a₂ + b₁ >= 0 ) ) & ( InsCode a₁ = 4 implies ex b₁ being Int_position ex b₂, b₃ being Integer st
( a₁ = b₁,b₂ <>0_goto b₃ & a₂ + b₃ >= 0 ) ) & ( InsCode a₁ = 5 implies ex b₁ being Int_position ex b₂, b₃ being Integer st
( a₁ = b₁,b₂ <=0_goto b₃ & a₂ + b₃ >= 0 ) ) & ( InsCode a₁ = 6 implies ex b₁ being Int_position ex b₂, b₃ being Integer st
( a₁ = b₁,b₂ >=0_goto b₃ & a₂ + b₃ >= 0 ) ) );

end;

:: deftheorem Def11 defines valid_at SCMPDS_4:def 11 :

theorem Th77: :: SCMPDS_4:77

for b₁ being Instruction of SCMPDS
for b₂, b₃ being Nat st b₁ valid_at b₂ & b₂ <= b₃ holds
b₁ valid_at b₃

proof end;

definition

let c₁ be FinPartState of SCMPDS ;
attr a₁ is shiftable means :Def12: :: SCMPDS_4:def 12
for b₁ being Nat
for b₂ being Instruction of SCMPDS st inspos b₁ in dom a₁ & b₂ = a₁ . (inspos b₁) holds
( InsCode b₂ <> 1 & InsCode b₂ <> 3 & b₂ valid_at b₁ );

end;

:: deftheorem Def12 defines shiftable SCMPDS_4:def 12 :

Lemma53: Load (halt SCMPDS ) is shiftable

proof end;

registration

cluster paraclosed parahalting shiftable FinPartState of SCMPDS ;
existence by Lemma37, Lemma53;

end;

definition

let c₁ be Instruction of SCMPDS ;
attr a₁ is shiftable means :Def13: :: SCMPDS_4:def 13
( InsCode a₁ = 2 or InsCode a₁ > 6 );

end;

:: deftheorem Def13 defines shiftable SCMPDS_4:def 13 :

registration

cluster shiftable Element of the Instructions of SCMPDS ;
existence

proof end;

end;

registration

let c₁ be Int_position ;
let c₂ be Integer;
cluster a₁ := a₂ -> shiftable ;
coherence

proof end;

end;

registration

let c₁ be Int_position ;
let c₂, c₃ be Integer;
cluster a₁,a₂ := a₃ -> shiftable ;
coherence

proof end;

end;

registration

let c₁ be Int_position ;
let c₂, c₃ be Integer;
cluster AddTo a₁,a₂,a₃ -> shiftable ;
coherence

proof end;

end;

registration

let c₁, c₂ be Int_position ;
let c₃, c₄ be Integer;
cluster AddTo a₁,a₃,a₂,a₄ -> shiftable ;
coherence

proof end;

cluster SubFrom a₁,a₃,a₂,a₄ -> shiftable ;
coherence

proof end;

cluster MultBy a₁,a₃,a₂,a₄ -> shiftable ;
coherence

proof end;

cluster Divide a₁,a₃,a₂,a₄ -> shiftable ;
coherence

proof end;

cluster a₁,a₃ := a₂,a₄ -> shiftable ;
coherence

proof end;

end;

registration

let c₁, c₂ be shiftable Program-block;
cluster a₁ ';' a₂ -> shiftable ;
coherence

proof end;

end;

registration

let c₁ be shiftable Instruction of SCMPDS ;
cluster Load a₁ -> non empty shiftable ;
coherence

proof end;

end;

registration

let c₁ be shiftable Instruction of SCMPDS ;
let c₂ be shiftable Program-block;
cluster a₁ ';' a₂ -> shiftable ;
coherence ;

end;

registration

let c₁ be shiftable Program-block;
let c₂ be shiftable Instruction of SCMPDS ;
cluster a₁ ';' a₂ -> shiftable ;
coherence ;

end;

registration

let c₁, c₂ be shiftable Instruction of SCMPDS ;
cluster a₁ ';' a₂ -> shiftable ;
coherence ;

end;

registration

cluster SCMPDS-Stop -> paraclosed parahalting shiftable ;
coherence by Lemma37, Lemma53;

end;

registration

let c₁ be shiftable Program-block;
cluster stop a₁ -> shiftable ;
coherence ;

end;

theorem Th78: :: SCMPDS_4:78

for b₁ being shiftable Program-block
for b₂ being Integer st (card b₁) + b₂ >= 0 holds
b₁ ';' (goto b₂) is shiftable

proof end;

registration

let c₁ be Nat;
cluster Load (goto a₁) -> non empty shiftable ;
coherence

proof end;

end;

theorem Th79: :: SCMPDS_4:79

for b₁ being shiftable Program-block
for b₂, b₃ being Integer
for b₄ being Int_position st (card b₁) + b₃ >= 0 holds
b₁ ';' (b₄,b₂ <>0_goto b₃) is shiftable

proof end;

registration

let c₁ be Integer;
let c₂ be Int_position ;
let c₃ be Nat;
cluster Load (a₂,a₁ <>0_goto a₃) -> non empty shiftable ;
coherence

proof end;

end;

theorem Th80: :: SCMPDS_4:80

for b₁ being shiftable Program-block
for b₂, b₃ being Integer
for b₄ being Int_position st (card b₁) + b₃ >= 0 holds
b₁ ';' (b₄,b₂ <=0_goto b₃) is shiftable

proof end;

registration

let c₁ be Integer;
let c₂ be Int_position ;
let c₃ be Nat;
cluster Load (a₂,a₁ <=0_goto a₃) -> non empty shiftable ;
coherence

proof end;

end;

theorem Th81: :: SCMPDS_4:81

for b₁ being shiftable Program-block
for b₂, b₃ being Integer
for b₄ being Int_position st (card b₁) + b₃ >= 0 holds
b₁ ';' (b₄,b₂ >=0_goto b₃) is shiftable

proof end;

registration

let c₁ be Integer;
let c₂ be Int_position ;
let c₃ be Nat;
cluster Load (a₂,a₁ >=0_goto a₃) -> non empty shiftable ;
coherence

proof end;

end;

theorem Th82: :: SCMPDS_4:82

for b₁, b₂ being State of SCMPDS
for b₃, b₄ being Nat
for b₅ being Integer st IC b₁ = inspos b₄ & b₄ + b₅ >= 0 & (IC b₁) + b₃ = IC b₂ holds
(ICplusConst b₁,b₅) + b₃ = ICplusConst b₂,b₅

proof end;

theorem Th83: :: SCMPDS_4:83

for b₁, b₂ being State of SCMPDS
for b₃, b₄ being Nat
for b₅ being Instruction of SCMPDS st IC b₁ = inspos b₄ & b₅ valid_at b₄ & InsCode b₅ <> 1 & InsCode b₅ <> 3 & (IC b₁) + b₃ = IC b₂ & b₁ | SCM-Data-Loc = b₂ | SCM-Data-Loc holds
( (IC (Exec b₅,b₁)) + b₃ = IC (Exec b₅,b₂) & (Exec b₅,b₁) | SCM-Data-Loc = (Exec b₅,b₂) | SCM-Data-Loc )

proof end;

theorem Th84: :: SCMPDS_4:84

for b₁, b₂ being State of SCMPDS
for b₃ being parahalting shiftable Program-block st Initialized (stop b₃) c= b₁ holds
for b₄ being Nat st Shift (stop b₃),b₄ c= b₂ & IC b₂ = inspos b₄ & b₁ | SCM-Data-Loc = b₂ | SCM-Data-Loc holds
for b₅ being Nat holds
( (IC ((Computation b₁) . b₅)) + b₄ = IC ((Computation b₂) . b₅) & CurInstr ((Computation b₁) . b₅) = CurInstr ((Computation b₂) . b₅) & ((Computation b₁) . b₅) | SCM-Data-Loc = ((Computation b₂) . b₅) | SCM-Data-Loc )

proof end;