:: SCMPDS_7 semantic presentation

set c₁ = the Instruction-Locations of SCMPDS ;

set c₂ = SCM-Data-Loc ;

theorem Th1: :: SCMPDS_7:1

for b₁ being State of SCMPDS
for b₂, b₃ being Nat st IC b₁ = inspos b₂ holds
ICplusConst b₁,(b₃ - b₂) = inspos b₃

proof end;

theorem Th2: :: SCMPDS_7:2

for b₁, b₂ being FinPartState of SCMPDS st b₁ c= b₂ holds
ProgramPart b₁ c= ProgramPart b₂

proof end;

theorem Th3: :: SCMPDS_7:3

for b₁, b₂ being programmed FinPartState of SCMPDS
for b₃ being Nat st b₁ c= b₂ holds
Shift b₁,b₃ c= Shift b₂,b₃

proof end;

theorem Th4: :: SCMPDS_7:4

for b₁ being State of SCMPDS st IC b₁ = inspos 0 holds
Initialized b₁ = b₁

proof end;

theorem Th5: :: SCMPDS_7:5

for b₁ being State of SCMPDS
for b₂ being Program-block st IC b₁ = inspos 0 holds
b₁ +* (Initialized b₂) = b₁ +* b₂

proof end;

theorem Th6: :: SCMPDS_7:6

for b₁ being Nat
for b₂ being State of SCMPDS holds ((Computation b₂) . b₁) | the Instruction-Locations of SCMPDS = b₂ | the Instruction-Locations of SCMPDS

proof end;

theorem Th7: :: SCMPDS_7:7

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

proof end;

theorem Th8: :: SCMPDS_7:8

for b₁ being Instruction-Location of SCMPDS
for b₂ being Program-block holds
( b₁ in dom b₂ iff b₁ in dom (Initialized b₂) )

proof end;

theorem Th9: :: SCMPDS_7:9

for b₁ being set
for b₂ being State of SCMPDS
for b₃ being Instruction-Location of SCMPDS
for b₄ being Program-block st b₁ in dom b₄ holds
b₄ . b₁ = (b₂ +* (b₄ +* (Start-At b₃))) . b₁

proof end;

theorem Th10: :: SCMPDS_7:10

for b₁ being State of SCMPDS
for b₂ being Instruction-Location of SCMPDS
for b₃ being Program-block st b₂ in dom b₃ holds
(b₁ +* (Initialized b₃)) . b₂ = b₃ . b₂

proof end;

theorem Th11: :: SCMPDS_7:11

for b₁ being Int_position
for b₂ being State of SCMPDS
for b₃ being Instruction-Location of SCMPDS
for b₄ being Program-block holds (b₂ +* (b₄ +* (Start-At b₃))) . b₁ = b₂ . b₁

proof end;

theorem Th12: :: SCMPDS_7:12

for b₁ being State of SCMPDS
for b₂ being Instruction-Location of SCMPDS holds (b₁ +* (Start-At b₂)) . (IC SCMPDS ) = b₂

proof end;

theorem Th13: :: SCMPDS_7:13

canceled;

theorem Th14: :: SCMPDS_7:14

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

proof end;

theorem Th15: :: SCMPDS_7:15

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

proof end;

theorem Th16: :: SCMPDS_7:16

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

proof end;

theorem Th17: :: SCMPDS_7:17

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

proof end;

theorem Th18: :: SCMPDS_7:18

for b₁ being Nat
for b₂ being Instruction-Location of SCMPDS
for b₃ being Program-block st b₂ in dom b₃ holds
(Shift (stop b₃),b₁) . (b₂ + b₁) = (Shift b₃,b₁) . (b₂ + b₁)

proof end;

theorem Th19: :: SCMPDS_7:19

for b₁ being Nat
for b₂ being Program-block st card b₂ > 0 holds
(Shift (stop b₂),b₁) . (inspos b₁) = (Shift b₂,b₁) . (inspos b₁)

proof end;

theorem Th20: :: SCMPDS_7:20

for b₁ being State of SCMPDS
for b₂ being Instruction of SCMPDS st InsCode b₂ in {0,4,5,6} holds
(Exec b₂,b₁) | SCM-Data-Loc = b₁ | SCM-Data-Loc

proof end;

theorem Th21: :: SCMPDS_7:21

for b₁, b₂ being State of SCMPDS holds (b₁ +* (b₂ | the Instruction-Locations of SCMPDS )) | SCM-Data-Loc = b₁ | SCM-Data-Loc

proof end;

theorem Th22: :: SCMPDS_7:22

for b₁ being Instruction of SCMPDS holds rng (Load b₁) = {b₁}

proof end;

theorem Th23: :: SCMPDS_7:23

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

proof end;

theorem Th24: :: SCMPDS_7:24

for b₁, b₂ being State of SCMPDS
for b₃ being Program-block st b₃ is_closed_on b₁ & Initialized (stop b₃) c= b₁ & Initialized (stop b₃) c= b₂ & b₁ | SCM-Data-Loc = b₂ | SCM-Data-Loc holds
for b₄ being Nat holds
( IC ((Computation 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;

theorem Th25: :: SCMPDS_7:25

for b₁, b₂ being State of SCMPDS
for b₃ being Program-block st b₃ is_closed_on b₁ & b₁ | SCM-Data-Loc = b₂ | SCM-Data-Loc holds
for b₄ being Nat holds
( (Computation (b₁ +* (Initialized (stop b₃)))) . b₄,(Computation (b₂ +* (Initialized (stop b₃)))) . b₄ equal_outside the Instruction-Locations of SCMPDS & CurInstr ((Computation (b₁ +* (Initialized (stop b₃)))) . b₄) = CurInstr ((Computation (b₂ +* (Initialized (stop b₃)))) . b₄) )

proof end;

theorem Th26: :: SCMPDS_7:26

for b₁, b₂ being State of SCMPDS
for b₃ being Program-block st b₃ is_closed_on b₁ & 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 Th27: :: SCMPDS_7:27

for b₁, b₂ being State of SCMPDS
for b₃ being Program-block st b₃ is_closed_on b₁ & b₃ is_halting_on b₁ & Initialized (stop b₃) c= b₁ & Initialized (stop b₃) c= b₂ & b₁ | SCM-Data-Loc = b₂ | SCM-Data-Loc holds
LifeSpan b₁ = LifeSpan b₂

proof end;

theorem Th28: :: SCMPDS_7:28

for b₁, b₂ being State of SCMPDS
for b₃ being Program-block st b₃ is_closed_on b₁ & b₃ is_halting_on b₁ & 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 Th29: :: SCMPDS_7:29

for b₁, b₂ being State of SCMPDS
for b₃ being Program-block st b₃ is_closed_on b₁ & b₃ is_halting_on b₁ & b₁ | SCM-Data-Loc = b₂ | SCM-Data-Loc holds
( LifeSpan (b₁ +* (Initialized (stop b₃))) = LifeSpan (b₂ +* (Initialized (stop b₃))) & Result (b₁ +* (Initialized (stop b₃))), Result (b₂ +* (Initialized (stop b₃))) equal_outside the Instruction-Locations of SCMPDS )

proof end;

theorem Th30: :: SCMPDS_7:30

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

proof end;

registration

let c₃ be Program-block;
cluster Initialized a₁ -> initial ;
correctness

proof end;

end;

theorem Th31: :: SCMPDS_7:31

for b₁ being State of SCMPDS
for b₂ being Program-block
for b₃ being Int_position st b₂ is_halting_on b₁ holds
(IExec b₂,b₁) . b₃ = ((Computation (b₁ +* (Initialized (stop b₂)))) . (LifeSpan (b₁ +* (Initialized (stop b₂))))) . b₃

proof end;

theorem Th32: :: SCMPDS_7:32

for b₁ being State of SCMPDS
for b₂ being parahalting Program-block
for b₃ being Int_position holds (IExec b₂,b₁) . b₃ = ((Computation (b₁ +* (Initialized (stop b₂)))) . (LifeSpan (b₁ +* (Initialized (stop b₂))))) . b₃

proof end;

theorem Th33: :: SCMPDS_7:33

for b₁ being State of SCMPDS
for b₂ being Program-block
for b₃ being Nat st Initialized (stop b₂) c= b₁ & b₂ is_closed_on b₁ & b₂ is_halting_on b₁ & b₃ < LifeSpan b₁ holds
IC ((Computation b₁) . b₃) in dom b₂

proof end;

theorem Th34: :: SCMPDS_7:34

for b₁, b₂ being State of SCMPDS
for b₃ being shiftable Program-block st Initialized (stop b₃) c= b₁ & b₃ is_closed_on b₁ & b₃ is_halting_on b₁ holds
for b₄ being Nat st Shift b₃,b₄ c= b₂ & card b₃ > 0 & IC b₂ = inspos b₄ & b₁ | SCM-Data-Loc = b₂ | SCM-Data-Loc holds
for b₅ being Nat st b₅ < LifeSpan b₁ 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;

theorem Th35: :: SCMPDS_7:35

for b₁ being State of SCMPDS
for b₂ being No-StopCode Program-block st Initialized (stop b₂) c= b₁ & b₂ is_halting_on b₁ & card b₂ > 0 holds
LifeSpan b₁ > 0

proof end;

theorem Th36: :: SCMPDS_7:36

for b₁, b₂ being State of SCMPDS
for b₃ being shiftable No-StopCode Program-block st Initialized (stop b₃) c= b₁ & b₃ is_closed_on b₁ & b₃ is_halting_on b₁ holds
for b₄ being Nat st Shift b₃,b₄ c= b₂ & card b₃ > 0 & IC b₂ = inspos b₄ & b₁ | SCM-Data-Loc = b₂ | SCM-Data-Loc holds
( IC ((Computation b₂) . (LifeSpan b₁)) = inspos ((card b₃) + b₄) & ((Computation b₁) . (LifeSpan b₁)) | SCM-Data-Loc = ((Computation b₂) . (LifeSpan b₁)) | SCM-Data-Loc )

proof end;

theorem Th37: :: SCMPDS_7:37

for b₁ being State of SCMPDS
for b₂ being Program-block
for b₃ being Nat st IC ((Computation (b₁ +* (Initialized b₂))) . b₃) = inspos 0 holds
((Computation (b₁ +* (Initialized b₂))) . b₃) +* (Initialized b₂) = (Computation (b₁ +* (Initialized b₂))) . b₃

proof end;

theorem Th38: :: SCMPDS_7:38

for b₁ being State of SCMPDS
for b₂, b₃ being Program-block
for b₄ being Nat st b₂ is_closed_on b₁ & b₂ is_halting_on b₁ & 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 Th39: :: SCMPDS_7:39

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

proof end;

theorem Th40: :: SCMPDS_7:40

for b₁ being State of SCMPDS
for b₂, b₃ being Program-block
for b₄ being Nat st b₄ <= LifeSpan (b₁ +* (Initialized (stop b₂))) & b₂ c= b₃ & b₂ is_closed_on b₁ & b₂ is_halting_on b₁ holds
IC ((Computation (b₁ +* (Initialized b₃))) . b₄) in dom (stop b₂)

proof end;

theorem Th41: :: SCMPDS_7:41

for b₁ being State of SCMPDS
for b₂, b₃ being Program-block st b₂ c= b₃ & b₂ is_closed_on b₁ & b₂ is_halting_on b₁ & not CurInstr ((Computation (b₁ +* (Initialized b₃))) . (LifeSpan (b₁ +* (Initialized (stop b₂))))) = halt SCMPDS holds
IC ((Computation (b₁ +* (Initialized b₃))) . (LifeSpan (b₁ +* (Initialized (stop b₂))))) = inspos (card b₂)

proof end;

theorem Th42: :: SCMPDS_7:42

for b₁ being State of SCMPDS
for b₂, b₃ being Program-block st b₂ is_halting_on b₁ & b₃ is_closed_on IExec b₂,b₁ & b₃ is_halting_on IExec b₂,b₁ holds
( b₃ is_closed_on (Computation (b₁ +* (Initialized (stop b₂)))) . (LifeSpan (b₁ +* (Initialized (stop b₂)))) & b₃ is_halting_on (Computation (b₁ +* (Initialized (stop b₂)))) . (LifeSpan (b₁ +* (Initialized (stop b₂)))) )

proof end;

theorem Th43: :: SCMPDS_7:43

for b₁ being State of SCMPDS
for b₂ being Program-block
for b₃ being shiftable Program-block st b₂ is_closed_on b₁ & b₂ is_halting_on b₁ & b₃ is_closed_on IExec b₂,b₁ & b₃ is_halting_on IExec b₂,b₁ holds
( b₂ ';' b₃ is_closed_on b₁ & b₂ ';' b₃ is_halting_on b₁ )

proof end;

theorem Th44: :: SCMPDS_7:44

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

proof end;

theorem Th45: :: SCMPDS_7:45

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

proof end;

theorem Th46: :: SCMPDS_7:46

for b₁, b₂ being Program-block
for b₃ being State of SCMPDS
for b₄ being Nat st b₁ is_closed_on b₃ & b₁ is_halting_on b₃ & b₄ < LifeSpan (b₃ +* (Initialized (stop b₁))) holds
CurInstr ((Computation (b₃ +* (Initialized (stop (b₁ ';' b₂))))) . b₄) <> halt SCMPDS

proof end;

Lemma35: for b₁ being No-StopCode Program-block
for b₂ being shiftable Program-block
for b₃, b₄, b₅ being State of SCMPDS st b₁ is_closed_on b₃ & b₁ is_halting_on b₃ & b₂ is_closed_on IExec b₁,b₃ & b₂ is_halting_on IExec b₁,b₃ & b₅ = b₃ +* (Initialized (stop (b₁ ';' 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 Th47: :: SCMPDS_7:47

for b₁ being State of SCMPDS
for b₂ being No-StopCode Program-block
for b₃ being shiftable Program-block st b₂ is_closed_on b₁ & b₂ is_halting_on b₁ & b₃ is_closed_on IExec b₂,b₁ & b₃ is_halting_on IExec b₂,b₁ holds
LifeSpan (b₁ +* (Initialized (stop (b₂ ';' b₃)))) = (LifeSpan (b₁ +* (Initialized (stop b₂)))) + (LifeSpan ((Result (b₁ +* (Initialized (stop b₂)))) +* (Initialized (stop b₃)))) by Lemma35;

theorem Th48: :: SCMPDS_7:48

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

proof end;

theorem Th49: :: SCMPDS_7:49

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

proof end;

theorem Th50: :: SCMPDS_7:50

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

proof end;

definition

let c₃ be Int_position ;
let c₄ be Integer;
let c₅ be Nat;
let c₆ be Program-block;
func for-up c₁,c₂,c₃,c₄ -> Program-block equals :: SCMPDS_7:def 1
(((a₁,a₂ >=0_goto ((card a₄) + 3)) ';' a₄) ';' (AddTo a₁,a₂,a₃)) ';' (goto (- ((card a₄) + 2)));
coherence ;

end;

:: deftheorem Def1 defines for-up SCMPDS_7:def 1 :

theorem Th51: :: SCMPDS_7:51

for b₁ being Int_position
for b₂ being Integer
for b₃ being Nat
for b₄ being Program-block holds card (for-up b₁,b₂,b₃,b₄) = (card b₄) + 3

proof end;

Lemma40: for b₁ being Int_position
for b₂ being Integer
for b₃ being Nat
for b₄ being Program-block holds card (stop (for-up b₁,b₂,b₃,b₄)) = (card b₄) + 4

proof end;

theorem Th52: :: SCMPDS_7:52

for b₁ being Int_position
for b₂ being Integer
for b₃, b₄ being Nat
for b₅ being Program-block holds
( b₄ < (card b₅) + 3 iff inspos b₄ in dom (for-up b₁,b₂,b₃,b₅) )

proof end;

theorem Th53: :: SCMPDS_7:53

for b₁ being Int_position
for b₂ being Integer
for b₃ being Nat
for b₄ being Program-block holds
( (for-up b₁,b₂,b₃,b₄) . (inspos 0) = b₁,b₂ >=0_goto ((card b₄) + 3) & (for-up b₁,b₂,b₃,b₄) . (inspos ((card b₄) + 1)) = AddTo b₁,b₂,b₃ & (for-up b₁,b₂,b₃,b₄) . (inspos ((card b₄) + 2)) = goto (- ((card b₄) + 2)) )

proof end;

Lemma43: for b₁ being Int_position
for b₂ being Integer
for b₃ being Nat
for b₄ being Program-block holds for-up b₁,b₂,b₃,b₄ = (b₁,b₂ >=0_goto ((card b₄) + 3)) ';' ((b₄ ';' (AddTo b₁,b₂,b₃)) ';' (goto (- ((card b₄) + 2))))
by Th15;

theorem Th54: :: SCMPDS_7:54

for b₁ being State of SCMPDS
for b₂ being Program-block
for b₃ being Int_position
for b₄ being Integer
for b₅ being Nat st b₁ . (DataLoc (b₁ . b₃),b₄) >= 0 holds
( for-up b₃,b₄,b₅,b₂ is_closed_on b₁ & for-up b₃,b₄,b₅,b₂ is_halting_on b₁ )

proof end;

theorem Th55: :: SCMPDS_7:55

for b₁ being State of SCMPDS
for b₂ being Program-block
for b₃, b₄ being Int_position
for b₅ being Integer
for b₆ being Nat st b₁ . (DataLoc (b₁ . b₃),b₅) >= 0 holds
IExec (for-up b₃,b₅,b₆,b₂),b₁ = b₁ +* (Start-At (inspos ((card b₂) + 3)))

proof end;

theorem Th56: :: SCMPDS_7:56

for b₁ being State of SCMPDS
for b₂ being Program-block
for b₃ being Int_position
for b₄ being Integer
for b₅ being Nat st b₁ . (DataLoc (b₁ . b₃),b₄) >= 0 holds
IC (IExec (for-up b₃,b₄,b₅,b₂),b₁) = inspos ((card b₂) + 3)

proof end;

theorem Th57: :: SCMPDS_7:57

for b₁ being State of SCMPDS
for b₂ being Program-block
for b₃, b₄ being Int_position
for b₅ being Integer
for b₆ being Nat st b₁ . (DataLoc (b₁ . b₃),b₅) >= 0 holds
(IExec (for-up b₃,b₅,b₆,b₂),b₁) . b₄ = b₁ . b₄

proof end;

Lemma46: for b₁ being Program-block
for b₂ being Int_position
for b₃ being Integer
for b₄ being Nat holds Shift b₁,1 c= for-up b₂,b₃,b₄,b₁

proof end;

theorem Th58: :: SCMPDS_7:58

for b₁ being State of SCMPDS
for b₂ being shiftable No-StopCode Program-block
for b₃ being Int_position
for b₄ being Integer
for b₅ being Nat
for b₆ being set st b₁ . (DataLoc (b₁ . b₃),b₄) < 0 & not DataLoc (b₁ . b₃),b₄ in b₆ & b₅ > 0 & card b₂ > 0 & b₃ <> DataLoc (b₁ . b₃),b₄ & ( for b₇ being State of SCMPDS st ( for b₈ being Int_position st b₈ in b₆ holds
b₇ . b₈ = b₁ . b₈ ) & b₇ . b₃ = b₁ . b₃ holds
( (IExec b₂,b₇) . b₃ = b₇ . b₃ & (IExec b₂,b₇) . (DataLoc (b₁ . b₃),b₄) = b₇ . (DataLoc (b₁ . b₃),b₄) & b₂ is_closed_on b₇ & b₂ is_halting_on b₇ & ( for b₈ being Int_position st b₈ in b₆ holds
(IExec b₂,b₇) . b₈ = b₇ . b₈ ) ) ) holds
( for-up b₃,b₄,b₅,b₂ is_closed_on b₁ & for-up b₃,b₄,b₅,b₂ is_halting_on b₁ )

proof end;

theorem Th59: :: SCMPDS_7:59

for b₁ being State of SCMPDS
for b₂ being shiftable No-StopCode Program-block
for b₃ being Int_position
for b₄ being Integer
for b₅ being Nat
for b₆ being set st b₁ . (DataLoc (b₁ . b₃),b₄) < 0 & not DataLoc (b₁ . b₃),b₄ in b₆ & b₅ > 0 & card b₂ > 0 & b₃ <> DataLoc (b₁ . b₃),b₄ & ( for b₇ being State of SCMPDS st ( for b₈ being Int_position st b₈ in b₆ holds
b₇ . b₈ = b₁ . b₈ ) & b₇ . b₃ = b₁ . b₃ holds
( (IExec b₂,b₇) . b₃ = b₇ . b₃ & (IExec b₂,b₇) . (DataLoc (b₁ . b₃),b₄) = b₇ . (DataLoc (b₁ . b₃),b₄) & b₂ is_closed_on b₇ & b₂ is_halting_on b₇ & ( for b₈ being Int_position st b₈ in b₆ holds
(IExec b₂,b₇) . b₈ = b₇ . b₈ ) ) ) holds
IExec (for-up b₃,b₄,b₅,b₂),b₁ = IExec (for-up b₃,b₄,b₅,b₂),(IExec (b₂ ';' (AddTo b₃,b₄,b₅)),b₁)

proof end;

registration

let c₃ be shiftable Program-block;
let c₄ be Int_position ;
let c₅ be Integer;
let c₆ be Nat;
cluster for-up a₂,a₃,a₄,a₁ -> shiftable ;
correctness

proof end;

end;

registration

let c₃ be No-StopCode Program-block;
let c₄ be Int_position ;
let c₅ be Integer;
let c₆ be Nat;
cluster for-up a₂,a₃,a₄,a₁ -> No-StopCode ;
correctness

proof end;

end;

definition

let c₃ be Int_position ;
let c₄ be Integer;
let c₅ be Nat;
let c₆ be Program-block;
func for-down c₁,c₂,c₃,c₄ -> Program-block equals :: SCMPDS_7:def 2
(((a₁,a₂ <=0_goto ((card a₄) + 3)) ';' a₄) ';' (AddTo a₁,a₂,(- a₃))) ';' (goto (- ((card a₄) + 2)));
coherence ;

end;

:: deftheorem Def2 defines for-down SCMPDS_7:def 2 :

theorem Th60: :: SCMPDS_7:60

for b₁ being Int_position
for b₂ being Integer
for b₃ being Nat
for b₄ being Program-block holds card (for-down b₁,b₂,b₃,b₄) = (card b₄) + 3

proof end;

Lemma49: for b₁ being Int_position
for b₂ being Integer
for b₃ being Nat
for b₄ being Program-block holds card (stop (for-down b₁,b₂,b₃,b₄)) = (card b₄) + 4

proof end;

theorem Th61: :: SCMPDS_7:61

for b₁ being Int_position
for b₂ being Integer
for b₃, b₄ being Nat
for b₅ being Program-block holds
( b₄ < (card b₅) + 3 iff inspos b₄ in dom (for-down b₁,b₂,b₃,b₅) )

proof end;

theorem Th62: :: SCMPDS_7:62

for b₁ being Int_position
for b₂ being Integer
for b₃ being Nat
for b₄ being Program-block holds
( (for-down b₁,b₂,b₃,b₄) . (inspos 0) = b₁,b₂ <=0_goto ((card b₄) + 3) & (for-down b₁,b₂,b₃,b₄) . (inspos ((card b₄) + 1)) = AddTo b₁,b₂,(- b₃) & (for-down b₁,b₂,b₃,b₄) . (inspos ((card b₄) + 2)) = goto (- ((card b₄) + 2)) )

proof end;

Lemma52: for b₁ being Int_position
for b₂ being Integer
for b₃ being Nat
for b₄ being Program-block holds for-down b₁,b₂,b₃,b₄ = (b₁,b₂ <=0_goto ((card b₄) + 3)) ';' ((b₄ ';' (AddTo b₁,b₂,(- b₃))) ';' (goto (- ((card b₄) + 2))))
by Th15;

theorem Th63: :: SCMPDS_7:63

for b₁ being State of SCMPDS
for b₂ being Program-block
for b₃ being Int_position
for b₄ being Integer
for b₅ being Nat st b₁ . (DataLoc (b₁ . b₃),b₄) <= 0 holds
( for-down b₃,b₄,b₅,b₂ is_closed_on b₁ & for-down b₃,b₄,b₅,b₂ is_halting_on b₁ )

proof end;

theorem Th64: :: SCMPDS_7:64

for b₁ being State of SCMPDS
for b₂ being Program-block
for b₃, b₄ being Int_position
for b₅ being Integer
for b₆ being Nat st b₁ . (DataLoc (b₁ . b₃),b₅) <= 0 holds
IExec (for-down b₃,b₅,b₆,b₂),b₁ = b₁ +* (Start-At (inspos ((card b₂) + 3)))

proof end;

theorem Th65: :: SCMPDS_7:65

for b₁ being State of SCMPDS
for b₂ being Program-block
for b₃ being Int_position
for b₄ being Integer
for b₅ being Nat st b₁ . (DataLoc (b₁ . b₃),b₄) <= 0 holds
IC (IExec (for-down b₃,b₄,b₅,b₂),b₁) = inspos ((card b₂) + 3)

proof end;

theorem Th66: :: SCMPDS_7:66

for b₁ being State of SCMPDS
for b₂ being Program-block
for b₃, b₄ being Int_position
for b₅ being Integer
for b₆ being Nat st b₁ . (DataLoc (b₁ . b₃),b₅) <= 0 holds
(IExec (for-down b₃,b₅,b₆,b₂),b₁) . b₄ = b₁ . b₄

proof end;

Lemma56: for b₁ being Program-block
for b₂ being Int_position
for b₃ being Integer
for b₄ being Nat holds Shift b₁,1 c= for-down b₂,b₃,b₄,b₁

proof end;

theorem Th67: :: SCMPDS_7:67

for b₁ being State of SCMPDS
for b₂ being shiftable No-StopCode Program-block
for b₃ being Int_position
for b₄ being Integer
for b₅ being Nat
for b₆ being set st b₁ . (DataLoc (b₁ . b₃),b₄) > 0 & not DataLoc (b₁ . b₃),b₄ in b₆ & b₅ > 0 & card b₂ > 0 & b₃ <> DataLoc (b₁ . b₃),b₄ & ( for b₇ being State of SCMPDS st ( for b₈ being Int_position st b₈ in b₆ holds
b₇ . b₈ = b₁ . b₈ ) & b₇ . b₃ = b₁ . b₃ holds
( (IExec b₂,b₇) . b₃ = b₇ . b₃ & (IExec b₂,b₇) . (DataLoc (b₁ . b₃),b₄) = b₇ . (DataLoc (b₁ . b₃),b₄) & b₂ is_closed_on b₇ & b₂ is_halting_on b₇ & ( for b₈ being Int_position st b₈ in b₆ holds
(IExec b₂,b₇) . b₈ = b₇ . b₈ ) ) ) holds
( for-down b₃,b₄,b₅,b₂ is_closed_on b₁ & for-down b₃,b₄,b₅,b₂ is_halting_on b₁ )

proof end;

theorem Th68: :: SCMPDS_7:68

for b₁ being State of SCMPDS
for b₂ being shiftable No-StopCode Program-block
for b₃ being Int_position
for b₄ being Integer
for b₅ being Nat
for b₆ being set st b₁ . (DataLoc (b₁ . b₃),b₄) > 0 & not DataLoc (b₁ . b₃),b₄ in b₆ & b₅ > 0 & card b₂ > 0 & b₃ <> DataLoc (b₁ . b₃),b₄ & ( for b₇ being State of SCMPDS st ( for b₈ being Int_position st b₈ in b₆ holds
b₇ . b₈ = b₁ . b₈ ) & b₇ . b₃ = b₁ . b₃ holds
( (IExec b₂,b₇) . b₃ = b₇ . b₃ & (IExec b₂,b₇) . (DataLoc (b₁ . b₃),b₄) = b₇ . (DataLoc (b₁ . b₃),b₄) & b₂ is_closed_on b₇ & b₂ is_halting_on b₇ & ( for b₈ being Int_position st b₈ in b₆ holds
(IExec b₂,b₇) . b₈ = b₇ . b₈ ) ) ) holds
IExec (for-down b₃,b₄,b₅,b₂),b₁ = IExec (for-down b₃,b₄,b₅,b₂),(IExec (b₂ ';' (AddTo b₃,b₄,(- b₅))),b₁)

proof end;

registration

let c₃ be shiftable Program-block;
let c₄ be Int_position ;
let c₅ be Integer;
let c₆ be Nat;
cluster for-down a₂,a₃,a₄,a₁ -> shiftable ;
correctness

proof end;

end;

registration

let c₃ be No-StopCode Program-block;
let c₄ be Int_position ;
let c₅ be Integer;
let c₆ be Nat;
cluster for-down a₂,a₃,a₄,a₁ -> No-StopCode ;
correctness

proof end;

end;

definition

let c₃ be Nat;
func sum c₁ -> Program-block equals :: SCMPDS_7:def 3
(((GBP := 0) ';' (GBP ,2 := a₁)) ';' (GBP ,3 := 0)) ';' (for-down GBP ,2,1,(Load (AddTo GBP ,3,1)));
coherence ;

end;

:: deftheorem Def3 defines sum SCMPDS_7:def 3 :

theorem Th69: :: SCMPDS_7:69

for b₁ being State of SCMPDS st b₁ . GBP = 0 holds
( for-down GBP ,2,1,(Load (AddTo GBP ,3,1)) is_closed_on b₁ & for-down GBP ,2,1,(Load (AddTo GBP ,3,1)) is_halting_on b₁ )

proof end;

theorem Th70: :: SCMPDS_7:70

for b₁ being State of SCMPDS
for b₂ being Nat st b₁ . GBP = 0 & b₁ . (intpos 2) = b₂ & b₁ . (intpos 3) = 0 holds
(IExec (for-down GBP ,2,1,(Load (AddTo GBP ,3,1))),b₁) . (intpos 3) = b₂

proof end;

theorem Th71: :: SCMPDS_7:71

for b₁ being State of SCMPDS
for b₂ being Nat holds (IExec (sum b₂),b₁) . (intpos 3) = b₂

proof end;

definition

let c₃, c₄, c₅, c₆, c₇ be Nat;
func sum c₁,c₂,c₃,c₄,c₅ -> Program-block equals :: SCMPDS_7:def 4
(((intpos a₁),a₃ := 0) ';' ((intpos a₄) := a₅)) ';' (for-down (intpos a₁),a₂,1,((AddTo (intpos a₁),a₃,(intpos a₅),0) ';' (AddTo (intpos a₄),0,1)));
coherence ;

end;

:: deftheorem Def4 defines sum SCMPDS_7:def 4 :

theorem Th72: :: SCMPDS_7:72

for b₁ being State of SCMPDS
for b₂, b₃, b₄, b₅, b₆ being Nat st b₁ . (intpos b₂) > b₂ & b₃ < b₄ & b₁ . (intpos b₅) = b₆ & (b₁ . (intpos b₂)) + b₄ < b₅ & b₅ < b₆ & b₆ < b₁ . (intpos b₆) holds
( for-down (intpos b₂),b₃,1,((AddTo (intpos b₂),b₄,(intpos b₆),0) ';' (AddTo (intpos b₅),0,1)) is_closed_on b₁ & for-down (intpos b₂),b₃,1,((AddTo (intpos b₂),b₄,(intpos b₆),0) ';' (AddTo (intpos b₅),0,1)) is_halting_on b₁ )

proof end;

theorem Th73: :: SCMPDS_7:73

for b₁ being State of SCMPDS
for b₂, b₃, b₄, b₅, b₆ being Nat
for b₇ being FinSequence of NAT st b₁ . (intpos b₂) > b₂ & b₃ < b₄ & b₁ . (intpos b₅) = b₆ & (b₁ . (intpos b₂)) + b₄ < b₅ & b₅ < b₆ & b₆ < b₁ . (intpos b₆) & b₁ . (DataLoc (b₁ . (intpos b₂)),b₄) = 0 & len b₇ = b₁ . (DataLoc (b₁ . (intpos b₂)),b₃) & ( for b₈ being Nat st b₈ < len b₇ holds
b₇ . (b₈ + 1) = b₁ . (DataLoc (b₁ . (intpos b₆)),b₈) ) holds
(IExec (for-down (intpos b₂),b₃,1,((AddTo (intpos b₂),b₄,(intpos b₆),0) ';' (AddTo (intpos b₅),0,1))),b₁) . (DataLoc (b₁ . (intpos b₂)),b₄) = Sum b₇

proof end;

theorem Th74: :: SCMPDS_7:74

for b₁ being State of SCMPDS
for b₂, b₃, b₄, b₅, b₆ being Nat
for b₇ being FinSequence of NAT st b₁ . (intpos b₂) > b₂ & b₃ < b₄ & (b₁ . (intpos b₂)) + b₄ < b₅ & b₅ < b₆ & b₆ < b₁ . (intpos b₆) & len b₇ = b₁ . (DataLoc (b₁ . (intpos b₂)),b₃) & ( for b₈ being Nat st b₈ < len b₇ holds
b₇ . (b₈ + 1) = b₁ . (DataLoc (b₁ . (intpos b₆)),b₈) ) holds
(IExec (sum b₂,b₃,b₄,b₅,b₆),b₁) . (DataLoc (b₁ . (intpos b₂)),b₄) = Sum b₇

proof end;