:: Computation of Two Consecutive Program Blocks for SCMPDS
:: by JingChao Chen
::
:: Received June 15, 1999
:: Copyright (c) 1999 Association of Mizar Users
theorem :: SCMPDS_5:1
canceled;
theorem Th2: :: SCMPDS_5:2
theorem Th3: :: SCMPDS_5:3
theorem :: SCMPDS_5:4
theorem Th5: :: SCMPDS_5:5
theorem Th6: :: SCMPDS_5:6
theorem :: SCMPDS_5:7
theorem Th8: :: SCMPDS_5:8
theorem Th9: :: SCMPDS_5:9
theorem Th10: :: SCMPDS_5:10
theorem Th11: :: SCMPDS_5:11
theorem :: SCMPDS_5:12
theorem Th13: :: SCMPDS_5:13
theorem :: SCMPDS_5:14
canceled;
theorem Th15: :: SCMPDS_5:15
theorem Th16: :: SCMPDS_5:16
theorem Th17: :: SCMPDS_5:17
theorem Th18: :: SCMPDS_5:18
theorem Th19: :: SCMPDS_5:19
theorem Th20: :: SCMPDS_5:20
theorem Th21: :: SCMPDS_5:21
theorem Th22: :: SCMPDS_5:22
theorem Th23: :: SCMPDS_5:23
theorem Th24: :: SCMPDS_5:24
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
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 -> parahalting ;
coherence
AddTo a,k1,b,k2 is parahalting
cluster SubFrom a,
k1,
b,
k2 -> parahalting ;
coherence
SubFrom a,k1,b,k2 is parahalting
cluster MultBy a,
k1,
b,
k2 -> parahalting ;
coherence
MultBy a,k1,b,k2 is parahalting
cluster Divide a,
k1,
b,
k2 -> parahalting ;
coherence
Divide a,k1,b,k2 is parahalting
cluster a,
k1 := b,
k2 -> parahalting ;
coherence
a,k1 := b,k2 is parahalting
end;
theorem Th26: :: SCMPDS_5:26
:: deftheorem Def3 defines No-StopCode SCMPDS_5:def 3 :
theorem Th27: :: SCMPDS_5:27
theorem Th28: :: SCMPDS_5:28
theorem Th29: :: SCMPDS_5:29
theorem Th30: :: SCMPDS_5:30
theorem Th31: :: SCMPDS_5:31
theorem Th32: :: SCMPDS_5:32
theorem Th33: :: SCMPDS_5:33
theorem Th34: :: SCMPDS_5:34
theorem Th35: :: SCMPDS_5:35
theorem :: SCMPDS_5:36
Lm3:
for I being parahalting No-StopCode Program of SCMPDS
for J being parahalting shiftable Program of SCMPDS
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) & DataPart (Computation s,(LifeSpan s1)) = DataPart ((Computation s1,(LifeSpan s1)) +* (Initialized (stop J))) & 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
theorem Th38: :: SCMPDS_5:38
theorem :: SCMPDS_5:39
:: deftheorem defines Initialized SCMPDS_5:def 4 :
theorem Th40: :: SCMPDS_5:40
theorem Th41: :: SCMPDS_5:41
theorem :: SCMPDS_5:42
canceled;
theorem Th43: :: SCMPDS_5:43
theorem Th44: :: SCMPDS_5:44
theorem Th45: :: SCMPDS_5:45
theorem Th46: :: SCMPDS_5:46
theorem :: SCMPDS_5:47