let p be Instruction-Sequence of SCM+FSA; :: thesis: for s being State of SCM+FSA

for I being InitHalting Program of SCM+FSA

for a being read-write Int-Location holds (IExec (I,p,s)) . a = (Comput ((p +* I),(Initialize (Initialized s)),(LifeSpan ((p +* I),(Initialize (Initialized s)))))) . a

let s be State of SCM+FSA; :: thesis: for I being InitHalting Program of SCM+FSA

for a being read-write Int-Location holds (IExec (I,p,s)) . a = (Comput ((p +* I),(Initialize (Initialized s)),(LifeSpan ((p +* I),(Initialize (Initialized s)))))) . a

let I be InitHalting Program of SCM+FSA; :: thesis: for a being read-write Int-Location holds (IExec (I,p,s)) . a = (Comput ((p +* I),(Initialize (Initialized s)),(LifeSpan ((p +* I),(Initialize (Initialized s)))))) . a

let a be read-write Int-Location; :: thesis: (IExec (I,p,s)) . a = (Comput ((p +* I),(Initialize (Initialized s)),(LifeSpan ((p +* I),(Initialize (Initialized s)))))) . a

I is_halting_on Initialized s,p by Th41;

hence (IExec (I,p,s)) . a = (Comput ((p +* I),(Initialize (Initialized s)),(LifeSpan ((p +* I),(Initialize (Initialized s)))))) . a by SCMFSA8C:58; :: thesis: verum

for I being InitHalting Program of SCM+FSA

for a being read-write Int-Location holds (IExec (I,p,s)) . a = (Comput ((p +* I),(Initialize (Initialized s)),(LifeSpan ((p +* I),(Initialize (Initialized s)))))) . a

let s be State of SCM+FSA; :: thesis: for I being InitHalting Program of SCM+FSA

for a being read-write Int-Location holds (IExec (I,p,s)) . a = (Comput ((p +* I),(Initialize (Initialized s)),(LifeSpan ((p +* I),(Initialize (Initialized s)))))) . a

let I be InitHalting Program of SCM+FSA; :: thesis: for a being read-write Int-Location holds (IExec (I,p,s)) . a = (Comput ((p +* I),(Initialize (Initialized s)),(LifeSpan ((p +* I),(Initialize (Initialized s)))))) . a

let a be read-write Int-Location; :: thesis: (IExec (I,p,s)) . a = (Comput ((p +* I),(Initialize (Initialized s)),(LifeSpan ((p +* I),(Initialize (Initialized s)))))) . a

I is_halting_on Initialized s,p by Th41;

hence (IExec (I,p,s)) . a = (Comput ((p +* I),(Initialize (Initialized s)),(LifeSpan ((p +* I),(Initialize (Initialized s)))))) . a by SCMFSA8C:58; :: thesis: verum