let p be Instruction-Sequence of SCM+FSA; for s being State of SCM+FSA
for a being read-write Int-Location
for I being MacroInstruction of SCM+FSA
for k being Nat st ((StepWhile=0 (a,I,p,s)) . k) . a <> 0 holds
DataPart ((StepWhile=0 (a,I,p,s)) . (k + 1)) = DataPart ((StepWhile=0 (a,I,p,s)) . k)
let s be State of SCM+FSA; for a being read-write Int-Location
for I being MacroInstruction of SCM+FSA
for k being Nat st ((StepWhile=0 (a,I,p,s)) . k) . a <> 0 holds
DataPart ((StepWhile=0 (a,I,p,s)) . (k + 1)) = DataPart ((StepWhile=0 (a,I,p,s)) . k)
let a be read-write Int-Location; for I being MacroInstruction of SCM+FSA
for k being Nat st ((StepWhile=0 (a,I,p,s)) . k) . a <> 0 holds
DataPart ((StepWhile=0 (a,I,p,s)) . (k + 1)) = DataPart ((StepWhile=0 (a,I,p,s)) . k)
let I be MacroInstruction of SCM+FSA ; for k being Nat st ((StepWhile=0 (a,I,p,s)) . k) . a <> 0 holds
DataPart ((StepWhile=0 (a,I,p,s)) . (k + 1)) = DataPart ((StepWhile=0 (a,I,p,s)) . k)
let k be Nat; ( ((StepWhile=0 (a,I,p,s)) . k) . a <> 0 implies DataPart ((StepWhile=0 (a,I,p,s)) . (k + 1)) = DataPart ((StepWhile=0 (a,I,p,s)) . k) )
assume A1:
((StepWhile=0 (a,I,p,s)) . k) . a <> 0
; DataPart ((StepWhile=0 (a,I,p,s)) . (k + 1)) = DataPart ((StepWhile=0 (a,I,p,s)) . k)
set SW = StepWhile=0 (a,I,p,s);
set PW = p +* (while=0 (a,I));
A2:
while=0 (a,I) c= p +* (while=0 (a,I))
by FUNCT_4:25;
A3:
DataPart (Initialize ((StepWhile=0 (a,I,p,s)) . k)) = DataPart ((StepWhile=0 (a,I,p,s)) . k)
by MEMSTR_0:79;
then A4:
((StepWhile=0 (a,I,p,s)) . k) . a = (Initialize ((StepWhile=0 (a,I,p,s)) . k)) . a
by SCMFSA_M:2;
thus DataPart ((StepWhile=0 (a,I,p,s)) . (k + 1)) =
DataPart (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
.=
DataPart ((StepWhile=0 (a,I,p,s)) . k)
by A1, A3, A4, Th16, A2
; verum