:: SCMPDS_5 semantic presentation

theorem Th1: :: SCMPDS_5:1

for N being with_non-empty_elements set
for S being non empty non void halting IC-Ins-separated definite AMI-Struct of N
for s being State of S st s = Following s holds
for n being Nat holds (Computation s) . n = s

proof end;

theorem Th2: :: SCMPDS_5:2

for x being set
for i being Instruction of SCMPDS holds
( x in dom (Load i) iff x = inspos 0 )

proof end;

theorem Th3: :: SCMPDS_5:3

for loc being Instruction-Location of SCMPDS
for I being Program-block st loc in dom (stop I) & (stop I) . loc <> halt SCMPDS holds
loc in dom I

proof end;

theorem Th4: :: SCMPDS_5:4

for i being Instruction of SCMPDS holds
( dom (Load i) = {(inspos 0)} & (Load i) . (inspos 0) = i ) by CQC_LANG:5, CQC_LANG:6;

theorem Th5: :: SCMPDS_5:5

for i being Instruction of SCMPDS holds inspos 0 in dom (Load i)

proof end;

theorem Th6: :: SCMPDS_5:6

for i being Instruction of SCMPDS holds card (Load i) = 1

proof end;

theorem Th7: :: SCMPDS_5:7

for I being Program-block holds card (stop I) = (card I) + 1 by SCMPDS_4:45, SCMPDS_4:74;

theorem Th8: :: SCMPDS_5:8

for i being Instruction of SCMPDS holds card (stop (Load i)) = 2

proof end;

theorem Th9: :: SCMPDS_5:9

for i being Instruction of SCMPDS holds
( inspos 0 in dom (stop (Load i)) & inspos 1 in dom (stop (Load i)) )

proof end;

theorem Th10: :: SCMPDS_5:10

for i being Instruction of SCMPDS holds
( (stop (Load i)) . (inspos 0) = i & (stop (Load i)) . (inspos 1) = halt SCMPDS )

proof end;

theorem Th11: :: SCMPDS_5:11

for x being set
for i being Instruction of SCMPDS holds
( x in dom (stop (Load i)) iff ( x = inspos 0 or x = inspos 1 ) )

proof end;

theorem :: SCMPDS_5:12

for i being Instruction of SCMPDS holds dom (stop (Load i)) = {(inspos 0),(inspos 1)}

proof end;

theorem Th13: :: SCMPDS_5:13

for i being Instruction of SCMPDS holds
( inspos 0 in dom (Initialized (stop (Load i))) & inspos 1 in dom (Initialized (stop (Load i))) & (Initialized (stop (Load i))) . (inspos 0) = i & (Initialized (stop (Load i))) . (inspos 1) = halt SCMPDS )

proof end;

theorem Th14: :: SCMPDS_5:14

for I, J being Program-block holds Initialized (stop (I ';' J)) = (I ';' (J ';' SCMPDS-Stop )) +* (Start-At (inspos 0)) by SCMPDS_4:46;

theorem Th15: :: SCMPDS_5:15

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

proof end;

theorem Th16: :: SCMPDS_5:16

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

proof end;

theorem Th17: :: SCMPDS_5:17

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

proof end;

theorem Th18: :: SCMPDS_5:18

for s being State of SCMPDS
for I being Program-block st Initialized I c= s holds
IC s = inspos 0

proof end;

theorem Th19: :: SCMPDS_5:19

for a being Int_position
for s being State of SCMPDS
for I being Program-block holds (s +* (Initialized I)) . a = s . a

proof end;

theorem Th20: :: SCMPDS_5:20

for s1, s2 being State of SCMPDS
for I being parahalting Program-block st Initialized (stop I) c= s1 & Initialized (stop I) c= s2 & s1,s2 equal_outside the Instruction-Locations of SCMPDS holds
for k being Nat holds
( (Computation s1) . k,(Computation s2) . k equal_outside the Instruction-Locations of SCMPDS & CurInstr ((Computation s1) . k) = CurInstr ((Computation s2) . k) )

proof end;

theorem Th21: :: SCMPDS_5:21

for s1, s2 being State of SCMPDS
for I being parahalting Program-block st Initialized (stop I) c= s1 & Initialized (stop I) c= s2 & s1,s2 equal_outside the Instruction-Locations of SCMPDS holds
( LifeSpan s1 = LifeSpan s2 & Result s1, Result s2 equal_outside the Instruction-Locations of SCMPDS )

proof end;

theorem Th22: :: SCMPDS_5:22

for s being State of SCMPDS
for I being Program-block holds IC (IExec I,s) = IC (Result (s +* (Initialized (stop I))))

proof end;

theorem Th23: :: SCMPDS_5:23

for s being State of SCMPDS
for I being parahalting Program-block
for J being Program-block st Initialized (stop I) c= s holds
for m being Nat st m <= LifeSpan s holds
(Computation s) . m,(Computation (s +* (I ';' J))) . m equal_outside the Instruction-Locations of SCMPDS

proof end;

theorem Th24: :: SCMPDS_5:24

for s being State of SCMPDS
for I being parahalting Program-block
for J being Program-block st Initialized (stop I) c= s holds
for m being Nat st m <= LifeSpan s holds
(Computation s) . m,(Computation (s +* (Initialized (stop (I ';' J))))) . m equal_outside the Instruction-Locations of SCMPDS

proof end;

Lm1: Load ((DataLoc 0,0) := 0) is parahalting

proof end;

definition

let i be Instruction of SCMPDS ;
attr i is No-StopCode means :Def1: :: SCMPDS_5:def 1
i <> halt SCMPDS ;

end;

:: deftheorem Def1 defines No-StopCode SCMPDS_5:def 1 :

definition

let i be Instruction of SCMPDS ;
attr i is parahalting means :Def2: :: SCMPDS_5:def 2
Load i is parahalting;

end;

:: deftheorem Def2 defines parahalting SCMPDS_5:def 2 :

registration

cluster shiftable No-StopCode parahalting M2(the Instructions of SCMPDS );
existence

proof end;

end;

theorem :: SCMPDS_5:25

for k1 being Integer st k1 <> 0 holds
goto k1 is No-StopCode

proof end;

registration

let a be Int_position ;
cluster return a -> No-StopCode ;
coherence

proof end;

end;

registration

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

proof end;

cluster saveIC a,k1 -> No-StopCode ;
coherence

proof end;

end;

registration

let a be Int_position ;
let k1, k2 be Integer;
cluster a,k1 <>0_goto k2 -> No-StopCode ;
coherence

proof end;

cluster a,k1 <=0_goto k2 -> No-StopCode ;
coherence

proof end;

cluster a,k1 >=0_goto k2 -> No-StopCode ;
coherence

proof end;

cluster a,k1 := k2 -> No-StopCode ;
coherence

proof end;

end;

registration

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

proof end;

end;

registration

let a, b be Int_position ;
let k1, k2 be Integer;
cluster AddTo a,k1,b,k2 -> No-StopCode ;
coherence

proof end;

cluster SubFrom a,k1,b,k2 -> No-StopCode ;
coherence

proof end;

cluster MultBy a,k1,b,k2 -> No-StopCode ;
coherence

proof end;

cluster Divide a,k1,b,k2 -> No-StopCode ;
coherence

proof end;

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

proof end;

end;

registration

cluster halt SCMPDS -> parahalting ;
coherence

proof end;

end;

registration

let i be parahalting Instruction of SCMPDS ;
cluster Load i -> parahalting ;
coherence by Def2;

end;

Lm2: for i being Instruction of SCMPDS st ( for s being State of SCMPDS holds (Exec i,s) . (IC SCMPDS ) = Next (IC s) ) holds
Load i is parahalting

proof end;

registration

let a be Int_position ;
let k1 be Integer;
cluster a := k1 -> No-StopCode parahalting ;
coherence

proof end;

end;

registration

let a be Int_position ;
let k1, k2 be Integer;
cluster a,k1 := k2 -> No-StopCode parahalting ;
coherence

proof end;

cluster AddTo a,k1,k2 -> No-StopCode parahalting ;
coherence

proof end;

end;

registration

let a, b be Int_position ;
let k1, k2 be Integer;
cluster AddTo a,k1,b,k2 -> No-StopCode parahalting ;
coherence

proof end;

cluster SubFrom a,k1,b,k2 -> No-StopCode parahalting ;
coherence

proof end;

cluster MultBy a,k1,b,k2 -> No-StopCode parahalting ;
coherence

proof end;

cluster Divide a,k1,b,k2 -> No-StopCode parahalting ;
coherence

proof end;

cluster a,k1 := b,k2 -> No-StopCode parahalting ;
coherence

proof end;

end;

theorem Th26: :: SCMPDS_5:26

for i being Instruction of SCMPDS st InsCode i = 1 holds
not i is parahalting

proof end;

definition

let IT be FinPartState of SCMPDS ;
attr IT is No-StopCode means :Def3: :: SCMPDS_5:def 3
for x being Instruction-Location of SCMPDS st x in dom IT holds
IT . x <> halt SCMPDS ;

end;

:: deftheorem Def3 defines No-StopCode SCMPDS_5:def 3 :

registration

cluster parahalting shiftable No-StopCode FinPartState of SCMPDS ;
existence

proof end;

end;

registration

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

proof end;

end;

registration

let i be No-StopCode Instruction of SCMPDS ;
cluster Load i -> No-StopCode ;
coherence

proof end;

end;

registration

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

end;

registration

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

end;

registration

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

end;

theorem Th27: :: SCMPDS_5:27

for s being State of SCMPDS
for I being parahalting No-StopCode Program-block st Initialized (stop I) c= s holds
IC ((Computation s) . (LifeSpan (s +* (Initialized (stop I))))) = inspos (card I)

proof end;

theorem Th28: :: SCMPDS_5:28

for s being State of SCMPDS
for I being parahalting Program-block
for k being Nat st k < LifeSpan (s +* (Initialized (stop I))) holds
IC ((Computation (s +* (Initialized (stop I)))) . k) in dom I

proof end;

theorem Th29: :: SCMPDS_5:29

for s being State of SCMPDS
for I being parahalting Program-block
for k being Nat st Initialized I c= s & k <= LifeSpan (s +* (Initialized (stop I))) holds
(Computation s) . k,(Computation (s +* (Initialized (stop I)))) . k equal_outside the Instruction-Locations of SCMPDS

proof end;

theorem Th30: :: SCMPDS_5:30

for s being State of SCMPDS
for I being parahalting No-StopCode Program-block st Initialized I c= s holds
IC ((Computation s) . (LifeSpan (s +* (Initialized (stop I))))) = inspos (card I)

proof end;

theorem Th31: :: SCMPDS_5:31

for s being State of SCMPDS
for I being parahalting Program-block holds
( not Initialized I c= s or CurInstr ((Computation s) . (LifeSpan (s +* (Initialized (stop I))))) = halt SCMPDS or IC ((Computation s) . (LifeSpan (s +* (Initialized (stop I))))) = inspos (card I) )

proof end;

theorem Th32: :: SCMPDS_5:32

for s being State of SCMPDS
for I being parahalting No-StopCode Program-block
for k being Nat st Initialized I c= s & k < LifeSpan (s +* (Initialized (stop I))) holds
CurInstr ((Computation s) . k) <> halt SCMPDS

proof end;

theorem Th33: :: SCMPDS_5:33

for s being State of SCMPDS
for I being parahalting Program-block
for J being Program-block
for k being Nat st k <= LifeSpan (s +* (Initialized (stop I))) holds
(Computation (s +* (Initialized (stop I)))) . k,(Computation (s +* ((I ';' J) +* (Start-At (inspos 0))))) . k equal_outside the Instruction-Locations of SCMPDS

proof end;

theorem Th34: :: SCMPDS_5:34

for s being State of SCMPDS
for I being parahalting Program-block
for J being Program-block
for k being Nat st k <= LifeSpan (s +* (Initialized (stop I))) holds
(Computation (s +* (Initialized (stop I)))) . k,(Computation (s +* (Initialized (stop (I ';' J))))) . k equal_outside the Instruction-Locations of SCMPDS

proof end;

registration

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

proof end;

end;

registration

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

end;

registration

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

end;

registration

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

end;

theorem Th35: :: SCMPDS_5:35

for m, n being Nat
for s, s1 being State of SCMPDS
for J being parahalting shiftable Program-block st s = (Computation (s1 +* (Initialized (stop J)))) . m holds
Exec (CurInstr s),(s +* (Start-At ((IC s) + n))) = (Following s) +* (Start-At ((IC (Following s)) + n))

proof end;

theorem :: SCMPDS_5:36

for s being State of SCMPDS
for I being parahalting No-StopCode Program-block
for J being parahalting shiftable Program-block
for k being Nat st Initialized (stop (I ';' J)) c= s holds
((Computation ((Result (s +* (Initialized (stop I)))) +* (Initialized (stop J)))) . k) +* (Start-At ((IC ((Computation ((Result (s +* (Initialized (stop I)))) +* (Initialized (stop J)))) . k)) + (card I))),(Computation (s +* (Initialized (stop (I ';' J))))) . ((LifeSpan (s +* (Initialized (stop I)))) + k) equal_outside the Instruction-Locations of SCMPDS

proof end;

Lm3: for I being parahalting No-StopCode Program-block
for J being parahalting shiftable Program-block
for s, s1 being State of SCMPDS st Initialized (stop (I ';' J)) c= s & s1 = s +* (Initialized (stop I)) holds
( IC ((Computation s) . (LifeSpan s1)) = inspos (card I) & ((Computation s) . (LifeSpan s1)) | SCM-Data-Loc = (((Computation s1) . (LifeSpan s1)) +* (Initialized (stop J))) | SCM-Data-Loc & Shift (stop J),(card I) c= (Computation s) . (LifeSpan s1) & LifeSpan s = (LifeSpan s1) + (LifeSpan ((Result s1) +* (Initialized (stop J)))) )

proof end;

theorem Th37: :: SCMPDS_5:37

for s being State of SCMPDS
for I being parahalting No-StopCode Program-block
for J being parahalting shiftable Program-block holds LifeSpan (s +* (Initialized (stop (I ';' J)))) = (LifeSpan (s +* (Initialized (stop I)))) + (LifeSpan ((Result (s +* (Initialized (stop I)))) +* (Initialized (stop J))))

proof end;

theorem Th38: :: SCMPDS_5:38

for s being State of SCMPDS
for I being parahalting No-StopCode Program-block
for J being parahalting shiftable Program-block holds IExec (I ';' J),s = (IExec J,(IExec I,s)) +* (Start-At ((IC (IExec J,(IExec I,s))) + (card I)))

proof end;

theorem :: SCMPDS_5:39

for a being Int_position
for s being State of SCMPDS
for I being parahalting No-StopCode Program-block
for J being parahalting shiftable Program-block holds (IExec (I ';' J),s) . a = (IExec J,(IExec I,s)) . a

proof end;

definition

let s be State of SCMPDS ;
func Initialized s -> State of SCMPDS equals :: SCMPDS_5:def 4
s +* (Start-At (inspos 0));
coherence ;

end;

:: deftheorem defines Initialized SCMPDS_5:def 4 :

theorem Th40: :: SCMPDS_5:40

for a being Int_position
for s being State of SCMPDS
for loc being Instruction-Location of SCMPDS holds
( IC (Initialized s) = inspos 0 & (Initialized s) . a = s . a & (Initialized s) . loc = s . loc )

proof end;

theorem Th41: :: SCMPDS_5:41

for s1, s2 being State of SCMPDS holds
( s1,s2 equal_outside the Instruction-Locations of SCMPDS iff s1 | (SCM-Data-Loc \/ {(IC SCMPDS )}) = s2 | (SCM-Data-Loc \/ {(IC SCMPDS )}) )

proof end;

theorem :: SCMPDS_5:42

canceled;

theorem Th43: :: SCMPDS_5:43

for i being Instruction of SCMPDS
for s1, s2 being State of SCMPDS st s1 | SCM-Data-Loc = s2 | SCM-Data-Loc & InsCode i <> 3 holds
(Exec i,s1) | SCM-Data-Loc = (Exec i,s2) | SCM-Data-Loc

proof end;

theorem Th44: :: SCMPDS_5:44

for s1, s2 being State of SCMPDS
for i being shiftable Instruction of SCMPDS st s1 | SCM-Data-Loc = s2 | SCM-Data-Loc holds
(Exec i,s1) | SCM-Data-Loc = (Exec i,s2) | SCM-Data-Loc

proof end;

theorem Th45: :: SCMPDS_5:45

for s being State of SCMPDS
for i being parahalting Instruction of SCMPDS holds Exec i,(Initialized s) = IExec (Load i),s

proof end;

theorem Th46: :: SCMPDS_5:46

for a being Int_position
for s being State of SCMPDS
for I being parahalting No-StopCode Program-block
for j being shiftable parahalting Instruction of SCMPDS holds (IExec (I ';' j),s) . a = (Exec j,(IExec I,s)) . a

proof end;

theorem :: SCMPDS_5:47

for a being Int_position
for s being State of SCMPDS
for i being No-StopCode parahalting Instruction of SCMPDS
for j being shiftable parahalting Instruction of SCMPDS holds (IExec (i ';' j),s) . a = (Exec j,(Exec i,(Initialized s))) . a

proof end;