:: The Construction and shiftability of Program Blocks for SCMPDS
:: by JingChao Chen
::
:: 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 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{ F1( set ) -> Integer, F2() -> Element of NAT } :
ex S being State of SCMPDS st
( IC S = F2() & ( for i being Nat holds S . (DataLoc (i,0)) = F1(i) ) )
proof end;

theorem :: SCMPDS_4:5
for s being State of SCMPDS holds dom s = {()} \/ 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 b1 being Program of holds ( b1 = I ';' J iff b1 = 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: proof end; registration existence ex b1 being Program of st b1 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
coherence
for b1 being Program of st b1 is parahalting holds
b1 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:
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
existence
ex b1 being Program of st
( b1 is parahalting & b1 is shiftable )
by ;
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
;
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
;
end;

registration
let a, b be Int_position;
let k1, k2 be Integer;
cluster AddTo (a,k1,b,k2) -> shiftable ;
coherence
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 b1 being Program of 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 ;
coherence
for b1 being Program of 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 ;
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
coherence by ;
end;

registration
let I be shiftable Program of ;
coherence ;
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 b1 being Program of st b1 = Load (goto n) holds
b1 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 b1 being Program of 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
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 b1 being Program of 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
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 b1 being Program of st b1 = Load ((a,k1) >=0_goto n) holds
b1 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;