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 Initialized ((StepWhile=0 a,I,s) . k) & I is_closed_on Initialized ((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 Initialized ((StepWhile=0 a,I,s) . k) & I is_closed_on Initialized ((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 Initialized ((StepWhile=0 a,I,s) . k) & I is_closed_on Initialized ((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 Initialized ((StepWhile=0 a,I,s) . k) & I is_closed_on Initialized ((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)) )
set Ins = NAT ;
assume that
A1: ( ( I is_halting_on Initialized ((StepWhile=0 a,I,s) . k) & I is_closed_on Initialized ((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 ISWk = Initialized ((StepWhile=0 a,I,s) . k);
set SW = StepWhile=0 a,I,s;
set SWkI = ((StepWhile=0 a,I,s) . k) +* (Initialized I);
DataPart (Initialized ((StepWhile=0 a,I,s) . k)) = DataPart ((StepWhile=0 a,I,s) . k) by A3, SCMFSA8C:27;
then A4: ( I is_closed_on (StepWhile=0 a,I,s) . k & I is_halting_on (StepWhile=0 a,I,s) . k ) by A1, SCMFSA7B:24, SCMFSA7B:25, SCMFSA8B:8;
I is_halting_on Initialized ((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 X: ( Start-At 0 ,SCM+FSA c= Initialized I & ProgramPart (((StepWhile=0 a,I,s) . k) +* ((Initialized I) +* (Start-At 0 ,SCM+FSA ))) halts_on ((StepWhile=0 a,I,s) . k) +* ((Initialized I) +* (Start-At 0 ,SCM+FSA )) ) by SCMFSA6B:4, SCMFSA7B:def 8;
then ((StepWhile=0 a,I,s) . k) +* (Initialized I) = ((StepWhile=0 a,I,s) . k) +* ((Initialized I) +* (Start-At 0 ,SCM+FSA )) by FUNCT_4:79;
then A5: ProgramPart (((StepWhile=0 a,I,s) . k) +* (Initialized I)) halts_on ((StepWhile=0 a,I,s) . k) +* (Initialized I) by X;
NAT misses Int-Locations \/ FinSeq-Locations by SCMFSA_2:13, SCMFSA_2:14, XBOOLE_1:70;
then A6: dom (((StepWhile=0 a,I,s) . k) | NAT ) misses Int-Locations \/ FinSeq-Locations by SCMFSA8A:3;
set IS = I +* (Start-At 0 ,SCM+FSA );
set SWkIS = ((StepWhile=0 a,I,s) . k) +* (I +* (Start-At 0 ,SCM+FSA ));
A7: ((StepWhile=0 a,I,s) . k) +* (Initialized I) = ((StepWhile=0 a,I,s) . k) +* (I +* (Start-At 0 ,SCM+FSA )) by A3, SCMFSA8C:18;
set WHS = (while=0 a,I) +* (Start-At 0 ,SCM+FSA );
A8: (StepWhile=0 a,I,s) . (k + 1) = Comput (ProgramPart (((StepWhile=0 a,I,s) . k) +* ((while=0 a,I) +* (Start-At 0 ,SCM+FSA )))),(((StepWhile=0 a,I,s) . k) +* ((while=0 a,I) +* (Start-At 0 ,SCM+FSA ))),((LifeSpan (ProgramPart (((StepWhile=0 a,I,s) . k) +* (I +* (Start-At 0 ,SCM+FSA )))),(((StepWhile=0 a,I,s) . k) +* (I +* (Start-At 0 ,SCM+FSA )))) + 3) by SCMFSA_9:def 4;
DataPart (IExec I,((StepWhile=0 a,I,s) . k)) = DataPart ((Result (ProgramPart (((StepWhile=0 a,I,s) . k) +* (Initialized I))),(((StepWhile=0 a,I,s) . k) +* (Initialized I))) +* (((StepWhile=0 a,I,s) . k) | NAT )) by SCMFSA6B:def 1
.= DataPart (Result (ProgramPart (((StepWhile=0 a,I,s) . k) +* (Initialized I))),(((StepWhile=0 a,I,s) . k) +* (Initialized I))) by A6, FUNCT_4:76, SCMFSA_2:127
.= DataPart (Comput (ProgramPart (((StepWhile=0 a,I,s) . k) +* (I +* (Start-At 0 ,SCM+FSA )))),(((StepWhile=0 a,I,s) . k) +* (I +* (Start-At 0 ,SCM+FSA ))),(LifeSpan (ProgramPart (((StepWhile=0 a,I,s) . k) +* (I +* (Start-At 0 ,SCM+FSA )))),(((StepWhile=0 a,I,s) . k) +* (I +* (Start-At 0 ,SCM+FSA ))))) by A7, A5, AMI_1:122 ;
hence DataPart ((StepWhile=0 a,I,s) . (k + 1)) = DataPart (IExec I,((StepWhile=0 a,I,s) . k)) by A2, A8, A4, Th23; :: thesis: verum