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

theorem Th1: :: SCMPDS_4:1

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

proof end;

theorem :: SCMPDS_4:2

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

proof end;

theorem Th3: :: SCMPDS_4:3

for k1, k2 being Nat st k1 <> k2 holds
DataLoc (k1,0) <> DataLoc (k2,0)

proof end;

theorem Th4: :: SCMPDS_4:4

for dl being Int_position ex i being Nat st dl = DataLoc (i,0)

proof end;

scheme :: SCMPDS_4:sch 1
SCMPDSEx{ F₁( set ) -> Integer, F₂() -> Element of NAT } :

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

proof end;

theorem :: SCMPDS_4:5

for s being State of SCMPDS holds dom s = {(IC )} \/ SCM-Data-Loc

proof end;

theorem :: SCMPDS_4:6

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

proof end;

theorem :: SCMPDS_4:7

canceled;

::$CT

theorem Th7: :: SCMPDS_4:8

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;

notation

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

end;

definition

let I, J be Program of ;

:: original: ';'
redefine func I ';' J -> Program of equals :: SCMPDS_4:def 1
I +* (Shift (J,(card I)));

compatibility
for b₁ being Program of holds
( b₁ = I ';' J iff b₁ = I +* (Shift (J,(card I))) ) by AFINSQ_1:77;
coherence
I ';' J is Program of ;

end;

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

definition

let i be Instruction of SCMPDS;
let J be Program of ;

func i ';' J -> Program of equals :: SCMPDS_4:def 2
(Load i) ';' J;

correctness
coherence
(Load i) ';' J is Program of ;
;

end;

:: deftheorem defines ';' SCMPDS_4:def 2 :
for i being Instruction of SCMPDS
for J being Program of holds i ';' J = (Load i) ';' J;

definition

let I be Program of ;
let j be Instruction of SCMPDS;

func I ';' j -> Program of equals :: SCMPDS_4:def 3
I ';' (Load j);

correctness
coherence
I ';' (Load j) is Program of ;
;

end;

:: deftheorem defines ';' SCMPDS_4:def 3 :
for I being Program of
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 equals :: SCMPDS_4:def 4
(Load i) ';' (Load j);

correctness
coherence
(Load i) ';' (Load j) is Program of ;
;

end;

:: deftheorem defines ';' SCMPDS_4:def 4 :
for i, j being Instruction of SCMPDS holds i ';' j = (Load i) ';' (Load j);

theorem :: SCMPDS_4:9

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

theorem :: SCMPDS_4:10

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

theorem :: SCMPDS_4:11

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

theorem :: SCMPDS_4:12

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

theorem :: SCMPDS_4:13

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

theorem :: SCMPDS_4:14

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

theorem :: SCMPDS_4:15

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

theorem :: SCMPDS_4:16

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

theorem :: SCMPDS_4:17

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

theorem :: SCMPDS_4:18

for a being Int_position
for l being Nat holds not a in dom (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;

definition

let I be Program of ;
let s be State of SCMPDS;
let P be Instruction-Sequence of SCMPDS;

func IExec (I,P,s) -> State of SCMPDS equals :: SCMPDS_4:def 5
Result ((P +* (stop I)),s);

coherence
Result ((P +* (stop I)),s) is State of SCMPDS ;

end;

:: deftheorem defines IExec SCMPDS_4:def 5 :
for I being Program of
for s being State of SCMPDS
for P being Instruction-Sequence of SCMPDS holds IExec (I,P,s) = Result ((P +* (stop I)),s);

definition

let I be Program of ;

attr I is paraclosed means :Def6: :: SCMPDS_4:def 6
for s being 0 -started State of SCMPDS
for n being Nat
for P being Instruction-Sequence of SCMPDS st stop I c= P holds
IC (Comput (P,s,n)) in dom (stop I);

attr I is parahalting means :: SCMPDS_4:def 7
for s being 0 -started State of SCMPDS
for P being Instruction-Sequence of SCMPDS st stop I c= P holds
P halts_on s;

end;

:: deftheorem Def6 defines paraclosed SCMPDS_4:def 6 :
for I being Program of holds
( I is paraclosed iff for s being 0 -started State of SCMPDS
for n being Nat
for P being Instruction-Sequence of SCMPDS st stop I c= P holds
IC (Comput (P,s,n)) in dom (stop I) );

:: deftheorem defines parahalting SCMPDS_4:def 7 :
for I being Program of holds
( I is parahalting iff for s being 0 -started State of SCMPDS
for P being Instruction-Sequence of SCMPDS 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 InstructionsF of SCMPDS -valued non empty V13() Function-like finite V47() V75() V145() parahalting for set ;

existence
ex b₁ being Program of st b₁ is parahalting by Lm1;

end;

theorem :: SCMPDS_4:19

canceled;

::$CT

theorem Th18: :: SCMPDS_4:20

for s being State of SCMPDS
for P, Q being Instruction-Sequence of SCMPDS st Q = P +* (((IC s),((IC s) + 1)) --> ((goto 1),(goto (- 1)))) holds
not Q halts_on s

proof end;

theorem Th19: :: SCMPDS_4:21

for n being Nat
for I being Program of
for s1, s2 being State of SCMPDS
for P1, P2 being Instruction-Sequence of SCMPDS st s1 = s2 & I c= P1 & I c= P2 & ( for m being Nat st m < n holds
IC (Comput (P2,s2,m)) in dom I ) holds
for m being Nat st m <= n holds
Comput (P1,s1,m) = Comput (P2,s2,m)

proof end;

registration

cluster Relation-like NAT -defined the InstructionsF of SCMPDS -valued non empty Function-like finite V75() parahalting -> paraclosed for set ;

coherence
for b₁ being Program of st b₁ is parahalting holds
b₁ is paraclosed

proof end;

end;

definition

let i be Instruction of SCMPDS;
let n be Nat;

pred i valid_at n means :: SCMPDS_4:def 8
( ( InsCode i = 14 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 defines valid_at SCMPDS_4:def 8 :
for i being Instruction of SCMPDS
for n being Nat holds
( i valid_at n iff ( ( InsCode i = 14 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 NAT -defined the InstructionsF of SCMPDS -valued finite Function;

attr IT is shiftable means :Def9: :: SCMPDS_4:def 9
for n being 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 Def9 defines shiftable SCMPDS_4:def 9 :
for IT being NAT -defined the InstructionsF of SCMPDS -valued finite Function holds
( IT is shiftable iff for n being 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 Th20: :: SCMPDS_4:22

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

proof end;

registration

cluster Relation-like NAT -defined the InstructionsF of SCMPDS -valued non empty V13() Function-like finite V47() V75() V145() parahalting shiftable for set ;

existence
ex b₁ being Program of st
( b₁ is parahalting & b₁ is shiftable ) by Lm1, Lm2;

end;

definition

let i be Instruction of SCMPDS;

attr i is shiftable means :Def10: :: SCMPDS_4:def 10
( InsCode i = 2 or ( InsCode i <> 14 & InsCode i > 6 ) );

end;

:: deftheorem Def10 defines shiftable SCMPDS_4:def 10 :
for i being Instruction of SCMPDS holds
( i is shiftable iff ( InsCode i = 2 or ( InsCode i <> 14 & InsCode i > 6 ) ) );

registration

cluster shiftable for Element of the InstructionsF 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 ;

end;

registration

let a be Int_position;
let k1, k2 be Integer;

cluster (a,k1) := k2 -> shiftable ;

coherence
(a,k1) := k2 is shiftable ;

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 ;

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 ;

cluster I ';' J -> shiftable for Program of ;

coherence
for b₁ being Program of st b₁ = I ';' J holds
b₁ is shiftable

proof end;

end;

registration

let i be shiftable Instruction of SCMPDS;

cluster Load -> shiftable for Program of ;

coherence
for b₁ being Program of 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 ;

cluster i ';' J -> shiftable ;

coherence
i ';' J is shiftable ;

end;

registration

let I be shiftable Program of ;
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 ;

cluster stop I -> shiftable ;

coherence
stop I is shiftable ;

end;

theorem :: SCMPDS_4:23

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

proof end;

registration

let n be Nat;

cluster Load -> shiftable for Program of ;

coherence
for b₁ being Program of st b₁ = Load (goto n) holds
b₁ is shiftable

proof end;

end;

theorem :: SCMPDS_4:24

for I being shiftable Program of
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 Nat;

cluster Load -> shiftable for Program of ;

coherence
for b₁ being Program of st b₁ = Load ((a,k1) <>0_goto n) holds
b₁ is shiftable

proof end;

end;

theorem :: SCMPDS_4:25

for I being shiftable Program of
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 Nat;

cluster Load -> shiftable for Program of ;

coherence
for b₁ being Program of st b₁ = Load ((a,k1) <=0_goto n) holds
b₁ is shiftable

proof end;

end;

theorem :: SCMPDS_4:26

for I being shiftable Program of
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 Nat;

cluster Load -> shiftable for Program of ;

coherence
for b₁ being Program of st b₁ = Load ((a,k1) >=0_goto n) holds
b₁ is shiftable

proof end;

end;

theorem Th25: :: SCMPDS_4:27

for s1, s2 being State of SCMPDS
for n, m being 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 Th26: :: SCMPDS_4:28

for s1, s2 being State of SCMPDS
for n, m being 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:29

for s2 being State of SCMPDS
for P1, P2 being Instruction-Sequence of SCMPDS
for s1 being 0 -started State of SCMPDS
for J being parahalting shiftable Program of st stop J c= P1 holds
for n being Nat st Shift ((stop J),n) c= P2 & IC s2 = n & DataPart s1 = DataPart s2 holds
for i being 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;