:: Initialization Halting Concepts and Their Basic Properties of SCM+FSA
:: by JingChao Chen and Yatsuka Nakamura
::
:: Received June 17, 1998
:: Copyright (c) 1998 Association of Mizar Users
:: deftheorem Def1 defines InitClosed SCM_HALT:def 1 :
:: deftheorem Def2 defines InitHalting SCM_HALT:def 2 :
:: deftheorem Def3 defines keepInt0_1 SCM_HALT:def 3 :
theorem Th1: :: SCM_HALT:1
theorem Th2: :: SCM_HALT:2
set iS = ((intloc 0 ) .--> 1) +* (Start-At (insloc 0 ));
theorem :: SCM_HALT:3
canceled;
theorem Th4: :: SCM_HALT:4
theorem Th5: :: SCM_HALT:5
theorem Th6: :: SCM_HALT:6
theorem Th7: :: SCM_HALT:7
theorem :: SCM_HALT:8
theorem :: SCM_HALT:9
theorem Th10: :: SCM_HALT:10
theorem Th11: :: SCM_HALT:11
theorem Th12: :: SCM_HALT:12
theorem Th13: :: SCM_HALT:13
theorem Th14: :: SCM_HALT:14
theorem Th15: :: SCM_HALT:15
theorem :: SCM_HALT:16
canceled;
theorem Th17: :: SCM_HALT:17
theorem Th18: :: SCM_HALT:18
theorem Th19: :: SCM_HALT:19
theorem Th20: :: SCM_HALT:20
theorem Th21: :: SCM_HALT:21
theorem Th22: :: SCM_HALT:22
theorem Th23: :: SCM_HALT:23
theorem Th24: :: SCM_HALT:24
theorem Th25: :: SCM_HALT:25
theorem Th26: :: SCM_HALT:26
theorem Th27: :: SCM_HALT:27
theorem Th28: :: SCM_HALT:28
theorem Th29: :: SCM_HALT:29
theorem Th30: :: SCM_HALT:30
theorem Th31: :: SCM_HALT:31
theorem Th32: :: SCM_HALT:32
theorem Th33: :: SCM_HALT:33
theorem Th34: :: SCM_HALT:34
:: deftheorem Def4 defines is_closed_onInit SCM_HALT:def 4 :
:: deftheorem Def5 defines is_halting_onInit SCM_HALT:def 5 :
theorem Th35: :: SCM_HALT:35
theorem Th36: :: SCM_HALT:36
theorem Th37: :: SCM_HALT:37
theorem :: SCM_HALT:38
theorem :: SCM_HALT:39
theorem Th40: :: SCM_HALT:40
theorem Th41: :: SCM_HALT:41
theorem :: SCM_HALT:42
theorem Th43: :: SCM_HALT:43
theorem Th44: :: SCM_HALT:44
theorem Th45: :: SCM_HALT:45
theorem Th46: :: SCM_HALT:46
theorem Th47: :: SCM_HALT:47
for
s being
State of
SCM+FSA for
I,
J being
InitHalting Program of
SCM+FSA for
a being
read-write Int-Location holds
(
if=0 a,
I,
J is
InitHalting & (
s . a = 0 implies
IExec (if=0 a,I,J),
s = (IExec I,s) +* (Start-At (insloc (((card I) + (card J)) + 3))) ) & (
s . a <> 0 implies
IExec (if=0 a,I,J),
s = (IExec J,s) +* (Start-At (insloc (((card I) + (card J)) + 3))) ) )
theorem :: SCM_HALT:48
for
s being
State of
SCM+FSA for
I,
J being
InitHalting Program of
SCM+FSA for
a being
read-write Int-Location holds
(
IC (IExec (if=0 a,I,J),s) = insloc (((card I) + (card J)) + 3) & (
s . a = 0 implies ( ( for
d being
Int-Location holds
(IExec (if=0 a,I,J),s) . d = (IExec I,s) . d ) & ( for
f being
FinSeq-Location holds
(IExec (if=0 a,I,J),s) . f = (IExec I,s) . f ) ) ) & (
s . a <> 0 implies ( ( for
d being
Int-Location holds
(IExec (if=0 a,I,J),s) . d = (IExec J,s) . d ) & ( for
f being
FinSeq-Location holds
(IExec (if=0 a,I,J),s) . f = (IExec J,s) . f ) ) ) )
theorem Th49: :: SCM_HALT:49
theorem Th50: :: SCM_HALT:50
theorem Th51: :: SCM_HALT:51
theorem Th52: :: SCM_HALT:52
theorem Th53: :: SCM_HALT:53
for
s being
State of
SCM+FSA for
I,
J being
InitHalting Program of
SCM+FSA for
a being
read-write Int-Location holds
(
if>0 a,
I,
J is
InitHalting & (
s . a > 0 implies
IExec (if>0 a,I,J),
s = (IExec I,s) +* (Start-At (insloc (((card I) + (card J)) + 3))) ) & (
s . a <= 0 implies
IExec (if>0 a,I,J),
s = (IExec J,s) +* (Start-At (insloc (((card I) + (card J)) + 3))) ) )
theorem :: SCM_HALT:54
for
s being
State of
SCM+FSA for
I,
J being
InitHalting Program of
SCM+FSA for
a being
read-write Int-Location holds
(
IC (IExec (if>0 a,I,J),s) = insloc (((card I) + (card J)) + 3) & (
s . a > 0 implies ( ( for
d being
Int-Location holds
(IExec (if>0 a,I,J),s) . d = (IExec I,s) . d ) & ( for
f being
FinSeq-Location holds
(IExec (if>0 a,I,J),s) . f = (IExec I,s) . f ) ) ) & (
s . a <= 0 implies ( ( for
d being
Int-Location holds
(IExec (if>0 a,I,J),s) . d = (IExec J,s) . d ) & ( for
f being
FinSeq-Location holds
(IExec (if>0 a,I,J),s) . f = (IExec J,s) . f ) ) ) )
theorem Th55: :: SCM_HALT:55
theorem Th56: :: SCM_HALT:56
theorem Th57: :: SCM_HALT:57
theorem Th58: :: SCM_HALT:58
for
s being
State of
SCM+FSA for
I,
J being
InitHalting Program of
SCM+FSA for
a being
read-write Int-Location holds
(
if<0 a,
I,
J is
InitHalting & (
s . a < 0 implies
IExec (if<0 a,I,J),
s = (IExec I,s) +* (Start-At (insloc ((((card I) + (card J)) + (card J)) + 7))) ) & (
s . a >= 0 implies
IExec (if<0 a,I,J),
s = (IExec J,s) +* (Start-At (insloc ((((card I) + (card J)) + (card J)) + 7))) ) )
registration
let I,
J be
InitHalting Program of
SCM+FSA ;
let a be
read-write Int-Location ;
cluster if=0 a,
I,
J -> InitHalting ;
correctness
coherence
if=0 a,I,J is InitHalting;
by Th47;
cluster if>0 a,
I,
J -> InitHalting ;
correctness
coherence
if>0 a,I,J is InitHalting;
by Th53;
cluster if<0 a,
I,
J -> InitHalting ;
correctness
coherence
if<0 a,I,J is InitHalting;
by Th58;
end;
theorem Th59: :: SCM_HALT:59
theorem Th60: :: SCM_HALT:60
theorem Th61: :: SCM_HALT:61
theorem Th62: :: SCM_HALT:62
set A = NAT ;
set D = Int-Locations \/ FinSeq-Locations ;
theorem Th63: :: SCM_HALT:63
theorem Th64: :: SCM_HALT:64
theorem Th65: :: SCM_HALT:65
theorem :: SCM_HALT:66
theorem Th67: :: SCM_HALT:67
theorem Th68: :: SCM_HALT:68
theorem Th69: :: SCM_HALT:69
theorem Th70: :: SCM_HALT:70
theorem Th71: :: SCM_HALT:71
theorem :: SCM_HALT:72
theorem Th73: :: SCM_HALT:73
theorem :: SCM_HALT:74
theorem :: SCM_HALT:75
theorem :: SCM_HALT:76
theorem Th77: :: SCM_HALT:77
for
s being
State of
SCM+FSA for
I being
good InitHalting Program of
SCM+FSA for
a being
read-write Int-Location st
I does_not_destroy a &
s . a > 0 holds
ex
s2 being
State of
SCM+FSA ex
k being
Element of
NAT st
(
s2 = s +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))))) &
k = (LifeSpan (s +* (Initialized (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))) + 1 &
(Computation s2,k) . a = (s . a) - 1 &
(Computation s2,k) . (intloc 0 ) = 1 & ( for
b being
read-write Int-Location st
b <> a holds
(Computation s2,k) . b = (IExec I,s) . b ) & ( for
f being
FinSeq-Location holds
(Computation s2,k) . f = (IExec I,s) . f ) &
IC (Computation s2,k) = insloc 0 & ( for
n being
Element of
NAT st
n <= k holds
IC (Computation s2,n) in dom (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) ) )
theorem Th78: :: SCM_HALT:78
theorem Th79: :: SCM_HALT:79
theorem :: SCM_HALT:80
theorem :: SCM_HALT:81
theorem :: SCM_HALT:82
theorem :: SCM_HALT:83
:: deftheorem Def6 defines good SCM_HALT:def 6 :