:: The Construction and shiftability of Program Blocks for SCMPDS
:: by JingChao Chen
::
:: Received June 15, 1999
:: Copyright (c) 1999 Association of Mizar Users
:: deftheorem defines Load SCMPDS_4:def 1 :
theorem Th1: :: SCMPDS_4:1
theorem Th2: :: SCMPDS_4:2
theorem Th3: :: SCMPDS_4:3
:: deftheorem defines Initialized SCMPDS_4:def 2 :
theorem :: SCMPDS_4:4
canceled;
theorem :: SCMPDS_4:5
canceled;
theorem Th6: :: SCMPDS_4:6
theorem Th7: :: SCMPDS_4:7
theorem :: SCMPDS_4:8
theorem Th9: :: SCMPDS_4:9
theorem :: SCMPDS_4:10
canceled;
theorem Th11: :: SCMPDS_4:11
theorem :: SCMPDS_4:12
canceled;
theorem Th13: :: SCMPDS_4:13
theorem Th14: :: SCMPDS_4:14
theorem Th15: :: SCMPDS_4:15
theorem :: SCMPDS_4:16
theorem Th17: :: SCMPDS_4:17
theorem Th18: :: SCMPDS_4:18
theorem :: SCMPDS_4:19
theorem :: SCMPDS_4:20
theorem :: SCMPDS_4:21
theorem :: SCMPDS_4:22
theorem Th23: :: SCMPDS_4:23
theorem :: SCMPDS_4:24
theorem :: SCMPDS_4:25
canceled;
theorem :: SCMPDS_4:26
theorem Th27: :: SCMPDS_4:27
theorem Th28: :: SCMPDS_4:28
theorem Th29: :: SCMPDS_4:29
theorem Th30: :: SCMPDS_4:30
theorem Th31: :: SCMPDS_4:31
theorem Th32: :: SCMPDS_4:32
theorem :: SCMPDS_4:33
theorem Th34: :: SCMPDS_4:34
theorem :: SCMPDS_4:35
theorem :: SCMPDS_4:36
:: deftheorem defines ';' SCMPDS_4:def 3 :
theorem Th37: :: SCMPDS_4:37
theorem Th38: :: SCMPDS_4:38
theorem Th39: :: SCMPDS_4:39
theorem :: SCMPDS_4:40
theorem :: SCMPDS_4:41
theorem :: SCMPDS_4:42
:: deftheorem defines ';' SCMPDS_4:def 4 :
:: deftheorem defines ';' SCMPDS_4:def 5 :
:: deftheorem defines ';' SCMPDS_4:def 6 :
theorem :: SCMPDS_4:43
theorem :: SCMPDS_4:44
theorem Th45: :: SCMPDS_4:45
theorem Th46: :: SCMPDS_4:46
theorem :: SCMPDS_4:47
theorem :: SCMPDS_4:48
theorem :: SCMPDS_4:49
theorem :: SCMPDS_4:50
theorem :: SCMPDS_4:51
theorem :: SCMPDS_4:52
theorem :: SCMPDS_4:53
theorem Th54: :: SCMPDS_4:54
theorem :: SCMPDS_4:55
canceled;
theorem Th56: :: SCMPDS_4:56
theorem :: SCMPDS_4:57
theorem Th58: :: SCMPDS_4:58
theorem Th59: :: SCMPDS_4:59
theorem :: SCMPDS_4:60
canceled;
theorem :: SCMPDS_4:61
theorem :: SCMPDS_4:62
:: deftheorem defines stop SCMPDS_4:def 7 :
:: deftheorem defines IExec SCMPDS_4:def 8 :
:: deftheorem Def9 defines paraclosed SCMPDS_4:def 9 :
:: deftheorem Def10 defines parahalting SCMPDS_4:def 10 :
Lm1:
Load (halt SCMPDS ) is parahalting
theorem Th63: :: SCMPDS_4:63
theorem :: SCMPDS_4:64
canceled;
theorem :: SCMPDS_4:65
canceled;
theorem Th66: :: SCMPDS_4:66
theorem Th67: :: SCMPDS_4:67
theorem Th68: :: SCMPDS_4:68
theorem Th69: :: SCMPDS_4:69
theorem :: SCMPDS_4:70
canceled;
theorem Th71: :: SCMPDS_4:71
theorem :: SCMPDS_4:72
canceled;
theorem :: SCMPDS_4:73
theorem Th74: :: SCMPDS_4:74
theorem Th75: :: SCMPDS_4:75
:: deftheorem Def11 defines valid_at SCMPDS_4:def 11 :
theorem :: SCMPDS_4:76
canceled;
theorem Th77: :: SCMPDS_4:77
:: deftheorem Def12 defines shiftable SCMPDS_4:def 12 :
Lm3:
Load (halt SCMPDS ) is shiftable
:: deftheorem Def13 defines shiftable SCMPDS_4:def 13 :
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
cluster SubFrom a,
k1,
b,
k2 -> shiftable ;
coherence
SubFrom a,k1,b,k2 is shiftable
cluster MultBy a,
k1,
b,
k2 -> shiftable ;
coherence
MultBy a,k1,b,k2 is shiftable
cluster Divide a,
k1,
b,
k2 -> shiftable ;
coherence
Divide a,k1,b,k2 is shiftable
cluster a,
k1 := b,
k2 -> shiftable ;
coherence
a,k1 := b,k2 is shiftable
end;
theorem :: SCMPDS_4:78
theorem :: SCMPDS_4:79
theorem :: SCMPDS_4:80
theorem :: SCMPDS_4:81
theorem Th82: :: SCMPDS_4:82
theorem Th83: :: SCMPDS_4:83
theorem :: SCMPDS_4:84