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

for I being Program of SCM+FSA holds
( I is InitClosed iff 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 );

:: deftheorem Def2 defines InitHalting SCM_HALT:def 2 :

for I being Program of SCM+FSA holds
( I is InitHalting iff Initialized I is halting );

:: deftheorem Def3 defines keepInt0_1 SCM_HALT:def 3 :

for I being Program of SCM+FSA holds
( I is keepInt0_1 iff 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 );

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 Relation-like NAT -defined the carrier of SCM+FSA -defined Function-like the Object-Kind of SCM+FSA -compatible V30() countable V101() InitHalting set ;
existence
ex b₁ being Program of SCM+FSA st b₁ is InitHalting 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

cluster Relation-like NAT -defined the carrier of SCM+FSA -defined Function-like the Object-Kind of SCM+FSA -compatible V30() V101() paraclosed -> InitClosed set ;
coherence
for b₁ being Program of SCM+FSA st b₁ is paraclosed holds
b₁ is InitClosed

proof end;

end;

registration

cluster Relation-like NAT -defined the carrier of SCM+FSA -defined Function-like the Object-Kind of SCM+FSA -compatible V30() V101() parahalting -> InitHalting set ;
coherence
for b₁ being Program of SCM+FSA st b₁ is parahalting holds
b₁ is InitHalting

proof end;

end;

registration

cluster Relation-like NAT -defined the carrier of SCM+FSA -defined Function-like the Object-Kind of SCM+FSA -compatible V30() V101() InitHalting -> InitClosed set ;
coherence
for b₁ being Program of SCM+FSA st b₁ is InitHalting holds
b₁ is InitClosed

proof end;

cluster Relation-like NAT -defined the carrier of SCM+FSA -defined Function-like the Object-Kind of SCM+FSA -compatible V30() V101() keepInt0_1 -> InitClosed set ;
coherence
for b₁ being Program of SCM+FSA st b₁ is keepInt0_1 holds
b₁ is InitClosed

proof end;

cluster Relation-like NAT -defined the carrier of SCM+FSA -defined Function-like the Object-Kind of SCM+FSA -compatible V30() V101() keeping_0 -> keepInt0_1 set ;
coherence
for b₁ being Program of SCM+FSA st b₁ is keeping_0 holds
b₁ is keepInt0_1

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
Initialized I is halting by Def2;

end;

registration

cluster Relation-like NAT -defined the carrier of SCM+FSA -defined Function-like the Object-Kind of SCM+FSA -compatible V30() V101() InitHalting -> non empty set ;
coherence
for b₁ being Program of SCM+FSA st b₁ is InitHalting holds
not b₁ is empty

proof end;

end;

theorem :: SCM_HALT:10

for I being InitHalting Program of SCM+FSA holds dom I <> {} ;

theorem Th11: :: SCM_HALT:11

for I being InitHalting Program of SCM+FSA holds 0 in dom I

proof end;

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 (Comput (ProgramPart s1),s1,i)),(Comput (ProgramPart s1),s1,i)),n = CurInstr (ProgramPart (Comput (ProgramPart s2),s2,i)),(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 (Comput (ProgramPart s1),s1,k)),(Comput (ProgramPart s1),s1,k) = CurInstr (ProgramPart (Comput (ProgramPart s2),s2,k)),(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 s1 = LifeSpan s2 & Result s1, Result s2 equal_outside NAT )

proof end;

registration

cluster Relation-like NAT -defined the carrier of SCM+FSA -defined Function-like the Object-Kind of SCM+FSA -compatible V30() countable V101() keeping_0 InitHalting set ;
existence
ex b₁ being Program of SCM+FSA st
( b₁ is keeping_0 & b₁ is InitHalting )

proof end;

end;

registration

cluster Relation-like NAT -defined the carrier of SCM+FSA -defined Function-like the Object-Kind of SCM+FSA -compatible V30() countable V101() InitHalting keepInt0_1 set ;
existence
ex b₁ being Program of SCM+FSA st
( b₁ is keepInt0_1 & b₁ is InitHalting )

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

cluster Relation-like NAT -defined the carrier of SCM+FSA -defined Function-like the Object-Kind of SCM+FSA -compatible V30() countable V101() InitClosed set ;
existence
ex b₁ being Program of SCM+FSA st b₁ is InitClosed

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 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 (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 (s +* I))) = DataPart (Comput (ProgramPart s),s,((LifeSpan (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 s holds
CurInstr (ProgramPart (Comput (ProgramPart (s +* (Directed I))),(s +* (Directed I)),k)),(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 (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

for I being InitHalting keepInt0_1 Program of SCM+FSA
for J being InitHalting Program of SCM+FSA
for s being State of SCM+FSA st Initialized (I ';' J) c= s holds
( IC (Comput (ProgramPart s),s,((LifeSpan (s +* I)) + 1)) = card I & DataPart (Comput (ProgramPart s),s,((LifeSpan (s +* I)) + 1)) = DataPart ((Comput (ProgramPart (s +* I)),(s +* I),(LifeSpan (s +* I))) +* (Initialized J)) & ProgramPart (Relocated J,(card I)) c= Comput (ProgramPart s),s,((LifeSpan (s +* I)) + 1) & (Comput (ProgramPart s),s,((LifeSpan (s +* I)) + 1)) . (intloc 0 ) = 1 & ProgramPart s halts_on s & LifeSpan s = ((LifeSpan (s +* I)) + 1) + (LifeSpan ((Result (s +* I)) +* (Initialized J))) & ( J is keeping_0 implies (Result s) . (intloc 0 ) = 1 ) )

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
I ';' J is InitHalting

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 (s +* I)) +* (Initialized J))),((Result (s +* I)) +* (Initialized J)),k) +* (Start-At ((IC (Comput (ProgramPart ((Result (s +* I)) +* (Initialized J))),((Result (s +* I)) +* (Initialized J)),k)) + (card I)),SCM+FSA ), Comput (ProgramPart (s +* (I ';' J))),(s +* (I ';' J)),(((LifeSpan (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 (s +* (Initialized (I ';' J))) = ((LifeSpan (s +* (Initialized I))) + 1) + (LifeSpan ((Result (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
Macro i is InitHalting ;

end;

registration

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

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
i ';' J is InitHalting ;

end;

registration

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

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
( I ';' j is InitHalting & I ';' j is keepInt0_1 ) ;

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
( i ';' J is InitHalting & i ';' J is keepInt0_1 ) ;

end;

registration

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

end;

registration

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

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

for I being Program of SCM+FSA
for s being State of SCM+FSA holds
( I is_closed_onInit s iff for k being Element of NAT holds IC (Comput (ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),k) in dom I );

:: deftheorem Def5 defines is_halting_onInit SCM_HALT:def 5 :

for I being Program of SCM+FSA
for s being State of SCM+FSA holds
( I is_halting_onInit s iff ProgramPart (s +* (Initialized I)) halts_on s +* (Initialized I) );

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 I does_not_destroy 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

cluster Relation-like NAT -defined the carrier of SCM+FSA -defined Function-like the Object-Kind of SCM+FSA -compatible V30() countable V101() good InitHalting set ;
existence
ex b₁ being Program of SCM+FSA st
( b₁ is InitHalting & b₁ is good )

proof end;

end;

registration

cluster Relation-like NAT -defined the carrier of SCM+FSA -defined Function-like the Object-Kind of SCM+FSA -compatible V30() V101() good InitClosed -> keepInt0_1 set ;
correctness
coherence
for b₁ being Program of SCM+FSA st b₁ is InitClosed & b₁ is good holds
b₁ is keepInt0_1 ;

proof end;

end;

registration

cluster Stop SCM+FSA -> good InitHalting ;
coherence
( Stop SCM+FSA is InitHalting & Stop SCM+FSA is good ) ;

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,(Initialize 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,(Initialize 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 Initialize 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 Initialize 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,(Initialize 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
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

for I being Program of SCM+FSA holds
( I is InitHalting iff for s being State of SCM+FSA holds I is_halting_on Initialize 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 Initialize 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 ((Initialize s) +* (I +* (Start-At 0 ,SCM+FSA )))),((Initialize s) +* (I +* (Start-At 0 ,SCM+FSA ))),(LifeSpan ((Initialize 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 I does_not_destroy a holds
(IExec I,s) . a = (Comput (ProgramPart ((Initialize s) +* (I +* (Start-At 0 ,SCM+FSA )))),((Initialize 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 I does_not_destroy a holds
(IExec I,s) . a = (Initialize 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 I does_not_destroy a holds
(Comput (ProgramPart ((Initialize s) +* ((I ';' (SubFrom a,(intloc 0 ))) +* (Start-At 0 ,SCM+FSA )))),((Initialize s) +* ((I ';' (SubFrom a,(intloc 0 ))) +* (Start-At 0 ,SCM+FSA ))),(LifeSpan ((Initialize 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 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 s holds
CurInstr (ProgramPart (Comput (ProgramPart (s +* (loop I))),(s +* (loop I)),k)),(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 (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 (s +* (Initialized I)) holds
CurInstr (ProgramPart (Comput (ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),m)),(Comput (ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),m) = CurInstr (ProgramPart (Comput (ProgramPart (s +* (Initialized (loop I)))),(s +* (Initialized (loop I))),m)),(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 (Comput (ProgramPart (s +* (Initialized (loop I)))),(s +* (Initialized (loop I))),(LifeSpan (s +* (Initialized I))))),(Comput (ProgramPart (s +* (Initialized (loop I)))),(s +* (Initialized (loop I))),(LifeSpan (s +* (Initialized I)))) = goto 0 & ( for m being Element of NAT st m <= LifeSpan (s +* (Initialized I)) holds
CurInstr (ProgramPart (Comput (ProgramPart (s +* (Initialized (loop I)))),(s +* (Initialized (loop I))),m)),(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 I does_not_destroy 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 I does_not_destroy 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 I does_not_destroy 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 I does_not_destroy 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
Times a,I is good

proof end;

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 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 2),(I ';' (SubFrom a,(intloc 0 )))))) & k = (LifeSpan (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 I does_not_destroy 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 = (Initialize 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 I does_not_destroy 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 I does_not_destroy 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 ;
attr i is good means :Def6: :: SCM_HALT:def 6
i does_not_destroy intloc 0 ;

end;

:: deftheorem Def6 defines good SCM_HALT:def 6 :

for i being Instruction of SCM+FSA holds
( i is good iff i does_not_destroy intloc 0 );

registration

cluster parahalting good Element of the Instructions of SCM+FSA ;
existence
ex b₁ being Instruction of SCM+FSA st
( b₁ is parahalting & b₁ is good )

proof end;

end;

registration

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

proof end;

cluster J ';' i -> good ;
coherence
J ';' i is good

proof end;

end;

registration

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

proof end;

end;

registration

let a be read-write Int-Location ;
let b be Int-Location ;
cluster a := b -> good ;
coherence
a := b is good

proof end;

cluster SubFrom a,b -> good ;
coherence
SubFrom a,b is good

proof end;

end;

registration

let a be read-write Int-Location ;
let b be Int-Location ;
let f be FinSeq-Location ;
cluster a := f,b -> good ;
coherence
a := f,b is good

proof end;

end;

registration

let a, b be Int-Location ;
let f be FinSeq-Location ;
cluster f,a := b -> good ;
coherence
f,a := b is good

proof end;

end;

registration

let a be read-write Int-Location ;
let f be FinSeq-Location ;
cluster a :=len f -> good ;
coherence
a :=len f is good

proof end;

end;

registration

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

proof end;

end;