:: Initialization Halting Concepts and Their Basic Properties of SCM+FSA :: by JingChao Chen and Yatsuka Nakamura :: :: Received June 17, 1998 :: Copyright (c) 1998-2012 Association of Mizar Users begin set SA0 = Start-At (0,SCM+FSA); set iS = Initialize ((intloc 0) .--> 1); reconsider EP = {} as PartState of SCM+FSA by FUNCT_1:104, RELAT_1:171; Lm1: IC (Initialize ((intloc 0) .--> 1)) = 0 by MEMSTR_0:def_11; Lm2: Start-At (0,SCM+FSA) c= Initialize ((intloc 0) .--> 1) by FUNCT_4:25; Lm3: dom (Initialize ((intloc 0) .--> 1)) = (dom ((intloc 0) .--> 1)) \/ (dom (Start-At (0,SCM+FSA))) by FUNCT_4:def_1 .= {(intloc 0)} \/ (dom (Start-At (0,SCM+FSA))) by FUNCOP_1:13 .= {(intloc 0)} \/ {(IC )} by FUNCOP_1:13 ; definition let I be Program of SCM+FSA; attrI is InitClosed means :Def1: :: SCM_HALT:def 1 for s being State of SCM+FSA for P being Instruction-Sequence of SCM+FSA st I c= P holds for n being Element of NAT st Initialize ((intloc 0) .--> 1) c= s holds IC (Comput (P,s,n)) in dom I; attrI is InitHalting means :Def2: :: SCM_HALT:def 2 for s being State of SCM+FSA st Initialize ((intloc 0) .--> 1) c= s holds for P being Instruction-Sequence of SCM+FSA st I c= P holds P halts_on s; attrI is keepInt0_1 means :Def3: :: SCM_HALT:def 3 for s being State of SCM+FSA st Initialize ((intloc 0) .--> 1) c= s holds for p being Instruction-Sequence of SCM+FSA st I c= p holds for k being Element of NAT holds (Comput (p,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 P being Instruction-Sequence of SCM+FSA st I c= P holds for n being Element of NAT st Initialize ((intloc 0) .--> 1) c= s holds IC (Comput (P,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 for s being State of SCM+FSA st Initialize ((intloc 0) .--> 1) c= s holds for P being Instruction-Sequence of SCM+FSA st I c= P holds P halts_on s ); :: 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 Initialize ((intloc 0) .--> 1) c= s holds for p being Instruction-Sequence of SCM+FSA st I c= p holds for k being Element of NAT holds (Comput (p,s,k)) . (intloc 0) = 1 ); theorem :: SCM_HALT:1 canceled; theorem Th2: :: SCM_HALT:2 Macro (halt SCM+FSA) is InitHalting proofend; registration cluster non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V30() V69() V162() InitHalting for set ; existence ex b1 being Program of SCM+FSA st b1 is InitHalting by Th2; end; registration cluster non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V30() V69() paraclosed -> InitClosed for set ; coherence for b1 being Program of SCM+FSA st b1 is paraclosed holds b1 is InitClosed proofend; end; registration cluster non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V30() V69() parahalting -> InitHalting for set ; coherence for b1 being Program of SCM+FSA st b1 is parahalting holds b1 is InitHalting proofend; end; registration cluster non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V30() V69() InitHalting -> InitClosed for set ; coherence for b1 being Program of SCM+FSA st b1 is InitHalting holds b1 is InitClosed proofend; cluster non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V30() V69() keepInt0_1 -> InitClosed for set ; coherence for b1 being Program of SCM+FSA st b1 is keepInt0_1 holds b1 is InitClosed proofend; cluster non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V30() V69() keeping_0 -> keepInt0_1 for set ; coherence for b1 being Program of SCM+FSA st b1 is keeping_0 holds b1 is keepInt0_1 proofend; end; theorem :: SCM_HALT:3 canceled; theorem :: SCM_HALT:4 for s being State of SCM+FSA for p being Instruction-Sequence 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,p,s)) . a = s . a proofend; theorem :: SCM_HALT:5 for s being State of SCM+FSA for p being Instruction-Sequence 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,p,s)) . f = s . f proofend; registration cluster non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V30() V69() InitHalting -> for set ; coherence for b1 being Program of SCM+FSA st b1 is InitHalting holds not b1 is empty ; end; theorem Th6: :: SCM_HALT:6 for s1, s2 being State of SCM+FSA for p1, p2 being Instruction-Sequence of SCM+FSA for J being InitHalting Program of SCM+FSA st Initialize ((intloc 0) .--> 1) c= s1 & J c= p1 holds for n being Element of NAT st Reloc (J,n) c= p2 & IC s2 = n & DataPart s1 = DataPart s2 holds for i being Element of 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)) ) proofend; theorem Th7: :: SCM_HALT:7 for s1, s2 being State of SCM+FSA for p1, p2 being Instruction-Sequence of SCM+FSA for I being InitHalting Program of SCM+FSA st Initialize ((intloc 0) .--> 1) c= s1 & Initialize ((intloc 0) .--> 1) c= s2 & I c= p1 & I c= p2 & s1 = s2 holds for k being Element of NAT holds ( Comput (p1,s1,k) = Comput (p2,s2,k) & CurInstr (p1,(Comput (p1,s1,k))) = CurInstr (p2,(Comput (p2,s2,k))) ) proofend; theorem Th8: :: SCM_HALT:8 for s1, s2 being State of SCM+FSA for p1, p2 being Instruction-Sequence of SCM+FSA for I being InitHalting Program of SCM+FSA st Initialize ((intloc 0) .--> 1) c= s1 & Initialize ((intloc 0) .--> 1) c= s2 & I c= p1 & I c= p2 & s1 = s2 holds ( LifeSpan (p1,s1) = LifeSpan (p2,s2) & Result (p1,s1) = Result (p2,s2) ) proofend; registration cluster non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V30() V69() keeping_0 V162() InitHalting for set ; existence ex b1 being Program of SCM+FSA st ( b1 is keeping_0 & b1 is InitHalting ) proofend; end; registration cluster non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V30() V69() V162() InitHalting keepInt0_1 for set ; existence ex b1 being Program of SCM+FSA st ( b1 is keepInt0_1 & b1 is InitHalting ) proofend; end; theorem Th9: :: 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)) . (intloc 0) = 1 proofend; registration cluster non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V30() V69() V162() InitClosed for set ; existence ex b1 being Program of SCM+FSA st b1 is InitClosed proofend; end; theorem Th10: :: SCM_HALT:10 for s being State of SCM+FSA for p being Instruction-Sequence of SCM+FSA for I being InitClosed Program of SCM+FSA for J being Program of SCM+FSA st Initialize ((intloc 0) .--> 1) c= s & I c= p & p halts_on s holds for m being Element of NAT st m <= LifeSpan (p,s) holds Comput (p,s,m) = Comput ((p +* (I ";" J)),s,m) proofend; theorem Th11: :: SCM_HALT:11 for s being State of SCM+FSA for p being Instruction-Sequence of SCM+FSA for I being InitClosed Program of SCM+FSA st p +* I halts_on s & Directed I c= p & Initialize ((intloc 0) .--> 1) c= s holds IC (Comput (p,s,((LifeSpan ((p +* I),s)) + 1))) = card I proofend; theorem Th12: :: SCM_HALT:12 for s being State of SCM+FSA for p being Instruction-Sequence of SCM+FSA for I being InitClosed Program of SCM+FSA st p +* I halts_on s & Directed I c= p & Initialize ((intloc 0) .--> 1) c= s holds DataPart (Comput (p,s,(LifeSpan ((p +* I),s)))) = DataPart (Comput (p,s,((LifeSpan ((p +* I),s)) + 1))) proofend; theorem Th13: :: SCM_HALT:13 for s being State of SCM+FSA for p being Instruction-Sequence of SCM+FSA for I being InitHalting Program of SCM+FSA st Initialize ((intloc 0) .--> 1) c= s & I c= p holds for k being Element of NAT st k <= LifeSpan (p,s) holds CurInstr ((p +* (Directed I)),(Comput ((p +* (Directed I)),s,k))) <> halt SCM+FSA proofend; theorem Th14: :: SCM_HALT:14 for s being State of SCM+FSA for p being Instruction-Sequence of SCM+FSA for I being InitClosed Program of SCM+FSA st p +* I halts_on Initialized s holds for J being Program of SCM+FSA for k being Element of NAT st k <= LifeSpan ((p +* I),(Initialized s)) holds Comput ((p +* I),(Initialized s),k) = Comput ((p +* (I ";" J)),(Initialized s),k) proofend; theorem Th15: :: SCM_HALT:15 for p being Instruction-Sequence of SCM+FSA 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 Initialize ((intloc 0) .--> 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 ((intloc 0) .--> 1))) & Reloc (J,(card I)) c= p & (Comput (p,s,((LifeSpan ((p +* I),s)) + 1))) . (intloc 0) = 1 & p halts_on s & LifeSpan (p,s) = ((LifeSpan ((p +* I),s)) + 1) + (LifeSpan (((p +* I) +* J),((Result ((p +* I),s)) +* (Initialize ((intloc 0) .--> 1))))) & ( J is keeping_0 implies (Result (p,s)) . (intloc 0) = 1 ) ) proofend; registration let I be InitHalting keepInt0_1 Program of SCM+FSA; let J be InitHalting Program of SCM+FSA; clusterI ";" J -> InitHalting ; coherence I ";" J is InitHalting proofend; end; theorem Th16: :: SCM_HALT:16 for s being State of SCM+FSA for p being Instruction-Sequence of SCM+FSA for I being keepInt0_1 Program of SCM+FSA st p +* I halts_on s holds for J being InitClosed Program of SCM+FSA st Initialize ((intloc 0) .--> 1) c= s & I ";" J c= p holds for k being Element of NAT holds (Comput (((p +* I) +* J),((Result ((p +* I),s)) +* (Initialize ((intloc 0) .--> 1))),k)) +* (Start-At (((IC (Comput (((p +* I) +* J),((Result ((p +* I),s)) +* (Initialize ((intloc 0) .--> 1))),k))) + (card I)),SCM+FSA)) = Comput ((p +* (I ";" J)),s,(((LifeSpan ((p +* I),s)) + 1) + k)) proofend; theorem Th17: :: SCM_HALT:17 for s being State of SCM+FSA for p being Instruction-Sequence of SCM+FSA for I being 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 Element of NAT holds Comput ((p +* I),(Initialized s),k) = Comput ((p +* (I ";" J)),(Initialized s),k) proofend; theorem Th18: :: SCM_HALT:18 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 for J being InitHalting Program of SCM+FSA holds LifeSpan ((p +* (I ";" J)),(Initialized s)) = ((LifeSpan ((p +* I),(Initialized s))) + 1) + (LifeSpan (((p +* I) +* J),((Result ((p +* I),(Initialized s))) +* (Initialize ((intloc 0) .--> 1))))) proofend; theorem Th19: :: SCM_HALT:19 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 for J being InitHalting Program of SCM+FSA holds IExec ((I ";" J),p,s) = IncIC ((IExec (J,p,(IExec (I,p,s)))),(card I)) proofend; 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; clusteri ";" 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; clusteri ";" J -> InitHalting ; coherence i ";" J is InitHalting ; end; registration let I, J be keepInt0_1 Program of SCM+FSA; clusterI ";" J -> keepInt0_1 ; coherence I ";" J is keepInt0_1 proofend; end; registration let j be parahalting keeping_0 Instruction of SCM+FSA; let I be InitHalting keepInt0_1 Program of SCM+FSA; clusterI ";" 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; clusteri ";" 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; clusterI ";" j -> InitHalting ; coherence I ";" j is InitHalting ; end; registration let i, j be parahalting Instruction of SCM+FSA; clusteri ";" j -> InitHalting ; coherence i ";" j is InitHalting ; end; theorem Th20: :: 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 InitHalting keepInt0_1 Program of SCM+FSA for J being InitHalting Program of SCM+FSA holds (IExec ((I ";" J),p,s)) . a = (IExec (J,p,(IExec (I,p,s)))) . a proofend; theorem Th21: :: 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 InitHalting keepInt0_1 Program of SCM+FSA for J being InitHalting Program of SCM+FSA holds (IExec ((I ";" J),p,s)) . f = (IExec (J,p,(IExec (I,p,s)))) . f proofend; theorem Th22: :: 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)) proofend; theorem Th23: :: 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 InitHalting keepInt0_1 Program of SCM+FSA for j being parahalting Instruction of SCM+FSA holds (IExec ((I ";" j),p,s)) . a = (Exec (j,(IExec (I,p,s)))) . a proofend; theorem Th24: :: 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 InitHalting keepInt0_1 Program of SCM+FSA for j being parahalting Instruction of SCM+FSA holds (IExec ((I ";" j),p,s)) . f = (Exec (j,(IExec (I,p,s)))) . f proofend; definition let I be Program of SCM+FSA; let s be State of SCM+FSA; let p be Instruction-Sequence of SCM+FSA; predI is_closed_onInit s,p means :Def4: :: SCM_HALT:def 4 for k being Element of NAT holds IC (Comput ((p +* I),(Initialized s),k)) in dom I; predI is_halting_onInit s,p means :Def5: :: SCM_HALT:def 5 p +* I halts_on Initialized s; 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 for p being Instruction-Sequence of SCM+FSA holds ( I is_closed_onInit s,p iff for k being Element of NAT holds IC (Comput ((p +* I),(Initialized s),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 for p being Instruction-Sequence of SCM+FSA holds ( I is_halting_onInit s,p iff p +* I halts_on Initialized s ); theorem Th25: :: SCM_HALT:25 for I being Program of SCM+FSA holds ( I is InitClosed iff for s being State of SCM+FSA for p being Instruction-Sequence of SCM+FSA holds I is_closed_onInit s,p ) proofend; theorem Th26: :: 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 ) proofend; theorem Th27: :: SCM_HALT:27 for p being Instruction-Sequence of SCM+FSA for s being State of SCM+FSA for I being Program of SCM+FSA for a being Int-Location st not I destroys a & I is_closed_onInit s,p & Initialize ((intloc 0) .--> 1) c= s & I c= p holds for k being Element of NAT holds (Comput (p,s,k)) . a = s . a proofend; registration cluster non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V30() V69() good V162() InitHalting for set ; existence ex b1 being Program of SCM+FSA st ( b1 is InitHalting & b1 is good ) proofend; end; registration cluster non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V30() V69() good InitClosed -> keepInt0_1 for set ; correctness coherence for b1 being Program of SCM+FSA st b1 is InitClosed & b1 is good holds b1 is keepInt0_1 ; proofend; end; registration cluster Stop SCM+FSA -> good InitHalting ; coherence ( Stop SCM+FSA is InitHalting & Stop SCM+FSA is good ) ; end; theorem :: SCM_HALT:28 for p being Instruction-Sequence of SCM+FSA 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),p,s)) . a = (IExec (J,p,(Exec (i,(Initialized s))))) . a proofend; theorem :: SCM_HALT:29 for p being Instruction-Sequence of SCM+FSA 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),p,s)) . f = (IExec (J,p,(Exec (i,(Initialized s))))) . f proofend; theorem Th30: :: SCM_HALT:30 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_closed_onInit s,p iff I is_closed_on Initialized s,p ) proofend; theorem Th31: :: 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 ) proofend; 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,(Initialized s)) proofend; theorem Th33: :: SCM_HALT:33 for p being Instruction-Sequence of SCM+FSA 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,p & I is_halting_onInit s,p holds ( if=0 (a,I,J) is_closed_onInit s,p & if=0 (a,I,J) is_halting_onInit s,p ) proofend; theorem Th34: :: SCM_HALT:34 for p being Instruction-Sequence of SCM+FSA 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,p & 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)) proofend; theorem Th35: :: SCM_HALT:35 for p being Instruction-Sequence of SCM+FSA 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,p & J is_halting_onInit s,p holds ( if=0 (a,I,J) is_closed_onInit s,p & if=0 (a,I,J) is_halting_onInit s,p ) proofend; theorem Th36: :: SCM_HALT:36 for p being Instruction-Sequence of SCM+FSA 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,p & 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)) proofend; theorem Th37: :: SCM_HALT:37 for p being Instruction-Sequence of SCM+FSA 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)),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)) ) ) proofend; theorem :: SCM_HALT:38 for p being Instruction-Sequence of SCM+FSA 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)),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 ) ) ) ) proofend; theorem Th39: :: SCM_HALT:39 for p being Instruction-Sequence of SCM+FSA 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,p & I is_halting_onInit s,p holds ( if>0 (a,I,J) is_closed_onInit s,p & if>0 (a,I,J) is_halting_onInit s,p ) proofend; theorem Th40: :: SCM_HALT:40 for p being Instruction-Sequence of SCM+FSA 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,p & 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)) proofend; theorem Th41: :: SCM_HALT:41 for p being Instruction-Sequence of SCM+FSA 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,p & J is_halting_onInit s,p holds ( if>0 (a,I,J) is_closed_onInit s,p & if>0 (a,I,J) is_halting_onInit s,p ) proofend; theorem Th42: :: SCM_HALT:42 for p being Instruction-Sequence of SCM+FSA 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,p & 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)) proofend; theorem Th43: :: SCM_HALT:43 for p being Instruction-Sequence of SCM+FSA 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)),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)) ) ) proofend; theorem :: SCM_HALT:44 for p being Instruction-Sequence of SCM+FSA 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)),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 ) ) ) ) proofend; theorem Th45: :: SCM_HALT:45 for p being Instruction-Sequence of SCM+FSA 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,p & 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)) + (card J)) + 7),SCM+FSA)) proofend; theorem Th46: :: SCM_HALT:46 for p being Instruction-Sequence of SCM+FSA 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,p & 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)) + (card J)) + 7),SCM+FSA)) proofend; theorem Th47: :: SCM_HALT:47 for p being Instruction-Sequence of SCM+FSA 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,p & 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)) + (card J)) + 7),SCM+FSA)) proofend; theorem Th48: :: SCM_HALT:48 for p being Instruction-Sequence of SCM+FSA 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)),p,s) = (IExec (I,p,s)) +* (Start-At (((((card I) + (card J)) + (card J)) + 7),SCM+FSA)) ) & ( s . a >= 0 implies IExec ((if<0 (a,I,J)),p,s) = (IExec (J,p,s)) +* (Start-At (((((card I) + (card J)) + (card J)) + 7),SCM+FSA)) ) ) proofend; 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 Th37; cluster if>0 (a,I,J) -> InitHalting ; correctness coherence if>0 (a,I,J) is InitHalting ; by Th43; cluster if<0 (a,I,J) -> InitHalting ; correctness coherence if<0 (a,I,J) is InitHalting ; by Th48; end; theorem Th49: :: 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 ) proofend; theorem Th50: :: SCM_HALT:50 for I being Program of SCM+FSA holds ( I is InitClosed iff for s being State of SCM+FSA for p being Instruction-Sequence of SCM+FSA holds I is_closed_on Initialized s,p ) proofend; theorem Th51: :: 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),(Initialize (Initialized s)),(LifeSpan ((p +* I),(Initialize (Initialized s)))))) . a proofend; theorem Th52: :: SCM_HALT:52 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 Int-Location for k being Element of NAT st not I destroys a holds (IExec (I,p,s)) . a = (Comput ((p +* I),(Initialize (Initialized s)),k)) . a proofend; set A = NAT ; set D = Data-Locations ; theorem Th53: :: SCM_HALT:53 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 Int-Location st not I destroys a holds (IExec (I,p,s)) . a = (Initialized s) . a proofend; theorem Th54: :: SCM_HALT:54 for p being Instruction-Sequence of SCM+FSA for s being State of SCM+FSA for I being InitHalting keepInt0_1 Program of SCM+FSA for a being read-write Int-Location st not I destroys a holds (Comput ((p +* (I ";" (SubFrom (a,(intloc 0))))),(Initialize (Initialized s)),(LifeSpan ((p +* (I ";" (SubFrom (a,(intloc 0))))),(Initialize (Initialized s)))))) . a = (s . a) - 1 proofend; theorem Th55: :: SCM_HALT:55 for p being Instruction-Sequence of SCM+FSA for s being State of SCM+FSA for I being InitClosed Program of SCM+FSA st Initialize ((intloc 0) .--> 1) c= s & I c= p & p halts_on s holds for m being Element of NAT st m <= LifeSpan (p,s) holds Comput (p,s,m) = Comput ((p +* (loop I)),s,m) proofend; theorem :: SCM_HALT:56 for p being Instruction-Sequence of SCM+FSA for s being State of SCM+FSA for I being InitHalting Program of SCM+FSA st Initialize ((intloc 0) .--> 1) c= s & I c= p holds for k being Element of NAT st k <= LifeSpan (p,s) holds CurInstr ((p +* (loop I)),(Comput ((p +* (loop I)),s,k))) <> halt SCM+FSA proofend; theorem Th57: :: SCM_HALT:57 for p being Instruction-Sequence of SCM+FSA for s being State of SCM+FSA for I being Program of SCM+FSA st I is_closed_onInit s,p & I is_halting_onInit s,p holds for m being Element of NAT st m <= LifeSpan ((p +* I),(Initialized s)) holds Comput ((p +* I),(Initialized s),m) = Comput ((p +* (loop I)),(Initialized s),m) proofend; theorem Th58: :: SCM_HALT:58 for p being Instruction-Sequence of SCM+FSA for s being State of SCM+FSA for I being Program of SCM+FSA st I is_closed_onInit s,p & I is_halting_onInit s,p holds for m being Element of NAT st m < LifeSpan ((p +* I),(Initialized s)) holds CurInstr ((p +* I),(Comput ((p +* I),(Initialized s),m))) = CurInstr ((p +* (loop I)),(Comput ((p +* (loop I)),(Initialized s),m))) proofend; theorem Th59: :: SCM_HALT:59 for p being Instruction-Sequence of SCM+FSA for s being State of SCM+FSA for I being Program of SCM+FSA st I is_closed_onInit s,p & I is_halting_onInit s,p holds ( CurInstr ((p +* (loop I)),(Comput ((p +* (loop I)),(Initialized s),(LifeSpan ((p +* I),(Initialized s)))))) = goto 0 & ( for m being Element of NAT st m <= LifeSpan ((p +* I),(Initialized s)) holds CurInstr ((p +* (loop I)),(Comput ((p +* (loop I)),(Initialized s),m))) <> halt SCM+FSA ) ) proofend; theorem Th60: :: SCM_HALT:60 for s being State of SCM+FSA for p being Instruction-Sequence of SCM+FSA for I being good InitHalting Program of SCM+FSA for a being read-write Int-Location st not I destroys a & s . (intloc 0) = 1 & s . a > 0 holds loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))) is_pseudo-closed_on s,p proofend; theorem :: SCM_HALT:61 for p being Instruction-Sequence of SCM+FSA for s being State of SCM+FSA for I being good InitHalting Program of SCM+FSA for a being read-write Int-Location st not I destroys a & s . a > 0 holds loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))) is_pseudo-closed_on Initialized s,p proofend; theorem :: SCM_HALT:62 for p being Instruction-Sequence of SCM+FSA for s being State of SCM+FSA for I being good InitHalting Program of SCM+FSA for a being read-write Int-Location st not I destroys a & s . (intloc 0) = 1 holds ( Times (a,I) is_closed_on s,p & Times (a,I) is_halting_on s,p ) proofend; theorem :: SCM_HALT:63 for I being good InitHalting Program of SCM+FSA for a being read-write Int-Location st not I destroys a holds Initialize ((intloc 0) .--> 1) is Times (a,I) -halted proofend; 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 ; end; theorem Th64: :: SCM_HALT:64 for p being Instruction-Sequence of SCM+FSA for s being State of SCM+FSA for I being good InitHalting Program of SCM+FSA for a being read-write Int-Location st not I destroys a & s . a > 0 holds ex s2 being State of SCM+FSA ex p2 being Instruction-Sequence of SCM+FSA ex k being Element of NAT st ( s2 = Initialized s & p2 = p +* (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))) & k = (LifeSpan ((p +* (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))),(Initialized s))) + 1 & (Comput (p2,s2,k)) . a = (s . a) - 1 & (Comput (p2,s2,k)) . (intloc 0) = 1 & ( for b being read-write Int-Location st b <> a holds (Comput (p2,s2,k)) . b = (IExec (I,p,s)) . b ) & ( for f being FinSeq-Location holds (Comput (p2,s2,k)) . f = (IExec (I,p,s)) . f ) & IC (Comput (p2,s2,k)) = 0 & ( for n being Element of NAT st n <= k holds IC (Comput (p2,s2,n)) in dom (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))) ) ) proofend; theorem Th65: :: SCM_HALT:65 for p being Instruction-Sequence of SCM+FSA 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)),p,s)) = DataPart s proofend; theorem Th66: :: SCM_HALT:66 for p being Instruction-Sequence of SCM+FSA for s being State of SCM+FSA for I being good InitHalting Program of SCM+FSA for a being read-write Int-Location st not I destroys a & s . a > 0 holds ( (IExec ((I ";" (SubFrom (a,(intloc 0)))),p,s)) . a = (s . a) - 1 & DataPart (IExec ((Times (a,I)),p,s)) = DataPart (IExec ((Times (a,I)),p,(IExec ((I ";" (SubFrom (a,(intloc 0)))),p,s)))) ) proofend; theorem :: SCM_HALT:67 for p being Instruction-Sequence of SCM+FSA 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)),p,s)) . f = s . f proofend; theorem :: SCM_HALT:68 for p being Instruction-Sequence of SCM+FSA 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)),p,s)) . b = (Initialized s) . b proofend; theorem :: SCM_HALT:69 for p being Instruction-Sequence of SCM+FSA for s being State of SCM+FSA for I being good InitHalting Program of SCM+FSA for f being FinSeq-Location for a being read-write Int-Location st not I destroys a & s . a > 0 holds (IExec ((Times (a,I)),p,s)) . f = (IExec ((Times (a,I)),p,(IExec ((I ";" (SubFrom (a,(intloc 0)))),p,s)))) . f proofend; theorem :: SCM_HALT:70 for p being Instruction-Sequence of SCM+FSA for s being State of SCM+FSA for I being good InitHalting Program of SCM+FSA for b being Int-Location for a being read-write Int-Location st not I destroys a & s . a > 0 holds (IExec ((Times (a,I)),p,s)) . b = (IExec ((Times (a,I)),p,(IExec ((I ";" (SubFrom (a,(intloc 0)))),p,s)))) . b proofend; definition let i be Instruction of SCM+FSA; redefine attr i is good means :: SCM_HALT:def 6 not i destroys intloc 0; compatibility ( i is good iff not i destroys intloc 0 ) proofend; end; :: deftheorem defines good SCM_HALT:def_6_:_ for i being Instruction of SCM+FSA holds ( i is good iff not i destroys intloc 0 );