:: The Construction and shiftability of Program Blocks for SCMPDS
:: by JingChao Chen
::
:: Received June 15, 1999
:: Copyright (c) 1999 Association of Mizar Users

begin

definition

let i be Instruction of SCMPDS ;
func Load i -> Program of SCMPDS equals :: SCMPDS_4:def 1
(inspos 0 ) .--> i;
coherence
(inspos 0 ) .--> i is Program of SCMPDS

proof end;

correctness
;

end;

:: deftheorem defines Load SCMPDS_4:def 1 :

for i being Instruction of SCMPDS holds Load i = (inspos 0 ) .--> i;

registration

let i be Instruction of SCMPDS ;
cluster Load i -> non empty ;
coherence
not Load i is empty ;

end;

theorem Th1: :: SCMPDS_4:1

for P being Program of SCMPDS
for n being Nat holds
( n < card P iff n in dom P )

proof end;

theorem Th2: :: SCMPDS_4:2

for I, J being Program of SCMPDS holds dom I misses dom (Shift J,(card I))

proof end;

theorem Th3: :: SCMPDS_4:3

for m being Element of NAT
for I being preProgram of SCMPDS holds card (Shift I,m) = card I

proof end;

definition

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

end;

:: deftheorem defines Initialized SCMPDS_4:def 2 :

for I being Program of SCMPDS holds Initialized I = I +* (Start-At (inspos 0 ));

theorem :: SCMPDS_4:4

canceled;

theorem :: SCMPDS_4:5

canceled;

theorem Th6: :: SCMPDS_4:6

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

proof end;

theorem Th7: :: SCMPDS_4:7

for I being Program of SCMPDS holds IC SCMPDS in dom (Initialized I)

proof end;

theorem :: SCMPDS_4:8

for I being Program of SCMPDS holds IC (Initialized I) = inspos 0

proof end;

theorem Th9: :: SCMPDS_4:9

for I being Program of SCMPDS holds I c= Initialized I

proof end;

theorem :: SCMPDS_4:10

canceled;

theorem Th11: :: SCMPDS_4:11

for s1, s2 being State of SCMPDS st IC s1 = IC s2 & ( for a being Int_position holds s1 . a = s2 . a ) holds
s1,s2 equal_outside NAT

proof end;

theorem :: SCMPDS_4:12

canceled;

theorem Th13: :: SCMPDS_4:13

for s1, s2 being State of SCMPDS st s1,s2 equal_outside NAT holds
for a being Int_position holds s1 . a = s2 . a

proof end;

theorem Th14: :: SCMPDS_4:14

for a being Int_position
for s1, s2 being State of SCMPDS
for k1 being Integer st s1,s2 equal_outside NAT holds
s1 . (DataLoc (s1 . a),k1) = s2 . (DataLoc (s2 . a),k1)

proof end;

theorem Th15: :: SCMPDS_4:15

for i being Instruction of SCMPDS
for s1, s2 being State of SCMPDS st s1,s2 equal_outside NAT holds
Exec i,s1, Exec i,s2 equal_outside NAT

proof end;

theorem :: SCMPDS_4:16

for I being Program of SCMPDS holds (Initialized I) | NAT = I

proof end;

theorem Th17: :: SCMPDS_4:17

for k1, k2 being Element of NAT st k1 <> k2 holds
DataLoc k1,0 <> DataLoc k2,0

proof end;

theorem Th18: :: SCMPDS_4:18

for dl being Int_position ex i being Element of NAT st dl = DataLoc i,0

proof end;

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

ex S being State of SCMPDS st
( IC S = F₃() & ( for i being Element of NAT holds
( S . (inspos i) = F₁(i) & S . (DataLoc i,0 ) = F₂(i) ) ) )

proof end;

theorem :: SCMPDS_4:19

for s being State of SCMPDS holds dom s = ({(IC SCMPDS )} \/ SCM-Data-Loc ) \/ NAT by AMI_1:79, SCMPDS_3:5;

theorem :: SCMPDS_4:20

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

proof end;

theorem :: SCMPDS_4:21

for s1, s2 being State of SCMPDS holds
( ( for l being Instruction-Location of SCMPDS holds s1 . l = s2 . l ) iff s1 | NAT = s2 | NAT )

proof end;

theorem :: SCMPDS_4:22

for i being Instruction-Location of SCMPDS holds not i in SCM-Data-Loc

proof end;

theorem Th23: :: SCMPDS_4:23

for s1, s2 being State of SCMPDS holds
( ( for a being Int_position holds s1 . a = s2 . a ) iff DataPart s1 = DataPart s2 )

proof end;

theorem :: SCMPDS_4:24

for s1, s2 being State of SCMPDS st s1,s2 equal_outside NAT holds
DataPart s1 = DataPart s2

proof end;

theorem :: SCMPDS_4:25

canceled;

theorem :: SCMPDS_4:26

for I, J being Program of SCMPDS holds I,J equal_outside NAT

proof end;

theorem Th27: :: SCMPDS_4:27

for I being Program of SCMPDS holds dom (Initialized I) = (dom I) \/ {(IC SCMPDS )}

proof end;

theorem Th28: :: SCMPDS_4:28

for I being Program of SCMPDS
for x being set holds
( not x in dom (Initialized I) or x in dom I or x = IC SCMPDS )

proof end;

theorem Th29: :: SCMPDS_4:29

for I being Program of SCMPDS holds (Initialized I) . (IC SCMPDS ) = inspos 0

proof end;

theorem Th30: :: SCMPDS_4:30

for I being Program of SCMPDS holds not IC SCMPDS in dom I

proof end;

theorem Th31: :: SCMPDS_4:31

for I being Program of SCMPDS
for a being Int_position holds not a in dom (Initialized I)

proof end;

theorem Th32: :: SCMPDS_4:32

for n being Element of NAT
for I being Program of SCMPDS
for x being set st x in dom I holds
I . x = (I +* (Start-At (inspos n))) . x

proof end;

theorem :: SCMPDS_4:33

for I being Program of SCMPDS
for x being set st x in dom I holds
I . x = (Initialized I) . x by Th32;

theorem Th34: :: SCMPDS_4:34

for I, J being Program of SCMPDS
for s being State of SCMPDS st Initialized J c= s holds
s +* (Initialized I) = s +* I

proof end;

theorem :: SCMPDS_4:35

for I, J being Program of SCMPDS
for s being State of SCMPDS st Initialized J c= s holds
Initialized I c= s +* I

proof end;

theorem :: SCMPDS_4:36

for I, J being Program of SCMPDS
for s being State of SCMPDS holds s +* (Initialized I),s +* (Initialized J) equal_outside NAT

proof end;

begin

definition

let I, J be Program of SCMPDS ;
func I ';' J -> Program of SCMPDS equals :: SCMPDS_4:def 3
I +* (Shift J,(card I));
coherence
I +* (Shift J,(card I)) is Program of SCMPDS

proof end;

correctness
;

end;

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

for I, J being Program of SCMPDS holds I ';' J = I +* (Shift J,(card I));

theorem Th37: :: SCMPDS_4:37

for I, J being Program of SCMPDS
for l being Instruction-Location of SCMPDS st l in dom I holds
(I ';' J) . l = I . l

proof end;

theorem Th38: :: SCMPDS_4:38

for I, J being Program of SCMPDS
for l being Instruction-Location of SCMPDS st l in dom J holds
(I ';' J) . (l + (card I)) = J . l

proof end;

theorem Th39: :: SCMPDS_4:39

for I, J being Program of SCMPDS holds dom I c= dom (I ';' J)

proof end;

theorem :: SCMPDS_4:40

for I, J being Program of SCMPDS holds I c= I ';' J

proof end;

theorem :: SCMPDS_4:41

for I, J being Program of SCMPDS holds I +* (I ';' J) = I ';' J

proof end;

theorem :: SCMPDS_4:42

for I, J being Program of SCMPDS holds (Initialized I) +* (I ';' J) = Initialized (I ';' J)

proof end;

begin

definition

let i be Instruction of SCMPDS ;
let J be Program of SCMPDS ;
func i ';' J -> Program of SCMPDS equals :: SCMPDS_4:def 4
(Load i) ';' J;
correctness
coherence
(Load i) ';' J is Program of SCMPDS ;
;

end;

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

for i being Instruction of SCMPDS
for J being Program of SCMPDS holds i ';' J = (Load i) ';' J;

definition

let I be Program of SCMPDS ;
let j be Instruction of SCMPDS ;
func I ';' j -> Program of SCMPDS equals :: SCMPDS_4:def 5
I ';' (Load j);
correctness
coherence
I ';' (Load j) is Program of SCMPDS ;
;

end;

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

for I being Program of SCMPDS
for j being Instruction of SCMPDS holds I ';' j = I ';' (Load j);

definition

let i, j be Instruction of SCMPDS ;
func i ';' j -> Program of SCMPDS equals :: SCMPDS_4:def 6
(Load i) ';' (Load j);
correctness
coherence
(Load i) ';' (Load j) is Program of SCMPDS ;
;

end;

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

for i, j being Instruction of SCMPDS holds i ';' j = (Load i) ';' (Load j);

theorem :: SCMPDS_4:43

for i, j being Instruction of SCMPDS holds i ';' j = (Load i) ';' j ;

theorem :: SCMPDS_4:44

for i, j being Instruction of SCMPDS holds i ';' j = i ';' (Load j) ;

theorem Th45: :: SCMPDS_4:45

for I, J being Program of SCMPDS holds card (I ';' J) = (card I) + (card J)

proof end;

theorem Th46: :: SCMPDS_4:46

for I, J, K being Program of SCMPDS holds (I ';' J) ';' K = I ';' (J ';' K)

proof end;

theorem :: SCMPDS_4:47

for k being Instruction of SCMPDS
for I, J being Program of SCMPDS holds (I ';' J) ';' k = I ';' (J ';' k) by Th46;

theorem :: SCMPDS_4:48

for j being Instruction of SCMPDS
for I, K being Program of SCMPDS holds (I ';' j) ';' K = I ';' (j ';' K) by Th46;

theorem :: SCMPDS_4:49

for j, k being Instruction of SCMPDS
for I being Program of SCMPDS holds (I ';' j) ';' k = I ';' (j ';' k) by Th46;

theorem :: SCMPDS_4:50

for i being Instruction of SCMPDS
for J, K being Program of SCMPDS holds (i ';' J) ';' K = i ';' (J ';' K) by Th46;

theorem :: SCMPDS_4:51

for i, k being Instruction of SCMPDS
for J being Program of SCMPDS holds (i ';' J) ';' k = i ';' (J ';' k) by Th46;

theorem :: SCMPDS_4:52

for i, j being Instruction of SCMPDS
for K being Program of SCMPDS holds (i ';' j) ';' K = i ';' (j ';' K) by Th46;

theorem :: SCMPDS_4:53

for i, j, k being Instruction of SCMPDS holds (i ';' j) ';' k = i ';' (j ';' k) by Th46;

theorem Th54: :: SCMPDS_4:54

for n being Element of NAT
for I being Program of SCMPDS holds dom I misses dom (Start-At (inspos n))

proof end;

theorem :: SCMPDS_4:55

canceled;

theorem Th56: :: SCMPDS_4:56

for n being Element of NAT
for I being Program of SCMPDS
for s being State of SCMPDS st I +* (Start-At (inspos n)) c= s holds
I c= s

proof end;

theorem :: SCMPDS_4:57

for I being Program of SCMPDS
for s being State of SCMPDS st Initialized I c= s holds
I c= s by Th56;

theorem Th58: :: SCMPDS_4:58

for n being Element of NAT
for I being Program of SCMPDS holds (I +* (Start-At (inspos n))) | NAT = I

proof end;

theorem Th59: :: SCMPDS_4:59

for a being Int_position
for l being Instruction-Location of SCMPDS holds not a in dom (Start-At l)

proof end;

theorem :: SCMPDS_4:60

canceled;

theorem :: SCMPDS_4:61

for I being Program of SCMPDS
for a being Int_position
for l being Instruction-Location of SCMPDS holds not a in dom (I +* (Start-At l))

proof end;

theorem :: SCMPDS_4:62

for I being Program of SCMPDS
for s being State of SCMPDS holds (s +* I) +* (Start-At (inspos 0 )) = (s +* (Start-At (inspos 0 ))) +* I

proof end;

definition

let s be State of SCMPDS ;
let li be Int_position ;
let k be Integer;
:: original: +*
redefine func s +* li,k -> State of SCMPDS ;
coherence
s +* li,k is State of SCMPDS

proof end;

end;

begin

definition

let I be Program of SCMPDS ;
func stop I -> Program of SCMPDS equals :: SCMPDS_4:def 7
I ';' (Stop SCMPDS );
coherence
I ';' (Stop SCMPDS ) is Program of SCMPDS ;

end;

:: deftheorem defines stop SCMPDS_4:def 7 :

for I being Program of SCMPDS holds stop I = I ';' (Stop SCMPDS );

definition

let I be Program of SCMPDS ;
let s be State of SCMPDS ;
func IExec I,s -> State of SCMPDS equals :: SCMPDS_4:def 8
(Result (s +* (Initialized (stop I)))) +* (s | NAT );
coherence
(Result (s +* (Initialized (stop I)))) +* (s | NAT ) is State of SCMPDS by CARD_3:96;

end;

:: deftheorem defines IExec SCMPDS_4:def 8 :

for I being Program of SCMPDS
for s being State of SCMPDS holds IExec I,s = (Result (s +* (Initialized (stop I)))) +* (s | NAT );

definition

let I be Program of SCMPDS ;
attr I is paraclosed means :Def9: :: SCMPDS_4:def 9
for s being State of SCMPDS
for n being Element of NAT st Initialized (stop I) c= s holds
IC (Computation s,n) in dom (stop I);
attr I is parahalting means :Def10: :: SCMPDS_4:def 10
Initialized (stop I) is halting ;

end;

:: deftheorem Def9 defines paraclosed SCMPDS_4:def 9 :

for I being Program of SCMPDS holds
( I is paraclosed iff for s being State of SCMPDS
for n being Element of NAT st Initialized (stop I) c= s holds
IC (Computation s,n) in dom (stop I) );

:: deftheorem Def10 defines parahalting SCMPDS_4:def 10 :

for I being Program of SCMPDS holds
( I is parahalting iff Initialized (stop I) is halting );

Lm1: Load (halt SCMPDS ) is parahalting

proof end;

registration

cluster parahalting Element of K234(the Object-Kind of SCMPDS );
existence
ex b₁ being Program of SCMPDS st b₁ is parahalting by Lm1;

end;

theorem Th63: :: SCMPDS_4:63

for s being State of SCMPDS
for I being parahalting Program of SCMPDS st Initialized (stop I) c= s holds
ProgramPart s halts_on s

proof end;

registration

let I be parahalting Program of SCMPDS ;
cluster Initialized (stop I) -> halting ;
coherence
Initialized (stop I) is halting

proof end;

end;

definition

let la, lb be Instruction-Location of SCMPDS ;
let a, b be Instruction of SCMPDS ;
:: original: -->
redefine func la,lb --> a,b -> FinPartState of SCMPDS ;
coherence
la,lb --> a,b is FinPartState of SCMPDS

proof end;

end;

theorem :: SCMPDS_4:64

canceled;

theorem :: SCMPDS_4:65

canceled;

theorem Th66: :: SCMPDS_4:66

for s2 being State of SCMPDS holds not ProgramPart (s2 +* ((IC s2),(Next (IC s2)) --> (goto 1),(goto (- 1)))) halts_on s2 +* ((IC s2),(Next (IC s2)) --> (goto 1),(goto (- 1)))

proof end;

theorem Th67: :: SCMPDS_4:67

for n being Element of NAT
for I being Program of SCMPDS
for s1, s2 being State of SCMPDS st s1,s2 equal_outside NAT & I c= s1 & I c= s2 & ( for m being Element of NAT st m < n holds
IC (Computation s2,m) in dom I ) holds
for m being Element of NAT st m <= n holds
Computation s1,m, Computation s2,m equal_outside NAT

proof end;

theorem Th68: :: SCMPDS_4:68

for s being State of SCMPDS
for l being Instruction-Location of SCMPDS holds l in dom s

proof end;

theorem Th69: :: SCMPDS_4:69

for s being State of SCMPDS
for l1, l2 being Instruction-Location of SCMPDS
for i1, i2 being Instruction of SCMPDS holds s +* (l1,l2 --> i1,i2) = (s +* l1,i1) +* l2,i2

proof end;

theorem :: SCMPDS_4:70

canceled;

theorem Th71: :: SCMPDS_4:71

for I being Program of SCMPDS
for s being State of SCMPDS st not IC s in dom I holds
not Next (IC s) in dom I

proof end;

registration

cluster parahalting -> paraclosed Element of K234(the Object-Kind of SCMPDS );
coherence
for b₁ being Program of SCMPDS st b₁ is parahalting holds
b₁ is paraclosed

proof end;

end;

theorem :: SCMPDS_4:72

canceled;

theorem :: SCMPDS_4:73

( inspos 0 in dom (Stop SCMPDS ) & (Stop SCMPDS ) . (inspos 0 ) = halt SCMPDS ) by AFINSQ_1:38, SCMNORM:2;

theorem Th74: :: SCMPDS_4:74

card (Stop SCMPDS ) = 1 by SCMNORM:3;

theorem Th75: :: SCMPDS_4:75

for I being Program of SCMPDS holds inspos 0 in dom (stop I)

proof end;

begin

definition

let i be Instruction of SCMPDS ;
let n be Element of NAT ;
pred i valid_at n means :Def11: :: SCMPDS_4:def 11
( ( InsCode i = 0 implies ex k1 being Integer st
( i = goto k1 & n + k1 >= 0 ) ) & ( InsCode i = 4 implies ex a being Int_position ex k1, k2 being Integer st
( i = a,k1 <>0_goto k2 & n + k2 >= 0 ) ) & ( InsCode i = 5 implies ex a being Int_position ex k1, k2 being Integer st
( i = a,k1 <=0_goto k2 & n + k2 >= 0 ) ) & ( InsCode i = 6 implies ex a being Int_position ex k1, k2 being Integer st
( i = a,k1 >=0_goto k2 & n + k2 >= 0 ) ) );

end;

:: deftheorem Def11 defines valid_at SCMPDS_4:def 11 :

for i being Instruction of SCMPDS
for n being Element of NAT holds
( i valid_at n iff ( ( InsCode i = 0 implies ex k1 being Integer st
( i = goto k1 & n + k1 >= 0 ) ) & ( InsCode i = 4 implies ex a being Int_position ex k1, k2 being Integer st
( i = a,k1 <>0_goto k2 & n + k2 >= 0 ) ) & ( InsCode i = 5 implies ex a being Int_position ex k1, k2 being Integer st
( i = a,k1 <=0_goto k2 & n + k2 >= 0 ) ) & ( InsCode i = 6 implies ex a being Int_position ex k1, k2 being Integer st
( i = a,k1 >=0_goto k2 & n + k2 >= 0 ) ) ) );

theorem :: SCMPDS_4:76

canceled;

theorem Th77: :: SCMPDS_4:77

for i being Instruction of SCMPDS
for m, n being Element of NAT st i valid_at m & m <= n holds
i valid_at n

proof end;

definition

let IT be FinPartState of SCMPDS ;
attr IT is shiftable means :Def12: :: SCMPDS_4:def 12
for n being Element of NAT
for i being Instruction of SCMPDS st inspos n in dom IT & i = IT . (inspos n) holds
( InsCode i <> 1 & InsCode i <> 3 & i valid_at n );

end;

:: deftheorem Def12 defines shiftable SCMPDS_4:def 12 :

for IT being FinPartState of SCMPDS holds
( IT is shiftable iff for n being Element of NAT
for i being Instruction of SCMPDS st inspos n in dom IT & i = IT . (inspos n) holds
( InsCode i <> 1 & InsCode i <> 3 & i valid_at n ) );

Lm2: Load (halt SCMPDS ) is shiftable

proof end;

registration

cluster parahalting shiftable Element of K234(the Object-Kind of SCMPDS );
existence
ex b₁ being Program of SCMPDS st
( b₁ is parahalting & b₁ is shiftable ) by Lm1, Lm2;

end;

definition

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

end;

:: deftheorem Def13 defines shiftable SCMPDS_4:def 13 :

for i being Instruction of SCMPDS holds
( i is shiftable iff ( InsCode i = 2 or InsCode i > 6 ) );

registration

cluster shiftable Element of the Instructions of SCMPDS ;
existence
ex b₁ being Instruction of SCMPDS st b₁ is shiftable

proof end;

end;

registration

let a be Int_position ;
let k1 be Integer;
cluster a := k1 -> shiftable ;
coherence
a := k1 is shiftable

proof end;

end;

registration

let a be Int_position ;
let k1, k2 be Integer;
cluster a,k1 := k2 -> shiftable ;
coherence
a,k1 := k2 is shiftable

proof end;

end;

registration

let a be Int_position ;
let k1, k2 be Integer;
cluster AddTo a,k1,k2 -> shiftable ;
coherence
AddTo a,k1,k2 is shiftable

proof end;

end;

registration

let a, b be Int_position ;
let k1, k2 be Integer;
cluster AddTo a,k1,b,k2 -> shiftable ;
coherence
AddTo a,k1,b,k2 is shiftable

proof end;

cluster SubFrom a,k1,b,k2 -> shiftable ;
coherence
SubFrom a,k1,b,k2 is shiftable

proof end;

cluster MultBy a,k1,b,k2 -> shiftable ;
coherence
MultBy a,k1,b,k2 is shiftable

proof end;

cluster Divide a,k1,b,k2 -> shiftable ;
coherence
Divide a,k1,b,k2 is shiftable

proof end;

cluster a,k1 := b,k2 -> shiftable ;
coherence
a,k1 := b,k2 is shiftable

proof end;

end;

registration

let I, J be shiftable Program of SCMPDS ;
cluster I ';' J -> shiftable ;
coherence
I ';' J is shiftable

proof end;

end;

registration

let i be shiftable Instruction of SCMPDS ;
cluster Load i -> shiftable ;
coherence
Load i is shiftable

proof end;

end;

registration

let i be shiftable Instruction of SCMPDS ;
let J be shiftable Program of SCMPDS ;
cluster i ';' J -> shiftable ;
coherence
i ';' J is shiftable ;

end;

registration

let I be shiftable Program of SCMPDS ;
let j be shiftable Instruction of SCMPDS ;
cluster I ';' j -> shiftable ;
coherence
I ';' j is shiftable ;

end;

registration

let i, j be shiftable Instruction of SCMPDS ;
cluster i ';' j -> shiftable ;
coherence
i ';' j is shiftable ;

end;

registration

cluster Stop SCMPDS -> parahalting shiftable ;
coherence
( Stop SCMPDS is parahalting & Stop SCMPDS is shiftable ) by Lm1, Lm2;

end;

registration

let I be shiftable Program of SCMPDS ;
cluster stop I -> shiftable ;
coherence
stop I is shiftable ;

end;

theorem :: SCMPDS_4:78

for I being shiftable Program of SCMPDS
for k1 being Integer st (card I) + k1 >= 0 holds
I ';' (goto k1) is shiftable

proof end;

registration

let n be Element of NAT ;
cluster Load (goto n) -> shiftable ;
coherence
Load (goto n) is shiftable

proof end;

end;

theorem :: SCMPDS_4:79

for I being shiftable Program of SCMPDS
for k1, k2 being Integer
for a being Int_position st (card I) + k2 >= 0 holds
I ';' (a,k1 <>0_goto k2) is shiftable

proof end;

registration

let k1 be Integer;
let a be Int_position ;
let n be Element of NAT ;
cluster Load (a,k1 <>0_goto n) -> shiftable ;
coherence
Load (a,k1 <>0_goto n) is shiftable

proof end;

end;

theorem :: SCMPDS_4:80

for I being shiftable Program of SCMPDS
for k1, k2 being Integer
for a being Int_position st (card I) + k2 >= 0 holds
I ';' (a,k1 <=0_goto k2) is shiftable

proof end;

registration

let k1 be Integer;
let a be Int_position ;
let n be Element of NAT ;
cluster Load (a,k1 <=0_goto n) -> shiftable ;
coherence
Load (a,k1 <=0_goto n) is shiftable

proof end;

end;

theorem :: SCMPDS_4:81

for I being shiftable Program of SCMPDS
for k1, k2 being Integer
for a being Int_position st (card I) + k2 >= 0 holds
I ';' (a,k1 >=0_goto k2) is shiftable

proof end;

registration

let k1 be Integer;
let a be Int_position ;
let n be Element of NAT ;
cluster Load (a,k1 >=0_goto n) -> shiftable ;
coherence
Load (a,k1 >=0_goto n) is shiftable

proof end;

end;

theorem Th82: :: SCMPDS_4:82

for s1, s2 being State of SCMPDS
for n, m being Element of NAT
for k1 being Integer st IC s1 = inspos m & m + k1 >= 0 & (IC s1) + n = IC s2 holds
(ICplusConst s1,k1) + n = ICplusConst s2,k1

proof end;

theorem Th83: :: SCMPDS_4:83

for s1, s2 being State of SCMPDS
for n, m being Element of NAT
for i being Instruction of SCMPDS st IC s1 = inspos m & i valid_at m & InsCode i <> 1 & InsCode i <> 3 & (IC s1) + n = IC s2 & DataPart s1 = DataPart s2 holds
( (IC (Exec i,s1)) + n = IC (Exec i,s2) & DataPart (Exec i,s1) = DataPart (Exec i,s2) )

proof end;

theorem :: SCMPDS_4:84

for s1, s2 being State of SCMPDS
for J being parahalting shiftable Program of SCMPDS st Initialized (stop J) c= s1 holds
for n being Element of NAT st Shift (stop J),n c= s2 & IC s2 = inspos n & DataPart s1 = DataPart s2 holds
for i being Element of NAT holds
( (IC (Computation s1,i)) + n = IC (Computation s2,i) & CurInstr (Computation s1,i) = CurInstr (Computation s2,i) & DataPart (Computation s1,i) = DataPart (Computation s2,i) )

proof end;