:: SCMPDS_4 semantic presentation

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

proof end;

correctness ;

end;

:: deftheorem defines Load SCMPDS_4:def 1 :

registration

let i be Instruction of SCMPDS ;
cluster Load i -> non empty ;
coherence ;

end;

theorem Th1: :: SCMPDS_4:1

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

proof end;

end;

theorem Th2: :: SCMPDS_4:2

for I, J being Program-block holds dom I misses dom (Shift J,(card I))

proof end;

theorem Th3: :: SCMPDS_4:3

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

for I, J being FinPartState of SCMPDS holds ProgramPart (I +* J) = (ProgramPart I) +* (ProgramPart J)

proof end;

theorem :: SCMPDS_4:5

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

end;

:: deftheorem defines Initialized SCMPDS_4:def 2 :

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

proof end;

theorem Th7: :: SCMPDS_4:7

for I being Program-block holds IC SCMPDS in dom (Initialized I)

proof end;

theorem :: SCMPDS_4:8

for I being Program-block holds IC (Initialized I) = inspos 0

proof end;

theorem Th9: :: SCMPDS_4:9

for I being Program-block holds I c= Initialized I

proof end;

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
s1,s2 equal_outside the Instruction-Locations of SCMPDS

proof end;

theorem :: SCMPDS_4:12

canceled;

theorem Th13: :: SCMPDS_4:13

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

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

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

for I being Program-block holds (Initialized I) | the Instruction-Locations of SCMPDS = I

proof end;

theorem Th17: :: SCMPDS_4:17

for k1, k2 being 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 Nat st dl = DataLoc i,0

proof end;

scheme :: SCMPDS_4:sch 1
SCMPDSEx{ F₁( set ) -> Instruction of SCMPDS , F₂( set ) -> Integer, F₃() -> Instruction-Location of SCMPDS } :

ex S being State of SCMPDS st
( IC S = F₃() & ( for i being Nat holds
( S . (inspos 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 SCMPDS )} \/ SCM-Data-Loc ) \/ the Instruction-Locations of SCMPDS by AMI_3:36, SCMPDS_3:5;

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 SCMPDS or x is Instruction-Location of SCMPDS )

proof end;

theorem :: SCMPDS_4:21

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

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

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

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

for s, ss being State of SCMPDS
for A being set holds (ss +* (s | A)) | A = s | A

proof end;

theorem :: SCMPDS_4:26

for I, J being Program-block holds I,J equal_outside the Instruction-Locations of SCMPDS

proof end;

theorem Th27: :: SCMPDS_4:27

for I being Program-block holds dom (Initialized I) = (dom I) \/ {(IC SCMPDS )}

proof end;

theorem Th28: :: SCMPDS_4:28

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

for I being Program-block holds (Initialized I) . (IC SCMPDS ) = inspos 0

proof end;

theorem Th30: :: SCMPDS_4:30

for I being Program-block holds not IC SCMPDS in dom I

proof end;

theorem Th31: :: SCMPDS_4:31

for I being Program-block
for a being Int_position holds not a in dom (Initialized I)

proof end;

theorem Th32: :: SCMPDS_4:32

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

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

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

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

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

proof end;

correctness ;

end;

:: deftheorem defines ';' SCMPDS_4:def 3 :

theorem Th37: :: SCMPDS_4:37

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

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

for I, J being Program-block holds dom I c= dom (I ';' J)

proof end;

theorem :: SCMPDS_4:40

for I, J being Program-block holds I c= I ';' J

proof end;

theorem :: SCMPDS_4:41

for I, J being Program-block holds I +* (I ';' J) = I ';' J

proof end;

theorem :: SCMPDS_4:42

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 ;

end;

:: deftheorem defines ';' SCMPDS_4:def 4 :

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 ;

end;

:: deftheorem defines ';' SCMPDS_4:def 5 :

definition

let i, j be Instruction of SCMPDS ;
func i ';' j -> Program-block equals :: SCMPDS_4:def 6
(Load i) ';' (Load j);
correctness ;

end;

:: deftheorem defines ';' SCMPDS_4:def 6 :

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

for I, J being Program-block holds card (I ';' J) = (card I) + (card J)

proof end;

theorem Th46: :: SCMPDS_4:46

for I, J, K being Program-block holds (I ';' J) ';' K = I ';' (J ';' K)

proof end;

theorem Th47: :: SCMPDS_4:47

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

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

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

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

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

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

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

proof end;

theorem Th54: :: SCMPDS_4:54

for n being Nat
for I being Program-block holds dom I misses dom (Start-At (inspos n))

proof end;

theorem :: SCMPDS_4:55

for I being Program-block holds Start-At (inspos 0) c= Initialized I by FUNCT_4:26;

theorem Th56: :: SCMPDS_4:56

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

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

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

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

for l1, l being Instruction-Location of SCMPDS holds not l1 in dom (Start-At l)

proof end;

theorem :: SCMPDS_4:61

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

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

proof end;

end;

definition

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

end;

:: deftheorem defines stop SCMPDS_4:def 7 :

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 by AMI_5:82;

end;

:: deftheorem defines IExec SCMPDS_4:def 8 :

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 :

:: deftheorem Def10 defines parahalting SCMPDS_4:def 10 :

Lm1: Load (halt SCMPDS ) is parahalting

proof end;

registration

cluster parahalting FinPartState of SCMPDS ;
existence by Lm1;

end;

theorem Th63: :: SCMPDS_4:63

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

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

proof end;

end;

theorem :: SCMPDS_4:64

canceled;

theorem Th65: :: SCMPDS_4:65

for s being State of SCMPDS holds IC s <> Next (IC s)

proof end;

theorem Th66: :: SCMPDS_4:66

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

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

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

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

for n being Nat holds Next (inspos n) = inspos (n + 1)

proof end;

theorem Th71: :: SCMPDS_4:71

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

proof end;

end;

theorem Th72: :: SCMPDS_4:72

dom SCMPDS-Stop = {(inspos 0)} by CQC_LANG:5;

theorem :: SCMPDS_4:73

( 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

card SCMPDS-Stop = 1

proof end;

theorem Th75: :: SCMPDS_4:75

for I being Program-block holds inspos 0 in dom (stop I)

proof end;

theorem Th76: :: SCMPDS_4:76

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 :

theorem Th77: :: SCMPDS_4:77

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 :

Lm2: Load (halt SCMPDS ) is shiftable

proof end;

registration

cluster paraclosed parahalting shiftable FinPartState of SCMPDS ;
existence 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 :

registration

cluster shiftable Element of the Instructions of SCMPDS ;
existence

proof end;

end;

registration

let a be Int_position ;
let k1 be Integer;
cluster a := k1 -> shiftable ;
coherence

proof end;

end;

registration

let a be Int_position ;
let k1, k2 be Integer;
cluster a,k1 := k2 -> shiftable ;
coherence

proof end;

end;

registration

let a be Int_position ;
let k1, k2 be Integer;
cluster AddTo a,k1,k2 -> shiftable ;
coherence

proof end;

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

proof end;

cluster MultBy a,k1,b,k2 -> shiftable ;
coherence

proof end;

cluster Divide a,k1,b,k2 -> shiftable ;
coherence

proof end;

cluster a,k1 := b,k2 -> shiftable ;
coherence

proof end;

end;

registration

let I, J be shiftable Program-block;
cluster I ';' J -> shiftable ;
coherence

proof end;

end;

registration

let i be shiftable Instruction of SCMPDS ;
cluster Load i -> non empty shiftable ;
coherence

proof end;

end;

registration

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

end;

registration

let I be shiftable Program-block;
let j be shiftable Instruction of SCMPDS ;
cluster I ';' j -> shiftable ;
coherence ;

end;

registration

let i, j be shiftable Instruction of SCMPDS ;
cluster i ';' j -> shiftable ;
coherence ;

end;

registration

cluster SCMPDS-Stop -> paraclosed parahalting shiftable ;
coherence by Lm1, Lm2;

end;

registration

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

end;

theorem :: SCMPDS_4:78

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

proof end;

end;

theorem :: SCMPDS_4:79

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

proof end;

end;

theorem :: SCMPDS_4:80

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

proof end;

end;

theorem :: SCMPDS_4:81

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

proof end;

end;

theorem Th82: :: SCMPDS_4:82

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

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

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;