:: SCMPDS_6 semantic presentation

set c₁ = the Instruction-Locations of SCMPDS ;

set c₂ = SCM-Data-Loc ;

theorem Th1: :: SCMPDS_6:1

for b₁ being State of SCMPDS holds dom (b₁ | the Instruction-Locations of SCMPDS ) = the Instruction-Locations of SCMPDS

proof end;

theorem Th2: :: SCMPDS_6:2

for b₁ being State of SCMPDS st b₁ is halting holds
for b₂ being Nat st LifeSpan b₁ <= b₂ holds
CurInstr ((Computation b₁) . b₂) = halt SCMPDS

proof end;

theorem Th3: :: SCMPDS_6:3

for b₁ being State of SCMPDS st b₁ is halting holds
for b₂ being Nat st LifeSpan b₁ <= b₂ holds
IC ((Computation b₁) . b₂) = IC ((Computation b₁) . (LifeSpan b₁))

proof end;

theorem Th4: :: SCMPDS_6:4

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

proof end;

theorem Th5: :: SCMPDS_6:5

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

proof end;

theorem Th6: :: SCMPDS_6:6

for b₁ being Program-block
for b₂ being Instruction-Location of SCMPDS holds b₁ c= b₁ +* (Start-At b₂)

proof end;

theorem Th7: :: SCMPDS_6:7

for b₁ being State of SCMPDS
for b₂ being Instruction-Location of SCMPDS holds b₁ | SCM-Data-Loc = (b₁ +* (Start-At b₂)) | SCM-Data-Loc

proof end;

theorem Th8: :: SCMPDS_6:8

for b₁ being State of SCMPDS
for b₂ being Program-block
for b₃ being Instruction-Location of SCMPDS holds b₁ | SCM-Data-Loc = (b₁ +* (b₂ +* (Start-At b₃))) | SCM-Data-Loc

proof end;

theorem Th9: :: SCMPDS_6:9

for b₁ being State of SCMPDS
for b₂ being Program-block holds b₁ | SCM-Data-Loc = (b₁ +* (Initialized b₂)) | SCM-Data-Loc

proof end;

theorem Th10: :: SCMPDS_6:10

for b₁ being State of SCMPDS
for b₂ being Instruction-Location of SCMPDS holds dom (b₁ | the Instruction-Locations of SCMPDS ) misses dom (Start-At b₂)

proof end;

theorem Th11: :: SCMPDS_6:11

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

proof end;

theorem Th12: :: SCMPDS_6:12

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

proof end;

theorem Th13: :: SCMPDS_6:13

canceled;

theorem Th14: :: SCMPDS_6:14

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

proof end;

theorem Th15: :: SCMPDS_6:15

for b₁ being Instruction of SCMPDS
for b₂ being Program-block holds card (b₁ ';' b₂) = (card b₂) + 1

proof end;

theorem Th16: :: SCMPDS_6:16

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

proof end;

theorem Th17: :: SCMPDS_6:17

for b₁ being Program-block holds b₁ c= Initialized (stop b₁)

proof end;

theorem Th18: :: SCMPDS_6:18

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

proof end;

theorem Th19: :: SCMPDS_6:19

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

proof end;

theorem Th20: :: SCMPDS_6:20

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

proof end;

theorem Th21: :: SCMPDS_6:21

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

proof end;

theorem Th22: :: SCMPDS_6:22

for b₁ being Instruction of SCMPDS
for b₂ being State of SCMPDS
for b₃ being Program-block holds CurInstr (b₂ +* (Initialized (stop (b₁ ';' b₃)))) = b₁

proof end;

theorem Th23: :: SCMPDS_6:23

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

proof end;

theorem Th24: :: SCMPDS_6:24

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

proof end;

theorem Th25: :: SCMPDS_6:25

for b₁ being Program-block holds
( inspos (card b₁) in dom (stop b₁) & (stop b₁) . (inspos (card b₁)) = halt SCMPDS )

proof end;

theorem Th26: :: SCMPDS_6:26

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

proof end;

theorem Th27: :: SCMPDS_6:27

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

proof end;

theorem Th28: :: SCMPDS_6:28

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

proof end;

theorem Th29: :: SCMPDS_6:29

for b₁ being Int_position
for b₂, b₃ being Integer holds b₁,b₂ <>0_goto b₃ <> halt SCMPDS

proof end;

theorem Th30: :: SCMPDS_6:30

for b₁ being Int_position
for b₂, b₃ being Integer holds b₁,b₂ <=0_goto b₃ <> halt SCMPDS

proof end;

theorem Th31: :: SCMPDS_6:31

for b₁ being Int_position
for b₂, b₃ being Integer holds b₁,b₂ >=0_goto b₃ <> halt SCMPDS

proof end;

definition

let c₃ be Integer;
func Goto c₁ -> Program-block equals :: SCMPDS_6:def 1
Load (goto a₁);
coherence ;

end;

:: deftheorem Def1 defines Goto SCMPDS_6:def 1 :

registration

let c₃ be Nat;
cluster goto (a₁ + 1) -> No-StopCode ;
correctness by SCMPDS_5:25;
cluster goto (- (a₁ + 1)) -> No-StopCode ;
correctness

proof end;

end;

registration

let c₃ be Nat;
cluster Goto (a₁ + 1) -> No-StopCode ;
correctness ;
cluster Goto (- (a₁ + 1)) -> No-StopCode ;
correctness ;

end;

theorem Th32: :: SCMPDS_6:32

for b₁ being Integer holds card (Goto b₁) = 1 by SCMPDS_5:6;

Lemma28: for b₁ being Integer holds
( inspos 0 in dom ((inspos 0) .--> (goto b₁)) & ((inspos 0) .--> (goto b₁)) . (inspos 0) = goto b₁ )

proof end;

theorem Th33: :: SCMPDS_6:33

for b₁ being Integer holds
( inspos 0 in dom (Goto b₁) & (Goto b₁) . (inspos 0) = goto b₁ )

proof end;

definition

let c₃ be Program-block;
let c₄ be State of SCMPDS ;
pred c₁ is_closed_on c₂ means :Def2: :: SCMPDS_6:def 2
for b₁ being Nat holds IC ((Computation (a₂ +* (Initialized (stop a₁)))) . b₁) in dom (stop a₁);
pred c₁ is_halting_on c₂ means :Def3: :: SCMPDS_6:def 3
a₂ +* (Initialized (stop a₁)) is halting;

end;

:: deftheorem Def2 defines is_closed_on SCMPDS_6:def 2 :

:: deftheorem Def3 defines is_halting_on SCMPDS_6:def 3 :

theorem Th34: :: SCMPDS_6:34

for b₁ being Program-block holds
( b₁ is paraclosed iff for b₂ being State of SCMPDS holds b₁ is_closed_on b₂ )

proof end;

theorem Th35: :: SCMPDS_6:35

for b₁ being Program-block holds
( b₁ is parahalting iff for b₂ being State of SCMPDS holds b₁ is_halting_on b₂ )

proof end;

theorem Th36: :: SCMPDS_6:36

for b₁, b₂ being State of SCMPDS
for b₃ being Program-block st b₁ | SCM-Data-Loc = b₂ | SCM-Data-Loc & b₃ is_closed_on b₁ holds
b₃ is_closed_on b₂

proof end;

theorem Th37: :: SCMPDS_6:37

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

proof end;

theorem Th38: :: SCMPDS_6:38

for b₁ being State of SCMPDS
for b₂, b₃ being Program-block holds
( b₂ is_closed_on b₁ iff b₂ is_closed_on b₁ +* (Initialized b₃) )

proof end;

theorem Th39: :: SCMPDS_6:39

for b₁, b₂ being Program-block
for b₃ being State of SCMPDS st b₁ is_closed_on b₃ & b₁ is_halting_on b₃ holds
( ( for b₄ being Nat st b₄ <= LifeSpan (b₃ +* (Initialized (stop b₁))) holds
IC ((Computation (b₃ +* (Initialized (stop b₁)))) . b₄) = IC ((Computation (b₃ +* (Initialized (stop (b₁ ';' b₂))))) . b₄) ) & ((Computation (b₃ +* (Initialized (stop b₁)))) . (LifeSpan (b₃ +* (Initialized (stop b₁))))) | SCM-Data-Loc = ((Computation (b₃ +* (Initialized (stop (b₁ ';' b₂))))) . (LifeSpan (b₃ +* (Initialized (stop b₁))))) | SCM-Data-Loc )

proof end;

theorem Th40: :: SCMPDS_6:40

for b₁ being State of SCMPDS
for 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
IC ((Computation (b₁ +* (Initialized (stop b₂)))) . b₃) in dom b₂

proof end;

theorem Th41: :: SCMPDS_6:41

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₄) = CurInstr ((Computation (b₃ +* (Initialized (stop (b₁ ';' b₂))))) . b₄)

proof end;

theorem Th42: :: SCMPDS_6:42

for b₁ being No-StopCode 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₃) <> halt SCMPDS

proof end;

theorem Th43: :: SCMPDS_6:43

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

proof end;

Lemma41: for b₁ being No-StopCode Program-block
for b₂ being Program-block
for b₃ being State of SCMPDS st b₁ is_closed_on b₃ & b₁ is_halting_on b₃ holds
( IC ((Computation (b₃ +* (Initialized (stop ((b₁ ';' (Goto ((card b₂) + 1))) ';' b₂))))) . ((LifeSpan (b₃ +* (Initialized (stop b₁)))) + 1)) = inspos (((card b₁) + (card b₂)) + 1) & ((Computation (b₃ +* (Initialized (stop b₁)))) . (LifeSpan (b₃ +* (Initialized (stop b₁))))) | SCM-Data-Loc = ((Computation (b₃ +* (Initialized (stop ((b₁ ';' (Goto ((card b₂) + 1))) ';' b₂))))) . ((LifeSpan (b₃ +* (Initialized (stop b₁)))) + 1)) | SCM-Data-Loc & ( for b₄ being Nat st b₄ <= LifeSpan (b₃ +* (Initialized (stop b₁))) holds
CurInstr ((Computation (b₃ +* (Initialized (stop ((b₁ ';' (Goto ((card b₂) + 1))) ';' b₂))))) . b₄) <> halt SCMPDS ) & IC ((Computation (b₃ +* (Initialized (stop ((b₁ ';' (Goto ((card b₂) + 1))) ';' b₂))))) . (LifeSpan (b₃ +* (Initialized (stop b₁))))) = inspos (card b₁) & b₃ +* (Initialized (stop ((b₁ ';' (Goto ((card b₂) + 1))) ';' b₂))) is halting & LifeSpan (b₃ +* (Initialized (stop ((b₁ ';' (Goto ((card b₂) + 1))) ';' b₂)))) = (LifeSpan (b₃ +* (Initialized (stop b₁)))) + 1 )

proof end;

theorem Th44: :: SCMPDS_6:44

for b₁, b₂ being Program-block
for b₃ being State of SCMPDS st b₁ is_closed_on b₃ & b₁ is_halting_on b₃ holds
( (b₁ ';' (Goto ((card b₂) + 1))) ';' b₂ is_halting_on b₃ & (b₁ ';' (Goto ((card b₂) + 1))) ';' b₂ is_closed_on b₃ )

proof end;

theorem Th45: :: SCMPDS_6:45

for b₁, b₂ being State of SCMPDS
for b₃ being shiftable Program-block st Initialized (stop b₃) c= b₁ & b₃ is_closed_on 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;

Lemma44: for b₁ being State of SCMPDS
for b₂, b₃ being shiftable Program-block
for b₄ being Nat holds (b₂ ';' (Goto b₄)) ';' b₃ is shiftable

proof end;

theorem Th46: :: SCMPDS_6:46

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

proof end;

theorem Th47: :: SCMPDS_6:47

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

proof end;

theorem Th48: :: SCMPDS_6:48

for b₁ being State of SCMPDS
for b₂ being No-StopCode Program-block st b₂ is_closed_on b₁ & b₂ is_halting_on b₁ holds
IC (IExec b₂,b₁) = inspos (card b₂)

proof end;

definition

let c₃ be Int_position ;
let c₄ be Integer;
let c₅, c₆ be Program-block;
func if=0 c₁,c₂,c₃,c₄ -> Program-block equals :: SCMPDS_6:def 4
(((a₁,a₂ <>0_goto ((card a₃) + 2)) ';' a₃) ';' (Goto ((card a₄) + 1))) ';' a₄;
coherence ;
func if>0 c₁,c₂,c₃,c₄ -> Program-block equals :: SCMPDS_6:def 5
(((a₁,a₂ <=0_goto ((card a₃) + 2)) ';' a₃) ';' (Goto ((card a₄) + 1))) ';' a₄;
coherence ;
func if<0 c₁,c₂,c₃,c₄ -> Program-block equals :: SCMPDS_6:def 6
(((a₁,a₂ >=0_goto ((card a₃) + 2)) ';' a₃) ';' (Goto ((card a₄) + 1))) ';' a₄;
coherence ;

end;

:: deftheorem Def4 defines if=0 SCMPDS_6:def 4 :

:: deftheorem Def5 defines if>0 SCMPDS_6:def 5 :

:: deftheorem Def6 defines if<0 SCMPDS_6:def 6 :

definition

let c₃ be Int_position ;
let c₄ be Integer;
let c₅ be Program-block;
func if=0 c₁,c₂,c₃ -> Program-block equals :: SCMPDS_6:def 7
(a₁,a₂ <>0_goto ((card a₃) + 1)) ';' a₃;
coherence ;
func if<>0 c₁,c₂,c₃ -> Program-block equals :: SCMPDS_6:def 8
((a₁,a₂ <>0_goto 2) ';' (goto ((card a₃) + 1))) ';' a₃;
coherence ;
func if>0 c₁,c₂,c₃ -> Program-block equals :: SCMPDS_6:def 9
(a₁,a₂ <=0_goto ((card a₃) + 1)) ';' a₃;
coherence ;
func if<=0 c₁,c₂,c₃ -> Program-block equals :: SCMPDS_6:def 10
((a₁,a₂ <=0_goto 2) ';' (goto ((card a₃) + 1))) ';' a₃;
coherence ;
func if<0 c₁,c₂,c₃ -> Program-block equals :: SCMPDS_6:def 11
(a₁,a₂ >=0_goto ((card a₃) + 1)) ';' a₃;
coherence ;
func if>=0 c₁,c₂,c₃ -> Program-block equals :: SCMPDS_6:def 12
((a₁,a₂ >=0_goto 2) ';' (goto ((card a₃) + 1))) ';' a₃;
coherence ;

end;

:: deftheorem Def7 defines if=0 SCMPDS_6:def 7 :

:: deftheorem Def8 defines if<>0 SCMPDS_6:def 8 :

:: deftheorem Def9 defines if>0 SCMPDS_6:def 9 :

:: deftheorem Def10 defines if<=0 SCMPDS_6:def 10 :

:: deftheorem Def11 defines if<0 SCMPDS_6:def 11 :

:: deftheorem Def12 defines if>=0 SCMPDS_6:def 12 :

Lemma48: for b₁ being Nat
for b₂ being Instruction of SCMPDS
for b₃, b₄ being Program-block holds card (((b₂ ';' b₃) ';' (Goto b₁)) ';' b₄) = ((card b₃) + (card b₄)) + 2

proof end;

theorem Th49: :: SCMPDS_6:49

for b₁ being Int_position
for b₂ being Integer
for b₃, b₄ being Program-block holds card (if=0 b₁,b₂,b₃,b₄) = ((card b₃) + (card b₄)) + 2 by Lemma48;

theorem Th50: :: SCMPDS_6:50

for b₁ being Int_position
for b₂ being Integer
for b₃, b₄ being Program-block holds
( inspos 0 in dom (if=0 b₁,b₂,b₃,b₄) & inspos 1 in dom (if=0 b₁,b₂,b₃,b₄) )

proof end;

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

proof end;

theorem Th51: :: SCMPDS_6:51

for b₁ being Int_position
for b₂ being Integer
for b₃, b₄ being Program-block holds (if=0 b₁,b₂,b₃,b₄) . (inspos 0) = b₁,b₂ <>0_goto ((card b₃) + 2) by Lemma50;

Lemma51: for b₁ being Nat
for b₂ being Instruction of SCMPDS
for b₃ being State of SCMPDS
for b₄ being Program-block holds Shift (stop b₄),1 c= (Computation (b₃ +* (Initialized (stop (b₂ ';' b₄))))) . b₁

proof end;

Lemma52: for b₁ being Nat
for b₂, b₃ being Instruction of SCMPDS
for b₄ being State of SCMPDS
for b₅ being Program-block holds Shift (stop b₅),2 c= (Computation (b₄ +* (Initialized (stop ((b₂ ';' b₃) ';' b₅))))) . b₁

proof end;

theorem Th52: :: SCMPDS_6:52

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

proof end;

theorem Th53: :: SCMPDS_6:53

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

proof end;

theorem Th54: :: SCMPDS_6:54

for b₁ being State of SCMPDS
for b₂ being shiftable No-StopCode Program-block
for b₃ being shiftable Program-block
for b₄ being Int_position
for b₅ being Integer st b₁ . (DataLoc (b₁ . b₄),b₅) = 0 & b₂ is_closed_on b₁ & b₂ is_halting_on b₁ holds
IExec (if=0 b₄,b₅,b₂,b₃),b₁ = (IExec b₂,b₁) +* (Start-At (inspos (((card b₂) + (card b₃)) + 2)))

proof end;

theorem Th55: :: SCMPDS_6:55

for b₁ being State of SCMPDS
for b₂ being Program-block
for b₃ being shiftable No-StopCode Program-block
for b₄ being Int_position
for b₅ being Integer st b₁ . (DataLoc (b₁ . b₄),b₅) <> 0 & b₃ is_closed_on b₁ & b₃ is_halting_on b₁ holds
IExec (if=0 b₄,b₅,b₂,b₃),b₁ = (IExec b₃,b₁) +* (Start-At (inspos (((card b₂) + (card b₃)) + 2)))

proof end;

registration

let c₃, c₄ be parahalting shiftable Program-block;
let c₅ be Int_position ;
let c₆ be Integer;
cluster if=0 a₃,a₄,a₁,a₂ -> parahalting shiftable ;
correctness

proof end;

end;

registration

let c₃, c₄ be No-StopCode Program-block;
let c₅ be Int_position ;
let c₆ be Integer;
cluster if=0 a₃,a₄,a₁,a₂ -> No-StopCode ;
coherence ;

end;

theorem Th56: :: SCMPDS_6:56

for b₁ being State of SCMPDS
for b₂, b₃ being parahalting shiftable No-StopCode Program-block
for b₄ being Int_position
for b₅ being Integer holds IC (IExec (if=0 b₄,b₅,b₂,b₃),b₁) = inspos (((card b₂) + (card b₃)) + 2)

proof end;

theorem Th57: :: SCMPDS_6:57

for b₁ being State of SCMPDS
for b₂ being parahalting shiftable No-StopCode Program-block
for b₃ being shiftable Program-block
for b₄, b₅ being Int_position
for b₆ being Integer st b₁ . (DataLoc (b₁ . b₄),b₆) = 0 holds
(IExec (if=0 b₄,b₆,b₂,b₃),b₁) . b₅ = (IExec b₂,b₁) . b₅

proof end;

theorem Th58: :: SCMPDS_6:58

for b₁ being State of SCMPDS
for b₂ being Program-block
for b₃ being parahalting shiftable No-StopCode Program-block
for b₄, b₅ being Int_position
for b₆ being Integer st b₁ . (DataLoc (b₁ . b₄),b₆) <> 0 holds
(IExec (if=0 b₄,b₆,b₂,b₃),b₁) . b₅ = (IExec b₃,b₁) . b₅

proof end;

theorem Th59: :: SCMPDS_6:59

for b₁ being Int_position
for b₂ being Integer
for b₃ being Program-block holds card (if=0 b₁,b₂,b₃) = (card b₃) + 1 by Th15;

theorem Th60: :: SCMPDS_6:60

for b₁ being Int_position
for b₂ being Integer
for b₃ being Program-block holds inspos 0 in dom (if=0 b₁,b₂,b₃)

proof end;

theorem Th61: :: SCMPDS_6:61

for b₁ being Int_position
for b₂ being Integer
for b₃ being Program-block holds (if=0 b₁,b₂,b₃) . (inspos 0) = b₁,b₂ <>0_goto ((card b₃) + 1) by Th16;

theorem Th62: :: SCMPDS_6:62

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

proof end;

theorem Th63: :: SCMPDS_6:63

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

proof end;

theorem Th64: :: SCMPDS_6:64

for b₁ being State of SCMPDS
for b₂ being shiftable No-StopCode Program-block
for b₃ being Int_position
for b₄ being Integer st b₁ . (DataLoc (b₁ . b₃),b₄) = 0 & b₂ is_closed_on b₁ & b₂ is_halting_on b₁ holds
IExec (if=0 b₃,b₄,b₂),b₁ = (IExec b₂,b₁) +* (Start-At (inspos ((card b₂) + 1)))

proof end;

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

proof end;

theorem Th65: :: SCMPDS_6:65

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

proof end;

registration

let c₃ be parahalting shiftable Program-block;
let c₄ be Int_position ;
let c₅ be Integer;
cluster if=0 a₂,a₃,a₁ -> parahalting shiftable ;
correctness

proof end;

end;

registration

let c₃ be No-StopCode Program-block;
let c₄ be Int_position ;
let c₅ be Integer;
cluster if=0 a₂,a₃,a₁ -> No-StopCode ;
coherence ;

end;

theorem Th66: :: SCMPDS_6:66

for b₁ being State of SCMPDS
for b₂ being parahalting shiftable No-StopCode Program-block
for b₃ being Int_position
for b₄ being Integer holds IC (IExec (if=0 b₃,b₄,b₂),b₁) = inspos ((card b₂) + 1)

proof end;

theorem Th67: :: SCMPDS_6:67

for b₁ being State of SCMPDS
for b₂ being parahalting shiftable No-StopCode Program-block
for b₃, b₄ being Int_position
for b₅ being Integer st b₁ . (DataLoc (b₁ . b₃),b₅) = 0 holds
(IExec (if=0 b₃,b₅,b₂),b₁) . b₄ = (IExec b₂,b₁) . b₄

proof end;

theorem Th68: :: SCMPDS_6:68

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

proof end;

Lemma63: for b₁, b₂ being Instruction of SCMPDS
for b₃ being Program-block holds card ((b₁ ';' b₂) ';' b₃) = (card b₃) + 2

proof end;

theorem Th69: :: SCMPDS_6:69

for b₁ being Int_position
for b₂ being Integer
for b₃ being Program-block holds card (if<>0 b₁,b₂,b₃) = (card b₃) + 2 by Lemma63;

Lemma65: for b₁, b₂ being Instruction of SCMPDS
for b₃ being Program-block holds
( inspos 0 in dom ((b₁ ';' b₂) ';' b₃) & inspos 1 in dom ((b₁ ';' b₂) ';' b₃) )

proof end;

theorem Th70: :: SCMPDS_6:70

for b₁ being Int_position
for b₂ being Integer
for b₃ being Program-block holds
( inspos 0 in dom (if<>0 b₁,b₂,b₃) & inspos 1 in dom (if<>0 b₁,b₂,b₃) ) by Lemma65;

Lemma67: for b₁, b₂ being Instruction of SCMPDS
for b₃ being Program-block holds
( ((b₁ ';' b₂) ';' b₃) . (inspos 0) = b₁ & ((b₁ ';' b₂) ';' b₃) . (inspos 1) = b₂ )

proof end;

theorem Th71: :: SCMPDS_6:71

for b₁ being Int_position
for b₂ being Integer
for b₃ being Program-block holds
( (if<>0 b₁,b₂,b₃) . (inspos 0) = b₁,b₂ <>0_goto 2 & (if<>0 b₁,b₂,b₃) . (inspos 1) = goto ((card b₃) + 1) ) by Lemma67;

theorem Th72: :: SCMPDS_6:72

for b₁ being State of SCMPDS
for b₂ being shiftable Program-block
for b₃ being Int_position
for b₄ being Integer st b₁ . (DataLoc (b₁ . b₃),b₄) <> 0 & b₂ is_closed_on b₁ & b₂ is_halting_on b₁ holds
( if<>0 b₃,b₄,b₂ is_closed_on b₁ & if<>0 b₃,b₄,b₂ is_halting_on b₁ )

proof end;

theorem Th73: :: SCMPDS_6:73

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

proof end;

theorem Th74: :: SCMPDS_6:74

for b₁ being State of SCMPDS
for b₂ being shiftable No-StopCode Program-block
for b₃ being Int_position
for b₄ being Integer st b₁ . (DataLoc (b₁ . b₃),b₄) <> 0 & b₂ is_closed_on b₁ & b₂ is_halting_on b₁ holds
IExec (if<>0 b₃,b₄,b₂),b₁ = (IExec b₂,b₁) +* (Start-At (inspos ((card b₂) + 2)))

proof end;

theorem Th75: :: SCMPDS_6:75

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

proof end;

registration

let c₃ be parahalting shiftable Program-block;
let c₄ be Int_position ;
let c₅ be Integer;
cluster if<>0 a₂,a₃,a₁ -> parahalting shiftable ;
correctness

proof end;

end;

registration

let c₃ be No-StopCode Program-block;
let c₄ be Int_position ;
let c₅ be Integer;
cluster if<>0 a₂,a₃,a₁ -> No-StopCode ;
coherence ;

end;

theorem Th76: :: SCMPDS_6:76

for b₁ being State of SCMPDS
for b₂ being parahalting shiftable No-StopCode Program-block
for b₃ being Int_position
for b₄ being Integer holds IC (IExec (if<>0 b₃,b₄,b₂),b₁) = inspos ((card b₂) + 2)

proof end;

theorem Th77: :: SCMPDS_6:77

for b₁ being State of SCMPDS
for b₂ being parahalting shiftable No-StopCode Program-block
for b₃, b₄ being Int_position
for b₅ being Integer st b₁ . (DataLoc (b₁ . b₃),b₅) <> 0 holds
(IExec (if<>0 b₃,b₅,b₂),b₁) . b₄ = (IExec b₂,b₁) . b₄

proof end;

theorem Th78: :: SCMPDS_6:78

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

proof end;

theorem Th79: :: SCMPDS_6:79

for b₁ being Int_position
for b₂ being Integer
for b₃, b₄ being Program-block holds card (if>0 b₁,b₂,b₃,b₄) = ((card b₃) + (card b₄)) + 2 by Lemma48;

theorem Th80: :: SCMPDS_6:80

for b₁ being Int_position
for b₂ being Integer
for b₃, b₄ being Program-block holds
( inspos 0 in dom (if>0 b₁,b₂,b₃,b₄) & inspos 1 in dom (if>0 b₁,b₂,b₃,b₄) )

proof end;

theorem Th81: :: SCMPDS_6:81

for b₁ being Int_position
for b₂ being Integer
for b₃, b₄ being Program-block holds (if>0 b₁,b₂,b₃,b₄) . (inspos 0) = b₁,b₂ <=0_goto ((card b₃) + 2) by Lemma50;

theorem Th82: :: SCMPDS_6:82

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

proof end;

theorem Th83: :: SCMPDS_6:83

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

proof end;

theorem Th84: :: SCMPDS_6:84

for b₁ being State of SCMPDS
for b₂ being shiftable No-StopCode Program-block
for b₃ being shiftable Program-block
for b₄ being Int_position
for b₅ being Integer st b₁ . (DataLoc (b₁ . b₄),b₅) > 0 & b₂ is_closed_on b₁ & b₂ is_halting_on b₁ holds
IExec (if>0 b₄,b₅,b₂,b₃),b₁ = (IExec b₂,b₁) +* (Start-At (inspos (((card b₂) + (card b₃)) + 2)))

proof end;

theorem Th85: :: SCMPDS_6:85

for b₁ being State of SCMPDS
for b₂ being Program-block
for b₃ being shiftable No-StopCode Program-block
for b₄ being Int_position
for b₅ being Integer st b₁ . (DataLoc (b₁ . b₄),b₅) <= 0 & b₃ is_closed_on b₁ & b₃ is_halting_on b₁ holds
IExec (if>0 b₄,b₅,b₂,b₃),b₁ = (IExec b₃,b₁) +* (Start-At (inspos (((card b₂) + (card b₃)) + 2)))

proof end;

registration

let c₃, c₄ be parahalting shiftable Program-block;
let c₅ be Int_position ;
let c₆ be Integer;
cluster if>0 a₃,a₄,a₁,a₂ -> parahalting shiftable ;
correctness

proof end;

end;

registration

let c₃, c₄ be No-StopCode Program-block;
let c₅ be Int_position ;
let c₆ be Integer;
cluster if>0 a₃,a₄,a₁,a₂ -> No-StopCode ;
coherence ;

end;

theorem Th86: :: SCMPDS_6:86

for b₁ being State of SCMPDS
for b₂, b₃ being parahalting shiftable No-StopCode Program-block
for b₄ being Int_position
for b₅ being Integer holds IC (IExec (if>0 b₄,b₅,b₂,b₃),b₁) = inspos (((card b₂) + (card b₃)) + 2)

proof end;

theorem Th87: :: SCMPDS_6:87

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

proof end;

theorem Th88: :: SCMPDS_6:88

for b₁ being State of SCMPDS
for b₂ being Program-block
for b₃ being parahalting shiftable No-StopCode Program-block
for b₄, b₅ being Int_position
for b₆ being Integer st b₁ . (DataLoc (b₁ . b₄),b₆) <= 0 holds
(IExec (if>0 b₄,b₆,b₂,b₃),b₁) . b₅ = (IExec b₃,b₁) . b₅

proof end;

theorem Th89: :: SCMPDS_6:89

for b₁ being Int_position
for b₂ being Integer
for b₃ being Program-block holds card (if>0 b₁,b₂,b₃) = (card b₃) + 1 by Th15;

theorem Th90: :: SCMPDS_6:90

for b₁ being Int_position
for b₂ being Integer
for b₃ being Program-block holds inspos 0 in dom (if>0 b₁,b₂,b₃)

proof end;

theorem Th91: :: SCMPDS_6:91

for b₁ being Int_position
for b₂ being Integer
for b₃ being Program-block holds (if>0 b₁,b₂,b₃) . (inspos 0) = b₁,b₂ <=0_goto ((card b₃) + 1) by Th16;

theorem Th92: :: SCMPDS_6:92

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

proof end;

theorem Th93: :: SCMPDS_6:93

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

proof end;

theorem Th94: :: SCMPDS_6:94

for b₁ being State of SCMPDS
for b₂ being shiftable No-StopCode Program-block
for b₃ being Int_position
for b₄ being Integer st b₁ . (DataLoc (b₁ . b₃),b₄) > 0 & b₂ is_closed_on b₁ & b₂ is_halting_on b₁ holds
IExec (if>0 b₃,b₄,b₂),b₁ = (IExec b₂,b₁) +* (Start-At (inspos ((card b₂) + 1)))

proof end;

theorem Th95: :: SCMPDS_6:95

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

proof end;

registration

let c₃ be parahalting shiftable Program-block;
let c₄ be Int_position ;
let c₅ be Integer;
cluster if>0 a₂,a₃,a₁ -> parahalting shiftable ;
correctness

proof end;

end;

registration

let c₃ be No-StopCode Program-block;
let c₄ be Int_position ;
let c₅ be Integer;
cluster if>0 a₂,a₃,a₁ -> No-StopCode ;
coherence ;

end;

theorem Th96: :: SCMPDS_6:96

for b₁ being State of SCMPDS
for b₂ being parahalting shiftable No-StopCode Program-block
for b₃ being Int_position
for b₄ being Integer holds IC (IExec (if>0 b₃,b₄,b₂),b₁) = inspos ((card b₂) + 1)

proof end;

theorem Th97: :: SCMPDS_6:97

for b₁ being State of SCMPDS
for b₂ being parahalting shiftable No-StopCode Program-block
for b₃, b₄ being Int_position
for b₅ being Integer st b₁ . (DataLoc (b₁ . b₃),b₅) > 0 holds
(IExec (if>0 b₃,b₅,b₂),b₁) . b₄ = (IExec b₂,b₁) . b₄

proof end;

theorem Th98: :: SCMPDS_6:98

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

proof end;

theorem Th99: :: SCMPDS_6:99

for b₁ being Int_position
for b₂ being Integer
for b₃ being Program-block holds card (if<=0 b₁,b₂,b₃) = (card b₃) + 2 by Lemma63;

theorem Th100: :: SCMPDS_6:100

for b₁ being Int_position
for b₂ being Integer
for b₃ being Program-block holds
( inspos 0 in dom (if<=0 b₁,b₂,b₃) & inspos 1 in dom (if<=0 b₁,b₂,b₃) ) by Lemma65;

theorem Th101: :: SCMPDS_6:101

for b₁ being Int_position
for b₂ being Integer
for b₃ being Program-block holds
( (if<=0 b₁,b₂,b₃) . (inspos 0) = b₁,b₂ <=0_goto 2 & (if<=0 b₁,b₂,b₃) . (inspos 1) = goto ((card b₃) + 1) ) by Lemma67;

theorem Th102: :: SCMPDS_6:102

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

proof end;

theorem Th103: :: SCMPDS_6:103

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

proof end;

theorem Th104: :: SCMPDS_6:104

for b₁ being State of SCMPDS
for b₂ being shiftable No-StopCode Program-block
for b₃ being Int_position
for b₄ being Integer st b₁ . (DataLoc (b₁ . b₃),b₄) <= 0 & b₂ is_closed_on b₁ & b₂ is_halting_on b₁ holds
IExec (if<=0 b₃,b₄,b₂),b₁ = (IExec b₂,b₁) +* (Start-At (inspos ((card b₂) + 2)))

proof end;

theorem Th105: :: SCMPDS_6:105

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

proof end;

registration

let c₃ be parahalting shiftable Program-block;
let c₄ be Int_position ;
let c₅ be Integer;
cluster if<=0 a₂,a₃,a₁ -> parahalting shiftable ;
correctness

proof end;

end;

registration

let c₃ be No-StopCode Program-block;
let c₄ be Int_position ;
let c₅ be Integer;
cluster if<=0 a₂,a₃,a₁ -> No-StopCode ;
coherence ;

end;

theorem Th106: :: SCMPDS_6:106

for b₁ being State of SCMPDS
for b₂ being parahalting shiftable No-StopCode Program-block
for b₃ being Int_position
for b₄ being Integer holds IC (IExec (if<=0 b₃,b₄,b₂),b₁) = inspos ((card b₂) + 2)

proof end;

theorem Th107: :: SCMPDS_6:107

for b₁ being State of SCMPDS
for b₂ being parahalting shiftable No-StopCode Program-block
for b₃, b₄ being Int_position
for b₅ being Integer st b₁ . (DataLoc (b₁ . b₃),b₅) <= 0 holds
(IExec (if<=0 b₃,b₅,b₂),b₁) . b₄ = (IExec b₂,b₁) . b₄

proof end;

theorem Th108: :: SCMPDS_6:108

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

proof end;

theorem Th109: :: SCMPDS_6:109

for b₁ being Int_position
for b₂ being Integer
for b₃, b₄ being Program-block holds card (if<0 b₁,b₂,b₃,b₄) = ((card b₃) + (card b₄)) + 2 by Lemma48;

theorem Th110: :: SCMPDS_6:110

for b₁ being Int_position
for b₂ being Integer
for b₃, b₄ being Program-block holds
( inspos 0 in dom (if<0 b₁,b₂,b₃,b₄) & inspos 1 in dom (if<0 b₁,b₂,b₃,b₄) )

proof end;

theorem Th111: :: SCMPDS_6:111

for b₁ being Int_position
for b₂ being Integer
for b₃, b₄ being Program-block holds (if<0 b₁,b₂,b₃,b₄) . (inspos 0) = b₁,b₂ >=0_goto ((card b₃) + 2) by Lemma50;

theorem Th112: :: SCMPDS_6:112

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

proof end;

theorem Th113: :: SCMPDS_6:113

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

proof end;

theorem Th114: :: SCMPDS_6:114

for b₁ being State of SCMPDS
for b₂ being shiftable No-StopCode Program-block
for b₃ being shiftable Program-block
for b₄ being Int_position
for b₅ being Integer st b₁ . (DataLoc (b₁ . b₄),b₅) < 0 & b₂ is_closed_on b₁ & b₂ is_halting_on b₁ holds
IExec (if<0 b₄,b₅,b₂,b₃),b₁ = (IExec b₂,b₁) +* (Start-At (inspos (((card b₂) + (card b₃)) + 2)))

proof end;

theorem Th115: :: SCMPDS_6:115

for b₁ being State of SCMPDS
for b₂ being Program-block
for b₃ being shiftable No-StopCode Program-block
for b₄ being Int_position
for b₅ being Integer st b₁ . (DataLoc (b₁ . b₄),b₅) >= 0 & b₃ is_closed_on b₁ & b₃ is_halting_on b₁ holds
IExec (if<0 b₄,b₅,b₂,b₃),b₁ = (IExec b₃,b₁) +* (Start-At (inspos (((card b₂) + (card b₃)) + 2)))

proof end;

registration

let c₃, c₄ be parahalting shiftable Program-block;
let c₅ be Int_position ;
let c₆ be Integer;
cluster if<0 a₃,a₄,a₁,a₂ -> parahalting shiftable ;
correctness

proof end;

end;

registration

let c₃, c₄ be No-StopCode Program-block;
let c₅ be Int_position ;
let c₆ be Integer;
cluster if<0 a₃,a₄,a₁,a₂ -> No-StopCode ;
coherence ;

end;

theorem Th116: :: SCMPDS_6:116

for b₁ being State of SCMPDS
for b₂, b₃ being parahalting shiftable No-StopCode Program-block
for b₄ being Int_position
for b₅ being Integer holds IC (IExec (if<0 b₄,b₅,b₂,b₃),b₁) = inspos (((card b₂) + (card b₃)) + 2)

proof end;

theorem Th117: :: SCMPDS_6:117

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

proof end;

theorem Th118: :: SCMPDS_6:118

for b₁ being State of SCMPDS
for b₂ being Program-block
for b₃ being parahalting shiftable No-StopCode Program-block
for b₄, b₅ being Int_position
for b₆ being Integer st b₁ . (DataLoc (b₁ . b₄),b₆) >= 0 holds
(IExec (if<0 b₄,b₆,b₂,b₃),b₁) . b₅ = (IExec b₃,b₁) . b₅

proof end;

theorem Th119: :: SCMPDS_6:119

for b₁ being Int_position
for b₂ being Integer
for b₃ being Program-block holds card (if<0 b₁,b₂,b₃) = (card b₃) + 1 by Th15;

theorem Th120: :: SCMPDS_6:120

for b₁ being Int_position
for b₂ being Integer
for b₃ being Program-block holds inspos 0 in dom (if<0 b₁,b₂,b₃)

proof end;

theorem Th121: :: SCMPDS_6:121

for b₁ being Int_position
for b₂ being Integer
for b₃ being Program-block holds (if<0 b₁,b₂,b₃) . (inspos 0) = b₁,b₂ >=0_goto ((card b₃) + 1) by Th16;

theorem Th122: :: SCMPDS_6:122

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

proof end;

theorem Th123: :: SCMPDS_6:123

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

proof end;

theorem Th124: :: SCMPDS_6:124

for b₁ being State of SCMPDS
for b₂ being shiftable No-StopCode Program-block
for b₃ being Int_position
for b₄ being Integer st b₁ . (DataLoc (b₁ . b₃),b₄) < 0 & b₂ is_closed_on b₁ & b₂ is_halting_on b₁ holds
IExec (if<0 b₃,b₄,b₂),b₁ = (IExec b₂,b₁) +* (Start-At (inspos ((card b₂) + 1)))

proof end;

theorem Th125: :: SCMPDS_6:125

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

proof end;

registration

let c₃ be parahalting shiftable Program-block;
let c₄ be Int_position ;
let c₅ be Integer;
cluster if<0 a₂,a₃,a₁ -> parahalting shiftable ;
correctness

proof end;

end;

registration

let c₃ be No-StopCode Program-block;
let c₄ be Int_position ;
let c₅ be Integer;
cluster if<0 a₂,a₃,a₁ -> No-StopCode ;
coherence ;

end;

theorem Th126: :: SCMPDS_6:126

for b₁ being State of SCMPDS
for b₂ being parahalting shiftable No-StopCode Program-block
for b₃ being Int_position
for b₄ being Integer holds IC (IExec (if<0 b₃,b₄,b₂),b₁) = inspos ((card b₂) + 1)

proof end;

theorem Th127: :: SCMPDS_6:127

for b₁ being State of SCMPDS
for b₂ being parahalting shiftable No-StopCode Program-block
for b₃, b₄ being Int_position
for b₅ being Integer st b₁ . (DataLoc (b₁ . b₃),b₅) < 0 holds
(IExec (if<0 b₃,b₅,b₂),b₁) . b₄ = (IExec b₂,b₁) . b₄

proof end;

theorem Th128: :: SCMPDS_6:128

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

proof end;

theorem Th129: :: SCMPDS_6:129

for b₁ being Int_position
for b₂ being Integer
for b₃ being Program-block holds card (if>=0 b₁,b₂,b₃) = (card b₃) + 2 by Lemma63;

theorem Th130: :: SCMPDS_6:130

for b₁ being Int_position
for b₂ being Integer
for b₃ being Program-block holds
( inspos 0 in dom (if>=0 b₁,b₂,b₃) & inspos 1 in dom (if>=0 b₁,b₂,b₃) ) by Lemma65;

theorem Th131: :: SCMPDS_6:131

for b₁ being Int_position
for b₂ being Integer
for b₃ being Program-block holds
( (if>=0 b₁,b₂,b₃) . (inspos 0) = b₁,b₂ >=0_goto 2 & (if>=0 b₁,b₂,b₃) . (inspos 1) = goto ((card b₃) + 1) ) by Lemma67;

theorem Th132: :: SCMPDS_6:132

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

proof end;

theorem Th133: :: SCMPDS_6:133

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

proof end;

theorem Th134: :: SCMPDS_6:134

for b₁ being State of SCMPDS
for b₂ being shiftable No-StopCode Program-block
for b₃ being Int_position
for b₄ being Integer st b₁ . (DataLoc (b₁ . b₃),b₄) >= 0 & b₂ is_closed_on b₁ & b₂ is_halting_on b₁ holds
IExec (if>=0 b₃,b₄,b₂),b₁ = (IExec b₂,b₁) +* (Start-At (inspos ((card b₂) + 2)))

proof end;

theorem Th135: :: SCMPDS_6:135

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

proof end;

registration

let c₃ be parahalting shiftable Program-block;
let c₄ be Int_position ;
let c₅ be Integer;
cluster if>=0 a₂,a₃,a₁ -> parahalting shiftable ;
correctness

proof end;

end;

registration

let c₃ be No-StopCode Program-block;
let c₄ be Int_position ;
let c₅ be Integer;
cluster if>=0 a₂,a₃,a₁ -> No-StopCode ;
coherence ;

end;

theorem Th136: :: SCMPDS_6:136

for b₁ being State of SCMPDS
for b₂ being parahalting shiftable No-StopCode Program-block
for b₃ being Int_position
for b₄ being Integer holds IC (IExec (if>=0 b₃,b₄,b₂),b₁) = inspos ((card b₂) + 2)

proof end;

theorem Th137: :: SCMPDS_6:137

for b₁ being State of SCMPDS
for b₂ being parahalting shiftable No-StopCode Program-block
for b₃, b₄ being Int_position
for b₅ being Integer st b₁ . (DataLoc (b₁ . b₃),b₅) >= 0 holds
(IExec (if>=0 b₃,b₅,b₂),b₁) . b₄ = (IExec b₂,b₁) . b₄

proof end;

theorem Th138: :: SCMPDS_6:138

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

proof end;