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