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

begin

theorem :: SCMPDS_4:1

canceled;

theorem :: SCMPDS_4:2

canceled;

theorem :: SCMPDS_4:3

canceled;

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 ) = succ (IC s) )

proof end;

theorem :: SCMPDS_4:7

canceled;

theorem :: SCMPDS_4:8

canceled;

theorem :: SCMPDS_4:9

canceled;

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
NPP s1 = NPP s2

proof end;

theorem :: SCMPDS_4:12

canceled;

theorem Th13: :: SCMPDS_4:13

for s1, s2 being State of SCMPDS st NPP s1 = NPP s2 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 NPP s1 = NPP s2 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 NPP s1 = NPP s2 holds
NPP (Exec (i,s1)) = NPP (Exec (i,s2))

proof end;

registration

cluster SCMPDS -> Exec-preserving ;
coherence
SCMPDS is Exec-preserving

proof end;

end;

theorem :: SCMPDS_4:16

canceled;

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₃() -> Element of NAT } :

ex S being State of SCMPDS st
( IC S = F₃() & ( for i being Element of NAT holds
( S . 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 )} \/ SCM-Data-Loc) \/ NAT

proof end;

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 or x is Element of NAT )

proof end;

theorem :: SCMPDS_4:21

canceled;

theorem :: SCMPDS_4:22

for i being Element of NAT holds not i in SCM-Data-Loc by AMI_2:29, XBOOLE_0:3;

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

canceled;

theorem :: SCMPDS_4:25

canceled;

theorem :: SCMPDS_4:26

canceled;

theorem :: SCMPDS_4:27

canceled;

theorem :: SCMPDS_4:28

canceled;

theorem :: SCMPDS_4:29

canceled;

theorem :: SCMPDS_4:30

canceled;

theorem :: SCMPDS_4:31

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

proof end;

begin

notation

let I, J be Program of SCMPDS;
synonym I ';' J for I ^ J;

end;

definition

canceled;
canceled;
let I, J be Program of SCMPDS;
:: original: ';'
redefine func I ';' J -> Program of SCMPDS equals :: SCMPDS_4:def 3
I +* (Shift (J,(card I)));
compatibility
for b₁ being Program of SCMPDS holds
( b₁ = I ';' J iff b₁ = I +* (Shift (J,(card I))) ) by AFINSQ_1:81;
coherence
I ';' J is Program of SCMPDS ;

end;

:: deftheorem SCMPDS_4:def 1 :
canceled;

:: deftheorem SCMPDS_4:def 2 :
canceled;

:: deftheorem defines ';' SCMPDS_4:def 3 :
for I, J being Program of SCMPDS holds I ';' J = I +* (Shift (J,(card I)));

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:32

canceled;

theorem :: SCMPDS_4:33

canceled;

theorem :: SCMPDS_4:34

canceled;

theorem :: SCMPDS_4:35

canceled;

theorem :: SCMPDS_4:36

canceled;

theorem :: SCMPDS_4:37

canceled;

theorem :: SCMPDS_4:38

canceled;

theorem :: SCMPDS_4:39

canceled;

theorem :: SCMPDS_4:40

canceled;

theorem :: SCMPDS_4:41

canceled;

theorem :: SCMPDS_4:42

canceled;

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 :: SCMPDS_4:45

canceled;

theorem :: SCMPDS_4:46

canceled;

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 AFINSQ_1:30;

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 AFINSQ_1:30;

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 AFINSQ_1:30;

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 AFINSQ_1:30;

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 AFINSQ_1:30;

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 AFINSQ_1:30;

theorem :: SCMPDS_4:53

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

theorem :: SCMPDS_4:54

canceled;

theorem :: SCMPDS_4:55

canceled;

theorem :: SCMPDS_4:56

canceled;

theorem :: SCMPDS_4:57

canceled;

theorem :: SCMPDS_4:58

canceled;

theorem Th59: :: SCMPDS_4:59

for a being Int_position
for l being Element of NAT holds not a in dom (Start-At (l,SCMPDS))

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 Element of NAT holds not a in dom (I +* (Start-At (l,SCMPDS)))

proof end;

definition

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

proof end;

end;

begin

registration

let s be State of SCMPDS;
cluster Initialize s -> total ;
coherence
Initialize s is total ;

end;

definition

canceled;
let I be Program of SCMPDS;
let s be State of SCMPDS;
let P be the Instructions of SCMPDS -valued ManySortedSet of NAT ;
func IExec (I,P,s) -> State of SCMPDS equals :: SCMPDS_4:def 8
(Result ((P +* (stop I)),(Initialize s))) +* (s | NAT);
coherence
(Result ((P +* (stop I)),(Initialize s))) +* (s | NAT) is State of SCMPDS ;

end;

:: deftheorem SCMPDS_4:def 7 :
canceled;

:: deftheorem defines IExec SCMPDS_4:def 8 :
for I being Program of SCMPDS
for s being State of SCMPDS
for P being the Instructions of SCMPDS -valued ManySortedSet of NAT holds IExec (I,P,s) = (Result ((P +* (stop I)),(Initialize s))) +* (s | NAT);

definition

let I be Program of SCMPDS;
attr I is paraclosed means :Def9: :: SCMPDS_4:def 9
for s being 0 -started State of SCMPDS
for n being Element of NAT
for P being the Instructions of SCMPDS -valued ManySortedSet of NAT st stop I c= P holds
IC (Comput (P,s,n)) in dom (stop I);
attr I is parahalting means :Def10: :: SCMPDS_4:def 10
for s being 0 -started State of SCMPDS
for P being the Instructions of SCMPDS -valued ManySortedSet of NAT st stop I c= P holds
P halts_on s;

end;

:: deftheorem Def9 defines paraclosed SCMPDS_4:def 9 :
for I being Program of SCMPDS holds
( I is paraclosed iff for s being 0 -started State of SCMPDS
for n being Element of NAT
for P being the Instructions of SCMPDS -valued ManySortedSet of NAT st stop I c= P holds
IC (Comput (P,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 for s being 0 -started State of SCMPDS
for P being the Instructions of SCMPDS -valued ManySortedSet of NAT st stop I c= P holds
P halts_on s );

Lm1: Load (halt SCMPDS) is parahalting

proof end;

registration

cluster Relation-like NAT -defined the carrier of SCMPDS -defined the Instructions of SCMPDS -valued V10() non empty Function-like the Object-Kind of SCMPDS -compatible V32() V68() V131() parahalting set ;
existence
ex b₁ being Program of SCMPDS st b₁ is parahalting by Lm1;

end;

definition

let la, lb be Element of NAT ;
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:62

canceled;

theorem :: SCMPDS_4:63

canceled;

theorem :: SCMPDS_4:64

canceled;

theorem :: SCMPDS_4:65

canceled;

theorem Th66: :: SCMPDS_4:66

for s being State of SCMPDS
for P, Q being the Instructions of SCMPDS -valued ManySortedSet of NAT st Q = P +* (((IC s),(succ (IC s))) --> ((goto 1),(goto (- 1)))) holds
not Q halts_on s

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
for P1, P2 being the Instructions of SCMPDS -valued ManySortedSet of NAT st NPP s1 = NPP s2 & I c= P1 & I c= P2 & ( for m being Element of NAT st m < n holds
IC (Comput (P2,s2,m)) in dom I ) holds
for m being Element of NAT st m <= n holds
NPP (Comput (P1,s1,m)) = NPP (Comput (P2,s2,m))

proof end;

registration

cluster Relation-like NAT -defined the carrier of SCMPDS -defined the Instructions of SCMPDS -valued non empty Function-like the Object-Kind of SCMPDS -compatible V32() V68() parahalting -> paraclosed set ;
coherence
for b₁ being Program of SCMPDS st b₁ is parahalting holds
b₁ is paraclosed

proof end;

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 ) ) ) );

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 n in dom IT & i = IT . 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 n in dom IT & i = IT . n holds
( InsCode i <> 1 & InsCode i <> 3 & i valid_at n ) );

Lm2: Load (halt SCMPDS) is shiftable

proof end;

theorem :: SCMPDS_4:68

canceled;

theorem :: SCMPDS_4:69

canceled;

theorem :: SCMPDS_4:70

canceled;

theorem :: SCMPDS_4:71

canceled;

theorem :: SCMPDS_4:72

canceled;

theorem :: SCMPDS_4:73

canceled;

theorem :: SCMPDS_4:74

canceled;

theorem :: SCMPDS_4:75

canceled;

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;

registration

cluster Relation-like NAT -defined the carrier of SCMPDS -defined the Instructions of SCMPDS -valued V10() non empty Function-like the Object-Kind of SCMPDS -compatible V32() V68() V131() parahalting shiftable set ;
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 Exec-preserving 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 Program of SCMPDS;
coherence
for b₁ being Program of SCMPDS st b₁ = I ';' J holds
b₁ is shiftable

proof end;

end;

registration

let i be shiftable Instruction of SCMPDS;
cluster Load -> shiftable Program of SCMPDS;
coherence
for b₁ being Program of SCMPDS st b₁ = Load i holds
b₁ 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 -> shiftable Program of SCMPDS;
coherence
for b₁ being Program of SCMPDS st b₁ = Load (goto n) holds
b₁ 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 -> shiftable Program of SCMPDS;
coherence
for b₁ being Program of SCMPDS st b₁ = Load ((a,k1) <>0_goto n) holds
b₁ 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 -> shiftable Program of SCMPDS;
coherence
for b₁ being Program of SCMPDS st b₁ = Load ((a,k1) <=0_goto n) holds
b₁ 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 -> shiftable Program of SCMPDS;
coherence
for b₁ being Program of SCMPDS st b₁ = Load ((a,k1) >=0_goto n) holds
b₁ 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 = 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 = 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 s2 being State of SCMPDS
for P1, P2 being the Instructions of SCMPDS -valued ManySortedSet of NAT
for s1 being 0 -started State of SCMPDS
for J being parahalting shiftable Program of SCMPDS st stop J c= P1 holds
for n being Element of NAT st Shift ((stop J),n) c= P2 & IC s2 = n & DataPart s1 = DataPart s2 holds
for i being Element of NAT holds
( (IC (Comput (P1,s1,i))) + n = IC (Comput (P2,s2,i)) & CurInstr (P1,(Comput (P1,s1,i))) = CurInstr (P2,(Comput (P2,s2,i))) & DataPart (Comput (P1,s1,i)) = DataPart (Comput (P2,s2,i)) )

proof end;