:: SCM_HALT semantic presentation

definition

let I be Macro-Instruction;
attr I is InitClosed means :Def1: :: SCM_HALT:def 1
for s being State of SCM+FSA
for n being Nat st Initialized I c= s holds
IC ((Computation 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 Nat holds ((Computation 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 Nat holds
( not x in dom (((intloc i) .--> m) +* (Start-At (insloc n))) or x = intloc i or x = IC SCM+FSA )

proof end;

theorem Th2: :: SCM_HALT:2

for I being Macro-Instruction
for i, m, n being Nat holds dom I misses dom (((intloc i) .--> m) +* (Start-At (insloc n)))

proof end;

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

theorem Th3: :: SCM_HALT:3

for I being Macro-Instruction holds Initialized I = I +* (((intloc 0) .--> 1) +* (Start-At (insloc 0)))

proof end;

theorem Th4: :: SCM_HALT:4

Macro (halt SCM+FSA ) is InitHalting

proof end;

registration

cluster InitHalting FinPartState of SCM+FSA ;
existence by Th4;

end;

theorem Th5: :: SCM_HALT:5

for s being State of SCM+FSA
for I being InitHalting Macro-Instruction st Initialized I c= s holds
s is halting

proof end;

theorem Th6: :: SCM_HALT:6

for I being Macro-Instruction holds I +* (Start-At (insloc 0)) c= Initialized I

proof end;

theorem Th7: :: SCM_HALT:7

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

proof end;

registration

cluster paraclosed -> InitClosed FinPartState of SCM+FSA ;
coherence

proof end;

end;

registration

cluster parahalting -> InitHalting FinPartState of SCM+FSA ;
coherence

proof end;

end;

registration

cluster InitHalting -> InitClosed FinPartState of SCM+FSA ;
coherence

proof end;

cluster keepInt0_1 -> InitClosed FinPartState of SCM+FSA ;
coherence

proof end;

cluster keeping_0 -> keepInt0_1 FinPartState of SCM+FSA ;
coherence

proof end;

end;

theorem :: SCM_HALT:8

for s being State of SCM+FSA
for I being InitHalting Macro-Instruction
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 Macro-Instruction
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 Macro-Instruction;
cluster Initialized I -> halting ;
coherence by Def2;

end;

registration

cluster InitHalting -> non empty FinPartState of SCM+FSA ;
coherence

proof end;

end;

theorem Th10: :: SCM_HALT:10

for I being InitHalting Macro-Instruction holds dom I <> {}

proof end;

theorem Th11: :: SCM_HALT:11

for I being InitHalting Macro-Instruction holds insloc 0 in dom I

proof end;

theorem Th12: :: SCM_HALT:12

for s1, s2 being State of SCM+FSA
for J being InitHalting Macro-Instruction st Initialized J c= s1 holds
for n being Nat st ProgramPart (Relocated J,n) c= s2 & IC s2 = insloc n & s1 | (Int-Locations \/ FinSeq-Locations ) = s2 | (Int-Locations \/ FinSeq-Locations ) holds
for i being Nat holds
( (IC ((Computation s1) . i)) + n = IC ((Computation s2) . i) & IncAddr (CurInstr ((Computation s1) . i)),n = CurInstr ((Computation s2) . i) & ((Computation s1) . i) | (Int-Locations \/ FinSeq-Locations ) = ((Computation s2) . i) | (Int-Locations \/ FinSeq-Locations ) )

proof end;

theorem Th13: :: SCM_HALT:13

for I being Macro-Instruction
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 Macro-Instruction st Initialized I c= s1 & Initialized I c= s2 & s1,s2 equal_outside the Instruction-Locations of SCM+FSA holds
for k being Nat holds
( (Computation s1) . k,(Computation s2) . k equal_outside the Instruction-Locations of SCM+FSA & CurInstr ((Computation s1) . k) = CurInstr ((Computation s2) . k) )

proof end;

theorem Th15: :: SCM_HALT:15

for s1, s2 being State of SCM+FSA
for I being InitHalting Macro-Instruction st Initialized I c= s1 & Initialized I c= s2 & s1,s2 equal_outside the Instruction-Locations of SCM+FSA holds
( LifeSpan s1 = LifeSpan s2 & Result s1, Result s2 equal_outside the Instruction-Locations of SCM+FSA )

proof end;

registration

cluster non empty keeping_0 InitClosed InitHalting keepInt0_1 FinPartState of SCM+FSA ;
existence

proof end;

end;

registration

cluster non empty InitClosed InitHalting keepInt0_1 FinPartState of SCM+FSA ;
existence

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 Macro-Instruction holds (IExec I,s) . (intloc 0) = 1

proof end;

theorem Th18: :: SCM_HALT:18

for s being State of SCM+FSA
for I being InitClosed Macro-Instruction
for J being Macro-Instruction st Initialized I c= s & s is halting holds
for m being Nat st m <= LifeSpan s holds
(Computation s) . m,(Computation (s +* (I ';' J))) . m equal_outside the Instruction-Locations of SCM+FSA

proof end;

theorem Th19: :: SCM_HALT:19

for I being Macro-Instruction
for s being State of SCM+FSA
for i, m, n being Nat holds (s +* I) +* (((intloc i) .--> m) +* (Start-At (insloc n))) = (s +* (((intloc i) .--> m) +* (Start-At (insloc n)))) +* I

proof end;

theorem Th20: :: SCM_HALT:20

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

proof end;

theorem Th21: :: SCM_HALT:21

for s being State of SCM+FSA
for I being InitClosed Macro-Instruction st s +* I is halting & Directed I c= s & ((intloc 0) .--> 1) +* (Start-At (insloc 0)) c= s holds
IC ((Computation s) . ((LifeSpan (s +* I)) + 1)) = insloc (card I)

proof end;

theorem Th22: :: SCM_HALT:22

for s being State of SCM+FSA
for I being InitClosed Macro-Instruction st s +* I is halting & Directed I c= s & ((intloc 0) .--> 1) +* (Start-At (insloc 0)) c= s holds
((Computation s) . (LifeSpan (s +* I))) | (Int-Locations \/ FinSeq-Locations ) = ((Computation s) . ((LifeSpan (s +* I)) + 1)) | (Int-Locations \/ FinSeq-Locations )

proof end;

theorem Th23: :: SCM_HALT:23

for s being State of SCM+FSA
for I being InitHalting Macro-Instruction st Initialized I c= s holds
for k being Nat st k <= LifeSpan s holds
CurInstr ((Computation (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 Macro-Instruction st s +* (Initialized I) is halting holds
for J being Macro-Instruction
for k being Nat st k <= LifeSpan (s +* (Initialized I)) holds
(Computation (s +* (Initialized I))) . k,(Computation (s +* (Initialized (I ';' J)))) . k equal_outside the Instruction-Locations of SCM+FSA

proof end;

theorem Th25: :: SCM_HALT:25

for I being InitHalting keepInt0_1 Macro-Instruction
for J being InitHalting Macro-Instruction
for s being State of SCM+FSA st Initialized (I ';' J) c= s holds
( IC ((Computation s) . ((LifeSpan (s +* I)) + 1)) = insloc (card I) & ((Computation s) . ((LifeSpan (s +* I)) + 1)) | (Int-Locations \/ FinSeq-Locations ) = (((Computation (s +* I)) . (LifeSpan (s +* I))) +* (Initialized J)) | (Int-Locations \/ FinSeq-Locations ) & ProgramPart (Relocated J,(card I)) c= (Computation s) . ((LifeSpan (s +* I)) + 1) & ((Computation s) . ((LifeSpan (s +* I)) + 1)) . (intloc 0) = 1 & s is halting & 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 Macro-Instruction;
let J be InitHalting Macro-Instruction;
cluster I ';' J -> non empty InitClosed InitHalting ;
coherence

proof end;

end;

theorem Th26: :: SCM_HALT:26

for s being State of SCM+FSA
for I being keepInt0_1 Macro-Instruction st s +* I is halting holds
for J being InitClosed Macro-Instruction st Initialized (I ';' J) c= s holds
for k being Nat holds ((Computation ((Result (s +* I)) +* (Initialized J))) . k) +* (Start-At ((IC ((Computation ((Result (s +* I)) +* (Initialized J))) . k)) + (card I))),(Computation (s +* (I ';' J))) . (((LifeSpan (s +* I)) + 1) + k) equal_outside the Instruction-Locations of SCM+FSA

proof end;

theorem Th27: :: SCM_HALT:27

for s being State of SCM+FSA
for I being keepInt0_1 Macro-Instruction st not s +* (Initialized I) is halting holds
for J being Macro-Instruction
for k being Nat holds (Computation (s +* (Initialized I))) . k,(Computation (s +* (Initialized (I ';' J)))) . k equal_outside the Instruction-Locations of SCM+FSA

proof end;

theorem Th28: :: SCM_HALT:28

for s being State of SCM+FSA
for I being InitHalting keepInt0_1 Macro-Instruction
for J being InitHalting Macro-Instruction 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 Macro-Instruction
for J being InitHalting Macro-Instruction holds IExec (I ';' J),s = (IExec J,(IExec I,s)) +* (Start-At ((IC (IExec J,(IExec I,s))) + (card I)))

proof end;

registration

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

end;

registration

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

end;

registration

let i be parahalting keeping_0 Instruction of SCM+FSA ;
let J be InitHalting Macro-Instruction;
cluster i ';' J -> non empty InitClosed InitHalting ;
coherence

proof end;

end;

registration

let I, J be keepInt0_1 Macro-Instruction;
cluster I ';' J -> InitClosed keepInt0_1 ;
coherence

proof end;

end;

registration

let j be parahalting keeping_0 Instruction of SCM+FSA ;
let I be InitHalting keepInt0_1 Macro-Instruction;
cluster I ';' j -> non empty InitClosed InitHalting keepInt0_1 ;
coherence

proof end;

end;

registration

let i be parahalting keeping_0 Instruction of SCM+FSA ;
let J be InitHalting keepInt0_1 Macro-Instruction;
cluster i ';' J -> non empty InitClosed InitHalting keepInt0_1 ;
coherence

proof end;

end;

registration

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

end;

registration

let i, j be parahalting Instruction of SCM+FSA ;
cluster i ';' j -> InitClosed 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 Macro-Instruction
for J being InitHalting Macro-Instruction 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 Macro-Instruction
for J being InitHalting Macro-Instruction 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 Macro-Instruction
for s being State of SCM+FSA holds (Initialize (IExec I,s)) | (Int-Locations \/ FinSeq-Locations ) = (IExec I,s) | (Int-Locations \/ FinSeq-Locations )

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 Macro-Instruction
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 Macro-Instruction
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 Macro-Instruction;
let s be State of SCM+FSA ;
pred I is_closed_onInit s means :Def4: :: SCM_HALT:def 4
for k being Nat holds IC ((Computation (s +* (Initialized I))) . k) in dom I;
pred I is_halting_onInit s means :Def5: :: SCM_HALT:def 5
s +* (Initialized I) is halting;

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 Macro-Instruction 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 Macro-Instruction 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 Macro-Instruction
for a being Int-Location st I does_not_destroy a & I is_closed_onInit s & Initialized I c= s holds
for k being Nat holds ((Computation s) . k) . a = s . a

proof end;

registration

cluster non empty good InitClosed InitHalting FinPartState of SCM+FSA ;
existence

proof end;

end;

registration

cluster good InitClosed -> InitClosed keepInt0_1 FinPartState of SCM+FSA ;
correctness

proof end;

end;

registration

cluster SCM+FSA-Stop -> good InitClosed InitHalting keepInt0_1 ;
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 Macro-Instruction
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 Macro-Instruction
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 Macro-Instruction 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 Macro-Instruction holds
( I is_halting_onInit s iff I is_halting_on Initialize s )

proof end;

theorem :: SCM_HALT:42

for I being Macro-Instruction
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 Macro-Instruction
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 Macro-Instruction
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 (insloc (((card I) + (card J)) + 3)))

proof end;

theorem Th45: :: SCM_HALT:45

for s being State of SCM+FSA
for I, J being Macro-Instruction
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 Macro-Instruction
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 (insloc (((card I) + (card J)) + 3)))

proof end;

theorem Th47: :: SCM_HALT:47

for s being State of SCM+FSA
for I, J being InitHalting Macro-Instruction
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))) ) )

proof end;

theorem :: SCM_HALT:48

for s being State of SCM+FSA
for I, J being InitHalting Macro-Instruction
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 ) ) ) )

proof end;

theorem Th49: :: SCM_HALT:49

for s being State of SCM+FSA
for I, J being Macro-Instruction
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 Macro-Instruction
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 (insloc (((card I) + (card J)) + 3)))

proof end;

theorem Th51: :: SCM_HALT:51

for s being State of SCM+FSA
for I, J being Macro-Instruction
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 Macro-Instruction
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 (insloc (((card I) + (card J)) + 3)))

proof end;

theorem Th53: :: SCM_HALT:53

for s being State of SCM+FSA
for I, J being InitHalting Macro-Instruction
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))) ) )

proof end;

theorem :: SCM_HALT:54

for s being State of SCM+FSA
for I, J being InitHalting Macro-Instruction
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 ) ) ) )

proof end;

theorem Th55: :: SCM_HALT:55

for s being State of SCM+FSA
for I, J being Macro-Instruction
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 (insloc ((((card I) + (card J)) + (card J)) + 7)))

proof end;

theorem Th56: :: SCM_HALT:56

for s being State of SCM+FSA
for I, J being Macro-Instruction
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 (insloc ((((card I) + (card J)) + (card J)) + 7)))

proof end;

theorem Th57: :: SCM_HALT:57

for s being State of SCM+FSA
for I, J being Macro-Instruction
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 (insloc ((((card I) + (card J)) + (card J)) + 7)))

proof end;

theorem Th58: :: SCM_HALT:58

for s being State of SCM+FSA
for I, J being InitHalting Macro-Instruction
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))) ) )

proof end;

registration

let I, J be InitHalting Macro-Instruction;
let a be read-write Int-Location ;
cluster if=0 a,I,J -> non empty InitClosed InitHalting ;
correctness by Th47;
cluster if>0 a,I,J -> non empty InitClosed InitHalting ;
correctness by Th53;
cluster if<0 a,I,J -> non empty InitClosed InitHalting ;
correctness by Th58;

end;

theorem Th59: :: SCM_HALT:59

for I being Macro-Instruction 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 Macro-Instruction 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 Macro-Instruction
for a being read-write Int-Location holds (IExec I,s) . a = ((Computation ((Initialize s) +* (I +* (Start-At (insloc 0))))) . (LifeSpan ((Initialize s) +* (I +* (Start-At (insloc 0)))))) . a

proof end;

theorem Th62: :: SCM_HALT:62

for s being State of SCM+FSA
for I being InitHalting Macro-Instruction
for a being Int-Location
for k being Nat st I does_not_destroy a holds
(IExec I,s) . a = ((Computation ((Initialize s) +* (I +* (Start-At (insloc 0))))) . k) . a

proof end;

set A = the Instruction-Locations of SCM+FSA ;

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

theorem Th63: :: SCM_HALT:63

for s being State of SCM+FSA
for I being InitHalting Macro-Instruction
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 Macro-Instruction
for a being read-write Int-Location st I does_not_destroy a holds
((Computation ((Initialize s) +* ((I ';' (SubFrom a,(intloc 0))) +* (Start-At (insloc 0))))) . (LifeSpan ((Initialize s) +* ((I ';' (SubFrom a,(intloc 0))) +* (Start-At (insloc 0)))))) . a = (s . a) - 1

proof end;

theorem Th65: :: SCM_HALT:65

for s being State of SCM+FSA
for I being InitClosed Macro-Instruction st Initialized I c= s & s is halting holds
for m being Nat st m <= LifeSpan s holds
(Computation s) . m,(Computation (s +* (loop I))) . m equal_outside the Instruction-Locations of SCM+FSA

proof end;

theorem :: SCM_HALT:66

for s being State of SCM+FSA
for I being InitHalting Macro-Instruction st Initialized I c= s holds
for k being Nat st k <= LifeSpan s holds
CurInstr ((Computation (s +* (loop I))) . k) <> halt SCM+FSA

proof end;

theorem Th67: :: SCM_HALT:67

for I being Macro-Instruction
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 Macro-Instruction st I is_closed_onInit s & I is_halting_onInit s holds
for m being Nat st m <= LifeSpan (s +* (Initialized I)) holds
(Computation (s +* (Initialized I))) . m,(Computation (s +* (Initialized (loop I)))) . m equal_outside the Instruction-Locations of SCM+FSA

proof end;

theorem Th69: :: SCM_HALT:69

for s being State of SCM+FSA
for I being Macro-Instruction st I is_closed_onInit s & I is_halting_onInit s holds
for m being Nat st m < LifeSpan (s +* (Initialized I)) holds
CurInstr ((Computation (s +* (Initialized I))) . m) = CurInstr ((Computation (s +* (Initialized (loop I)))) . m)

proof end;

theorem Th70: :: SCM_HALT:70

for l being Instruction-Location of SCM+FSA holds not l in dom (((intloc 0) .--> 1) +* (Start-At (insloc 0)))

proof end;

theorem Th71: :: SCM_HALT:71

for s being State of SCM+FSA
for I being Macro-Instruction st I is_closed_onInit s & I is_halting_onInit s holds
( CurInstr ((Computation (s +* (Initialized (loop I)))) . (LifeSpan (s +* (Initialized I)))) = goto (insloc 0) & ( for m being Nat st m <= LifeSpan (s +* (Initialized I)) holds
CurInstr ((Computation (s +* (Initialized (loop I)))) . m) <> halt SCM+FSA ) )

proof end;

theorem :: SCM_HALT:72

for s being State of SCM+FSA
for I being Macro-Instruction st I is_closed_onInit s & I is_halting_onInit s holds
CurInstr ((Computation (s +* (Initialized (loop I)))) . (LifeSpan (s +* (Initialized I)))) = goto (insloc 0) by Th71;

theorem Th73: :: SCM_HALT:73

for s being State of SCM+FSA
for I being good InitHalting Macro-Instruction
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 (insloc 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 Macro-Instruction
for a being read-write Int-Location st I does_not_destroy a & s . a > 0 holds
Initialized (loop (if=0 a,(Goto (insloc 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 Macro-Instruction
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 Macro-Instruction
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 Macro-Instruction;
cluster Times a,I -> good ;
coherence

proof end;

end;

theorem Th77: :: SCM_HALT:77

for s being State of SCM+FSA
for I being good InitHalting Macro-Instruction
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 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 Nat st n <= k holds
IC ((Computation s2) . n) in dom (loop (if=0 a,(Goto (insloc 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 Macro-Instruction
for a being read-write Int-Location st s . (intloc 0) = 1 & s . a <= 0 holds
(IExec (Times a,I),s) | (Int-Locations \/ FinSeq-Locations ) = s | (Int-Locations \/ FinSeq-Locations )

proof end;

Lm1: for a being Int-Location
for l being Instruction-Location of SCM+FSA
for ic being Instruction of SCM+FSA st ( ic = a =0_goto l or ic = goto l ) holds
ic <> halt SCM+FSA
by SCMFSA_2:47, SCMFSA_2:48, SCMFSA_2:124;

theorem Th79: :: SCM_HALT:79

for s being State of SCM+FSA
for I being good InitHalting Macro-Instruction
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 & (IExec (Times a,I),s) | (Int-Locations \/ FinSeq-Locations ) = (IExec (Times a,I),(IExec (I ';' (SubFrom a,(intloc 0))),s)) | (Int-Locations \/ FinSeq-Locations ) )

proof end;

theorem :: SCM_HALT:80

for s being State of SCM+FSA
for I being good InitHalting Macro-Instruction
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 Macro-Instruction
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 Macro-Instruction
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 Macro-Instruction
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 :

registration

cluster parahalting good M3(the Instructions of SCM+FSA );
existence

proof end;

end;

registration

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

proof end;

cluster J ';' i -> good ;
coherence

proof end;

end;

registration

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

proof end;

end;

registration

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

proof end;

cluster SubFrom a,b -> good ;
coherence

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

proof end;

end;

registration

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

proof end;

end;

registration

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

proof end;

end;

registration

let n be Nat;
cluster intloc (n + 1) -> read-write ;
coherence

proof end;

end;