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₁[ Nat] means ((StepWhile>0 a,Ig,s) . $1) . (intloc 0 ) = 1;
A3: 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 A4: ((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 Th37;
hence S₁[k + 1] by A4, SCMFSA6A:38; :: thesis: verum

end;

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

set SWkI = ((StepWhile>0 a,Ig,s) . k) +* (Initialized Ig);
set ISWk = Initialized ((StepWhile>0 a,Ig,s) . k);
A6: DataPart ((StepWhile>0 a,Ig,s) . k) = DataPart (Initialized ((StepWhile>0 a,Ig,s) . k)) by A4, SCMFSA8C:27;
set Ins = NAT ;
set SWkIS = ((StepWhile>0 a,Ig,s) . k) +* (Ig +* (Start-At 0 ,SCM+FSA ));
NAT misses Int-Locations \/ FinSeq-Locations by SCMFSA_2:13, SCMFSA_2:14, XBOOLE_1:70;
then A7: dom (((StepWhile>0 a,Ig,s) . k) | NAT ) misses Int-Locations \/ FinSeq-Locations by SCMFSA8A:3;
A8: ((StepWhile>0 a,Ig,s) . k) +* (Initialized Ig) = ((StepWhile>0 a,Ig,s) . k) +* (Ig +* (Start-At 0 ,SCM+FSA )) by A4, SCMFSA8C:18;
A9: ProperBodyWhile>0 a,Ig,s by A1, Th32;
then A10: Ig is_closed_on (StepWhile>0 a,Ig,s) . k by A5, Def4;
Ig is_halting_on (StepWhile>0 a,Ig,s) . k by A5, A9, Def4;
then A11: Ig is_halting_on Initialized ((StepWhile>0 a,Ig,s) . k) by A10, A6, SCMFSA8B:8;
then Initialized Ig is_halting_on (StepWhile>0 a,Ig,s) . k by SCMFSA8C:22;
then X: ( Start-At 0 ,SCM+FSA c= Initialized Ig & ProgramPart (((StepWhile>0 a,Ig,s) . k) +* ((Initialized Ig) +* (Start-At 0 ,SCM+FSA ))) halts_on ((StepWhile>0 a,Ig,s) . k) +* ((Initialized Ig) +* (Start-At 0 ,SCM+FSA )) ) by SCMFSA6B:4, SCMFSA7B:def 8;
then ((StepWhile>0 a,Ig,s) . k) +* (Initialized Ig) = ((StepWhile>0 a,Ig,s) . k) +* ((Initialized Ig) +* (Start-At 0 ,SCM+FSA )) by FUNCT_4:79;
then A12: ProgramPart (((StepWhile>0 a,Ig,s) . k) +* (Initialized Ig)) halts_on ((StepWhile>0 a,Ig,s) . k) +* (Initialized Ig) by X;
A13: DataPart (IExec Ig,((StepWhile>0 a,Ig,s) . k)) = DataPart ((Result (ProgramPart (((StepWhile>0 a,Ig,s) . k) +* (Initialized Ig))),(((StepWhile>0 a,Ig,s) . k) +* (Initialized Ig))) +* (((StepWhile>0 a,Ig,s) . k) | NAT )) by SCMFSA6B:def 1
.= DataPart (Result (ProgramPart (((StepWhile>0 a,Ig,s) . k) +* (Initialized Ig))),(((StepWhile>0 a,Ig,s) . k) +* (Initialized Ig))) by A7, FUNCT_4:76, SCMFSA_2:127
.= DataPart (Comput (ProgramPart (((StepWhile>0 a,Ig,s) . k) +* (Ig +* (Start-At 0 ,SCM+FSA )))),(((StepWhile>0 a,Ig,s) . k) +* (Ig +* (Start-At 0 ,SCM+FSA ))),(LifeSpan (ProgramPart (((StepWhile>0 a,Ig,s) . k) +* (Ig +* (Start-At 0 ,SCM+FSA )))),(((StepWhile>0 a,Ig,s) . k) +* (Ig +* (Start-At 0 ,SCM+FSA ))))) by A8, A12, AMI_1:122 ;
Ig is_closed_on Initialized ((StepWhile>0 a,Ig,s) . k) by A10, A6, SCMFSA8B:6;
then DataPart ((StepWhile>0 a,Ig,s) . (k + 1)) = DataPart (IExec Ig,((StepWhile>0 a,Ig,s) . k)) by A4, A5, A11, Th38;
hence ((StepWhile>0 a,Ig,s) . (k + 1)) . (intloc 0 ) = (Comput (ProgramPart (((StepWhile>0 a,Ig,s) . k) +* (Ig +* (Start-At 0 ,SCM+FSA )))),(((StepWhile>0 a,Ig,s) . k) +* (Ig +* (Start-At 0 ,SCM+FSA ))),(LifeSpan (ProgramPart (((StepWhile>0 a,Ig,s) . k) +* (Ig +* (Start-At 0 ,SCM+FSA )))),(((StepWhile>0 a,Ig,s) . k) +* (Ig +* (Start-At 0 ,SCM+FSA ))))) . (intloc 0 ) by A13, SCMFSA6A:38
.= 1 by A4, A10, SCMFSA8C:97 ;
:: thesis: verum

end;

end;

end;

A14: S₁[ 0 ] by A2, SCMFSA_9:def 5;
thus for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A14, A3); :: thesis: verum