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

for I being really-closed InitHalting keepInt0_1 Program of SCM+FSA

for a being read-write Int-Location st not I destroys a holds

(Comput ((p +* (I ";" (SubFrom (a,(intloc 0))))),(Initialize (Initialized s)),(LifeSpan ((p +* (I ";" (SubFrom (a,(intloc 0))))),(Initialize (Initialized s)))))) . a = (s . a) - 1

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

for a being read-write Int-Location st not I destroys a holds

(Comput ((p +* (I ";" (SubFrom (a,(intloc 0))))),(Initialize (Initialized s)),(LifeSpan ((p +* (I ";" (SubFrom (a,(intloc 0))))),(Initialize (Initialized s)))))) . a = (s . a) - 1

let I be really-closed InitHalting keepInt0_1 Program of SCM+FSA; :: thesis: for a being read-write Int-Location st not I destroys a holds

(Comput ((p +* (I ";" (SubFrom (a,(intloc 0))))),(Initialize (Initialized s)),(LifeSpan ((p +* (I ";" (SubFrom (a,(intloc 0))))),(Initialize (Initialized s)))))) . a = (s . a) - 1

let a be read-write Int-Location; :: thesis: ( not I destroys a implies (Comput ((p +* (I ";" (SubFrom (a,(intloc 0))))),(Initialize (Initialized s)),(LifeSpan ((p +* (I ";" (SubFrom (a,(intloc 0))))),(Initialize (Initialized s)))))) . a = (s . a) - 1 )

assume A1: not I destroys a ; :: thesis: (Comput ((p +* (I ";" (SubFrom (a,(intloc 0))))),(Initialize (Initialized s)),(LifeSpan ((p +* (I ";" (SubFrom (a,(intloc 0))))),(Initialize (Initialized s)))))) . a = (s . a) - 1

set s0 = Initialized s;

set p0 = p;

set s1 = Initialize (Initialized s);

set p1 = p +* (I ";" (SubFrom (a,(intloc 0))));

A2: a <> IC by SCMFSA_2:56;

A3: not a in dom (Start-At (0,SCM+FSA)) by A2, TARSKI:def 1;

(IExec ((I ";" (SubFrom (a,(intloc 0)))),p,s)) . a = (Exec ((SubFrom (a,(intloc 0))),(IExec (I,p,s)))) . a by Th21

.= ((IExec (I,p,s)) . a) - ((IExec (I,p,s)) . (intloc 0)) by SCMFSA_2:65

.= ((IExec (I,p,s)) . a) - 1 by Th7

.= ((Comput ((p +* I),(Initialize (Initialized s)),0)) . a) - 1 by A1, Th43

.= ((Initialize (Initialized s)) . a) - 1

.= ((Initialized s) . a) - 1 by A3, FUNCT_4:11 ;

hence (Comput ((p +* (I ";" (SubFrom (a,(intloc 0))))),(Initialize (Initialized s)),(LifeSpan ((p +* (I ";" (SubFrom (a,(intloc 0))))),(Initialize (Initialized s)))))) . a = ((Initialized s) . a) - 1 by Th42

.= (s . a) - 1 by SCMFSA_M:37 ;

:: thesis: verum

for I being really-closed InitHalting keepInt0_1 Program of SCM+FSA

for a being read-write Int-Location st not I destroys a holds

(Comput ((p +* (I ";" (SubFrom (a,(intloc 0))))),(Initialize (Initialized s)),(LifeSpan ((p +* (I ";" (SubFrom (a,(intloc 0))))),(Initialize (Initialized s)))))) . a = (s . a) - 1

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

for a being read-write Int-Location st not I destroys a holds

(Comput ((p +* (I ";" (SubFrom (a,(intloc 0))))),(Initialize (Initialized s)),(LifeSpan ((p +* (I ";" (SubFrom (a,(intloc 0))))),(Initialize (Initialized s)))))) . a = (s . a) - 1

let I be really-closed InitHalting keepInt0_1 Program of SCM+FSA; :: thesis: for a being read-write Int-Location st not I destroys a holds

(Comput ((p +* (I ";" (SubFrom (a,(intloc 0))))),(Initialize (Initialized s)),(LifeSpan ((p +* (I ";" (SubFrom (a,(intloc 0))))),(Initialize (Initialized s)))))) . a = (s . a) - 1

let a be read-write Int-Location; :: thesis: ( not I destroys a implies (Comput ((p +* (I ";" (SubFrom (a,(intloc 0))))),(Initialize (Initialized s)),(LifeSpan ((p +* (I ";" (SubFrom (a,(intloc 0))))),(Initialize (Initialized s)))))) . a = (s . a) - 1 )

assume A1: not I destroys a ; :: thesis: (Comput ((p +* (I ";" (SubFrom (a,(intloc 0))))),(Initialize (Initialized s)),(LifeSpan ((p +* (I ";" (SubFrom (a,(intloc 0))))),(Initialize (Initialized s)))))) . a = (s . a) - 1

set s0 = Initialized s;

set p0 = p;

set s1 = Initialize (Initialized s);

set p1 = p +* (I ";" (SubFrom (a,(intloc 0))));

A2: a <> IC by SCMFSA_2:56;

A3: not a in dom (Start-At (0,SCM+FSA)) by A2, TARSKI:def 1;

(IExec ((I ";" (SubFrom (a,(intloc 0)))),p,s)) . a = (Exec ((SubFrom (a,(intloc 0))),(IExec (I,p,s)))) . a by Th21

.= ((IExec (I,p,s)) . a) - ((IExec (I,p,s)) . (intloc 0)) by SCMFSA_2:65

.= ((IExec (I,p,s)) . a) - 1 by Th7

.= ((Comput ((p +* I),(Initialize (Initialized s)),0)) . a) - 1 by A1, Th43

.= ((Initialize (Initialized s)) . a) - 1

.= ((Initialized s) . a) - 1 by A3, FUNCT_4:11 ;

hence (Comput ((p +* (I ";" (SubFrom (a,(intloc 0))))),(Initialize (Initialized s)),(LifeSpan ((p +* (I ";" (SubFrom (a,(intloc 0))))),(Initialize (Initialized s)))))) . a = ((Initialized s) . a) - 1 by Th42

.= (s . a) - 1 by SCMFSA_M:37 ;

:: thesis: verum