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