let p be the Instructions of SCM+FSA -valued ManySortedSet of NAT ; :: thesis: for s being State of SCM+FSA
for a being read-write Int-Location
for Ig being good Program of SCM+FSA st ( ProperBodyWhile>0 a,Ig,s,p or Ig is parahalting ) & s . (intloc 0) = 1 holds
for k being Element of NAT holds ((StepWhile>0 (a,Ig,p,s)) . k) . (intloc 0) = 1
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,p or Ig is parahalting ) & s . (intloc 0) = 1 holds
for k being Element of NAT holds ((StepWhile>0 (a,Ig,p,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,p or Ig is parahalting ) & s . (intloc 0) = 1 holds
for k being Element of NAT holds ((StepWhile>0 (a,Ig,p,s)) . k) . (intloc 0) = 1
let Ig be good Program of SCM+FSA; :: thesis: ( ( ProperBodyWhile>0 a,Ig,s,p or Ig is parahalting ) & s . (intloc 0) = 1 implies for k being Element of NAT holds ((StepWhile>0 (a,Ig,p,s)) . k) . (intloc 0) = 1 )
set I = Ig;
assume that
A1: ( ProperBodyWhile>0 a,Ig,s,p or Ig is parahalting ) and
A2: s . (intloc 0) = 1 ; :: thesis: for k being Element of NAT holds ((StepWhile>0 (a,Ig,p,s)) . k) . (intloc 0) = 1
set SW = StepWhile>0 (a,Ig,p,s);
set PW = p +* (while>0 (a,Ig));
defpred S₁[ Nat] means ((StepWhile>0 (a,Ig,p,s)) . $1) . (intloc 0) = 1;
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,p,s)) . k) . (intloc 0) = 1 ; :: thesis: S₁[k + 1]

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

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

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

end;

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

set SWkI = ((StepWhile>0 (a,Ig,p,s)) . k) +* (Initialize ((intloc 0) .--> 1));
set PWI = (p +* (while>0 (a,Ig))) +* Ig;
set ISWk = Initialized ((StepWhile>0 (a,Ig,p,s)) . k);
A7: DataPart ((StepWhile>0 (a,Ig,p,s)) . k) = DataPart (Initialized ((StepWhile>0 (a,Ig,p,s)) . k)) by A5, SCMFSA8C:27;
set Ins = NAT ;
set SWkIS = Initialize ((StepWhile>0 (a,Ig,p,s)) . k);
set PWIS = (p +* (while>0 (a,Ig))) +* Ig;
A8: dom (((StepWhile>0 (a,Ig,p,s)) . k) | NAT) c= NAT by RELAT_1:87;
NAT misses Int-Locations \/ FinSeq-Locations by SCMFSA_2:13, SCMFSA_2:14, XBOOLE_1:70;
then A9: dom (((StepWhile>0 (a,Ig,p,s)) . k) | NAT) misses Int-Locations \/ FinSeq-Locations by A8, XBOOLE_1:63;
A10: ((StepWhile>0 (a,Ig,p,s)) . k) +* (Initialize ((intloc 0) .--> 1)) = Initialize ((StepWhile>0 (a,Ig,p,s)) . k) by A5, SCMFSA8C:18;
A11: ProperBodyWhile>0 a,Ig,s,p by A1, Th32;
then A12: Ig is_closed_on (StepWhile>0 (a,Ig,p,s)) . k,p +* (while>0 (a,Ig)) by A6, Def4;
Ig is_halting_on (StepWhile>0 (a,Ig,p,s)) . k,p +* (while>0 (a,Ig)) by A6, A11, Def4;
then A14: Ig is_halting_on Initialized ((StepWhile>0 (a,Ig,p,s)) . k),p +* (while>0 (a,Ig)) by A12, A7, SCMFSA8B:8;
XX: Start-At (0,SCM+FSA) c= Initialized ((StepWhile>0 (a,Ig,p,s)) . k) by SCMFSA6B:4;
((StepWhile>0 (a,Ig,p,s)) . k) +* (Initialize ((intloc 0) .--> 1)) = ((StepWhile>0 (a,Ig,p,s)) . k) +* (Initialize ((intloc 0) .--> 1))
.= Initialized ((StepWhile>0 (a,Ig,p,s)) . k)
.= Initialize (Initialized ((StepWhile>0 (a,Ig,p,s)) . k)) by XX, FUNCT_4:104 ;
then B15: (p +* (while>0 (a,Ig))) +* Ig halts_on ((StepWhile>0 (a,Ig,p,s)) . k) +* (Initialize ((intloc 0) .--> 1)) by A14, SCMFSA7B:def 8;
A16: (p +* (while>0 (a,Ig))) +* Ig halts_on ((StepWhile>0 (a,Ig,p,s)) . k) +* (Initialize ((intloc 0) .--> 1)) by B15;
A17: DataPart (IExec (Ig,(p +* (while>0 (a,Ig))),((StepWhile>0 (a,Ig,p,s)) . k))) = DataPart ((Result (((p +* (while>0 (a,Ig))) +* Ig),(((StepWhile>0 (a,Ig,p,s)) . k) +* (Initialize ((intloc 0) .--> 1))))) +* (((StepWhile>0 (a,Ig,p,s)) . k) | NAT)) by SCMFSA6B:def 1
.= DataPart (Result (((p +* (while>0 (a,Ig))) +* Ig),(((StepWhile>0 (a,Ig,p,s)) . k) +* (Initialize ((intloc 0) .--> 1))))) by A9, FUNCT_4:76, SCMFSA_2:127
.= DataPart (Comput (((p +* (while>0 (a,Ig))) +* Ig),(Initialize ((StepWhile>0 (a,Ig,p,s)) . k)),(LifeSpan (((p +* (while>0 (a,Ig))) +* Ig),(Initialize ((StepWhile>0 (a,Ig,p,s)) . k)))))) by A10, A16, EXTPRO_1:23 ;
Ig is_closed_on Initialized ((StepWhile>0 (a,Ig,p,s)) . k),p +* (while>0 (a,Ig)) by A12, A7, SCMFSA8B:6;
then DataPart ((StepWhile>0 (a,Ig,p,s)) . (k + 1)) = DataPart (IExec (Ig,(p +* (while>0 (a,Ig))),((StepWhile>0 (a,Ig,p,s)) . k))) by A5, A6, A14, Th38;
hence ((StepWhile>0 (a,Ig,p,s)) . (k + 1)) . (intloc 0) = (Comput (((p +* (while>0 (a,Ig))) +* Ig),(Initialize ((StepWhile>0 (a,Ig,p,s)) . k)),(LifeSpan (((p +* (while>0 (a,Ig))) +* Ig),(Initialize ((StepWhile>0 (a,Ig,p,s)) . k)))))) . (intloc 0) by A17, SCMFSA6A:38
.= 1 by A5, A12, SCMFSA8C:97 ;
:: thesis: verum

end;

end;

end;

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