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) +* ((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 (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 5;
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, Th36; :: thesis: verum