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