let P be the Instructions of SCM+FSA -valued ManySortedSet of NAT ; :: thesis: for s being State of SCM+FSA
for I being parahalting keeping_0 Program of SCM+FSA
for a being read-write Int-Location st not I destroys a holds
(Comput ((P +* (I ';' (SubFrom (a,(intloc 0))))),((Initialized s) +* (Initialize (I ';' (SubFrom (a,(intloc 0)))))),(LifeSpan ((P +* (I ';' (SubFrom (a,(intloc 0))))),((Initialized s) +* (Initialize (I ';' (SubFrom (a,(intloc 0)))))))))) . a = (s . a) - 1
let s be State of SCM+FSA; :: thesis: for I being parahalting keeping_0 Program of SCM+FSA
for a being read-write Int-Location st not I destroys a holds
(Comput ((P +* (I ';' (SubFrom (a,(intloc 0))))),((Initialized s) +* (Initialize (I ';' (SubFrom (a,(intloc 0)))))),(LifeSpan ((P +* (I ';' (SubFrom (a,(intloc 0))))),((Initialized s) +* (Initialize (I ';' (SubFrom (a,(intloc 0)))))))))) . a = (s . a) - 1
let I be parahalting keeping_0 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))))),((Initialized s) +* (Initialize (I ';' (SubFrom (a,(intloc 0)))))),(LifeSpan ((P +* (I ';' (SubFrom (a,(intloc 0))))),((Initialized s) +* (Initialize (I ';' (SubFrom (a,(intloc 0)))))))))) . a = (s . a) - 1
let a be read-write Int-Location ; :: thesis: ( not I destroys a implies (Comput ((P +* (I ';' (SubFrom (a,(intloc 0))))),((Initialized s) +* (Initialize (I ';' (SubFrom (a,(intloc 0)))))),(LifeSpan ((P +* (I ';' (SubFrom (a,(intloc 0))))),((Initialized s) +* (Initialize (I ';' (SubFrom (a,(intloc 0)))))))))) . a = (s . a) - 1 )
assume A1: not I destroys a ; :: thesis: (Comput ((P +* (I ';' (SubFrom (a,(intloc 0))))),((Initialized s) +* (Initialize (I ';' (SubFrom (a,(intloc 0)))))),(LifeSpan ((P +* (I ';' (SubFrom (a,(intloc 0))))),((Initialized s) +* (Initialize (I ';' (SubFrom (a,(intloc 0)))))))))) . a = (s . a) - 1
set s0 = Initialized s;
set s1 = (Initialized s) +* (Initialize (I ';' (SubFrom (a,(intloc 0)))));
set P1 = P +* (I ';' (SubFrom (a,(intloc 0))));
A2: not a in dom (Initialize I) by SCMFSA6B:12;
(IExec ((I ';' (SubFrom (a,(intloc 0)))),P,s)) . a = (Exec ((SubFrom (a,(intloc 0))),(IExec (I,P,s)))) . a by SCMFSA6C:7
.= ((IExec (I,P,s)) . a) - ((IExec (I,P,s)) . (intloc 0)) by SCMFSA_2:91
.= ((IExec (I,P,s)) . a) - 1 by SCMFSA6B:35
.= ((Comput ((P +* I),((Initialized s) +* (Initialize I)),0)) . a) - 1 by A1, Th90
.= (((Initialized s) +* (Initialize I)) . a) - 1 by EXTPRO_1:3
.= ((Initialized s) . a) - 1 by A2, FUNCT_4:12 ;
hence (Comput ((P +* (I ';' (SubFrom (a,(intloc 0))))),((Initialized s) +* (Initialize (I ';' (SubFrom (a,(intloc 0)))))),(LifeSpan ((P +* (I ';' (SubFrom (a,(intloc 0))))),((Initialized s) +* (Initialize (I ';' (SubFrom (a,(intloc 0)))))))))) . a = ((Initialized s) . a) - 1 by Th88
.= (s . a) - 1 by SCMFSA6C:3 ;
:: thesis: verum