let I be Program of SCM+FSA ; :: thesis: for a being read-write Int-Location
for s being State of SCM+FSA holds (StepWhile>0 a,I,s) . (0 + 1) = Comput (ProgramPart (s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),((LifeSpan (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA )))) + 3)
let a be read-write Int-Location ; :: thesis: for s being State of SCM+FSA holds (StepWhile>0 a,I,s) . (0 + 1) = Comput (ProgramPart (s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),((LifeSpan (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA )))) + 3)
let s be State of SCM+FSA ; :: thesis: (StepWhile>0 a,I,s) . (0 + 1) = Comput (ProgramPart (s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),((LifeSpan (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA )))) + 3)
X: (StepWhile>0 a,I,s) . 0 = s by Def5;
thus (StepWhile>0 a,I,s) . (0 + 1) = Comput (ProgramPart (((StepWhile>0 a,I,s) . 0 ) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),(((StepWhile>0 a,I,s) . 0 ) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),((LifeSpan (ProgramPart (((StepWhile>0 a,I,s) . 0 ) +* (I +* (Start-At 0 ,SCM+FSA )))),(((StepWhile>0 a,I,s) . 0 ) +* (I +* (Start-At 0 ,SCM+FSA )))) + 3) by Def5
.= Comput (ProgramPart (s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),((LifeSpan (ProgramPart (((StepWhile>0 a,I,s) . 0 ) +* (I +* (Start-At 0 ,SCM+FSA )))),(((StepWhile>0 a,I,s) . 0 ) +* (I +* (Start-At 0 ,SCM+FSA )))) + 3) by X
.= Comput (ProgramPart (s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),((LifeSpan (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA )))) + 3) by X ; :: thesis: verum