SCM_HALT: Initialization Halting Concepts and Their Basic Properties of SCM+FSA

:: 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

begin

definition

let I be Program of SCM+FSA;
attr I is InitClosed means :Def1: :: SCM_HALT:def 1
for s being State of SCM+FSA
for n being Element of NAT st Initialized I c= s holds
IC (Comput ((ProgramPart s),s,n)) in dom I;
attr I is InitHalting means :Def2: :: SCM_HALT:def 2
Initialized I is halting ;
attr I is keepInt0_1 means :Def3: :: SCM_HALT:def 3
for s being State of SCM+FSA st Initialized I c= s holds
for k being Element of NAT holds (Comput ((ProgramPart s),s,k)) . (intloc 0) = 1;

end;

:: 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

for x being set
for i, m, n being Element of NAT holds
( not x in dom (((intloc i) .--> m) +* (Start-At (n,SCM+FSA))) or x = intloc i or x = IC SCM+FSA )

proof end;

theorem Th2: :: SCM_HALT:2

for I being Program of SCM+FSA
for i, m, n being Element of NAT holds dom I misses dom (((intloc i) .--> m) +* (Start-At (n,SCM+FSA)))

proof end;

set iS = ((intloc 0) .--> 1) +* (Start-At (0,SCM+FSA));

theorem :: SCM_HALT:3

canceled;

theorem Th4: :: SCM_HALT:4

Macro (halt SCM+FSA) is InitHalting

proof end;

registration

cluster non empty Relation-like NAT -defined the carrier of SCM+FSA -defined the Instructions of SCM+FSA -valued Function-like the Object-Kind of SCM+FSA -compatible V27() V63() InitHalting set ;
existence by Th4;

end;

theorem Th5: :: SCM_HALT:5

for s being State of SCM+FSA
for I being InitHalting Program of SCM+FSA st Initialized I c= s holds
ProgramPart s halts_on s

proof end;

theorem Th6: :: SCM_HALT:6

for I being Program of SCM+FSA holds I +* (Start-At (0,SCM+FSA)) c= Initialized I

proof end;

theorem Th7: :: SCM_HALT:7

for I being Program of SCM+FSA
for s being State of SCM+FSA st Initialized I c= s holds
s . (intloc 0) = 1

proof end;

registration

proof end;

end;

registration

proof end;

end;

registration

proof end;

end;

theorem :: SCM_HALT:8

for s being State of SCM+FSA
for I being InitHalting Program of SCM+FSA
for a being read-write Int-Location st not a in UsedIntLoc I holds
(IExec (I,s)) . a = s . a

proof end;

theorem :: SCM_HALT:9

for s being State of SCM+FSA
for I being InitHalting Program of SCM+FSA
for f being FinSeq-Location st not f in UsedInt*Loc I holds
(IExec (I,s)) . f = s . f

proof end;

registration

let I be InitHalting Program of SCM+FSA;
cluster Initialized I -> halting ;
coherence by Def2;

end;

registration

end;

theorem :: SCM_HALT:10

canceled;

theorem :: SCM_HALT:11

canceled;

theorem Th12: :: SCM_HALT:12

for s1, s2 being State of SCM+FSA
for J being InitHalting Program of SCM+FSA st Initialized J c= s1 holds
for n being Element of NAT st ProgramPart (Relocated (J,n)) c= s2 & IC s2 = n & DataPart s1 = DataPart s2 holds
for i being Element of NAT holds
( (IC (Comput ((ProgramPart s1),s1,i))) + n = IC (Comput ((ProgramPart s2),s2,i)) & IncAddr ((CurInstr ((ProgramPart s1),(Comput ((ProgramPart s1),s1,i)))),n) = CurInstr ((ProgramPart s2),(Comput ((ProgramPart s2),s2,i))) & DataPart (Comput ((ProgramPart s1),s1,i)) = DataPart (Comput ((ProgramPart s2),s2,i)) )

proof end;

theorem Th13: :: SCM_HALT:13

for I being Program of SCM+FSA
for s being State of SCM+FSA st Initialized I c= s holds
I c= s

proof end;

theorem Th14: :: SCM_HALT:14

for s1, s2 being State of SCM+FSA
for I being InitHalting Program of SCM+FSA st Initialized I c= s1 & Initialized I c= s2 & s1,s2 equal_outside NAT holds
for k being Element of NAT holds
( Comput ((ProgramPart s1),s1,k), Comput ((ProgramPart s2),s2,k) equal_outside NAT & CurInstr ((ProgramPart s1),(Comput ((ProgramPart s1),s1,k))) = CurInstr ((ProgramPart s2),(Comput ((ProgramPart s2),s2,k))) )

proof end;

theorem Th15: :: SCM_HALT:15

for s1, s2 being State of SCM+FSA
for I being InitHalting Program of SCM+FSA st Initialized I c= s1 & Initialized I c= s2 & s1,s2 equal_outside NAT holds
( LifeSpan ((ProgramPart s1),s1) = LifeSpan ((ProgramPart s2),s2) & Result ((ProgramPart s1),s1), Result ((ProgramPart s2),s2) equal_outside NAT )

proof end;

registration

proof end;

end;

registration

proof end;

end;

theorem :: SCM_HALT:16

canceled;

theorem Th17: :: SCM_HALT:17

for s being State of SCM+FSA
for I being InitHalting keepInt0_1 Program of SCM+FSA holds (IExec (I,s)) . (intloc 0) = 1

proof end;

registration

proof end;

end;

theorem Th18: :: SCM_HALT:18

for s being State of SCM+FSA
for I being InitClosed Program of SCM+FSA
for J being Program of SCM+FSA st Initialized I c= s & ProgramPart s halts_on s holds
for m being Element of NAT st m <= LifeSpan ((ProgramPart s),s) holds
Comput ((ProgramPart s),s,m), Comput ((ProgramPart (s +* (I ';' J))),(s +* (I ';' J)),m) equal_outside NAT

proof end;

theorem Th19: :: SCM_HALT:19

for I being Program of SCM+FSA
for s being State of SCM+FSA
for i, m, n being Element of NAT holds (s +* I) +* (((intloc i) .--> m) +* (Start-At (n,SCM+FSA))) = (s +* (((intloc i) .--> m) +* (Start-At (n,SCM+FSA)))) +* I

proof end;

theorem Th20: :: SCM_HALT:20

for I being Program of SCM+FSA
for s being State of SCM+FSA st ((intloc 0) .--> 1) +* (Start-At (0,SCM+FSA)) c= s holds
( Initialized I c= s +* (I +* (((intloc 0) .--> 1) +* (Start-At (0,SCM+FSA)))) & s +* (I +* (((intloc 0) .--> 1) +* (Start-At (0,SCM+FSA)))) = s +* I & (s +* (I +* (((intloc 0) .--> 1) +* (Start-At (0,SCM+FSA))))) +* (Directed I) = s +* (Directed I) )

proof end;

theorem Th21: :: SCM_HALT:21

for s being State of SCM+FSA
for I being InitClosed Program of SCM+FSA st ProgramPart (s +* I) halts_on s +* I & Directed I c= s & ((intloc 0) .--> 1) +* (Start-At (0,SCM+FSA)) c= s holds
IC (Comput ((ProgramPart s),s,((LifeSpan ((ProgramPart (s +* I)),(s +* I))) + 1))) = card I

proof end;

theorem Th22: :: SCM_HALT:22

for s being State of SCM+FSA
for I being InitClosed Program of SCM+FSA st ProgramPart (s +* I) halts_on s +* I & Directed I c= s & ((intloc 0) .--> 1) +* (Start-At (0,SCM+FSA)) c= s holds
DataPart (Comput ((ProgramPart s),s,(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) = DataPart (Comput ((ProgramPart s),s,((LifeSpan ((ProgramPart (s +* I)),(s +* I))) + 1)))

proof end;

theorem Th23: :: SCM_HALT:23

for s being State of SCM+FSA
for I being InitHalting Program of SCM+FSA st Initialized I c= s holds
for k being Element of NAT st k <= LifeSpan ((ProgramPart s),s) holds
CurInstr ((ProgramPart (s +* (Directed I))),(Comput ((ProgramPart (s +* (Directed I))),(s +* (Directed I)),k))) <> halt SCM+FSA

proof end;

theorem Th24: :: SCM_HALT:24

for s being State of SCM+FSA
for I being InitClosed Program of SCM+FSA st ProgramPart (s +* (Initialized I)) halts_on s +* (Initialized I) holds
for J being Program of SCM+FSA
for k being Element of NAT st k <= LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) holds
Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),k), Comput ((ProgramPart (s +* (Initialized (I ';' J)))),(s +* (Initialized (I ';' J))),k) equal_outside NAT

proof end;

theorem Th25: :: SCM_HALT:25

proof end;

registration

let I be InitHalting keepInt0_1 Program of SCM+FSA;
let J be InitHalting Program of SCM+FSA;
cluster I ';' J -> InitHalting ;
coherence

proof end;

end;

theorem Th26: :: SCM_HALT:26

for s being State of SCM+FSA
for I being keepInt0_1 Program of SCM+FSA st ProgramPart (s +* I) halts_on s +* I holds
for J being InitClosed Program of SCM+FSA st Initialized (I ';' J) c= s holds
for k being Element of NAT holds (Comput ((ProgramPart ((Result ((ProgramPart (s +* I)),(s +* I))) +* (Initialized J))),((Result ((ProgramPart (s +* I)),(s +* I))) +* (Initialized J)),k)) +* (Start-At (((IC (Comput ((ProgramPart ((Result ((ProgramPart (s +* I)),(s +* I))) +* (Initialized J))),((Result ((ProgramPart (s +* I)),(s +* I))) +* (Initialized J)),k))) + (card I)),SCM+FSA)), Comput ((ProgramPart (s +* (I ';' J))),(s +* (I ';' J)),(((LifeSpan ((ProgramPart (s +* I)),(s +* I))) + 1) + k)) equal_outside NAT

proof end;

theorem Th27: :: SCM_HALT:27

for s being State of SCM+FSA
for I being keepInt0_1 Program of SCM+FSA st not ProgramPart (s +* (Initialized I)) halts_on s +* (Initialized I) holds
for J being Program of SCM+FSA
for k being Element of NAT holds Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),k), Comput ((ProgramPart (s +* (Initialized (I ';' J)))),(s +* (Initialized (I ';' J))),k) equal_outside NAT

proof end;

theorem Th28: :: SCM_HALT:28

for s being State of SCM+FSA
for I being InitHalting keepInt0_1 Program of SCM+FSA
for J being InitHalting Program of SCM+FSA holds LifeSpan ((ProgramPart (s +* (Initialized (I ';' J)))),(s +* (Initialized (I ';' J)))) = ((LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) + 1) + (LifeSpan ((ProgramPart ((Result ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) +* (Initialized J))),((Result ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) +* (Initialized J))))

proof end;

theorem Th29: :: SCM_HALT:29

for s being State of SCM+FSA
for I being InitHalting keepInt0_1 Program of SCM+FSA
for J being InitHalting Program of SCM+FSA holds IExec ((I ';' J),s) = (IExec (J,(IExec (I,s)))) +* (Start-At (((IC (IExec (J,(IExec (I,s))))) + (card I)),SCM+FSA))

proof end;

registration

let i be parahalting Instruction of SCM+FSA;
cluster Macro i -> InitHalting ;
coherence ;

end;

registration

let i be parahalting Instruction of SCM+FSA;
let J be parahalting Program of SCM+FSA;
cluster i ';' J -> InitHalting ;
coherence ;

end;

registration

let i be parahalting keeping_0 Instruction of SCM+FSA;
let J be InitHalting Program of SCM+FSA;
cluster i ';' J -> InitHalting ;
coherence ;

end;

registration

let I, J be keepInt0_1 Program of SCM+FSA;
cluster I ';' J -> keepInt0_1 ;
coherence

proof end;

end;

registration

let j be parahalting keeping_0 Instruction of SCM+FSA;
let I be InitHalting keepInt0_1 Program of SCM+FSA;
cluster I ';' j -> InitHalting keepInt0_1 ;
coherence ;

end;

registration

let i be parahalting keeping_0 Instruction of SCM+FSA;
let J be InitHalting keepInt0_1 Program of SCM+FSA;
cluster i ';' J -> InitHalting keepInt0_1 ;
coherence ;

end;

registration

let j be parahalting Instruction of SCM+FSA;
let I be parahalting Program of SCM+FSA;
cluster I ';' j -> InitHalting ;
coherence ;

end;

registration

let i, j be parahalting Instruction of SCM+FSA;
cluster i ';' j -> InitHalting ;
coherence ;

end;

theorem Th30: :: SCM_HALT:30

for s being State of SCM+FSA
for a being Int-Location
for I being InitHalting keepInt0_1 Program of SCM+FSA
for J being InitHalting Program of SCM+FSA holds (IExec ((I ';' J),s)) . a = (IExec (J,(IExec (I,s)))) . a

proof end;

theorem Th31: :: SCM_HALT:31

for s being State of SCM+FSA
for f being FinSeq-Location
for I being InitHalting keepInt0_1 Program of SCM+FSA
for J being InitHalting Program of SCM+FSA holds (IExec ((I ';' J),s)) . f = (IExec (J,(IExec (I,s)))) . f

proof end;

theorem Th32: :: SCM_HALT:32

for I being InitHalting keepInt0_1 Program of SCM+FSA
for s being State of SCM+FSA holds DataPart (Initialized (IExec (I,s))) = DataPart (IExec (I,s))

proof end;

theorem Th33: :: SCM_HALT:33

for s being State of SCM+FSA
for a being Int-Location
for I being InitHalting keepInt0_1 Program of SCM+FSA
for j being parahalting Instruction of SCM+FSA holds (IExec ((I ';' j),s)) . a = (Exec (j,(IExec (I,s)))) . a

proof end;

theorem Th34: :: SCM_HALT:34

for s being State of SCM+FSA
for f being FinSeq-Location
for I being InitHalting keepInt0_1 Program of SCM+FSA
for j being parahalting Instruction of SCM+FSA holds (IExec ((I ';' j),s)) . f = (Exec (j,(IExec (I,s)))) . f

proof end;

definition

let I be Program of SCM+FSA;
let s be State of SCM+FSA;
pred I is_closed_onInit s means :Def4: :: SCM_HALT:def 4
for k being Element of NAT holds IC (Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),k)) in dom I;
pred I is_halting_onInit s means :Def5: :: SCM_HALT:def 5
ProgramPart (s +* (Initialized I)) halts_on s +* (Initialized I);

end;

:: 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

for I being Program of SCM+FSA holds
( I is InitClosed iff for s being State of SCM+FSA holds I is_closed_onInit s )

proof end;

theorem Th36: :: SCM_HALT:36

for I being Program of SCM+FSA holds
( I is InitHalting iff for s being State of SCM+FSA holds I is_halting_onInit s )

proof end;

theorem Th37: :: SCM_HALT:37

for s being State of SCM+FSA
for I being Program of SCM+FSA
for a being Int-Location st not I destroys a & I is_closed_onInit s & Initialized I c= s holds
for k being Element of NAT holds (Comput ((ProgramPart s),s,k)) . a = s . a

proof end;

registration

proof end;

end;

registration

proof end;

end;

registration

cluster Stop SCM+FSA -> good InitHalting ;
coherence ;

end;

theorem :: SCM_HALT:38

for s being State of SCM+FSA
for i being parahalting keeping_0 Instruction of SCM+FSA
for J being InitHalting Program of SCM+FSA
for a being Int-Location holds (IExec ((i ';' J),s)) . a = (IExec (J,(Exec (i,(Initialized s))))) . a

proof end;

theorem :: SCM_HALT:39

for s being State of SCM+FSA
for i being parahalting keeping_0 Instruction of SCM+FSA
for J being InitHalting Program of SCM+FSA
for f being FinSeq-Location holds (IExec ((i ';' J),s)) . f = (IExec (J,(Exec (i,(Initialized s))))) . f

proof end;

theorem Th40: :: SCM_HALT:40

for s being State of SCM+FSA
for I being Program of SCM+FSA holds
( I is_closed_onInit s iff I is_closed_on Initialized s )

proof end;

theorem Th41: :: SCM_HALT:41

for s being State of SCM+FSA
for I being Program of SCM+FSA holds
( I is_halting_onInit s iff I is_halting_on Initialized s )

proof end;

theorem :: SCM_HALT:42

for I being Program of SCM+FSA
for s being State of SCM+FSA holds IExec (I,s) = IExec (I,(Initialized s))

proof end;

theorem Th43: :: SCM_HALT:43

for s being State of SCM+FSA
for I, J being Program of SCM+FSA
for a being read-write Int-Location st s . a = 0 & I is_closed_onInit s & I is_halting_onInit s holds
( if=0 (a,I,J) is_closed_onInit s & if=0 (a,I,J) is_halting_onInit s )

proof end;

theorem Th44: :: SCM_HALT:44

for s being State of SCM+FSA
for I, J being Program of SCM+FSA
for a being read-write Int-Location st s . a = 0 & I is_closed_onInit s & I is_halting_onInit s holds
IExec ((if=0 (a,I,J)),s) = (IExec (I,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA))

proof end;

theorem Th45: :: SCM_HALT:45

for s being State of SCM+FSA
for I, J being Program of SCM+FSA
for a being read-write Int-Location st s . a <> 0 & J is_closed_onInit s & J is_halting_onInit s holds
( if=0 (a,I,J) is_closed_onInit s & if=0 (a,I,J) is_halting_onInit s )

proof end;

theorem Th46: :: SCM_HALT:46

for I, J being Program of SCM+FSA
for a being read-write Int-Location
for s being State of SCM+FSA st s . a <> 0 & J is_closed_onInit s & J is_halting_onInit s holds
IExec ((if=0 (a,I,J)),s) = (IExec (J,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA))

proof end;

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 ((((card I) + (card J)) + 3),SCM+FSA)) ) & ( s . a <> 0 implies IExec ((if=0 (a,I,J)),s) = (IExec (J,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA)) ) )

proof end;

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)) = ((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 ) ) ) )

proof end;

theorem Th49: :: SCM_HALT:49

for s being State of SCM+FSA
for I, J being Program of SCM+FSA
for a being read-write Int-Location st s . a > 0 & I is_closed_onInit s & I is_halting_onInit s holds
( if>0 (a,I,J) is_closed_onInit s & if>0 (a,I,J) is_halting_onInit s )

proof end;

theorem Th50: :: SCM_HALT:50

for s being State of SCM+FSA
for I, J being Program of SCM+FSA
for a being read-write Int-Location st s . a > 0 & I is_closed_onInit s & I is_halting_onInit s holds
IExec ((if>0 (a,I,J)),s) = (IExec (I,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA))

proof end;

theorem Th51: :: SCM_HALT:51

for s being State of SCM+FSA
for I, J being Program of SCM+FSA
for a being read-write Int-Location st s . a <= 0 & J is_closed_onInit s & J is_halting_onInit s holds
( if>0 (a,I,J) is_closed_onInit s & if>0 (a,I,J) is_halting_onInit s )

proof end;

theorem Th52: :: SCM_HALT:52

for I, J being Program of SCM+FSA
for a being read-write Int-Location
for s being State of SCM+FSA st s . a <= 0 & J is_closed_onInit s & J is_halting_onInit s holds
IExec ((if>0 (a,I,J)),s) = (IExec (J,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA))

proof end;

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 ((((card I) + (card J)) + 3),SCM+FSA)) ) & ( s . a <= 0 implies IExec ((if>0 (a,I,J)),s) = (IExec (J,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA)) ) )

proof end;

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)) = ((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 ) ) ) )

proof end;

theorem Th55: :: SCM_HALT:55

for s being State of SCM+FSA
for I, J being Program of SCM+FSA
for a being read-write Int-Location st s . a < 0 & I is_closed_onInit s & I is_halting_onInit s holds
IExec ((if<0 (a,I,J)),s) = (IExec (I,s)) +* (Start-At (((((card I) + (card J)) + (card J)) + 7),SCM+FSA))

proof end;

theorem Th56: :: SCM_HALT:56

for s being State of SCM+FSA
for I, J being Program of SCM+FSA
for a being read-write Int-Location st s . a = 0 & J is_closed_onInit s & J is_halting_onInit s holds
IExec ((if<0 (a,I,J)),s) = (IExec (J,s)) +* (Start-At (((((card I) + (card J)) + (card J)) + 7),SCM+FSA))

proof end;

theorem Th57: :: SCM_HALT:57

for s being State of SCM+FSA
for I, J being Program of SCM+FSA
for a being read-write Int-Location st s . a > 0 & J is_closed_onInit s & J is_halting_onInit s holds
IExec ((if<0 (a,I,J)),s) = (IExec (J,s)) +* (Start-At (((((card I) + (card J)) + (card J)) + 7),SCM+FSA))

proof end;

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 (((((card I) + (card J)) + (card J)) + 7),SCM+FSA)) ) & ( s . a >= 0 implies IExec ((if<0 (a,I,J)),s) = (IExec (J,s)) +* (Start-At (((((card I) + (card J)) + (card J)) + 7),SCM+FSA)) ) )

proof end;

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 by Th47;
cluster if>0 (a,I,J) -> InitHalting ;
correctness by Th53;
cluster if<0 (a,I,J) -> InitHalting ;
correctness by Th58;

end;

theorem Th59: :: SCM_HALT:59

for I being Program of SCM+FSA holds
( I is InitHalting iff for s being State of SCM+FSA holds I is_halting_on Initialized s )

proof end;

theorem Th60: :: SCM_HALT:60

for I being Program of SCM+FSA holds
( I is InitClosed iff for s being State of SCM+FSA holds I is_closed_on Initialized s )

proof end;

theorem Th61: :: SCM_HALT:61

for s being State of SCM+FSA
for I being InitHalting Program of SCM+FSA
for a being read-write Int-Location holds (IExec (I,s)) . a = (Comput ((ProgramPart ((Initialized s) +* (I +* (Start-At (0,SCM+FSA))))),((Initialized s) +* (I +* (Start-At (0,SCM+FSA)))),(LifeSpan ((ProgramPart ((Initialized s) +* (I +* (Start-At (0,SCM+FSA))))),((Initialized s) +* (I +* (Start-At (0,SCM+FSA)))))))) . a

proof end;

theorem Th62: :: SCM_HALT:62

for s being State of SCM+FSA
for I being InitHalting Program of SCM+FSA
for a being Int-Location
for k being Element of NAT st not I destroys a holds
(IExec (I,s)) . a = (Comput ((ProgramPart ((Initialized s) +* (I +* (Start-At (0,SCM+FSA))))),((Initialized s) +* (I +* (Start-At (0,SCM+FSA)))),k)) . a

proof end;

set A = NAT ;

set D = Int-Locations \/ FinSeq-Locations;

theorem Th63: :: SCM_HALT:63

for s being State of SCM+FSA
for I being InitHalting Program of SCM+FSA
for a being Int-Location st not I destroys a holds
(IExec (I,s)) . a = (Initialized s) . a

proof end;

theorem Th64: :: SCM_HALT:64

for s being State of SCM+FSA
for I being InitHalting keepInt0_1 Program of SCM+FSA
for a being read-write Int-Location st not I destroys a holds
(Comput ((ProgramPart ((Initialized s) +* ((I ';' (SubFrom (a,(intloc 0)))) +* (Start-At (0,SCM+FSA))))),((Initialized s) +* ((I ';' (SubFrom (a,(intloc 0)))) +* (Start-At (0,SCM+FSA)))),(LifeSpan ((ProgramPart ((Initialized s) +* ((I ';' (SubFrom (a,(intloc 0)))) +* (Start-At (0,SCM+FSA))))),((Initialized s) +* ((I ';' (SubFrom (a,(intloc 0)))) +* (Start-At (0,SCM+FSA)))))))) . a = (s . a) - 1

proof end;

theorem Th65: :: SCM_HALT:65

for s being State of SCM+FSA
for I being InitClosed Program of SCM+FSA st Initialized I c= s & ProgramPart s halts_on s holds
for m being Element of NAT st m <= LifeSpan ((ProgramPart s),s) holds
Comput ((ProgramPart s),s,m), Comput ((ProgramPart (s +* (loop I))),(s +* (loop I)),m) equal_outside NAT

proof end;

theorem :: SCM_HALT:66

for s being State of SCM+FSA
for I being InitHalting Program of SCM+FSA st Initialized I c= s holds
for k being Element of NAT st k <= LifeSpan ((ProgramPart s),s) holds
CurInstr ((ProgramPart (s +* (loop I))),(Comput ((ProgramPart (s +* (loop I))),(s +* (loop I)),k))) <> halt SCM+FSA

proof end;

theorem Th67: :: SCM_HALT:67

for I being Program of SCM+FSA
for s being State of SCM+FSA holds I c= s +* (Initialized I)

proof end;

theorem Th68: :: SCM_HALT:68

for s being State of SCM+FSA
for I being Program of SCM+FSA st I is_closed_onInit s & I is_halting_onInit s holds
for m being Element of NAT st m <= LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) holds
Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),m), Comput ((ProgramPart (s +* (Initialized (loop I)))),(s +* (Initialized (loop I))),m) equal_outside NAT

proof end;

theorem Th69: :: SCM_HALT:69

for s being State of SCM+FSA
for I being Program of SCM+FSA st I is_closed_onInit s & I is_halting_onInit s holds
for m being Element of NAT st m < LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) holds
CurInstr ((ProgramPart (s +* (Initialized I))),(Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),m))) = CurInstr ((ProgramPart (s +* (Initialized (loop I)))),(Comput ((ProgramPart (s +* (Initialized (loop I)))),(s +* (Initialized (loop I))),m)))

proof end;

theorem Th70: :: SCM_HALT:70

for l being Element of NAT holds not l in dom (((intloc 0) .--> 1) +* (Start-At (0,SCM+FSA)))

proof end;

theorem Th71: :: SCM_HALT:71

for s being State of SCM+FSA
for I being Program of SCM+FSA st I is_closed_onInit s & I is_halting_onInit s holds
( CurInstr ((ProgramPart (s +* (Initialized (loop I)))),(Comput ((ProgramPart (s +* (Initialized (loop I)))),(s +* (Initialized (loop I))),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I))))))) = goto 0 & ( for m being Element of NAT st m <= LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) holds
CurInstr ((ProgramPart (s +* (Initialized (loop I)))),(Comput ((ProgramPart (s +* (Initialized (loop I)))),(s +* (Initialized (loop I))),m))) <> halt SCM+FSA ) )

proof end;

theorem :: SCM_HALT:72

canceled;

theorem Th73: :: SCM_HALT:73

for s being State of SCM+FSA
for I being good InitHalting Program of SCM+FSA
for a being read-write Int-Location st not I destroys a & s . (intloc 0) = 1 & s . a > 0 holds
loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) is_pseudo-closed_on s

proof end;

theorem :: SCM_HALT:74

for s being State of SCM+FSA
for I being good InitHalting Program of SCM+FSA
for a being read-write Int-Location st not I destroys a & s . a > 0 holds
Initialized (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) is_pseudo-closed_on s

proof end;

theorem :: SCM_HALT:75

for s being State of SCM+FSA
for I being good InitHalting Program of SCM+FSA
for a being read-write Int-Location st not I destroys a & s . (intloc 0) = 1 holds
( Times (a,I) is_closed_on s & Times (a,I) is_halting_on s )

proof end;

theorem :: SCM_HALT:76

for I being good InitHalting Program of SCM+FSA
for a being read-write Int-Location st not I destroys a holds
Initialized (Times (a,I)) is halting

proof end;

registration

let a be read-write Int-Location ;
let I be good Program of SCM+FSA;
cluster Times (a,I) -> good ;
coherence ;

end;

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 not I destroys 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 2),(I ';' (SubFrom (a,(intloc 0)))))))) & k = (LifeSpan ((ProgramPart (s +* (Initialized (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))))),(s +* (Initialized (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))))) + 1 & (Comput ((ProgramPart s2),s2,k)) . a = (s . a) - 1 & (Comput ((ProgramPart s2),s2,k)) . (intloc 0) = 1 & ( for b being read-write Int-Location st b <> a holds
(Comput ((ProgramPart s2),s2,k)) . b = (IExec (I,s)) . b ) & ( for f being FinSeq-Location holds (Comput ((ProgramPart s2),s2,k)) . f = (IExec (I,s)) . f ) & IC (Comput ((ProgramPart s2),s2,k)) = 0 & ( for n being Element of NAT st n <= k holds
IC (Comput ((ProgramPart s2),s2,n)) in dom (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ) )

proof end;

theorem Th78: :: SCM_HALT:78

for s being State of SCM+FSA
for I being good InitHalting Program of SCM+FSA
for a being read-write Int-Location st s . (intloc 0) = 1 & s . a <= 0 holds
DataPart (IExec ((Times (a,I)),s)) = DataPart s

proof end;

theorem Th79: :: SCM_HALT:79

for s being State of SCM+FSA
for I being good InitHalting Program of SCM+FSA
for a being read-write Int-Location st not I destroys a & s . a > 0 holds
( (IExec ((I ';' (SubFrom (a,(intloc 0)))),s)) . a = (s . a) - 1 & DataPart (IExec ((Times (a,I)),s)) = DataPart (IExec ((Times (a,I)),(IExec ((I ';' (SubFrom (a,(intloc 0)))),s)))) )

proof end;

theorem :: SCM_HALT:80

for s being State of SCM+FSA
for I being good InitHalting Program of SCM+FSA
for f being FinSeq-Location
for a being read-write Int-Location st s . a <= 0 holds
(IExec ((Times (a,I)),s)) . f = s . f

proof end;

theorem :: SCM_HALT:81

for s being State of SCM+FSA
for I being good InitHalting Program of SCM+FSA
for b being Int-Location
for a being read-write Int-Location st s . a <= 0 holds
(IExec ((Times (a,I)),s)) . b = (Initialized s) . b

proof end;

theorem :: SCM_HALT:82

for s being State of SCM+FSA
for I being good InitHalting Program of SCM+FSA
for f being FinSeq-Location
for a being read-write Int-Location st not I destroys a & s . a > 0 holds
(IExec ((Times (a,I)),s)) . f = (IExec ((Times (a,I)),(IExec ((I ';' (SubFrom (a,(intloc 0)))),s)))) . f

proof end;

theorem :: SCM_HALT:83

for s being State of SCM+FSA
for I being good InitHalting Program of SCM+FSA
for b being Int-Location
for a being read-write Int-Location st not I destroys a & s . a > 0 holds
(IExec ((Times (a,I)),s)) . b = (IExec ((Times (a,I)),(IExec ((I ';' (SubFrom (a,(intloc 0)))),s)))) . b

proof end;

definition

let i be Instruction of SCM+FSA;
redefine attr i is good means :Def6: :: SCM_HALT:def 6
not i destroys intloc 0;
compatibility

proof end;

end;

:: deftheorem Def6 defines good SCM_HALT:def 6 :

registration

cluster good parahalting with_explicit_jumps IC-good Exec-preserving Element of the Instructions of SCM+FSA;
existence

proof end;

end;

registration

let n be Element of NAT ;
cluster intloc (n + 1) -> read-write ;
coherence

proof end;

end;