:: Initialization Halting Concepts and Their Basic Properties of SCM+FSA
:: by JingChao Chen and Yatsuka Nakamura
::
:: Copyright (c) 1998-2021 Association of Mizar Users

set SA0 = Start-At (0,SCM+FSA);

set iS = Initialize (() .--> 1);

reconsider EP = {} as PartState of SCM+FSA by ;

Lm1: IC (Initialize (() .--> 1)) = 0
by MEMSTR_0:def 11;

Lm2: dom (Initialize (() .--> 1)) = (dom (() .--> 1)) \/ (dom ()) by FUNCT_4:def 1
.= {()} \/ (dom ())
.= {()} \/ {()} ;

canceled;

::$CD definition let I be Program of SCM+FSA; attr I is InitHalting means :Def1: :: SCM_HALT:def 1 for s being State of SCM+FSA st Initialize (() .--> 1) c= s holds for P being Instruction-Sequence of SCM+FSA st I c= P holds P halts_on s; attr I is keepInt0_1 means :Def2: :: SCM_HALT:def 2 for s being State of SCM+FSA st Initialize (() .--> 1) c= s holds for p being Instruction-Sequence of SCM+FSA st I c= p holds for k being Nat holds (Comput (p,s,k)) . () = 1; end; :: deftheorem Def1 defines InitHalting SCM_HALT:def 1 : for I being Program of SCM+FSA holds ( I is InitHalting iff for s being State of SCM+FSA st Initialize (() .--> 1) c= s holds for P being Instruction-Sequence of SCM+FSA st I c= P holds P halts_on s ); :: deftheorem Def2 defines keepInt0_1 SCM_HALT:def 2 : for I being Program of SCM+FSA holds ( I is keepInt0_1 iff for s being State of SCM+FSA st Initialize (() .--> 1) c= s holds for p being Instruction-Sequence of SCM+FSA st I c= p holds for k being Nat holds (Comput (p,s,k)) . () = 1 ); theorem :: SCM_HALT:1 canceled; ::$CT
theorem Th1: :: SCM_HALT:2
proof end;

registration
existence
ex b1 being Program of SCM+FSA st b1 is InitHalting
by Th1;
end;

registration
coherence
for b1 being Program of SCM+FSA st b1 is parahalting holds
b1 is InitHalting
proof end;
end;

registration
coherence
for b1 being Program of SCM+FSA st b1 is keeping_0 holds
b1 is keepInt0_1
proof end;
end;

theorem :: SCM_HALT:3
canceled;

::$CT theorem :: SCM_HALT:4 for s being State of SCM+FSA for p being Instruction-Sequence of SCM+FSA for I being really-closed InitHalting Program of SCM+FSA for a being read-write Int-Location st not a in UsedILoc I holds (IExec (I,p,s)) . a = s . a proof end; theorem :: SCM_HALT:5 for s being State of SCM+FSA for p being Instruction-Sequence of SCM+FSA for I being really-closed InitHalting Program of SCM+FSA for f being FinSeq-Location st not f in UsedI*Loc I holds (IExec (I,p,s)) . f = s . f proof end; registration coherence for b1 being Program of SCM+FSA st b1 is InitHalting holds not b1 is empty ; end; theorem Th4: :: SCM_HALT:6 for s1, s2 being State of SCM+FSA for p1, p2 being Instruction-Sequence of SCM+FSA for J being really-closed InitHalting Program of SCM+FSA st Initialize (() .--> 1) c= s1 & J c= p1 holds for n being Nat st Reloc (J,n) c= p2 & IC s2 = n & DataPart s1 = DataPart s2 holds for i being Nat holds ( (IC (Comput (p1,s1,i))) + n = IC (Comput (p2,s2,i)) & IncAddr ((CurInstr (p1,(Comput (p1,s1,i)))),n) = CurInstr (p2,(Comput (p2,s2,i))) & DataPart (Comput (p1,s1,i)) = DataPart (Comput (p2,s2,i)) ) proof end; theorem Th5: :: SCM_HALT:7 for s1, s2 being State of SCM+FSA for p1, p2 being Instruction-Sequence of SCM+FSA for I being really-closed InitHalting Program of SCM+FSA st Initialize (() .--> 1) c= s1 & Initialize (() .--> 1) c= s2 & I c= p1 & I c= p2 & s1 = s2 holds for k being Nat holds ( Comput (p1,s1,k) = Comput (p2,s2,k) & CurInstr (p1,(Comput (p1,s1,k))) = CurInstr (p2,(Comput (p2,s2,k))) ) proof end; theorem Th6: :: SCM_HALT:8 for s1, s2 being State of SCM+FSA for p1, p2 being Instruction-Sequence of SCM+FSA for I being really-closed InitHalting Program of SCM+FSA st Initialize (() .--> 1) c= s1 & Initialize (() .--> 1) c= s2 & I c= p1 & I c= p2 & s1 = s2 holds ( LifeSpan (p1,s1) = LifeSpan (p2,s2) & Result (p1,s1) = Result (p2,s2) ) proof end; registration existence ex b1 being Program of SCM+FSA st ( b1 is keeping_0 & b1 is InitHalting ) proof end; end; registration existence ex b1 being really-closed Program of SCM+FSA st ( b1 is keepInt0_1 & b1 is InitHalting ) proof end; end; theorem Th7: :: SCM_HALT:9 for s being State of SCM+FSA for p being Instruction-Sequence of SCM+FSA for I being InitHalting keepInt0_1 Program of SCM+FSA holds (IExec (I,p,s)) . () = 1 proof end; theorem Th8: :: SCM_HALT:10 for s being State of SCM+FSA for p being Instruction-Sequence of SCM+FSA for I being really-closed Program of SCM+FSA for J being Program of SCM+FSA st Initialize (() .--> 1) c= s & I c= p & p halts_on s holds for m being Nat st m <= LifeSpan (p,s) holds Comput (p,s,m) = Comput ((p +* (I ";" J)),s,m) proof end; theorem Th9: :: SCM_HALT:11 for s being State of SCM+FSA for p being Instruction-Sequence of SCM+FSA for I being really-closed Program of SCM+FSA st p +* I halts_on s & Directed I c= p & Initialize (() .--> 1) c= s holds IC (Comput (p,s,((LifeSpan ((p +* I),s)) + 1))) = card I proof end; theorem Th10: :: SCM_HALT:12 for s being State of SCM+FSA for p being Instruction-Sequence of SCM+FSA for I being really-closed Program of SCM+FSA st p +* I halts_on s & Directed I c= p & Initialize (() .--> 1) c= s holds DataPart (Comput (p,s,(LifeSpan ((p +* I),s)))) = DataPart (Comput (p,s,((LifeSpan ((p +* I),s)) + 1))) proof end; theorem Th11: :: SCM_HALT:13 for s being State of SCM+FSA for p being Instruction-Sequence of SCM+FSA for I being really-closed InitHalting Program of SCM+FSA st Initialize (() .--> 1) c= s & I c= p holds for k being Nat st k <= LifeSpan (p,s) holds CurInstr ((p +* ()),(Comput ((p +* ()),s,k))) <> halt SCM+FSA proof end; theorem Th12: :: SCM_HALT:14 for s being State of SCM+FSA for p being Instruction-Sequence of SCM+FSA for I being really-closed Program of SCM+FSA st p +* I halts_on Initialized s holds for J being Program of SCM+FSA for k being Nat st k <= LifeSpan ((p +* I),()) holds Comput ((p +* I),(),k) = Comput ((p +* (I ";" J)),(),k) proof end; theorem Th13: :: SCM_HALT:15 for p being Instruction-Sequence of SCM+FSA for I being really-closed InitHalting keepInt0_1 Program of SCM+FSA for J being really-closed InitHalting Program of SCM+FSA for s being State of SCM+FSA st Initialize (() .--> 1) c= s & I ";" J c= p holds ( IC (Comput (p,s,((LifeSpan ((p +* I),s)) + 1))) = card I & DataPart (Comput (p,s,((LifeSpan ((p +* I),s)) + 1))) = DataPart ((Comput ((p +* I),s,(LifeSpan ((p +* I),s)))) +* (Initialize (() .--> 1))) & Reloc (J,(card I)) c= p & (Comput (p,s,((LifeSpan ((p +* I),s)) + 1))) . () = 1 & p halts_on s & LifeSpan (p,s) = ((LifeSpan ((p +* I),s)) + 1) + (LifeSpan (((p +* I) +* J),((Result ((p +* I),s)) +* (Initialize (() .--> 1))))) & ( J is keeping_0 implies (Result (p,s)) . () = 1 ) ) proof end; registration let I be really-closed InitHalting keepInt0_1 Program of SCM+FSA; let J be really-closed InitHalting Program of SCM+FSA; coherence I ";" J is InitHalting proof end; end; theorem Th14: :: SCM_HALT:16 for s being State of SCM+FSA for p being Instruction-Sequence of SCM+FSA for I being really-closed keepInt0_1 Program of SCM+FSA st p +* I halts_on s holds for J being really-closed Program of SCM+FSA st Initialize (() .--> 1) c= s & I ";" J c= p holds for k being Element of NAT holds (Comput (((p +* I) +* J),((Result ((p +* I),s)) +* (Initialize (() .--> 1))),k)) +* (Start-At (((IC (Comput (((p +* I) +* J),((Result ((p +* I),s)) +* (Initialize (() .--> 1))),k))) + (card I)),SCM+FSA)) = Comput ((p +* (I ";" J)),s,(((LifeSpan ((p +* I),s)) + 1) + k)) proof end; theorem Th15: :: SCM_HALT:17 for s being State of SCM+FSA for p being Instruction-Sequence of SCM+FSA for I being really-closed keepInt0_1 Program of SCM+FSA st not p +* I halts_on Initialized s holds for J being Program of SCM+FSA for k being Nat holds Comput ((p +* I),(),k) = Comput ((p +* (I ";" J)),(),k) proof end; theorem Th16: :: SCM_HALT:18 for s being State of SCM+FSA for p being Instruction-Sequence of SCM+FSA for I being really-closed InitHalting keepInt0_1 Program of SCM+FSA for J being really-closed InitHalting Program of SCM+FSA holds LifeSpan ((p +* (I ";" J)),()) = ((LifeSpan ((p +* I),())) + 1) + (LifeSpan (((p +* I) +* J),((Result ((p +* I),())) +* (Initialize (() .--> 1))))) proof end; theorem Th17: :: SCM_HALT:19 for s being State of SCM+FSA for p being Instruction-Sequence of SCM+FSA for I being really-closed InitHalting keepInt0_1 Program of SCM+FSA for J being really-closed InitHalting Program of SCM+FSA holds IExec ((I ";" J),p,s) = IncIC ((IExec (J,p,(IExec (I,p,s)))),(card I)) proof end; registration let i be sequential Instruction of SCM+FSA; coherence ; end; registration let i be sequential Instruction of SCM+FSA; let J be really-closed parahalting Program of SCM+FSA; coherence i ";" J is InitHalting ; end; registration let i be keeping_0 sequential Instruction of SCM+FSA; let J be really-closed InitHalting Program of SCM+FSA; coherence i ";" J is InitHalting ; end; registration let I, J be really-closed keepInt0_1 Program of SCM+FSA; cluster I ";" J -> keepInt0_1 ; coherence I ";" J is keepInt0_1 proof end; end; registration let j be keeping_0 sequential Instruction of SCM+FSA; let I be really-closed InitHalting keepInt0_1 Program of SCM+FSA; coherence ( I ";" j is InitHalting & I ";" j is keepInt0_1 ) ; end; registration let i be keeping_0 sequential Instruction of SCM+FSA; let J be really-closed InitHalting keepInt0_1 Program of SCM+FSA; coherence ( i ";" J is InitHalting & i ";" J is keepInt0_1 ) ; end; registration let j be sequential Instruction of SCM+FSA; let I be really-closed parahalting Program of SCM+FSA; coherence I ";" j is InitHalting ; end; registration let i, j be sequential Instruction of SCM+FSA; coherence i ";" j is InitHalting ; end; theorem Th18: :: SCM_HALT:20 for s being State of SCM+FSA for a being Int-Location for p being Instruction-Sequence of SCM+FSA for I being really-closed InitHalting keepInt0_1 Program of SCM+FSA for J being really-closed InitHalting Program of SCM+FSA holds (IExec ((I ";" J),p,s)) . a = (IExec (J,p,(IExec (I,p,s)))) . a proof end; theorem Th19: :: SCM_HALT:21 for s being State of SCM+FSA for f being FinSeq-Location for p being Instruction-Sequence of SCM+FSA for I being really-closed InitHalting keepInt0_1 Program of SCM+FSA for J being really-closed InitHalting Program of SCM+FSA holds (IExec ((I ";" J),p,s)) . f = (IExec (J,p,(IExec (I,p,s)))) . f proof end; theorem Th20: :: SCM_HALT:22 for p being Instruction-Sequence of SCM+FSA for I being InitHalting keepInt0_1 Program of SCM+FSA for s being State of SCM+FSA holds DataPart (Initialized (IExec (I,p,s))) = DataPart (IExec (I,p,s)) proof end; theorem Th21: :: SCM_HALT:23 for s being State of SCM+FSA for a being Int-Location for p being Instruction-Sequence of SCM+FSA for I being really-closed InitHalting keepInt0_1 Program of SCM+FSA for j being sequential Instruction of SCM+FSA holds (IExec ((I ";" j),p,s)) . a = (Exec (j,(IExec (I,p,s)))) . a proof end; theorem :: SCM_HALT:24 for s being State of SCM+FSA for f being FinSeq-Location for p being Instruction-Sequence of SCM+FSA for I being really-closed InitHalting keepInt0_1 Program of SCM+FSA for j being sequential Instruction of SCM+FSA holds (IExec ((I ";" j),p,s)) . f = (Exec (j,(IExec (I,p,s)))) . f proof end; definition let I be Program of SCM+FSA; let s be State of SCM+FSA; let p be Instruction-Sequence of SCM+FSA; end; :: deftheorem defines is_halting_onInit SCM_HALT:def 3 : for I being Program of SCM+FSA for s being State of SCM+FSA for p being Instruction-Sequence of SCM+FSA holds ( I is_halting_onInit s,p iff p +* I halts_on Initialized s ); canceled; theorem :: SCM_HALT:25 canceled; ::$CD
::$CT theorem Th23: :: SCM_HALT:26 for I being Program of SCM+FSA holds ( I is InitHalting iff for s being State of SCM+FSA for p being Instruction-Sequence of SCM+FSA holds I is_halting_onInit s,p ) proof end; theorem :: SCM_HALT:27 for p being Instruction-Sequence of SCM+FSA for s being State of SCM+FSA for I being really-closed Program of SCM+FSA for a being Int-Location st not I destroys a & Initialize (() .--> 1) c= s & I c= p holds for k being Nat holds (Comput (p,s,k)) . a = s . a proof end; registration existence ex b1 being Program of SCM+FSA st ( b1 is InitHalting & b1 is good ) proof end; end; registration correctness coherence for b1 being Program of SCM+FSA st b1 is really-closed & b1 is good holds b1 is keepInt0_1 ; ; end; registration coherence ; end; theorem :: SCM_HALT:28 for p being Instruction-Sequence of SCM+FSA for s being State of SCM+FSA for i being keeping_0 sequential Instruction of SCM+FSA for J being really-closed InitHalting Program of SCM+FSA for a being Int-Location holds (IExec ((i ";" J),p,s)) . a = (IExec (J,p,(Exec (i,())))) . a proof end; theorem :: SCM_HALT:29 for p being Instruction-Sequence of SCM+FSA for s being State of SCM+FSA for i being keeping_0 sequential Instruction of SCM+FSA for J being really-closed InitHalting Program of SCM+FSA for f being FinSeq-Location holds (IExec ((i ";" J),p,s)) . f = (IExec (J,p,(Exec (i,())))) . f proof end; theorem :: SCM_HALT:30 canceled; ::$CT
theorem Th27: :: SCM_HALT:31
for p being Instruction-Sequence of SCM+FSA
for s being State of SCM+FSA
for I being Program of SCM+FSA holds
( I is_halting_onInit s,p iff I is_halting_on Initialized s,p ) by MEMSTR_0:44;

theorem :: SCM_HALT:32
for p being Instruction-Sequence of SCM+FSA
for I being Program of SCM+FSA
for s being State of SCM+FSA holds IExec (I,p,s) = IExec (I,p,())
proof end;

theorem Th29: :: SCM_HALT:33
for p being Instruction-Sequence of SCM+FSA
for s being State of SCM+FSA
for I being really-closed MacroInstruction of SCM+FSA
for J being MacroInstruction of SCM+FSA
for a being read-write Int-Location st s . a = 0 & I is_halting_onInit s,p holds
if=0 (a,I,J) is_halting_onInit s,p
proof end;

theorem Th30: :: SCM_HALT:34
for p being Instruction-Sequence of SCM+FSA
for s being State of SCM+FSA
for I being really-closed MacroInstruction of SCM+FSA
for J being MacroInstruction of SCM+FSA
for a being read-write Int-Location st s . a = 0 & I is_halting_onInit s,p holds
IExec ((if=0 (a,I,J)),p,s) = (IExec (I,p,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA)) by ;

theorem Th31: :: SCM_HALT:35
for p being Instruction-Sequence of SCM+FSA
for s being State of SCM+FSA
for I, J being really-closed MacroInstruction of SCM+FSA
for a being read-write Int-Location st s . a <> 0 & J is_halting_onInit s,p holds
if=0 (a,I,J) is_halting_onInit s,p
proof end;

theorem Th32: :: SCM_HALT:36
for p being Instruction-Sequence of SCM+FSA
for I, J being really-closed MacroInstruction of SCM+FSA
for s being State of SCM+FSA st s . a <> 0 & J is_halting_onInit s,p holds
IExec ((if=0 (a,I,J)),p,s) = (IExec (J,p,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA)) by ;

theorem Th33: :: SCM_HALT:37
for p being Instruction-Sequence of SCM+FSA
for s being State of SCM+FSA
for I, J being really-closed InitHalting MacroInstruction 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)),p,s) = (IExec (I,p,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA)) ) & ( s . a <> 0 implies IExec ((if=0 (a,I,J)),p,s) = (IExec (J,p,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA)) ) )
proof end;

theorem :: SCM_HALT:38
for p being Instruction-Sequence of SCM+FSA
for s being State of SCM+FSA
for I, J being really-closed InitHalting MacroInstruction of SCM+FSA
for a being read-write Int-Location holds
( IC (IExec ((if=0 (a,I,J)),p,s)) = ((card I) + (card J)) + 3 & ( s . a = 0 implies ( ( for d being Int-Location holds (IExec ((if=0 (a,I,J)),p,s)) . d = (IExec (I,p,s)) . d ) & ( for f being FinSeq-Location holds (IExec ((if=0 (a,I,J)),p,s)) . f = (IExec (I,p,s)) . f ) ) ) & ( s . a <> 0 implies ( ( for d being Int-Location holds (IExec ((if=0 (a,I,J)),p,s)) . d = (IExec (J,p,s)) . d ) & ( for f being FinSeq-Location holds (IExec ((if=0 (a,I,J)),p,s)) . f = (IExec (J,p,s)) . f ) ) ) )
proof end;

theorem Th35: :: SCM_HALT:39
for p being Instruction-Sequence of SCM+FSA
for s being State of SCM+FSA
for I, J being really-closed MacroInstruction of SCM+FSA
for a being read-write Int-Location st s . a > 0 & I is_halting_onInit s,p holds
if>0 (a,I,J) is_halting_onInit s,p
proof end;

theorem Th36: :: SCM_HALT:40
for p being Instruction-Sequence of SCM+FSA
for s being State of SCM+FSA
for I, J being really-closed MacroInstruction of SCM+FSA
for a being read-write Int-Location st s . a > 0 & I is_halting_onInit s,p holds
IExec ((if>0 (a,I,J)),p,s) = (IExec (I,p,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA)) by ;

theorem Th37: :: SCM_HALT:41
for p being Instruction-Sequence of SCM+FSA
for s being State of SCM+FSA
for I, J being really-closed MacroInstruction of SCM+FSA
for a being read-write Int-Location st s . a <= 0 & J is_halting_onInit s,p holds
if>0 (a,I,J) is_halting_onInit s,p
proof end;

theorem Th38: :: SCM_HALT:42
for p being Instruction-Sequence of SCM+FSA
for I, J being really-closed MacroInstruction of SCM+FSA
for s being State of SCM+FSA st s . a <= 0 & J is_halting_onInit s,p holds
IExec ((if>0 (a,I,J)),p,s) = (IExec (J,p,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA)) by ;

theorem Th39: :: SCM_HALT:43
for p being Instruction-Sequence of SCM+FSA
for s being State of SCM+FSA
for I, J being really-closed InitHalting MacroInstruction 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)),p,s) = (IExec (I,p,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA)) ) & ( s . a <= 0 implies IExec ((if>0 (a,I,J)),p,s) = (IExec (J,p,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA)) ) )
proof end;

theorem :: SCM_HALT:44
for p being Instruction-Sequence of SCM+FSA
for s being State of SCM+FSA
for I, J being really-closed InitHalting MacroInstruction of SCM+FSA
for a being read-write Int-Location holds
( IC (IExec ((if>0 (a,I,J)),p,s)) = ((card I) + (card J)) + 3 & ( s . a > 0 implies ( ( for d being Int-Location holds (IExec ((if>0 (a,I,J)),p,s)) . d = (IExec (I,p,s)) . d ) & ( for f being FinSeq-Location holds (IExec ((if>0 (a,I,J)),p,s)) . f = (IExec (I,p,s)) . f ) ) ) & ( s . a <= 0 implies ( ( for d being Int-Location holds (IExec ((if>0 (a,I,J)),p,s)) . d = (IExec (J,p,s)) . d ) & ( for f being FinSeq-Location holds (IExec ((if>0 (a,I,J)),p,s)) . f = (IExec (J,p,s)) . f ) ) ) )
proof end;

theorem :: SCM_HALT:45
canceled;

theorem :: SCM_HALT:46
canceled;

theorem :: SCM_HALT:47
canceled;

theorem :: SCM_HALT:48
canceled;

::$CT 4 registration let I, J be really-closed InitHalting MacroInstruction 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 Th33; cluster if>0 (a,I,J) -> InitHalting ; correctness coherence if>0 (a,I,J) is InitHalting ; by Th39; end; theorem Th41: :: SCM_HALT:49 for I being Program of SCM+FSA holds ( I is InitHalting iff for s being State of SCM+FSA for p being Instruction-Sequence of SCM+FSA holds I is_halting_on Initialized s,p ) proof end; theorem :: SCM_HALT:50 canceled; ::$CT
theorem Th42: :: SCM_HALT:51
for p being Instruction-Sequence of SCM+FSA
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,p,s)) . a = (Comput ((p +* I),(),(LifeSpan ((p +* I),())))) . a
proof end;

theorem Th43: :: SCM_HALT:52
for p being Instruction-Sequence of SCM+FSA
for s being State of SCM+FSA
for I being really-closed InitHalting Program of SCM+FSA
for a being Int-Location
for k being Element of NAT st not I destroys a holds
(IExec (I,p,s)) . a = (Comput ((p +* I),(),k)) . a by ;

set A = NAT ;

set D = Data-Locations ;

theorem Th44: :: SCM_HALT:53
for p being Instruction-Sequence of SCM+FSA
for s being State of SCM+FSA
for I being really-closed InitHalting Program of SCM+FSA
for a being Int-Location st not I destroys a holds
(IExec (I,p,s)) . a = () . a
proof end;

theorem :: SCM_HALT:54
for p being Instruction-Sequence of SCM+FSA
for s being State of SCM+FSA
for I being really-closed InitHalting keepInt0_1 Program of SCM+FSA
for a being read-write Int-Location st not I destroys a holds
(Comput ((p +* (I ";" (SubFrom (a,())))),(),(LifeSpan ((p +* (I ";" (SubFrom (a,())))),())))) . a = (s . a) - 1
proof end;

Lm3: for p being Instruction-Sequence of SCM+FSA
for s being 0 -started State of SCM+FSA
for I being really-closed good InitHalting MacroInstruction of SCM+FSA
for a being read-write Int-Location st not I destroys a & s . () = 1 holds
for k being Nat holds
( ((StepTimes (a,I,p,s)) . k) . () = 1 & I is_halting_on (StepTimes (a,I,p,s)) . k,p +* (Times (a,I)) )

proof end;

theorem :: SCM_HALT:55
canceled;

theorem :: SCM_HALT:56
canceled;

theorem :: SCM_HALT:57
canceled;

theorem :: SCM_HALT:58
canceled;

theorem :: SCM_HALT:59
canceled;

theorem :: SCM_HALT:60
canceled;

theorem :: SCM_HALT:61
canceled;

::$CT 7 theorem :: SCM_HALT:62 for p being Instruction-Sequence of SCM+FSA for s being 0 -started State of SCM+FSA for I being really-closed good InitHalting MacroInstruction of SCM+FSA for a being read-write Int-Location st not I destroys a & s . () = 1 holds Times (a,I) is_halting_on s,p proof end; registration let a be read-write Int-Location; let I be good MacroInstruction of SCM+FSA ; cluster Times (a,I) -> good ; coherence Times (a,I) is good ; end; theorem :: SCM_HALT:63 canceled; theorem :: SCM_HALT:64 canceled; ::$CT 2
theorem Th47: :: SCM_HALT:65
for p being Instruction-Sequence of SCM+FSA
for s being State of SCM+FSA
for I being really-closed good InitHalting MacroInstruction of SCM+FSA
for a being read-write Int-Location st s . () = 1 & s . a <= 0 holds
DataPart (IExec ((Times (a,I)),p,s)) = DataPart s by SCMFSA9A:58;

Lm4: for P1, P2 being Instruction-Sequence of SCM+FSA
for s being State of SCM+FSA
for I being really-closed InitHalting Program of SCM+FSA st Initialize (() .--> 1) c= s & I c= P1 & I c= P2 holds
for k being Nat holds
( Comput (P1,s,k) = Comput (P2,s,k) & CurInstr (P1,(Comput (P1,s,k))) = CurInstr (P2,(Comput (P2,s,k))) )

proof end;

Lm5: for P1, P2 being Instruction-Sequence of SCM+FSA
for s being State of SCM+FSA
for I being really-closed InitHalting Program of SCM+FSA st Initialize (() .--> 1) c= s & I c= P1 & I c= P2 holds
( LifeSpan (P1,s) = LifeSpan (P2,s) & Result (P1,s) = Result (P2,s) )

by Th6;

Lm6: for P being Instruction-Sequence of SCM+FSA
for s being State of SCM+FSA
for I being really-closed MacroInstruction of SCM+FSA
for a being read-write Int-Location st s . a <= 0 holds
while>0 (a,I) is_halting_onInit s,P

proof end;

Lm7: for P being Instruction-Sequence of SCM+FSA
for s being State of SCM+FSA
for I being really-closed MacroInstruction of SCM+FSA
for a being read-write Int-Location st I is_halting_onInit s,P & s . a > 0 holds
( IC (Comput ((P +* (while>0 (a,I))),(),((LifeSpan ((P +* I),())) + 2))) = 0 & DataPart (Comput ((P +* (while>0 (a,I))),(),((LifeSpan ((P +* I),())) + 2))) = DataPart (Comput ((P +* I),(),(LifeSpan ((P +* I),())))) )

proof end;

Lm8: for P being Instruction-Sequence of SCM+FSA
for s being State of SCM+FSA
for I being really-closed good InitHalting MacroInstruction of SCM+FSA
for a being read-write Int-Location st s . a > 0 & while>0 (a,I) is InitHalting holds
DataPart (IExec ((while>0 (a,I)),P,s)) = DataPart (IExec ((while>0 (a,I)),P,(IExec (I,P,s))))

proof end;

Lm9: for I being really-closed good InitHalting MacroInstruction of SCM+FSA
for a being read-write Int-Location st ( for s being State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA st s . a > 0 holds
(IExec (I,P,s)) . a < s . a ) holds
while>0 (a,I) is InitHalting

proof end;

Lm10: for p being Instruction-Sequence of SCM+FSA
for s being State of SCM+FSA
for I being really-closed good InitHalting Program of SCM+FSA
for a being read-write Int-Location st not I destroys a holds
(IExec ((I ";" (SubFrom (a,()))),p,s)) . a = (s . a) - 1

proof end;

theorem Th48: :: SCM_HALT:66
for p being Instruction-Sequence of SCM+FSA
for s being State of SCM+FSA
for I being really-closed good InitHalting MacroInstruction of SCM+FSA
for a being read-write Int-Location st not I destroys a holds
( (IExec ((I ";" (SubFrom (a,()))),p,s)) . a = (s . a) - 1 & ( s . a > 0 implies DataPart (IExec ((Times (a,I)),p,s)) = DataPart (IExec ((Times (a,I)),p,(IExec ((I ";" (SubFrom (a,()))),p,s)))) ) )
proof end;

theorem :: SCM_HALT:67
for p being Instruction-Sequence of SCM+FSA
for s being State of SCM+FSA
for I being really-closed good InitHalting MacroInstruction of SCM+FSA
for f being FinSeq-Location
for a being read-write Int-Location st s . a <= 0 holds
(IExec ((Times (a,I)),p,s)) . f = s . f
proof end;

theorem :: SCM_HALT:68
for p being Instruction-Sequence of SCM+FSA
for s being State of SCM+FSA
for I being really-closed good InitHalting MacroInstruction of SCM+FSA
for b being Int-Location
for a being read-write Int-Location st s . a <= 0 holds
(IExec ((Times (a,I)),p,s)) . b = () . b
proof end;

theorem :: SCM_HALT:69
for p being Instruction-Sequence of SCM+FSA
for s being State of SCM+FSA
for I being really-closed good InitHalting MacroInstruction 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)),p,s)) . f = (IExec ((Times (a,I)),p,(IExec ((I ";" (SubFrom (a,()))),p,s)))) . f
proof end;

theorem :: SCM_HALT:70
for p being Instruction-Sequence of SCM+FSA
for s being State of SCM+FSA
for I being really-closed good InitHalting MacroInstruction 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)),p,s)) . b = (IExec ((Times (a,I)),p,(IExec ((I ";" (SubFrom (a,()))),p,s)))) . b
proof end;

definition
let i be Instruction of SCM+FSA;
redefine attr i is good means :: SCM_HALT:def 4
not i destroys intloc 0;
compatibility
( i is good iff not i destroys intloc 0 )
proof end;
end;

:: deftheorem defines good SCM_HALT:def 4 :
for i being Instruction of SCM+FSA holds
( i is good iff not i destroys intloc 0 );

theorem :: SCM_HALT:71
for P1, P2 being Instruction-Sequence of SCM+FSA
for s being State of SCM+FSA
for I being really-closed InitHalting Program of SCM+FSA st Initialize (() .--> 1) c= s & I c= P1 & I c= P2 holds
for k being Nat holds
( Comput (P1,s,k) = Comput (P2,s,k) & CurInstr (P1,(Comput (P1,s,k))) = CurInstr (P2,(Comput (P2,s,k))) ) by Lm4;

theorem :: SCM_HALT:72
for P1, P2 being Instruction-Sequence of SCM+FSA
for s being State of SCM+FSA
for I being really-closed InitHalting Program of SCM+FSA st Initialize (() .--> 1) c= s & I c= P1 & I c= P2 holds
( LifeSpan (P1,s) = LifeSpan (P2,s) & Result (P1,s) = Result (P2,s) ) by Lm5;

theorem :: SCM_HALT:73
for P being Instruction-Sequence of SCM+FSA
for s being State of SCM+FSA
for I being really-closed MacroInstruction of SCM+FSA
for a being read-write Int-Location st s . a <= 0 holds
while>0 (a,I) is_halting_onInit s,P by Lm6;

theorem :: SCM_HALT:74
for P being Instruction-Sequence of SCM+FSA
for s being State of SCM+FSA
for I being really-closed MacroInstruction of SCM+FSA
for a being read-write Int-Location st I is_halting_onInit s,P & s . a > 0 holds
( IC (Comput ((P +* (while>0 (a,I))),(),((LifeSpan ((P +* I),())) + 2))) = 0 & DataPart (Comput ((P +* (while>0 (a,I))),(),((LifeSpan ((P +* I),())) + 2))) = DataPart (Comput ((P +* I),(),(LifeSpan ((P +* I),())))) ) by Lm7;

theorem :: SCM_HALT:75
for P being Instruction-Sequence of SCM+FSA
for s being State of SCM+FSA
for I being really-closed good InitHalting MacroInstruction of SCM+FSA
for a being read-write Int-Location st s . a > 0 & while>0 (a,I) is InitHalting holds
DataPart (IExec ((while>0 (a,I)),P,s)) = DataPart (IExec ((while>0 (a,I)),P,(IExec (I,P,s)))) by Lm8;

theorem :: SCM_HALT:76
for I being really-closed good InitHalting MacroInstruction of SCM+FSA
for a being read-write Int-Location st ( for s being State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA st s . a > 0 holds
(IExec (I,P,s)) . a < s . a ) holds
while>0 (a,I) is InitHalting by Lm9;