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 FUNCT_4:26, SCMFSA7B:def 8;
then ((StepWhile=0 (a,I,s)) . k) +* (Initialized I) = ((StepWhile=0 (a,I,s)) . k) +* (Initialize (Initialized I)) 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 (ProgramPart ((StepWhile=0 (a,I,s)) . k)) misses Int-Locations \/ FinSeq-Locations by COMPOS_1:34;
set IS = Initialize I;
set SWkIS = ((StepWhile=0 (a,I,s)) . k) +* (Initialize I);
A7: ((StepWhile=0 (a,I,s)) . k) +* (Initialized I) = ((StepWhile=0 (a,I,s)) . k) +* (Initialize I) 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) +* (Initialize I))),(((StepWhile=0 (a,I,s)) . k) +* (Initialize I)))) + 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) +* (Initialize I))),(((StepWhile=0 (a,I,s)) . k) +* (Initialize I)),(LifeSpan ((ProgramPart (((StepWhile=0 (a,I,s)) . k) +* (Initialize I))),(((StepWhile=0 (a,I,s)) . k) +* (Initialize I)))))) by A7, A5, EXTPRO_1:23 ;
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