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


begin

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 ) = succ (IC s) )
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 Element of 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 Element of NAT st dl = DataLoc (i,0)
proof end;

scheme :: SCMPDS_4:sch 1
SCMPDSEx{ F1( set ) -> Integer, F2() -> Element of NAT } :
ex S being State of SCMPDS st
( IC S = F2() & ( for i being Element of NAT holds S . (DataLoc (i,0)) = F1(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;

theorem Th8: :: 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;

begin

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

definition
let I, J be Program of SCMPDS;
:: original: ';'
redefine func I ';' J -> Program of SCMPDS equals :: SCMPDS_4:def 1
I +* (Shift (J,(card I)));
compatibility
for b1 being Program of SCMPDS holds
( b1 = I ';' J iff b1 = I +* (Shift (J,(card I))) )
by AFINSQ_1:77;
coherence
I ';' J is Program of SCMPDS
;
end;

:: deftheorem defines ';' SCMPDS_4:def 1 :
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 2
(Load i) ';' J;
correctness
coherence
(Load i) ';' J is Program of SCMPDS
;
;
end;

:: deftheorem defines ';' SCMPDS_4:def 2 :
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 3
I ';' (Load j);
correctness
coherence
I ';' (Load j) is Program of SCMPDS
;
;
end;

:: deftheorem defines ';' SCMPDS_4:def 3 :
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 4
(Load i) ';' (Load j);
correctness
coherence
(Load i) ';' (Load j) is Program of SCMPDS
;
;
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 SCMPDS 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 SCMPDS 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 SCMPDS 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 SCMPDS 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 SCMPDS 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 SCMPDS 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 Element of 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;

begin

definition
let I be Program of SCMPDS;
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 SCMPDS
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 SCMPDS;
attr I is paraclosed means :Def6: :: SCMPDS_4:def 6
for s being 0 -started State of SCMPDS
for n being Element of 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 :Def7: :: 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 SCMPDS holds
( I is paraclosed iff for s being 0 -started State of SCMPDS
for n being Element of NAT
for P being Instruction-Sequence of SCMPDS st stop I c= P holds
IC (Comput (P,s,n)) in dom (stop I) );

:: deftheorem Def7 defines parahalting SCMPDS_4:def 7 :
for I being Program of SCMPDS 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 non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like finite V43() V71() V136() parahalting for set ;
existence
ex b1 being Program of SCMPDS st b1 is parahalting
by Lm1;
end;

theorem :: SCMPDS_4:19
canceled;

theorem Th20: :: SCMPDS_4:20
for s being State of SCMPDS
for P, Q being Instruction-Sequence of SCMPDS st Q = P +* (((IC s),(succ (IC s))) --> ((goto 1),(goto (- 1)))) holds
not Q halts_on s
proof end;

theorem Th21: :: SCMPDS_4:21
for n being Element of NAT
for I being Program of SCMPDS
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 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
Comput (P1,s1,m) = Comput (P2,s2,m)
proof end;

registration
cluster non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like finite V71() parahalting -> paraclosed for set ;
coherence
for b1 being Program of SCMPDS st b1 is parahalting holds
b1 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 :Def8: :: 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 Def8 defines valid_at SCMPDS_4:def 8 :
for i being Instruction of SCMPDS
for n being Element of 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 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 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 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 Th22: :: SCMPDS_4:22
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 non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like finite V43() V71() V136() parahalting shiftable for set ;
existence
ex b1 being Program of SCMPDS st
( b1 is parahalting & b1 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 b1 being Instruction of SCMPDS st b1 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 for Program of SCMPDS;
coherence
for b1 being Program of SCMPDS st b1 = I ';' J holds
b1 is shiftable
proof end;
end;

registration
let i be shiftable Instruction of SCMPDS;
cluster Load -> shiftable for Program of SCMPDS;
coherence
for b1 being Program of SCMPDS st b1 = Load i holds
b1 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:23
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 for Program of SCMPDS;
coherence
for b1 being Program of SCMPDS st b1 = Load (goto n) holds
b1 is shiftable
proof end;
end;

theorem :: SCMPDS_4:24
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 for Program of SCMPDS;
coherence
for b1 being Program of SCMPDS st b1 = Load ((a,k1) <>0_goto n) holds
b1 is shiftable
proof end;
end;

theorem :: SCMPDS_4:25
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 for Program of SCMPDS;
coherence
for b1 being Program of SCMPDS st b1 = Load ((a,k1) <=0_goto n) holds
b1 is shiftable
proof end;
end;

theorem :: SCMPDS_4:26
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 for Program of SCMPDS;
coherence
for b1 being Program of SCMPDS st b1 = Load ((a,k1) >=0_goto n) holds
b1 is shiftable
proof end;
end;

theorem Th27: :: SCMPDS_4:27
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 Th28: :: SCMPDS_4:28
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: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 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;