:: SCMPDS_4 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

definition
mode Program-block is programmed initial FinPartState of SCMPDS ;
end;

definition
let i be Instruction of SCMPDS ;
func Load i -> Program-block equals :: SCMPDS_4:def 1
(inspos 0) .--> i;
coherence
(inspos 0) .--> i is Program-block
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for P being Program-block
for n being Nat holds
( n < card P iff inspos n in dom P )
proof end;

registration
let I be initial FinPartState of SCMPDS ;
cluster ProgramPart I -> initial ;
coherence
ProgramPart I is initial
proof end;
end;

theorem Th2: :: SCMPDS_4:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I, J being Program-block holds dom I misses dom (Shift J,(card I))
proof end;

theorem Th3: :: SCMPDS_4:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for m being Nat
for I being programmed FinPartState of SCMPDS holds card (Shift I,m) = card I
proof end;

theorem Th4: :: SCMPDS_4:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I, J being FinPartState of SCMPDS holds ProgramPart (I +* J) = (ProgramPart I) +* (ProgramPart J)
proof end;

theorem :: SCMPDS_4:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for I, J being FinPartState of SCMPDS holds Shift (ProgramPart (I +* J)),n = (Shift (ProgramPart I),n) +* (Shift (ProgramPart J),n)
proof end;

definition
let I be Program-block;
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-block holds Initialized I = I +* (Start-At (inspos 0));

theorem Th6: :: SCMPDS_4:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being Program-block holds IC SCMPDS in dom (Initialized I)
proof end;

theorem :: SCMPDS_4:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being Program-block holds IC (Initialized I) = inspos 0
proof end;

theorem Th9: :: SCMPDS_4:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being Program-block holds I c= Initialized I
proof end;

theorem :: SCMPDS_4:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th11: :: SCMPDS_4:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 the Instruction-Locations of SCMPDS
proof end;

theorem :: SCMPDS_4:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th13: :: SCMPDS_4:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s1, s2 being State of SCMPDS st s1,s2 equal_outside the Instruction-Locations of SCMPDS holds
for a being Int_position holds s1 . a = s2 . a
proof end;

theorem Th14: :: SCMPDS_4:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being Int_position
for s1, s2 being State of SCMPDS
for k1 being Integer st s1,s2 equal_outside the Instruction-Locations of SCMPDS holds
s1 . (DataLoc (s1 . a),k1) = s2 . (DataLoc (s2 . a),k1)
proof end;

theorem Th15: :: SCMPDS_4:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i being Instruction of SCMPDS
for s1, s2 being State of SCMPDS st s1,s2 equal_outside the Instruction-Locations of SCMPDS holds
Exec i,s1, Exec i,s2 equal_outside the Instruction-Locations of SCMPDS
proof end;

theorem :: SCMPDS_4:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being Program-block holds (Initialized I) | the Instruction-Locations of SCMPDS = I
proof end;

theorem Th17: :: SCMPDS_4:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for k1, k2 being Nat st k1 <> k2 holds
DataLoc k1,0 <> DataLoc k2,0
proof end;

theorem Th18: :: SCMPDS_4:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for dl being Int_position ex i being Nat st dl = DataLoc i,0
proof end;

scheme :: SCMPDS_4:sch 1
SCMPDSEx{ F1( set ) -> Instruction of SCMPDS , F2( set ) -> Integer, F3() -> Instruction-Location of SCMPDS } :
ex S being State of SCMPDS st
( IC S = F3() & ( for i being Nat holds
( S . (inspos i) = F1(i) & S . (DataLoc i,0) = F2(i) ) ) )
proof end;

theorem :: SCMPDS_4:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s being State of SCMPDS holds dom s = ({(IC SCMPDS )} \/ SCM-Data-Loc ) \/ the Instruction-Locations of SCMPDS by AMI_3:36, SCMPDS_3:5;

theorem :: SCMPDS_4:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s1, s2 being State of SCMPDS holds
( ( for l being Instruction-Location of SCMPDS holds s1 . l = s2 . l ) iff s1 | the Instruction-Locations of SCMPDS = s2 | the Instruction-Locations of SCMPDS )
proof end;

theorem :: SCMPDS_4:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i being Instruction-Location of SCMPDS holds not i in SCM-Data-Loc by SCMPDS_2:10, XBOOLE_0:3;

theorem Th23: :: SCMPDS_4:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s1, s2 being State of SCMPDS holds
( ( for a being Int_position holds s1 . a = s2 . a ) iff s1 | SCM-Data-Loc = s2 | SCM-Data-Loc )
proof end;

theorem :: SCMPDS_4:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s1, s2 being State of SCMPDS st s1,s2 equal_outside the Instruction-Locations of SCMPDS holds
s1 | SCM-Data-Loc = s2 | SCM-Data-Loc
proof end;

theorem :: SCMPDS_4:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s, ss being State of SCMPDS
for A being set holds (ss +* (s | A)) | A = s | A
proof end;

theorem :: SCMPDS_4:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I, J being Program-block holds I,J equal_outside the Instruction-Locations of SCMPDS
proof end;

theorem Th27: :: SCMPDS_4:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being Program-block holds dom (Initialized I) = (dom I) \/ {(IC SCMPDS )}
proof end;

theorem Th28: :: SCMPDS_4:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being Program-block
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being Program-block holds (Initialized I) . (IC SCMPDS ) = inspos 0
proof end;

theorem Th30: :: SCMPDS_4:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being Program-block holds not IC SCMPDS in dom I
proof end;

theorem Th31: :: SCMPDS_4:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being Program-block
for a being Int_position holds not a in dom (Initialized I)
proof end;

theorem Th32: :: SCMPDS_4:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for I being Program-block
for x being set st x in dom I holds
I . x = (I +* (Start-At (inspos n))) . x
proof end;

theorem Th33: :: SCMPDS_4:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being Program-block
for x being set st x in dom I holds
I . x = (Initialized I) . x by Th32;

theorem Th34: :: SCMPDS_4:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I, J being Program-block
for s being State of SCMPDS st Initialized J c= s holds
s +* (Initialized I) = s +* I
proof end;

theorem :: SCMPDS_4:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I, J being Program-block
for s being State of SCMPDS st Initialized J c= s holds
Initialized I c= s +* I
proof end;

theorem :: SCMPDS_4:36  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I, J being Program-block
for s being State of SCMPDS holds s +* (Initialized I),s +* (Initialized J) equal_outside the Instruction-Locations of SCMPDS
proof end;

definition
let I, J be Program-block;
func I ';' J -> Program-block equals :: SCMPDS_4:def 3
I +* (Shift J,(card I));
coherence
I +* (Shift J,(card I)) is Program-block
proof end;
correctness
;
end;

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

theorem Th37: :: SCMPDS_4:37  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I, J being Program-block
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I, J being Program-block
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I, J being Program-block holds dom I c= dom (I ';' J)
proof end;

theorem :: SCMPDS_4:40  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I, J being Program-block holds I c= I ';' J
proof end;

theorem :: SCMPDS_4:41  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I, J being Program-block holds I +* (I ';' J) = I ';' J
proof end;

theorem :: SCMPDS_4:42  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I, J being Program-block holds (Initialized I) +* (I ';' J) = Initialized (I ';' J)
proof end;

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

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

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

:: deftheorem defines ';' SCMPDS_4:def 5 :
for I being Program-block
for j being Instruction of SCMPDS holds I ';' j = I ';' (Load j);

definition
let i, j be Instruction of SCMPDS ;
func i ';' j -> Program-block equals :: SCMPDS_4:def 6
(Load i) ';' (Load j);
correctness
coherence
(Load i) ';' (Load j) is Program-block
;
;
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i, j being Instruction of SCMPDS holds i ';' j = (Load i) ';' j ;

theorem :: SCMPDS_4:44  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i, j being Instruction of SCMPDS holds i ';' j = i ';' (Load j) ;

theorem Th45: :: SCMPDS_4:45  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I, J being Program-block holds card (I ';' J) = (card I) + (card J)
proof end;

theorem Th46: :: SCMPDS_4:46  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I, J, K being Program-block holds (I ';' J) ';' K = I ';' (J ';' K)
proof end;

theorem Th47: :: SCMPDS_4:47  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for k being Instruction of SCMPDS
for I, J being Program-block holds (I ';' J) ';' k = I ';' (J ';' k) by Th46;

theorem :: SCMPDS_4:48  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for j being Instruction of SCMPDS
for I, K being Program-block holds (I ';' j) ';' K = I ';' (j ';' K) by Th46;

theorem :: SCMPDS_4:49  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for j, k being Instruction of SCMPDS
for I being Program-block holds (I ';' j) ';' k = I ';' (j ';' k)
proof end;

theorem Th50: :: SCMPDS_4:50  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i being Instruction of SCMPDS
for J, K being Program-block holds (i ';' J) ';' K = i ';' (J ';' K) by Th46;

theorem :: SCMPDS_4:51  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i, k being Instruction of SCMPDS
for J being Program-block holds (i ';' J) ';' k = i ';' (J ';' k) by Th47;

theorem Th52: :: SCMPDS_4:52  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i, j being Instruction of SCMPDS
for K being Program-block holds (i ';' j) ';' K = i ';' (j ';' K)
proof end;

theorem :: SCMPDS_4:53  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i, j, k being Instruction of SCMPDS holds (i ';' j) ';' k = i ';' (j ';' k)
proof end;

theorem Th54: :: SCMPDS_4:54  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for I being Program-block holds dom I misses dom (Start-At (inspos n))
proof end;

theorem :: SCMPDS_4:55  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being Program-block holds Start-At (inspos 0) c= Initialized I by FUNCT_4:26;

theorem Th56: :: SCMPDS_4:56  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for I being Program-block
for s being State of SCMPDS st I +* (Start-At (inspos n)) c= s holds
I c= s
proof end;

theorem :: SCMPDS_4:57  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being Program-block
for s being State of SCMPDS st Initialized I c= s holds
I c= s by Th56;

theorem Th58: :: SCMPDS_4:58  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for I being Program-block holds (I +* (Start-At (inspos n))) | the Instruction-Locations of SCMPDS = I
proof end;

theorem Th59: :: SCMPDS_4:59  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for l1, l being Instruction-Location of SCMPDS holds not l1 in dom (Start-At l)
proof end;

theorem :: SCMPDS_4:61  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being Program-block
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being Program-block
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;

definition
let I be Program-block;
func stop I -> Program-block equals :: SCMPDS_4:def 7
I ';' SCMPDS-Stop ;
coherence
I ';' SCMPDS-Stop is Program-block
;
end;

:: deftheorem defines stop SCMPDS_4:def 7 :
for I being Program-block holds stop I = I ';' SCMPDS-Stop ;

definition
let I be Program-block;
let s be State of SCMPDS ;
func IExec I,s -> State of SCMPDS equals :: SCMPDS_4:def 8
(Result (s +* (Initialized (stop I)))) +* (s | the Instruction-Locations of SCMPDS );
coherence
(Result (s +* (Initialized (stop I)))) +* (s | the Instruction-Locations of SCMPDS ) is State of SCMPDS
by AMI_5:82;
end;

:: deftheorem defines IExec SCMPDS_4:def 8 :
for I being Program-block
for s being State of SCMPDS holds IExec I,s = (Result (s +* (Initialized (stop I)))) +* (s | the Instruction-Locations of SCMPDS );

definition
let I be Program-block;
attr I is paraclosed means :Def9: :: SCMPDS_4:def 9
for s being State of SCMPDS
for n being 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-block holds
( I is paraclosed iff for s being State of SCMPDS
for n being 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-block holds
( I is parahalting iff Initialized (stop I) is halting );

Lm1: Load (halt SCMPDS ) is parahalting
proof end;

registration
cluster parahalting FinPartState of SCMPDS ;
existence
ex b1 being Program-block st b1 is parahalting
by Lm1;
end;

theorem Th63: :: SCMPDS_4:63  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s being State of SCMPDS
for I being parahalting Program-block st Initialized (stop I) c= s holds
s is halting
proof end;

registration
let I be parahalting Program-block;
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th65: :: SCMPDS_4:65  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s being State of SCMPDS holds IC s <> Next (IC s)
proof end;

theorem Th66: :: SCMPDS_4:66  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s2 being State of SCMPDS holds not s2 +* ((IC s2),(Next (IC s2)) --> (goto 1),(goto (- 1))) is halting
proof end;

theorem Th67: :: SCMPDS_4:67  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for I being Program-block
for s1, s2 being State of SCMPDS st s1,s2 equal_outside the Instruction-Locations of SCMPDS & I c= s1 & I c= s2 & ( for m being Nat st m < n holds
IC ((Computation s2) . m) in dom I ) holds
for m being Nat st m <= n holds
(Computation s1) . m,(Computation s2) . m equal_outside the Instruction-Locations of SCMPDS
proof end;

theorem Th68: :: SCMPDS_4:68  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th70: :: SCMPDS_4:70  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat holds Next (inspos n) = inspos (n + 1)
proof end;

theorem Th71: :: SCMPDS_4:71  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being Program-block
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 FinPartState of SCMPDS ;
coherence
for b1 being Program-block st b1 is parahalting holds
b1 is paraclosed
proof end;
end;

theorem Th72: :: SCMPDS_4:72  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
dom SCMPDS-Stop = {(inspos 0)} by CQC_LANG:5;

theorem :: SCMPDS_4:73  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
( inspos 0 in dom SCMPDS-Stop & SCMPDS-Stop . (inspos 0) = halt SCMPDS ) by Th72, CQC_LANG:6, TARSKI:def 1;

theorem Th74: :: SCMPDS_4:74  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
card SCMPDS-Stop = 1
proof end;

theorem Th75: :: SCMPDS_4:75  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being Program-block holds inspos 0 in dom (stop I)
proof end;

theorem Th76: :: SCMPDS_4:76  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being programmed FinPartState of SCMPDS
for k being Nat
for il being Instruction-Location of SCMPDS st il in dom p holds
il + k in dom (Shift p,k)
proof end;

definition
let i be Instruction of SCMPDS ;
let n be 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 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 Th77: :: SCMPDS_4:77  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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;

definition
let IT be FinPartState of SCMPDS ;
attr IT is shiftable means :Def12: :: SCMPDS_4:def 12
for n being 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 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 paraclosed parahalting shiftable FinPartState of SCMPDS ;
existence
ex b1 being Program-block st
( b1 is parahalting & b1 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 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-block;
cluster I ';' J -> shiftable ;
coherence
I ';' J is shiftable
proof end;
end;

registration
let i be shiftable Instruction of SCMPDS ;
cluster Load i -> non empty shiftable ;
coherence
Load i is shiftable
proof end;
end;

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

registration
let I be shiftable Program-block;
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 SCMPDS-Stop -> paraclosed parahalting shiftable ;
coherence
( SCMPDS-Stop is parahalting & SCMPDS-Stop is shiftable )
by Lm1, Lm2;
end;

registration
let I be shiftable Program-block;
cluster stop I -> shiftable ;
coherence
stop I is shiftable
;
end;

theorem :: SCMPDS_4:78  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being shiftable Program-block
for k1 being Integer st (card I) + k1 >= 0 holds
I ';' (goto k1) is shiftable
proof end;

registration
let n be Nat;
cluster Load (goto n) -> non empty shiftable ;
coherence
Load (goto n) is shiftable
proof end;
end;

theorem :: SCMPDS_4:79  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being shiftable Program-block
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 (a,k1 <>0_goto n) -> non empty shiftable ;
coherence
Load (a,k1 <>0_goto n) is shiftable
proof end;
end;

theorem :: SCMPDS_4:80  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being shiftable Program-block
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 (a,k1 <=0_goto n) -> non empty shiftable ;
coherence
Load (a,k1 <=0_goto n) is shiftable
proof end;
end;

theorem :: SCMPDS_4:81  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being shiftable Program-block
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 (a,k1 >=0_goto n) -> non empty shiftable ;
coherence
Load (a,k1 >=0_goto n) is shiftable
proof end;
end;

theorem Th82: :: SCMPDS_4:82  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s1, s2 being State of SCMPDS
for n, m being 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s1, s2 being State of SCMPDS
for n, m being 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 & s1 | SCM-Data-Loc = s2 | SCM-Data-Loc holds
( (IC (Exec i,s1)) + n = IC (Exec i,s2) & (Exec i,s1) | SCM-Data-Loc = (Exec i,s2) | SCM-Data-Loc )
proof end;

theorem :: SCMPDS_4:84  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s1, s2 being State of SCMPDS
for J being parahalting shiftable Program-block st Initialized (stop J) c= s1 holds
for n being Nat st Shift (stop J),n c= s2 & IC s2 = inspos n & s1 | SCM-Data-Loc = s2 | SCM-Data-Loc holds
for i being Nat holds
( (IC ((Computation s1) . i)) + n = IC ((Computation s2) . i) & CurInstr ((Computation s1) . i) = CurInstr ((Computation s2) . i) & ((Computation s1) . i) | SCM-Data-Loc = ((Computation s2) . i) | SCM-Data-Loc )
proof end;