let p be Instruction-Sequence of SCM+FSA; for s being State of SCM+FSA
for a being read-write Int-Location
for k being Nat
for I being really-closed MacroInstruction of SCM+FSA st ( I is_halting_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; for a being read-write Int-Location
for k being Nat
for I being really-closed MacroInstruction of SCM+FSA st ( I is_halting_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; for k being Nat
for I being really-closed MacroInstruction of SCM+FSA st ( I is_halting_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 Nat; for I being really-closed MacroInstruction of SCM+FSA st ( I is_halting_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 really-closed MacroInstruction of SCM+FSA ; ( ( I is_halting_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)) 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
; 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 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 = Initialized ((StepWhile=0 (a,I,p,s)) . k);
set PWI = (p +* (while=0 (a,I))) +* I;
DataPart (Initialized ((StepWhile=0 (a,I,p,s)) . k)) = DataPart ((StepWhile=0 (a,I,p,s)) . k)
by A3, SCMFSA_M:19;
then A4:
I is_halting_on (StepWhile=0 (a,I,p,s)) . k,p +* (while=0 (a,I))
by A1, SCMFSA7B:19, SCMFSA8B:5;
I is_halting_on Initialized ((StepWhile=0 (a,I,p,s)) . k),p +* (while=0 (a,I))
by A1, SCMFSA7B:19;
then A5:
I is_halting_on Initialized ((StepWhile=0 (a,I,p,s)) . k),p +* (while=0 (a,I))
;
Initialized ((StepWhile=0 (a,I,p,s)) . k) = Initialize (Initialized ((StepWhile=0 (a,I,p,s)) . k))
by MEMSTR_0:44;
then A6:
(p +* (while=0 (a,I))) +* I halts_on Initialized ((StepWhile=0 (a,I,p,s)) . k)
by A5, SCMFSA7B:def 7;
A7:
(p +* (while=0 (a,I))) +* I halts_on Initialized ((StepWhile=0 (a,I,p,s)) . k)
by A6;
set SWkIS = Initialize ((StepWhile=0 (a,I,p,s)) . k);
set PWIS = (p +* (while=0 (a,I))) +* I;
A8:
Initialized ((StepWhile=0 (a,I,p,s)) . k) = Initialize ((StepWhile=0 (a,I,p,s)) . k)
by A3, SCMFSA_M:18;
A9:
(StepWhile=0 (a,I,p,s)) . (k + 1) = Comput (((p +* (while=0 (a,I))) +* (while=0 (a,I))),(Initialize ((StepWhile=0 (a,I,p,s)) . k)),((LifeSpan (((p +* (while=0 (a,I))) +* I),(Initialize ((StepWhile=0 (a,I,p,s)) . k)))) + 2))
by SCMFSA_9:def 4;
A10: DataPart (IExec (I,(p +* (while=0 (a,I))),((StepWhile=0 (a,I,p,s)) . k))) =
DataPart (Result (((p +* (while=0 (a,I))) +* I),(Initialized ((StepWhile=0 (a,I,p,s)) . k))))
by SCMFSA6B:def 1
.=
DataPart (Comput (((p +* (while=0 (a,I))) +* I),(Initialize ((StepWhile=0 (a,I,p,s)) . k)),(LifeSpan (((p +* (while=0 (a,I))) +* I),(Initialize ((StepWhile=0 (a,I,p,s)) . k))))))
by A8, A7, EXTPRO_1:23
;
thus DataPart ((StepWhile=0 (a,I,p,s)) . (k + 1)) =
DataPart (Comput (((p +* (while=0 (a,I))) +* I),(Initialize ((StepWhile=0 (a,I,p,s)) . k)),(LifeSpan (((p +* (while=0 (a,I))) +* I),(Initialize ((StepWhile=0 (a,I,p,s)) . k))))))
by A2, A4, Th17, A9
.=
DataPart (IExec (I,(p +* (while=0 (a,I))),((StepWhile=0 (a,I,p,s)) . k)))
by A10
; verum