let s be State of SCM+FSA; for p being Instruction-Sequence of SCM+FSA
for J being good MacroInstruction of SCM+FSA
for a being read-write Int-Location holds ((StepTimes (a,J,p,s)) . 0) . (intloc 0) = 1
let p be Instruction-Sequence of SCM+FSA; for J being good MacroInstruction of SCM+FSA
for a being read-write Int-Location holds ((StepTimes (a,J,p,s)) . 0) . (intloc 0) = 1
let J be good MacroInstruction of SCM+FSA ; for a being read-write Int-Location holds ((StepTimes (a,J,p,s)) . 0) . (intloc 0) = 1
let a be read-write Int-Location; ((StepTimes (a,J,p,s)) . 0) . (intloc 0) = 1
set I = J;
set ST = StepTimes (a,J,p,s);
set Is = Initialized s;
thus ((StepTimes (a,J,p,s)) . 0) . (intloc 0) =
(Initialized s) . (intloc 0)
by SCMFSA_9:def 5
.=
1
by SCMFSA_M:9
; verum