let s be State of SCM+FSA ; :: thesis: for a being read-write Int-Location
for I being Program of SCM+FSA
for k being Element of NAT st ( ( I is_halting_on Initialize ((StepWhile>0 a,I,s) . k) & I is_closed_on Initialize ((StepWhile>0 a,I,s) . k) ) or I is parahalting ) & ((StepWhile>0 a,I,s) . k) . a > 0 & ((StepWhile>0 a,I,s) . k) . (intloc 0 ) = 1 holds
DataPart ((StepWhile>0 a,I,s) . (k + 1)) = DataPart (IExec I,((StepWhile>0 a,I,s) . k))
let a be read-write Int-Location ; :: thesis: for I being Program of SCM+FSA
for k being Element of NAT st ( ( I is_halting_on Initialize ((StepWhile>0 a,I,s) . k) & I is_closed_on Initialize ((StepWhile>0 a,I,s) . k) ) or I is parahalting ) & ((StepWhile>0 a,I,s) . k) . a > 0 & ((StepWhile>0 a,I,s) . k) . (intloc 0 ) = 1 holds
DataPart ((StepWhile>0 a,I,s) . (k + 1)) = DataPart (IExec I,((StepWhile>0 a,I,s) . k))
let I be Program of SCM+FSA ; :: thesis: for k being Element of NAT st ( ( I is_halting_on Initialize ((StepWhile>0 a,I,s) . k) & I is_closed_on Initialize ((StepWhile>0 a,I,s) . k) ) or I is parahalting ) & ((StepWhile>0 a,I,s) . k) . a > 0 & ((StepWhile>0 a,I,s) . k) . (intloc 0 ) = 1 holds
DataPart ((StepWhile>0 a,I,s) . (k + 1)) = DataPart (IExec I,((StepWhile>0 a,I,s) . k))
let k be Element of NAT ; :: thesis: ( ( ( I is_halting_on Initialize ((StepWhile>0 a,I,s) . k) & I is_closed_on Initialize ((StepWhile>0 a,I,s) . k) ) or I is parahalting ) & ((StepWhile>0 a,I,s) . k) . a > 0 & ((StepWhile>0 a,I,s) . k) . (intloc 0 ) = 1 implies DataPart ((StepWhile>0 a,I,s) . (k + 1)) = DataPart (IExec I,((StepWhile>0 a,I,s) . k)) )
assume that
A1: ( ( I is_halting_on Initialize ((StepWhile>0 a,I,s) . k) & I is_closed_on Initialize ((StepWhile>0 a,I,s) . k) ) or I is parahalting ) and
A2: ((StepWhile>0 a,I,s) . k) . a > 0 and
A3: ((StepWhile>0 a,I,s) . k) . (intloc 0 ) = 1 ; :: thesis: DataPart ((StepWhile>0 a,I,s) . (k + 1)) = DataPart (IExec I,((StepWhile>0 a,I,s) . k))
set SW = StepWhile>0 a,I,s;
set ISWk = Initialize ((StepWhile>0 a,I,s) . k);
set SWkI = ((StepWhile>0 a,I,s) . k) +* (Initialized I);
set WHS = (while>0 a,I) +* (Start-At (insloc 0 ));
set IS = I +* (Start-At (insloc 0 ));
set SWkIS = ((StepWhile>0 a,I,s) . k) +* (I +* (Start-At (insloc 0 )));
set Ins = NAT ;
A4: ((StepWhile>0 a,I,s) . k) +* (Initialized I) = ((StepWhile>0 a,I,s) . k) +* (I +* (Start-At (insloc 0 ))) by A3, SCMFSA8C:18;
A5: Start-At (insloc 0 ) c= Initialized I by SCMFSA6B:4;
I is_halting_on Initialize ((StepWhile>0 a,I,s) . k) by A1, SCMFSA7B:25;
then Initialized I is_halting_on (StepWhile>0 a,I,s) . k by SCMFSA8C:22;
then ((StepWhile>0 a,I,s) . k) +* ((Initialized I) +* (Start-At (insloc 0 ))) is halting by SCMFSA7B:def 8;
then A6: ((StepWhile>0 a,I,s) . k) +* (Initialized I) is halting by A5, FUNCT_4:79;
NAT misses Int-Locations \/ FinSeq-Locations by SCMFSA_2:13, SCMFSA_2:14, XBOOLE_1:70;
then A7: dom (((StepWhile>0 a,I,s) . k) | NAT ) misses Int-Locations \/ FinSeq-Locations by SCMFSA8A:3;
A8: DataPart (IExec I,((StepWhile>0 a,I,s) . k)) = DataPart ((Result (((StepWhile>0 a,I,s) . k) +* (Initialized I))) +* (((StepWhile>0 a,I,s) . k) | NAT )) by SCMFSA6B:def 1
.= DataPart (Result (((StepWhile>0 a,I,s) . k) +* (Initialized I))) by A7, FUNCT_4:94, SCMFSA_2:127
.= DataPart (Computation (((StepWhile>0 a,I,s) . k) +* (I +* (Start-At (insloc 0 )))),(LifeSpan (((StepWhile>0 a,I,s) . k) +* (I +* (Start-At (insloc 0 )))))) by A4, A6, AMI_1:122 ;
A9: (StepWhile>0 a,I,s) . (k + 1) = Computation (((StepWhile>0 a,I,s) . k) +* ((while>0 a,I) +* (Start-At (insloc 0 )))),((LifeSpan (((StepWhile>0 a,I,s) . k) +* (I +* (Start-At (insloc 0 ))))) + 3) by SCMFSA_9:def 5;
A10: DataPart (Initialize ((StepWhile>0 a,I,s) . k)) = DataPart ((StepWhile>0 a,I,s) . k) by A3, SCMFSA8C:27;
A11: I is_closed_on (StepWhile>0 a,I,s) . k by A1, A10, SCMFSA7B:24, SCMFSA8B:6;
I is_halting_on (StepWhile>0 a,I,s) . k by A1, A10, SCMFSA7B:25, SCMFSA8B:8;
hence DataPart ((StepWhile>0 a,I,s) . (k + 1)) = DataPart (IExec I,((StepWhile>0 a,I,s) . k)) by A2, A8, A9, A11, Th36; :: thesis: verum