:: SCMPDS_5 semantic presentation
:: Showing IDV graph ... (Click the Palm Trees again to close it)
theorem Th1: :: SCMPDS_5:1
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th2: :: SCMPDS_5:2
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th3: :: SCMPDS_5:3
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th4: :: SCMPDS_5:4
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th5: :: SCMPDS_5:5
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th6: :: SCMPDS_5:6
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th7: :: SCMPDS_5:7
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th8: :: SCMPDS_5:8
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th9: :: SCMPDS_5:9
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th10: :: SCMPDS_5:10
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th11: :: SCMPDS_5:11
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: SCMPDS_5:12
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th13: :: SCMPDS_5:13
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th14: :: SCMPDS_5:14
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th15: :: SCMPDS_5:15
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th16: :: SCMPDS_5:16
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th17: :: SCMPDS_5:17
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th18: :: SCMPDS_5:18
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th19: :: SCMPDS_5:19
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th20: :: SCMPDS_5:20
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th21: :: SCMPDS_5:21
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th22: :: SCMPDS_5:22
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th23: :: SCMPDS_5:23
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th24: :: SCMPDS_5:24
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
Lm1:
Load ((DataLoc 0,0) := 0) is parahalting
:: deftheorem Def1 defines No-StopCode SCMPDS_5:def 1 :
:: deftheorem Def2 defines parahalting SCMPDS_5:def 2 :
theorem :: SCMPDS_5:25
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
registration
let a,
b be
Int_position ;
let k1,
k2 be
Integer;
cluster AddTo a,
k1,
b,
k2 -> No-StopCode ;
coherence
AddTo a,k1,b,k2 is No-StopCode
cluster SubFrom a,
k1,
b,
k2 -> No-StopCode ;
coherence
SubFrom a,k1,b,k2 is No-StopCode
cluster MultBy a,
k1,
b,
k2 -> No-StopCode ;
coherence
MultBy a,k1,b,k2 is No-StopCode
cluster Divide a,
k1,
b,
k2 -> No-StopCode ;
coherence
Divide a,k1,b,k2 is No-StopCode
cluster a,
k1 := b,
k2 -> No-StopCode ;
coherence
a,k1 := b,k2 is No-StopCode
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
registration
let a,
b be
Int_position ;
let k1,
k2 be
Integer;
cluster AddTo a,
k1,
b,
k2 -> No-StopCode parahalting ;
coherence
AddTo a,k1,b,k2 is parahalting
cluster SubFrom a,
k1,
b,
k2 -> No-StopCode parahalting ;
coherence
SubFrom a,k1,b,k2 is parahalting
cluster MultBy a,
k1,
b,
k2 -> No-StopCode parahalting ;
coherence
MultBy a,k1,b,k2 is parahalting
cluster Divide a,
k1,
b,
k2 -> No-StopCode parahalting ;
coherence
Divide a,k1,b,k2 is parahalting
cluster a,
k1 := b,
k2 -> No-StopCode parahalting ;
coherence
a,k1 := b,k2 is parahalting
end;
theorem Th26: :: SCMPDS_5:26
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
:: deftheorem Def3 defines No-StopCode SCMPDS_5:def 3 :
theorem Th27: :: SCMPDS_5:27
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th28: :: SCMPDS_5:28
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th29: :: SCMPDS_5:29
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th30: :: SCMPDS_5:30
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th31: :: SCMPDS_5:31
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th32: :: SCMPDS_5:32
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th33: :: SCMPDS_5:33
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th34: :: SCMPDS_5:34
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th35: :: SCMPDS_5:35
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: SCMPDS_5:36
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
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)))) )
theorem Th37: :: SCMPDS_5:37
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th38: :: SCMPDS_5:38
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: SCMPDS_5:39
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
:: deftheorem defines Initialized SCMPDS_5:def 4 :
theorem Th40: :: SCMPDS_5:40
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th41: :: SCMPDS_5:41
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: SCMPDS_5:42
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
canceled;
theorem Th43: :: SCMPDS_5:43
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th44: :: SCMPDS_5:44
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th45: :: SCMPDS_5:45
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th46: :: SCMPDS_5:46
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: SCMPDS_5:47
:: Showing IDV graph ... (Click the Palm Tree again to close it) 