:: The {\bf loop} and {\bf Times} Macroinstruction for {\SCMFSA} :: by Noriko Asamoto :: :: Received October 29, 1997 :: Copyright (c) 1997-2012 Association of Mizar Users begin set SA0 = Start-At (0,SCM+FSA); set Q = (intloc 0) .--> 1; theorem Th1: :: SCMFSA8C:1 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_pseudo-closed_on s,P holds for k being Element of NAT st ( for n being Element of NAT st n <= k holds IC (Comput ((P +* I),(Initialize s),n)) in dom I ) holds k < pseudo-LifeSpan (s,P,I) proofend; theorem Th2: :: SCMFSA8C:2 for I, J being Program of SCM+FSA for k being Element of NAT st card I <= k & k < (card I) + (card J) holds for i being Instruction of SCM+FSA st i = J . (k -' (card I)) holds (I ";" J) . k = IncAddr (i,(card I)) proofend; theorem :: SCMFSA8C:3 for P being Instruction-Sequence of SCM+FSA for s being State of SCM+FSA for I being Program of SCM+FSA holds IExec (I,P,s) = IExec (I,P,(Initialized s)) ; theorem :: SCMFSA8C:4 canceled; theorem Th5: :: SCMFSA8C:5 for I being Program of SCM+FSA st ( for s being State of SCM+FSA for P being Instruction-Sequence of SCM+FSA holds I is_halting_on Initialized s,P ) holds Initialize ((intloc 0) .--> 1) is I -halted proofend; theorem Th6: :: SCMFSA8C:6 for I being Program of SCM+FSA st ( for s being State of SCM+FSA for P being Instruction-Sequence of SCM+FSA holds I is_halting_on Initialized s,P ) holds Initialize ((intloc 0) .--> 1) is I -halted by Th5; theorem :: SCMFSA8C:7 canceled; theorem :: SCMFSA8C:8 canceled; theorem :: SCMFSA8C:9 canceled; theorem :: SCMFSA8C:10 canceled; theorem :: SCMFSA8C:11 canceled; theorem Th12: :: SCMFSA8C:12 for s being State of SCM+FSA for i being Instruction of SCM+FSA st InsCode i in {0,6,7,8} holds DataPart (Exec (i,s)) = DataPart s proofend; theorem :: SCMFSA8C:13 canceled; theorem Th14: :: SCMFSA8C:14 for P being Instruction-Sequence of SCM+FSA for s being State of SCM+FSA holds IExec ((Stop SCM+FSA),P,s) = Initialized s proofend; theorem Th15: :: SCMFSA8C:15 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_on s,P holds 0 in dom I proofend; theorem Th16: :: SCMFSA8C:16 for P1, P2 being Instruction-Sequence of SCM+FSA for s1 being 0 -started State of SCM+FSA for s2 being State of SCM+FSA for I being Program of SCM+FSA st I is_closed_on s1,P1 & I c= P1 holds for n being Element of NAT st Reloc (I,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 Th17: :: SCMFSA8C:17 for P1, P2 being Instruction-Sequence of SCM+FSA for s1, s2 being 0 -started State of SCM+FSA for I being Program of SCM+FSA st I is_closed_on s1,P1 & I c= P1 & I c= P2 & DataPart s1 = DataPart s2 holds for i being Element of NAT holds ( IC (Comput (P1,s1,i)) = IC (Comput (P2,s2,i)) & CurInstr (P1,(Comput (P1,s1,i))) = CurInstr (P2,(Comput (P2,s2,i))) & DataPart (Comput (P1,s1,i)) = DataPart (Comput (P2,s2,i)) ) proofend; theorem Th18: :: SCMFSA8C:18 for P1, P2 being Instruction-Sequence of SCM+FSA for s1, s2 being 0 -started State of SCM+FSA for I being Program of SCM+FSA st I is_closed_on s1,P1 & I is_halting_on s1,P1 & I c= P1 & I c= P2 & DataPart s1 = DataPart s2 holds LifeSpan (P1,s1) = LifeSpan (P2,s2) proofend; theorem :: SCMFSA8C:19 for P1, P2 being Instruction-Sequence of SCM+FSA for s1, s2 being State of SCM+FSA for I being Program of SCM+FSA st s1 . (intloc 0) = 1 & I is_closed_on s1,P1 & I is_halting_on s1,P1 & ( for a being read-write Int-Location holds s1 . a = s2 . a ) & ( for f being FinSeq-Location holds s1 . f = s2 . f ) holds DataPart (IExec (I,P1,s1)) = DataPart (IExec (I,P2,s2)) proofend; theorem Th20: :: SCMFSA8C:20 for P1, P2 being Instruction-Sequence of SCM+FSA for s1, s2 being State of SCM+FSA for I being Program of SCM+FSA st s1 . (intloc 0) = 1 & I is_closed_on s1,P1 & I is_halting_on s1,P1 & DataPart s1 = DataPart s2 holds DataPart (IExec (I,P1,s1)) = DataPart (IExec (I,P2,s2)) proofend; theorem Th21: :: SCMFSA8C:21 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_pseudo-closed_on s,P holds ( I is_pseudo-closed_on Initialize s,P +* I & pseudo-LifeSpan (s,P,I) = pseudo-LifeSpan ((Initialize s),(P +* I),I) ) proofend; theorem Th22: :: SCMFSA8C:22 for P1, P2 being Instruction-Sequence of SCM+FSA for s1 being 0 -started State of SCM+FSA for s2 being State of SCM+FSA for I being Program of SCM+FSA st I c= P1 & I is_pseudo-closed_on s1,P1 holds for n being Element of NAT st Reloc (I,n) c= P2 & IC s2 = n & DataPart s1 = DataPart s2 holds ( ( for i being Element of NAT st i < pseudo-LifeSpan (s1,P1,I) holds IncAddr ((CurInstr (P1,(Comput (P1,s1,i)))),n) = CurInstr (P2,(Comput (P2,s2,i))) ) & ( for i being Element of NAT st i <= pseudo-LifeSpan (s1,P1,I) holds ( (IC (Comput (P1,s1,i))) + n = IC (Comput (P2,s2,i)) & DataPart (Comput (P1,s1,i)) = DataPart (Comput (P2,s2,i)) ) ) ) proofend; theorem Th23: :: SCMFSA8C:23 for P1, P2 being Instruction-Sequence of SCM+FSA for s1, s2 being State of SCM+FSA for I being Program of SCM+FSA st DataPart s1 = DataPart s2 & I is_pseudo-closed_on s1,P1 holds I is_pseudo-closed_on s2,P2 proofend; theorem Th24: :: SCMFSA8C:24 for P being Instruction-Sequence of SCM+FSA for s being State of SCM+FSA for I being Program of SCM+FSA st s . (intloc 0) = 1 holds ( I is_pseudo-closed_on s,P iff I is_pseudo-closed_on Initialized s,P ) proofend; theorem Th25: :: SCMFSA8C:25 for a being Int-Location for I, J being Program of SCM+FSA holds ( 0 in dom (if=0 (a,I,J)) & 1 in dom (if=0 (a,I,J)) & 0 in dom (if>0 (a,I,J)) & 1 in dom (if>0 (a,I,J)) ) proofend; theorem Th26: :: SCMFSA8C:26 for a being Int-Location for I, J being Program of SCM+FSA holds ( (if=0 (a,I,J)) . 0 = a =0_goto ((card J) + 3) & (if=0 (a,I,J)) . 1 = goto 2 & (if>0 (a,I,J)) . 0 = a >0_goto ((card J) + 3) & (if>0 (a,I,J)) . 1 = goto 2 ) proofend; theorem Th27: :: SCMFSA8C:27 for a being Int-Location for I, J being Program of SCM+FSA for n being Element of NAT st n < ((card I) + (card J)) + 3 holds ( n in dom (if=0 (a,I,J)) & (if=0 (a,I,J)) . n <> halt SCM+FSA ) proofend; theorem Th28: :: SCMFSA8C:28 for a being Int-Location for I, J being Program of SCM+FSA for n being Element of NAT st n < ((card I) + (card J)) + 3 holds ( n in dom (if>0 (a,I,J)) & (if>0 (a,I,J)) . n <> halt SCM+FSA ) proofend; theorem Th29: :: SCMFSA8C:29 for P being Instruction-Sequence of SCM+FSA for s being State of SCM+FSA for I being Program of SCM+FSA st Directed I is_pseudo-closed_on s,P holds ( I ";" (Stop SCM+FSA) is_closed_on s,P & I ";" (Stop SCM+FSA) is_halting_on s,P & LifeSpan ((P +* (I ";" (Stop SCM+FSA))),(Initialize s)) = pseudo-LifeSpan (s,P,(Directed I)) & ( for n being Element of NAT st n < pseudo-LifeSpan (s,P,(Directed I)) holds IC (Comput ((P +* I),(Initialize s),n)) = IC (Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),n)) ) & ( for n being Element of NAT st n <= pseudo-LifeSpan (s,P,(Directed I)) holds DataPart (Comput ((P +* I),(Initialize s),n)) = DataPart (Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),n)) ) ) proofend; theorem Th30: :: SCMFSA8C:30 for P being Instruction-Sequence of SCM+FSA for s being State of SCM+FSA for I being Program of SCM+FSA st Directed I is_pseudo-closed_on s,P holds DataPart (Result ((P +* (I ";" (Stop SCM+FSA))),(Initialize s))) = DataPart (Comput ((P +* I),(Initialize s),(pseudo-LifeSpan (s,P,(Directed I))))) proofend; theorem :: SCMFSA8C:31 for P being Instruction-Sequence of SCM+FSA for s being State of SCM+FSA for I being Program of SCM+FSA st s . (intloc 0) = 1 & Directed I is_pseudo-closed_on s,P holds DataPart (IExec ((I ";" (Stop SCM+FSA)),P,s)) = DataPart (Comput ((P +* I),(Initialize s),(pseudo-LifeSpan (s,P,(Directed I))))) proofend; theorem Th32: :: SCMFSA8C:32 for I, J being Program of SCM+FSA for a being Int-Location holds (if=0 (a,I,J)) . (((card I) + (card J)) + 3) = halt SCM+FSA proofend; theorem Th33: :: SCMFSA8C:33 for I, J being Program of SCM+FSA for a being Int-Location holds (if>0 (a,I,J)) . (((card I) + (card J)) + 3) = halt SCM+FSA proofend; theorem Th34: :: SCMFSA8C:34 for I, J being Program of SCM+FSA for a being Int-Location holds (if=0 (a,I,J)) . ((card J) + 2) = goto (((card I) + (card J)) + 3) proofend; theorem Th35: :: SCMFSA8C:35 for I, J being Program of SCM+FSA for a being Int-Location holds (if>0 (a,I,J)) . ((card J) + 2) = goto (((card I) + (card J)) + 3) proofend; theorem Th36: :: SCMFSA8C:36 for J being Program of SCM+FSA for a being Int-Location holds (if=0 (a,(Goto 2),J)) . ((card J) + 3) = goto ((card J) + 5) proofend; theorem Th37: :: SCMFSA8C:37 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 & Directed I is_pseudo-closed_on s,P holds ( if=0 (a,I,J) is_halting_on s,P & if=0 (a,I,J) is_closed_on s,P & LifeSpan ((P +* (if=0 (a,I,J))),(Initialize s)) = (LifeSpan ((P +* (I ";" (Stop SCM+FSA))),(Initialize s))) + 1 ) proofend; theorem :: SCMFSA8C:38 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 . (intloc 0) = 1 & s . a = 0 & Directed I is_pseudo-closed_on s,P holds DataPart (IExec ((if=0 (a,I,J)),P,s)) = DataPart (IExec ((I ";" (Stop SCM+FSA)),P,s)) proofend; theorem Th39: :: SCMFSA8C: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 & Directed I is_pseudo-closed_on s,P holds ( if>0 (a,I,J) is_halting_on s,P & if>0 (a,I,J) is_closed_on s,P & LifeSpan ((P +* (if>0 (a,I,J))),(Initialize s)) = (LifeSpan ((P +* (I ";" (Stop SCM+FSA))),(Initialize s))) + 1 ) proofend; theorem Th40: :: SCMFSA8C: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 . (intloc 0) = 1 & s . a > 0 & Directed I is_pseudo-closed_on s,P holds DataPart (IExec ((if>0 (a,I,J)),P,s)) = DataPart (IExec ((I ";" (Stop SCM+FSA)),P,s)) proofend; theorem Th41: :: SCMFSA8C: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 & Directed J is_pseudo-closed_on s,P holds ( if=0 (a,I,J) is_halting_on s,P & if=0 (a,I,J) is_closed_on s,P & LifeSpan ((P +* (if=0 (a,I,J))),(Initialize s)) = (LifeSpan ((P +* (J ";" (Stop SCM+FSA))),(Initialize s))) + 3 ) proofend; theorem :: SCMFSA8C:42 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 . (intloc 0) = 1 & s . a <> 0 & Directed J is_pseudo-closed_on s,P holds DataPart (IExec ((if=0 (a,I,J)),P,s)) = DataPart (IExec ((J ";" (Stop SCM+FSA)),P,s)) proofend; theorem Th43: :: SCMFSA8C:43 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 & Directed J is_pseudo-closed_on s,P holds ( if>0 (a,I,J) is_halting_on s,P & if>0 (a,I,J) is_closed_on s,P & LifeSpan ((P +* (if>0 (a,I,J))),(s +* (Start-At (0,SCM+FSA)))) = (LifeSpan ((P +* (J ";" (Stop SCM+FSA))),(Initialize s))) + 3 ) proofend; theorem Th44: :: SCMFSA8C:44 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 . (intloc 0) = 1 & s . a <= 0 & Directed J is_pseudo-closed_on s,P holds DataPart (IExec ((if>0 (a,I,J)),P,s)) = DataPart (IExec ((J ";" (Stop SCM+FSA)),P,s)) proofend; theorem :: SCMFSA8C: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 Directed I is_pseudo-closed_on s,P & Directed J is_pseudo-closed_on s,P holds ( if=0 (a,I,J) is_closed_on s,P & if=0 (a,I,J) is_halting_on s,P ) proofend; theorem :: SCMFSA8C: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 Directed I is_pseudo-closed_on s,P & Directed J is_pseudo-closed_on s,P holds ( if>0 (a,I,J) is_closed_on s,P & if>0 (a,I,J) is_halting_on s,P ) proofend; theorem :: SCMFSA8C:47 for I being Program of SCM+FSA for a being Int-Location st not I destroys a holds not Directed I destroys a by SCMFSA8A:13; theorem Th48: :: SCMFSA8C:48 for i being Instruction of SCM+FSA for a being Int-Location st not i destroys a holds not Macro i destroys a proofend; theorem Th49: :: SCMFSA8C:49 for a being Int-Location holds not halt SCM+FSA refers a proofend; theorem :: SCMFSA8C:50 for a, b, c being Int-Location st a <> b holds not AddTo (c,b) refers a proofend; theorem :: SCMFSA8C:51 for i being Instruction of SCM+FSA for a being Int-Location st not i refers a holds not Macro i refers a proofend; theorem Th52: :: SCMFSA8C:52 for I, J being Program of SCM+FSA for a being Int-Location st not I destroys a & not J destroys a holds not I ";" J destroys a proofend; theorem Th53: :: SCMFSA8C:53 for J being Program of SCM+FSA for i being Instruction of SCM+FSA for a being Int-Location st not i destroys a & not J destroys a holds not i ";" J destroys a proofend; theorem :: SCMFSA8C:54 for I being Program of SCM+FSA for j being Instruction of SCM+FSA for a being Int-Location st not I destroys a & not j destroys a holds not I ";" j destroys a proofend; theorem :: SCMFSA8C:55 for i, j being Instruction of SCM+FSA for a being Int-Location st not i destroys a & not j destroys a holds not i ";" j destroys a proofend; theorem Th56: :: SCMFSA8C:56 for a being Int-Location holds not Stop SCM+FSA destroys a proofend; theorem Th57: :: SCMFSA8C:57 for a being Int-Location for l being Element of NAT holds not Goto l destroys a proofend; theorem Th58: :: SCMFSA8C: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_halting_on Initialized s,P holds ( ( 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 ) & ( for f being FinSeq-Location holds (IExec (I,P,s)) . f = (Comput ((P +* I),(Initialize (Initialized s)),(LifeSpan ((P +* I),(Initialize (Initialized s)))))) . f ) ) proofend; theorem Th59: :: SCMFSA8C:59 for P being Instruction-Sequence of SCM+FSA for s being State of SCM+FSA for I being parahalting 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 Th60: :: SCMFSA8C:60 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 for k being Element of NAT st I is_closed_on Initialized s,P & I is_halting_on Initialized s,P & not I destroys a holds (IExec (I,P,s)) . a = (Comput ((P +* I),(Initialize (Initialized s)),k)) . a proofend; theorem Th61: :: SCMFSA8C:61 for P being Instruction-Sequence of SCM+FSA for s being State of SCM+FSA for I being parahalting 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; theorem Th62: :: SCMFSA8C:62 for P being Instruction-Sequence of SCM+FSA for s being State of SCM+FSA for I being parahalting 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 Th63: :: SCMFSA8C:63 for P being Instruction-Sequence of SCM+FSA for s being State of SCM+FSA for I being keeping_0 Program of SCM+FSA st I is_halting_on Initialized s,P holds ( (IExec (I,P,s)) . (intloc 0) = 1 & ( for k being Element of NAT holds (Comput ((P +* I),(Initialize (Initialized s)),k)) . (intloc 0) = 1 ) ) proofend; theorem Th64: :: SCMFSA8C:64 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 holds for k being Element of NAT st IC (Comput ((P +* I),(Initialize s),k)) in dom I holds (Comput ((P +* I),(Initialize s),(k + 1))) . a = (Comput ((P +* I),(Initialize s),k)) . a proofend; theorem Th65: :: SCMFSA8C:65 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 holds for m being Element of NAT st ( for n being Element of NAT st n < m holds IC (Comput ((P +* I),(Initialize s),n)) in dom I ) holds for n being Element of NAT st n <= m holds (Comput ((P +* I),(Initialize s),n)) . a = s . a proofend; theorem Th66: :: SCMFSA8C:66 for P being Instruction-Sequence of SCM+FSA for s being State of SCM+FSA for I being good Program of SCM+FSA for m being Element of NAT st ( for n being Element of NAT st n < m holds IC (Comput ((P +* I),(Initialize s),n)) in dom I ) holds for n being Element of NAT st n <= m holds (Comput ((P +* I),(Initialize s),n)) . (intloc 0) = s . (intloc 0) proofend; theorem Th67: :: SCMFSA8C:67 for P being Instruction-Sequence of SCM+FSA for s being State of SCM+FSA for I being good Program of SCM+FSA st I is_halting_on Initialized s,P & I is_closed_on Initialized s,P holds ( (IExec (I,P,s)) . (intloc 0) = 1 & ( for k being Element of NAT holds (Comput ((P +* I),(Initialize (Initialized s)),k)) . (intloc 0) = 1 ) ) proofend; theorem :: SCMFSA8C:68 for P being Instruction-Sequence of SCM+FSA for s being State of SCM+FSA for I being good Program of SCM+FSA st I is_closed_on s,P holds for k being Element of NAT holds (Comput ((P +* I),(Initialize s),k)) . (intloc 0) = s . (intloc 0) proofend; theorem Th69: :: SCMFSA8C:69 for P being Instruction-Sequence of SCM+FSA for s being State of SCM+FSA for I being keeping_0 parahalting 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 Th70: :: SCMFSA8C:70 for i being Instruction of SCM+FSA st not i destroys intloc 0 holds Macro i is good proofend; theorem Th71: :: SCMFSA8C:71 for P1, P2 being Instruction-Sequence of SCM+FSA for s1, s2 being State of SCM+FSA for I being Program of SCM+FSA st I is_closed_on s1,P1 & I is_halting_on s1,P1 & DataPart s1 = DataPart s2 holds for k being Element of NAT holds ( Comput ((P1 +* I),(Initialize s1),k) = Comput ((P2 +* I),(Initialize s2),k) & CurInstr ((P1 +* I),(Comput ((P1 +* I),(Initialize s1),k))) = CurInstr ((P2 +* I),(Comput ((P2 +* I),(Initialize s2),k))) ) proofend; theorem Th72: :: SCMFSA8C:72 for P1, P2 being Instruction-Sequence of SCM+FSA for s1, s2 being State of SCM+FSA for I being Program of SCM+FSA st I is_closed_on s1,P1 & I is_halting_on s1,P1 & DataPart s1 = DataPart s2 holds ( LifeSpan ((P1 +* I),(Initialize s1)) = LifeSpan ((P2 +* I),(Initialize s2)) & Result ((P1 +* I),(Initialize s1)) = Result ((P2 +* I),(Initialize s2)) ) proofend; theorem Th73: :: SCMFSA8C:73 for P1, P2 being Instruction-Sequence of SCM+FSA for s1, s2 being 0 -started State of SCM+FSA for I being Program of SCM+FSA st I is_closed_on s1,P1 & I is_halting_on s1,P1 & I c= P1 & I c= P2 & ex k being Element of NAT st Comput (P1,s1,k) = s2 holds Result (P1,s1) = Result (P2,s2) proofend; begin definition let I be Program of SCM+FSA; func loop I -> halt-free Program of SCM+FSA equals :: SCMFSA8C:def 1 Directed (I,0); coherence Directed (I,0) is halt-free Program of SCM+FSA proofend; end; :: deftheorem defines loop SCMFSA8C:def_1_:_ for I being Program of SCM+FSA holds loop I = Directed (I,0); theorem :: SCMFSA8C:74 for I being Program of SCM+FSA for a being Int-Location st loop I destroys a holds I destroys a by SCMFSA8A:13; registration let I be good Program of SCM+FSA; cluster loop I -> halt-free good ; correctness coherence loop I is good ; ; end; theorem Th75: :: SCMFSA8C:75 for I being Program of SCM+FSA holds not halt SCM+FSA in rng (loop I) by FUNCT_4:100; theorem Th76: :: SCMFSA8C:76 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_on s,P & I is_halting_on s,P holds for m being Element of NAT st m <= LifeSpan ((P +* I),(Initialize s)) holds Comput ((P +* I),(Initialize s),m) = Comput ((P +* (loop I)),(Initialize s),m) proofend; theorem Th77: :: SCMFSA8C:77 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_on s,P & I is_halting_on s,P holds for m being Element of NAT st m < LifeSpan ((P +* I),(Initialize s)) holds CurInstr ((P +* I),(Comput ((P +* I),(Initialize s),m))) = CurInstr ((P +* (loop I)),(Comput ((P +* (loop I)),(Initialize s),m))) proofend; Lm1: 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_on s,P & I is_halting_on s,P holds ( CurInstr ((P +* (loop I)),(Comput ((P +* (loop I)),(Initialize s),(LifeSpan ((P +* I),(Initialize s)))))) = goto 0 & ( for m being Element of NAT st m <= LifeSpan ((P +* I),(Initialize s)) holds CurInstr ((P +* (loop I)),(Comput ((P +* (loop I)),(Initialize s),m))) <> halt SCM+FSA ) ) proofend; theorem :: SCMFSA8C:78 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_on s,P & I is_halting_on s,P holds for m being Element of NAT st m <= LifeSpan ((P +* I),(Initialize s)) holds CurInstr ((P +* (loop I)),(Comput ((P +* (loop I)),(Initialize s),m))) <> halt SCM+FSA by Lm1; theorem :: SCMFSA8C:79 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_on s,P & I is_halting_on s,P holds CurInstr ((P +* (loop I)),(Comput ((P +* (loop I)),(Initialize s),(LifeSpan ((P +* I),(Initialize s)))))) = goto 0 by Lm1; theorem Th80: :: SCMFSA8C:80 for P being Instruction-Sequence of SCM+FSA for s being 0 -started State of SCM+FSA for I being paraclosed Program of SCM+FSA st 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 :: SCMFSA8C:81 for P being Instruction-Sequence of SCM+FSA for s being State of SCM+FSA for I being parahalting 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; begin definition let a be Int-Location; let I be Program of SCM+FSA; func Times (a,I) -> Program of SCM+FSA equals :: SCMFSA8C:def 2 if>0 (a,(loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))),(Stop SCM+FSA)); correctness coherence if>0 (a,(loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))),(Stop SCM+FSA)) is Program of SCM+FSA; ; end; :: deftheorem defines Times SCMFSA8C:def_2_:_ for a being Int-Location for I being Program of SCM+FSA holds Times (a,I) = if>0 (a,(loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))),(Stop SCM+FSA)); registration let a be Int-Location; let I be Program of SCM+FSA; cluster Times (a,I) -> non halt-free ; coherence not Times (a,I) is halt-free ; end; theorem Th82: :: SCMFSA8C:82 for I being good Program of SCM+FSA for a being read-write Int-Location holds if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))) is good proofend; theorem Th83: :: SCMFSA8C:83 for I, J being Program of SCM+FSA for a being Int-Location holds (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))) . ((card (I ";" (SubFrom (a,(intloc 0))))) + 3) = goto ((card (I ";" (SubFrom (a,(intloc 0))))) + 5) proofend; theorem Th84: :: SCMFSA8C:84 for P being Instruction-Sequence of SCM+FSA for s being State of SCM+FSA for I being good parahalting 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 :: SCMFSA8C:85 for P being Instruction-Sequence of SCM+FSA for s being State of SCM+FSA for I being good parahalting 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 :: SCMFSA8C:86 for P being Instruction-Sequence of SCM+FSA for s being State of SCM+FSA for I being good parahalting 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 :: SCMFSA8C:87 for I being good parahalting 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; theorem :: SCMFSA8C:88 for I, J being Program of SCM+FSA for a, c being Int-Location st not I destroys c & not J destroys c holds ( not if=0 (a,I,J) destroys c & not if>0 (a,I,J) destroys c ) proofend; theorem Th89: :: SCMFSA8C:89 for P being Instruction-Sequence of SCM+FSA for s being State of SCM+FSA for I being good parahalting Program of SCM+FSA for a being read-write Int-Location st not I destroys a & s . (intloc 0) = 1 & 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 = s +* (Start-At (0,SCM+FSA)) & 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))))))),(s +* (Start-At (0,SCM+FSA))))) + 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 Th90: :: SCMFSA8C:90 for P being Instruction-Sequence of SCM+FSA for s being State of SCM+FSA for I being good parahalting 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 Th91: :: SCMFSA8C:91 for P being Instruction-Sequence of SCM+FSA for s being State of SCM+FSA for I being good parahalting 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; begin theorem :: SCMFSA8C:92 for P being Instruction-Sequence of SCM+FSA for s being State of SCM+FSA for a, b, c being read-write Int-Location st a <> b & a <> c & b <> c & s . a >= 0 holds (IExec ((Times (a,(Macro (AddTo (b,c))))),P,s)) . b = (s . b) + ((s . c) * (s . a)) proofend;