let s be State of SCM+FSA; :: thesis: for p being Instruction-Sequence of SCM+FSA
for a being Int-Location
for J being really-closed good MacroInstruction of SCM+FSA st s . (intloc 0) = 1 & ( ProperTimesBody a,J,s,p or J is parahalting ) holds
times (a,J) is_halting_on s,p
let p be Instruction-Sequence of SCM+FSA; :: thesis: for a being Int-Location
for J being really-closed good MacroInstruction of SCM+FSA st s . (intloc 0) = 1 & ( ProperTimesBody a,J,s,p or J is parahalting ) holds
times (a,J) is_halting_on s,p
let a be Int-Location; :: thesis: for J being really-closed good MacroInstruction of SCM+FSA st s . (intloc 0) = 1 & ( ProperTimesBody a,J,s,p or J is parahalting ) holds
times (a,J) is_halting_on s,p
let J be really-closed good MacroInstruction of SCM+FSA ; :: thesis: ( s . (intloc 0) = 1 & ( ProperTimesBody a,J,s,p or J is parahalting ) implies times (a,J) is_halting_on s,p )
set I = J;
assume A1: s . (intloc 0) = 1 ; :: thesis: ( ( not ProperTimesBody a,J,s,p & not J is parahalting ) or times (a,J) is_halting_on s,p )
set taI = times (a,J);
set ST = StepTimes (a,J,p,s);
set au = 1 -stRWNotIn ({a} \/ (UsedILoc J));
set ISu = J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(intloc 0)));
set WH = while>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(intloc 0)))));
set s1 = Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s));
set Is1 = Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s)));
set SW = StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(intloc 0)))),p,(Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s))));
set ISW = StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(intloc 0)))),p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s)))));
A2: Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s)) = IExec ((Macro ((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a)),p,s) by SCMFSA6C:5;
(Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s))) . (intloc 0) = (Initialized s) . (intloc 0) by SCMFSA_2:63
.= 1 by SCMFSA_M:9 ;
then A3: DataPart (Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s)))) = DataPart (Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s))) by SCMFSA_M:19;
assume A4: ( ProperTimesBody a,J,s,p or J is parahalting ) ; :: thesis: times (a,J) is_halting_on s,p
then A5: ProperTimesBody a,J,s,p by Th11;
A6: Macro ((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a) is_halting_on Initialized s,p by SCMFSA7B:19;