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) = Computation (s +* ((while=0 a,I) +* (Start-At (insloc 0 )))),((LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 3)
let a be read-write Int-Location ; :: thesis: for s being State of SCM+FSA holds (StepWhile=0 a,I,s) . (0 + 1) = Computation (s +* ((while=0 a,I) +* (Start-At (insloc 0 )))),((LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 3)
let s be State of SCM+FSA ; :: thesis: (StepWhile=0 a,I,s) . (0 + 1) = Computation (s +* ((while=0 a,I) +* (Start-At (insloc 0 )))),((LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 3)
thus (StepWhile=0 a,I,s) . (0 + 1) = Computation (((StepWhile=0 a,I,s) . 0 ) +* ((while=0 a,I) +* (Start-At (insloc 0 )))),((LifeSpan (((StepWhile=0 a,I,s) . 0 ) +* (I +* (Start-At (insloc 0 ))))) + 3) by Def4
.= Computation (s +* ((while=0 a,I) +* (Start-At (insloc 0 )))),((LifeSpan (((StepWhile=0 a,I,s) . 0 ) +* (I +* (Start-At (insloc 0 ))))) + 3) by Def4
.= Computation (s +* ((while=0 a,I) +* (Start-At (insloc 0 )))),((LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 3) by Def4 ; :: thesis: verum