let P be Instruction-Sequence of SCM+FSA; :: thesis: for s being State of SCM+FSA
for I being good parahalting Program of SCM+FSA
for a being read-write Int-Location st not I destroys a & s . (intloc 0) = 1 & s . a > 0 holds
ex s2 being State of SCM+FSA ex P2 being Instruction-Sequence of SCM+FSA ex k being Element of NAT st
( s2 = s +* (Start-At (0,SCM+FSA)) & P2 = P +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) & k = (LifeSpan ((P +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(s +* (Start-At (0,SCM+FSA))))) + 1 & (Comput (P2,s2,k)) . a = (s . a) - 1 & (Comput (P2,s2,k)) . (intloc 0) = 1 & ( for b being read-write Int-Location st b <> a holds
(Comput (P2,s2,k)) . b = (IExec (I,P,s)) . b ) & ( for f being FinSeq-Location holds (Comput (P2,s2,k)) . f = (IExec (I,P,s)) . f ) & IC (Comput (P2,s2,k)) = 0 & ( for n being Element of NAT st n <= k holds
IC (Comput (P2,s2,n)) in dom (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ) )
let s be State of SCM+FSA; :: thesis: for I being good parahalting Program of SCM+FSA
for a being read-write Int-Location st not I destroys a & s . (intloc 0) = 1 & s . a > 0 holds
ex s2 being State of SCM+FSA ex P2 being Instruction-Sequence of SCM+FSA ex k being Element of NAT st
( s2 = s +* (Start-At (0,SCM+FSA)) & P2 = P +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) & k = (LifeSpan ((P +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(s +* (Start-At (0,SCM+FSA))))) + 1 & (Comput (P2,s2,k)) . a = (s . a) - 1 & (Comput (P2,s2,k)) . (intloc 0) = 1 & ( for b being read-write Int-Location st b <> a holds
(Comput (P2,s2,k)) . b = (IExec (I,P,s)) . b ) & ( for f being FinSeq-Location holds (Comput (P2,s2,k)) . f = (IExec (I,P,s)) . f ) & IC (Comput (P2,s2,k)) = 0 & ( for n being Element of NAT st n <= k holds
IC (Comput (P2,s2,n)) in dom (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ) )
set A = NAT ;
let I be good parahalting Program of SCM+FSA; :: thesis: for a being read-write Int-Location st not I destroys a & s . (intloc 0) = 1 & s . a > 0 holds
ex s2 being State of SCM+FSA ex P2 being Instruction-Sequence of SCM+FSA ex k being Element of NAT st
( s2 = s +* (Start-At (0,SCM+FSA)) & P2 = P +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) & k = (LifeSpan ((P +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(s +* (Start-At (0,SCM+FSA))))) + 1 & (Comput (P2,s2,k)) . a = (s . a) - 1 & (Comput (P2,s2,k)) . (intloc 0) = 1 & ( for b being read-write Int-Location st b <> a holds
(Comput (P2,s2,k)) . b = (IExec (I,P,s)) . b ) & ( for f being FinSeq-Location holds (Comput (P2,s2,k)) . f = (IExec (I,P,s)) . f ) & IC (Comput (P2,s2,k)) = 0 & ( for n being Element of NAT st n <= k holds
IC (Comput (P2,s2,n)) in dom (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ) )
let a be read-write Int-Location ; :: thesis: ( not I destroys a & s . (intloc 0) = 1 & s . a > 0 implies ex s2 being State of SCM+FSA ex P2 being Instruction-Sequence of SCM+FSA ex k being Element of NAT st
( s2 = s +* (Start-At (0,SCM+FSA)) & P2 = P +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) & k = (LifeSpan ((P +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(s +* (Start-At (0,SCM+FSA))))) + 1 & (Comput (P2,s2,k)) . a = (s . a) - 1 & (Comput (P2,s2,k)) . (intloc 0) = 1 & ( for b being read-write Int-Location st b <> a holds
(Comput (P2,s2,k)) . b = (IExec (I,P,s)) . b ) & ( for f being FinSeq-Location holds (Comput (P2,s2,k)) . f = (IExec (I,P,s)) . f ) & IC (Comput (P2,s2,k)) = 0 & ( for n being Element of NAT st n <= k holds
IC (Comput (P2,s2,n)) in dom (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ) ) )
assume A1: not I destroys a ; :: thesis: ( not s . (intloc 0) = 1 or not s . a > 0 or ex s2 being State of SCM+FSA ex P2 being Instruction-Sequence of SCM+FSA ex k being Element of NAT st
( s2 = s +* (Start-At (0,SCM+FSA)) & P2 = P +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) & k = (LifeSpan ((P +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(s +* (Start-At (0,SCM+FSA))))) + 1 & (Comput (P2,s2,k)) . a = (s . a) - 1 & (Comput (P2,s2,k)) . (intloc 0) = 1 & ( for b being read-write Int-Location st b <> a holds
(Comput (P2,s2,k)) . b = (IExec (I,P,s)) . b ) & ( for f being FinSeq-Location holds (Comput (P2,s2,k)) . f = (IExec (I,P,s)) . f ) & IC (Comput (P2,s2,k)) = 0 & ( for n being Element of NAT st n <= k holds
IC (Comput (P2,s2,n)) in dom (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ) ) )
reconsider I1 = I ';' (SubFrom (a,(intloc 0))) as parahalting Program of SCM+FSA ;
set I2 = if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))));
set s1 = Initialize s;
set P1 = P +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))));
A3: I1 is_halting_on s,P by SCMFSA7B:19;
set Is = Initialize (Initialized s);
set IP = P +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))));
A4: intloc 0 in dom s by SCMFSA_2:42;
assume s . (intloc 0) = 1 ; :: thesis: ( not s . a > 0 or ex s2 being State of SCM+FSA ex P2 being Instruction-Sequence of SCM+FSA ex k being Element of NAT st
( s2 = s +* (Start-At (0,SCM+FSA)) & P2 = P +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) & k = (LifeSpan ((P +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(s +* (Start-At (0,SCM+FSA))))) + 1 & (Comput (P2,s2,k)) . a = (s . a) - 1 & (Comput (P2,s2,k)) . (intloc 0) = 1 & ( for b being read-write Int-Location st b <> a holds
(Comput (P2,s2,k)) . b = (IExec (I,P,s)) . b ) & ( for f being FinSeq-Location holds (Comput (P2,s2,k)) . f = (IExec (I,P,s)) . f ) & IC (Comput (P2,s2,k)) = 0 & ( for n being Element of NAT st n <= k holds
IC (Comput (P2,s2,n)) in dom (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ) ) )
then A5: s +* ((intloc 0) .--> 1) = s by A4, FUNCT_7:109;
A6: I1 is_closed_on Initialized s,P by SCMFSA7B:18;
A7: I1 is_halting_on Initialized s,P by SCMFSA7B:19;
assume A8: s . a > 0 ; :: thesis: ex s2 being State of SCM+FSA ex P2 being Instruction-Sequence of SCM+FSA ex k being Element of NAT st
( s2 = s +* (Start-At (0,SCM+FSA)) & P2 = P +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) & k = (LifeSpan ((P +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(s +* (Start-At (0,SCM+FSA))))) + 1 & (Comput (P2,s2,k)) . a = (s . a) - 1 & (Comput (P2,s2,k)) . (intloc 0) = 1 & ( for b being read-write Int-Location st b <> a holds
(Comput (P2,s2,k)) . b = (IExec (I,P,s)) . b ) & ( for f being FinSeq-Location holds (Comput (P2,s2,k)) . f = (IExec (I,P,s)) . f ) & IC (Comput (P2,s2,k)) = 0 & ( for n being Element of NAT st n <= k holds
IC (Comput (P2,s2,n)) in dom (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ) )
then A9: (Initialized s) . a > 0 by SCMFSA6C:3;
then A10: if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))) is_halting_on Initialized s,P by A6, A7, SCMFSA8B:15;
A11: if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))) is_closed_on Initialized s,P by A9, A6, A7, SCMFSA8B:15;
take s2 = Initialize s; :: thesis: ex P2 being Instruction-Sequence of SCM+FSA ex k being Element of NAT st
( s2 = s +* (Start-At (0,SCM+FSA)) & P2 = P +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) & k = (LifeSpan ((P +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(s +* (Start-At (0,SCM+FSA))))) + 1 & (Comput (P2,s2,k)) . a = (s . a) - 1 & (Comput (P2,s2,k)) . (intloc 0) = 1 & ( for b being read-write Int-Location st b <> a holds
(Comput (P2,s2,k)) . b = (IExec (I,P,s)) . b ) & ( for f being FinSeq-Location holds (Comput (P2,s2,k)) . f = (IExec (I,P,s)) . f ) & IC (Comput (P2,s2,k)) = 0 & ( for n being Element of NAT st n <= k holds
IC (Comput (P2,s2,n)) in dom (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ) )
take P2 = P +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))); :: thesis: ex k being Element of NAT st
( s2 = s +* (Start-At (0,SCM+FSA)) & P2 = P +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) & k = (LifeSpan ((P +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(s +* (Start-At (0,SCM+FSA))))) + 1 & (Comput (P2,s2,k)) . a = (s . a) - 1 & (Comput (P2,s2,k)) . (intloc 0) = 1 & ( for b being read-write Int-Location st b <> a holds
(Comput (P2,s2,k)) . b = (IExec (I,P,s)) . b ) & ( for f being FinSeq-Location holds (Comput (P2,s2,k)) . f = (IExec (I,P,s)) . f ) & IC (Comput (P2,s2,k)) = 0 & ( for n being Element of NAT st n <= k holds
IC (Comput (P2,s2,n)) in dom (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ) )
reconsider k = (LifeSpan ((P +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialize s))) + 1 as Element of NAT ;
take k ; :: thesis: ( s2 = s +* (Start-At (0,SCM+FSA)) & P2 = P +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) & k = (LifeSpan ((P +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(s +* (Start-At (0,SCM+FSA))))) + 1 & (Comput (P2,s2,k)) . a = (s . a) - 1 & (Comput (P2,s2,k)) . (intloc 0) = 1 & ( for b being read-write Int-Location st b <> a holds
(Comput (P2,s2,k)) . b = (IExec (I,P,s)) . b ) & ( for f being FinSeq-Location holds (Comput (P2,s2,k)) . f = (IExec (I,P,s)) . f ) & IC (Comput (P2,s2,k)) = 0 & ( for n being Element of NAT st n <= k holds
IC (Comput (P2,s2,n)) in dom (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ) )
thus s2 = s +* (Start-At (0,SCM+FSA)) ; :: thesis: ( P2 = P +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) & k = (LifeSpan ((P +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(s +* (Start-At (0,SCM+FSA))))) + 1 & (Comput (P2,s2,k)) . a = (s . a) - 1 & (Comput (P2,s2,k)) . (intloc 0) = 1 & ( for b being read-write Int-Location st b <> a holds
(Comput (P2,s2,k)) . b = (IExec (I,P,s)) . b ) & ( for f being FinSeq-Location holds (Comput (P2,s2,k)) . f = (IExec (I,P,s)) . f ) & IC (Comput (P2,s2,k)) = 0 & ( for n being Element of NAT st n <= k holds
IC (Comput (P2,s2,n)) in dom (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ) )
thus P2 = P +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ; :: thesis: ( k = (LifeSpan ((P +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(s +* (Start-At (0,SCM+FSA))))) + 1 & (Comput (P2,s2,k)) . a = (s . a) - 1 & (Comput (P2,s2,k)) . (intloc 0) = 1 & ( for b being read-write Int-Location st b <> a holds
(Comput (P2,s2,k)) . b = (IExec (I,P,s)) . b ) & ( for f being FinSeq-Location holds (Comput (P2,s2,k)) . f = (IExec (I,P,s)) . f ) & IC (Comput (P2,s2,k)) = 0 & ( for n being Element of NAT st n <= k holds
IC (Comput (P2,s2,n)) in dom (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ) )
thus k = (LifeSpan ((P +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(s +* (Start-At (0,SCM+FSA))))) + 1 ; :: thesis: ( (Comput (P2,s2,k)) . a = (s . a) - 1 & (Comput (P2,s2,k)) . (intloc 0) = 1 & ( for b being read-write Int-Location st b <> a holds
(Comput (P2,s2,k)) . b = (IExec (I,P,s)) . b ) & ( for f being FinSeq-Location holds (Comput (P2,s2,k)) . f = (IExec (I,P,s)) . f ) & IC (Comput (P2,s2,k)) = 0 & ( for n being Element of NAT st n <= k holds
IC (Comput (P2,s2,n)) in dom (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ) )
A13: Initialize (Initialized s) = ((s +* ((intloc 0) .--> 1)) +* (Start-At (0,SCM+FSA))) +* (Start-At (0,SCM+FSA)) by FUNCT_4:14
.= s +* (Start-At (0,SCM+FSA)) by A5, FUNCT_4:93 ;
A14: I1 is_halting_on Initialized s,P by SCMFSA7B:19;
B14: I1 is_closed_on Initialized s,P by SCMFSA7B:18;
A15: IExec ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))),P,s) = (IExec (I1,P,s)) +* (Start-At ((((card (Goto 2)) + (card I1)) + 3),SCM+FSA)) by A8, A14, B14, SCMFSA8B:16;
then A16: (IExec ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))),P,s)) . a = (IExec (I1,P,s)) . a by SCMFSA_3:3;
A17: I1 is_closed_on s,P by SCMFSA7B:18;
then A18: if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))) is_closed_on s,P by A8, A3, SCMFSA8B:15;
A19: if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))) is_halting_on s,P by A8, A17, A3, SCMFSA8B:15;
A20: Comput (P2,s2,((LifeSpan ((P +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialize s))) + 1)) = Following (P2,(Comput (P2,s2,(LifeSpan ((P +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialize s)))))) by EXTPRO_1:3;
then A21: Comput (P2,s2,((LifeSpan ((P +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialize s))) + 1)) = Exec ((goto 0),(Comput (P2,s2,(LifeSpan ((P +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialize s)))))) by A18, A19, Lm2;
XX: Comput ((P +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialize s),(LifeSpan ((P +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialize (Initialized s))))) = Comput ((P +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))),(Initialize s),(LifeSpan ((P +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialize (Initialized s))))) by A18, A19, A13, Th109;
A22: for b being Int-Location holds (Comput (P2,s2,((LifeSpan ((P +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialize s))) + 1))) . b = (Comput ((P +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialize (Initialized s)),(LifeSpan ((P +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialize (Initialized s)))))) . b by A13, XX, A21, SCMFSA_2:69;
then (Comput (P2,s2,((LifeSpan ((P +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialize s))) + 1))) . a = (Comput ((P +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialize (Initialized s)),(LifeSpan ((P +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialize (Initialized s)))))) . a
.= (IExec ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))),P,s)) . a by A10, Th87 ;
hence (Comput (P2,s2,k)) . a = (Comput ((P +* I1),(Initialize (Initialized s)),(LifeSpan ((P +* I1),(Initialize (Initialized s)))))) . a by A14, A16, Th87
.= (s . a) - 1 by A1, Th98 ;
:: thesis: ( (Comput (P2,s2,k)) . (intloc 0) = 1 & ( for b being read-write Int-Location st b <> a holds
(Comput (P2,s2,k)) . b = (IExec (I,P,s)) . b ) & ( for f being FinSeq-Location holds (Comput (P2,s2,k)) . f = (IExec (I,P,s)) . f ) & IC (Comput (P2,s2,k)) = 0 & ( for n being Element of NAT st n <= k holds
IC (Comput (P2,s2,n)) in dom (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ) )
A23: if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))) is good by Th115;
(Comput (P2,s2,((LifeSpan ((P +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialize s))) + 1))) . (intloc 0) = (Comput ((P +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialize (Initialized s)),(LifeSpan ((P +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialize (Initialized s)))))) . (intloc 0) by A22
.= 1 by A10, A11, A23, Th96 ;
hence (Comput (P2,s2,k)) . (intloc 0) = 1 ; :: thesis: ( ( for b being read-write Int-Location st b <> a holds
(Comput (P2,s2,k)) . b = (IExec (I,P,s)) . b ) & ( for f being FinSeq-Location holds (Comput (P2,s2,k)) . f = (IExec (I,P,s)) . f ) & IC (Comput (P2,s2,k)) = 0 & ( for n being Element of NAT st n <= k holds
IC (Comput (P2,s2,n)) in dom (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ) )

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

let b be read-write Int-Location ; :: thesis: ( b <> a implies (Comput (P2,s2,k)) . b = (IExec (I,P,s)) . b )
assume A24: b <> a ; :: thesis: (Comput (P2,s2,k)) . b = (IExec (I,P,s)) . b
thus (Comput (P2,s2,k)) . b = (Comput ((P +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialize (Initialized s)),(LifeSpan ((P +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialize (Initialized s)))))) . b by A22
.= (IExec ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))),P,s)) . b by A10, Th87
.= (IExec (I1,P,s)) . b by A15, SCMFSA_3:3
.= (Exec ((SubFrom (a,(intloc 0))),(IExec (I,P,s)))) . b by SCMFSA6C:6
.= (IExec (I,P,s)) . b by A24, SCMFSA_2:65 ; :: thesis: verum

end;

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

let f be FinSeq-Location ; :: thesis: (Comput (P2,s2,k)) . f = (IExec (I,P,s)) . f
(Comput (P2,s2,((LifeSpan ((P +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialize s))) + 1))) . f = (Comput (P2,s2,(LifeSpan ((P +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialize s))))) . f by A21, SCMFSA_2:69;
hence (Comput (P2,s2,k)) . f = (Comput ((P +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialize (Initialized s)),(LifeSpan ((P +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialize (Initialized s)))))) . f by A13, XX
.= (IExec ((if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))),P,s)) . f by A10, Th87
.= (IExec (I1,P,s)) . f by A15, SCMFSA_3:4
.= (Exec ((SubFrom (a,(intloc 0))),(IExec (I,P,s)))) . f by SCMFSA6C:7
.= (IExec (I,P,s)) . f by SCMFSA_2:65 ;
:: thesis: verum

end;

A25: IC (Comput (P2,s2,((LifeSpan ((P +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialize s))) + 1))) = (Exec ((goto 0),(Comput (P2,s2,(LifeSpan ((P +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialize s))))))) . (IC ) by A18, A19, A20, Lm2
.= 0 by SCMFSA_2:69 ;
hence IC (Comput (P2,s2,k)) = 0 ; :: thesis: for n being Element of NAT st n <= k holds
IC (Comput (P2,s2,n)) in dom (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))
let n be Element of NAT ; :: thesis: ( n <= k implies IC (Comput (P2,s2,n)) in dom (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) )
assume A26: n <= k ; :: thesis: IC (Comput (P2,s2,n)) in dom (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))

per cases ( n <= LifeSpan ((P +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialize s)) or n = (LifeSpan ((P +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialize s))) + 1 ) by A26, NAT_1:8;

suppose A27: n <= LifeSpan ((P +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialize s)) ; :: thesis: IC (Comput (P2,s2,n)) in dom (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))

A28: I1 is_halting_on s,P by SCMFSA7B:19;
A29: I1 is_closed_on s,P by SCMFSA7B:18;
then A30: if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))) is_closed_on s,P by A8, A28, SCMFSA8B:15;
if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))) is_halting_on s,P by A8, A29, A28, SCMFSA8B:15;
then Comput ((P +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialize s),n) = Comput (P2,s2,n) by A27, A30, Th109;
then A31: IC (Comput (P2,s2,n)) = IC (Comput ((P +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialize s),n)) ;
IC (Comput ((P +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialize s),n)) in dom (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) by A30, SCMFSA7B:def 6;
hence IC (Comput (P2,s2,n)) in dom (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) by A31, FUNCT_4:99; :: thesis: verum

end;

suppose A32: n = (LifeSpan ((P +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Initialize s))) + 1 ; :: thesis: IC (Comput (P2,s2,n)) in dom (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))

card (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) = card (dom (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))))
.= card (dom (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) by FUNCT_4:99
.= card (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) ;
hence IC (Comput (P2,s2,n)) in dom (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) by A25, A32, AFINSQ_1:66; :: thesis: verum

end;

end;