let p be Instruction-Sequence of SCM+FSA; :: thesis: for s being State of SCM+FSA
for a being read-write Int-Location
for Ig being good really-closed MacroInstruction of SCM+FSA st ( ProperBodyWhile>0 a,Ig,s,p or Ig is parahalting ) & s . (intloc 0) = 1 holds
for k being 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 really-closed MacroInstruction of SCM+FSA st ( ProperBodyWhile>0 a,Ig,s,p or Ig is parahalting ) & s . (intloc 0) = 1 holds
for k being Nat holds ((StepWhile>0 (a,Ig,p,s)) . k) . (intloc 0) = 1
let a be read-write Int-Location; :: thesis: for Ig being good really-closed MacroInstruction of SCM+FSA st ( ProperBodyWhile>0 a,Ig,s,p or Ig is parahalting ) & s . (intloc 0) = 1 holds
for k being Nat holds ((StepWhile>0 (a,Ig,p,s)) . k) . (intloc 0) = 1
let Ig be good really-closed MacroInstruction of SCM+FSA ; :: thesis: ( ( ProperBodyWhile>0 a,Ig,s,p or Ig is parahalting ) & s . (intloc 0) = 1 implies for k being 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 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 S1[ Nat] means ((StepWhile>0 (a,Ig,p,s)) . $1) . (intloc 0) = 1;
A3: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A4: ((StepWhile>0 (a,Ig,p,s)) . k) . (intloc 0) = 1 ; :: thesis: S1[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: S1[k + 1]
then DataPart ((StepWhile>0 (a,Ig,p,s)) . (k + 1)) = DataPart ((StepWhile>0 (a,Ig,p,s)) . k) by Th31;
hence S1[k + 1] by A4, SCMFSA_M:2; :: thesis: verum
end;
suppose A5: ((StepWhile>0 (a,Ig,p,s)) . k) . a > 0 ; :: thesis: S1[k + 1]
set SWkI = Initialized ((StepWhile>0 (a,Ig,p,s)) . k);
set PWI = (p +* (while>0 (a,Ig))) +* Ig;
A6: DataPart ((StepWhile>0 (a,Ig,p,s)) . k) = DataPart (Initialized ((StepWhile>0 (a,Ig,p,s)) . k)) by A4, SCMFSA_M:19;
set Ins = NAT ;
set SWkIS = Initialize ((StepWhile>0 (a,Ig,p,s)) . k);
set PWIS = (p +* (while>0 (a,Ig))) +* Ig;
A7: Initialized ((StepWhile>0 (a,Ig,p,s)) . k) = Initialize ((StepWhile>0 (a,Ig,p,s)) . k) by A4, SCMFSA_M:18;
A8: ProperBodyWhile>0 a,Ig,s,p by A1, Th26;
Ig is_halting_on (StepWhile>0 (a,Ig,p,s)) . k,p +* (while>0 (a,Ig)) by A5, A8;
then A9: Ig is_halting_on Initialized ((StepWhile>0 (a,Ig,p,s)) . k),p +* (while>0 (a,Ig)) by A6, SCMFSA8B:5;
Initialized ((StepWhile>0 (a,Ig,p,s)) . k) = Initialize (Initialized ((StepWhile>0 (a,Ig,p,s)) . k)) by MEMSTR_0:44;
then A10: (p +* (while>0 (a,Ig))) +* Ig halts_on Initialized ((StepWhile>0 (a,Ig,p,s)) . k) by A9, SCMFSA7B:def 7;
A11: (p +* (while>0 (a,Ig))) +* Ig halts_on Initialized ((StepWhile>0 (a,Ig,p,s)) . k) by A10;
A12: DataPart (IExec (Ig,(p +* (while>0 (a,Ig))),((StepWhile>0 (a,Ig,p,s)) . k))) = DataPart (Result (((p +* (while>0 (a,Ig))) +* Ig),(Initialized ((StepWhile>0 (a,Ig,p,s)) . k)))) by SCMFSA6B:def 1
.= 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 A7, A11, EXTPRO_1:23 ;
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 A4, A5, A9, Th32;
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 A12, SCMFSA_M:2
.= 1 by A4, SCMFSA8C:68 ;
:: thesis: verum
end;
end;
end;
A13: S1[ 0 ] by A2, SCMFSA_9:def 5;
thus for k being Nat holds S1[k] from NAT_1:sch 2(A13, A3); :: thesis: verum