:: SCMPDS_5 semantic presentation

theorem Th1: :: SCMPDS_5:1

for b₁ being with_non-empty_elements set
for b₂ being non empty non void halting IC-Ins-separated definite AMI-Struct of b₁
for b₃ being State of b₂ st b₃ = Following b₃ holds
for b₄ being Nat holds (Computation b₃) . b₄ = b₃

proof end;

theorem Th2: :: SCMPDS_5:2

for b₁ being set
for b₂ being Instruction of SCMPDS holds
( b₁ in dom (Load b₂) iff b₁ = inspos 0 )

proof end;

theorem Th3: :: SCMPDS_5:3

for b₁ being Instruction-Location of SCMPDS
for b₂ being Program-block st b₁ in dom (stop b₂) & (stop b₂) . b₁ <> halt SCMPDS holds
b₁ in dom b₂

proof end;

theorem Th4: :: SCMPDS_5:4

for b₁ being Instruction of SCMPDS holds
( dom (Load b₁) = {(inspos 0)} & (Load b₁) . (inspos 0) = b₁ ) by CQC_LANG:5, CQC_LANG:6;

theorem Th5: :: SCMPDS_5:5

for b₁ being Instruction of SCMPDS holds inspos 0 in dom (Load b₁)

proof end;

theorem Th6: :: SCMPDS_5:6

for b₁ being Instruction of SCMPDS holds card (Load b₁) = 1

proof end;

theorem Th7: :: SCMPDS_5:7

for b₁ being Program-block holds card (stop b₁) = (card b₁) + 1 by SCMPDS_4:45, SCMPDS_4:74;

theorem Th8: :: SCMPDS_5:8

for b₁ being Instruction of SCMPDS holds card (stop (Load b₁)) = 2

proof end;

theorem Th9: :: SCMPDS_5:9

for b₁ being Instruction of SCMPDS holds
( inspos 0 in dom (stop (Load b₁)) & inspos 1 in dom (stop (Load b₁)) )

proof end;

theorem Th10: :: SCMPDS_5:10

for b₁ being Instruction of SCMPDS holds
( (stop (Load b₁)) . (inspos 0) = b₁ & (stop (Load b₁)) . (inspos 1) = halt SCMPDS )

proof end;

theorem Th11: :: SCMPDS_5:11

for b₁ being set
for b₂ being Instruction of SCMPDS holds
( b₁ in dom (stop (Load b₂)) iff ( b₁ = inspos 0 or b₁ = inspos 1 ) )

proof end;

theorem Th12: :: SCMPDS_5:12

for b₁ being Instruction of SCMPDS holds dom (stop (Load b₁)) = {(inspos 0),(inspos 1)}

proof end;

theorem Th13: :: SCMPDS_5:13

for b₁ being Instruction of SCMPDS holds
( inspos 0 in dom (Initialized (stop (Load b₁))) & inspos 1 in dom (Initialized (stop (Load b₁))) & (Initialized (stop (Load b₁))) . (inspos 0) = b₁ & (Initialized (stop (Load b₁))) . (inspos 1) = halt SCMPDS )

proof end;

theorem Th14: :: SCMPDS_5:14

for b₁, b₂ being Program-block holds Initialized (stop (b₁ ';' b₂)) = (b₁ ';' (b₂ ';' SCMPDS-Stop )) +* (Start-At (inspos 0)) by SCMPDS_4:46;

theorem Th15: :: SCMPDS_5:15

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

proof end;

theorem Th16: :: SCMPDS_5:16

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

proof end;

theorem Th17: :: SCMPDS_5:17

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

proof end;

theorem Th18: :: SCMPDS_5:18

for b₁ being State of SCMPDS
for b₂ being Program-block st Initialized b₂ c= b₁ holds
IC b₁ = inspos 0

proof end;

theorem Th19: :: SCMPDS_5:19

for b₁ being Int_position
for b₂ being State of SCMPDS
for b₃ being Program-block holds (b₂ +* (Initialized b₃)) . b₁ = b₂ . b₁

proof end;

theorem Th20: :: SCMPDS_5:20

for b₁, b₂ being State of SCMPDS
for b₃ being parahalting Program-block st Initialized (stop b₃) c= b₁ & Initialized (stop b₃) c= b₂ & b₁,b₂ equal_outside the Instruction-Locations of SCMPDS holds
for b₄ being Nat holds
( (Computation b₁) . b₄,(Computation b₂) . b₄ equal_outside the Instruction-Locations of SCMPDS & CurInstr ((Computation b₁) . b₄) = CurInstr ((Computation b₂) . b₄) )

proof end;

theorem Th21: :: SCMPDS_5:21

for b₁, b₂ being State of SCMPDS
for b₃ being parahalting Program-block st Initialized (stop b₃) c= b₁ & Initialized (stop b₃) c= b₂ & b₁,b₂ equal_outside the Instruction-Locations of SCMPDS holds
( LifeSpan b₁ = LifeSpan b₂ & Result b₁, Result b₂ equal_outside the Instruction-Locations of SCMPDS )

proof end;

theorem Th22: :: SCMPDS_5:22

for b₁ being State of SCMPDS
for b₂ being Program-block holds IC (IExec b₂,b₁) = IC (Result (b₁ +* (Initialized (stop b₂))))

proof end;

theorem Th23: :: SCMPDS_5:23

for b₁ being State of SCMPDS
for b₂ being parahalting Program-block
for b₃ being Program-block st Initialized (stop b₂) c= b₁ holds
for b₄ being Nat st b₄ <= LifeSpan b₁ holds
(Computation b₁) . b₄,(Computation (b₁ +* (b₂ ';' b₃))) . b₄ equal_outside the Instruction-Locations of SCMPDS

proof end;

theorem Th24: :: SCMPDS_5:24

for b₁ being State of SCMPDS
for b₂ being parahalting Program-block
for b₃ being Program-block st Initialized (stop b₂) c= b₁ holds
for b₄ being Nat st b₄ <= LifeSpan b₁ holds
(Computation b₁) . b₄,(Computation (b₁ +* (Initialized (stop (b₂ ';' b₃))))) . b₄ equal_outside the Instruction-Locations of SCMPDS

proof end;

Lemma24: Load ((DataLoc 0,0) := 0) is parahalting

proof end;

definition

let c₁ be Instruction of SCMPDS ;
attr a₁ is No-StopCode means :Def1: :: SCMPDS_5:def 1
a₁ <> halt SCMPDS ;

end;

:: deftheorem Def1 defines No-StopCode SCMPDS_5:def 1 :

definition

let c₁ be Instruction of SCMPDS ;
attr a₁ is parahalting means :Def2: :: SCMPDS_5:def 2
Load a₁ is parahalting;

end;

:: deftheorem Def2 defines parahalting SCMPDS_5:def 2 :

registration

cluster shiftable No-StopCode parahalting M2(the Instructions of SCMPDS );
existence

proof end;

end;

theorem Th25: :: SCMPDS_5:25

for b₁ being Integer st b₁ <> 0 holds
goto b₁ is No-StopCode

proof end;

registration

let c₁ be Int_position ;
cluster return a₁ -> No-StopCode ;
coherence

proof end;

end;

registration

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

proof end;

cluster saveIC a₁,a₂ -> No-StopCode ;
coherence

proof end;

end;

registration

let c₁ be Int_position ;
let c₂, c₃ be Integer;
cluster a₁,a₂ <>0_goto a₃ -> No-StopCode ;
coherence

proof end;

cluster a₁,a₂ <=0_goto a₃ -> No-StopCode ;
coherence

proof end;

cluster a₁,a₂ >=0_goto a₃ -> No-StopCode ;
coherence

proof end;

cluster a₁,a₂ := a₃ -> No-StopCode ;
coherence

proof end;

end;

registration

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

proof end;

end;

registration

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

end;

registration

cluster halt SCMPDS -> parahalting ;
coherence

proof end;

end;

registration

let c₁ be parahalting Instruction of SCMPDS ;
cluster Load a₁ -> parahalting ;
coherence by Def2;

end;

Lemma27: for b₁ being Instruction of SCMPDS st ( for b₂ being State of SCMPDS holds (Exec b₁,b₂) . (IC SCMPDS ) = Next (IC b₂) ) holds
Load b₁ is parahalting

proof end;

registration

let c₁ be Int_position ;
let c₂ be Integer;
cluster a₁ := a₂ -> No-StopCode parahalting ;
coherence

proof end;

end;

registration

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

proof end;

cluster AddTo a₁,a₂,a₃ -> No-StopCode parahalting ;
coherence

proof end;

end;

registration

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

proof end;

cluster SubFrom a₁,a₃,a₂,a₄ -> No-StopCode parahalting ;
coherence

proof end;

cluster MultBy a₁,a₃,a₂,a₄ -> No-StopCode parahalting ;
coherence

proof end;

cluster Divide a₁,a₃,a₂,a₄ -> No-StopCode parahalting ;
coherence

proof end;

cluster a₁,a₃ := a₂,a₄ -> No-StopCode parahalting ;
coherence

proof end;

end;

theorem Th26: :: SCMPDS_5:26

for b₁ being Instruction of SCMPDS st InsCode b₁ = 1 holds
not b₁ is parahalting

proof end;

definition

let c₁ be FinPartState of SCMPDS ;
attr a₁ is No-StopCode means :Def3: :: SCMPDS_5:def 3
for b₁ being Instruction-Location of SCMPDS st b₁ in dom a₁ holds
a₁ . b₁ <> halt SCMPDS ;

end;

:: deftheorem Def3 defines No-StopCode SCMPDS_5:def 3 :

registration

cluster parahalting shiftable No-StopCode FinPartState of SCMPDS ;
existence

proof end;

end;

registration

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

proof end;

end;

registration

let c₁ be No-StopCode Instruction of SCMPDS ;
cluster Load a₁ -> No-StopCode ;
coherence

proof end;

end;

registration

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

end;

registration

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

end;

registration

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

end;

theorem Th27: :: SCMPDS_5:27

for b₁ being State of SCMPDS
for b₂ being parahalting No-StopCode Program-block st Initialized (stop b₂) c= b₁ holds
IC ((Computation b₁) . (LifeSpan (b₁ +* (Initialized (stop b₂))))) = inspos (card b₂)

proof end;

theorem Th28: :: SCMPDS_5:28

for b₁ being State of SCMPDS
for b₂ being parahalting Program-block
for b₃ being Nat st b₃ < LifeSpan (b₁ +* (Initialized (stop b₂))) holds
IC ((Computation (b₁ +* (Initialized (stop b₂)))) . b₃) in dom b₂

proof end;

theorem Th29: :: SCMPDS_5:29

for b₁ being State of SCMPDS
for b₂ being parahalting Program-block
for b₃ being Nat st Initialized b₂ c= b₁ & b₃ <= LifeSpan (b₁ +* (Initialized (stop b₂))) holds
(Computation b₁) . b₃,(Computation (b₁ +* (Initialized (stop b₂)))) . b₃ equal_outside the Instruction-Locations of SCMPDS

proof end;

theorem Th30: :: SCMPDS_5:30

for b₁ being State of SCMPDS
for b₂ being parahalting No-StopCode Program-block st Initialized b₂ c= b₁ holds
IC ((Computation b₁) . (LifeSpan (b₁ +* (Initialized (stop b₂))))) = inspos (card b₂)

proof end;

theorem Th31: :: SCMPDS_5:31

for b₁ being State of SCMPDS
for b₂ being parahalting Program-block holds
( not Initialized b₂ c= b₁ or CurInstr ((Computation b₁) . (LifeSpan (b₁ +* (Initialized (stop b₂))))) = halt SCMPDS or IC ((Computation b₁) . (LifeSpan (b₁ +* (Initialized (stop b₂))))) = inspos (card b₂) )

proof end;

theorem Th32: :: SCMPDS_5:32

for b₁ being State of SCMPDS
for b₂ being parahalting No-StopCode Program-block
for b₃ being Nat st Initialized b₂ c= b₁ & b₃ < LifeSpan (b₁ +* (Initialized (stop b₂))) holds
CurInstr ((Computation b₁) . b₃) <> halt SCMPDS

proof end;

theorem Th33: :: SCMPDS_5:33

for b₁ being State of SCMPDS
for b₂ being parahalting Program-block
for b₃ being Program-block
for b₄ being Nat st b₄ <= LifeSpan (b₁ +* (Initialized (stop b₂))) holds
(Computation (b₁ +* (Initialized (stop b₂)))) . b₄,(Computation (b₁ +* ((b₂ ';' b₃) +* (Start-At (inspos 0))))) . b₄ equal_outside the Instruction-Locations of SCMPDS

proof end;

theorem Th34: :: SCMPDS_5:34

for b₁ being State of SCMPDS
for b₂ being parahalting Program-block
for b₃ being Program-block
for b₄ being Nat st b₄ <= LifeSpan (b₁ +* (Initialized (stop b₂))) holds
(Computation (b₁ +* (Initialized (stop b₂)))) . b₄,(Computation (b₁ +* (Initialized (stop (b₂ ';' b₃))))) . b₄ equal_outside the Instruction-Locations of SCMPDS

proof end;

registration

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

proof end;

end;

registration

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

end;

registration

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

end;

registration

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

end;

theorem Th35: :: SCMPDS_5:35

for b₁, b₂ being Nat
for b₃, b₄ being State of SCMPDS
for b₅ being parahalting shiftable Program-block st b₃ = (Computation (b₄ +* (Initialized (stop b₅)))) . b₁ holds
Exec (CurInstr b₃),(b₃ +* (Start-At ((IC b₃) + b₂))) = (Following b₃) +* (Start-At ((IC (Following b₃)) + b₂))

proof end;

theorem Th36: :: SCMPDS_5:36

for b₁ being State of SCMPDS
for b₂ being parahalting No-StopCode Program-block
for b₃ being parahalting shiftable Program-block
for b₄ being Nat st Initialized (stop (b₂ ';' b₃)) c= b₁ holds
((Computation ((Result (b₁ +* (Initialized (stop b₂)))) +* (Initialized (stop b₃)))) . b₄) +* (Start-At ((IC ((Computation ((Result (b₁ +* (Initialized (stop b₂)))) +* (Initialized (stop b₃)))) . b₄)) + (card b₂))),(Computation (b₁ +* (Initialized (stop (b₂ ';' b₃))))) . ((LifeSpan (b₁ +* (Initialized (stop b₂)))) + b₄) equal_outside the Instruction-Locations of SCMPDS

proof end;

Lemma39: for b₁ being parahalting No-StopCode Program-block
for b₂ being parahalting shiftable Program-block
for b₃, b₄ being State of SCMPDS st Initialized (stop (b₁ ';' b₂)) c= b₃ & b₄ = b₃ +* (Initialized (stop b₁)) holds
( IC ((Computation b₃) . (LifeSpan b₄)) = inspos (card b₁) & ((Computation b₃) . (LifeSpan b₄)) | SCM-Data-Loc = (((Computation b₄) . (LifeSpan b₄)) +* (Initialized (stop b₂))) | SCM-Data-Loc & Shift (stop b₂),(card b₁) c= (Computation b₃) . (LifeSpan b₄) & LifeSpan b₃ = (LifeSpan b₄) + (LifeSpan ((Result b₄) +* (Initialized (stop b₂)))) )

proof end;

theorem Th37: :: SCMPDS_5:37

for b₁ being State of SCMPDS
for b₂ being parahalting No-StopCode Program-block
for b₃ being parahalting shiftable Program-block holds LifeSpan (b₁ +* (Initialized (stop (b₂ ';' b₃)))) = (LifeSpan (b₁ +* (Initialized (stop b₂)))) + (LifeSpan ((Result (b₁ +* (Initialized (stop b₂)))) +* (Initialized (stop b₃))))

proof end;

theorem Th38: :: SCMPDS_5:38

for b₁ being State of SCMPDS
for b₂ being parahalting No-StopCode Program-block
for b₃ being parahalting shiftable Program-block holds IExec (b₂ ';' b₃),b₁ = (IExec b₃,(IExec b₂,b₁)) +* (Start-At ((IC (IExec b₃,(IExec b₂,b₁))) + (card b₂)))

proof end;

theorem Th39: :: SCMPDS_5:39

for b₁ being Int_position
for b₂ being State of SCMPDS
for b₃ being parahalting No-StopCode Program-block
for b₄ being parahalting shiftable Program-block holds (IExec (b₃ ';' b₄),b₂) . b₁ = (IExec b₄,(IExec b₃,b₂)) . b₁

proof end;

definition

let c₁ be State of SCMPDS ;
func Initialized c₁ -> State of SCMPDS equals :: SCMPDS_5:def 4
a₁ +* (Start-At (inspos 0));
coherence ;

end;

:: deftheorem Def4 defines Initialized SCMPDS_5:def 4 :

theorem Th40: :: SCMPDS_5:40

for b₁ being Int_position
for b₂ being State of SCMPDS
for b₃ being Instruction-Location of SCMPDS holds
( IC (Initialized b₂) = inspos 0 & (Initialized b₂) . b₁ = b₂ . b₁ & (Initialized b₂) . b₃ = b₂ . b₃ )

proof end;

theorem Th41: :: SCMPDS_5:41

for b₁, b₂ being State of SCMPDS holds
( b₁,b₂ equal_outside the Instruction-Locations of SCMPDS iff b₁ | (SCM-Data-Loc \/ {(IC SCMPDS )}) = b₂ | (SCM-Data-Loc \/ {(IC SCMPDS )}) )

proof end;

theorem Th42: :: SCMPDS_5:42

canceled;

theorem Th43: :: SCMPDS_5:43

for b₁ being Instruction of SCMPDS
for b₂, b₃ being State of SCMPDS st b₂ | SCM-Data-Loc = b₃ | SCM-Data-Loc & InsCode b₁ <> 3 holds
(Exec b₁,b₂) | SCM-Data-Loc = (Exec b₁,b₃) | SCM-Data-Loc

proof end;

theorem Th44: :: SCMPDS_5:44

for b₁, b₂ being State of SCMPDS
for b₃ being shiftable Instruction of SCMPDS st b₁ | SCM-Data-Loc = b₂ | SCM-Data-Loc holds
(Exec b₃,b₁) | SCM-Data-Loc = (Exec b₃,b₂) | SCM-Data-Loc

proof end;

theorem Th45: :: SCMPDS_5:45

for b₁ being State of SCMPDS
for b₂ being parahalting Instruction of SCMPDS holds Exec b₂,(Initialized b₁) = IExec (Load b₂),b₁

proof end;

theorem Th46: :: SCMPDS_5:46

for b₁ being Int_position
for b₂ being State of SCMPDS
for b₃ being parahalting No-StopCode Program-block
for b₄ being shiftable parahalting Instruction of SCMPDS holds (IExec (b₃ ';' b₄),b₂) . b₁ = (Exec b₄,(IExec b₃,b₂)) . b₁

proof end;

theorem Th47: :: SCMPDS_5:47

for b₁ being Int_position
for b₂ being State of SCMPDS
for b₃ being No-StopCode parahalting Instruction of SCMPDS
for b₄ being shiftable parahalting Instruction of SCMPDS holds (IExec (b₃ ';' b₄),b₂) . b₁ = (Exec b₄,(Exec b₃,(Initialized b₂))) . b₁

proof end;