:: The Construction and Computation of Conditional Statements for SCMPDS
:: by JingChao Chen
::
:: Received June 15, 1999
:: Copyright (c) 1999 Association of Mizar Users
set A = NAT ;
set D = SCM-Data-Loc ;
theorem Th1: :: SCMPDS_6:1
theorem Th2: :: SCMPDS_6:2
theorem Th3: :: SCMPDS_6:3
theorem Th4: :: SCMPDS_6:4
theorem :: SCMPDS_6:5
theorem :: SCMPDS_6:6
theorem Th7: :: SCMPDS_6:7
theorem Th8: :: SCMPDS_6:8
theorem Th9: :: SCMPDS_6:9
theorem Th10: :: SCMPDS_6:10
theorem :: SCMPDS_6:11
theorem Th12: :: SCMPDS_6:12
theorem :: SCMPDS_6:13
canceled;
theorem Th14: :: SCMPDS_6:14
theorem Th15: :: SCMPDS_6:15
theorem Th16: :: SCMPDS_6:16
theorem Th17: :: SCMPDS_6:17
theorem Th18: :: SCMPDS_6:18
theorem Th19: :: SCMPDS_6:19
theorem Th20: :: SCMPDS_6:20
theorem :: SCMPDS_6:21
theorem Th22: :: SCMPDS_6:22
theorem Th23: :: SCMPDS_6:23
theorem Th24: :: SCMPDS_6:24
theorem Th25: :: SCMPDS_6:25
theorem Th26: :: SCMPDS_6:26
theorem Th27: :: SCMPDS_6:27
theorem :: SCMPDS_6:28
theorem Th29: :: SCMPDS_6:29
theorem Th30: :: SCMPDS_6:30
theorem Th31: :: SCMPDS_6:31
:: deftheorem defines Goto SCMPDS_6:def 1 :
Lm1:
for k1 being Integer holds
( inspos 0 in dom ((inspos 0 ) .--> (goto k1)) & ((inspos 0 ) .--> (goto k1)) . (inspos 0 ) = goto k1 )
theorem :: SCMPDS_6:32
canceled;
theorem Th33: :: SCMPDS_6:33
:: deftheorem Def2 defines is_closed_on SCMPDS_6:def 2 :
:: deftheorem Def3 defines is_halting_on SCMPDS_6:def 3 :
theorem Th34: :: SCMPDS_6:34
theorem Th35: :: SCMPDS_6:35
theorem Th36: :: SCMPDS_6:36
theorem :: SCMPDS_6:37
theorem Th38: :: SCMPDS_6:38
theorem Th39: :: SCMPDS_6:39
theorem Th40: :: SCMPDS_6:40
theorem Th41: :: SCMPDS_6:41
theorem Th42: :: SCMPDS_6:42
theorem Th43: :: SCMPDS_6:43
Lm2:
for I being No-StopCode Program of SCMPDS
for J being Program of SCMPDS
for s being State of SCMPDS st I is_closed_on s & I is_halting_on s holds
( IC (Computation (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),((LifeSpan (s +* (Initialized (stop I)))) + 1)) = inspos (((card I) + (card J)) + 1) & DataPart (Computation (s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) = DataPart (Computation (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),((LifeSpan (s +* (Initialized (stop I)))) + 1)) & ( for k being Element of NAT st k <= LifeSpan (s +* (Initialized (stop I))) holds
CurInstr (Computation (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),k) <> halt SCMPDS ) & IC (Computation (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),(LifeSpan (s +* (Initialized (stop I))))) = inspos (card I) & s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J))) is halting & LifeSpan (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J)))) = (LifeSpan (s +* (Initialized (stop I)))) + 1 )
theorem Th44: :: SCMPDS_6:44
theorem Th45: :: SCMPDS_6:45
theorem Th46: :: SCMPDS_6:46
theorem Th47: :: SCMPDS_6:47
theorem Th48: :: SCMPDS_6:48
definition
let a be
Int_position ;
let k be
Integer;
let I,
J be
Program of
SCMPDS ;
func if=0 a,
k,
I,
J -> Program of
SCMPDS equals :: SCMPDS_6:def 4
(((a,k <>0_goto ((card I) + 2)) ';' I) ';' (Goto ((card J) + 1))) ';' J;
coherence
(((a,k <>0_goto ((card I) + 2)) ';' I) ';' (Goto ((card J) + 1))) ';' J is Program of SCMPDS
;
func if>0 a,
k,
I,
J -> Program of
SCMPDS equals :: SCMPDS_6:def 5
(((a,k <=0_goto ((card I) + 2)) ';' I) ';' (Goto ((card J) + 1))) ';' J;
coherence
(((a,k <=0_goto ((card I) + 2)) ';' I) ';' (Goto ((card J) + 1))) ';' J is Program of SCMPDS
;
func if<0 a,
k,
I,
J -> Program of
SCMPDS equals :: SCMPDS_6:def 6
(((a,k >=0_goto ((card I) + 2)) ';' I) ';' (Goto ((card J) + 1))) ';' J;
coherence
(((a,k >=0_goto ((card I) + 2)) ';' I) ';' (Goto ((card J) + 1))) ';' J is Program of SCMPDS
;
end;
:: deftheorem defines if=0 SCMPDS_6:def 4 :
:: deftheorem defines if>0 SCMPDS_6:def 5 :
:: deftheorem defines if<0 SCMPDS_6:def 6 :
definition
let a be
Int_position ;
let k be
Integer;
let I be
Program of
SCMPDS ;
func if=0 a,
k,
I -> Program of
SCMPDS equals :: SCMPDS_6:def 7
(a,k <>0_goto ((card I) + 1)) ';' I;
coherence
(a,k <>0_goto ((card I) + 1)) ';' I is Program of SCMPDS
;
func if<>0 a,
k,
I -> Program of
SCMPDS equals :: SCMPDS_6:def 8
((a,k <>0_goto 2) ';' (goto ((card I) + 1))) ';' I;
coherence
((a,k <>0_goto 2) ';' (goto ((card I) + 1))) ';' I is Program of SCMPDS
;
func if>0 a,
k,
I -> Program of
SCMPDS equals :: SCMPDS_6:def 9
(a,k <=0_goto ((card I) + 1)) ';' I;
coherence
(a,k <=0_goto ((card I) + 1)) ';' I is Program of SCMPDS
;
func if<=0 a,
k,
I -> Program of
SCMPDS equals :: SCMPDS_6:def 10
((a,k <=0_goto 2) ';' (goto ((card I) + 1))) ';' I;
coherence
((a,k <=0_goto 2) ';' (goto ((card I) + 1))) ';' I is Program of SCMPDS
;
func if<0 a,
k,
I -> Program of
SCMPDS equals :: SCMPDS_6:def 11
(a,k >=0_goto ((card I) + 1)) ';' I;
coherence
(a,k >=0_goto ((card I) + 1)) ';' I is Program of SCMPDS
;
func if>=0 a,
k,
I -> Program of
SCMPDS equals :: SCMPDS_6:def 12
((a,k >=0_goto 2) ';' (goto ((card I) + 1))) ';' I;
coherence
((a,k >=0_goto 2) ';' (goto ((card I) + 1))) ';' I is Program of SCMPDS
;
end;
:: deftheorem defines if=0 SCMPDS_6:def 7 :
:: deftheorem defines if<>0 SCMPDS_6:def 8 :
:: deftheorem defines if>0 SCMPDS_6:def 9 :
:: deftheorem defines if<=0 SCMPDS_6:def 10 :
:: deftheorem defines if<0 SCMPDS_6:def 11 :
:: deftheorem defines if>=0 SCMPDS_6:def 12 :
Lm4:
for n being Element of NAT
for i being Instruction of SCMPDS
for I, J being Program of SCMPDS holds card (((i ';' I) ';' (Goto n)) ';' J) = ((card I) + (card J)) + 2
theorem :: SCMPDS_6:49
theorem :: SCMPDS_6:50
Lm5:
for i being Instruction of SCMPDS
for I, J, K being Program of SCMPDS holds (((i ';' I) ';' J) ';' K) . (inspos 0 ) = i
theorem :: SCMPDS_6:51
Lm6:
for n being Element of NAT
for i being Instruction of SCMPDS
for s being State of SCMPDS
for I being Program of SCMPDS holds Shift (stop I),1 c= Computation (s +* (Initialized (stop (i ';' I)))),n
Lm7:
for n being Element of NAT
for i, j being Instruction of SCMPDS
for s being State of SCMPDS
for I being Program of SCMPDS holds Shift (stop I),2 c= Computation (s +* (Initialized (stop ((i ';' j) ';' I)))),n
theorem Th52: :: SCMPDS_6:52
theorem Th53: :: SCMPDS_6:53
theorem Th54: :: SCMPDS_6:54
theorem Th55: :: SCMPDS_6:55
registration
let I,
J be
parahalting shiftable Program of
SCMPDS ;
let a be
Int_position ;
let k1 be
Integer;
cluster if=0 a,
k1,
I,
J -> parahalting shiftable ;
correctness
coherence
( if=0 a,k1,I,J is shiftable & if=0 a,k1,I,J is parahalting );
end;
theorem :: SCMPDS_6:56
theorem :: SCMPDS_6:57
theorem :: SCMPDS_6:58
theorem :: SCMPDS_6:59
theorem :: SCMPDS_6:60
theorem :: SCMPDS_6:61
theorem Th62: :: SCMPDS_6:62
theorem Th63: :: SCMPDS_6:63
theorem Th64: :: SCMPDS_6:64
Lm8:
for s being State of SCMPDS
for loc being Instruction-Location of SCMPDS holds (s +* (Start-At loc)) . (IC SCMPDS ) = loc
theorem Th65: :: SCMPDS_6:65
theorem :: SCMPDS_6:66
theorem :: SCMPDS_6:67
theorem :: SCMPDS_6:68
Lm9:
for i, j being Instruction of SCMPDS
for I being Program of SCMPDS holds card ((i ';' j) ';' I) = (card I) + 2
theorem :: SCMPDS_6:69
Lm10:
for i, j being Instruction of SCMPDS
for I being Program of SCMPDS holds
( inspos 0 in dom ((i ';' j) ';' I) & inspos 1 in dom ((i ';' j) ';' I) )
theorem :: SCMPDS_6:70
Lm11:
for i, j being Instruction of SCMPDS
for I being Program of SCMPDS holds
( ((i ';' j) ';' I) . (inspos 0 ) = i & ((i ';' j) ';' I) . (inspos 1) = j )
theorem :: SCMPDS_6:71
theorem Th72: :: SCMPDS_6:72
theorem Th73: :: SCMPDS_6:73
theorem Th74: :: SCMPDS_6:74
theorem Th75: :: SCMPDS_6:75
theorem :: SCMPDS_6:76
theorem :: SCMPDS_6:77
theorem :: SCMPDS_6:78
theorem :: SCMPDS_6:79
theorem :: SCMPDS_6:80
theorem :: SCMPDS_6:81
theorem Th82: :: SCMPDS_6:82
theorem Th83: :: SCMPDS_6:83
theorem Th84: :: SCMPDS_6:84
theorem Th85: :: SCMPDS_6:85
registration
let I,
J be
parahalting shiftable Program of
SCMPDS ;
let a be
Int_position ;
let k1 be
Integer;
cluster if>0 a,
k1,
I,
J -> parahalting shiftable ;
correctness
coherence
( if>0 a,k1,I,J is shiftable & if>0 a,k1,I,J is parahalting );
end;
theorem :: SCMPDS_6:86
theorem :: SCMPDS_6:87
theorem :: SCMPDS_6:88
theorem :: SCMPDS_6:89
theorem :: SCMPDS_6:90
theorem :: SCMPDS_6:91
theorem Th92: :: SCMPDS_6:92
theorem Th93: :: SCMPDS_6:93
theorem Th94: :: SCMPDS_6:94
theorem Th95: :: SCMPDS_6:95
theorem :: SCMPDS_6:96
theorem :: SCMPDS_6:97
theorem :: SCMPDS_6:98
theorem :: SCMPDS_6:99
theorem :: SCMPDS_6:100
theorem :: SCMPDS_6:101
theorem Th102: :: SCMPDS_6:102
theorem Th103: :: SCMPDS_6:103
theorem Th104: :: SCMPDS_6:104
theorem Th105: :: SCMPDS_6:105
theorem :: SCMPDS_6:106
theorem :: SCMPDS_6:107
theorem :: SCMPDS_6:108
theorem :: SCMPDS_6:109
theorem :: SCMPDS_6:110
theorem :: SCMPDS_6:111
theorem Th112: :: SCMPDS_6:112
theorem Th113: :: SCMPDS_6:113
theorem Th114: :: SCMPDS_6:114
theorem Th115: :: SCMPDS_6:115
registration
let I,
J be
parahalting shiftable Program of
SCMPDS ;
let a be
Int_position ;
let k1 be
Integer;
cluster if<0 a,
k1,
I,
J -> parahalting shiftable ;
correctness
coherence
( if<0 a,k1,I,J is shiftable & if<0 a,k1,I,J is parahalting );
end;
theorem :: SCMPDS_6:116
theorem :: SCMPDS_6:117
theorem :: SCMPDS_6:118
theorem :: SCMPDS_6:119
theorem :: SCMPDS_6:120
theorem :: SCMPDS_6:121
theorem Th122: :: SCMPDS_6:122
theorem Th123: :: SCMPDS_6:123
theorem Th124: :: SCMPDS_6:124
theorem Th125: :: SCMPDS_6:125
theorem :: SCMPDS_6:126
theorem :: SCMPDS_6:127
theorem :: SCMPDS_6:128
theorem :: SCMPDS_6:129
theorem :: SCMPDS_6:130
theorem :: SCMPDS_6:131
theorem Th132: :: SCMPDS_6:132
theorem Th133: :: SCMPDS_6:133
theorem Th134: :: SCMPDS_6:134
theorem Th135: :: SCMPDS_6:135
theorem :: SCMPDS_6:136
theorem :: SCMPDS_6:137
theorem :: SCMPDS_6:138