let s be State of SCM+FSA ; :: thesis: for a being read-write Int-Location
for Ig being good Program of SCM+FSA st ( ProperBodyWhile=0 a,Ig,s or Ig is parahalting ) & s . (intloc 0 ) = 1 holds
for k being Element of NAT holds ((StepWhile=0 a,Ig,s) . k) . (intloc 0 ) = 1
let a be read-write Int-Location ; :: thesis: for Ig being good Program of SCM+FSA st ( ProperBodyWhile=0 a,Ig,s or Ig is parahalting ) & s . (intloc 0 ) = 1 holds
for k being Element of NAT holds ((StepWhile=0 a,Ig,s) . k) . (intloc 0 ) = 1
let Ig be good Program of SCM+FSA ; :: thesis: ( ( ProperBodyWhile=0 a,Ig,s or Ig is parahalting ) & s . (intloc 0 ) = 1 implies for k being Element of NAT holds ((StepWhile=0 a,Ig,s) . k) . (intloc 0 ) = 1 )
set I = Ig;
assume that
A1: ( ProperBodyWhile=0 a,Ig,s or Ig is parahalting ) and
A2: s . (intloc 0 ) = 1 ; :: thesis: for k being Element of NAT holds ((StepWhile=0 a,Ig,s) . k) . (intloc 0 ) = 1
set SW = StepWhile=0 a,Ig,s;
defpred S₁[ Element of NAT ] means ((StepWhile=0 a,Ig,s) . $1) . (intloc 0 ) = 1;
A3: S₁[ 0 ] by A2, SCMFSA_9:def 4;
A4: for k being Element of NAT st S₁[k] holds
S₁[k + 1]

proof

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A5: ((StepWhile=0 a,Ig,s) . k) . (intloc 0 ) = 1 ; :: thesis: S₁[k + 1]

per cases ( ((StepWhile=0 a,Ig,s) . k) . a <> 0 or ((StepWhile=0 a,Ig,s) . k) . a = 0 ) ;

suppose ((StepWhile=0 a,Ig,s) . k) . a <> 0 ; :: thesis: S₁[k + 1]

then DataPart ((StepWhile=0 a,Ig,s) . (k + 1)) = DataPart ((StepWhile=0 a,Ig,s) . k) by Th24;
hence S₁[k + 1] by A5, SCMFSA6A:38; :: thesis: verum

end;

suppose A6: ((StepWhile=0 a,Ig,s) . k) . a = 0 ; :: thesis: S₁[k + 1]

ProperBodyWhile=0 a,Ig,s by A1, Th19;
then A7: ( Ig is_closed_on (StepWhile=0 a,Ig,s) . k & Ig is_halting_on (StepWhile=0 a,Ig,s) . k ) by A6, Def1;
set ISWk = Initialize ((StepWhile=0 a,Ig,s) . k);
set SWkI = ((StepWhile=0 a,Ig,s) . k) +* (Initialized Ig);
set IS = Ig +* (Start-At (insloc 0 ));
set SWkIS = ((StepWhile=0 a,Ig,s) . k) +* (Ig +* (Start-At (insloc 0 )));
set Ins = NAT ;
A8: DataPart ((StepWhile=0 a,Ig,s) . k) = DataPart (Initialize ((StepWhile=0 a,Ig,s) . k)) by A5, SCMFSA8C:27;
then A9: Ig is_halting_on Initialize ((StepWhile=0 a,Ig,s) . k) by A7, SCMFSA8B:8;
A10: Ig is_closed_on Initialize ((StepWhile=0 a,Ig,s) . k) by A7, A8, SCMFSA8B:6;
A11: ((StepWhile=0 a,Ig,s) . k) +* (Initialized Ig) = ((StepWhile=0 a,Ig,s) . k) +* (Ig +* (Start-At (insloc 0 ))) by A5, SCMFSA8C:18;
A12: Start-At (insloc 0 ) c= Initialized Ig by SCMFSA6B:4;
Initialized Ig is_halting_on (StepWhile=0 a,Ig,s) . k by A9, SCMFSA8C:22;
then ((StepWhile=0 a,Ig,s) . k) +* ((Initialized Ig) +* (Start-At (insloc 0 ))) is halting by SCMFSA7B:def 8;
then A13: ((StepWhile=0 a,Ig,s) . k) +* (Initialized Ig) is halting by A12, FUNCT_4:79;
NAT misses Int-Locations \/ FinSeq-Locations by SCMFSA_2:13, SCMFSA_2:14, XBOOLE_1:70;
then A14: dom (((StepWhile=0 a,Ig,s) . k) | NAT ) misses Int-Locations \/ FinSeq-Locations by SCMFSA8A:3;
A15: DataPart (IExec Ig,((StepWhile=0 a,Ig,s) . k)) = DataPart ((Result (((StepWhile=0 a,Ig,s) . k) +* (Initialized Ig))) +* (((StepWhile=0 a,Ig,s) . k) | NAT )) by SCMFSA6B:def 1
.= DataPart (Result (((StepWhile=0 a,Ig,s) . k) +* (Initialized Ig))) by A14, FUNCT_4:94, SCMFSA_2:127
.= DataPart (Computation (((StepWhile=0 a,Ig,s) . k) +* (Ig +* (Start-At (insloc 0 )))),(LifeSpan (((StepWhile=0 a,Ig,s) . k) +* (Ig +* (Start-At (insloc 0 )))))) by A11, A13, AMI_1:122 ;
DataPart ((StepWhile=0 a,Ig,s) . (k + 1)) = DataPart (IExec Ig,((StepWhile=0 a,Ig,s) . k)) by A5, A6, A9, A10, Th25;
hence ((StepWhile=0 a,Ig,s) . (k + 1)) . (intloc 0 ) = (Computation (((StepWhile=0 a,Ig,s) . k) +* (Ig +* (Start-At (insloc 0 )))),(LifeSpan (((StepWhile=0 a,Ig,s) . k) +* (Ig +* (Start-At (insloc 0 )))))) . (intloc 0 ) by A15, SCMFSA6A:38
.= 1 by A5, A7, SCMFSA8C:97 ;
:: thesis: verum

end;

end;

end;

thus for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A3, A4); :: thesis: verum