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 not I destroysdestroy 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 2),(I ';' (SubFrom a,(intloc 0 ))))) +* (Start-At 0 ,SCM+FSA )) & k = (LifeSpan (ProgramPart (s +* ((if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At 0 ,SCM+FSA )))),(s +* ((if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At 0 ,SCM+FSA )))) + 1 & (Comput (ProgramPart s2),s2,k) . a = (s . a) - 1 & (Comput (ProgramPart s2),s2,k) . (intloc 0 ) = 1 & ( for b being read-write Int-Location st b <> a holds
(Comput (ProgramPart s2),s2,k) . b = (IExec I,s) . b ) & ( for f being FinSeq-Location holds (Comput (ProgramPart s2),s2,k) . f = (IExec I,s) . f ) & IC (Comput (ProgramPart s2),s2,k) = 0 & ( for n being Element of NAT st n <= k holds
IC (Comput (ProgramPart s2),s2,n) in dom (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) ) )
set A = NAT ;
let I be parahalting good Program of SCM+FSA ; :: thesis: for a being read-write Int-Location st not I destroysdestroy 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 2),(I ';' (SubFrom a,(intloc 0 ))))) +* (Start-At 0 ,SCM+FSA )) & k = (LifeSpan (ProgramPart (s +* ((if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At 0 ,SCM+FSA )))),(s +* ((if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At 0 ,SCM+FSA )))) + 1 & (Comput (ProgramPart s2),s2,k) . a = (s . a) - 1 & (Comput (ProgramPart s2),s2,k) . (intloc 0 ) = 1 & ( for b being read-write Int-Location st b <> a holds
(Comput (ProgramPart s2),s2,k) . b = (IExec I,s) . b ) & ( for f being FinSeq-Location holds (Comput (ProgramPart s2),s2,k) . f = (IExec I,s) . f ) & IC (Comput (ProgramPart s2),s2,k) = 0 & ( for n being Element of NAT st n <= k holds
IC (Comput (ProgramPart s2),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 destroysdestroy 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 2),(I ';' (SubFrom a,(intloc 0 ))))) +* (Start-At 0 ,SCM+FSA )) & k = (LifeSpan (ProgramPart (s +* ((if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At 0 ,SCM+FSA )))),(s +* ((if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At 0 ,SCM+FSA )))) + 1 & (Comput (ProgramPart s2),s2,k) . a = (s . a) - 1 & (Comput (ProgramPart s2),s2,k) . (intloc 0 ) = 1 & ( for b being read-write Int-Location st b <> a holds
(Comput (ProgramPart s2),s2,k) . b = (IExec I,s) . b ) & ( for f being FinSeq-Location holds (Comput (ProgramPart s2),s2,k) . f = (IExec I,s) . f ) & IC (Comput (ProgramPart s2),s2,k) = 0 & ( for n being Element of NAT st n <= k holds
IC (Comput (ProgramPart s2),s2,n) in dom (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) ) ) )
assume A1: not I destroysdestroy 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 2),(I ';' (SubFrom a,(intloc 0 ))))) +* (Start-At 0 ,SCM+FSA )) & k = (LifeSpan (ProgramPart (s +* ((if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At 0 ,SCM+FSA )))),(s +* ((if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At 0 ,SCM+FSA )))) + 1 & (Comput (ProgramPart s2),s2,k) . a = (s . a) - 1 & (Comput (ProgramPart s2),s2,k) . (intloc 0 ) = 1 & ( for b being read-write Int-Location st b <> a holds
(Comput (ProgramPart s2),s2,k) . b = (IExec I,s) . b ) & ( for f being FinSeq-Location holds (Comput (ProgramPart s2),s2,k) . f = (IExec I,s) . f ) & IC (Comput (ProgramPart s2),s2,k) = 0 & ( for n being Element of NAT st n <= k holds
IC (Comput (ProgramPart s2),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 P = if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )));
set s1 = s +* ((if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At 0 ,SCM+FSA ));
A2: I1 is_halting_on s by SCMFSA7B:25;
set Is = (Initialized s) +* ((if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At 0 ,SCM+FSA ));
A3: intloc 0 in dom s by SCMFSA_2:66;
assume 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 2),(I ';' (SubFrom a,(intloc 0 ))))) +* (Start-At 0 ,SCM+FSA )) & k = (LifeSpan (ProgramPart (s +* ((if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At 0 ,SCM+FSA )))),(s +* ((if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At 0 ,SCM+FSA )))) + 1 & (Comput (ProgramPart s2),s2,k) . a = (s . a) - 1 & (Comput (ProgramPart s2),s2,k) . (intloc 0 ) = 1 & ( for b being read-write Int-Location st b <> a holds
(Comput (ProgramPart s2),s2,k) . b = (IExec I,s) . b ) & ( for f being FinSeq-Location holds (Comput (ProgramPart s2),s2,k) . f = (IExec I,s) . f ) & IC (Comput (ProgramPart s2),s2,k) = 0 & ( for n being Element of NAT st n <= k holds
IC (Comput (ProgramPart s2),s2,n) in dom (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) ) ) )
then A4: s +* ((intloc 0 ) .--> 1) = s by A3, FUNCT_7:111;
A5: I1 is_closed_on Initialized s by SCMFSA7B:24;
A6: I1 is_halting_on Initialized s by SCMFSA7B:25;
assume A7: 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 2),(I ';' (SubFrom a,(intloc 0 ))))) +* (Start-At 0 ,SCM+FSA )) & k = (LifeSpan (ProgramPart (s +* ((if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At 0 ,SCM+FSA )))),(s +* ((if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At 0 ,SCM+FSA )))) + 1 & (Comput (ProgramPart s2),s2,k) . a = (s . a) - 1 & (Comput (ProgramPart s2),s2,k) . (intloc 0 ) = 1 & ( for b being read-write Int-Location st b <> a holds
(Comput (ProgramPart s2),s2,k) . b = (IExec I,s) . b ) & ( for f being FinSeq-Location holds (Comput (ProgramPart s2),s2,k) . f = (IExec I,s) . f ) & IC (Comput (ProgramPart s2),s2,k) = 0 & ( for n being Element of NAT st n <= k holds
IC (Comput (ProgramPart s2),s2,n) in dom (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) ) )
then A8: (Initialized s) . a > 0 by SCMFSA6C:3;
then A9: if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))) is_halting_on Initialized s by A5, A6, SCMFSA8B:18;
A10: if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))) is_closed_on Initialized s by A8, A5, A6, SCMFSA8B:18;
take s2 = s +* ((loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) +* (Start-At 0 ,SCM+FSA )); :: thesis: ex k being Element of NAT st
( s2 = s +* ((loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) +* (Start-At 0 ,SCM+FSA )) & k = (LifeSpan (ProgramPart (s +* ((if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At 0 ,SCM+FSA )))),(s +* ((if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At 0 ,SCM+FSA )))) + 1 & (Comput (ProgramPart s2),s2,k) . a = (s . a) - 1 & (Comput (ProgramPart s2),s2,k) . (intloc 0 ) = 1 & ( for b being read-write Int-Location st b <> a holds
(Comput (ProgramPart s2),s2,k) . b = (IExec I,s) . b ) & ( for f being FinSeq-Location holds (Comput (ProgramPart s2),s2,k) . f = (IExec I,s) . f ) & IC (Comput (ProgramPart s2),s2,k) = 0 & ( for n being Element of NAT st n <= k holds
IC (Comput (ProgramPart s2),s2,n) in dom (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) ) )
take k = (LifeSpan (ProgramPart (s +* ((if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At 0 ,SCM+FSA )))),(s +* ((if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At 0 ,SCM+FSA )))) + 1; :: thesis: ( s2 = s +* ((loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) +* (Start-At 0 ,SCM+FSA )) & k = (LifeSpan (ProgramPart (s +* ((if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At 0 ,SCM+FSA )))),(s +* ((if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At 0 ,SCM+FSA )))) + 1 & (Comput (ProgramPart s2),s2,k) . a = (s . a) - 1 & (Comput (ProgramPart s2),s2,k) . (intloc 0 ) = 1 & ( for b being read-write Int-Location st b <> a holds
(Comput (ProgramPart s2),s2,k) . b = (IExec I,s) . b ) & ( for f being FinSeq-Location holds (Comput (ProgramPart s2),s2,k) . f = (IExec I,s) . f ) & IC (Comput (ProgramPart s2),s2,k) = 0 & ( for n being Element of NAT st n <= k holds
IC (Comput (ProgramPart s2),s2,n) in dom (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) ) )
thus ( s2 = s +* ((loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) +* (Start-At 0 ,SCM+FSA )) & k = (LifeSpan (ProgramPart (s +* ((if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At 0 ,SCM+FSA )))),(s +* ((if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At 0 ,SCM+FSA )))) + 1 ) ; :: thesis: ( (Comput (ProgramPart s2),s2,k) . a = (s . a) - 1 & (Comput (ProgramPart s2),s2,k) . (intloc 0 ) = 1 & ( for b being read-write Int-Location st b <> a holds
(Comput (ProgramPart s2),s2,k) . b = (IExec I,s) . b ) & ( for f being FinSeq-Location holds (Comput (ProgramPart s2),s2,k) . f = (IExec I,s) . f ) & IC (Comput (ProgramPart s2),s2,k) = 0 & ( for n being Element of NAT st n <= k holds
IC (Comput (ProgramPart s2),s2,n) in dom (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) ) )
A11: dom (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))) misses dom (Start-At 0 ,SCM+FSA ) by SF_MASTR:64;
Initialized s = (s +* ((intloc 0 ) .--> 1)) +* (Start-At 0 ,SCM+FSA ) by SCMFSA6A:def 4;
then A12: (Initialized s) +* ((if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At 0 ,SCM+FSA )) = (s +* (Start-At 0 ,SCM+FSA )) +* ((Start-At 0 ,SCM+FSA ) +* (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) by A4, A11, FUNCT_4:36
.= ((s +* (Start-At 0 ,SCM+FSA )) +* (Start-At 0 ,SCM+FSA )) +* (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))) by FUNCT_4:15
.= (s +* ((Start-At 0 ,SCM+FSA ) +* (Start-At 0 ,SCM+FSA ))) +* (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))) by FUNCT_4:15
.= s +* ((Start-At 0 ,SCM+FSA ) +* (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) by FUNCT_4:15
.= s +* ((if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At 0 ,SCM+FSA )) by A11, FUNCT_4:36 ;
A13: I1 is_halting_on Initialized s by SCMFSA7B:25;
I1 is_closed_on Initialized s by SCMFSA7B:24;
then A14: IExec (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))),s = (IExec I1,s) +* (Start-At (((card (Goto 2)) + (card I1)) + 3),SCM+FSA ) by A7, A13, SCMFSA8B:19;
then A15: (IExec (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))),s) . a = (IExec I1,s) . a by SCMFSA_3:11;
A16: I1 is_closed_on s by SCMFSA7B:24;
then A17: if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))) is_closed_on s by A7, A2, SCMFSA8B:18;
A18: if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))) is_halting_on s by A7, A16, A2, SCMFSA8B:18;
T: ProgramPart s2 = ProgramPart (Comput (ProgramPart s2),s2,(LifeSpan (ProgramPart (s +* ((if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At 0 ,SCM+FSA )))),(s +* ((if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At 0 ,SCM+FSA ))))) by AMI_1:123;
A19: Comput (ProgramPart s2),s2,((LifeSpan (ProgramPart (s +* ((if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At 0 ,SCM+FSA )))),(s +* ((if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At 0 ,SCM+FSA )))) + 1) = Following (ProgramPart s2),(Comput (ProgramPart s2),s2,(LifeSpan (ProgramPart (s +* ((if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At 0 ,SCM+FSA )))),(s +* ((if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At 0 ,SCM+FSA ))))) by AMI_1:14
.= Exec (CurInstr (ProgramPart (Comput (ProgramPart s2),s2,(LifeSpan (ProgramPart (s +* ((if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At 0 ,SCM+FSA )))),(s +* ((if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At 0 ,SCM+FSA )))))),(Comput (ProgramPart s2),s2,(LifeSpan (ProgramPart (s +* ((if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At 0 ,SCM+FSA )))),(s +* ((if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At 0 ,SCM+FSA )))))),(Comput (ProgramPart s2),s2,(LifeSpan (ProgramPart (s +* ((if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At 0 ,SCM+FSA )))),(s +* ((if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At 0 ,SCM+FSA ))))) by T ;
then A20: Comput (ProgramPart s2),s2,((LifeSpan (ProgramPart (s +* ((if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At 0 ,SCM+FSA )))),(s +* ((if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At 0 ,SCM+FSA )))) + 1) = Exec (goto 0 ),(Comput (ProgramPart s2),s2,(LifeSpan (ProgramPart (s +* ((if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At 0 ,SCM+FSA )))),(s +* ((if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At 0 ,SCM+FSA ))))) by A17, A18, Lm2, T;

A21: now

let b be Int-Location ; :: thesis: (Comput (ProgramPart s2),s2,((LifeSpan (ProgramPart (s +* ((if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At 0 ,SCM+FSA )))),(s +* ((if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At 0 ,SCM+FSA )))) + 1)) . b = (Comput (ProgramPart ((Initialized s) +* ((if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At 0 ,SCM+FSA )))),((Initialized s) +* ((if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At 0 ,SCM+FSA ))),(LifeSpan (ProgramPart ((Initialized s) +* ((if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At 0 ,SCM+FSA )))),((Initialized s) +* ((if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At 0 ,SCM+FSA ))))) . b
(Comput (ProgramPart s2),s2,((LifeSpan (ProgramPart (s +* ((if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At 0 ,SCM+FSA )))),(s +* ((if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At 0 ,SCM+FSA )))) + 1)) . b = (Comput (ProgramPart s2),s2,(LifeSpan (ProgramPart (s +* ((if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At 0 ,SCM+FSA )))),(s +* ((if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At 0 ,SCM+FSA ))))) . b by A20, SCMFSA_2:95;
hence (Comput (ProgramPart s2),s2,((LifeSpan (ProgramPart (s +* ((if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At 0 ,SCM+FSA )))),(s +* ((if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At 0 ,SCM+FSA )))) + 1)) . b = (Comput (ProgramPart ((Initialized s) +* ((if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At 0 ,SCM+FSA )))),((Initialized s) +* ((if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At 0 ,SCM+FSA ))),(LifeSpan (ProgramPart ((Initialized s) +* ((if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At 0 ,SCM+FSA )))),((Initialized s) +* ((if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At 0 ,SCM+FSA ))))) . b by A17, A18, A12, Th109, SCMFSA10:92; :: thesis: verum

end;

then (Comput (ProgramPart s2),s2,((LifeSpan (ProgramPart (s +* ((if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At 0 ,SCM+FSA )))),(s +* ((if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At 0 ,SCM+FSA )))) + 1)) . a = (Comput (ProgramPart ((Initialized s) +* ((if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At 0 ,SCM+FSA )))),((Initialized s) +* ((if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At 0 ,SCM+FSA ))),(LifeSpan (ProgramPart ((Initialized s) +* ((if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At 0 ,SCM+FSA )))),((Initialized s) +* ((if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At 0 ,SCM+FSA ))))) . a
.= (IExec (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))),s) . a by A9, Th87 ;
hence (Comput (ProgramPart s2),s2,k) . a = (Comput (ProgramPart ((Initialized s) +* (I1 +* (Start-At 0 ,SCM+FSA )))),((Initialized s) +* (I1 +* (Start-At 0 ,SCM+FSA ))),(LifeSpan (ProgramPart ((Initialized s) +* (I1 +* (Start-At 0 ,SCM+FSA )))),((Initialized s) +* (I1 +* (Start-At 0 ,SCM+FSA ))))) . a by A13, A15, Th87
.= (s . a) - 1 by A1, Th98 ;
:: thesis: ( (Comput (ProgramPart s2),s2,k) . (intloc 0 ) = 1 & ( for b being read-write Int-Location st b <> a holds
(Comput (ProgramPart s2),s2,k) . b = (IExec I,s) . b ) & ( for f being FinSeq-Location holds (Comput (ProgramPart s2),s2,k) . f = (IExec I,s) . f ) & IC (Comput (ProgramPart s2),s2,k) = 0 & ( for n being Element of NAT st n <= k holds
IC (Comput (ProgramPart s2),s2,n) in dom (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) ) )
A22: if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))) is good by Th115;
(Comput (ProgramPart s2),s2,((LifeSpan (ProgramPart (s +* ((if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At 0 ,SCM+FSA )))),(s +* ((if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At 0 ,SCM+FSA )))) + 1)) . (intloc 0 ) = (Comput (ProgramPart ((Initialized s) +* ((if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At 0 ,SCM+FSA )))),((Initialized s) +* ((if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At 0 ,SCM+FSA ))),(LifeSpan (ProgramPart ((Initialized s) +* ((if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At 0 ,SCM+FSA )))),((Initialized s) +* ((if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At 0 ,SCM+FSA ))))) . (intloc 0 ) by A21
.= 1 by A9, A10, A22, Th96 ;
hence (Comput (ProgramPart s2),s2,k) . (intloc 0 ) = 1 ; :: thesis: ( ( for b being read-write Int-Location st b <> a holds
(Comput (ProgramPart s2),s2,k) . b = (IExec I,s) . b ) & ( for f being FinSeq-Location holds (Comput (ProgramPart s2),s2,k) . f = (IExec I,s) . f ) & IC (Comput (ProgramPart s2),s2,k) = 0 & ( for n being Element of NAT st n <= k holds
IC (Comput (ProgramPart s2),s2,n) in dom (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) ) )

hereby :: thesis: ( ( for f being FinSeq-Location holds (Comput (ProgramPart s2),s2,k) . f = (IExec I,s) . f ) & IC (Comput (ProgramPart s2),s2,k) = 0 & ( for n being Element of NAT st n <= k holds
IC (Comput (ProgramPart s2),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 (ProgramPart s2),s2,k) . b = (IExec I,s) . b )
assume A23: b <> a ; :: thesis: (Comput (ProgramPart s2),s2,k) . b = (IExec I,s) . b
thus (Comput (ProgramPart s2),s2,k) . b = (Comput (ProgramPart ((Initialized s) +* ((if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At 0 ,SCM+FSA )))),((Initialized s) +* ((if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At 0 ,SCM+FSA ))),(LifeSpan (ProgramPart ((Initialized s) +* ((if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At 0 ,SCM+FSA )))),((Initialized s) +* ((if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At 0 ,SCM+FSA ))))) . b by A21
.= (IExec (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))),s) . b by A9, Th87
.= (IExec I1,s) . b by A14, SCMFSA_3:11
.= (Exec (SubFrom a,(intloc 0 )),(IExec I,s)) . b by SCMFSA6C:7
.= (IExec I,s) . b by A23, SCMFSA_2:91 ; :: thesis: verum

end;

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

let f be FinSeq-Location ; :: thesis: (Comput (ProgramPart s2),s2,k) . f = (IExec I,s) . f
(Comput (ProgramPart s2),s2,((LifeSpan (ProgramPart (s +* ((if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At 0 ,SCM+FSA )))),(s +* ((if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At 0 ,SCM+FSA )))) + 1)) . f = (Comput (ProgramPart s2),s2,(LifeSpan (ProgramPart (s +* ((if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At 0 ,SCM+FSA )))),(s +* ((if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At 0 ,SCM+FSA ))))) . f by A20, SCMFSA_2:95;
hence (Comput (ProgramPart s2),s2,k) . f = (Comput (ProgramPart ((Initialized s) +* ((if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At 0 ,SCM+FSA )))),((Initialized s) +* ((if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At 0 ,SCM+FSA ))),(LifeSpan (ProgramPart ((Initialized s) +* ((if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At 0 ,SCM+FSA )))),((Initialized s) +* ((if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At 0 ,SCM+FSA ))))) . f by A17, A18, A12, Th109, SCMFSA10:93
.= (IExec (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))),s) . f by A9, Th87
.= (IExec I1,s) . f by A14, 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;

A24: IC (Comput (ProgramPart s2),s2,((LifeSpan (ProgramPart (s +* ((if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At 0 ,SCM+FSA )))),(s +* ((if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At 0 ,SCM+FSA )))) + 1)) = (Exec (goto 0 ),(Comput (ProgramPart s2),s2,(LifeSpan (ProgramPart (s +* ((if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At 0 ,SCM+FSA )))),(s +* ((if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At 0 ,SCM+FSA )))))) . (IC SCM+FSA ) by A17, A18, A19, Lm2, T
.= 0 by SCMFSA_2:95 ;
hence IC (Comput (ProgramPart s2),s2,k) = 0 ; :: thesis: for n being Element of NAT st n <= k holds
IC (Comput (ProgramPart s2),s2,n) in dom (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))

hereby :: thesis: verum

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

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

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

A27: I1 is_halting_on s by SCMFSA7B:25;
A28: I1 is_closed_on s by SCMFSA7B:24;
then A29: if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))) is_closed_on s by A7, A27, SCMFSA8B:18;
if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))) is_halting_on s by A7, A28, A27, SCMFSA8B:18;
then Comput (ProgramPart (s +* ((if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At 0 ,SCM+FSA )))),(s +* ((if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At 0 ,SCM+FSA ))),n, Comput (ProgramPart s2),s2,n equal_outside NAT by A26, A29, Th109;
then A30: IC (Comput (ProgramPart s2),s2,n) = IC (Comput (ProgramPart (s +* ((if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At 0 ,SCM+FSA )))),(s +* ((if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At 0 ,SCM+FSA ))),n) by SCMFSA8A:6;
IC (Comput (ProgramPart (s +* ((if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At 0 ,SCM+FSA )))),(s +* ((if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At 0 ,SCM+FSA ))),n) in dom (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))) by A29, SCMFSA7B:def 7;
hence IC (Comput (ProgramPart s2),s2,n) in dom (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) by A30, FUNCT_4:105; :: thesis: verum

end;

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

A32: card (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))) = ((card (Goto 2)) + (card I1)) + 4 by SCMFSA8B:14
.= ((card I1) + 1) + 4 by SCMFSA8A:29
.= ((card I1) + 3) + 2 ;
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:105
.= card (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))) ;
hence IC (Comput (ProgramPart s2),s2,n) in dom (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) by A24, A31, A32, AFINSQ_1:70; :: thesis: verum

end;

end;

end;