let p be the Instructions of SCM+FSA -valued ManySortedSet of NAT ; :: thesis: for s being State of SCM+FSA
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,p,s)) . k),p +* (while=0 (a,I)) & I is_closed_on Initialized ((StepWhile=0 (a,I,p,s)) . k),p +* (while=0 (a,I)) ) or I is parahalting ) & ((StepWhile=0 (a,I,p,s)) . k) . a = 0 & ((StepWhile=0 (a,I,p,s)) . k) . (intloc 0) = 1 holds
DataPart ((StepWhile=0 (a,I,p,s)) . (k + 1)) = DataPart (IExec (I,(p +* (while=0 (a,I))),((StepWhile=0 (a,I,p,s)) . k)))
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,p,s)) . k),p +* (while=0 (a,I)) & I is_closed_on Initialized ((StepWhile=0 (a,I,p,s)) . k),p +* (while=0 (a,I)) ) or I is parahalting ) & ((StepWhile=0 (a,I,p,s)) . k) . a = 0 & ((StepWhile=0 (a,I,p,s)) . k) . (intloc 0) = 1 holds
DataPart ((StepWhile=0 (a,I,p,s)) . (k + 1)) = DataPart (IExec (I,(p +* (while=0 (a,I))),((StepWhile=0 (a,I,p,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,p,s)) . k),p +* (while=0 (a,I)) & I is_closed_on Initialized ((StepWhile=0 (a,I,p,s)) . k),p +* (while=0 (a,I)) ) or I is parahalting ) & ((StepWhile=0 (a,I,p,s)) . k) . a = 0 & ((StepWhile=0 (a,I,p,s)) . k) . (intloc 0) = 1 holds
DataPart ((StepWhile=0 (a,I,p,s)) . (k + 1)) = DataPart (IExec (I,(p +* (while=0 (a,I))),((StepWhile=0 (a,I,p,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,p,s)) . k),p +* (while=0 (a,I)) & I is_closed_on Initialized ((StepWhile=0 (a,I,p,s)) . k),p +* (while=0 (a,I)) ) or I is parahalting ) & ((StepWhile=0 (a,I,p,s)) . k) . a = 0 & ((StepWhile=0 (a,I,p,s)) . k) . (intloc 0) = 1 holds
DataPart ((StepWhile=0 (a,I,p,s)) . (k + 1)) = DataPart (IExec (I,(p +* (while=0 (a,I))),((StepWhile=0 (a,I,p,s)) . k)))
let k be Element of NAT ; :: thesis: ( ( ( I is_halting_on Initialized ((StepWhile=0 (a,I,p,s)) . k),p +* (while=0 (a,I)) & I is_closed_on Initialized ((StepWhile=0 (a,I,p,s)) . k),p +* (while=0 (a,I)) ) or I is parahalting ) & ((StepWhile=0 (a,I,p,s)) . k) . a = 0 & ((StepWhile=0 (a,I,p,s)) . k) . (intloc 0) = 1 implies DataPart ((StepWhile=0 (a,I,p,s)) . (k + 1)) = DataPart (IExec (I,(p +* (while=0 (a,I))),((StepWhile=0 (a,I,p,s)) . k))) )
set Ins = NAT ;
assume that
A1: ( ( I is_halting_on Initialized ((StepWhile=0 (a,I,p,s)) . k),p +* (while=0 (a,I)) & I is_closed_on Initialized ((StepWhile=0 (a,I,p,s)) . k),p +* (while=0 (a,I)) ) or I is parahalting ) and
A2: ((StepWhile=0 (a,I,p,s)) . k) . a = 0 and
A3: ((StepWhile=0 (a,I,p,s)) . k) . (intloc 0) = 1 ; :: thesis: DataPart ((StepWhile=0 (a,I,p,s)) . (k + 1)) = DataPart (IExec (I,(p +* (while=0 (a,I))),((StepWhile=0 (a,I,p,s)) . k)))
A4: ProgramPart (Initialized I) = I by SCMFSA6A:33;
set ISWk = Initialized ((StepWhile=0 (a,I,p,s)) . k);
set SW = StepWhile=0 (a,I,p,s);
set PW = p +* (while=0 (a,I));
set SWkI = ((StepWhile=0 (a,I,p,s)) . k) +* (Initialized I);
set PWI = (p +* (while=0 (a,I))) +* I;
A5: (p +* (while=0 (a,I))) +* (while=0 (a,I)) = p +* (while=0 (a,I)) by FUNCT_4:99;
DataPart (Initialized ((StepWhile=0 (a,I,p,s)) . k)) = DataPart ((StepWhile=0 (a,I,p,s)) . k) by A3, SCMFSA8C:27;
then A6: ( I is_closed_on (StepWhile=0 (a,I,p,s)) . k,p +* (while=0 (a,I)) & I is_halting_on (StepWhile=0 (a,I,p,s)) . k,p +* (while=0 (a,I)) ) by A1, SCMFSA7B:24, SCMFSA7B:25, SCMFSA8B:8;
I is_halting_on Initialized ((StepWhile=0 (a,I,p,s)) . k),p +* (while=0 (a,I)) by A1, SCMFSA7B:25;
then A7: Initialized I is_halting_on (StepWhile=0 (a,I,p,s)) . k,p +* (while=0 (a,I)) by SCMFSA8C:22;
Initialized I = Initialize (I +* ((intloc 0) .--> 1)) by FUNCT_4:15;
then A8: Start-At (0,SCM+FSA) c= Initialized I by FUNCT_4:26;
A9: (p +* (while=0 (a,I))) +* I halts_on ((StepWhile=0 (a,I,p,s)) . k) +* (Initialize (Initialized I)) by SCMFSA7B:def 8, A4, A7;
((StepWhile=0 (a,I,p,s)) . k) +* (Initialized I) = ((StepWhile=0 (a,I,p,s)) . k) +* (Initialize (Initialized I)) by FUNCT_4:79, A8;
then A10: (p +* (while=0 (a,I))) +* I halts_on ((StepWhile=0 (a,I,p,s)) . k) +* (Initialized I) by A9;
A11: dom (((StepWhile=0 (a,I,p,s)) . k) | NAT) c= NAT by RELAT_1:87;
NAT misses Int-Locations \/ FinSeq-Locations by SCMFSA_2:13, SCMFSA_2:14, XBOOLE_1:70;
then A12: dom (((StepWhile=0 (a,I,p,s)) . k) | NAT) misses Int-Locations \/ FinSeq-Locations by A11, XBOOLE_1:63;
set IS = Initialize I;
set SWkIS = ((StepWhile=0 (a,I,p,s)) . k) +* (Initialize I);
set PWIS = (p +* (while=0 (a,I))) +* I;
A13: ((StepWhile=0 (a,I,p,s)) . k) +* (Initialized I) = ((StepWhile=0 (a,I,p,s)) . k) +* (Initialize I) by A3, SCMFSA8C:18;
set WHS = Initialize (while=0 (a,I));
A14: (StepWhile=0 (a,I,p,s)) . (k + 1) = Comput (((p +* (while=0 (a,I))) +* (while=0 (a,I))),(((StepWhile=0 (a,I,p,s)) . k) +* (Initialize (while=0 (a,I)))),((LifeSpan (((p +* (while=0 (a,I))) +* I),(((StepWhile=0 (a,I,p,s)) . k) +* (Initialize I)))) + 3)) by SCMFSA_9:def 4, A5;
A15: DataPart (IExec (I,(p +* (while=0 (a,I))),((StepWhile=0 (a,I,p,s)) . k))) = DataPart ((Result (((p +* (while=0 (a,I))) +* I),(((StepWhile=0 (a,I,p,s)) . k) +* (Initialized I)))) +* (((StepWhile=0 (a,I,p,s)) . k) | NAT)) by SCMFSA6B:def 1
.= DataPart (Result (((p +* (while=0 (a,I))) +* I),(((StepWhile=0 (a,I,p,s)) . k) +* (Initialized I)))) by A12, FUNCT_4:76, SCMFSA_2:127
.= DataPart (Comput (((p +* (while=0 (a,I))) +* I),(((StepWhile=0 (a,I,p,s)) . k) +* (Initialize I)),(LifeSpan (((p +* (while=0 (a,I))) +* I),(((StepWhile=0 (a,I,p,s)) . k) +* (Initialize I)))))) by A13, A10, EXTPRO_1:23 ;
thus DataPart ((StepWhile=0 (a,I,p,s)) . (k + 1)) = DataPart (Comput (((p +* (while=0 (a,I))) +* (while=0 (a,I))),(((StepWhile=0 (a,I,p,s)) . k) +* (Initialize (while=0 (a,I)))),((LifeSpan (((p +* (while=0 (a,I))) +* I),(((StepWhile=0 (a,I,p,s)) . k) +* (Initialize I)))) + 3))) by A14
.= DataPart (Comput (((p +* (while=0 (a,I))) +* I),(((StepWhile=0 (a,I,p,s)) . k) +* (Initialize I)),(LifeSpan (((p +* (while=0 (a,I))) +* I),(((StepWhile=0 (a,I,p,s)) . k) +* (Initialize I)))))) by A2, A6, Th23
.= DataPart (IExec (I,(p +* (while=0 (a,I))),((StepWhile=0 (a,I,p,s)) . k))) by A15 ; :: thesis: verum