set A = NAT ;
let s be State of SCM+FSA ; :: thesis: for I being parahalting good Program of SCM+FSA
for a being read-write Int-Location st I does_not_destroy a & s . (intloc 0 ) = 1 & s . a > 0 holds
ex s2 being State of SCM+FSA ex k being Element of NAT st
( s2 = s +* ((loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) +* (Start-At (insloc 0 ))) & k = (LifeSpan (s +* ((if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At (insloc 0 ))))) + 1 & (Computation s2,k) . a = (s . a) - 1 & (Computation s2,k) . (intloc 0 ) = 1 & ( for b being read-write Int-Location st b <> a holds
(Computation s2,k) . b = (IExec I,s) . b ) & ( for f being FinSeq-Location holds (Computation s2,k) . f = (IExec I,s) . f ) & IC (Computation s2,k) = insloc 0 & ( for n being Element of NAT st n <= k holds
IC (Computation s2,n) in dom (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) ) )
let I be parahalting good Program of SCM+FSA ; :: thesis: for a being read-write Int-Location st I does_not_destroy a & s . (intloc 0 ) = 1 & s . a > 0 holds
ex s2 being State of SCM+FSA ex k being Element of NAT st
( s2 = s +* ((loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) +* (Start-At (insloc 0 ))) & k = (LifeSpan (s +* ((if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At (insloc 0 ))))) + 1 & (Computation s2,k) . a = (s . a) - 1 & (Computation s2,k) . (intloc 0 ) = 1 & ( for b being read-write Int-Location st b <> a holds
(Computation s2,k) . b = (IExec I,s) . b ) & ( for f being FinSeq-Location holds (Computation s2,k) . f = (IExec I,s) . f ) & IC (Computation s2,k) = insloc 0 & ( for n being Element of NAT st n <= k holds
IC (Computation s2,n) in dom (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) ) )
let a be read-write Int-Location ; :: thesis: ( I does_not_destroy a & s . (intloc 0 ) = 1 & s . a > 0 implies ex s2 being State of SCM+FSA ex k being Element of NAT st
( s2 = s +* ((loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) +* (Start-At (insloc 0 ))) & k = (LifeSpan (s +* ((if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At (insloc 0 ))))) + 1 & (Computation s2,k) . a = (s . a) - 1 & (Computation s2,k) . (intloc 0 ) = 1 & ( for b being read-write Int-Location st b <> a holds
(Computation s2,k) . b = (IExec I,s) . b ) & ( for f being FinSeq-Location holds (Computation s2,k) . f = (IExec I,s) . f ) & IC (Computation s2,k) = insloc 0 & ( for n being Element of NAT st n <= k holds
IC (Computation s2,n) in dom (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) ) ) )
assume A1: I does_not_destroy a ; :: thesis: ( not s . (intloc 0 ) = 1 or not s . a > 0 or ex s2 being State of SCM+FSA ex k being Element of NAT st
( s2 = s +* ((loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) +* (Start-At (insloc 0 ))) & k = (LifeSpan (s +* ((if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At (insloc 0 ))))) + 1 & (Computation s2,k) . a = (s . a) - 1 & (Computation s2,k) . (intloc 0 ) = 1 & ( for b being read-write Int-Location st b <> a holds
(Computation s2,k) . b = (IExec I,s) . b ) & ( for f being FinSeq-Location holds (Computation s2,k) . f = (IExec I,s) . f ) & IC (Computation s2,k) = insloc 0 & ( for n being Element of NAT st n <= k holds
IC (Computation s2,n) in dom (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) ) ) )
assume A2: s . (intloc 0 ) = 1 ; :: thesis: ( not s . a > 0 or ex s2 being State of SCM+FSA ex k being Element of NAT st
( s2 = s +* ((loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) +* (Start-At (insloc 0 ))) & k = (LifeSpan (s +* ((if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At (insloc 0 ))))) + 1 & (Computation s2,k) . a = (s . a) - 1 & (Computation s2,k) . (intloc 0 ) = 1 & ( for b being read-write Int-Location st b <> a holds
(Computation s2,k) . b = (IExec I,s) . b ) & ( for f being FinSeq-Location holds (Computation s2,k) . f = (IExec I,s) . f ) & IC (Computation s2,k) = insloc 0 & ( for n being Element of NAT st n <= k holds
IC (Computation s2,n) in dom (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) ) ) )
assume A3: s . a > 0 ; :: thesis: ex s2 being State of SCM+FSA ex k being Element of NAT st
( s2 = s +* ((loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) +* (Start-At (insloc 0 ))) & k = (LifeSpan (s +* ((if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At (insloc 0 ))))) + 1 & (Computation s2,k) . a = (s . a) - 1 & (Computation s2,k) . (intloc 0 ) = 1 & ( for b being read-write Int-Location st b <> a holds
(Computation s2,k) . b = (IExec I,s) . b ) & ( for f being FinSeq-Location holds (Computation s2,k) . f = (IExec I,s) . f ) & IC (Computation s2,k) = insloc 0 & ( for n being Element of NAT st n <= k holds
IC (Computation s2,n) in dom (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) ) )
set P = if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )));
reconsider I1 = I ';' (SubFrom a,(intloc 0 )) as parahalting Program of SCM+FSA ;
set s1 = s +* ((if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At (insloc 0 )));
take s2 = s +* ((loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) +* (Start-At (insloc 0 ))); :: thesis: ex k being Element of NAT st
( s2 = s +* ((loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) +* (Start-At (insloc 0 ))) & k = (LifeSpan (s +* ((if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At (insloc 0 ))))) + 1 & (Computation s2,k) . a = (s . a) - 1 & (Computation s2,k) . (intloc 0 ) = 1 & ( for b being read-write Int-Location st b <> a holds
(Computation s2,k) . b = (IExec I,s) . b ) & ( for f being FinSeq-Location holds (Computation s2,k) . f = (IExec I,s) . f ) & IC (Computation s2,k) = insloc 0 & ( for n being Element of NAT st n <= k holds
IC (Computation s2,n) in dom (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) ) )
take k = (LifeSpan (s +* ((if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At (insloc 0 ))))) + 1; :: thesis: ( s2 = s +* ((loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) +* (Start-At (insloc 0 ))) & k = (LifeSpan (s +* ((if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At (insloc 0 ))))) + 1 & (Computation s2,k) . a = (s . a) - 1 & (Computation s2,k) . (intloc 0 ) = 1 & ( for b being read-write Int-Location st b <> a holds
(Computation s2,k) . b = (IExec I,s) . b ) & ( for f being FinSeq-Location holds (Computation s2,k) . f = (IExec I,s) . f ) & IC (Computation s2,k) = insloc 0 & ( for n being Element of NAT st n <= k holds
IC (Computation s2,n) in dom (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) ) )
thus ( s2 = s +* ((loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) +* (Start-At (insloc 0 ))) & k = (LifeSpan (s +* ((if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At (insloc 0 ))))) + 1 ) ; :: thesis: ( (Computation s2,k) . a = (s . a) - 1 & (Computation s2,k) . (intloc 0 ) = 1 & ( for b being read-write Int-Location st b <> a holds
(Computation s2,k) . b = (IExec I,s) . b ) & ( for f being FinSeq-Location holds (Computation s2,k) . f = (IExec I,s) . f ) & IC (Computation s2,k) = insloc 0 & ( for n being Element of NAT st n <= k holds
IC (Computation s2,n) in dom (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) ) )
( I1 is_closed_on s & I1 is_halting_on s ) by SCMFSA7B:24, SCMFSA7B:25;
then A4: ( if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))) is_closed_on s & if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))) is_halting_on s ) by A3, SCMFSA8B:18;
A5: Computation s2,((LifeSpan (s +* ((if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At (insloc 0 ))))) + 1) = Following (Computation s2,(LifeSpan (s +* ((if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At (insloc 0 )))))) by AMI_1:14
.= Exec (CurInstr (Computation s2,(LifeSpan (s +* ((if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At (insloc 0 ))))))),(Computation s2,(LifeSpan (s +* ((if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At (insloc 0 )))))) ;
then A6: Computation s2,((LifeSpan (s +* ((if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At (insloc 0 ))))) + 1) = Exec (goto (insloc 0 )),(Computation s2,(LifeSpan (s +* ((if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At (insloc 0 )))))) by A4, Lm3;
A7: IC (Computation s2,((LifeSpan (s +* ((if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At (insloc 0 ))))) + 1)) = (Exec (goto (insloc 0 )),(Computation s2,(LifeSpan (s +* ((if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At (insloc 0 ))))))) . (IC SCM+FSA ) by A4, A5, Lm3
.= insloc 0 by SCMFSA_2:95 ;

A8: now

intloc 0 in dom s by SCMFSA_2:66;
then A9: s +* ((intloc 0 ) .--> 1) = s by A2, FUNCT_7:111;
A10: dom (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) misses dom (Start-At (insloc 0 )) by SF_MASTR:64;
Initialize s = (s +* ((intloc 0 ) .--> 1)) +* (Start-At (insloc 0 )) by SCMFSA6C:def 3;
hence (Initialize s) +* ((if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At (insloc 0 ))) = (s +* (Start-At (insloc 0 ))) +* ((Start-At (insloc 0 )) +* (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) by A9, A10, FUNCT_4:36
.= ((s +* (Start-At (insloc 0 ))) +* (Start-At (insloc 0 ))) +* (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) by FUNCT_4:15
.= (s +* ((Start-At (insloc 0 )) +* (Start-At (insloc 0 )))) +* (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) by FUNCT_4:15
.= s +* ((Start-At (insloc 0 )) +* (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) by FUNCT_4:15
.= s +* ((if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At (insloc 0 ))) by A10, FUNCT_4:36 ;
:: thesis: verum

end;

set Is = (Initialize s) +* ((if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At (insloc 0 )));

A11: now

let b be Int-Location ; :: thesis: (Computation s2,((LifeSpan (s +* ((if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At (insloc 0 ))))) + 1)) . b = (Computation ((Initialize s) +* ((if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At (insloc 0 )))),(LifeSpan ((Initialize s) +* ((if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At (insloc 0 )))))) . b
( Computation (s +* ((if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At (insloc 0 )))),(LifeSpan (s +* ((if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At (insloc 0 ))))), Computation s2,(LifeSpan (s +* ((if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At (insloc 0 ))))) equal_outside NAT & (Computation s2,((LifeSpan (s +* ((if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At (insloc 0 ))))) + 1)) . b = (Computation s2,(LifeSpan (s +* ((if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At (insloc 0 )))))) . b ) by A4, A6, Th109, SCMFSA_2:95;
hence (Computation s2,((LifeSpan (s +* ((if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At (insloc 0 ))))) + 1)) . b = (Computation ((Initialize s) +* ((if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At (insloc 0 )))),(LifeSpan ((Initialize s) +* ((if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At (insloc 0 )))))) . b by A8, SCMFSA6A:30; :: thesis: verum

end;

A12: I1 is_halting_on Initialize s by SCMFSA7B:25;
( (Initialize s) . a > 0 & I1 is_closed_on Initialize s & I1 is_halting_on Initialize s ) by A3, SCMFSA6C:3, SCMFSA7B:24, SCMFSA7B:25;
then A13: ( if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))) is_halting_on Initialize s & if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))) is_closed_on Initialize s ) by SCMFSA8B:18;

A14: now

thus (Computation s2,((LifeSpan (s +* ((if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At (insloc 0 ))))) + 1)) . a = (Computation ((Initialize s) +* ((if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At (insloc 0 )))),(LifeSpan ((Initialize s) +* ((if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At (insloc 0 )))))) . a by A11
.= (IExec (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))),s) . a by A13, Th87 ; :: thesis: (Computation s2,((LifeSpan (s +* ((if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At (insloc 0 ))))) + 1)) . (intloc 0 ) = 1
A15: if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))) is good by Th115;
thus (Computation s2,((LifeSpan (s +* ((if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At (insloc 0 ))))) + 1)) . (intloc 0 ) = (Computation ((Initialize s) +* ((if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At (insloc 0 )))),(LifeSpan ((Initialize s) +* ((if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At (insloc 0 )))))) . (intloc 0 ) by A11
.= 1 by A13, A15, Th96 ; :: thesis: verum

end;

( s . a <> 0 & I1 is_closed_on Initialize s ) by A3, SCMFSA7B:24;
then A16: IExec (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))),s = (IExec I1,s) +* (Start-At (insloc (((card (Goto (insloc 2))) + (card I1)) + 3))) by A12, SCMFSA8B:19;
then (IExec (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))),s) . a = (IExec I1,s) . a by SCMFSA_3:11;
hence (Computation s2,k) . a = (Computation ((Initialize s) +* (I1 +* (Start-At (insloc 0 )))),(LifeSpan ((Initialize s) +* (I1 +* (Start-At (insloc 0 )))))) . a by A12, A14, Th87
.= (s . a) - 1 by A1, Th98 ;
:: thesis: ( (Computation s2,k) . (intloc 0 ) = 1 & ( for b being read-write Int-Location st b <> a holds
(Computation s2,k) . b = (IExec I,s) . b ) & ( for f being FinSeq-Location holds (Computation s2,k) . f = (IExec I,s) . f ) & IC (Computation s2,k) = insloc 0 & ( for n being Element of NAT st n <= k holds
IC (Computation s2,n) in dom (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) ) )
thus (Computation s2,k) . (intloc 0 ) = 1 by A14; :: thesis: ( ( for b being read-write Int-Location st b <> a holds
(Computation s2,k) . b = (IExec I,s) . b ) & ( for f being FinSeq-Location holds (Computation s2,k) . f = (IExec I,s) . f ) & IC (Computation s2,k) = insloc 0 & ( for n being Element of NAT st n <= k holds
IC (Computation s2,n) in dom (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) ) )

hereby :: thesis: ( ( for f being FinSeq-Location holds (Computation s2,k) . f = (IExec I,s) . f ) & IC (Computation s2,k) = insloc 0 & ( for n being Element of NAT st n <= k holds
IC (Computation s2,n) in dom (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) ) )

let b be read-write Int-Location ; :: thesis: ( b <> a implies (Computation s2,k) . b = (IExec I,s) . b )
assume A17: b <> a ; :: thesis: (Computation s2,k) . b = (IExec I,s) . b
thus (Computation s2,k) . b = (Computation ((Initialize s) +* ((if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At (insloc 0 )))),(LifeSpan ((Initialize s) +* ((if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At (insloc 0 )))))) . b by A11
.= (IExec (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))),s) . b by A13, Th87
.= (IExec I1,s) . b by A16, SCMFSA_3:11
.= (Exec (SubFrom a,(intloc 0 )),(IExec I,s)) . b by SCMFSA6C:7
.= (IExec I,s) . b by A17, SCMFSA_2:91 ; :: thesis: verum

end;

hereby :: thesis: ( IC (Computation s2,k) = insloc 0 & ( for n being Element of NAT st n <= k holds
IC (Computation s2,n) in dom (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) ) )

let f be FinSeq-Location ; :: thesis: (Computation s2,k) . f = (IExec I,s) . f
( Computation (s +* ((if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At (insloc 0 )))),(LifeSpan (s +* ((if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At (insloc 0 ))))), Computation s2,(LifeSpan (s +* ((if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At (insloc 0 ))))) equal_outside NAT & (Computation s2,((LifeSpan (s +* ((if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At (insloc 0 ))))) + 1)) . f = (Computation s2,(LifeSpan (s +* ((if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At (insloc 0 )))))) . f ) by A4, A6, Th109, SCMFSA_2:95;
hence (Computation s2,k) . f = (Computation ((Initialize s) +* ((if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At (insloc 0 )))),(LifeSpan ((Initialize s) +* ((if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At (insloc 0 )))))) . f by A8, SCMFSA6A:31
.= (IExec (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))),s) . f by A13, Th87
.= (IExec I1,s) . f by A16, SCMFSA_3:12
.= (Exec (SubFrom a,(intloc 0 )),(IExec I,s)) . f by SCMFSA6C:8
.= (IExec I,s) . f by SCMFSA_2:91 ;
:: thesis: verum

end;

thus IC (Computation s2,k) = insloc 0 by A7; :: thesis: for n being Element of NAT st n <= k holds
IC (Computation s2,n) in dom (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))))

hereby :: thesis: verum

let n be Element of NAT ; :: thesis: ( n <= k implies IC (Computation s2,b₁) in dom (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) )
assume A18: n <= k ; :: thesis: IC (Computation s2,b₁) in dom (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))))

per cases ( n <= LifeSpan (s +* ((if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At (insloc 0 )))) or n = (LifeSpan (s +* ((if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At (insloc 0 ))))) + 1 ) by A18, NAT_1:8;

suppose A19: n <= LifeSpan (s +* ((if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At (insloc 0 )))) ; :: thesis: IC (Computation s2,b₁) in dom (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))))

( I1 is_closed_on s & I1 is_halting_on s ) by SCMFSA7B:24, SCMFSA7B:25;
then A20: ( if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))) is_closed_on s & if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))) is_halting_on s ) by A3, SCMFSA8B:18;
then Computation (s +* ((if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At (insloc 0 )))),n, Computation s2,n equal_outside NAT by A19, Th109;
then A21: IC (Computation s2,n) = IC (Computation (s +* ((if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At (insloc 0 )))),n) by SCMFSA8A:6;
IC (Computation (s +* ((if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At (insloc 0 )))),n) in dom (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) by A20, SCMFSA7B:def 7;
hence IC (Computation s2,n) in dom (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) by A21, FUNCT_4:105; :: thesis: verum

end;

suppose A22: n = (LifeSpan (s +* ((if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At (insloc 0 ))))) + 1 ; :: thesis: IC (Computation s2,b₁) in dom (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))))

A23: card (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) = card (dom (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))))) by CARD_1:104
.= card (dom (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) by FUNCT_4:105
.= card (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) by CARD_1:104 ;
card (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) = ((card (Goto (insloc 2))) + (card I1)) + 4 by SCMFSA8B:14
.= ((card I1) + 1) + 4 by SCMFSA8A:29
.= ((card I1) + 3) + 2 ;
hence IC (Computation s2,n) in dom (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) by A7, A22, A23, SCMFSA6A:15; :: thesis: verum

end;

end;

end;